Make (dolmen_model.Dolmen_model.Loop.Make)

Parameters

module State : Dolmen_loop.State.S

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

module Typer : 
  Dolmen_loop.Typer.Typer_Full
    with type state := State.t
     and type 'a key := 'a State.key
     and type ty_state := Dolmen_loop.Typer.ty_state
     and type env = Dolmen_loop.Typer.T.env

module Typer_Pipe : 
  Dolmen_loop.Typer.S
    with type state := State.t
     and type 'a key := 'a State.key
     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

Signature

val core_builtins : Env.builtins

val pipe : string

val check_model : bool State.key

val check_state : State.t t State.key

val builtins : Env.builtins State.key

val init : 
  check_model:bool ->
  ?extension_builtins:Ext.t list ->
  State.t ->
  State.t

val eval : 
  reraise_for_delayed_eval:bool ->
  file:'a Dolmen_loop__State.input_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 record_defs : 
  State.t ->
  Model.t ->
  Dolmen.Std.Expr.Term.Const.t list ->
  Dolmen.Std.Statement.defs ->
  [< `Instanceof of
       'a
       * Dolmen.Std.Expr.Term.Const.t
       * Dolmen_model.Fun.E.Ty.t list
       * 'b list
       * Dolmen_model.Fun.E.Term.Var.t list
       * Dolmen.Std.Expr.Term.t
  | `Term_def of
    'c
    * 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_alias of 'd ]
    list ->
  State.t * Model.t * Dolmen.Std.Expr.Term.Const.t list

val are_defs_declared : State.t -> Dolmen.Std.Statement.defs -> State.t * bool

val type_model_aux : 
  input:Typer.input ->
  ?attrs:Dolmen.Std.Term.t list ->
  State.t ->
  Model.t ->
  Dolmen.Std.Expr.Term.Const.t list ->
  Dolmen.Std.Statement.def Dolmen.Std.Statement.group ->
  State.t * Model.t * Dolmen.Std.Expr.Term.Const.t list

val type_model_defined : 
  input:Typer.input ->
  ?attrs:Dolmen.Std.Term.t list ->
  State.t ->
  Model.t ->
  Dolmen.Std.Expr.Term.Const.t list ->
  Dolmen.Std.Statement.defs list ->
  State.t
  * Model.t
  * Dolmen.Std.Expr.Term.Const.t list
  * Dolmen.Std.Statement.defs list

val type_model_partial : 
  ?attrs:Dolmen.Std.Term.t list ->
  State.t ->
  Model.t ->
  Dolmen.Std.Statement.defs list ->
  State.t
  * Model.t
  * Dolmen.Std.Expr.Term.Const.t list
  * Dolmen.Std.Statement.defs list

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.input_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_prop : 
  reraise:bool ->
  file:Dolmen_loop.Logic.language Dolmen_loop.State.input_file ->
  loc:Dolmen.Std.Loc.full ->
  State.t ->
  Model.t ->
  Dolmen.Std.Expr.Term.t ->
  bool

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

val check_hyps : 
  State.t ->
  file:Dolmen_loop.Logic.language Dolmen_loop.State.input_file ->
  loc:Dolmen.Std.Loc.full ->
  term ->
  State.t

val check_goal : 
  State.t ->
  file:Dolmen_loop.Logic.language Dolmen_loop.State.input_file ->
  loc:Dolmen.Std.Loc.full ->
  term ->
  State.t

val check_clause : 
  State.t ->
  file:Dolmen_loop.Logic.language Dolmen_loop.State.input_file ->
  loc:Dolmen.Std.Loc.full ->
  term list ->
  State.t

val check_solve : 
  State.t ->
  file:Dolmen_loop.Logic.language Dolmen_loop.State.input_file ->
  loc:Dolmen.Std.Loc.full ->
  term list ->
  term list ->
  State.t

val check : 
  State.t ->
  Typer_Pipe.typechecked Typer_Pipe.stmt list ->
  State.t * Typer_Pipe.typechecked Typer_Pipe.stmt list