package dolmen_model
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type env = Dolmen_loop.Typer.T.env
The type of the typechecker environment.
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
Force the typechecker to use the given logic (instead of using the one declared in the `set-logic` statement).
This signature includes the requirements to instantiate the {Pipes.Make: functor
include Dolmen_loop.Typer_intf.Typer
with type env := env
and 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 ty_def := Dolmen.Std.Expr.ty_def
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 env := env
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 ty_def := Dolmen.Std.Expr.ty_def
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 * Dolmen_type.Logic.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_alias 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
| `Instanceof of
Dolmen.Std.Id.t
* Dolmen.Std.Expr.term_cst
* Dolmen.Std.Expr.ty list
* 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 * Dolmen.Std.Expr.ty_def option
| `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
val typing_wrap :
?attrs:Dolmen.Std.Term.t list ->
?loc:Dolmen.Std.Loc.t ->
input:input ->
State.t ->
f:(env -> 'a) ->
State.t * 'a
val init :
?ty_state:Dolmen_loop.Typer.ty_state ->
?smtlib2_forced_logic:string option ->
?additional_builtins:(State.t -> lang -> builtin_symbols) ->
State.t ->
State.t
val additional_builtins : (State.t -> lang -> builtin_symbols) State.key
Add new builtin symbols to the typechecker, depending on the current language.
Note. The additional builtins are never used for Dimacs and iCNF.
Report a typing error by calling the appropriate state function.
Return a typing warning by calling the appropriate state function.
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)"
>