diff options
| author | Peter Sewell | 2013-06-21 08:27:37 +0100 |
|---|---|---|
| committer | Peter Sewell | 2013-06-21 08:27:37 +0100 |
| commit | 74e9441821bab0630dc7d42c987cc3fec5bb5147 (patch) | |
| tree | 81cde71d800868a7cc5ecf4fb2de1d1f476b99a8 | |
| parent | d2da2d4f98d7821762e766cc394e857a3ddce7e8 (diff) | |
add effects
| -rw-r--r-- | language/l2.ott | 32 |
1 files changed, 29 insertions, 3 deletions
diff --git a/language/l2.ott b/language/l2.ott index 309ab7ec..c2b98935 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -318,17 +318,42 @@ nexp :: '' ::= end_aux :: 'End_' ::= - {{ com Numerical expressions for specifying vector lengths and indexes}} + {{ com endianness specifications}} | EN :: :: var | inc :: :: inc | dec :: :: dec | ( end ) :: S :: paren {{ icho [[end]] }} end :: '' ::= - {{ com Location-annotated vector lengths }} + {{ com Location-annotated endianness specifications }} | end_aux l :: :: End_l +effect_aux :: 'Effect_' ::= + {{ com effect }} + | rreg :: :: rreg {{ com read register }} + | wreg :: :: wreg {{ com write register }} + | rmem :: :: rmem {{ com read memory }} + | wmem :: :: wmem {{ com write memory }} + | undef :: :: undef {{ com undefined-instruction exception }} + | unspec :: :: unspec {{ com unspecified values }} + | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} + +effect :: '' ::= + {{ com location-annotated effect }} + | effect_aux l :: :: Effect_l + + +effects_aux :: 'Effects_' ::= + {{ com effect set }} + | { effect1 , .. , effectn } :: :: set {{ com effect set }} + | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} + +effects :: '' ::= + {{ com location-annotated effect set }} + | effects_aux l :: :: Effects_l +% TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. + typ_aux :: 'Typ_' ::= {{ com Constructors (of all kinds, not just Type) }} @@ -336,9 +361,10 @@ typ_aux :: 'Typ_' ::= {{ com Unspecified type }} | a_l :: :: var {{ com Type variables }} - | typ1 -> typ2 :: :: fn + | typ1 -> typ2 effects :: :: fn {{ com Function types -- first-order only}} % TODO: build first-order restriction into AST or just into type rules? +% TODO: concrete syntax for effects in a function type? | typ1 * .... * typn :: :: tup {{ com Tuple types }} | nexp :: :: nexps |