Merge remote-tracking branch 'origin/sail2' into separate_bv

1 files changed, 92 insertions, 56 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index b1fb0cdd..0f747f59 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -771,23 +771,23 @@ and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)
 
 (* A simple check for pattern disjointness; used for optimisation in the
    guarded pattern rewrite step *)
-let rec disjoint_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
+let rec disjoint_pat env (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
   match p1, p2 with
-  | P_as (pat1, _), _ -> disjoint_pat pat1 pat2
-  | _, P_as (pat2, _) -> disjoint_pat pat1 pat2
-  | P_typ (_, pat1), _ -> disjoint_pat pat1 pat2
-  | _, P_typ (_, pat2) -> disjoint_pat pat1 pat2
-  | P_var (pat1, _), _ -> disjoint_pat pat1 pat2
-  | _, P_var (pat2, _) -> disjoint_pat pat1 pat2
-  | P_id id, _ when id_is_unbound id (env_of_annot annot1) -> false
-  | _, P_id id when id_is_unbound id (env_of_annot annot2) -> false
+  | P_as (pat1, _), _ -> disjoint_pat env pat1 pat2
+  | _, P_as (pat2, _) -> disjoint_pat env pat1 pat2
+  | P_typ (_, pat1), _ -> disjoint_pat env pat1 pat2
+  | _, P_typ (_, pat2) -> disjoint_pat env pat1 pat2
+  | P_var (pat1, _), _ -> disjoint_pat env pat1 pat2
+  | _, P_var (pat2, _) -> disjoint_pat env pat1 pat2
+  | P_id id, _ when id_is_unbound id env -> false
+  | _, P_id id when id_is_unbound id env -> false
   | P_id id1, P_id id2 -> Id.compare id1 id2 <> 0
   | P_app (id1, args1), P_app (id2, args2) ->
-     Id.compare id1 id2 <> 0 || List.exists2 disjoint_pat args1 args2
+     Id.compare id1 id2 <> 0 || List.exists2 (disjoint_pat env) args1 args2
   | P_vector pats1, P_vector pats2
   | P_tup pats1, P_tup pats2
   | P_list pats1, P_list pats2 ->
-     List.exists2 disjoint_pat pats1 pats2
+     List.exists2 (disjoint_pat env) pats1 pats2
   | _ -> false
 
 let equiv_pats pat1 pat2 =
@@ -846,6 +846,8 @@ let case_exp e t cs =
   let env = env_of e in
   let annot = (get_loc_exp e, Some (env_of e, t, no_effect)) in
   match cs with
+  | [(P_aux (P_wild, _), body, _)] ->
+    fix_eff_exp body
   | [(P_aux (P_id id, pannot) as pat, body, _)] ->
     fix_eff_exp (annot_exp (E_let (LB_aux (LB_val (pat, e), pannot), body)) l env t)
   | _ ->
@@ -873,7 +875,7 @@ let case_exp e t cs =
   strategy to ours: group *mutually exclusive* clauses, and try to merge them
   into a pattern match first instead of an if-then-else cascade.
 *)
-let rewrite_guarded_clauses l cs =
+let rewrite_guarded_clauses l env pat_typ typ cs =
   let rec group fallthrough clauses =
     let add_clause (pat,cls,annot) c = (pat,cls @ [c],annot) in
     let rec group_aux current acc = (function
@@ -889,10 +891,12 @@ let rewrite_guarded_clauses l cs =
                 let c' = (pat',guard',body',annot) in
                 group_aux (add_clause current c') acc cs
             | None ->
-                let pat = remove_wildcards "g__" pat in
+                let pat = match cs with _::_ -> remove_wildcards "g__" pat | _ -> pat in
                 group_aux (pat,[c],annot) (acc @ [current]) cs)
       | [] -> acc @ [current]) in
     let groups = match clauses with
+      | [(pat,guard,body,annot) as c] ->
+          [(pat, [c], annot)]
       | ((pat,guard,body,annot) as c) :: cs ->
           group_aux (remove_wildcards "g__" pat, [c], annot) [] cs
       | _ ->
@@ -924,7 +928,7 @@ let rewrite_guarded_clauses l cs =
         (* For singleton clauses with a guard, use fallthrough clauses if the
            guard is not satisfied, but only those fallthrough clauses that are
            not disjoint with the current pattern *)
-        let overlapping_clause (pat, _, _) = not (disjoint_pat current_pat pat) in
+        let overlapping_clause (pat, _, _) = not (disjoint_pat env current_pat pat) in
         let fallthrough = List.filter overlapping_clause fallthrough in
         (match guard, fallthrough with
           | Some exp, _ :: _ ->
@@ -934,7 +938,18 @@ let rewrite_guarded_clauses l cs =
     | [] ->
         raise (Reporting.err_unreachable l __POS__
             "if_exp given empty list in rewrite_guarded_clauses")) in
