diff options
| author | Gabriel Kerneis | 2014-05-20 15:03:20 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-05-20 15:03:34 +0100 |
| commit | 1c5d405883febc79ea3958a989221dad2e491d27 (patch) | |
| tree | d6bebd90e9b2a571649928e7f53f0094f3c02463 /language/l2.ott | |
| parent | f45a2717796f2c416e857f6db25c242b701e4dba (diff) | |
| parent | 8cd3f794d59170d519f5000cc13f6a3c9cde849c (diff) | |
Merge new pretty-printer
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/language/l2.ott b/language/l2.ott index 7b619652..a880527c 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -482,7 +482,7 @@ pat :: 'P_' ::= | [ pat1 , .. , patn ] :: :: vector {{ com vector pattern }} - | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed + | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed {{ com vector pattern (with explicit indices) }} % cf ntoes for this @@ -561,7 +561,7 @@ exp :: 'E_' ::= % here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn % the expi and the result are both of type vector of 'a - | [ num1 = exp1 , ... , numn = expn ] :: :: vector_indexed {{ com vector (indexed consecutively) }} + | [ num1 = exp1 , ... , numn = expn , opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }} % num1 .. numn must be a consecutive list of naturals % we pick [ ] not { } for vector literals for consistency with their @@ -655,6 +655,12 @@ fexps :: 'FES_' ::= {{ aux _ annot }} {{ auxparam 'a }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps +opt_default :: 'Def_val_' ::= + {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }} + {{ aux _ annot }} {{ auxparam 'a }} + | :: :: empty + | default = exp :: :: dec + pexp :: 'Pat_' ::= {{ com Pattern match }} {{ aux _ annot }} {{ auxparam 'a }} |