module Parsetree:`sig`

..`end`

`type `

type_declaration = {

` ` |
`ptype_params : ` |

` ` |
`ptype_cstrs : ` |

` ` |
`ptype_kind : ` |

` ` |
`ptype_private : ` |

` ` |
`ptype_manifest : ` |

` ` |
`ptype_variance : ` |

` ` |
`ptype_loc : ` |

`type `

type_kind =

`|` |
`Ptype_abstract of ` |

`|` |
`Ptype_variant of ` |

`|` |
`Ptype_record of ` |

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.

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.

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$).

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.

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:

`cmp`

induces a`>=`

total ordering:

` x >= y`

if and only if ` cmp x y >= 0 `

; then
` >= `

must be a total ordering:`>=`

is reflexive: for all x, x`>=`

x`>=`

is transitive: for all x y z, x`>=`

y /\ y`>=`

z => x`>=`

z`>=`

is anti-symmetric: for all x y, x`>=`

y /\ y`>=`

x => x $=$ y (in this definition $=$ is the syntactic equality, ie. x $=$ y if and only if`Pervasives.compare x y = 0`

)`>=`

is total: for all x y, x`>=`

y \/ y`>=`

x

`cmp`

is compatible with the language structural equality: $\forall x y. cmp x y = 0 => Pervasives.compare x y = 0$.

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 : ` |

` ` |
`pgen_loc : ` |

`type `

relations = {

` ` |
`prels_desc : ` |

` ` |
`prels_loc : ` |

`type `

relations_desc =

`|` |
`Prels_none` |

`|` |
`Prels_commented of ` |

`|` |
`Prels_begend of ` |

`type `

relation = {

` ` |
`prel_desc : ` |

` ` |
`prel_loc : ` |

`type `

rel_desc =

`|` |
`Absorbent of ` |
`(*` | ## Specification for Absorbent (side, A)
- For zeroary generators: not applicable.
- For unary generators:
Absorbent (Left, A) and Absorbent (Right, A) are erroneous.
- For binary generators:
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:
`b1; ...; bn; A; c1; ...; cn` -> A.
In particular:
C ` A ` -> A.
If C has Absorbent (Left, A), then
C
If C has Absorbent (Right, A), then
C Absorbent (Both, A) is the conjunction of Absorbent (Left, A) and Absorbent (Right, A).
- For nary generators: not applicable.
| `*)` |

`|` |
`Absorbing of ` |
`(*` | ## Specification for Absorbing
- For zeroary generators: not applicable
- For unary generators: not applicable
- For binary generators:
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 ` |
`(*` | 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 (Right), then C (x, C (y, z)) -> C (C (x, y), z). Associative (Both) is equivalent to Associative (Left).
- For listary generators:
`...; C [x; ...; y]; ...` -> C `...; x; ...; y; ...` ,
Associative (Both) and Associative (Right) are equivalent to Associative (Left).
- For nary generators: not applicable.
| `*)` |

`|` |
`Commutative of ` |
`(*` | ## Specification for Commutative (cmp)
The optional argument
If no
- For zeroary generators: not applicable.
- For unary generators: not applicable.
- For binary generators:
If C has Commutative (Some cmp), then the arguments of
C are sorted in increasing order with respect to 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 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:
`cmp` ,
C
- For nary generators: not applicable.
| `*)` |

`|` |
`Distributive of ` |
`(*` | ## 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, 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)`
Distributive (Right, D, generator_option, dir) and Distributive (Left, D, generator_option, dir) are errors.
- For binary generators:
`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:
`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
if E is listary:
if D is zeroary:
C
if E is nary (then D must be nary with the same arity as E),
C Distributive (Right, D, generator_option, dir) and Distributive (Left, D, generator_option, dir) are errors.
- For nary generators: not applicable.
| `*)` |

`|` |
`Division_by_Absorbent of ` |
`(*` | 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:
- 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 ` |
`(*` | ## Specification of Idempotent (side)
- For zeroary generators: not applicable.
- For unary generators:
Idempotent (Left) and Idempotent (Right) are errors.
- For binary generators:
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:
`...; 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 ` |
`(*` | ## Specification for Inverse (side, generator, generator option)
- For zeroary generators: not applicable.
- For unary generators:
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 (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 (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 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 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:
- For binary generators: not applicable.
- For listary generators: not applicable.
- For nary generators: not applicable.
| `*)` |

`|` |
`Neutral of ` |
`(*` | ## Specification for Neutral (side, generator)
- For zeroary generators: not applicable.
- For unary generators:
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 (Right, E), then C (x, E) -> x, Neutral (Both, E) is the conjunction of Neutral (Left, E) and Neutral (Right, E).
- For listary generators:
`...; 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 Neutral (Both, E) is the conjunction of Neutral (Left, E) and Neutral (Right, E).
- For nary generators: not applicable.
| `*)` |

`|` |
`Nilpotent of ` |
`(*` | ## Specification for Nilpotent (side, generator)
- For zeroary generators: not applicable.
- For unary generators:
Nilpotent (Left, A) and Nilpotent (Right, A) are errors.
- For binary generators:
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:
C Nilpotent (Left, A) and Nilpotent (Right, A) are equivalent to Both.
- For nary generators: not applicable.
| `*)` |

`|` |
`Precedence of ` |
`(*` | ## Definition: Recursive Path Ordering
The
## Specification for Precedece pMoca 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 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 ` |
`(*` | ## 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
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 ` |
`(*` | 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.
`lexicographic` or `multiset` . | `*)` |

`|` |
`Structure_item of ` |
`(*` | 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.
| `*)` |