package dolmen_loop

  1. Overview
  2. Docs

Parameters

module State : State.S

Signature

type state = State.t

Global state for the while pipeline.

type ty_state = ty_state

The type for the state of the typer.

type env = T.env

The type of the typechecker environment.

type 'a fragment = 'a T.fragment

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

type error = T.error

The type of type-checking errors.

type warning = T.warning

The type of type-checking warnings.

type builtin_symbols = T.builtin_symbols

The type of builin symbols for the type-checker.

val ty_state : ty_state State.key

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

val check_model : bool State.key

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

val smtlib2_forced_logic : string option State.key

Force the typechecker to use the given logic (instead of using the one declared in the `set-logic` statement).

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

include Typer_intf.Typer with type env := env and 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 ty_def := Dolmen.Std.Expr.ty_def 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 env := env 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 ty_def := Dolmen.Std.Expr.ty_def 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
type input = [
  1. | `Logic of Logic.language State.file
  2. | `Response of Response.language State.file
]
type lang = [
  1. | `Logic of Logic.language
  2. | `Response of Response.language
]
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 * Dolmen_type.Logic.t
val 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 * Dolmen.Std.Expr.ty_def option | `Term_decl of Dolmen.Std.Expr.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 * Dolmen.Std.Expr.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 * Dolmen.Std.Expr.formula
val 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
val typing_wrap : ?attrs:Dolmen.Std.Term.t list -> ?loc:Dolmen.Std.Loc.t -> input:input -> state -> f:(env -> 'a) -> state * 'a
val init : ?ty_state:ty_state -> ?smtlib2_forced_logic:string option -> ?additional_builtins:(state -> lang -> builtin_symbols) -> state -> state
val additional_builtins : (state -> lang -> builtin_symbols) State.key

Add new builtin symbols to the typechecker, depending on the current language.

Note. The additional builtins are never used for Dimacs and iCNF.

  • before 0.9

    additional_builtins had type builtin_symbols ref.

val report_error : input:input -> state -> error -> state

Report a typing error by calling the appropriate state function.

val report_warning : input:input -> state -> warning -> state

Return a typing warning by calling the appropriate state function.

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

TODO:doc