sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page
include Dolmen_loop.Typer_intf.Types
with type state := State.t
with type env = Typer.env
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 env = Typer.env
val type_check : bool State.key
type +'a stmt = {
id : Dolmen.Std.Id.t;
loc : Dolmen.Std.Loc.t;
contents : 'a;
attrs : Dolmen.Std.Term.t list;
}
Wrapper around statements. It records implicit type declarations.
type decl = [
| `Type_decl of Dolmen.Std.Expr.ty_cst * Dolmen.Std.Expr.ty_def option
| `Term_decl of Dolmen.Std.Expr.term_cst
]
The type of top-level type declarations.
A list of type declarations.
type def = [
| `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
]
The type of top-level type definitions. Type definitions are inlined and so can be ignored.
A list of definitions
type assume = [
| `Hyp of Dolmen.Std.Expr.formula
| `Goal of Dolmen.Std.Expr.formula
| `Clause of Dolmen.Std.Expr.formula list
]
The type of top-level assertion statements
type solve = [
| `Solve of Dolmen.Std.Expr.formula list * Dolmen.Std.Expr.formula list
`Solve (hyps, goals)
represents a sequent with local hypotheses hyps
and local goals goals
.
]
Top-level solve instruction
type get_info = [
| `Get_info of string
| `Get_option of string
| `Get_proof
| `Get_unsat_core
| `Get_unsat_assumptions
| `Get_model
| `Get_value of Dolmen.Std.Expr.term list
| `Get_assignment
| `Get_assertions
| `Echo of string
| `Plain of Dolmen.Std.Statement.term
]
Various info getters
type set_info = [
| `Set_logic of string * Dolmen_type.Logic.t
| `Set_info of Dolmen.Std.Statement.term
| `Set_option of Dolmen.Std.Statement.term
]
Info setters
The type of statements after typechecking
val print : Stdlib.Format.formatter -> typechecked stmt -> unit
Printing funciton for typechecked statements.
val check : State.t -> Dolmen.Std.Statement.t -> State.t * typechecked stmt
Typechecks a statement.
val typecheck :
State.t ->
Dolmen.Std.Statement.t ->
State.t * [ `Continue of typechecked stmt | `Done of unit ]
Typechecks a statement.