diff options
| author | Peter Sewell | 2013-06-28 12:03:02 +0100 |
|---|---|---|
| committer | Peter Sewell | 2013-06-28 12:03:02 +0100 |
| commit | dd6e180bc284fd162911ce8fe471c3598b8303ed (patch) | |
| tree | 273ca7cfc371fdc44ea9e6acc5a10ab0b0e1ac1c | |
| parent | 65c5f6dc271578ac0ac9da797ad03930abf535b2 (diff) | |
Brian, Gabriel, Dominic, Thomas, Peter
| -rw-r--r-- | language/l2.ott | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/language/l2.ott b/language/l2.ott index 3234a8e4..eaa07cb2 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -350,13 +350,16 @@ typ :: 'Typ_' ::= % TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. | typ1 * .... * typn :: :: tup {{ com Tuple types }} - | nexp :: :: nexps - {{ com here to permit applications to nexps, otherwise not accepted }} % TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker - | id typ1 .. typn :: :: app - {{ com Type applications }} - | ( typ ) - :: S :: paren {{ icho [[typ]] }} + | id typ_arg1 .. typ_argn :: :: app + {{ com type constructor applications }} + | ( typ ) :: S :: paren {{ icho [[typ]] }} + +typ_arg :: 'Typ_Arg_' ::= + | nexp :: :: nexp + | typ :: :: typ + | endian :: :: endian + | effects :: :: effects % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ @@ -411,6 +414,8 @@ typquant :: 'TQ_' ::= {{ aux _ l }} | forall id1 ... idn . nexp_constraint1 , ... , nexp_constrainti . :: :: Ts {{ texlong }} +% TODO those ids have to have optional kind annotations + % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE | forall id1 ... idn . :: :: Ts_no_constraint {{ com sugar }} @@ -481,6 +486,8 @@ c_tdefbody :: 'C_Te_' ::= {{ com enumeration type definition}} +% + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |