This modules defines the result signature of the Typer.Make functor

type state

The type of state for a whole pipeline.

type ty_state

The type for the state of the typer.

type env

The type of the typechecker environment.

type 'a fragment

The type of fragments on which error/warning can occur.

type error

The type of type-checking errors.

type warning

The type of type-checking warnings.

type builtin_symbols

The type of builin symbols for the type-checker.

This signature includes the requirements to instantiate the {Pipes.Make: functor

include Pipe_arg with type state := state 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 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
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 decls : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.decls -> state * [ `Type_decl of Dolmen.Std.Expr.ty_cst | `Term_decl of Dolmen.Std.Expr.term_cst ] list
val terms : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * Dolmen.Std.Expr.term list
val formula : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> state * Dolmen.Std.Expr.formula
val formulas : state -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * Dolmen.Std.Expr.formula list
val report_error : state -> error -> state

Report a typing error by calling the appropriate state function.

val report_warning : state -> warning -> state

Return a typing warning by calling the appropriate state function.

val additional_builtins : builtin_symbols Stdlib.ref

This reference can be modified to parse new builtin symbols. By default no additional builtin symbols are parsed. It is added for all the languages except Dimacs, and iCNF.