package dolmen_model

  1. Overview
  2. Docs

Parameters

module Parse : Dolmen_loop.Parser.S with type state := State.t and type 'a key := 'a State.key

Signature

val pipe : string
val check_model : bool State.key
val check_state : State.t t State.key
val init : check_model:bool -> State.t -> State.t
val builtins : Env.builtins
val eval : reraise_for_delayed_eval:bool -> file:'a Dolmen_loop__State.file -> loc:Dolmen.Std.Loc.full -> State.t -> Model.t -> Dolmen_model.Fun.E.term -> Value.t
val pack_abstract_defs : loc:Dolmen.Std.Loc.full -> file:Dolmen_loop.Logic.language file -> [< `Instanceof of 'a | `Term_def of 'b * 'c * Dolmen.Std.Expr.Term.ty_var list * Dolmen.Std.Expr.Term.Var.t list * Dolmen.Std.Expr.Term.t | `Type_alias of 'd ] list -> ('c * Dolmen.Std.Expr.Term.t) list located
val are_defs_declared : State.t -> Dolmen.Std.Statement.defs -> State.t * bool
val gen_answer : (State.t -> 'a * Dolmen.Std.Answer.t option) -> State.t -> 'a * answer
val next_answer : State.t -> State.t * answer
val get_answer : file:'a Dolmen_loop__State.file -> loc:Dolmen.Std.Loc.full -> State.t -> State.t * answer
val eval_loop : State.t -> Dolmen.Std.Statement.defs list -> Model.t -> acc list Dolmen_model.Model.C.t -> bool located list -> acc -> State.t * Dolmen.Std.Statement.defs list * Model.t * acc list Dolmen_model.Model.C.t * bool located list
val eval_newly_defined : State.t -> Model.t -> acc list Dolmen_model.Model.C.t -> bool located list -> Dolmen_model.Model.C.key list -> State.t * Model.t * acc list Dolmen_model.Model.C.t * bool located list
val eval_delayed : State.t -> Model.t -> acc list Dolmen_model.Model.C.t -> bool located list -> (Dolmen_model.Model.C.key * acc list) list -> State.t * Model.t * acc list Dolmen_model.Model.C.t * bool located list
val eval_acc_direct : reraise:bool -> State.t -> Model.t -> acc list Dolmen_model.Model.C.t -> bool located list -> acc -> State.t * Model.t * acc list Dolmen_model.Model.C.t * bool located list
val eval_acc : State.t -> Model.t -> acc list Dolmen_model.Model.C.t -> bool located list -> acc -> State.t * Model.t * acc list Dolmen_model.Model.C.t * bool located list
val eval_def : reraise:bool -> State.t -> Model.t -> acc list Dolmen_model.Model.C.t -> bool located list -> (Dolmen.Std.Expr.Term.Const.t * Dolmen.Std.Expr.Term.t) list located -> State.t * Model.t * acc list Dolmen_model.Model.C.t * bool located list
val eval_hyp : reraise:bool -> State.t -> Model.t -> term located -> State.t
val eval_goal : reraise:bool -> State.t -> Model.t -> bool located list -> term located -> State.t * bool located list
val eval_clause : reraise:bool -> State.t -> Model.t -> Dolmen.Std.Expr.Term.t list located -> State.t
val check_acc : State.t -> acc -> State.t
val check_defs : State.t -> file:Dolmen_loop.Logic.language file -> loc:Dolmen.Std.Loc.full -> [< `Instanceof of 'a | `Term_def of 'b * cst * Dolmen.Std.Expr.Term.ty_var list * Dolmen.Std.Expr.Term.Var.t list * Dolmen.Std.Expr.Term.t | `Type_alias of 'c ] list -> State.t
OCaml

Innovation. Community. Security.