Module `Dolmen_model.Loop`Source

Sourcetype model = Model.t

Sourcetype cst = Dolmen.Std.Expr.term_cst

Sourcetype term = Dolmen.Std.Expr.Term.t

Sourcetype answer =

| Sat
| Unsat of Dolmen.Std.Loc.full
| Error of Dolmen.Std.Loc.full

Sourcetype 'st answers =

| Init
| Response_loaded of 'st -> 'st * answer option

Sourcetype 't located = {

contents : 't;
loc : Dolmen.Std.Loc.full;
file : Dolmen_loop.Logic.language Dolmen_loop.State.file;

}

Sourcetype 'st t = {

model : model;
answers : 'st answers;
defs : (cst * term) list located list;
hyps : term located list;
goals : term located list;
clauses : term list located list;

}

Sourceval empty : unit -> 'a t

Source

val pp_wrap : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a ->
  unit

Sourceval code : Dolmen_loop.Code.t

Sourceval type_def_in_model : unit Dolmen_loop.Report.Error.t

Sourceval bad_model : [ `Clause | `Goal | `Hyp ] Dolmen_loop.Report.Error.t

Sourceval cannot_check_proofs : unit Dolmen_loop.Report.Warning.t

Sourceval error_in_response : unit Dolmen_loop.Report.Error.t

Sourceval missing_answer : unit Dolmen_loop.Report.Error.t

Sourceval assertion_stack_not_supported : unit Dolmen_loop.Report.Error.t

Sourceval fo_model : unit Dolmen_loop.Report.Error.t

Sourceval undefined_variable : Dolmen.Std.Expr.Term.Var.t Dolmen_loop.Report.Error.t

Source

val undefined_constant : 
  Dolmen.Std.Expr.Term.Const.t Dolmen_loop.Report.Error.t

Sourceval unhandled_builtin : Dolmen.Std.Expr.Term.Const.t Dolmen_loop.Report.Error.t

Source

val partial_destructor : 
  (Dolmen.Std.Expr.Term.Const.t * Value.t) Dolmen_loop.Report.Error.t

Sourcetype 'a file = 'a Dolmen_loop.State.file

Source

module Make
  (State : Dolmen_loop.State.S)
  (Parse : 
    Dolmen_loop.Parser.S
      with type state := State.t
       and type 'a key := 'a State.key)
  (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)
  (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) : 
  sig ... end

package dolmen_model

Module Dolmen_model.LoopSource

Module `Dolmen_model.Loop`Source