Module `Dolmen_model.Loop`Source

Sourcetype typed_model = Model.t

Sourcetype parsed_model = Dolmen.Std.Statement.defs list

Sourcetype cst = Dolmen.Std.Expr.term_cst

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

Sourcetype 't located = {

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

}

Sourcetype acc =

| Def of (cst * term) list located
| Hyp of term located
| Goal of term located
| Clause of term list located

Sourcetype answer =

| None
| Unsat of Dolmen.Std.Loc.full
| Error of Dolmen.Std.Loc.full
| Sat of {
1. parsed : parsed_model;
2. model : typed_model;
3. evaluated_goals : bool located list;
4. delayed : acc list Model.C.t;
}
| Post_sat

Sourcetype 'st input =

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

Sourcetype 'st t = {

answer : answer;
input : 'st input;

}

Sourceval empty : 'a t

Source

val file_loc_of_acc : 
  acc ->
  Dolmen_loop.Logic.language Dolmen_loop.State.file * Dolmen.Std.Loc.full

Sourcemodule E = Dolmen.Std.Expr

Source

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

Sourceval pp_app : Format.formatter -> (E.Term.Const.t * Value.t list) -> unit

Source

val pp_defs_loc : 
  file:Dolmen.Std.Loc.file ->
  Format.formatter ->
  Dolmen.Std.Statement.defs ->
  unit

Sourceval pp_located : Format.formatter -> 'a located -> unit

Sourceval code : Dolmen_loop.Code.t

Sourceval incr_check_not_supported : unit Dolmen_loop.Report.Error.t

Sourceval type_def_in_model : unit Dolmen_loop.Report.Error.t

Source

val bad_model : 
  [ `Clause | `Goals of bool located list | `Hyp ] Dolmen_loop.Report.Error.t

Sourceval cannot_check_proofs : unit Dolmen_loop.Report.Warning.t

Source

val parsed_model : 
  (Dolmen.Std.Loc.file * Dolmen.Std.Statement.defs list)
    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_interpretation : 
  (Dolmen.Std.Expr.Term.Const.t * Value.t list) Dolmen_loop.Report.Error.t

Source

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

Source

val unhandled_float_exponand_and_mantissa : 
  (int * int) 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 env = Typer.env
       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) : 
  sig ... end

package dolmen_model

Module Dolmen_model.LoopSource

Module `Dolmen_model.Loop`Source