-  group [] cs
+  let is_complete = Pattern_completeness.is_complete (Env.pattern_completeness_ctx env) (List.map construct_pexp cs) in
+  let fallthrough =
+    if not is_complete then
+      let p = P_aux (P_wild, (gen_loc l, mk_tannot env pat_typ no_effect)) in
+      let msg = "Pattern match failure at " ^ Reporting.short_loc_to_string l in
+      let a = mk_exp ~loc:(gen_loc l) (E_assert (mk_lit_exp L_false, mk_lit_exp (L_string msg))) in
+      let b = mk_exp ~loc:(gen_loc l) (E_exit (mk_lit_exp L_unit)) in
+      let (E_aux (_, (_, ann)) as e) = check_exp env (mk_exp ~loc:(gen_loc l) (E_block [a; b])) typ in
+      [(p,None,e,(gen_loc l,ann))]
+    else []
+  in
+  group [] (cs @ fallthrough)
 
 let bitwise_and_exp exp1 exp2 =
   let (E_aux (_,(l,_))) = exp1 in
@@ -1316,7 +1331,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
       (pat, None, rewrite_rec body, annot)
     | Pat_aux (Pat_when (pat, guard, body), annot) ->
       (pat, Some (rewrite_rec guard), rewrite_rec body, annot) in
-    let clauses = rewrite_guarded_clauses l (List.map clause ps) in
+    let clauses = rewrite_guarded_clauses l (env_of full_exp) (typ_of e) (typ_of full_exp) (List.map clause ps) in
     let e = rewrite_rec e in
     if (effectful e) then
       let (E_aux (_,(el,eannot))) = e in
@@ -1334,7 +1349,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
       (pat, None, rewrite_rec body, annot)
     | Pat_aux (Pat_when (pat, guard, body), annot) ->
       (pat, Some (rewrite_rec guard), rewrite_rec body, annot) in
-    let clauses = rewrite_guarded_clauses l (List.map clause ps) in
+    let clauses = rewrite_guarded_clauses l (env_of full_exp) (typ_of e) (typ_of full_exp) (List.map clause ps) in
     let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in
     let ps = List.map pexp clauses in
     fix_eff_exp (annot_exp (E_try (e,ps)) l (env_of full_exp) (typ_of full_exp))
@@ -1342,12 +1357,21 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
 
 let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fdannot))) =
    let funcls = match funcls with
-    | (FCL_aux (FCL_Funcl(id,_),_) :: _) ->
+    | (FCL_aux (FCL_Funcl(id,pexp), fclannot) :: _) ->
        let clause (FCL_aux (FCL_Funcl(_,pexp),annot)) =
          let pat,guard,exp,_ = destruct_pexp pexp in
          let exp = rewriters.rewrite_exp rewriters exp in
          (pat,guard,exp,annot) in
-       let cs = rewrite_guarded_clauses l (List.map clause funcls) in
+       let pexp_pat_typ, pexp_ret_typ =
+         let pat, _, exp, _ = destruct_pexp pexp in
+         (typ_of_pat pat, typ_of exp)
+       in
+       let pat_typ, ret_typ = match Env.get_val_spec_orig id (env_of_annot fclannot) with
+         | (tq, Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _)) -> (arg_typ, ret_typ)
+         | (tq, Typ_aux (Typ_fn (arg_typs, ret_typ, _), _)) -> (tuple_typ arg_typs, ret_typ)
+         | _ -> (pexp_pat_typ, pexp_ret_typ) | exception _ -> (pexp_pat_typ, pexp_ret_typ)
+       in
+       let cs = rewrite_guarded_clauses l (env_of_annot fclannot) pat_typ ret_typ (List.map clause funcls) in
        List.map (fun (pat,exp,annot) ->
          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
@@ -1440,7 +1464,7 @@ let rewrite_defs_exp_lift_assign env defs = rewrite_defs_base
      write_reg_ref (vector_access (GPR, i)) exp
  *)
 let rewrite_register_ref_writes (Defs defs) =
-  let (Defs write_reg_spec) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
+  let (Defs write_reg_spec) = fst (Type_error.check initial_env (Defs (List.map gen_vs
     [("write_reg_ref", "forall ('a : Type). (register('a), 'a) -> unit effect {wreg}")]))) in
   let lexp_ref_exp (LEXP_aux (_, annot) as lexp) =
     try
