package dolmen_loop

  1. Overview
  2. Docs
A tool library for automated deduction tools

Install

Dune Dependency

Authors

Maintainers

Sources

dolmen-0.8.tbz
sha256=3ee4b4b028b18ab0066cb4648fa14cd4d628a3afd79455f85fb796a9969ac80c
sha512=06d455f0221814dae44d9d8614cab7c1d4fb43a383e603a92ffc9cf4a753d42c5f2a0f3c5ae64aa6cf02da769c4666b130443ae2cf8fa0918c906d46e0caec9a

doc/src/dolmen_loop/parser_intf.ml.html

Source file parser_intf.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
56
57
58
59

(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *)

module type S = sig

  type state
  (** The type of state for a whole pipeline *)

  type 'a key
  (** Keys into the state. *)

  val syntax_error_ref : bool key
  (** A key to determine whether to print a syntax error identifier/reference
      in Syntax error messages. Mainly useful when debugging syntax error messages. *)

  val interactive_prompt : (state -> string option) key
  (** The interactive prompt key. This is used to determine whether we are parsing
      in interactive mode, and if so, what prelude to print before parsing each
      toplevel phrase. *)

  val interactive_prompt_lang : state -> string option
  (** A standard implementation for the interactive prompt key/function. When the
      logic input is set to `Stdin, it will return a prompt string prelude that
      contains the currently set input language. *)

  val init :
    ?syntax_error_ref:bool ->
    ?interactive_prompt:(state -> string option) ->
    state -> state
  (** Init a state with all the relevant keys for this pipeline.
      @param syntax_error_ref : false by default.
      @param interactive_prompt : does nothing by default.
  *)

  val parse_logic :
    Dolmen.Std.Statement.t list -> state -> Logic.language State.file ->
    state * (state -> state * Dolmen.Std.Statement.t option)
  (** Parsing function. Reads a list of prelude statements, and the state and
      returns a tuple of the new state (including the detected input language),
      together with a statement generator. *)

  val parse_response :
    Dolmen.Std.Answer.t list -> state -> Response.language State.file ->
    state * (state -> state * Dolmen.Std.Answer.t option)
  (** Parsing function. Reads a list of prelude statements, and the state and
      returns a tuple of the new state (including the detected input language),
      together with a statement generator. *)

  val expand : state -> Dolmen.Std.Statement.t ->
    state * [ `Ok | `Gen of (state -> state -> state) *
                              (state -> state * Dolmen.Std.Statement.t option) ]
  (** Expand statements (such as includes). Returns the new state, and either:
      - [ `Ok ], which means the statement can be propagated as is
      - [ `Gen (flat, g) ], if the statement expands into a generator [g]. The bool [flat]
        indicates wether the statements in [g] should be treated as a single group of
        statements (with regards to timeouts, etc...), or as a list of independant statements
        (each with its own timeout...). *)

end
OCaml

Innovation. Community. Security.