diff options
| -rw-r--r-- | language/sail.ott | 32 | ||||
| -rw-r--r-- | src/parse_ast.ml | 38 |
2 files changed, 63 insertions, 7 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 diff --git a/src/parse_ast.ml b/src/parse_ast.ml index f71498be..d845265f 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -151,6 +151,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_default_ord (* default order for increasing or decreasing signficant bits *) | ATyp_set of (base_effect) list (* effect set *) | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) + | ATyp_bidir of atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) | ATyp_wild | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) @@ -392,7 +393,6 @@ type funcl = FCL_aux of funcl_aux * l - type type_union = Tu_aux of type_union_aux * l @@ -420,6 +420,41 @@ default_typing_spec_aux = (* Default kinding or typing assumption, and default | DT_typ of typschm * id +type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only constructible parts *) + | MP_lit of lit + | MP_id of id + | MP_app of id * ( mpat) list + | MP_record of ( fpat) list * bool + | MP_vector of ( mpat) list + | MP_vector_concat of ( mpat) list + | MP_tup of ( mpat) list + | MP_list of ( mpat) list + | MP_cons of ( mpat) * ( mpat) + | MP_string_append of ( mpat) * ( mpat) + +and mpat = + | MP_aux of ( mpat_aux) * l + +type mpexp_aux = + | MPat_pat of ( mpat) + | MPat_when of ( mpat) * ( exp) + +type mpexp = + | MPat_aux of ( mpexp_aux) * l + +type mapcl_aux = (* mapping clause (bidirectional pattern-match) *) + | MCL_mapcl of ( mpexp) * ( mpexp) + +type mapcl = + | MCL_aux of ( mapcl_aux) * l + +type mapdef_aux = (* mapping definition (bidirectional pattern-match function) *) + | MD_mapping of id * ( mapcl) list + +type mapdef = + | MD_aux of ( mapdef_aux) * l + + type fundef_aux = (* Function definition *) FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list @@ -502,6 +537,7 @@ def = (* Top-level definition *) DEF_kind of kind_def (* definition of named kind identifiers *) | DEF_type of type_def (* type definition *) | DEF_fundef of fundef (* function definition *) + | DEF_mapdef of mapdef (* mapping definition *) | DEF_val of letbind (* value definition *) | DEF_overload of id * id list (* operator overload specifications *) | DEF_fixity of prec * Big_int.num * id (* fixity declaration *) |