dolmen_loop
  1. Overview
  2. Docs
On This Page
  1. Types

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

include Pipe_types
type state
type ty
type ty_var
type ty_cst
type term
type term_var
type term_cst
type 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 ty_cst
  2. | `Term_decl of 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 * ty_cst * ty_var list * ty
  2. | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * 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 formula
  2. | `Goal of formula
  3. | `Clause of formula list
]

The type of top-level assertion statements

type solve = [
  1. | `Solve of 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 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 : Format.formatter -> typechecked stmt -> unit

Printing funciton for typechecked statements.

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

Typechecks a statement.