Merge branch 'mappings' into sail2

1 files changed, 52 insertions, 3 deletions

diff --git a/language/sail.ott b/language/sail.ott
index 8469e029..6094f74e 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -245,12 +245,15 @@ effect :: 'Effect_' ::=
 typ :: 'Typ_' ::=
   {{ com type expressions, of kind $[[Type]]$ }}
   {{ aux _ l }}
+  |                                            :: :: internal_unknown
   | id                                         :: :: id
     {{ com defined type }}
   | kid                                         :: :: var
     {{ 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 +512,8 @@ typ_pat :: 'TP_' ::=
   | kid                             :: :: var
   | id ( typ_pat1 , .. , typ_patn ) :: :: app
 
+
+
 pat :: 'P_' ::= 
   {{ com pattern }}
   {{ aux _ annot }} {{ auxparam 'a }}
@@ -554,12 +559,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 +575,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 +989,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 tannot_opt = { mapcl1 , ... , mapcln } :: :: mapping {{ texlong }}
+
 letbind :: 'LB_' ::=
   {{ com let binding }}
   {{ aux _ annot }} {{ auxparam 'a }}
@@ -1076,6 +1120,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 +1162,9 @@ terminals :: '' ::=
 %     {{ com \texttt{<=} }}
    | ->                                  :: :: arrow
     {{ tex \ensuremath{\rightarrow} }}
+   | <->                                 :: :: bidir
+    {{ tex \ensuremath{\leftrightarrow} }}
+
 %     {{ tex \ottsym{-\textgreater} }}
 %     {{ com \texttt{->} }}
    | ==>                                 :: :: Longrightarrow