diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 1 | ||||
| -rw-r--r-- | language/l2.ml | 21 | ||||
| -rw-r--r-- | language/l2.ott | 1 |
3 files changed, 13 insertions, 10 deletions
diff --git a/language/l2.lem b/language/l2.lem index 4ba01310..32b6f1c7 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -247,6 +247,7 @@ and exp 'a = and lexp_aux 'a = (* lvalue expression *) | LEXP_id of id (* identifier *) | LEXP_memory of id * list (exp 'a) (* memory write via function call *) + | LEXP_cast of typ * id | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) | LEXP_field of (lexp 'a) * id (* struct field *) diff --git a/language/l2.ml b/language/l2.ml index 4e58d63c..80c94b39 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -74,6 +74,12 @@ base_effect = type +effect_aux = (* effect set, of kind Effects *) + Effect_var of kid + | Effect_set of (base_effect) list (* effect set *) + + +type order_aux = (* vector order specifications, of kind Order *) Ord_var of kid (* variable *) | Ord_inc (* increasing (little-endian) *) @@ -81,25 +87,19 @@ order_aux = (* vector order specifications, of kind Order *) type -effect_aux = (* effect set, of kind Effects *) - Effect_var of kid - | Effect_set of (base_effect) list (* effect set *) - - -type id_aux = (* Identifier *) Id of x | DeIid of x (* remove infix status *) type -order = - Ord_aux of order_aux * l +effect = + Effect_aux of effect_aux * l type -effect = - Effect_aux of effect_aux * l +order = + Ord_aux of order_aux * l type @@ -289,6 +289,7 @@ and 'a exp = and 'a lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) | LEXP_memory of id * ('a exp) list (* memory write via function call *) + | LEXP_cast of typ * id | LEXP_vector of 'a lexp * 'a exp (* vector element *) | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) | LEXP_field of 'a lexp * id (* struct field *) diff --git a/language/l2.ott b/language/l2.ott index 6efabf62..8aa7417a 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -636,6 +636,7 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ com identifier }} | id ( exp1 , .. , expn ) :: :: memory {{ com memory write via function call }} | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} + | ( typ ) id :: :: cast | lexp [ exp ] :: :: vector {{ com vector element }} | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} % maybe comma-sep such lists too |