Module Parsetree


module Parsetree: sig .. end

Modified OCaml parsetree for Moca




Type declarations with Moca additions



type type_declaration = {
   ptype_params : string list;
   ptype_cstrs : (core_type * core_type * Location.t) list;
   ptype_kind : type_kind;
   ptype_private : Asttypes.private_flag;
   ptype_manifest : core_type option;
   ptype_variance : (bool * bool) list;
   ptype_loc : Location.t;
}
type type_kind =
| Ptype_abstract of relations
| Ptype_variant of (string * core_type list * relations * Location.t) list
| Ptype_record of (string * Asttypes.mutable_flag * core_type * relations *
Location.t)
list

Generators/relations for relational types



Definitions

Definition: Relational data type

A relational data type is a private data type with a set of relations that specifies the way the values of the type must be built.

Definition: Generator

The constructors of a relational data type are named generators, to emphasis their special status of constructors with relations that govern their associated construction functions.

Definition: Arity of generators

A zeroary generator is a generator that has no argument. A zeroary generator is also called a constant generator,

A unary generator is a generator that has exactly one argument which is not a list,

A binary generator is a generator that has exactly two arguments,

A listary generator is a generator that has exactly one argument which is a list. A listary generator generator is also called a vary-adic generator.

A nary generator is a generator that has $n$ arguments ($n >= 3$).

Definition: Compatibility of arities

The arity $e$ is compatible with arity $d$, if and only if $e$ is listary or $e = d$.

Note: if a relation is defined for a listary generator and the relation states a particular case for singletons, then the relation must also have a definition for unary generators and both definitions must agree.

Definition: Comparison function

A comparison function is a total ordering on the relational data type that is compatible with the structural equality of the language.

In the usual mathematical sense, this definition expands to the following:

cmp is a comparison function if and only if:

Define by x >= y if and only if cmp x y >= 0 ; then >= must be a total ordering: Note: This definition implies that a comparison function must be a total function (it must always terminates).

The argument option of algebraic relation commutative is the name of a comparison function that is used to sort the arguments of the given generator. The comparison function is normally bound via a previous Structure_item definition of the relational data type definition.

If the arguments of the commutative generator have type t then the comparison function must have type t -> t -> int .

type relation_side =
| Left
| Right
| Both

type distributivity_direction =
| Dist_Inverse
| Dist_Direct

type rpo_status =
| Lexicographic
| Multiset

type rpo_precedence = int 

type generator = {
   pgen_desc : Longident.t;
   pgen_loc : Location.t;
}
type relations = {
   prels_desc : relations_desc;
   prels_loc : Location.t;
}
type relations_desc =
| Prels_none
| Prels_commented of relations
| Prels_begend of relation list

type relation = {
   prel_desc : rel_desc;
   prel_loc : Location.t;
}

Specifications of algebraic relations for generators



