Merge branch 'sail2' of github.com:rems-project/sail into sail2

1 files changed, 84 insertions, 68 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 5a903a40..5ed174ea 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -83,11 +83,11 @@ let get_loc_exp (E_aux (_,(l,_))) = l
 
 let gen_vs (id, spec) = Initial_check.extern_of_string dec_ord (mk_id id) spec
 
-let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Some (env, typ, effect)))
+let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, mk_tannot env typ effect))
 let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect
-let annot_pat p_aux l env typ = P_aux (p_aux, (l, Some (env, typ, no_effect)))
+let annot_pat p_aux l env typ = P_aux (p_aux, (l, mk_tannot env typ no_effect))
 let annot_letbind (p_aux, exp) l env typ =
-  LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, Some (env, typ, effect_of exp)))
+  LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, mk_tannot env typ (effect_of exp)))
 
 let simple_num l n = E_aux (
   E_lit (L_aux (L_num n, gen_loc l)),
@@ -141,7 +141,7 @@ let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
   | LEXP_vector_range (lexp,_,_)
   | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env
 
-let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
+let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match destruct_tannot annot with
   | Some (_, _, eff) -> effectful_effs eff
   | _ -> false
 
@@ -238,18 +238,22 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
        Typ_arg_aux (Typ_arg_order ord, l)
   in
 
-  let rewrite_annot = function
-    | (l, Some (env, typ, eff)) -> (l, Some (env, rewrite_typ env typ, eff))
-    | (l, None) -> (l, None)
+  let rewrite_annot (l, tannot) =
+    match destruct_tannot tannot with
+    | Some (env, typ, eff) -> l, replace_typ (rewrite_typ env typ) tannot
+    | None -> l, empty_tannot
   in
 
   let rewrite_def rewriters = function
-    | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, Some (env, typ, eff)))) ->
+    | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, tannot))) when not (is_empty_tannot tannot) ->
+       let env = env_of_annot (l, tannot) in
+       let typ = typ_of_annot (l, tannot) in
+       let eff = effect_of_annot tannot in
        let typschm = match typschm with
          | TypSchm_aux (TypSchm_ts (tq, typ), l) ->
             TypSchm_aux (TypSchm_ts (tq, rewrite_typ env typ), l)
        in
-       let a = rewrite_annot (l, Some (env, typ, eff)) in
+       let a = rewrite_annot (l, mk_tannot env typ eff) in
        DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a))
     | d -> Rewriter.rewrite_def rewriters d
   in
@@ -262,8 +266,11 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
 
 let rewrite_bitvector_exps defs =
   let e_aux = function
-    | (E_vector es, ((l, Some (env, typ, eff)) as a)) when is_bitvector_typ typ ->
-       begin
+    | (E_vector es, ((l, tannot) as a)) when not (is_empty_tannot tannot) ->
+       let env = env_of_annot (l, tannot) in
+       let typ = typ_of_annot (l, tannot) in
+       let eff = effect_of_annot tannot in
+       if is_bitvector_typ typ then
          try
            let len = mk_lit_exp (L_num (Big_int.of_int (List.length es))) in
            let es = mk_exp (E_list (List.map strip_exp es)) in
@@ -271,7 +278,8 @@ let rewrite_bitvector_exps defs =
            check_exp env exp typ
          with
          | _ -> E_aux (E_vector es, a)
-       end
+       else
+         E_aux (E_vector es, a)
     | (e_aux, a) -> E_aux (e_aux, a)
   in
   let rewrite_exp _ = fold_exp { id_exp_alg with e_aux = e_aux } in
@@ -285,7 +293,7 @@ let rewrite_bitvector_exps defs =
    variables in scope. *)
 let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
   let extract_typ_var l env nexp (id, (_, typ)) =
-    let var = E_aux (E_id id, (l, Some (env, typ, no_effect))) in
+    let var = E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
     match destruct_atom_nexp env typ with
     | Some size when prove env (nc_eq size nexp) -> Some var
     (* AA: This next case is a bit of a hack... is there a more
@@ -294,12 +302,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
        scope. *)
     | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) ->
        let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in
-       Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect))))
+       Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, mk_tannot env (atom_typ (nsum size (nint 1))) no_effect)))
     | _ ->
        begin
          match destruct_vector env typ with
          | Some (len, _, _) when prove env (nc_eq len nexp) ->
-            Some (E_aux (E_app (mk_id "length", [var]), (l, Some (env, atom_typ len, no_effect))))
+            Some (E_aux (E_app (mk_id "length", [var]), (l, mk_tannot env (atom_typ len) no_effect)))
          | _ -> None
        end
   in
