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 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 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 builtins : Env.t -> Eval.Cst.t -> Value.t

val eval : 
  State.t ->
  file:'a Dolmen_loop__State.file ->
  loc:Dolmen.Std.Loc.full ->
  Fun.E.Term.t ->
  Value.t

val define_value : 
  State.t ->
  Dolmen.Std.Expr.Term.Const.t ->
  Value.t ->
  State.t

val corner_2 : 
  [> `Term_def of
       'a * 'b * 'c list * Dolmen.Std.Expr.Term.Var.t list * 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 ->
  ('d * 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 type_model : 
  State.t ->
  file:Dolmen_loop.Response.language Dolmen_loop.State.file ->
  loc:Dolmen.Std.Loc.full ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.def Dolmen.Std.Statement.group 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 ->
  Fun.E.Term.t ->
  bool

val eval_def : 
  (Dolmen.Std.Expr.Term.Const.t * Fun.E.Term.t) list located ->
  State.t ->
  State.t

val eval_hyp : State.t -> Fun.E.Term.t located -> State.t

val eval_goal : State.t -> Fun.E.Term.t located -> State.t

val eval_clause : State.t -> Fun.E.Term.t list located -> State.t

val check_aux : State.t -> 'a t -> answer -> State.t

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