Module Qed.Engine

Generic Engine Signature

type op =
| Op of string(*

Infix or prefix operator

*)
| Assoc of string(*

Left-associative binary operator (like + and -)

*)
| Call of string(*

Logic function or predicate

*)
type callstyle =
| CallVar(*

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

*)
| CallVoid(*

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

*)
| CallApply(*

Call is f x ...

*)
type mode =
| Mpositive(*

Current scope is Prop in positive position.

*)
| Mnegative(*

Current scope is Prop in negative position.

*)
| Mterm(*

Current scope is Term.

*)
| Mterm_int(*

Int is required but actual scope is Term.

*)
| Mterm_real(*

Real is required but actual scope is Term.

*)
| Mint(*

Current scope is Int.

*)
| Mreal(*

Current scope is Real.

*)
type flow =
| Flow
| Atom
type cmode =
| Cprop
| Cterm
type amode =
| Aint
| Areal
type pmode =
| Positive
| Negative
| Boolean
type ('x, 'f) ftrigger =
| TgAny
| TgVar of 'x
| TgGet of ( 'x, 'f ) ftrigger * ( 'x, 'f ) ftrigger
| TgSet of ( 'x, 'f ) ftrigger * ( 'x, 'f ) ftrigger * ( 'x, 'f ) ftrigger
| TgFun of 'f * ( 'x, 'f ) ftrigger list
| TgProp of 'f * ( 'x, 'f ) ftrigger list
type ('t, 'f, 'c) ftypedef =
| Tabs
| Tdef of 't
| Trec of ('f * 't) list
| Tsum of ('c * 't list) list
type scope = [
| `Auto
| `Unfolded
| `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