Allow wildcards in forwards and backwards mapping clauses

editors/sail-mode.el

@@ -36,7 +36,7 @@
     "overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from"
     "pure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to"
     "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
-    "mapping" "where" "with" "implicit" "instantiation" "impl"))
+    "mapping" "where" "with" "implicit" "instantiation" "impl" "forwards" "backwards"))
 
 (defconst sail-project-keywords
   '("after" "before" "directory" "else" "file" "files" "if" "default" "module" "optional" "requires" "then" "variable"))

language/sail.ott

@@ -539,8 +539,8 @@ opt_default :: 'Def_val_' ::=
 pexp :: 'Pat_' ::=
   {{ com pattern match }}
   {{ aux _ annot }} {{ auxparam 'a }}
-  | pat -> exp                          :: :: exp
-  | pat when exp1 -> exp                :: :: when
+  | pat => exp                        :: :: exp
+  | pat if exp1 => exp                :: :: when
 % apparently could use -> or => for this.
 
 %% % psexp :: 'Pats' ::=
@@ -647,8 +647,8 @@ mapcl :: 'MCL_' ::=
   {{ com mapping clause (bidirectional pattern-match) }}
   {{ aux _ clause_annot }} {{ auxparam 'a }}
   | mpexp1 <-> mpexp2 :: :: bidir
-  | mpexp   => exp    :: :: forwards
-  | mpexp  <-  exp    :: :: backwards
+  | forwards pexp     :: :: forwards
+  | backwards pexp    :: :: backwards
 
 
 mapdef :: 'MD_' ::=

src/lib/ast_util.ml

@@ -743,10 +743,8 @@ and map_mpexp_annot_aux f = function
 and map_mapcl_annot f = function
   | MCL_aux (MCL_bidir (mpexp1, mpexp2), annot) ->
       MCL_aux (MCL_bidir (map_mpexp_annot f mpexp1, map_mpexp_annot f mpexp2), map_clause_annot f annot)
-  | MCL_aux (MCL_forwards (mpexp, exp), annot) ->
-      MCL_aux (MCL_forwards (map_mpexp_annot f mpexp, map_exp_annot f exp), map_clause_annot f annot)
-  | MCL_aux (MCL_backwards (mpexp, exp), annot) ->
-      MCL_aux (MCL_backwards (map_mpexp_annot f mpexp, map_exp_annot f exp), map_clause_annot f annot)
+  | MCL_aux (MCL_forwards pexp, annot) -> MCL_aux (MCL_forwards (map_pexp_annot f pexp), map_clause_annot f annot)
+  | MCL_aux (MCL_backwards pexp, annot) -> MCL_aux (MCL_backwards (map_pexp_annot f pexp), map_clause_annot f annot)
 
 and map_mpat_annot f (MP_aux (mpat, annot)) = MP_aux (map_mpat_annot_aux f mpat, f annot)
 

src/lib/effects.ml

@@ -229,6 +229,12 @@ let infer_mapdef_extra_direct_effects def =
   let forward_effects = ref EffectSet.empty in
   let backward_effects = ref EffectSet.empty in
 
+  let scan_pat set p_aux annot =
+    begin
+      match p_aux with P_string_append _ -> set := EffectSet.add NonExec !set | _ -> ()
+    end;
+    P_aux (p_aux, annot)
+  in
   let scan_mpat set mp_aux annot =
     match mp_aux with
     | Some (MP_string_append _ as aux) ->
@@ -237,7 +243,11 @@ let infer_mapdef_extra_direct_effects def =
     | Some aux -> Some (MP_aux (aux, annot))
     | None -> None
   in
+  let rw_pat set = fold_pat { id_pat_alg with p_aux = (fun (p_aux, annot) -> scan_pat set p_aux annot) } in
   let rw_mpat set = fold_mpat { id_mpat_alg with p_aux = (fun (mp_aux, annot) -> scan_mpat set mp_aux annot) } in
+  let scan_pexp set (Pat_aux (aux, _)) =
+    match aux with Pat_exp (pat, _) -> ignore (rw_pat set pat) | Pat_when (pat, _, _) -> ignore (rw_pat set pat)
+  in
   let scan_mpexp set (MPat_aux (aux, _)) =
     match aux with MPat_pat mpat -> ignore (rw_mpat set mpat) | MPat_when (mpat, _) -> ignore (rw_mpat set mpat)
   in
@@ -246,8 +256,8 @@ let infer_mapdef_extra_direct_effects def =
     | MCL_bidir (forward, backward) ->
         scan_mpexp forward_effects forward;
         scan_mpexp backward_effects backward
-    | MCL_forwards (forward, _) -> scan_mpexp forward_effects forward
-    | MCL_backwards (backward, _) -> scan_mpexp backward_effects backward
+    | MCL_forwards forward -> scan_pexp forward_effects forward
+    | MCL_backwards backward -> scan_pexp backward_effects backward
   in
 
   begin

src/lib/initial_check.ml

@@ -1162,6 +1162,11 @@ let to_ast_mpexp ctx (P.MPat_aux (mpexp, l)) =
   | P.MPat_pat mpat -> MPat_aux (MPat_pat (to_ast_mpat ctx mpat), (l, empty_uannot))
   | P.MPat_when (mpat, exp) -> MPat_aux (MPat_when (to_ast_mpat ctx mpat, to_ast_exp ctx exp), (l, empty_uannot))
 
+let pexp_of_mpexp (MPat_aux (aux, annot)) exp =
+  match aux with
+  | MPat_pat mpat -> Pat_aux (Pat_exp (pat_of_mpat mpat, exp), annot)
+  | MPat_when (mpat, guard) -> Pat_aux (Pat_when (pat_of_mpat mpat, guard, exp), annot)
+
 let rec to_ast_mapcl doc attrs ctx (P.MCL_aux (mapcl, l)) =
   match mapcl with
   | P.MCL_attribute (attr, arg, mcl) -> to_ast_mapcl doc (attrs @ [(l, attr, arg)]) ctx mcl
@@ -1172,10 +1177,12 @@ let rec to_ast_mapcl doc attrs ctx (P.MCL_aux (mapcl, l)) =
     end
   | P.MCL_bidir (mpexp1, mpexp2) ->
       MCL_aux (MCL_bidir (to_ast_mpexp ctx mpexp1, to_ast_mpexp ctx mpexp2), (mk_def_annot ?doc ~attrs l, empty_uannot))
-  | P.MCL_forwards (mpexp, exp) ->
-      MCL_aux (MCL_forwards (to_ast_mpexp ctx mpexp, to_ast_exp ctx exp), (mk_def_annot ?doc ~attrs l, empty_uannot))
-  | P.MCL_backwards (mpexp, exp) ->
-      MCL_aux (MCL_backwards (to_ast_mpexp ctx mpexp, to_ast_exp ctx exp), (mk_def_annot ?doc ~attrs l, empty_uannot))
+  | P.MCL_forwards_deprecated (mpexp, exp) ->
+      let mpexp = to_ast_mpexp ctx mpexp in
+      let exp = to_ast_exp ctx exp in
+      MCL_aux (MCL_forwards (pexp_of_mpexp mpexp exp), (mk_def_annot ?doc ~attrs l, empty_uannot))
+  | P.MCL_forwards pexp -> MCL_aux (MCL_forwards (to_ast_case ctx pexp), (mk_def_annot ?doc ~attrs l, empty_uannot))
+  | P.MCL_backwards pexp -> MCL_aux (MCL_backwards (to_ast_case ctx pexp), (mk_def_annot ?doc ~attrs l, empty_uannot))
 
 let to_ast_mapdef ctx (P.MD_aux (md, l) : P.mapdef) : uannot mapdef =
   match md with

src/lib/parse_ast.ml

@@ -362,8 +362,9 @@ and mapcl_aux =
   | MCL_attribute of string * string * mapcl
   | MCL_doc of string * mapcl
   | MCL_bidir of mpexp * mpexp
-  | MCL_forwards of mpexp * exp
-  | MCL_backwards of mpexp * exp
+  | MCL_forwards_deprecated of mpexp * exp
+  | MCL_forwards of pexp
+  | MCL_backwards of pexp
 
 type mapdef_aux =
   (* mapping definition (bidirectional pattern-match function) *)

src/lib/parser.mly

@@ -154,8 +154,9 @@ let mk_subst ev n m = IS_aux (ev, loc n m)
 let mk_mpexp mpexp n m = MPat_aux (mpexp, loc n m)
 let mk_mpat mpat n m = MP_aux (mpat, loc n m)
 let mk_bidir_mapcl mpexp1 mpexp2 n m = MCL_aux (MCL_bidir (mpexp1, mpexp2), loc n m)
-let mk_forwards_mapcl mpexp exp n m = MCL_aux (MCL_forwards (mpexp, exp), loc n m)
-let mk_backwards_mapcl mpexp exp n m = MCL_aux (MCL_backwards (mpexp, exp), loc n m)
+let mk_forwards_mapcl_deprecated mpexp exp n m = MCL_aux (MCL_forwards_deprecated (mpexp, exp), loc n m)
+let mk_forwards_mapcl pexp n m = MCL_aux (MCL_forwards pexp, loc n m)
+let mk_backwards_mapcl pexp n m = MCL_aux (MCL_backwards pexp, loc n m)
 let mk_map id tannot mapcls n m = MD_aux (MD_mapping (id, tannot, mapcls), loc n m)
 
 let qi_id_of_kopt (KOpt_aux (_, l) as kopt) = QI_aux (QI_id kopt, l)
@@ -223,6 +224,9 @@ let old_bitfield_deprecated ?(bitfield = "<bitfield>") l field =
 let warn_extern_effect l =
   Reporting.warn ~once_from:__POS__ "Deprecated" l "All external bindings should be marked as either monadic or pure"
 
+let forwards_mapcl_deprecated l =
+  Reporting.warn ~once_from:__POS__ "Deprecated" l "Single direction mapping clause should be prefixed by a direction, either forwards or backwards"
+
 let set_syntax_deprecated l =
   Reporting.warn ~once_from:__POS__ "Deprecated" l "Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}."
 
@@ -1138,11 +1142,12 @@ mapcl:
   | mpexp Bidir mpexp
     { mk_bidir_mapcl $1 $3 $startpos $endpos }
   | mpexp EqGt exp
-    { mk_forwards_mapcl $1 $3 $startpos $endpos }
-  | Forwards mpexp EqGt exp
-    { mk_forwards_mapcl $2 $4 $startpos $endpos }
-  | Backwards mpexp EqGt exp
-    { mk_backwards_mapcl $2 $4 $startpos $endpos }
+    { forwards_mapcl_deprecated (loc $startpos $endpos);
+      mk_forwards_mapcl_deprecated $1 $3 $startpos $endpos }
+  | Forwards case
+    { mk_forwards_mapcl $2 $startpos $endpos }
+  | Backwards case
+    { mk_backwards_mapcl $2 $startpos $endpos }
 
 mapcl_list:
   | mapcl Comma?

src/lib/pretty_print_sail.ml

@@ -634,14 +634,8 @@ let doc_mapcl (MCL_aux (cl, (def_annot, _))) =
       let left = doc_mpexp mpexp1 in
       let right = doc_mpexp mpexp2 in
       separate space [left; string "<->"; right]
-  | MCL_forwards (mpexp, exp) ->
-      let left = doc_mpexp mpexp in
-      let right = doc_exp exp in
-      separate space [left; string "=>"; right]
-  | MCL_backwards (mpexp, exp) ->
-      let left = doc_mpexp mpexp in
-      let right = doc_exp exp in
-      separate space [left; string "<-"; right]
+  | MCL_forwards pexp -> string "forwards" ^^ space ^^ doc_pexp pexp
+  | MCL_backwards pexp -> string "backwards" ^^ space ^^ doc_pexp pexp
 
 let doc_mapdef (MD_aux (MD_mapping (id, _, mapcls), _)) =
   match mapcls with

src/lib/rewriter.ml

@@ -304,8 +304,8 @@ let rewrite_mapcl rewriters (MCL_aux (aux, def_annot)) =
   let aux =
     match aux with
     | MCL_bidir (mpexp1, mpexp2) -> MCL_bidir (rewrite_mpexp rewriters mpexp1, mpexp2)
-    | MCL_forwards (mpexp, exp) -> MCL_forwards (rewrite_mpexp rewriters mpexp, rewriters.rewrite_exp rewriters exp)
-    | MCL_backwards (mpexp, exp) -> MCL_backwards (rewrite_mpexp rewriters mpexp, rewriters.rewrite_exp rewriters exp)
+    | MCL_forwards pexp -> MCL_forwards (rewrite_pexp rewriters pexp)
+    | MCL_backwards pexp -> MCL_backwards (rewrite_pexp rewriters pexp)
   in
   MCL_aux (aux, def_annot)
 

src/lib/rewrites.ml

@@ -3225,26 +3225,23 @@ let rewrite_ast_realize_mappings effect_info env ast =
     | MPat_aux (MPat_pat mpat, annot) -> Pat_aux (Pat_exp (pat_of_mpat mpat, exp), annot)
     | MPat_aux (MPat_when (mpat, guard), annot) -> Pat_aux (Pat_when (pat_of_mpat mpat, guard, exp), annot)
   in
-  let realize_single_mpexp mpexp exp =
-    match mpexp with
-    | MPat_aux (MPat_pat mpat, annot) -> Pat_aux (Pat_exp (pat_of_mpat mpat, exp), annot)
-    | MPat_aux (MPat_when (mpat, guard), annot) -> Pat_aux (Pat_when (pat_of_mpat mpat, guard, exp), annot)
+  let true_pexp = function
+    | Pat_aux (Pat_exp (pat, _), annot) -> Pat_aux (Pat_exp (pat, mk_lit_exp L_true), annot)
+    | Pat_aux (Pat_when (pat, guard, _), annot) -> Pat_aux (Pat_when (pat, guard, mk_lit_exp L_true), annot)
   in
   let realize_mapcl forwards id mapcl =
     match mapcl with
     | MCL_aux (MCL_bidir (mpexp1, mpexp2), _) -> [realize_mpexps forwards mpexp1 mpexp2]
-    | MCL_aux (MCL_forwards (mpexp, exp), _) -> if forwards then [realize_single_mpexp mpexp exp] else []
-    | MCL_aux (MCL_backwards (mpexp, exp), _) -> if forwards then [] else [realize_single_mpexp mpexp exp]
+    | MCL_aux (MCL_forwards pexp, _) -> if forwards then [pexp] else []
+    | MCL_aux (MCL_backwards pexp, _) -> if forwards then [] else [pexp]
   in
   let realize_bool_mapcl forwards id mapcl =
     match mapcl with
     | MCL_aux (MCL_bidir (mpexp1, mpexp2), _) ->
         let mpexp = if forwards then mpexp1 else mpexp2 in
         [realize_mpexps true mpexp (mk_mpexp (MPat_pat (mk_mpat (MP_lit (mk_lit L_true)))))]
-    | MCL_aux (MCL_forwards (mpexp, exp), _) ->
-        if forwards then [realize_single_mpexp mpexp (mk_lit_exp L_true)] else []
-    | MCL_aux (MCL_backwards (mpexp, exp), _) ->
-        if forwards then [] else [realize_single_mpexp mpexp (mk_lit_exp L_true)]
+    | MCL_aux (MCL_forwards pexp, _) -> if forwards then [true_pexp pexp] else []
+    | MCL_aux (MCL_backwards pexp, _) -> if forwards then [] else [true_pexp pexp]
   in
   let arg_id = mk_id "arg#" in
   let arg_exp = mk_exp (E_id arg_id) in

src/lib/type_check.ml

@@ -3985,21 +3985,13 @@ let check_mapcl env (MCL_aux (cl, (def_annot, _))) typ =
           let typed_right_mpexp = check_mpexp left_id_env env right_mpexp typ2 in
           MCL_aux (MCL_bidir (typed_left_mpexp, typed_right_mpexp), (def_annot, mk_expected_tannot env typ (Some typ)))
         end
-      | MCL_forwards (mpexp, exp) -> begin
-          let mpat, _, _ = destruct_mpexp mpexp in
-          ignore (check_pattern_duplicates env (pat_of_mpat mpat));
-          let _, mpat_env, _ = bind_mpat false Env.empty env mpat typ1 in
-          let typed_mpexp = check_mpexp Env.empty env mpexp typ1 in
-          let typed_exp = check_exp mpat_env exp typ2 in
-          MCL_aux (MCL_forwards (typed_mpexp, typed_exp), (def_annot, mk_expected_tannot env typ (Some typ)))
+      | MCL_forwards pexp -> begin
+          let typed_pexp = check_case env typ1 pexp typ2 in
+          MCL_aux (MCL_forwards typed_pexp, (def_annot, mk_expected_tannot env typ (Some typ)))
         end
-      | MCL_backwards (mpexp, exp) -> begin
-          let mpat, _, _ = destruct_mpexp mpexp in
-          ignore (check_pattern_duplicates env (pat_of_mpat mpat));
-          let _, mpat_env, _ = bind_mpat false Env.empty env mpat typ2 in
-          let typed_mpexp = check_mpexp Env.empty env mpexp typ2 in
-          let typed_exp = check_exp mpat_env exp typ1 in
-          MCL_aux (MCL_backwards (typed_mpexp, typed_exp), (def_annot, mk_expected_tannot env typ (Some typ)))
+      | MCL_backwards pexp -> begin
+          let typed_pexp = check_case env typ2 pexp typ1 in
+          MCL_aux (MCL_backwards typed_pexp, (def_annot, mk_expected_tannot env typ (Some typ)))
         end
     end
   | _ ->

src/sail_doc_backend/docinfo.ml

@@ -531,6 +531,9 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct
   let docinfo_for_mpexp (MPat_aux (aux, _)) =
     match aux with MPat_pat mpat -> pat_of_mpat mpat | MPat_when (mpat, _) -> pat_of_mpat mpat
 
+  let docinfo_for_pexp (Pat_aux (aux, _)) =
+    match aux with Pat_exp (pat, body) -> (pat, body) | Pat_when (pat, _, body) -> (pat, body)
+
   let docinfo_for_mapcl n (MCL_aux (aux, (def_annot, _)) as clause) =
     let source = doc_loc def_annot.loc Type_check.strip_mapcl Pretty_print_sail.doc_mapcl clause in
     let wavedrom_attr = find_attribute_opt "wavedrom" def_annot.attrs in
@@ -543,13 +546,13 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct
           let right = docinfo_for_mpexp right in
           let right_wavedrom = Wavedrom.of_pattern ~labels:wavedrom_attr right in
           (Some left, left_wavedrom, Some right, right_wavedrom, None)
-      | MCL_forwards (left, body) ->
-          let left = docinfo_for_mpexp left in
+      | MCL_forwards pexp ->
+          let left, body = docinfo_for_pexp pexp in
           let left_wavedrom = Wavedrom.of_pattern ~labels:wavedrom_attr left in
           let body = doc_loc (exp_loc body) Type_check.strip_exp Pretty_print_sail.doc_exp body in
           (Some left, left_wavedrom, None, None, Some body)
-      | MCL_backwards (right, body) ->
-          let right = docinfo_for_mpexp right in
+      | MCL_backwards pexp ->
+          let right, body = docinfo_for_pexp pexp in
           let right_wavedrom = Wavedrom.of_pattern ~labels:wavedrom_attr right in
           let body = doc_loc (exp_loc body) Type_check.strip_exp Pretty_print_sail.doc_exp body in
           (None, None, Some right, right_wavedrom, Some body)

test/typecheck/pass/wildcard_mapping.sail

@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+mapping Foo : bits(2) <-> int = {
+  0b00 <-> 10,
+  0b01 <-> 1,
+  forwards _ => 5,
+  backwards _ => 0b11
+}