Module Qed.LogicSource

First Order Logic Definition

Sourcetype 'a element =
  1. | E_none
  2. | E_true
  3. | E_false
  4. | E_int of int
  5. | E_fun of 'a * 'a element list
Sourcetype 'a operator = {
  1. invertible : bool;
  2. associative : bool;
  3. commutative : bool;
  4. idempotent : bool;
  5. neutral : 'a element;
  6. absorbant : 'a element;
}

Algebraic properties for user operators.

Sourcetype 'a category =
  1. | Function
    (*

    logic function

    *)
  2. | Constructor
    (*

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

    *)
  3. | Injection
    (*

    f xs = f ys iff xi=yi

    *)
  4. | Operator of 'a operator

Algebraic properties for functions.

Sourcetype binder =
  1. | Forall
  2. | Exists
  3. | Lambda

Quantifiers and Binders

Sourcetype ('f, 'a) datatype =
  1. | Prop
  2. | Bool
  3. | Int
  4. | Real
  5. | Tvar of int
    (*

    ranges over 1..arity

    *)
  6. | Array of ('f, 'a) datatype * ('f, 'a) datatype
  7. | Record of ('f * ('f, 'a) datatype) list
  8. | Data of 'a * ('f, 'a) datatype list
Sourcetype sort =
  1. | Sprop
  2. | Sbool
  3. | Sint
  4. | Sreal
  5. | Sdata
  6. | Sarray of sort
Sourcetype maybe =
  1. | Yes
  2. | No
  3. | Maybe
Sourcemodule type Symbol = sig ... end

Ordered, hash-able and pretty-printable symbols

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

Representation of Patterns, Functions and Terms

Sourcetype ('f, 'a) funtype = {
  1. result : ('f, 'a) datatype;
    (*

    Type of returned value

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

    Type of parameters

    *)
}
Sourcetype ('f, 'a, 'd, 'x, 'b, 'e) term_repr =
  1. | True
  2. | False
  3. | Kint of Z.t
  4. | Kreal of Q.t
  5. | Times of Z.t * 'e
    (*

    mult: k1 * e2

    *)
  6. | Add of 'e list
    (*

    add: e11 + ... + e1n

    *)
  7. | Mul of 'e list
    (*

    mult: e11 * ... * e1n

    *)
  8. | Div of 'e * 'e
  9. | Mod of 'e * 'e
  10. | Eq of 'e * 'e
  11. | Neq of 'e * 'e
  12. | Leq of 'e * 'e
  13. | Lt of 'e * 'e
  14. | Aget of 'e * 'e
    (*

    access: array1idx2

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

    update: array1idx2 -> elem3

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

    constant array type -> value

    *)
  17. | Rget of 'e * 'f
  18. | Rdef of ('f * 'e) list
  19. | And of 'e list
    (*

    and: e11 && ... && e1n

    *)
  20. | Or of 'e list
    (*

    or: e11 || ... || e1n

    *)
  21. | Not of 'e
  22. | Imply of 'e list * 'e
    (*

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

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

    ite: if c1 then e2 else e3

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

    Complete call (no partial app.)

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

    High-Order application (Cf. binder)

    *)
  28. | 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
Sourcetype 'a affine = Z.t * (Z.t * 'a) list
Sourcemodule type Term = sig ... end