diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 2 | ||||
| -rw-r--r-- | language/l2.ml | 22 | ||||
| -rw-r--r-- | language/l2.ott | 9 | ||||
| -rw-r--r-- | language/l2_parse.ml | 2 | ||||
| -rw-r--r-- | language/l2_parse.ott | 5 |
5 files changed, 21 insertions, 19 deletions
diff --git a/language/l2.lem b/language/l2.lem index 64838e88..630c976d 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -155,7 +155,7 @@ type exp = (* Expression *) | E_app_infix of exp * id * exp (* infix function application *) | E_tuple of list exp (* tuple *) | E_if of exp * exp * exp (* conditional *) - | E_for of id * exp * exp * exp * exp (* loop *) + | E_for of id * exp * exp * exp * order * exp (* loop *) | E_vector of list exp (* vector (indexed from 0) *) | E_vector_indexed of list (natural * exp) (* vector (indexed consecutively) *) | E_vector_access of exp * exp (* vector access *) diff --git a/language/l2.ml b/language/l2.ml index 02b5276a..b01a25ac 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -73,12 +73,6 @@ 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) *) @@ -86,19 +80,25 @@ 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 -effect = - Effect_aux of effect_aux * l +order = + Ord_aux of order_aux * l type -order = - Ord_aux of order_aux * l +effect = + Effect_aux of effect_aux * l type @@ -266,7 +266,7 @@ and 'a exp_aux = (* Expression *) | E_app_infix of 'a exp * id * 'a exp (* infix function application *) | E_tuple of ('a exp) list (* tuple *) | E_if of 'a exp * 'a exp * 'a exp (* conditional *) - | E_for of id * 'a exp * 'a exp * 'a exp * 'a exp (* loop *) + | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *) | E_vector of ('a exp) list (* vector (indexed from 0) *) | E_vector_indexed of ((int * 'a exp)) list (* vector (indexed consecutively) *) | E_vector_access of 'a exp * 'a exp (* vector access *) diff --git a/language/l2.ott b/language/l2.ott index b760ca75..8cbacf0d 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -545,10 +545,11 @@ exp :: 'E_' ::= | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }} - | foreach id from exp1 to exp2 by exp3 exp4 :: :: for {{ com loop }} - | foreach id from exp1 to exp2 exp3 :: S :: forbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 exp4 ]] }} - | foreach id from exp1 downto exp2 by exp3 exp4 :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }} - | foreach id from exp1 downto exp2 exp3 :: S :: fordownbyone {{ ichlo [[ foreach id from exp1 downto exp2 by 1 exp4 ]] }} + | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }} + | foreach ( id from exp1 to exp2 by exp3 ) exp4 :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }} + | foreach ( id from exp1 to exp2 ) exp3 :: S :: forupbyone {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }} + | foreach ( id from exp1 downto exp2 by exp3 ) exp4 :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in dec exp4 ]] }} + | foreach ( id from exp1 downto exp2 ) exp3 :: S :: fordownbyone {{ ichlo [[ foreach id from exp1 downto exp2 by 1 in dec exp4 ]] }} % vectors | [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index a6ada0ec..8615faa6 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -205,7 +205,7 @@ exp_aux = (* Expression *) | E_app_infix of exp * id * exp (* infix function application *) | E_tuple of (exp) list (* tuple *) | E_if of exp * exp * exp (* conditional *) - | E_for of id * exp * exp * exp * exp (* loop *) + | E_for of id * exp * exp * exp * atyp * exp (* loop *) | E_vector of (exp) list (* vector (indexed from 0) *) | E_vector_indexed of ((int * exp)) list (* vector (indexed consecutively) *) | E_vector_access of exp * exp (* vector access *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 2fbf860e..da3d57ca 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -444,8 +444,9 @@ exp :: 'E_' ::= | if exp1 then exp2 :: S :: ifnoelse {{ icho [[ if exp1 then exp2 else unit ]] }} - | foreach id from exp1 to exp2 by exp3 exp4 :: :: for {{ com loop }} - | foreach id from exp1 to exp2 exp3 :: S :: forbyone {{ icho [[ foreach id from exp1 to exp2 by 1 exp4 ]] }} + | foreach id from exp1 to exp2 by exp3 in atyp exp4 :: :: for {{ com loop }} + | foreach id from exp1 to exp2 by exp3 exp4 :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }} + | foreach id from exp1 to exp2 exp3 :: S :: forupbyone {{ icho [[ foreach id from exp1 to exp2 by 1 exp4 ]] }} | foreach id from exp1 downto exp2 by exp3 exp4 :: S :: fordown {{ icho [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }} | foreach id from exp1 downto exp2 exp3 :: S :: fordownbyone {{ icho [[ foreach id from exp1 downto exp2 by 1 exp4 ]] }} |