Module D_loop.Typer

type state = State.t
type ty_state = Dolmen_loop__Typer.ty_state
type env = Dolmen_loop__Typer.T.env
type !'a fragment = 'a Dolmen_loop__Typer.T.fragment
type error = Dolmen_loop__Typer.T.error
type warning = Dolmen_loop__Typer.T.warning
type builtin_symbols = Dolmen_loop__Typer.T.builtin_symbols
type input = [
  1. | `Logic of Dolmen_loop.Logic.language Dolmen_loop.State.file
  2. | `Response of Dolmen_loop.Response.language Dolmen_loop.State.file
]
type lang = [
  1. | `Logic of Dolmen_loop.Logic.language
  2. | `Response of Dolmen_loop.Response.language
]
type decl = [
  1. | `Term_decl of Dolmen.Std.Expr.term_cst
  2. | `Type_decl of Dolmen.Std.Expr.ty_cst * Dolmen.Std.Expr.ty_def option
]
type def = [
  1. | `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
  2. | `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
  3. | `Type_alias of Dolmen.Std.Id.t * Dolmen.Std.Expr.ty_cst * Dolmen.Std.Expr.ty_var list * Dolmen.Std.Expr.ty
]
type !'a ret = 'a Dolmen_loop__Typer.Typer(State).ret = {
  1. implicit_decls : decl list;
  2. implicit_defs : def list;
  3. ret : 'a;
}
val reset : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state
val reset_assertions : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state
val push : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> state
val pop : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> state
val set_logic : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> string -> state * Dolmen_type.Logic.t
val decls : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.decls -> state * decl list ret
val defs : mode:[ `Create_id | `Use_declared_id ] -> state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.defs -> state * def list ret
val terms : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * Dolmen.Std.Expr.term list ret
val formula : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> state * Dolmen.Std.Expr.formula ret
val formulas : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * Dolmen.Std.Expr.formula list ret
val typing_wrap : ?attrs:Dolmen.Std.Term.t list -> ?loc:Dolmen.Std.Loc.t -> input:input -> state -> f:(env -> 'a) -> state * 'a
module Ext : sig ... end
val ty_state : ty_state State.key
val check_model : bool State.key
val smtlib2_forced_logic : string option State.key
val extension_builtins : Ext.t list State.key
val additional_builtins : (state -> lang -> builtin_symbols) State.key
val init : ?ty_state:ty_state -> ?smtlib2_forced_logic:string option -> ?extension_builtins:Ext.t list -> ?additional_builtins:(state -> lang -> builtin_symbols) -> state -> state
val report_error : input:input -> state -> error -> state
val report_warning : input:input -> state -> warning -> state
val pop_inferred_model_constants : state -> Dolmen.Std.Expr.term_cst list