@@ -318,12 +326,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
     let env = env_of orig_exp in
     match e_aux with
     | E_sizeof (Nexp_aux (Nexp_constant c, _) as nexp) ->
-       E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect)))
+       E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect))
     | E_sizeof nexp ->
        begin
          match nexp_simp (rewrite_nexp_ids (env_of orig_exp) nexp) with
          | Nexp_aux (Nexp_constant c, _) ->
-            E_aux (E_lit (L_aux (L_num c, l)), (l, Some (env, atom_typ nexp, no_effect)))
+            E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect))
          | _ ->
             let locals = Env.get_locals env in
             let exps = Bindings.bindings locals
@@ -428,7 +436,7 @@ let rewrite_sizeof (Defs defs) =
              let uvar = try Some (KBindings.find (orig_kid kid) inst) with Not_found -> None in
              match uvar with
              | Some (U_nexp nexp) ->
-                let sizeof = E_aux (E_sizeof nexp, (l, Some (env, atom_typ nexp, no_effect))) in
+                let sizeof = E_aux (E_sizeof nexp, (l, mk_tannot env (atom_typ nexp) no_effect)) in
                 (try rewrite_trivial_sizeof_exp sizeof with
                 | Type_error (l, err) ->
                   raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)))
@@ -554,11 +562,11 @@ let rewrite_sizeof (Defs defs) =
              let ptyp' = Typ_aux (Typ_tup (kid_typs @ typs), l) in
              (match pat with
               | P_tup pats ->
-                 P_aux (P_tup (kid_pats @ pats), (l, Some (penv, ptyp', peff)))
-              | P_wild -> P_aux (pat, (l, Some (penv, ptyp', peff)))
+                 P_aux (P_tup (kid_pats @ pats), (l, mk_tannot penv ptyp' peff))
+              | P_wild -> P_aux (pat, (l, mk_tannot penv ptyp' peff))
               | P_typ (Typ_aux (Typ_tup typs, l), pat) ->
                  P_aux (P_typ (Typ_aux (Typ_tup (kid_typs @ typs), l),
-                               rewrite_pat pat), (l, Some (penv, ptyp', peff)))
+                               rewrite_pat pat), (l, mk_tannot penv ptyp' peff))
               | P_as (_, id) | P_id id ->
                  (* adding parameters here would change the type of id;
               we should remove the P_as/P_id here and add a let-binding to the body *)
@@ -569,7 +577,7 @@ let rewrite_sizeof (Defs defs) =
                                                         "unexpected pattern while rewriting function parameters for sizeof expressions"))
           | ptyp ->
              let ptyp' = Typ_aux (Typ_tup (kid_typs @ [ptyp]), l) in
-             P_aux (P_tup (kid_pats @ [paux]), (l, Some (penv, ptyp', peff))) in
+             P_aux (P_tup (kid_pats @ [paux]), (l, mk_tannot penv ptyp' peff)) in
       let pat,guard,exp,pannot = destruct_pexp pexp in
       let pat' = rewrite_pat pat in
       let guard' = match guard with
@@ -907,7 +915,7 @@ let remove_vector_concat_pat pat =
         let typ = Env.base_typ_of env (typ_of_annot annot) in
         let eff = effect_of_annot (snd annot) in
         let (l,_) = annot in
-        let wild _ = P_aux (P_wild,(gen_loc l, Some (env, bit_typ, eff))) in
+        let wild _ = P_aux (P_wild,(gen_loc l, mk_tannot env bit_typ eff)) in
         if is_vector_typ typ then
           match p, vector_typ_args_of typ with
           | P_vector ps,_ -> acc @ ps
@@ -1136,7 +1144,7 @@ let subst_id_pat pat (id1,id2) =
   fold_pat {id_pat_alg with p_id = p_id} pat
 
 let subst_id_exp exp (id1,id2) =
-  Ast_util.subst (Id_aux (id1,Parse_ast.Unknown)) (E_aux (E_id (Id_aux (id2,Parse_ast.Unknown)),(Parse_ast.Unknown,None))) exp
+  Ast_util.subst (Id_aux (id1,Parse_ast.Unknown)) (E_aux (E_id (Id_aux (id2,Parse_ast.Unknown)),(Parse_ast.Unknown,empty_tannot))) exp
 
 let rec pat_to_exp (P_aux (pat,(l,annot))) =
   let rewrap e = E_aux (e,(l,annot)) in
@@ -1370,7 +1378,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     let rannot = simple_annot l typ in
     let elem = access_bit_exp rootid l typ idx in
     let e = annot_pat (P_id id) l env bit_typ in
-    let letbind = LB_aux (LB_val (e,elem), (l, Some (env, bit_typ, no_effect))) in
+    let letbind = LB_aux (LB_val (e,elem), (l, mk_tannot env bit_typ no_effect)) in
     let letexp = (fun body ->
       let (E_aux (_,(_,bannot))) = body in
       if IdSet.mem id (find_used_vars body)
@@ -1614,7 +1622,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
     if (effectful e) then
       let e = rewrite_rec e in
       let (E_aux (_,(el,eannot))) = e in
-      let pat_e' = fresh_id_pat "p__" (el, Some (env_of e, typ_of e, no_effect)) in
+      let pat_e' = fresh_id_pat "p__" (el, mk_tannot (env_of e) (typ_of e) no_effect) in
       let exp_e' = pat_to_exp pat_e' in
       let letbind_e = LB_aux (LB_val (pat_e',e), (el,eannot)) in
       let exp' = case_exp exp_e' (typ_of full_exp) clauses in
@@ -1631,7 +1639,7 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd
          (pat,guard,exp,annot) in
        let cs = rewrite_guarded_clauses l (List.map clause funcls) in
        List.map (fun (pat,exp,annot) ->
-         FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,None))),annot)) cs
+         FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,empty_tannot))),annot)) cs
      | _ -> funcls (* TODO is the empty list possible here? *) in
    FD_aux (FD_function(r,t,e,funcls),(l,fdannot))
 
@@ -1681,14 +1689,15 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
   | E_block exps ->
     let rec walker exps = match exps with
       | [] -> []
-      | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps
-        when lexp_is_local_intro le env && not (lexp_is_effectful le) ->
-        let (le', re') = rewrite_lexp_to_rhs le in
-        let e' = re' (rewrite_base e) in
-        let exps' = walker exps in
-        let effects = union_eff_exps exps' in
-        let block = E_aux (E_block exps', (l, Some (env, unit_typ, effects))) in
-        [fix_eff_exp (E_aux (E_var(le', e', block), annot))]
+      | (E_aux(E_assign(le,e), (l, tannot)) as exp)::exps
+           when not (is_empty_tannot tannot) && lexp_is_local_intro le (env_of_annot (l, tannot)) && not (lexp_is_effectful le) ->
+         let env = env_of_annot (l, tannot) in
+         let (le', re') = rewrite_lexp_to_rhs le in
+         let e' = re' (rewrite_base e) in
+         let exps' = walker exps in
+         let effects = union_eff_exps exps' in
+         let block = E_aux (E_block exps', (l, mk_tannot env unit_typ effects)) in
+         [fix_eff_exp (E_aux (E_var(le', e', block), annot))]
       (*| ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps ->
         let vars_t = introduced_variables t in
         let vars_e = introduced_variables e in
@@ -1919,7 +1928,7 @@ let rewrite_defs_early_return (Defs defs) =
     let annot = match List.map get_return_pexp pes with
     | Pat_aux (Pat_exp (_, E_aux (_, annot)), _) :: _ -> annot
     | Pat_aux (Pat_when (_, _, E_aux (_, annot)), _) :: _ -> annot
-    | [] -> (Parse_ast.Unknown, None) in
+    | [] -> (Parse_ast.Unknown, empty_tannot) in
     if List.for_all is_return_pexp pes
     then E_return (E_aux (E_case (e, List.map get_return_pexp pes), annot))
     else E_case (e, pes) in
@@ -1945,12 +1954,15 @@ let rewrite_defs_early_return (Defs defs) =
     let full_exp = propagate_exp_effect (E_aux (exp, (l, annot))) in
     let env = env_of full_exp in
     match full_exp with
-    | E_aux (E_return exp, (l, Some (env, typ, eff))) ->
+    | E_aux (E_return exp, (l, tannot)) when not (is_empty_tannot tannot) ->
       (* Add escape effect annotation, since we use the exception mechanism
          of the state monad to implement early return in the Lem backend *)
-      let annot' = Some (env, typ, union_effects eff (mk_effect [BE_escape])) in
-      let exp' = add_e_cast (typ_of exp) exp in
-      E_aux (E_app (mk_id "early_return", [exp']), (l, annot'))
+       let typ = typ_of_annot (l, tannot) in
+       let env = env_of_annot (l, tannot) in
+       let eff = effect_of_annot tannot in
+       let tannot' = mk_tannot env typ (union_effects eff (mk_effect [BE_escape])) in
+       let exp' = add_e_cast (typ_of exp) exp in
+       E_aux (E_app (mk_id "early_return", [exp']), (l, tannot'))
     | _ -> full_exp in
 
   (* Make sure that all final leaves of an expression (e.g. all branches of
@@ -1998,10 +2010,10 @@ let rewrite_defs_early_return (Defs defs) =
           (if is_return exp' then get_return exp' else exp)
       else exp
     in
-    let a = match a with
-    | (l, Some (env, typ, eff)) ->
-      (l, Some (env, typ, union_effects eff (effect_of exp)))
-    | _ -> a in
+    let a = match destruct_tannot (snd a) with
+      | Some (env, typ, eff) ->
+         (fst a, mk_tannot env typ (union_effects eff (effect_of exp)))
+      | _ -> a in
     FCL_aux (FCL_Funcl (id, construct_pexp (pat, guard, exp, pannot)), a) in
 
   let rewrite_fun_early_return rewriters
@@ -2016,14 +2028,14 @@ let rewrite_defs_early_return (Defs defs) =
     { rewriters_base with rewrite_fun = rewrite_fun_early_return }
     (Defs (early_ret_spec @ defs))
 
-let swaptyp typ (l,tannot) = match tannot with
-  | Some (env, typ', eff) -> (l, Some (env, typ, eff))
+let swaptyp typ (l,tannot) = match destruct_tannot tannot with
+  | Some (env, typ', eff) -> (l, mk_tannot env typ eff)
   | _ -> raise (Reporting_basic.err_unreachable l "swaptyp called with empty type annotation")
 
 let is_funcl_rec (FCL_aux (FCL_Funcl (id, pexp), _)) =
   let pat,guard,exp,pannot = destruct_pexp pexp in
   let exp = match guard with None -> exp
-    | Some exp' -> E_aux (E_block [exp';exp],(Parse_ast.Unknown,None)) in
+    | Some exp' -> E_aux (E_block [exp';exp],(Parse_ast.Unknown,empty_tannot)) in
   fst (fold_exp
     { (compute_exp_alg false (||) ) with
       e_app = (fun (f, es) ->
@@ -2126,7 +2138,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
       let val_spec =
         VS_aux (VS_val_spec
           (mk_typschm typquant fun_typ, id, (fun _ -> None), false),
-          (Parse_ast.Unknown, None))
+          (Parse_ast.Unknown, empty_tannot))
       in
       let fundef = FD_aux (FD_function (r_o, t_o, e_o, funcls), fdannot) in
       [DEF_spec val_spec; DEF_fundef fundef] @ defs
@@ -2173,13 +2185,17 @@ let rewrite_fix_val_specs (Defs defs) =
 
   let e_aux val_specs (exp, (l, annot)) =
     match fix_eff_exp (E_aux (exp, (l, annot))) with
-    | E_aux (E_app_infix (_, f, _) as exp, (l, Some (env, typ, eff)))
-    | E_aux (E_app (f, _) as exp, (l, Some (env, typ, eff))) ->
+    | E_aux (E_app_infix (_, f, _) as exp, (l, tannot))
+    | E_aux (E_app (f, _) as exp, (l, tannot))
+         when not (is_empty_tannot tannot) ->
+       let env = env_of_annot (l, tannot) in
+       let typ = typ_of_annot (l, tannot) in
+       let eff = effect_of_annot tannot in
        let vs = find_vs env val_specs f in
        (* The (updated) environment is used later by fix_eff_exp to look up
           the actual effects of a function call *)
        let env = Env.update_val_spec f vs env in
-       E_aux (exp, (l, Some (env, typ, union_effects eff (eff_of_vs vs))))
+       E_aux (exp, (l, mk_tannot env typ (union_effects eff (eff_of_vs vs))))
     | e_aux -> e_aux
   in
 
@@ -2567,7 +2583,7 @@ let rewrite_defs_remove_blocks =
 let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
   (* body is a function : E_id variable -> actual body *)
   let (E_aux (_,(l,annot))) = v in
-  match annot with
+  match destruct_tannot annot with
   | Some (env, typ, eff) when is_unit_typ typ ->
      let body = body (annot_exp (E_lit (mk_lit L_unit)) l env unit_typ) in
      let body_typ = try typ_of body with _ -> unit_typ in
@@ -2964,7 +2980,7 @@ let fresh_stringappend_id () =
   id
 
 let unk = Parse_ast.Unknown
-let unkt = (Parse_ast.Unknown, None)
+let unkt = (Parse_ast.Unknown, empty_tannot)
 
 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
@@ -3384,13 +3400,13 @@ let rewrite_defs_pat_lits rewrite_lit =
          match !guards with
          | [] -> pexp
          | (g :: gs) ->
-            let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in
+            let guard_annot = (fst annot, mk_tannot (env_of exp) bool_typ no_effect) in
             Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) g gs, exp), annot)
        end
     | Pat_when (pat, guard, exp) ->
        begin
          let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat } pat in
-         let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in
+         let guard_annot = (fst annot, mk_tannot (env_of exp) bool_typ no_effect) in
          Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) guard !guards, exp), annot)
        end
   in
@@ -3562,7 +3578,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          let env = env_of_annot annot in
          let typ = typ_of e1 in
          let eff = union_eff_exps [c;e1;e2] in
-         let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in
+         let v = E_aux (E_if (c,e1,e2), (gen_loc el, mk_tannot env typ eff)) in
          Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
     | E_case (e1,ps) | E_try (e1, ps) ->
        let is_case = match expaux with E_case _ -> true | _ -> false in
@@ -3587,7 +3603,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          let rewrite_pexp (Pat_aux (pexp, (l, _))) = match pexp with
            | Pat_exp (pat, exp) ->
              let exp = rewrite_var_updates (add_vars overwrite exp vars) in
-             let pannot = (l, Some (env_of exp, typ_of exp, effect_of exp)) in
+             let pannot = (l, mk_tannot (env_of exp) (typ_of exp) (effect_of exp)) in
              Pat_aux (Pat_exp (pat, exp), pannot)
            | Pat_when _ ->
              raise (Reporting_basic.err_unreachable l
@@ -3689,9 +3705,10 @@ let remove_reference_types exp =
     | Typ_arg_aux (Typ_arg_typ t, a) -> Typ_arg_aux (Typ_arg_typ (rewrite_t t), a)
     | _ -> t_arg in
 
-  let rec rewrite_annot = function
-    | (l, None) -> (l, None)
-    | (l, Some (env, typ, eff)) -> (l, Some (env, rewrite_t typ, eff)) in
+  let rec rewrite_annot (l, tannot) =
+    match destruct_tannot tannot with
+    | None -> l, empty_tannot
+    | Some (_, typ, _) -> l, replace_typ (rewrite_t typ) tannot in
 
   map_exp_annot rewrite_annot exp
 
@@ -3715,7 +3732,7 @@ let rewrite_defs_remove_superfluous_letbinds =
          when Id.compare id id' = 0 && small exp1 ->
           let (E_aux (_,e1annot)) = exp1 in
           E_aux (E_internal_return (exp1),e1annot)
-       | _ -> E_aux (exp,annot) 
+       | _ -> E_aux (exp,annot)
        end
     | _ -> E_aux (exp,annot) in
 
@@ -3729,7 +3746,6 @@ let rewrite_defs_remove_superfluous_letbinds =
     ; rewrite_def = rewrite_def
     ; rewrite_defs = rewrite_defs_base
     }
-  
 
 let rewrite_defs_remove_superfluous_returns =
 
@@ -3808,12 +3824,12 @@ let merge_funcls (Defs defs) =
     | (FCL_aux (FCL_Funcl (id,_),(l,_)))::_ ->
        let var = mk_id "merge#var" in
        let l_g = Parse_ast.Generated l in
-       let ann_g : _ * tannot = (l_g,None) in
+       let ann_g : _ * tannot = (l_g,empty_tannot) in
        let clauses = List.map (fun (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp) fcls in
        FD_aux (FD_function (r,t,e,[
          FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (P_aux (P_id var,ann_g),
                                                   E_aux (E_case (E_aux (E_id var,ann_g),clauses),ann_g)),ann_g)),
-                  (l,None))]),ann)
+                  (l,empty_tannot))]),ann)
   in
   let merge_in_def = function
     | DEF_fundef f -> DEF_fundef (merge_function f)
@@ -4261,11 +4277,11 @@ let rewrite_case (e,ann) =
             (fst ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
 
         let l = Parse_ast.Generated Parse_ast.Unknown in
-        let p = P_aux (P_wild, (l, None)) in
-        let ann' = Some (env, typ_of_annot ann, mk_effect [BE_escape]) in
+        let p = P_aux (P_wild, (l, empty_tannot)) in
+        let ann' = mk_tannot env (typ_of_annot ann) (mk_effect [BE_escape]) in
         (* TODO: use an expression that specifically indicates a failed pattern match *)
-        let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,None))),(l,ann')) in
-        E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,None))]),ann)
+        let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in
+        E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,empty_tannot))]),ann)
      end
   | _ -> E_aux (e,ann)