package dolmen_loop

  1. Overview
  2. Docs

This modules defines the smallest signatures for a typechecker that allow to instantiate the Typer.Pipe functor.

include Pipe_types
type state
type ty
type ty_var
type ty_cst
type term
type term_var
type term_cst
type formula
val typecheck : state -> bool
val reset : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state
val reset_assertions : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state
val push : state -> ?loc:Dolmen.Std.Loc.t -> int -> state
val pop : state -> ?loc:Dolmen.Std.Loc.t -> int -> state
val set_logic : state -> ?loc:Dolmen.Std.Loc.t -> string -> state
val defs : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.defs -> state * [ `Type_def of Dolmen.Std.Id.t * ty_cst * ty_var list * ty | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term ] list
val decls : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.decls -> state * [ `Type_decl of ty_cst | `Term_decl of term_cst ] list
val terms : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * term list
val formula : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> state * formula
val formulas : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * formula list