Merge branch 'mappings' into sail2

1 files changed, 661 insertions, 1 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 0ea6ef79..b938d2d7 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -690,6 +690,7 @@ let remove_vector_concat_pat pat =
     ; p_tup            = (fun ps -> P_tup (List.map (fun p -> p false) ps))
     ; p_list           = (fun ps -> P_list (List.map (fun p -> p false) ps))
     ; p_cons           = (fun (p,ps) -> P_cons (p false, ps false))
+    ; p_string_append  = (fun (ps) -> P_string_append (List.map (fun p -> p false) ps))
     ; p_aux =
         (fun (pat,((l,_) as annot)) contained_in_p_as ->
           match pat with
@@ -710,10 +711,12 @@ let remove_vector_concat_pat pat =
     let p_vector_concat pats =
       let rec aux ((P_aux (p,((l,_) as a))) as pat) = match p with
         | P_vector _ -> P_aux (P_as (pat,fresh_id_v l),a)
+        | P_lit _ -> P_aux (P_as (pat, fresh_id_v l), a)
         | P_id id -> P_aux (P_id id,a)
         | P_as (p,id) -> P_aux (P_as (p,id),a)
         | P_typ (typ, pat) -> P_aux (P_typ (typ, aux pat),a)
         | P_wild -> P_aux (P_wild,a)
+        | P_app (id, pats) when Env.is_mapping id (env_of_annot a) -> P_aux (P_app (id, List.map aux pats), a)
         | _ ->
            raise
              (Reporting_basic.err_unreachable
@@ -804,6 +807,9 @@ let remove_vector_concat_pat pat =
                let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in
                (pos', pat_acc @ [P_aux (P_id cname,cannot)], decl_acc @ [((lb,decl),info)])
             | P_typ (typ, pat) -> aux (Some typ) (pos,pat_acc,decl_acc) (pat, is_last)
+            (* | P_app (cname, pats) if Env.is_mapping cname (en) ->
+             *    let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in
+             *    (pos', pat_acc @ [P_aux (P_app (cname,pats),cannot)], decl_acc @ [((lb,decl),info)]) *)
             (* normal vector patterns are fine *)
             | _ -> (pos', pat_acc @ [P_aux (p,cannot)],decl_acc)) in
           let pats_tagged = tag_last pats in
@@ -832,6 +838,8 @@ let remove_vector_concat_pat pat =
                                     (P_tup ps,List.flatten decls))
     ; p_list           = (fun ps -> let (ps,decls) = List.split ps in
                                     (P_list ps,List.flatten decls))
+    ; p_string_append  = (fun ps -> let (ps,decls) = List.split ps in
+                                    (P_string_append ps,List.flatten decls))
     ; p_cons           = (fun ((p,decls),(p',decls')) -> (P_cons (p,p'), decls @ decls'))
     ; p_aux            = (fun ((pat,decls),annot) -> p_aux ((pat,decls),annot))
     ; fP_aux           = (fun ((fpat,decls),annot) -> (FP_aux (fpat,annot),decls))
@@ -1086,6 +1094,8 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) =
   | P_tup pats -> rewrap (E_tuple (List.map pat_to_exp pats))
   | P_list pats -> rewrap (E_list (List.map pat_to_exp pats))
   | P_cons (p,ps) -> rewrap (E_cons (pat_to_exp p, pat_to_exp ps))
+  | P_string_append (ps) -> raise (Reporting_basic.err_unreachable l
+      "pat_to_exp not implemented for P_string_append")
 and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
   FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot))
 
@@ -1174,6 +1184,7 @@ let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
 | P_app (_,pats) | P_tup pats | P_list pats ->
     List.exists contains_bitvector_pat pats
 | P_cons (p,ps) -> contains_bitvector_pat p || contains_bitvector_pat ps
+| P_string_append (ps) -> List.exists contains_bitvector_pat ps
 | P_record (fpats,_) ->
     List.exists (fun (FP_aux (FP_Fpat (_,pat),_)) -> contains_bitvector_pat pat) fpats
 
@@ -1199,6 +1210,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     ; p_record = (fun (fpats,b) -> P_record (fpats, b))
     ; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
     ; p_vector_concat  = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
+    ; p_string_append  = (fun ps -> P_string_append (List.map (fun p -> p false) ps))
     ; p_tup            = (fun ps -> P_tup (List.map (fun p -> p false) ps))
     ; p_list           = (fun ps -> P_list (List.map (fun p -> p false) ps))
     ; p_cons           = (fun (p,ps) -> P_cons (p false, ps false))
@@ -1350,6 +1362,8 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
                                     (P_vector ps, flatten_guards_decls gdls))
     ; p_vector_concat  = (fun ps -> let (ps,gdls) = List.split ps in
                                     (P_vector_concat ps, flatten_guards_decls gdls))
+    ; p_string_append  = (fun ps -> let (ps,gdls) = List.split ps in
+                                    (P_string_append ps, flatten_guards_decls gdls))
     ; p_tup            = (fun ps -> let (ps,gdls) = List.split ps in
                                     (P_tup ps, flatten_guards_decls gdls))
     ; p_list           = (fun ps -> let (ps,gdls) = List.split ps in
@@ -1488,7 +1502,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
     | Pat_aux (Pat_exp (pat, body), annot) ->
       (pat, None, rewrite_rec body, annot)
     | Pat_aux (Pat_when (pat, guard, body), annot) ->
-      (pat, Some guard, rewrite_rec body, annot) in
+      (pat, Some (rewrite_rec guard), rewrite_rec body, annot) in
     let clauses = rewrite_guarded_clauses l (List.map clause ps) in
     if (effectful e) then
       let e = rewrite_rec e in
@@ -2803,12 +2817,436 @@ let rewrite_defs_internal_lets =
     ; rewrite_defs = rewrite_defs_base
     }
 
+
+let fold_guards guards =
+  match guards with
+  | [] -> (mk_exp (E_lit (mk_lit L_true)))
+  | g :: gs -> List.fold_left (fun g g' -> mk_exp (E_app (mk_id "and_bool", [strip_exp g; strip_exp g']))) g gs
+
+let fold_typed_guards env guards =
+  match guards with
+  | [] -> annot_exp (E_lit (mk_lit L_true)) Parse_ast.Unknown env bool_typ
+  | g :: gs -> List.fold_left (fun g g' -> annot_exp (E_app (mk_id "and_bool", [g; g'])) Parse_ast.Unknown env bool_typ) g gs
+
+
+let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot annot)) as pexp) =
+  let guards = ref [] in
+
+  match pexp_aux with
+  | Pat_exp (pat, exp) ->
+     begin
+       let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in
+       match !guards with
+       | [] -> pexp
+       | gs ->
+          let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in
+          check_case (pat_env_of pat) (pat_typ_of pat) unchecked_pexp (typ_of exp)
+     end
+  | Pat_when (pat, guard, exp) ->
+     begin
+       let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in
+       let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in
+       check_case (pat_env_of pat) (pat_typ_of pat) unchecked_pexp (typ_of exp)
+     end
+
+
+let pexp_rewriters rewrite_pexp =
+  let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in
+  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) }
+
+
+let stringappend_counter = ref 0
+
+let fresh_stringappend_id () =
+  let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in
+  stringappend_counter := !stringappend_counter + 1;
+  id
+
+let unk = Parse_ast.Unknown
+let unkt = (Parse_ast.Unknown, None)
+
+let construct_bool_match env (match_on : tannot exp) (pexp : tannot pexp) : tannot exp =
+  let true_exp = annot_exp (E_lit (mk_lit L_true)) unk env bool_typ in
+  let false_exp = annot_exp (E_lit (mk_lit L_false)) unk env bool_typ in
+    let true_pexp =
+      match pexp with
+      | Pat_aux (Pat_exp (pat, exp), annot) ->
+         Pat_aux (Pat_exp (pat, true_exp), unkt)
+      | Pat_aux (Pat_when (pat, guards, exp), annot) ->
+         Pat_aux (Pat_when (pat, guards, true_exp), unkt)
+    in
+    let false_pexp = Pat_aux (Pat_exp (annot_pat P_wild unk env (typ_of match_on), false_exp), unkt) in
+    annot_exp (E_case (match_on, [true_pexp; false_pexp])) unk env bool_typ
+
+
+let rec rewrite_defs_pat_string_append =
+  let rec rewrite_pat env ((pat : tannot pat), (guards : tannot exp list), (expr : tannot exp)) =
+    let guards_ref = ref guards in
+    let expr_ref = ref expr in
+    let folder p =
+      let p, g, e = rewrite_pat env (p, !guards_ref, !expr_ref) in
+      guards_ref := g;
+      expr_ref := e;
+      p
+    in
+    match pat with
+    (*
+        "lit" ^^ pat2 => expr ---> s# if startswith(s#, "lit")
+                                        && match str_drop(s#, strlen("lit")) {
+                                             pat2 => true, _ => false
+                                           }
+                                   => match str_drop(s#, strlen("lit")) {
+                                        pat2 => expr
+                                      }
+     *)
+    | P_aux (P_string_append (
+                 P_aux (P_lit (L_aux (L_string s, _) as lit), _)
+                 :: pats
+               ), psa_annot) ->
+
+       let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in
+       stringappend_counter := !stringappend_counter + 1;
+
+       (* construct drop expression -- string_drop(s#, strlen("lit")) *)
+       let drop_exp = annot_exp (E_app (mk_id "string_drop", [annot_exp (E_id id) unk env string_typ; annot_exp (E_app (mk_id "string_length", [annot_exp (E_lit lit) unk env string_typ])) unk env nat_typ])) unk env string_typ  in
+
+       (* recurse into pat2 *)
+       let new_pat2_pexp =
+         match rewrite_pat env (P_aux (P_string_append (pats), psa_annot), guards, expr) with
+         | pat, [], expr -> Pat_aux (Pat_exp (pat, expr), unkt)
+         | pat, gs, expr -> Pat_aux (Pat_when (pat, fold_typed_guards env gs, expr), unkt)
+       in
+
+       (* construct the two new guards *)
+       let guard1 = annot_exp (E_app (mk_id "string_startswith",
+                                      [annot_exp (E_id id) unk env string_typ;
+                                       annot_exp (E_lit lit) unk env string_typ]
+                      )) unk env bool_typ in
+       let guard2 = construct_bool_match env drop_exp new_pat2_pexp in
+
+       (* construct new match expr *)
+       let new_expr = annot_exp (E_case (drop_exp, [new_pat2_pexp])) unk env (typ_of expr) in
+
+       (* construct final result *)
+       annot_pat (P_id id) unk env string_typ, guard1 :: guard2 :: guards, new_expr
+
+    (*
+        (builtin x) ^^ pat2 => expr ---> s# if match maybe_atoi s# {
+                                                 Some (n#, len#) =>
+                                                   match string_drop(s#, len#) {
+                                                     pat2 => true, _ => false
+                                                   }
+                                                 None => false
+                                               }
+                                         => let (x, len#) = match maybe_int_of_prefix s# {
+                                                              Some (n#, len#) => (n#, len#)
+                                                            } in
+                                            match string_drop(s#, len#) {
+                                              pat2 => expr
+                                            }
+     *)
+
+    | P_aux (P_string_append (
+                 P_aux (P_app (mapping_id, arg_pats) , _)
+                 :: pats
+               ), psa_annot)
+         when Env.is_mapping mapping_id env ->
+
+       (* common things *)
+       let mapping_prefix_func =
+         match mapping_id with
+         | Id_aux (Id id, _)
+         | Id_aux (DeIid id, _) -> id ^ "_matches_prefix"
+       in
+       let mapping_inner_typ =
+         match Env.get_val_spec (mk_id mapping_prefix_func) env with
+         | (_, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [Typ_arg_aux (Typ_arg_typ typ, _)]), _), _), _)) -> typ
+         | _ -> typ_error Parse_ast.Unknown "mapping prefix func without correct function type?"
+       in
+
+       let s_id = fresh_stringappend_id () in
+       let n_id = fresh_stringappend_id () in
+       let len_id = fresh_stringappend_id () in
+
+       (* construct drop expression -- string_drop(s#, len#) *)
+       let drop_exp = annot_exp (E_app (mk_id "string_drop",
+                                        [annot_exp (E_id s_id) unk env string_typ;
+                                         annot_exp (E_id len_id) unk env nat_typ]))
+                        unk env string_typ in
+       (* construct func expression -- maybe_atoi s# *)
+       let func_exp = annot_exp (E_app (mk_id mapping_prefix_func,
+                                        [annot_exp (E_id s_id) unk env string_typ]))
+                        unk env mapping_inner_typ in
+       (* construct some pattern -- Some (n#, len#) *)
+       let opt_typ = app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [mapping_inner_typ; nat_typ]), unk)] in
+       let some_pat = annot_pat (P_app (mk_id "Some",
+                                        [annot_pat (P_id n_id) unk env mapping_inner_typ;
+                                         annot_pat (P_id len_id) unk env nat_typ]))
+                        unk env opt_typ in
+       (* construct None pattern *)
+       let none_pat = annot_pat (P_app (mk_id "None", [annot_pat (P_lit (mk_lit L_unit)) unk env unit_typ])) unk env opt_typ in
+
+       (* recurse into pat2 *)
+       let new_pat2_pexp =
+         match rewrite_pat env (P_aux (P_string_append (pats), psa_annot), guards, expr) with
+         | pat, [], expr -> Pat_aux (Pat_exp (pat, expr), unkt)
+         | pat, gs, expr -> Pat_aux (Pat_when (pat, fold_typed_guards env gs, expr), unkt)
+       in
+
+       (* construct the new guard *)
+       let guard_inner_match = construct_bool_match env drop_exp new_pat2_pexp in
+       let new_guard = annot_exp (E_case (func_exp, [
+                                     Pat_aux (Pat_exp (some_pat, guard_inner_match), unkt);
+                                     Pat_aux (Pat_exp (none_pat, annot_exp (E_lit (mk_lit (L_false))) unk env bool_typ), unkt)
+                         ])) unk env bool_typ in
+
+       (* construct the new match *)
+       let new_match = annot_exp (E_case (drop_exp, [new_pat2_pexp])) unk env (typ_of expr) in
+
+       (* construct the new let *)
+       let new_binding = annot_exp (E_cast (mapping_inner_typ,
+                                            annot_exp (E_case (func_exp, [
+                                                             Pat_aux (Pat_exp (some_pat,
+                                                                               annot_exp (E_tuple [
+                                                                                           annot_exp (E_id n_id) unk env mapping_inner_typ;
+                                                                                           annot_exp (E_id len_id) unk env nat_typ
+                                                                                 ]) unk env (tuple_typ [mapping_inner_typ; nat_typ])
+                                                                        ), unkt)
+                                              ])) unk env (tuple_typ [mapping_inner_typ; nat_typ])
+                           )) unk env mapping_inner_typ in
+       let new_letbind =
+         match arg_pats with
+         | [] -> assert false
+         | [arg_pat] -> annot_letbind
+                          (P_tup [arg_pat; annot_pat (P_id len_id) unk env nat_typ], new_binding)
+                          unk env (tuple_typ [pat_typ_of arg_pat; nat_typ])
+         | arg_pats -> annot_letbind
+                         (P_tup
+                            [annot_pat (P_tup arg_pats) unk env (tuple_typ (List.map pat_typ_of arg_pats));
+                             annot_pat (P_id len_id) unk env nat_typ],
+                          new_binding)
+                         unk env (tuple_typ [tuple_typ (List.map pat_typ_of arg_pats); nat_typ])
+       in
+       let new_let = annot_exp (E_let (new_letbind, new_match)) unk env (typ_of expr) in
+
+       (* construct final result *)
+       annot_pat (P_id s_id) unk env string_typ,
+       new_guard :: guards,
+       new_let
+
+    | P_aux (P_string_append [pat], _) ->
+       pat, guards, expr
+
+    | P_aux (P_string_append [], (l, _)) ->
+       annot_pat (P_lit (L_aux (L_string "", l))) l env string_typ, guards, expr
+
+    | P_aux (P_string_append _, _) ->
+       failwith ("encountered a variety of string append pattern that is not yet implemented: " ^ string_of_pat pat)
+
+    | P_aux (P_as (inner_pat, inner_id), p_annot) ->
+       let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
+       P_aux (P_as (inner_pat, inner_id), p_annot), guards, expr
+    | P_aux (P_typ (inner_typ, inner_pat), p_annot) ->
+       let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
+       P_aux (P_typ (inner_typ, inner_pat), p_annot), guards, expr
+    | P_aux (P_var (inner_pat, typ_pat), p_annot) ->
+       let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
+       P_aux (P_var (inner_pat, typ_pat), p_annot), guards, expr
+    | P_aux (P_record _, p_annot) ->
+       failwith "record patterns not yet implemented"
+    | P_aux (P_vector pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_vector pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_vector_concat pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_vector_concat pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_tup pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_tup pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_list pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_list pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_app (f, pats), p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_app (f, pats), p_annot), !guards_ref, !expr_ref
+    | P_aux (P_cons (pat1, pat2), p_annot) ->
+       let pat1, guards, expr = rewrite_pat env (pat1, guards, expr) in
+       let pat2, guards, expr = rewrite_pat env (pat2, guards, expr) in
+       P_aux (P_cons (pat1, pat2), p_annot), guards, expr
+    | P_aux (P_id _, _)
+    | P_aux (P_lit _, _)
+    | P_aux (P_wild, _) -> pat, guards, expr
+  in
+
+  let rec rewrite_pexp (Pat_aux (pexp_aux, pexp_annot) as pexp) =
+
+    (* merge cases of Pat_exp and Pat_when *)
+    let (P_aux (p_aux, p_annot) as pat, guards, expr) =
+      match pexp_aux with
+      | Pat_exp (pat, expr) -> (pat, [], expr)
+      | Pat_when (pat, guard, expr) -> (pat, [guard], expr)
+    in
+
+    let env = env_of_annot p_annot in
+
+    let (new_pat, new_guards, new_expr) =
+      rewrite_pat env (pat, guards, expr)
+    in
+
+    (* un-merge Pat_exp and Pat_when cases *)
+    let new_pexp = match new_guards with
+    | [] -> Pat_aux (Pat_exp (new_pat, new_expr), pexp_annot)
+    | gs -> Pat_aux (Pat_when (new_pat, fold_typed_guards env gs, new_expr), pexp_annot)
+    in
+    new_pexp
+
+  in
+  pexp_rewriters rewrite_pexp
+
+
+let mappingpatterns_counter = ref 0
+
+let fresh_mappingpatterns_id () =
+  let id = mk_id ("_mappingpatterns_" ^ (string_of_int !mappingpatterns_counter) ^ "#") in
+  mappingpatterns_counter := !mappingpatterns_counter + 1;
+  id
+
+let rewrite_defs_mapping_patterns =
+  let rec rewrite_pat env (pat, guards, expr) =
+    let guards_ref = ref guards in
+    let expr_ref = ref expr in
+    let folder p =
+      let p, g, e = rewrite_pat env (p, !guards_ref, !expr_ref) in
+      guards_ref := g;
+      expr_ref := e;
+      p
+    in
+    let env = pat_env_of pat in
+    match pat with
+      (*
+          mapping(args) => expr ----> s# if mapping_matches(s#) => let args = mapping(s#) in expr
+
+          (plus 'infer the mapping type' shenanigans)
+       *)
+    | P_aux (P_app (mapping_id, arg_pats), p_annot) when Env.is_mapping mapping_id env ->
+
+       let mapping_in_typ = typ_of_annot p_annot in
+
+       let x = Env.get_val_spec mapping_id env in
+       let (_, Typ_aux(Typ_bidir(typ1, typ2), _)) = x in
+
+       let mapping_direction =
+         if mapping_in_typ = typ1 then
+           "forwards"
+         else
+           "backwards"
+       in
+
+       let mapping_out_typ =
+         if mapping_in_typ = typ2 then
+           typ2
+         else
+           typ1
+       in
+
+       let mapping_name =
+         match mapping_id with
+         | Id_aux (Id id, _)
+         | Id_aux (DeIid id, _) -> id
+       in
+
+       let mapping_matches_id = mk_id (mapping_name ^ "_" ^ mapping_direction ^ "_matches") in
+       let mapping_perform_id = mk_id (mapping_name ^ "_" ^ mapping_direction) in
+       let s_id = fresh_mappingpatterns_id () in
+
+       let s_exp = annot_exp (E_id s_id) unk env mapping_in_typ in
+       let new_guard = annot_exp (E_app (mapping_matches_id, [s_exp])) unk env bool_typ in
+       let new_binding = annot_exp (E_app (mapping_perform_id, [s_exp])) unk env typ2 in
+       let new_letbind = match arg_pats with
+         | [] -> assert false
+         | [arg_pat] -> LB_aux (LB_val (arg_pat, new_binding), unkt)
+         | arg_pats ->
+            let checked_tup = annot_pat (P_tup arg_pats) unk env mapping_out_typ in
+            LB_aux (LB_val (checked_tup, new_binding), unkt)
+       in
+
+       let new_let = annot_exp (E_let (new_letbind, expr)) unk env (typ_of expr) in
+
+       annot_pat (P_id s_id) unk env mapping_in_typ, new_guard :: guards, new_let
+
+    | P_aux (P_as (inner_pat, inner_id), p_annot) ->
+       let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
+       P_aux (P_as (inner_pat, inner_id), p_annot), guards, expr
+    | P_aux (P_typ (inner_typ, inner_pat), p_annot) ->
+       let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
+       P_aux (P_typ (inner_typ, inner_pat), p_annot), guards, expr
+    | P_aux (P_var (inner_pat, typ_pat), p_annot) ->
+       let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
+       P_aux (P_var (inner_pat, typ_pat), p_annot), guards, expr
+    | P_aux (P_record _, p_annot) ->
+       failwith "record patterns not yet implemented"
+    | P_aux (P_vector pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_vector pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_vector_concat pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_vector_concat pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_tup pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_tup pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_list pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_list pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_app (f, pats), p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_app (f, pats), p_annot), !guards_ref, !expr_ref
+    | P_aux (P_string_append pats, p_annot) ->
+       let pats = List.map folder pats in
+       P_aux (P_string_append pats, p_annot), !guards_ref, !expr_ref
+    | P_aux (P_cons (pat1, pat2), p_annot) ->
+       let pat1, guards, expr = rewrite_pat env (pat1, guards, expr) in
+       let pat2, guards, expr = rewrite_pat env (pat2, guards, expr) in
+       P_aux (P_cons (pat1, pat2), p_annot), guards, expr
+    | P_aux (P_id _, _)
+    | P_aux (P_lit _, _)
+    | P_aux (P_wild, _) -> pat, guards, expr
+  in
+
+  let rec rewrite_pexp (Pat_aux (pexp_aux, pexp_annot) as pexp) =
+
+    (* merge cases of Pat_exp and Pat_when *)
+    let (P_aux (p_aux, p_annot) as pat, guards, expr) =
+      match pexp_aux with
+      | Pat_exp (pat, expr) -> (pat, [], expr)
+      | Pat_when (pat, guard, expr) -> (pat, [guard], expr)
+    in
+
+    let env = env_of_annot p_annot in
+
+    let (new_pat, new_guards, new_expr) =
+      rewrite_pat env (pat, guards, expr)
+    in
+
+    (* un-merge Pat_exp and Pat_when cases *)
+    let new_pexp = match new_guards with
+    | [] -> Pat_aux (Pat_exp (new_pat, new_expr), pexp_annot)
+    | gs -> Pat_aux (Pat_when (new_pat, fold_typed_guards env gs, new_expr), pexp_annot)
+    in
+    typ_debug (lazy (Printf.sprintf "rewritten pexp: %s\n%!" (Pretty_print_sail.doc_pexp new_pexp |> Pretty_print_sail.to_string)));
+    new_pexp
+
+  in
+  pexp_rewriters rewrite_pexp
+
+
 let rewrite_defs_pat_lits =
   let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) =
     let guards = ref [] in
     let counter = ref 0 in
 
     let rewrite_pat = function
+      (* HACK: ignore strings for now *)
+      | P_lit (L_aux (L_string _, _)) as p_aux, p_annot -> P_aux (p_aux, p_annot)
       | P_lit lit, p_annot ->
          let env = env_of_annot p_annot in
          let typ = typ_of_annot p_annot in
@@ -3260,9 +3698,222 @@ let merge_funcls (Defs defs) =
     | d -> d
   in Defs (List.map merge_in_def defs)
 
+
+let rec exp_of_mpat (MP_aux (mpat, annot)) =
+  let empty_vec = E_aux (E_vector [], annot) in
+  let concat_vectors annot vec1 vec2 = (* TODO FIXME, this should be OK for typing but doesn't attach location information properly *)
+    E_aux (E_vector_append (vec1, vec2), annot)
+  in
+  let empty_string = E_aux (E_lit (L_aux (L_string "", Parse_ast.Unknown)), annot) in
+  let string_append annot str1 str2 =
+    E_aux (E_app (mk_id "string_append", [str1; str2]), annot)
+  in
+  match mpat with
+  | MP_lit lit                      -> E_aux (E_lit lit, annot)
+  | MP_id id                        -> E_aux (E_id id, annot)
+  | MP_app (id, args)               -> E_aux (E_app (id, (List.map exp_of_mpat args)), annot)
+  | MP_record (mfpats, flag)        -> E_aux (E_record (fexps_of_mfpats mfpats flag annot), annot)
+  | MP_vector mpats                 -> E_aux (E_vector (List.map exp_of_mpat mpats), annot)
+  | MP_vector_concat mpats          -> List.fold_right (concat_vectors annot) (List.map exp_of_mpat mpats) empty_vec
+  | MP_tup mpats                    -> E_aux (E_tuple (List.map exp_of_mpat mpats), annot)
+  | MP_list mpats                   -> E_aux (E_list (List.map exp_of_mpat mpats), annot)
+  | MP_cons (mpat1, mpat2)          -> E_aux (E_cons (exp_of_mpat mpat1, exp_of_mpat mpat2), annot)
+  | MP_string_append mpats          -> List.fold_right (string_append annot) (List.map exp_of_mpat mpats) empty_string
+  | MP_typ (mpat, typ)              -> E_aux (E_cast (typ, exp_of_mpat mpat), annot)
+
+and fexps_of_mfpats mfpats flag annot =
+  let fexp_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) =
+    FE_aux (FE_Fexp (id, exp_of_mpat mpat), annot)
+  in
+  FES_aux (FES_Fexps (List.map fexp_of_mfpat mfpats, flag), annot)
+
+let rec pat_of_mpat (MP_aux (mpat, annot)) =
+  match mpat with
+  | MP_lit lit                      -> P_aux (P_lit lit, annot)
+  | MP_id id                        -> P_aux (P_id id, annot)
+  | MP_app (id, args)               -> P_aux (P_app (id, (List.map pat_of_mpat args)), annot)
+  | MP_record (mfpats, flag)        -> P_aux (P_record ((fpats_of_mfpats mfpats), flag), annot)
+  | MP_vector mpats                 -> P_aux (P_vector (List.map pat_of_mpat mpats), annot)
+  | MP_vector_concat mpats          -> P_aux (P_vector_concat (List.map pat_of_mpat mpats), annot)
+  | MP_tup mpats                    -> P_aux (P_tup (List.map pat_of_mpat mpats), annot)
+  | MP_list mpats                   -> P_aux (P_list (List.map pat_of_mpat mpats), annot)
+  | MP_cons (mpat1, mpat2)          -> P_aux ((P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2), annot))
+  | MP_string_append (mpats)        -> P_aux ((P_string_append (List.map pat_of_mpat mpats), annot))
+  | MP_typ (mpat, typ)              -> P_aux (P_typ (typ, pat_of_mpat mpat), annot)
+
+and fpats_of_mfpats mfpats =
+  let fpat_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) =
+    FP_aux (FP_Fpat (id, pat_of_mpat mpat), annot)
+  in
+  List.map fpat_of_mfpat mfpats
+
+let rewrite_defs_realise_mappings (Defs defs) =
+  let realise_mpexps forwards mpexp1 mpexp2 =
+    let mpexp_pat, mpexp_exp =
+      if forwards then mpexp1, mpexp2
+      else mpexp2, mpexp1
+    in
+    let exp =
+      match mpexp_exp with
+      | MPat_aux ((MPat_pat mpat), _) -> exp_of_mpat mpat
+      | MPat_aux ((MPat_when (mpat, _), _)) -> exp_of_mpat mpat
+    in
+    match mpexp_pat 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)
+  in
+  let realise_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) =
+    realise_mpexps forwards mpexp1 mpexp2
+  in
+  let realise_bool_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) =
+    let mpexp = if forwards then mpexp1 else mpexp2 in
+    realise_mpexps true mpexp (mk_mpexp (MPat_pat (mk_mpat (MP_lit (mk_lit L_true)))))
+  in
+  let arg_id = mk_id "arg#" in
+  let arg_exp = (mk_exp (E_id arg_id)) in
+  let arg_pat = mk_pat (P_id arg_id) in
+  let placeholder_id = mk_id "s#" in
+  let append_placeholder = function
+    | MPat_aux (MPat_pat (MP_aux (MP_string_append mpats, p_annot)), aux_annot) ->
+       MPat_aux (MPat_pat (MP_aux (MP_string_append (mpats @ [mk_mpat (MP_id placeholder_id)]), p_annot)), aux_annot)
+    | MPat_aux (MPat_when (MP_aux (MP_string_append mpats, p_annot), guard), aux_annot) ->
+       MPat_aux (MPat_when (MP_aux (MP_string_append (mpats @ [mk_mpat (MP_id placeholder_id)]), p_annot), guard), aux_annot)
+    | MPat_aux (MPat_pat mpat, aux_annot) ->
+       MPat_aux (MPat_pat (mk_mpat (MP_string_append [mpat; mk_mpat (MP_id placeholder_id)])), aux_annot)
+    | MPat_aux (MPat_when (mpat, guard), aux_annot) ->
+       MPat_aux (MPat_when (mk_mpat (MP_string_append [mpat; mk_mpat (MP_id placeholder_id)]), guard), aux_annot)
+  in
+  let realise_prefix_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) =
+    let mpexp = if forwards then mpexp1 else mpexp2 in
+    let other = if forwards then mpexp2 else mpexp1 in
+    let strlen = (
+        mk_mpat (MP_app ( mk_id "sub_nat",
+                     [
+                       mk_mpat (MP_app ( mk_id "string_length" , [mk_mpat (MP_id arg_id        )]));
+                       mk_mpat (MP_app ( mk_id "string_length" , [mk_mpat (MP_id placeholder_id)]));
+                     ]
+          ))
+      ) in
+    match other with
+    | MPat_aux (MPat_pat mpat2, _)
+      | MPat_aux (MPat_when (mpat2, _), _)->
+       realise_mpexps true (append_placeholder mpexp) (mk_mpexp (MPat_pat (mk_mpat (MP_app ((mk_id "Some"), [ mk_mpat (MP_tup [mpat2; strlen]) ])))))
+  in
+  let realise_mapdef (MD_aux (MD_mapping (id, _, mapcls), ((l, (tannot:tannot)) as annot))) =
+    let forwards_id = mk_id (string_of_id id ^ "_forwards") in
+    let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in
+    let backwards_id = mk_id (string_of_id id ^ "_backwards") in
+    let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
+
+    let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
+    let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in
+    let env = match mapcls with
+      | MCL_aux (_, mapcl_annot) :: _ -> env_of_annot mapcl_annot
+      | _ -> Type_check.typ_error l "mapping with no clauses?"
+    in
+    let (typq, bidir_typ) = Env.get_val_spec id env in
+    let (typ1, typ2, l) = match bidir_typ with
+      | Typ_aux (Typ_bidir (typ1, typ2), l) -> typ1, typ2, l
+      | _ -> Type_check.typ_error l "non-bidir type of mapping?"
+    in
+    let forwards_typ = Typ_aux (Typ_fn (typ1, typ2, no_effect), l) in
+    let forwards_matches_typ = Typ_aux (Typ_fn (typ1, bool_typ, no_effect), l) in
+    let backwards_typ = Typ_aux (Typ_fn (typ2, typ1, no_effect), l) in
+    let backwards_matches_typ = Typ_aux (Typ_fn (typ2, bool_typ, no_effect), l) in
+
+    let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+    let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+    let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+    let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+
+    let forwards_spec, env = Type_check.check_val_spec env forwards_spec in
+    let backwards_spec, env = Type_check.check_val_spec env backwards_spec in
+    let forwards_matches_spec, env = Type_check.check_val_spec env forwards_matches_spec in
+    let backwards_matches_spec, env = Type_check.check_val_spec env backwards_matches_spec in
+
+    let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
+    let forwards_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl true forwards_id) mapcls))) in
+    let backwards_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl false backwards_id) mapcls))) in
+
+    let wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_lit (mk_lit L_false)))) in
+    let forwards_matches_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl true forwards_matches_id) mapcls) @ [wildcard])) in
+    let backwards_matches_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl false backwards_matches_id) mapcls) @ [wildcard])) in
+
+    let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in
+    let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in
+    let forwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_matches_id arg_pat forwards_matches_match]), (l, ()))) in
+    let backwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_matches_id arg_pat backwards_matches_match]), (l, ()))) in
+
+    typ_debug (lazy (Printf.sprintf "forwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_fun |> Pretty_print_sail.to_string)));
+    typ_debug (lazy (Printf.sprintf "backwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_fun |> Pretty_print_sail.to_string)));
+    typ_debug (lazy (Printf.sprintf "forwards matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_matches_fun |> Pretty_print_sail.to_string)));
+    typ_debug (lazy (Printf.sprintf "backwards matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_matches_fun |> Pretty_print_sail.to_string)));
+    let forwards_fun, _ = Type_check.check_fundef env forwards_fun in
+    let backwards_fun, _ = Type_check.check_fundef env backwards_fun in
+    let forwards_matches_fun, _ = Type_check.check_fundef env forwards_matches_fun in
+    let backwards_matches_fun, _ = Type_check.check_fundef env backwards_matches_fun in
+
+    let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in
+    let prefix_wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_exp (E_lit (mk_lit L_unit))])))) in
+    let string_defs =
+      begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then
+              let forwards_prefix_typ = Typ_aux (Typ_fn (typ1, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+              let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+              let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
+              let forwards_prefix_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) @ [prefix_wildcard])) in
+              let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
+              typ_debug (lazy (Printf.sprintf "forwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_prefix_fun |> Pretty_print_sail.to_string)));
+              let forwards_prefix_fun, _ = Type_check.check_fundef env forwards_prefix_fun in
+              forwards_prefix_spec @ forwards_prefix_fun
+            else
+              if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then
+                let backwards_prefix_typ = Typ_aux (Typ_fn (typ2, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+                let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
+                let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
+                let backwards_prefix_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) @ [prefix_wildcard])) in
+                let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
+                typ_debug (lazy (Printf.sprintf "backwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_prefix_fun |> Pretty_print_sail.to_string)));
+                let backwards_prefix_fun, _ = Type_check.check_fundef env backwards_prefix_fun in
+                backwards_prefix_spec @ backwards_prefix_fun
+              else
+                []
+      end
+    in
+
+      forwards_spec
+    @ forwards_fun
+    @ backwards_spec
+    @ backwards_fun
+    @ forwards_matches_spec
+    @ forwards_matches_fun
+    @ backwards_matches_spec
+    @ backwards_matches_fun
+    @ string_defs
+  in
+  let rewrite_def def =
+    match def with
+    | DEF_mapdef mdef -> realise_mapdef mdef
+    | d -> [d]
+  in
+  Defs (List.map rewrite_def defs |> List.flatten)
+
 let recheck_defs defs = fst (Type_error.check initial_env defs)
 
+let remove_mapping_valspecs (Defs defs) =
+  let allowed_def def =
+    match def with
+    | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (_, Typ_aux (Typ_bidir _, _)), _), _, _, _), _)) -> false
+    | _ -> true
+  in
+  Defs (List.filter allowed_def defs)
+
+
 let rewrite_defs_lem = [
+  ("realise_mappings", rewrite_defs_realise_mappings);
+  ("remove_mapping_valspecs", remove_mapping_valspecs);
+  ("pat_string_append", rewrite_defs_pat_string_append);
+  ("mapping_builtins", rewrite_defs_mapping_patterns);
+  ("pat_lits", rewrite_defs_pat_lits);
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
@@ -3297,6 +3948,9 @@ let rewrite_defs_lem = [
 let rewrite_defs_ocaml = [
     (* ("undefined", rewrite_undefined); *)
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+  ("realise_mappings", rewrite_defs_realise_mappings);
+  ("pat_string_append", rewrite_defs_pat_string_append);
+  ("mapping_builtins", rewrite_defs_mapping_patterns);
   ("pat_lits", rewrite_defs_pat_lits);
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
@@ -3316,6 +3970,9 @@ let rewrite_defs_ocaml = [
 
 let rewrite_defs_c = [
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+  ("realise_mappings", rewrite_defs_realise_mappings);
+  ("pat_string_append", rewrite_defs_pat_string_append);
+  ("mapping_builtins", rewrite_defs_mapping_patterns);
   ("pat_lits", rewrite_defs_pat_lits);
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
@@ -3333,6 +3990,9 @@ let rewrite_defs_c = [
 
 let rewrite_defs_interpreter = [
     ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+    ("realise_mappings", rewrite_defs_realise_mappings);
+    ("pat_string_append", rewrite_defs_pat_string_append);
+    ("mapping_builtins", rewrite_defs_mapping_patterns);
     ("vector_concat_assignments", rewrite_vector_concat_assignments);
     ("tuple_assignments", rewrite_tuple_assignments);
     ("simple_assignments", rewrite_simple_assignments);