package dolmen_loop

  1. Overview
  2. Docs

Parameters

module S : State_intf.Typer with type ty_state := ty_state

Signature

This signature includes the requirements to instantiate the {Pipes.Make: functor

include Typer_intf.Pipe_arg with type state := S.t and type ty := Dolmen.Std.Expr.ty and type ty_var := Dolmen.Std.Expr.ty_var and type ty_cst := Dolmen.Std.Expr.ty_cst and type term := Dolmen.Std.Expr.term and type term_var := Dolmen.Std.Expr.term_var and type term_cst := Dolmen.Std.Expr.term_cst and type formula := Dolmen.Std.Expr.formula
val typecheck : S.t -> bool
val reset : S.t -> ?loc:Dolmen.Std.Loc.t -> unit -> S.t
val reset_assertions : S.t -> ?loc:Dolmen.Std.Loc.t -> unit -> S.t
val push : S.t -> ?loc:Dolmen.Std.Loc.t -> int -> S.t
val pop : S.t -> ?loc:Dolmen.Std.Loc.t -> int -> S.t
val set_logic : S.t -> ?loc:Dolmen.Std.Loc.t -> string -> S.t
val decls : S.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.decls -> S.t * [ `Type_decl of Dolmen.Std.Expr.ty_cst | `Term_decl of Dolmen.Std.Expr.term_cst ] list
val terms : S.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> S.t * Dolmen.Std.Expr.term list
val formula : S.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> S.t * Dolmen.Std.Expr.formula
val formulas : S.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> S.t * Dolmen.Std.Expr.formula list
val report_error : S.t -> T.error -> S.t

Report a typing error by calling the appropriate state function.

val report_warning : S.t -> T.warning -> S.t

Return a typing warning by calling the appropriate state function.

val additional_builtins : T.builtin_symbols ref

This reference can be modified to parse new builtin symbols. By default no additional builtin symbols are parsed. It is added for all the languages except Dimacs, and iCNF.