package dolmen_model
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val ty_state : Dolmen_loop.Typer.ty_state State.key
Key to store the local typechecking state in the global pipeline state.
val check_model : bool State.key
The typechecker needs to know whether we are checking models or not.
val smtlib2_forced_logic : string option State.key
The typechecker needs to know whether we are checking models or not.
val init :
?ty_state:Dolmen_loop.Typer.ty_state ->
?smtlib2_forced_logic:string option ->
State.t ->
State.t
This signature includes the requirements to instantiate the {Pipes.Make: functor
include Dolmen_loop.Typer_intf.Typer
with type state := State.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
include Dolmen_loop.Typer_intf.Types
with type state := State.t
with type ty := Dolmen.Std.Expr.ty
with type ty_var := Dolmen.Std.Expr.ty_var
with type ty_cst := Dolmen.Std.Expr.ty_cst
with type term := Dolmen.Std.Expr.term
with type term_var := Dolmen.Std.Expr.term_var
with type term_cst := Dolmen.Std.Expr.term_cst
with type formula := Dolmen.Std.Expr.formula
type input = [
| `Logic of Dolmen_loop.Logic.language Dolmen_loop.State.file
| `Response of Dolmen_loop.Response.language Dolmen_loop.State.file
]
val reset : State.t -> ?loc:Dolmen.Std.Loc.t -> unit -> State.t
val reset_assertions : State.t -> ?loc:Dolmen.Std.Loc.t -> unit -> State.t
val push : State.t -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> State.t
val pop : State.t -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> State.t
val set_logic :
State.t ->
input:input ->
?loc:Dolmen.Std.Loc.t ->
string ->
State.t
val defs :
mode:[ `Create_id | `Use_declared_id ] ->
State.t ->
input:input ->
?loc:Dolmen.Std.Loc.t ->
?attrs:Dolmen.Std.Term.t list ->
Dolmen.Std.Statement.defs ->
State.t
* [ `Type_def of
Dolmen.Std.Id.t
* Dolmen.Std.Expr.ty_cst
* Dolmen.Std.Expr.ty_var list
* Dolmen.Std.Expr.ty
| `Term_def of
Dolmen.Std.Id.t
* Dolmen.Std.Expr.term_cst
* Dolmen.Std.Expr.ty_var list
* Dolmen.Std.Expr.term_var list
* Dolmen.Std.Expr.term ]
list
val decls :
State.t ->
input:input ->
?loc:Dolmen.Std.Loc.t ->
?attrs:Dolmen.Std.Term.t list ->
Dolmen.Std.Statement.decls ->
State.t
* [ `Type_decl of Dolmen.Std.Expr.ty_cst
| `Term_decl of Dolmen.Std.Expr.term_cst ]
list
val terms :
State.t ->
input:input ->
?loc:Dolmen.Std.Loc.t ->
?attrs:Dolmen.Std.Term.t list ->
Dolmen.Std.Term.t list ->
State.t * Dolmen.Std.Expr.term list
val formula :
State.t ->
input:input ->
?loc:Dolmen.Std.Loc.t ->
?attrs:Dolmen.Std.Term.t list ->
goal:bool ->
Dolmen.Std.Term.t ->
State.t * Dolmen.Std.Expr.formula
val formulas :
State.t ->
input:input ->
?loc:Dolmen.Std.Loc.t ->
?attrs:Dolmen.Std.Term.t list ->
Dolmen.Std.Term.t list ->
State.t * Dolmen.Std.Expr.formula list
Report a typing error by calling the appropriate state function.
Return a typing warning by calling the appropriate state function.
val additional_builtins : builtin_symbols Stdlib.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.
val pop_inferred_model_constants : State.t -> Dolmen.Std.Expr.term_cst list
TODO:doc
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>