Module Export.Dummy

Parameters

module Expr : Expr_intf.S
module Typer_Types : Typer.Types with type ty = Expr.ty and type ty_var = Expr.ty_var and type ty_cst = Expr.ty_cst and type ty_def = Expr.ty_def and type term = Expr.term and type term_var = Expr.term_var and type term_cst = Expr.term_cst and type formula = Expr.term

Signature

include module type of struct include Typer_Types end
include Expr_intf.S with type ty = Expr.ty with type ty_var = Expr.ty_var with type ty_cst = Expr.ty_cst with type ty_def = Expr.ty_def with type term = Expr.term with type term_var = Expr.term_var with type term_cst = Expr.term_cst with type formula = Expr.term
type ty = Expr.ty
type ty_var = Expr.ty_var
type ty_cst = Expr.ty_cst
type ty_def = Expr.ty_def
type term = Expr.term
type term_var = Expr.term_var
type term_cst = Expr.term_cst
type formula = Expr.term
type nonrec +'a stmt = 'a Typer_intf.stmt = {
  1. id : Dolmen.Std.Id.t;
  2. loc : Dolmen.Std.Loc.t;
  3. contents : 'a;
  4. attrs : Dolmen.Std.Term.t list;
  5. implicit : bool;
}

Wrapper around statements. It records implicit type declarations.

type decl = [
  1. | `Implicit_type_var
  2. | `Type_decl of ty_cst * ty_def option
  3. | `Term_decl of term_cst
]

The type of top-level type declarations.

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

A list of type declarations.

type def = [
  1. | `Type_alias 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
  3. | `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * 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 bool * 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 * formula list
    (*

    `Solve (hyps, goals) represents a sequent with local hypotheses hyps and local goals goals.

    *)
]

Top-level solve instruction

type get_info = [
  1. | `Get_info of Dolmen.Std.Statement.term
  2. | `Get_option of Dolmen.Std.Statement.term
  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. | `Other of Dolmen.Std.Id.t * Dolmen.Std.Statement.term list
]

Various info getters

type set_info = [
  1. | `Set_logic of string * Dolmen_type.Logic.t
  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
]

Stack control

type exit = [
  1. | `Exit
]

Exit statement

type end_ = [
  1. | `End
]
type typechecked = [
  1. | defs
  2. | decls
  3. | assume
  4. | solve
  5. | get_info
  6. | set_info
  7. | stack_control
  8. | exit
  9. | end_
]

The type of statements after typechecking

type acc = Stdlib.Format.formatter
val init : 'a -> 'a
val print : 'a -> Stdlib.Format.formatter -> 'b -> 'a * Stdlib.Format.formatter