@@ -1630,7 +1654,7 @@ let rewrite_defs_early_return env (Defs defs) =
     FD_aux (FD_function (rec_opt, tannot_opt, effect_opt,
       List.map (rewrite_funcl_early_return rewriters) funcls), a) in
 
-  let (Defs early_ret_spec) = fst (Type_error.check Env.empty (Defs [gen_vs
+  let (Defs early_ret_spec) = fst (Type_error.check initial_env (Defs [gen_vs
     ("early_return", "forall ('a : Type) ('b : Type). 'a -> 'b effect {escape}")])) in
 
   rewrite_defs_base
@@ -1870,10 +1894,9 @@ let rewrite_fix_val_specs env (Defs defs) =
          Rec_aux (Rec_rec, Parse_ast.Unknown)
       | _ -> recopt
     in
-    let tannotopt = match tannotopt, funcls with
-    | Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), l),
-      FCL_aux (FCL_Funcl (_, Pat_aux ((Pat_exp (_, exp) | Pat_when (_, _, exp)), _)), _) :: _ ->
-       Typ_annot_opt_aux (Typ_annot_opt_some (typq, Env.expand_synonyms (env_of exp) typ), l)
+    let tannotopt = match tannotopt with
+    | Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), l) ->
+       Typ_annot_opt_aux (Typ_annot_opt_none, l)
     | _ -> tannotopt in
     (val_specs, FD_aux (FD_function (recopt, tannotopt, effopt, funcls), a)) in
 
@@ -2459,7 +2482,8 @@ let rewrite_defs_letbind_effects env =
        rewrap (E_var (lexp,exp1,n_exp exp2 k))))
     | E_internal_return exp1 ->
        n_exp_name exp1 (fun exp1 ->
-       k (if effectful (propagate_exp_effect exp1) then exp1 else rewrap (E_internal_return exp1)))
+       let exp1 = fix_eff_exp (propagate_exp_effect exp1) in
+       k (if effectful exp1 then exp1 else rewrap (E_internal_return exp1)))
     | E_internal_value v ->
        k (rewrap (E_internal_value v))
     | E_return exp' ->
@@ -3628,7 +3652,8 @@ let remove_reference_types exp =
 let rewrite_defs_remove_superfluous_letbinds env =
 
   let e_aux (exp,annot) = match exp with
