package dolmen_loop

  1. Overview
  2. Docs

Module Typer.TyperSource

Parameters

module State : State.S

Signature

Sourcetype state = State.t

Global state for the while pipeline.

Sourcetype ty_state = ty_state

The type for the state of the typer.

Sourcetype env = T.env

The type of the typechecker environment.

Sourcetype 'a fragment = 'a T.fragment

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

Sourcetype error = T.error

The type of type-checking errors.

Sourcetype warning = T.warning

The type of type-checking warnings.

Sourcetype builtin_symbols = T.builtin_symbols

The type of builin symbols for the type-checker.

Sourceval ty_state : ty_state State.key

Key to store the local typechecking state in the global pipeline state.

Sourceval check_model : bool State.key

The typechecker needs to know whether we are checking models or not.

Sourceval smtlib2_forced_logic : string option State.key

The typechecker needs to know whether we are checking models or not.

Sourceval init : ?ty_state:ty_state -> ?smtlib2_forced_logic:string option -> state -> state

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

include Typer_intf.Typer 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
include Typer_intf.Types with type state := state with type ty := Dolmen.Std.Expr.ty with type ty_var := Dolmen.Std.Expr.ty_var with type ty_cst := Dolmen.Std.Expr.ty_cst with type term := Dolmen.Std.Expr.term with type term_var := Dolmen.Std.Expr.term_var with type term_cst := Dolmen.Std.Expr.term_cst with type formula := Dolmen.Std.Expr.formula
Sourcetype input = [
  1. | `Logic of Logic.language State.file
  2. | `Response of Response.language State.file
]
Sourceval reset : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state
Sourceval reset_assertions : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state
Sourceval push : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> state
Sourceval pop : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> state
Sourceval set_logic : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> string -> state
Sourceval decls : state -> input:input -> ?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
Sourceval terms : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * Dolmen.Std.Expr.term list
Sourceval formula : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> state * Dolmen.Std.Expr.formula
Sourceval formulas : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> state * Dolmen.Std.Expr.formula list
Sourceval report_error : input:input -> state -> error -> state

Report a typing error by calling the appropriate state function.

Sourceval report_warning : input:input -> state -> warning -> state

Return a typing warning by calling the appropriate state function.

Sourceval additional_builtins : builtin_symbols 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.

Sourceval pop_inferred_model_constants : state -> Dolmen.Std.Expr.term_cst list

TODO:doc