Parameters

module Expr : Expr_intf.S
module Print : Expr_intf.Print with type ty := Expr.ty and type ty_var := Expr.ty_var and type ty_cst := Expr.ty_cst and type term := Expr.term and type term_var := Expr.term_var and type term_cst := Expr.term_cst and type formula := Expr.formula
module Typer : Pipe_arg with type state := State.t and type ty := Expr.ty and type ty_var := Expr.ty_var and type ty_cst := Expr.ty_cst and type term := Expr.term and type term_var := Expr.term_var and type term_cst := Expr.term_cst and type formula := Expr.formula

Signature

include Typer_intf.Pipe_types with type state := State.t with type ty := Expr.ty with type ty_var := Expr.ty_var with type ty_cst := Expr.ty_cst with type term := Expr.term with type term_var := Expr.term_var with type term_cst := Expr.term_cst with type formula := Expr.formula

Types

type +'a stmt = {
  1. id : Dolmen.Std.Id.t;
  2. loc : Dolmen.Std.Loc.t;
  3. contents : 'a;
}

Wrapper around statements. It records implicit type declarations.

type decl = [
  1. | `Type_decl of Expr.ty_cst
  2. | `Term_decl of Expr.term_cst
]

The type of top-level type declarations.

type decls = [
  1. | `Decls of decl list
]

A list of type declarations.

type def = [
  1. | `Type_def of Dolmen.Std.Id.t * Expr.ty_cst * Expr.ty_var list * Expr.ty
  2. | `Term_def of Dolmen.Std.Id.t * Expr.term_cst * Expr.ty_var list * Expr.term_var list * Expr.term
]

The type of top-level type definitions. Type definitions are inlined and so can be ignored.

type defs = [
  1. | `Defs of def list
]

A list of definitions

type assume = [
  1. | `Hyp of Expr.formula
  2. | `Goal of Expr.formula
  3. | `Clause of Expr.formula list
]

The type of top-level assertion statements

type solve = [
  1. | `Solve of Expr.formula list
]

Top-level solve instruction

type get_info = [
  1. | `Get_info of string
  2. | `Get_option of string
  3. | `Get_proof
  4. | `Get_unsat_core
  5. | `Get_unsat_assumptions
  6. | `Get_model
  7. | `Get_value of Expr.term list
  8. | `Get_assignment
  9. | `Get_assertions
  10. | `Echo of string
  11. | `Plain of Dolmen.Std.Statement.term
]

Various info getters

type set_info = [
  1. | `Set_logic of string
  2. | `Set_info of Dolmen.Std.Statement.term
  3. | `Set_option of Dolmen.Std.Statement.term
]

Info setters

type stack_control = [
  1. | `Pop of int
  2. | `Push of int
  3. | `Reset_assertions
  4. | `Reset
  5. | `Exit
]

Stack control

type typechecked = [
  1. | defs
  2. | decls
  3. | assume
  4. | solve
  5. | get_info
  6. | set_info
  7. | stack_control
]

The type of statements after typechecking

val print : Stdlib.Format.formatter -> typechecked stmt -> unit

Printing funciton for typechecked statements.

val typecheck : State.t -> Dolmen.Std.Statement.t -> State.t * [ `Continue of typechecked stmt | `Done of unit ]

Typechecks a statement.