diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/sail.ott | 54 |
1 files changed, 51 insertions, 3 deletions
diff --git a/language/sail.ott b/language/sail.ott index 8469e029..83d80be8 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -251,6 +251,8 @@ typ :: 'Typ_' ::= {{ com type variable }} | typ1 -> typ2 effectkw effect :: :: fn {{ com Function (first-order only in user code) }} + | 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. | ( typ1 , .... , typn ) :: :: tup @@ -509,6 +511,8 @@ typ_pat :: 'TP_' ::= | kid :: :: var | id ( typ_pat1 , .. , typ_patn ) :: :: app + + pat :: 'P_' ::= {{ com pattern }} {{ aux _ annot }} {{ auxparam 'a }} @@ -554,12 +558,15 @@ pat :: 'P_' ::= | ( pat1 , .... , patn ) :: :: tup {{ com tuple pattern }} - | [|| pat1 , .. , patn ||] :: :: list + | [|| pat1 , .. , patn ||] :: :: list {{ com list pattern }} | ( pat ) :: S :: paren {{ ichlo [[pat]] }} - | pat1 '::' pat2 :: :: cons - {{ com Cons patterns }} + | pat1 '::' pat2 :: :: cons + {{ com Cons patterns }} + + | pat1 ^^ ... ^^ patn :: :: string_append + {{ com string append pattern, x ^^ y }} % XXX Is this still useful? fpat :: 'FP_' ::= @@ -567,6 +574,11 @@ fpat :: 'FP_' ::= {{ aux _ annot }} {{ auxparam 'a }} | id = pat :: :: Fpat +mfpat :: 'MFP_' ::= + {{ com Mapping field pattern, why does this have to exist }} + {{ aux _ annot }} {{ auxparam 'a }} + | id = mpat :: :: mpat + parsing P_app <= P_app P_app <= P_as @@ -976,6 +988,37 @@ 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 +mpat :: 'MP_' ::= + {{ com Mapping pattern. Mostly the same as normal patterns but only constructible parts }} + {{ aux _ annot }} {{ auxparam 'a }} + | lit :: :: lit + | id :: :: id + | id ( mpat1 , ... , mpatn ) :: :: app + | { mfpat1 ; ... ; mfpatn 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 ^^ ... ^^ mpatn :: :: string_append + | mpat : typ :: :: typ + +mpexp :: 'MPat_' ::= + {{ aux _ annot }} {{ auxparam 'a }} + | mpat :: :: pat + | mpat when exp :: :: when + +mapcl :: 'MCL_' ::= + {{ com mapping clause (bidirectional pattern-match) }} + {{ aux _ annot }} {{ auxparam 'a }} + | mpexp1 <-> mpexp2 :: :: mapcl + +mapdef :: 'MD_' ::= + {{ com mapping definition (bidirectional pattern-match function) }} + {{ aux _ annot }} {{ auxparam 'a }} + | mapping id = { mapcl1 , ... , mapcln } :: :: mapping {{ texlong }} + letbind :: 'LB_' ::= {{ com let binding }} {{ aux _ annot }} {{ auxparam 'a }} @@ -1076,6 +1119,8 @@ def :: 'DEF_' ::= {{ com type definition }} | fundef :: :: fundef {{ com function definition }} + | mapdef :: :: mapdef + {{ com mapping definition }} | letbind :: :: val {{ com value definition }} | val_spec :: :: spec @@ -1116,6 +1161,9 @@ terminals :: '' ::= % {{ com \texttt{<=} }} | -> :: :: arrow {{ tex \ensuremath{\rightarrow} }} + | <-> :: :: bidir + {{ tex \ensuremath{\leftrightarrow} }} + % {{ tex \ottsym{-\textgreater} }} % {{ com \texttt{->} }} | ==> :: :: Longrightarrow |