diff options
| author | Kathy Gray | 2013-07-18 15:16:16 +0100 |
|---|---|---|
| committer | Kathy Gray | 2013-07-18 15:16:16 +0100 |
| commit | ce3b6b0c3ea8562c7f58aa960f57ed09622061ce (patch) | |
| tree | b9bc29c137ebbeeba09c5312a92d37f52f9c5345 /language | |
| parent | beec6f494f7a0073d672851d6b949ac2b2fc817f (diff) | |
More parsing
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 8 | ||||
| -rw-r--r-- | language/l2_parse.ott | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/language/l2.ott b/language/l2.ott index 3bdfeba8..47283a84 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -5,7 +5,7 @@ indexvar n , i , j , k ::= metavar num ::= {{ phantom }} {{ lex numeric }} - {{ ocaml terminal * int }} + {{ ocaml (terminal * int) }} {{ hol num }} {{ lem (terminal * num) }} {{ com Numeric literals }} @@ -332,7 +332,7 @@ order :: 'Ord_' ::= | dec :: :: dec {{ com decreasing (big-endian) }} | ( order ) :: S :: paren {{ icho [[order]] }} -effect :: 'Effect_' ::= +efct :: 'Effect_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} @@ -347,8 +347,8 @@ effect :: 'Effect_' ::= effects :: 'Effects_' ::= {{ com effect set, of kind $[[Effects]]$ }} {{ aux _ l }} - | id :: :: var - | { effect1 , .. , effectn } :: :: set {{ com effect set }} + | effect id :: :: var + | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 86f31122..0481c602 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -5,7 +5,7 @@ indexvar n , i , j , k ::= metavar num ::= {{ phantom }} {{ lex numeric }} - {{ ocaml terminal * int }} + {{ ocaml (terminal * int) }} {{ hol num }} {{ lem (terminal * num) }} {{ com Numeric literals }} @@ -304,7 +304,7 @@ kind :: 'K_' ::= | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat -effect :: 'Effect_' ::= +efct :: 'Effect_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} @@ -328,8 +328,8 @@ atyp :: 'ATyp_' ::= | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} - - | { effect1 , .. , effectn } :: :: set {{ com effect set }} + | effect id :: :: efid + | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. |