-    | E_let (LB_aux (LB_val (pat, exp1), _), exp2) ->
+    | E_let (LB_aux (LB_val (pat, exp1), _), exp2)
+    | E_internal_plet (pat, exp1, exp2) ->
        begin match untyp_pat pat, uncast_exp exp1, uncast_exp exp2 with
        (* 'let x = EXP1 in x' can be replaced with 'EXP1' *)
        | (P_aux (P_id id, _), _), _, (E_aux (E_id id', _), _)
@@ -3640,22 +3665,22 @@ let rewrite_defs_remove_superfluous_letbinds env =
        (* "let x = EXP1 in return x" can be replaced with 'return (EXP1)', at
           least when EXP1 is 'small' enough *)
        | (P_aux (P_id id, _), _), _, (E_aux (E_internal_return (E_aux (E_id id', _)), _), _)
-         when Id.compare id id' = 0 && small exp1 ->
+         when Id.compare id id' = 0 && small exp1 && not (effectful exp1) ->
           let (E_aux (_,e1annot)) = exp1 in
           E_aux (E_internal_return (exp1),e1annot)
+       | _, (E_aux (E_throw e, a), _), _ -> E_aux (E_throw e, a)
+       | (pat, _), (E_aux (E_assert (c, msg), a) as assert_exp, _), _ ->
+          begin match typ_of c with
+          | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _)
+            when prove __POS__ (env_of c) (nc_not nc) ->
+             (* Drop rest of block after an 'assert(false)' *)
+             let exit_exp = E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) in
+             E_aux (E_internal_plet (pat, assert_exp, exit_exp), annot)
+          | _ ->
+             E_aux (exp, annot)
+          end
        | _ -> E_aux (exp,annot)
        end
-    | E_internal_plet (_, E_aux (E_throw e, a), _) -> E_aux (E_throw e, a)
-    | E_internal_plet (pat, (E_aux (E_assert (c, msg), a) as assert_exp), _) ->
-       begin match typ_of c with
-       | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _)
-         when prove __POS__ (env_of c) (nc_not nc) ->
-          (* Drop rest of block after an 'assert(false)' *)
-          let exit_exp = E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) in
-          E_aux (E_internal_plet (pat, assert_exp, exit_exp), annot)
-       | _ ->
-          E_aux (exp, annot)
-       end
     | _ -> E_aux (exp,annot) in
 
   let alg = { id_exp_alg with e_aux = e_aux } in
@@ -3737,7 +3762,7 @@ let rewrite_defs_remove_superfluous_returns env =
          when lit = lit' ->
           add_opt_cast ptyp etyp a exp1
        | (P_aux (P_wild,pannot), ptyp),
-         (E_aux (E_internal_return (E_aux (E_lit (L_aux (L_unit,_)),_)), a), etyp)
+         (E_aux ((E_internal_return (E_aux (E_lit (L_aux (L_unit,_)),_)) | E_lit (L_aux (L_unit,_))), a), etyp)
          when is_unit_typ (typ_of exp1) ->
           add_opt_cast ptyp etyp a exp1
        | (P_aux (P_id id,_), ptyp),
@@ -3773,7 +3798,7 @@ let rewrite_defs_remove_superfluous_returns env =
 
 
 let rewrite_defs_remove_e_assign env (Defs defs) =
-  let (Defs loop_specs) = fst (Type_error.check Env.empty (Defs (List.map gen_vs
+  let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs
     [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
      ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
      ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
@@ -4660,11 +4685,11 @@ let rewrite_loops_with_escape_effect env defs =
   in
   rewrite_defs_base { rewriters_base with rewrite_exp } defs
 
-let recheck_defs env defs = fst (Type_error.check initial_env defs)
+let recheck_defs env defs = Type_error.check initial_env defs
 let recheck_defs_without_effects env defs =
   let old = !opt_no_effects in
   let () = opt_no_effects := true in
-  let result,_ = Type_error.check initial_env defs in
+  let result = Type_error.check initial_env defs in
   let () = opt_no_effects := old in
   result
 
@@ -4749,9 +4774,10 @@ let opt_auto_mono = ref false
 let opt_dall_split_errors = ref false
 let opt_dmono_continue = ref false
 
-let monomorphise env defs =
+let monomorphise target env defs =
   let open Monomorphise in
   monomorphise
+    target
     { auto = !opt_auto_mono;
       debug_analysis = !opt_dmono_analysis;
       all_split_errors = !opt_dall_split_errors;
@@ -4764,12 +4790,20 @@ let if_mono f env defs =
   | [], false -> defs
   | _, _ -> f env defs
 
+let if_mono_env f env defs =
+  match !opt_mono_split, !opt_auto_mono with
+  | [], false -> defs, env
+  | _, _ -> f env defs
+
 (* Also turn mwords stages on when we're just trying out mono *)
 let if_mwords f env defs =
   if !Pretty_print_lem.opt_mwords then f env defs else if_mono f env defs
+let if_mwords_env f env defs =
+  if !Pretty_print_lem.opt_mwords then f env defs else if_mono_env f env defs
 
 type rewriter =
   | Basic_rewriter of (Env.t -> tannot defs -> tannot defs)
+  | Checking_rewriter of (Env.t -> tannot defs -> tannot defs * Env.t)
   | Bool_rewriter of (bool -> rewriter)
   | String_rewriter of (string -> rewriter)
   | Literal_rewriter of ((lit -> bool) -> rewriter)
@@ -4793,6 +4827,8 @@ let instantiate_rewrite rewriter args =
     match rewriter, arg with
     | Basic_rewriter rw, If_mono_arg -> Basic_rewriter (if_mono rw)
     | Basic_rewriter rw, If_mwords_arg -> Basic_rewriter (if_mwords rw)
+    | Checking_rewriter rw, If_mono_arg -> Checking_rewriter (if_mono_env rw)
+    | Checking_rewriter rw, If_mwords_arg -> Checking_rewriter (if_mwords_env rw)
     | Bool_rewriter rw, Bool_arg b -> rw b
     | String_rewriter rw, String_arg str -> rw str
     | Literal_rewriter rw, Literal_arg selector -> rw (selector_function selector)
@@ -4800,14 +4836,15 @@ let instantiate_rewrite rewriter args =
        raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Invalid rewrite argument")
   in
   match List.fold_left instantiate rewriter args with
-  | Basic_rewriter rw -> rw
+  | Basic_rewriter rw -> fun env defs -> rw env defs, env
+  | Checking_rewriter rw -> rw
   | _ ->
      raise (Reporting.err_general Parse_ast.Unknown "Rewrite not fully instantiated")
 
 let all_rewrites = [
     ("no_effect_check", Basic_rewriter (fun _ defs -> opt_no_effects := true; defs));
-    ("recheck_defs", Basic_rewriter recheck_defs);
-    ("recheck_defs_without_effects", Basic_rewriter recheck_defs_without_effects);
+    ("recheck_defs", Checking_rewriter recheck_defs);
+    ("recheck_defs_without_effects", Checking_rewriter recheck_defs_without_effects);
     ("optimize_recheck_defs", Basic_rewriter (fun _ -> Optimize.recheck));
     ("realise_mappings", Basic_rewriter rewrite_defs_realise_mappings);
     ("remove_mapping_valspecs", Basic_rewriter remove_mapping_valspecs);
@@ -4816,12 +4853,12 @@ let all_rewrites = [
     ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns);
     ("mono_rewrites", Basic_rewriter mono_rewrites);
     ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps);
-    ("monomorphise", Basic_rewriter monomorphise);
+    ("monomorphise", String_rewriter (fun target -> Basic_rewriter (monomorphise target)));
     ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons));
     ("add_bitvector_casts", Basic_rewriter (fun _ -> Monomorphise.add_bitvector_casts));
     ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons));
     ("remove_impossible_int_cases", Basic_rewriter Constant_propagation.remove_impossible_int_cases);
-    ("const_prop_mutrec", Basic_rewriter Constant_propagation_mutrec.rewrite_defs);
+    ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_defs target)));
     ("make_cases_exhaustive", Basic_rewriter MakeExhaustive.rewrite);
     ("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b)));
     ("vector_string_pats_to_bit_list", Basic_rewriter rewrite_defs_vector_string_pats_to_bit_list);
@@ -4853,7 +4890,7 @@ let all_rewrites = [
     ("simple_types", Basic_rewriter rewrite_simple_types);
     ("overload_cast", Basic_rewriter rewrite_overload_cast);
     ("top_sort_defs", Basic_rewriter (fun _ -> top_sort_defs));
-    ("constant_fold", Basic_rewriter (fun _ -> Constant_fold.rewrite_constant_function_calls));
+    ("constant_fold", String_rewriter (fun target -> Basic_rewriter (fun _ -> Constant_fold.rewrite_constant_function_calls target)));
     ("split", String_rewriter (fun str -> Basic_rewriter (rewrite_split_fun_ctor_pats str)));
     ("properties", Basic_rewriter (fun _ -> Property.rewrite));
   ]
@@ -4868,7 +4905,7 @@ let rewrites_lem = [
     ("recheck_defs", [If_mono_arg]);
     ("undefined", [Bool_arg false]);
     ("toplevel_nexps", [If_mono_arg]);
-    ("monomorphise", [If_mono_arg]);
+    ("monomorphise", [String_arg "lem"; If_mono_arg]);
     ("recheck_defs", [If_mwords_arg]);
     ("add_bitvector_casts", [If_mwords_arg]);
     ("atoms_to_singletons", [If_mono_arg]);
@@ -4891,7 +4928,7 @@ let rewrites_lem = [
     ("split", [String_arg "execute"]);
     ("recheck_defs", []);
     ("top_sort_defs", []);
-    ("const_prop_mutrec", []);
+    ("const_prop_mutrec", [String_arg "lem"]);
     ("vector_string_pats_to_bit_list", []);
     ("exp_lift_assign", []);
     ("early_return", []);
@@ -4987,7 +5024,7 @@ let rewrites_c = [
     ("mono_rewrites", [If_mono_arg]);
     ("recheck_defs", [If_mono_arg]);
     ("toplevel_nexps", [If_mono_arg]);
-    ("monomorphise", [If_mono_arg]);
+    ("monomorphise", [String_arg "c"; If_mono_arg]);
     ("atoms_to_singletons", [If_mono_arg]);
     ("recheck_defs", [If_mono_arg]);
     ("undefined", [Bool_arg false]);
@@ -5002,7 +5039,7 @@ let rewrites_c = [
     ("exp_lift_assign", []);
     ("merge_function_clauses", []);
     ("optimize_recheck_defs", []);
-    ("constant_fold", [])
+    ("constant_fold", [String_arg "c"])
   ]
 
 let rewrites_interpreter = [
@@ -5025,7 +5062,6 @@ let rewrites_target tgt =
   | "c" -> rewrites_c
   | "ir" -> rewrites_c @ [("properties", [])]
   | "smt" -> rewrites_c @ [("properties", [])]
-  | "smtfuzz" -> rewrites_c @ [("properties", [])]
   | "sail" -> []
   | "latex" -> []
   | "interpreter" -> rewrites_interpreter
@@ -5065,5 +5101,5 @@ let rewrite_check_annot =
                                           rewrite_pat = (fun _ -> check_pat) }
 
 let rewrite_defs_check = [
-  ("check_annotations", fun _ -> rewrite_check_annot);
+  ("check_annotations", fun env defs -> rewrite_check_annot defs, env);
   ]