type rel_desc =
| Absorbent of relation_side * generator (*

Specification for Absorbent (side, A)

  • For zeroary generators: not applicable.
  • For unary generators:
If C has Absorbent (Both, A), then C (A) -> A.

Absorbent (Left, A) and Absorbent (Right, A) are erroneous.

  • For binary generators:
If C has Absorbent (Left, A), then C (A, x) -> A.

If C has Absorbent (Right, A), then C (x, A) -> A.

Absorbent (Both, A) is the conjunction of Absorbent (Left, A) and Absorbent (Right, A).

  • For listary generators:
If C has Absorbent (Both, A), then C b1; ...; bn; A; c1; ...; cn -> A. In particular: C A -> A.

If C has Absorbent (Left, A), then C b1; ...; bn; A; c1; ...; cn -> C b1; ...; bn; A. C A -> A.

If C has Absorbent (Right, A), then C b1; ...; bn; A; c1; ...; cn -> C A; c1; ...; cn. C A -> A.

Absorbent (Both, A) is the conjunction of Absorbent (Left, A) and Absorbent (Right, A).

  • For nary generators: not applicable.
Overall hint for absorbent: Absorbent (side, A) is (mostly) equivalent to Distributive (side, A, None, Dist_Direct).
*)
| Absorbing of relation_side * generator (*

Specification for Absorbing

  • For zeroary generators: not applicable
  • For unary generators: not applicable
  • For binary generators:
if C has Absorbing (Left, D), then C (D (x, y), y) -> y,

if C has Absorbing (Right, D), then C (x, D (x, y)) -> x,

Absorbing (Both, D) is the conjunction of Absorbing (Left, D) and Absorbing (Right, D).

  • For listary generators: not applicable.
  • For nary generators: not applicable.
*)
| Associative of relation_side (*Note: for the time being the relation_side argument cannot be specified in source code. The default is Left (hence associative means Associative Left).

Specification for Associative

  • For zeroary generators: not applicable.
  • For unary generators: not applicable.
  • For binary generators:
If C has Associative (Left), then C (C (x, y), z) -> C (x, C (y, z)).

If C has Associative (Right), then C (x, C (y, z)) -> C (C (x, y), z).

Associative (Both) is equivalent to Associative (Left).

  • For listary generators:
If C has Associative (Left), then (flattening) C ...; C [x; ...; y]; ... -> C ...; x; ...; y; ...,

Associative (Both) and Associative (Right) are equivalent to Associative (Left).

  • For nary generators: not applicable.
*)
| Commutative of Longident.t option (*

Specification for Commutative (cmp)

The optional argument cmp is a comparison function, as defined above.

If no cmp option is given, the default comparison function is Pervasives.compare . In other words, the relation Commutative (None) is equivalent to the relation Commutative (Some Pervasives.compare).

  • For zeroary generators: not applicable.
  • For unary generators: not applicable.
  • For binary generators:
If C is not associative:

If C has Commutative (Some cmp), then the arguments of C are sorted in increasing order with respect to cmp,

C (x, y) -> C (y, x) if cmp x y > 0.

If C is associative:

If C has Commutative (Some cmp), then the leaves of C-combs are sorted in increasing order with respect to cmp,

C (x, C (y, z)) -> C (y, C (x, z)) if cmp x y > 0. C (x, y) -> C (y, x) if cmp x y > 0 and y not of the form C (u, v).

  • For listary generators:
If C has Commutative (Some cmp), then the elements of the list argument of C are sorted in increasing order with respect to cmp,

C ...; x; y; ... -> C ...; y; x; ... if cmp x y > 0.

  • For nary generators: not applicable.
*)
| Distributive of relation_side * generator * generator option
* distributivity_direction
(*

Prerequisites for distributivity

  • For having Distributive (side, D, Some E, dir), the arity of E must be compatible with the arity of D (compatibility of arities is define above)..
  • Distributive (side, D, None, dir) is equivalent to Distributive (side, D, Some D, dir).
  • In relation Distributive (side, D, Some E, dir), the dir argument governs the order of the arguments of generator E in the right-hand side of the following definition rules for distributivity.
  • In particular, to obtain the rules for Distributive (side, D, Some E, Dist_Inverse), take the rules for Distributive (side, D, Some E, Dist_Direct) and simply write the arguments of E in reverse order.

Specification for Distributive (side, generator, generator option, dir)

  • For zeroary generators: not applicable.
  • For unary generators:
If C has Distributive (Both, D, None, dir), then C has Distributive (Both, D, Some D, dir), else

If C has Distributive (Both, D, Some E, dir), then if E is zeroary (then D must be zeroary), C (D) -> E

if E is unary (then D must be unary), C (D (x)) -> E (x)

if E is binary (then D must be binary), if dir = Dist_Direct then C (D (x, y)) -> E (x, y) else C (D (x, y)) -> E (y, x)

if E is listary then if D is:

  • zeroary C (D) -> E []
  • unary C (D (y)) -> E C (y)
  • binary C (D (y1, y2)) -> E C (y1); C (y2)
  • listary C (D y1; ...; yn) -> E C (y1); ...; C (yn)
  • nary C (D (y1; ...; yn)) -> E C (y1); ...; C (yn)
if E is nary (then D must be nary), C (D (y1; ...; yn)) -> E (C (y1); ...; C (yn))

Distributive (Right, D, generator_option, dir) and Distributive (Left, D, generator_option, dir) are errors.

  • For binary generators:
If C has Distributive (Left, D, Some E, Dist_Direct), then if E is zeroary (then D must be zeroary), C (D, z) -> E, if E is unary (then D must be unary), C (D (x), z) -> E (C (x, z)), if E is binary (then D must be binary), C (D (x, y), z) -> E (C (x, z), C (y, z)), if E is listary: if D is zeroary: C (D, z) -> E [], if D is unary: C (D (x), z) -> E C (x, z), if D is binary: C (D (x, y), z) -> E C (x, z); C (y, z), if D is listary: C (D x1, ..., xn, z) -> E C (x1; z), ..., C (xn; z), if D is nary: C (D (x1, ..., xn), z) -> E C (x1, z), ..., C (xn, z), if E is nary (then D must be nary), C (D (x1, ..., xn), z) -> E (C (x1, z), ..., C (xn, z)),

If C has Distributive (Right, D, Some E, Dist_Direct), then C (z, D) -> E if D and E are zeroary, C (z, D (x1, ..., xn)) -> E (C (z, x1), ..., C (z, xn)) otherwise.

Distributive (Both, D, Some E, dir) is the conjunction of Distributive (Left, D, Some E, dir) and Distributive (Right, D, Some E, dir).

  • For listary generators:
If C has Distributive (Both, D, Some E, Dist_Direct), then if E is zeroary (then D must be zeroary), C u1; ...; un; D; t1; ...; tn -> E, if E is unary (then D must be unary), C u1; ...; un; D (x); t1; ...; tn -> E (C u1; ...; un; x; t1; ...; tn),

if E is binary (then D must be binary), C u1; ...; un; D (x, y); t1; ...; tn -> E (C u1; ...; un; x; t1; ...; tn, C u1; ...; un; y; t1; ...; tn),

if E is listary: if D is zeroary: C u1; ...; un; D; t1; ...; tn -> E [], if D is unary: C u1; ...; un; D (x); t1; ...; tn -> E C [u1; ...; un; x; t1; ...; tn], if D is binary: C u1; ...; un; D (x, y); t1; ...; tn -> E C [u1; ...; un; x; t1; ...; tn]; C [u1; ...; un; y; t1; ...; tn]; if D is listary: C u1; ...; un; D [x1; ...; xn]; t1; ...; tn -> E C [u1; ...; un; x1; t1; ...; tn]; ...; C [u1; ...; un; xn; t1; ...; tn]; if D is nary: C u1; ...; un; D (x1, ..., xn); t1; ...; tn -> E C [u1; ...; un; x1; t1; ...; tn]; ...; C [u1; ...; un; xn; t1; ...; tn];

if E is nary (then D must be nary with the same arity as E), C u1; ...; un; D (x1, ..., xn); t1; ...; tn -> E (C u1; ...; un; x1; t1; ...; tn, ..., C u1; ...; un; xn; t1; ...; tn)

Distributive (Right, D, generator_option, dir) and Distributive (Left, D, generator_option, dir) are errors.

  • For nary generators: not applicable.
*)
| Division_by_Absorbent of generator (*This is an internal generator for Moca that is automatically added to the relations of a generator when appropriate.

Specification for Division_by_Absorbent (generator)

  • For zeroary generators: not applicable.
  • For unary operators:
If C has Division_by_Absorbent (A), then C (A) -> failwith "Division by absorbent element".

  • For binary generators: If C has Division_by_Absorbent (A), then C (x, A) -> failwith "Division by absorbent element".
  • For listary generators and
  • For nary generators: Division_by_Absorbent is not applicable.
*)
| Idempotent of relation_side (*

Specification of Idempotent (side)

  • For zeroary generators: not applicable.
  • For unary generators:
If C has Idempotent (Both), then C (C x) -> C x,

Idempotent (Left) and Idempotent (Right) are errors.

  • For binary generators:
If C has Idempotent (Left), then C (C (x, y), y) -> C (x, y), if x and C (x, x) have the same type, then C (x, x) -> x,

If C has Idempotent (Right), then C (x, C (x, y)) -> C (x, y), if x and C (x, x) have the same type, then C (x, x) -> x,

Idempotent (Both) is the conjunction of Idempotent (Left) and Idempotent (Right).

  • For listary generators:
If C has Idempotent (Left), then C ...; x; x; ... -> C ...; x; ... if the list of arguments has >= 3 elements if x and C x, x have the same type, then C x; x -> x,

Idempotent (Both) and Idempotent (Right) are equivalent to Idempotent (Left).

  • For nary generators: not applicable.
*)
| Inverse of relation_side * generator * generator option (*

Specification for Inverse (side, generator, generator option)

  • For zeroary generators: not applicable.
  • For unary generators:
If C has (Inverse (Left, I, None), then C (I (x)) -> x.

If C has (Inverse (Right, I, None), then I (C (x)) -> x.

Inverse (Both, I, None) is the conjunction of Inverse (Left, I, None) and Inverse (Right, I, None).

If C has Inverse (Left, I, Some A), then C (I (x)) -> A.

If C has Inverse (Right, I, Some A), then I (C (x)) -> A.

Inverse (Both, I, Some A) is equivalent to Inverse (Left, I, Some A) and Inverse (Right, I, Some A).

  • For binary generators:
If C has Inverse (side, I, None), then C must have Neutral (side, E) and Inverse (side, I, None) is equivalent to Inverse (side, I, Some E).

If C has Inverse (Left, I, Some A), then I implicitely has Involutive and C implicitely has Distributive (Left, E, Some A, Dist_Direct) and

C (I (x), x) -> A.

If C has Inverse (Right, I, Some A), then I implicitely has Involutive and C implicitely has Distributive (Right, E, Some A, Dist_Direct) and

C (x, I (x)) -> A

Inverse (Both, I, Some A) is equivalent to Inverse (Left, I, Some A) and Inverse (Right, I, Some A).

  • For listary generators:
If C has Inverse (side, I, None), then C must have Neutral (side, E) and Inverse (side, I, None) is equivalent to Inverse (side, I, Some E).

If C has Inverse (Left, I, Some A), then I implicitely has Involutive and C implicitely has Distributive (Left, E, Some A, Dist_Direct) and

I implicitely has Involutive and C implicitely has Distributive (Right, E, Some A, Dist_Direct) and

C ...; I (x); x; ... -> C ...; A; ... if the list of arguments has >= 3 elements, C I (x); x -> A.

If C has Inverse (Right, I, Some A), then I implicitely has Involutive and C implicitely has Distributive (Right, E, Some A, Dist_Direct) and

C ...; x; I (x); ... -> C ...; A; ... if the list of arguments has >= 3 elements, C x; I (x) -> A.

Inverse (Both, I, Some A) is the conjunction of Inverse (Left, I, Some A) and Inverse (Right, I, Some A).

  • For nary generators: not applicable.
*)
| Involutive (*

Specification for Involutive

  • For zeroary generators: not applicable.
  • For unary generators:
If C has Involutive, then C (C (x)) -> x.

  • For binary generators: not applicable.
  • For listary generators: not applicable.
  • For nary generators: not applicable.
*)
| Neutral of relation_side * generator (*

Specification for Neutral (side, generator)

  • For zeroary generators: not applicable.
  • For unary generators:
C has Neutral (side, E) is equivalent to E is a fixpoint for C.

If C has Neutral (Both, E), then C (E) -> E.

Neutral (Right, E) and Neutral (Left, E) are errors.

  • For binary generators:
If C has Neutral (Left, E), then C (E, x) -> x,

If C has Neutral (Right, E), then C (x, E) -> x,

Neutral (Both, E) is the conjunction of Neutral (Left, E) and Neutral (Right, E).

  • For listary generators:
If C has Neutral (Left, E), then C ...; E; x; ... -> C ...; x; ... if the list of arguments has at least 2 elements, C x -> x, C [] -> E,

If C has Neutral (Right, E), then C ...; x; E; ... -> C ...; x; ... if the list of arguments has at least 2 elements, C x -> x C [] -> E,

Neutral (Both, E) is the conjunction of Neutral (Left, E) and Neutral (Right, E).

  • For nary generators: not applicable.
*)
| Nilpotent of relation_side * generator (*

Specification for Nilpotent (side, generator)

  • For zeroary generators: not applicable.
  • For unary generators:
If C has Nilpotent (Both, A), then C (C x) -> A.

Nilpotent (Left, A) and Nilpotent (Right, A) are errors.

  • For binary generators:
If C has Nilpotent (Left, A), then C (C (x, y), y) -> C (x, A), C (x, x) -> A,

If C has Nilpotent (Right, A), then C (x, C (x, y)) -> C (A, y), C (x, x) -> A,

Nilpotent (Both, A) is the conjunction of Nilpotent (Left, A) and Nilpotent (Right, A).

  • For listary generators:
If C has Nilpotent (Both, A), then

C ...; x; x; ... -> C ...; A; ... if the list has >= 3 elements, C x; x -> A.

Nilpotent (Left, A) and Nilpotent (Right, A) are equivalent to Both.

  • For nary generators: not applicable.
*)
| Precedence of rpo_precedence (*
Definition: Recursive Path Ordering

The Recursive Path Ordering (rpo for short) is an ordering for terms.

Specification for Precedece p

Moca uses a rpo-based completion algorithm to complete the set of rules given by the programmer for the relational data type at hand.

For any generator C, if C has Precedence (p) then C will have precedence p for the rpo-based completion.

Note: integer p must be positive and not equal to Pervasives.max_int.

Per se, the Precedence annotation does not define any statically known rewrite rule. The annotation simply helps moca to complete the set of rules defined so far for the relational data type.

*)
| Rewrite of pattern * expression (*

Specification for Rewrite (pattern, expression)

  • For any generator C, if C has relation Rewrite (pat, expr) then the first clause of its construction function is
| pat -> expr

This clause precedes any other clause necessary for non Rewrite algebraic relations.

  • Multiple Rewrite rules for generator C appears in C construction function in the order of presentation in the relational data type definition.
*)
| Status of rpo_status (*The Status relation is an annotation for a companion generator that mocac uses to complete the set of rules defined so far for the relational data type (Knuth-Bendix competion algorithm).

Per se, the Status relation does not define any rewrite rule.

Specification of Status (stat)

  • For any generator C, if C has property Status (stat) then C will have the stat status for the rpo-based completion.
The status could be lexicographic or multiset.
*)
| Structure_item of structure_item (*A Structure_item holds any Caml definition of some value associated to the relational type specification. Functions defined that way can be used inside the generated construction functions. The definition of a specific compare function for the values of the relational type is typical, to get a semantically sound comparison within the compiler generated construction functions.

Specification of Structure_item (str_item)

  • For any generator C, if C has Structure_item (auxiliary_definition) then the definition auxiliary_definition) is written in the resulting implementation file before the mocac generated definitions for construction functions.
For instance, if C has annotation: begin let f = e;; end then the code "let f = e;;" will be written in the target file before any other mocac generated code.
*)