diff options
| author | Jon French | 2018-04-25 08:45:43 +0100 |
|---|---|---|
| committer | Jon French | 2018-05-01 16:57:35 +0100 |
| commit | 414fe86dbf3f4606d9e1382f238001f58d691620 (patch) | |
| tree | 45dcc2ed5a45573add538791176c817f64968bb7 /language | |
| parent | a9c35efc8e37c1239f1c9dd7514e13e5e884943d (diff) | |
add mpats to asts
Diffstat (limited to 'language')
| -rw-r--r-- | language/sail.ott | 32 |
1 files changed, 26 insertions, 6 deletions
diff --git a/language/sail.ott b/language/sail.ott index a5b30852..cf70fdce 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -251,7 +251,7 @@ typ :: 'Typ_' ::= {{ com type variable }} | typ1 -> typ2 effectkw effect :: :: fn {{ com Function (first-order only in user code) }} - | typ1 <-> typ2 effectkw effect :: :: mapping + | typ1 <-> typ2 :: :: bidir {{ com Mapping }} % TODO: build first-order restriction into AST or just into type rules? neither - see note % TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. @@ -511,6 +511,8 @@ typ_pat :: 'TP_' ::= | kid :: :: var | id ( typ_pat1 , .. , typ_patn ) :: :: app + + pat :: 'P_' ::= {{ com pattern }} {{ aux _ annot }} {{ auxparam 'a }} @@ -980,20 +982,35 @@ fundef :: 'FD_' ::= % recursive functions - the tannot_opt scopes over all the funcli, % which is ok for the typ_quant part but not for the typ part -if_opt :: 'If_' ::= +mpat :: 'MP_' ::= + {{ com Mapping pattern. Mostly the same as normal patterns but only constructible parts }} {{ aux _ annot }} {{ auxparam 'a }} - | if exp :: :: some {{ ocaml Some exp }} - | :: :: none {{ ocaml None }} + | lit :: :: lit + | id :: :: id + | id ( mpat1 , ... , mpatn ) :: :: app + | { fpat1 ; ... ; fpatn semi_opt } :: :: record + | [ mpat1 , ... , mpatn ] :: :: vector + | mpat1 : ... : mpatn :: :: vector_concat + | ( mpat1 , ... , mpatn ) :: :: tup + | [|| mpat1 , ... , mpatn ||] :: :: list + | ( mpat ) :: S :: paren {{ ichlo [[mpat]] }} + | mpat1 '::' mpat2 :: :: cons + | mpat1 ^^ mpat2 :: :: string_append + +mpexp :: 'MPat_' ::= + {{ aux _ annot }} {{ auxparam 'a }} + | mpat :: :: pat + | mpat when exp :: :: when mapcl :: 'MCL_' ::= {{ com mapping clause (bidirectional pattern-match) }} {{ aux _ annot }} {{ auxparam 'a }} - | ( pat1 if_opt1 ) <-> ( pat2 if_opt2 ) :: :: clause + | mpexp1 <-> mpexp2 :: :: mapcl mapdef :: 'MD_' ::= {{ com mapping definition (bidirectional pattern-match function) }} {{ aux _ annot }} {{ auxparam 'a }} - | mapping tannot_opt { mapcl1 , ... , mapcln } :: :: mapping {{ texlong }} + | mapping id = { mapcl1 , ... , mapcln } :: :: mapping {{ texlong }} letbind :: 'LB_' ::= {{ com let binding }} @@ -1137,6 +1154,9 @@ terminals :: '' ::= % {{ com \texttt{<=} }} | -> :: :: arrow {{ tex \ensuremath{\rightarrow} }} + | <-> :: :: bidir + {{ tex \ensuremath{\leftrightarrow} }} + % {{ tex \ottsym{-\textgreater} }} % {{ com \texttt{->} }} | ==> :: :: Longrightarrow |