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 -> ?check_state:State.t t -> State.t -> State.t
val eval : State.t -> file:'a Dolmen_loop__State.file -> loc:Dolmen.Std.Loc.full -> Dolmen_model.Fun.E.Term.t -> Value.t
val corner_2 : [> `Term_def of 'a * 'b * 'c list * Dolmen.Std.Expr.Term.Var.t list * Dolmen_model.Fun.E.Term.t ] list -> (Env.t -> Value.t -> Value.t -> Value.t) option
val pack_abstract_defs : loc:Dolmen.Std.Loc.full -> file:Dolmen_loop.Logic.language file -> [< `Term_def of 'a * 'b * Dolmen.Std.Expr.Term.ty_var list * Dolmen.Std.Expr.Term.Var.t list * Dolmen.Std.Expr.Term.t | `Type_def of 'c ] list -> ('b * Dolmen.Std.Expr.Term.t) list located
val record_defs : State.t -> loc:Dolmen.Std.Loc.full -> file:'a file -> [< `Term_def of 'b * Dolmen.Std.Expr.Term.Const.t * Dolmen.Std.Expr.Term.ty_var list * Dolmen.Std.Expr.Term.Var.t list * Dolmen.Std.Expr.Term.t | `Type_def of 'c ] list -> State.t
val get_answer : State.t -> State.t * answer option
val eval_term : State.t -> file:'a Dolmen_loop__State.file -> loc:Dolmen.Std.Loc.full -> Dolmen_model.Fun.E.Term.t -> bool
val eval_clause : State.t -> Dolmen_model.Fun.E.Term.t list located -> State.t
val check_aux : State.t -> 'a t -> answer -> State.t
OCaml

Innovation. Community. Security.