package dolmen_loop

  1. Overview
  2. Docs

This modules defines the smallest signatures for a solver state that allow to instantiate the Parser.Pipe functor.

common interface

include Common
type t

The type of state

exception Error of t

Convenient exception.

val warn : ?loc:Dolmen.Std.Loc.full -> t -> 'a Report.Warning.t -> 'a -> t

Emit a warning

val error : ?loc:Dolmen.Std.Loc.full -> t -> 'a Report.Error.t -> 'a -> t

Emit an error.

type term

The type of solver terms.

val input_file_loc : t -> Dolmen.Std.Loc.file

CUrrent input file location meta-data.

val set_input_file_loc : t -> Dolmen.Std.Loc.file -> t

Set the input file location meta-data.

val prelude : t -> string

Some prelude to print at the begining of lines when in interactive mode.

val is_interactive : t -> bool

Whether we are running in interactive mode.

val set_mode : t -> mode -> t
val set_lang : t -> Logic.language -> t

Set the input language.

val input_mode : t -> mode option

Return the current mode (if any).

val input_lang : t -> Logic.language option

Return the input language (if any).

val input_dir : t -> string

Return the directory of the input source (e.g. the directory of the input file, or the current directory if in interactive mode).

val input_source : t -> source

Return the input source.