diff options
Diffstat (limited to 'language')
| -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}} +% + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |