diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 3 | ||||
| -rw-r--r-- | language/l2.ml | 3 | ||||
| -rw-r--r-- | language/l2.ott | 3 | ||||
| -rw-r--r-- | language/l2_parse.ml | 1 | ||||
| -rw-r--r-- | language/l2_parse.ott | 1 | ||||
| -rw-r--r-- | language/l2_typ.ott | 1 |
6 files changed, 9 insertions, 3 deletions
diff --git a/language/l2.lem b/language/l2.lem index d9b410cd..eb598113 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -50,8 +50,9 @@ type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_constant of integer (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction, error for nexp1 to be smaller than nexp2 *) | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* For internal use. Not M as a dataconstructor is required *) + | Nexp_neg of nexp (* For internal use *) and nexp = | Nexp_aux of nexp_aux * l diff --git a/language/l2.ml b/language/l2.ml index dc96020d..d4423c54 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -45,8 +45,9 @@ nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_constant of int (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction, error for nexp1 to be smaller than nexp2 *) | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* For internal use. Not M as a dataconstructor is required *) + | Nexp_neg of nexp (* For internal use *) and nexp = Nexp_aux of nexp_aux * l diff --git a/language/l2.ott b/language/l2.ott index 77b2483b..59de79cd 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -166,8 +166,9 @@ nexp :: 'Nexp_' ::= | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} | nexp1 + nexp2 :: :: sum {{ com sum }} + | nexp1 - nexp2 :: :: minus {{ com subtraction, error for nexp1 to be smaller than nexp2 }} | 2** nexp :: :: exp {{ com exponential }} - | neg nexp :: :: neg {{ com For internal use. Not M as a dataconstructor is required }} + | neg nexp :: :: neg {{ com For internal use }} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 5aaf8086..ed594d3b 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -84,6 +84,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_constant of int (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) + | ATyp_minus of atyp * atyp (* subtraction *) | ATyp_exp of atyp (* exponential *) | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *) | ATyp_inc (* increasing (little-endian) *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 74522150..7126b9e0 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -168,6 +168,7 @@ atyp :: 'ATyp_' ::= | num :: :: constant {{ com constant }} | atyp1 * atyp2 :: :: times {{ com product }} | atyp1 + atyp2 :: :: sum {{ com sum }} + | atyp1 - atyp2 :: :: minus {{ com subtraction }} | 2** atyp :: :: exp {{ com exponential }} | neg atyp :: :: neg {{ com Internal (but not M as I want a datatype constructor) negative nexp }} | ( atyp ) :: S :: paren {{ icho [[atyp]] }} diff --git a/language/l2_typ.ott b/language/l2_typ.ott index 12baa059..3ffc5b2b 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -85,6 +85,7 @@ ne :: 'Ne_' ::= | infinity :: :: inf | ne1 * ne2 :: :: mult | ne1 + ... + nen :: :: add + | ne1 - ne2 :: :: minus | 2 ** ne :: :: exp | ( - ne ) :: :: unary | zero :: S :: zero |