package dolmen_loop

  1. Overview
  2. Docs

This modules defines a wrapper around the bare-bones typechecker provided by Dolmen_type. It provides convenience function to match on Dolmen untyped statements and type-check them.

include Types
type state
type ty
type ty_var
type ty_cst
type term
type term_var
type term_cst
type formula
type input = [
  1. | `Logic of Logic.language State.file
  2. | `Response of Response.language State.file
]
val reset : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state
val reset_assertions : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state
val push : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> state
val pop : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> state
val set_logic : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> string -> state
val defs : mode:[ `Create_id | `Use_declared_id ] -> state -> input:input -> ?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 -> input:input -> ?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 -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * term list
val formula : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> state * formula
val formulas : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * formula list