dolmen_model 0.8 · OCaml Package

type model = Model.t

type cst = Dolmen.Std.Expr.term_cst

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

type answer =

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

type 'st answers =

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

type 't located = {

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

}

type '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;

}

val empty : unit -> 'a t

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

val code : Dolmen_loop.Code.t

val type_def_in_model : unit Dolmen_loop.Report.Error.t

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

val cannot_check_proofs : unit Dolmen_loop.Report.Warning.t

val error_in_response : unit Dolmen_loop.Report.Error.t

val missing_answer : unit Dolmen_loop.Report.Error.t

val assertion_stack_not_supported : unit Dolmen_loop.Report.Error.t

val fo_model : unit Dolmen_loop.Report.Error.t

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

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

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

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

type 'a file = 'a Dolmen_loop.State.file

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