Module Qed.Engine

Generic Engine Signature

type op =
  1. | Op of string
    (*

    Infix or prefix operator

    *)
  2. | Assoc of string
    (*

    Left-associative binary operator (like + and -)

    *)
  3. | Call of string
    (*

    Logic function or predicate

    *)
type callstyle =
  1. | CallVar
    (*

    Call is f(x,...) ; f() can be written f

    *)
  2. | CallVoid
    (*

    Call is f(x,...) ; in f(), () is mandatory

    *)
  3. | CallApply
    (*

    Call is f x ...

    *)
type mode =
  1. | Mpositive
    (*

    Current scope is Prop in positive position.

    *)
  2. | Mnegative
    (*

    Current scope is Prop in negative position.

    *)
  3. | Mterm
    (*

    Current scope is Term.

    *)
  4. | Mterm_int
    (*

    Int is required but actual scope is Term.

    *)
  5. | Mterm_real
    (*

    Real is required but actual scope is Term.

    *)
  6. | Mint
    (*

    Current scope is Int.

    *)
  7. | Mreal
    (*

    Current scope is Real.

    *)
type flow =
  1. | Flow
  2. | Atom
type cmode =
  1. | Cprop
  2. | Cterm
type amode =
  1. | Aint
  2. | Areal
type pmode =
  1. | Positive
  2. | Negative
  3. | Boolean
type ('x, 'f) ftrigger =
  1. | TgAny
  2. | TgVar of 'x
  3. | TgGet of ('x, 'f) ftrigger * ('x, 'f) ftrigger
  4. | TgSet of ('x, 'f) ftrigger * ('x, 'f) ftrigger * ('x, 'f) ftrigger
  5. | TgFun of 'f * ('x, 'f) ftrigger list
  6. | TgProp of 'f * ('x, 'f) ftrigger list
type ('t, 'f, 'c) ftypedef =
  1. | Tabs
  2. | Tdef of 't
  3. | Trec of ('f * 't) list
  4. | Tsum of ('c * 't list) list
type scope = [
  1. | `Auto
  2. | `Unfolded
  3. | `Defined of string
]
module type Env = sig ... end

Generic Engine Signature

class type virtual ['z, 'adt, 'field, 'logic, 'tau, 'var, 'term, 'env] engine = object ... end