Module D_loop.Typer_Pipe

type ty = DStd.Expr.ty
type ty_var = DStd.Expr.ty_var
type ty_cst = DStd.Expr.ty_cst
type ty_def = DStd.Expr.ty_def
type term = DStd.Expr.term
type term_var = DStd.Expr.term_var
type term_cst = DStd.Expr.term_cst
type formula = DStd.Expr.formula
type nonrec !'a stmt = 'a Dolmen_loop__Typer_intf.stmt = {
  1. id : Dolmen.Std.Id.t;
  2. loc : Dolmen.Std.Loc.t;
  3. contents : 'a;
  4. attrs : Dolmen.Std.Term.t list;
  5. implicit : bool;
}
type decl = [
  1. | `Implicit_type_var
  2. | `Term_decl of term_cst
  3. | `Type_decl of ty_cst * ty_def option
]
type decls = [
  1. | `Decls of bool * decl list
]
type def = [
  1. | `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term
  2. | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term
  3. | `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty
]
type defs = [
  1. | `Defs of bool * def list
]
type assume = [
  1. | `Clause of formula list
  2. | `Goal of formula
  3. | `Hyp of formula
]
type solve = [
  1. | `Solve of formula list * formula list
]
type get_info = [
  1. | `Echo of string
  2. | `Get_assertions
  3. | `Get_assignment
  4. | `Get_info of Dolmen.Std.Statement.term
  5. | `Get_model
  6. | `Get_option of Dolmen.Std.Statement.term
  7. | `Get_proof
  8. | `Get_unsat_assumptions
  9. | `Get_unsat_core
  10. | `Get_value of term list
  11. | `Other of Dolmen.Std.Id.t * Dolmen.Std.Statement.term list
]
type set_info = [
  1. | `Set_info of Dolmen.Std.Statement.term
  2. | `Set_logic of string * Dolmen_type.Logic.t
  3. | `Set_option of Dolmen.Std.Statement.term
]
type stack_control = [
  1. | `Pop of int
  2. | `Push of int
  3. | `Reset
  4. | `Reset_assertions
]
type exit = [
  1. | `Exit
]
type end_ = [
  1. | `End
]
type typechecked = [
  1. | `Clause of formula list
  2. | `Decls of bool * decl list
  3. | `Defs of bool * def list
  4. | `Echo of string
  5. | `End
  6. | `Exit
  7. | `Get_assertions
  8. | `Get_assignment
  9. | `Get_info of Dolmen.Std.Statement.term
  10. | `Get_model
  11. | `Get_option of Dolmen.Std.Statement.term
  12. | `Get_proof
  13. | `Get_unsat_assumptions
  14. | `Get_unsat_core
  15. | `Get_value of term list
  16. | `Goal of formula
  17. | `Hyp of formula
  18. | `Other of Dolmen.Std.Id.t * Dolmen.Std.Statement.term list
  19. | `Pop of int
  20. | `Push of int
  21. | `Reset
  22. | `Reset_assertions
  23. | `Set_info of Dolmen.Std.Statement.term
  24. | `Set_logic of string * Dolmen_type.Logic.t
  25. | `Set_option of Dolmen.Std.Statement.term
  26. | `Solve of formula list * formula list
]
type state = State.t
type 'a key = 'a State.key
val type_check : bool key
val init : type_check:bool -> state -> state
val print : Stdlib.Format.formatter -> typechecked stmt -> unit
val check : state -> Dolmen.Std.Statement.t -> state * typechecked stmt list
val typecheck : state -> Dolmen.Std.Statement.t -> state * [ `Continue of typechecked stmt list | `Done of unit ]