package forester

  1. Overview
  2. Docs

Source file Tape_effect.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
(*
 * SPDX-FileCopyrightText: 2024 The Forester Project Contributors
 *
 * SPDX-License-Identifier: GPL-3.0-or-later
 *)

open Forester_core

module type S = sig
  val run : tape: Syn.t -> (unit -> 'a) -> 'a
  val pop_node_opt : unit -> Syn.node Range.located option

  val pop_arg_opt : unit -> Syn.t Range.located option
  val pop_arg : loc: Range.t option -> Syn.t Range.located
  val pop_args : unit -> Syn.t Range.located list
end

module Make () = struct
  open Bwd

  module T = Algaeff.State.Make(struct type t = Syn.t end)

  let pop_node_opt () =
    match T.get () with
    | node :: nodes ->
      T.set nodes;
      Some node
    | [] -> None

  let pop_arg_opt () =
    match T.get () with
    | Range.{value = Syn.Group (Braces, arg); _} as node :: nodes ->
      T.set nodes;
      Some ({node with value = arg})
    | Range.{value = (Syn.Sym _ | Syn.Verbatim _ | Syn.Var _ | Syn.Dx_sequent _ | Syn.Dx_query _); _} as node :: nodes ->
      T.set nodes;
      Some ({node with value = [node]})
    | _ -> None

  let pop_arg ~loc =
    match pop_arg_opt () with
    | Some arg -> arg
    | None -> Reporter.fatal ?loc (Type_error {got = None; expected = [Argument]})

  let pop_args () =
    let rec loop acc =
      match pop_arg_opt () with
      | Some arg -> loop @@ Bwd.Snoc (acc, arg)
      | None -> Bwd.prepend acc []
    in
    loop Bwd.Emp

  let run ~tape =
    T.run ~init: tape
end