Module Qed.Logic

First Order Logic Definition

type 'a element =
| E_none
| E_true
| E_false
| E_int of int
| E_fun of 'a * 'a element list
type 'a operator = {
invertible : bool;
associative : bool;
commutative : bool;
idempotent : bool;
neutral : 'a element;
absorbant : 'a element;
}

Algebraic properties for user operators.

type 'a category =
| Function(*

logic function

*)
| Constructor(*

f xs = g ys iff f=g && xi=yi

*)
| Injection(*

f xs = f ys iff xi=yi

*)
| Operator of 'a operator

Algebraic properties for functions.

type binder =
| Forall
| Exists
| Lambda

Quantifiers and Binders

type ('f, 'a) datatype =
| Prop
| Bool
| Int
| Real
| Tvar of int(*

ranges over 1..arity

*)
| Array of ( 'f, 'a ) datatype * ( 'f, 'a ) datatype
| Record of ('f * ( 'f, 'a ) datatype) list
| Data of 'a * ( 'f, 'a ) datatype list
type sort =
| Sprop
| Sbool
| Sint
| Sreal
| Sdata
| Sarray of sort
type maybe =
| Yes
| No
| Maybe
module type Symbol = sig ... end

Ordered, hash-able and pretty-printable symbols

module type Data = sig ... end
module type Field = sig ... end
module type Function = sig ... end
module type Variable = sig ... end

Representation of Patterns, Functions and Terms

type ('f, 'a) funtype = {
result : ( 'f, 'a ) datatype;(*

Type of returned value

*)
params : ( 'f, 'a ) datatype list;(*

Type of parameters

*)
}
type ('f, 'a, 'd, 'x, 'b, 'e) term_repr =
| True
| False
| Kint of Z.t
| Kreal of Q.t
| Times of Z.t * 'e(*

mult: k1 * e2

*)
| Add of 'e list(*

add: e11 + ... + e1n

*)
| Mul of 'e list(*

mult: e11 * ... * e1n

*)
| Div of 'e * 'e
| Mod of 'e * 'e
| Eq of 'e * 'e
| Neq of 'e * 'e
| Leq of 'e * 'e
| Lt of 'e * 'e
| Aget of 'e * 'e(*

access: array1idx2

*)
| Aset of 'e * 'e * 'e(*

update: array1idx2 -> elem3

*)
| Acst of ( 'f, 'a ) datatype * 'e(*

constant array type -> value

*)
| Rget of 'e * 'f
| Rdef of ('f * 'e) list
| And of 'e list(*

and: e11 && ... && e1n

*)
| Or of 'e list(*

or: e11 || ... || e1n

*)
| Not of 'e
| Imply of 'e list * 'e(*

imply: (e11 && ... && e1n) ==> e2

*)
| If of 'e * 'e * 'e(*

ite: if c1 then e2 else e3

*)
| Fun of 'd * 'e list(*

Complete call (no partial app.)

*)
| Fvar of 'x
| Bvar of int * ( 'f, 'a ) datatype
| Apply of 'e * 'e list(*

High-Order application (Cf. binder)

*)
| Bind of binder * ( 'f, 'a ) datatype * 'b

representation of terms. type arguments are the following:

  • 'z: representation of integral constants
  • 'f: representation of fields
  • 'a: representation of abstract data types
  • 'd: representation of functions
  • 'x: representation of free variables
  • 'b: representation of bound term (phantom type equal to 'e)
  • 'e: sub-expression
type 'a affine = Z.t * (Z.t * 'a) list
module type Term = sig ... end