package dolmen_loop

  1. Overview
  2. Docs

Module Typer.MakeSource

Parameters

module S : State_intf.Typer with type ty_state := ty_state

Signature

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

include Typer_intf.Pipe_arg with type state := S.t 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.Pipe_types with type state := S.t 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
Sourceval typecheck : S.t -> bool
Sourceval reset : S.t -> ?loc:Dolmen.Std.Loc.t -> unit -> S.t
Sourceval reset_assertions : S.t -> ?loc:Dolmen.Std.Loc.t -> unit -> S.t
Sourceval push : S.t -> ?loc:Dolmen.Std.Loc.t -> int -> S.t
Sourceval pop : S.t -> ?loc:Dolmen.Std.Loc.t -> int -> S.t
Sourceval set_logic : S.t -> ?loc:Dolmen.Std.Loc.t -> string -> S.t
Sourceval decls : S.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Statement.decls -> S.t * [ `Type_decl of Dolmen.Std.Expr.ty_cst | `Term_decl of Dolmen.Std.Expr.term_cst ] list
Sourceval terms : S.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> S.t * Dolmen.Std.Expr.term list
Sourceval formula : S.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> goal:bool -> Dolmen.Std.Term.t -> S.t * Dolmen.Std.Expr.formula
Sourceval formulas : S.t -> ?loc:Dolmen.Std.Loc.t -> ?attrs:Dolmen.Std.Term.t list -> Dolmen.Std.Term.t list -> S.t * Dolmen.Std.Expr.formula list
Sourceval report_error : S.t -> T.error -> S.t

Report a typing error by calling the appropriate state function.

Sourceval report_warning : S.t -> T.warning -> S.t

Return a typing warning by calling the appropriate state function.

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