dolmen_loop 0.7 · OCaml Package

include Typer_intf.Pipe_types
  with type state := State.t
  with type ty := Expr.ty
  with type ty_var := Expr.ty_var
  with type ty_cst := Expr.ty_cst
  with type term := Expr.term
  with type term_var := Expr.term_var
  with type term_cst := Expr.term_cst
  with type formula := Expr.formula

val typecheck : State.t -> bool

val reset : State.t -> ?loc:Dolmen.Std.Loc.t -> unit -> State.t

val reset_assertions : State.t -> ?loc:Dolmen.Std.Loc.t -> unit -> State.t

val push : State.t -> ?loc:Dolmen.Std.Loc.t -> int -> State.t

val pop : State.t -> ?loc:Dolmen.Std.Loc.t -> int -> State.t

val set_logic : State.t -> ?loc:Dolmen.Std.Loc.t -> string -> State.t

val defs : 
  State.t ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.defs ->
  State.t
  * [ `Type_def of Dolmen.Std.Id.t * Expr.ty_cst * Expr.ty_var list * Expr.ty
    | `Term_def of
      Dolmen.Std.Id.t
      * Expr.term_cst
      * Expr.ty_var list
      * Expr.term_var list
      * Expr.term ]
      list

val decls : 
  State.t ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.decls ->
  State.t * [ `Type_decl of Expr.ty_cst | `Term_decl of Expr.term_cst ] list

val terms : 
  State.t ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Term.t list ->
  State.t * Expr.term list

val formula : 
  State.t ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  goal:bool ->
  Dolmen.Std.Term.t ->
  State.t * Expr.formula

val formulas : 
  State.t ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Term.t list ->
  State.t * Expr.formula list