Refactor: Rename 'a defs to 'a ast

Change internal terminology so we more clearly distinguish between a list of
definitions 'defs' and functions that take an entire abstract syntax
trees 'ast'.

34 files changed, 187 insertions, 186 deletions

diff --git a/src/ast_defs.ml b/src/ast_defs.ml
index 7d7c7ac5..0ce71618 100644
--- a/src/ast_defs.ml
+++ b/src/ast_defs.ml
@@ -50,4 +50,4 @@
 
 open Ast
 
-type 'a defs = Defs of 'a def list
+type 'a ast = Defs of 'a def list
diff --git a/src/ast_util.ml b/src/ast_util.ml
index a342fc6b..b0137880 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -713,7 +713,7 @@ and map_def_annot f = function
   | DEF_reg_dec ds -> DEF_reg_dec (map_decspec_annot f ds)
   | DEF_internal_mutrec fds -> DEF_internal_mutrec (List.map (map_fundef_annot f) fds)
   | DEF_pragma (name, arg, l) -> DEF_pragma (name, arg, l)
-and map_defs_annot f = function
+and map_ast_annot f = function
   | Defs defs -> Defs (List.map (map_def_annot f) defs)
 
 and map_loop_measure_annot f = function
@@ -1086,7 +1086,7 @@ let ids_of_def = function
   | DEF_spec vs -> IdSet.singleton (id_of_val_spec vs)
   | DEF_internal_mutrec fds -> IdSet.of_list (List.map id_of_fundef fds)
   | _ -> IdSet.empty
-let ids_of_defs (Defs defs) =
+let ids_of_ast (Defs defs) =
   List.fold_left IdSet.union IdSet.empty (List.map ids_of_def defs)
 
 let val_spec_ids (Defs defs) =
@@ -1540,7 +1540,7 @@ let rec split_defs' f defs acc =
   | def :: defs when f def -> Some (acc, def, defs)
   | def :: defs -> split_defs' f defs (def :: acc)
 
-let split_defs f (Defs defs) =
+let split_ast f (Defs defs) =
   match split_defs' f defs [] with
   | None -> None
   | Some (pre_defs, def, post_defs) ->
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 5d740277..d9f80778 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -355,7 +355,7 @@ val map_valspec_annot : ('a annot -> 'b annot) -> 'a val_spec -> 'b val_spec
 val map_scattered_annot : ('a annot -> 'b annot) -> 'a scattered_def -> 'b scattered_def
 
 val map_def_annot : ('a annot -> 'b annot) -> 'a def -> 'b def
-val map_defs_annot : ('a annot -> 'b annot) -> 'a defs -> 'b defs
+val map_ast_annot : ('a annot -> 'b annot) -> 'a ast -> 'b ast
 
 (** {2 Extract locations from terms} *)
 val id_loc : id -> Parse_ast.l
@@ -455,17 +455,17 @@ val rename_valspec : id -> 'a val_spec -> 'a val_spec
 
 val rename_fundef : id -> 'a fundef -> 'a fundef
 
-val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option
+val split_ast : ('a def -> bool) -> 'a ast -> ('a ast * 'a def * 'a ast) option
 
-val append_ast : 'a defs -> 'a defs -> 'a defs
-val concat_ast : 'a defs list -> 'a defs
+val append_ast : 'a ast -> 'a ast -> 'a ast
+val concat_ast : 'a ast list -> 'a ast
 
 val type_union_id : type_union -> id
 
 val ids_of_def : 'a def -> IdSet.t
-val ids_of_defs : 'a defs -> IdSet.t
+val ids_of_ast : 'a ast -> IdSet.t
 
-val val_spec_ids : 'a defs -> IdSet.t
+val val_spec_ids : 'a ast -> IdSet.t
 
 val pat_ids : 'a pat -> IdSet.t
 
@@ -502,7 +502,7 @@ val extern_assoc : string -> (string * string) list -> string option
    the closest annotation or even finding an annotation at all. This
    is used by the Emacs mode to provide type-at-cursor functionality
    and we don't mind if it's a bit fuzzy in that context. *)
-val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a defs -> (Ast.l * 'a) option
+val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a ast -> (Ast.l * 'a) option
 
 (** {2 Substitutions}
 
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 1c273df1..c9314002 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -302,7 +302,7 @@ let rec rewrite_constant_function_calls' fixed target ast =
       rewriters_base with
       rewrite_exp = (fun _ -> rw_exp fixed target ok not_ok istate)
     } in
-  let ast = rewrite_defs_base rw_defs ast in
+  let ast = rewrite_ast_base rw_defs ast in
   (* We keep iterating until we have no more re-writes to do *)
   if !rewrite_count > 0
   then rewrite_constant_function_calls' fixed target ast
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index c190cffc..b7bc0a69 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -307,7 +307,7 @@ let const_props target defs ref_vars =
     let interpreter_istate =
       (* Do not interpret undefined_X functions *)
       let open Interpreter in
-      let undefined_builtin_ids = ids_of_defs (Defs Initial_check.undefined_builtin_val_specs) in
+      let undefined_builtin_ids = ids_of_ast (Defs Initial_check.undefined_builtin_val_specs) in
       let remove_primop id = StringMap.remove (string_of_id id) in
       let remove_undefined_primops = IdSet.fold remove_primop undefined_builtin_ids in
       let (lstate, gstate) = Constant_fold.initial_state defs Type_check.initial_env in
@@ -894,4 +894,4 @@ let remove_impossible_int_cases _ =
   in
   let open Rewriter in
   let rewrite_exp _ = fold_exp { id_exp_alg with e_case = e_case; e_if = e_if } in
-  rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp }
+  rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp }
diff --git a/src/constant_propagation.mli b/src/constant_propagation.mli
index 1312290a..fb2ad179 100644
--- a/src/constant_propagation.mli
+++ b/src/constant_propagation.mli
@@ -61,7 +61,7 @@ open Type_check
 
 val const_prop :
   string ->
-  tannot defs ->
+  tannot ast ->
   IdSet.t ->
   tannot exp Bindings.t * nexp KBindings.t ->
   tannot exp Bindings.t ->
@@ -70,4 +70,4 @@ val const_prop :
 
 val referenced_vars : tannot exp -> IdSet.t
 
-val remove_impossible_int_cases : 'a -> tannot defs -> tannot defs
+val remove_impossible_int_cases : 'a -> tannot ast -> tannot ast
diff --git a/src/constant_propagation_mutrec.ml b/src/constant_propagation_mutrec.ml
index a8c26bff..67d218dd 100644
--- a/src/constant_propagation_mutrec.ml
+++ b/src/constant_propagation_mutrec.ml
@@ -191,7 +191,7 @@ let prop_args_pexp target defs ksubsts args pexp =
   in
   construct_pexp (pat', guard, exp', annot)
 
-let rewrite_defs target env (Defs defs) =
+let rewrite_ast target env (Defs defs) =
   let rec rewrite = function
     | [] -> []
     | DEF_internal_mutrec mutrecs :: ds ->
@@ -206,7 +206,7 @@ let rewrite_defs target env (Defs defs) =
              | [] -> [infer_exp env (mk_lit_exp L_unit)]
              | args' -> args'
            in
-           if not (IdSet.mem id' (ids_of_defs (Defs !valspecs))) then begin
+           if not (IdSet.mem id' (ids_of_ast (Defs !valspecs))) then begin
              (* Generate copy of function with constant arguments propagated in *)
              let (FD_aux (FD_function (_, _, _, fcls), _)) =
                List.find (fun fd -> Id.compare id (id_of_fundef fd) = 0) mutrecs
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 48bdc785..0a5db7c2 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -97,14 +97,14 @@ val undefined_builtin_val_specs : unit def list
 
 (** If the generate flag is false, then we won't generate any
    auxilliary definitions, like the initialize_registers function *)
-val process_ast : ?generate:bool -> Parse_ast.defs -> unit defs
+val process_ast : ?generate:bool -> Parse_ast.defs -> unit ast
 
 (** {2 Parsing expressions and definitions from strings} *)
 
 val extern_of_string : id -> string -> unit def
 val val_spec_of_string : id -> string -> unit def
-val ast_of_def_string : string -> unit defs
-val ast_of_def_string_with : (Parse_ast.def list -> Parse_ast.def list) -> string -> unit defs
+val ast_of_def_string : string -> unit ast
+val ast_of_def_string_with : (Parse_ast.def list -> Parse_ast.def list) -> string -> unit ast
 val exp_of_string : string -> unit exp
 val typ_of_string : string -> typ
 val constraint_of_string : string -> n_constraint
diff --git a/src/interactive.mli b/src/interactive.mli
index 46b52022..0b087dc7 100644
--- a/src/interactive.mli
+++ b/src/interactive.mli
@@ -57,7 +57,7 @@ val opt_emacs_mode : bool ref
 val opt_suppress_banner : bool ref
 val opt_auto_interpreter_rewrites : bool ref
 
-val ast : tannot defs ref
+val ast : tannot ast ref
 
 val env : Env.t ref
 
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index d4478c88..cbd0d36e 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -48,6 +48,7 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+open Ast_defs
 open Jib
 open Type_check
 
@@ -99,7 +100,7 @@ val optimize_alias : bool ref
 val optimize_fixed_int : bool ref
 val optimize_fixed_bits : bool ref
 
-val jib_of_ast : Env.t -> tannot Ast_defs.defs -> cdef list * Jib_compile.ctx
-val compile_ast : Env.t -> out_channel -> string list -> tannot Ast_defs.defs -> unit
+val jib_of_ast : Env.t -> tannot ast -> cdef list * Jib_compile.ctx
+val compile_ast : Env.t -> out_channel -> string list -> tannot ast -> unit
 
-val compile_ast_clib : Env.t -> tannot Ast_defs.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit
+val compile_ast_clib : Env.t -> tannot ast -> (Jib_compile.ctx -> cdef list -> unit) -> unit
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 38d03d40..a0acdd0d 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -128,7 +128,7 @@ module Make(C: Config) : sig
        (see Util.progress). *)
   val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx
 
-  val compile_ast : ctx -> tannot defs -> cdef list * ctx
+  val compile_ast : ctx -> tannot ast -> cdef list * ctx
 end
 
 (** Adds some special functions to the environment that are used to
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 2e0299d9..b03c1134 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -91,7 +91,7 @@ type ctx = {
     tc_env : Type_check.Env.t;
     pragma_l : Ast.l;
     arg_stack : (int * string) Stack.t;
-    ast : Type_check.tannot defs;
+    ast : Type_check.tannot ast;
     shared : ctyp Bindings.t;
     preserved : IdSet.t;
     events : smt_exp Stack.t EventMap.t ref;
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index 421cbf2c..820f06d1 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -92,7 +92,7 @@ type ctx = {
        generating the SMT for. Used for error messages. *)
     arg_stack : (int * string) Stack.t;
     (** Used internally to keep track of function argument names *)
-    ast : Type_check.tannot defs;
+    ast : Type_check.tannot ast;
     (** The fully type-checked ast *)
     shared : ctyp Bindings.t;
     (** Shared variables. These variables do not get renamed by
@@ -124,7 +124,7 @@ type ctx = {
   }
 
 (** Compile an AST into Jib suitable for SMT generation, and initialise a context. *)
-val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * Jib_compile.ctx * ctx
+val compile : Type_check.Env.t -> Type_check.tannot ast -> cdef list * Jib_compile.ctx * ctx
 
 (* TODO: Currently we internally use mutable stacks and queues to
    avoid any issues with stack overflows caused by some non
@@ -154,7 +154,7 @@ module Make_optimizer(S : Sequence) : sig
 end
 
 val serialize_smt_model :
-  string -> Type_check.Env.t -> Type_check.tannot defs -> unit
+  string -> Type_check.Env.t -> Type_check.tannot ast -> unit
 
 val deserialize_smt_model :
   string -> cdef list * ctx
@@ -165,5 +165,5 @@ val generate_smt :
   (string * string * l * 'a val_spec) Bindings.t (* See Property.find_properties *)
   -> (string -> string) (* Applied to each function name to generate the file name for the smtlib file *)
   -> Type_check.Env.t
-  -> Type_check.tannot defs
+  -> Type_check.tannot ast
   -> unit
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 318cfa63..968b1172 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3410,7 +3410,7 @@ and rewrite_exp exp = Rewriter.fold_exp { Rewriter.id_exp_alg with e_aux = rewri
 
 let mono_rewrite defs =
   let open Rewriter in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewriters_base with
       rewrite_exp = fun _ -> fold_exp { id_exp_alg with e_aux = rewrite_aux } }
     defs
diff --git a/src/monomorphise.mli b/src/monomorphise.mli
index 7db12078..bf6c9520 100644
--- a/src/monomorphise.mli
+++ b/src/monomorphise.mli
@@ -61,17 +61,17 @@ val monomorphise :
   string -> (* Target backend *)
   options ->
   ((string * int) * string) list -> (* List of splits from the command line *)
-  Type_check.tannot defs ->
-  Type_check.tannot defs
+  Type_check.tannot ast ->
+  Type_check.tannot ast
 
 (* Rewrite (combinations of) variable-sized operations into fixed-sized operations *)
-val mono_rewrites : Type_check.tannot defs -> Type_check.tannot defs
+val mono_rewrites : Type_check.tannot ast -> Type_check.tannot ast
 
 (* Move complex nexps in function signatures into constraints *)
-val rewrite_toplevel_nexps : Type_check.tannot defs -> Type_check.tannot defs
+val rewrite_toplevel_nexps : Type_check.tannot ast -> Type_check.tannot ast
 
 (* Add casts across case splits *)
-val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs
+val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast
 
 (* Replace atom arguments which are fixed by a type parameter for a size with a singleton type *)
-val rewrite_atoms_to_singletons : string -> Type_check.tannot defs -> Type_check.tannot defs
+val rewrite_atoms_to_singletons : string -> Type_check.tannot ast -> Type_check.tannot ast
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 2738e025..2995b8a3 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -53,4 +53,4 @@ open Ast_defs
 open Type_check
 
 (* Prints on formatter the defs as Lem Ast nodes *)
-val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> Env.t -> tannot defs -> string -> unit
+val pp_ast_lem : (out_channel * string list) -> (out_channel * string list) -> Env.t -> tannot ast -> string -> unit
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c3006d7a..dff937a7 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1561,7 +1561,7 @@ let find_exc_typ defs =
     | _ -> false in
   if List.exists is_exc_typ_def defs then "exception" else "unit"
 
-let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) type_env (Defs defs) top_line =
+let pp_ast_lem (types_file,types_modules) (defs_file,defs_modules) type_env (Defs defs) top_line =
   (* let regtypes = find_regtypes d in *)
   let state_ids =
     State.generate_regstate_defs !opt_mwords defs
diff --git a/src/process_file.ml b/src/process_file.ml
index 2cf0325e..63ea49cc 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -264,9 +264,9 @@ let opt_ddump_tc_ast = ref false
 let opt_ddump_rewrite_ast = ref None
 let opt_dno_cast = ref false
 
-let check_ast (env : Type_check.Env.t) (defs : unit defs) : Type_check.tannot defs * Type_check.Env.t =
+let check_ast (env : Type_check.Env.t) (ast : unit ast) : Type_check.tannot ast * Type_check.Env.t =
   let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in
-  let ast, env = Type_error.check env defs in
+  let ast, env = Type_error.check env ast in
   let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in
   let () = if !opt_just_check then exit 0 else () in
   (ast, env)
@@ -367,7 +367,7 @@ let output_lem filename libs type_env defs =
     open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in
   let ((o,_,_,_) as ext_o) =
     open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in
-  (Pretty_print.pp_defs_lem
+  (Pretty_print.pp_ast_lem
      (ot, base_imports)
      (o, base_imports @ (String.capitalize_ascii types_module :: libs))
      type_env defs generated_line);
@@ -446,11 +446,11 @@ let rewrite env rewriters defs =
   | Type_check.Type_error (_, l, err) ->
      raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
-let rewrite_ast_initial env = rewrite env [("initial", fun env defs -> Rewriter.rewrite_defs defs, env)]
+let rewrite_ast_initial env = rewrite env [("initial", fun env defs -> Rewriter.rewrite_ast defs, env)]
 
-let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_defs_target tgt)
+let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_ast_target tgt)
 
-let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check
+let rewrite_ast_check env = rewrite env Rewrites.rewrite_ast_check
 
 let descatter type_envs ast =
   let ast = Scattered.descatter ast in
diff --git a/src/process_file.mli b/src/process_file.mli
index 041026d5..1c4cddc9 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -59,10 +59,10 @@ val have_symbol : string -> bool
 val add_symbol : string -> unit
 
 val preprocess : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.def list -> Parse_ast.def list
-val check_ast : Type_check.Env.t -> unit defs -> Type_check.tannot defs * Type_check.Env.t
-val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t
-val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t
-val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t
+val check_ast : Type_check.Env.t -> unit ast -> Type_check.tannot ast * Type_check.Env.t
+val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t
+val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t
+val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t
 
 val opt_file_out : string option ref
 val opt_memo_z3 : bool ref
@@ -84,9 +84,9 @@ type out_type =
   | Coq_out of string list (* If present, the strings are files to open in the coq backend*)
 
 val output :
-  string ->                           (* The path to the library *)
-  out_type ->                         (* Backend kind *)
-  (string * Type_check.Env.t * Type_check.tannot Ast_defs.defs) list -> (*File names paired with definitions *)
+  string -> (* The path to the library *)
+  out_type -> (* Backend kind *)
+  (string * Type_check.Env.t * Type_check.tannot ast) list -> (*File names paired with definitions *)
   unit
 
 (** [always_replace_files] determines whether Sail only updates modified files.
@@ -95,6 +95,6 @@ val output :
     the output file is only updated, if its content really changes. *)
 val always_replace_files : bool ref
 
-val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot defs * Type_check.Env.t)
+val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot ast * Type_check.Env.t)
 
-val descatter : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t
+val descatter : Type_check.Env.t -> Type_check.tannot ast -> Type_check.tannot ast * Type_check.Env.t
diff --git a/src/property.mli b/src/property.mli
index bba1f638..2d366fa0 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -67,7 +67,7 @@ open Type_check
    where prop_type is either "counterexample" or "property" and the
    location loc is the location that was attached to the pragma
 *)
-val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t
+val find_properties : 'a ast -> (string * string * l * 'a val_spec) Bindings.t
 
 (** For a property
 
@@ -87,7 +87,7 @@ val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t
    generation/proving we want to ensure that inputs outside the
    constraints of the function are ignored.
 *)
-val rewrite : tannot defs -> tannot defs
+val rewrite : tannot ast -> tannot ast
 
 type event = Overflow | Assertion | Assumption | Match | Return
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index eb8208dd..49689b96 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -61,7 +61,7 @@ type 'a rewriters = {
     rewrite_let  : 'a rewriters -> 'a letbind -> 'a letbind;
     rewrite_fun  : 'a rewriters -> 'a fundef -> 'a fundef;
     rewrite_def  : 'a rewriters -> 'a def -> 'a def;
-    rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
+    rewrite_ast  : 'a rewriters -> 'a ast -> 'a ast;
   }
 
 let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a
@@ -386,13 +386,13 @@ let rewrite_def rewriters d = match d with
   | DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp)
   | DEF_loop_measures (id,_) -> raise (Reporting.err_unreachable (id_loc id) __POS__ "DEF_loop_measures survived to rewriter")
 
-let rewrite_defs_base rewriters (Defs defs) =
+let rewrite_ast_base rewriters (Defs defs) =
   let rec rewrite ds = match ds with
     | [] -> []
     | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in
   Defs (rewrite defs)
 
-let rewrite_defs_base_progress prefix rewriters (Defs defs) =
+let rewrite_ast_base_progress prefix rewriters (Defs defs) =
   let total = List.length defs in
   let rec rewrite n = function
     | [] -> []
@@ -411,7 +411,7 @@ let rec takedrop n xs =
      let ys, xs = takedrop (n - 1) xs in
      x :: ys, xs
 
-let rewrite_defs_base_parallel j rewriters (Defs defs) =
+let rewrite_ast_base_parallel j rewriters (Defs defs) =
   let module IntMap = Map.Make(struct type t = int let compare = compare end) in
   let total = List.length defs in
   let defs = ref defs in
@@ -428,7 +428,7 @@ let rewrite_defs_base_parallel j rewriters (Defs defs) =
     let pid = Unix.fork () in
     begin
       if pid = 0 then
-        let Defs work = rewrite_defs_base rewriters (Defs work) in
+        let Defs work = rewrite_ast_base rewriters (Defs work) in
         let out_chan = open_out result in
         Marshal.to_channel out_chan work [Marshal.Closures];
         close_out out_chan;
@@ -468,9 +468,9 @@ let rewriters_base =
    rewrite_lexp = rewrite_lexp;
    rewrite_fun = rewrite_fun;
    rewrite_def = rewrite_def;
-   rewrite_defs = rewrite_defs_base}
+   rewrite_ast = rewrite_ast_base}
 
-let rewrite_defs (Defs defs) = rewrite_defs_base rewriters_base (Defs defs)
+let rewrite_ast (Defs defs) = rewrite_ast_base rewriters_base (Defs defs)
 
 type ('a,'pat,'pat_aux) pat_alg =
   { p_lit            : lit -> 'pat_aux
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 9ea01096..fd874ba0 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -61,7 +61,7 @@ type 'a rewriters = { rewrite_exp  : 'a rewriters -> 'a exp -> 'a exp;
                       rewrite_let  : 'a rewriters -> 'a letbind -> 'a letbind;
                       rewrite_fun  : 'a rewriters -> 'a fundef -> 'a fundef;
                       rewrite_def  : 'a rewriters -> 'a def -> 'a def;
-                      rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
+                      rewrite_ast : 'a rewriters -> 'a ast -> 'a ast;
                     }
 
 val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
@@ -69,14 +69,14 @@ val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
 val rewriters_base : tannot rewriters
 
 (** The identity re-writer *)
-val rewrite_defs : tannot defs -> tannot defs
+val rewrite_ast : tannot ast -> tannot ast
 
-val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs
+val rewrite_ast_base : tannot rewriters -> tannot ast -> tannot ast
 
-val rewrite_defs_base_parallel : int -> tannot rewriters -> tannot defs -> tannot defs
+val rewrite_ast_base_parallel : int -> tannot rewriters -> tannot ast -> tannot ast
 
 (** Same as rewrite_defs_base but display a progress bar when verbosity >= 1 *)
-val rewrite_defs_base_progress : string -> tannot rewriters -> tannot defs -> tannot defs
+val rewrite_ast_base_progress : string -> tannot rewriters -> tannot ast -> tannot ast
 
 val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index b1cfce86..ff909a35 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -219,7 +219,7 @@ let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with
   | Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l)
   | _ -> nexp_aux
 
-let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
+let rewrite_ast_nexp_ids, rewrite_typ_nexp_ids =
   let rec rewrite_typ env (Typ_aux (typ, l) as typ_aux) = match typ with
     | Typ_fn (arg_ts, ret_t, eff) ->
        Typ_aux (Typ_fn (List.map (rewrite_typ env) arg_ts, rewrite_typ env ret_t, eff), l)
@@ -271,20 +271,20 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
     | d -> Rewriter.rewrite_def rewriters d
   in
 
-  (fun env defs -> rewrite_defs_base { rewriters_base with
+  (fun env defs -> rewrite_ast_base { rewriters_base with
     rewrite_exp = (fun _ -> map_exp_annot rewrite_annot);
     rewrite_def = rewrite_def env
     } defs),
   rewrite_typ
 
 
-let rewrite_defs_remove_assert defs =
+let rewrite_ast_remove_assert defs =
   let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with
     | E_constraint _ ->
        E_assert (exp, str)
     | _ ->
        E_assert (E_aux (E_lit (mk_lit L_true), simple_annot l bool_typ), str) in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewriters_base with
       rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_assert = e_assert}) }
     defs
@@ -595,7 +595,7 @@ let rewrite_fun_remove_vector_concat_pat
     (FCL_aux (FCL_Funcl (id,pexp'),(l,annot)))
   in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
 
-let rewrite_defs_remove_vector_concat env (Defs defs) =
+let rewrite_ast_remove_vector_concat env (Defs defs) =
   let rewriters =
     {rewrite_exp = rewrite_exp_remove_vector_concat_pat;
      rewrite_pat = rewrite_pat;
@@ -603,7 +603,7 @@ let rewrite_defs_remove_vector_concat env (Defs defs) =
      rewrite_lexp = rewrite_lexp;
      rewrite_fun = rewrite_fun_remove_vector_concat_pat;
      rewrite_def = rewrite_def;
-     rewrite_defs = rewrite_defs_base} in
+     rewrite_ast = rewrite_ast_base} in
   let rewrite_def d =
     let d = rewriters.rewrite_def rewriters d in
     match d with
@@ -1188,7 +1188,7 @@ let rewrite_fun_remove_bitvector_pat
     | _ -> funcls in
   FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))
 
-let rewrite_defs_remove_bitvector_pats env (Defs defs) =
+let rewrite_ast_remove_bitvector_pats env (Defs defs) =
   let rewriters =
     {rewrite_exp = rewrite_exp_remove_bitvector_pat;
      rewrite_pat = rewrite_pat;
@@ -1196,7 +1196,7 @@ let rewrite_defs_remove_bitvector_pats env (Defs defs) =
      rewrite_lexp = rewrite_lexp;
      rewrite_fun = rewrite_fun_remove_bitvector_pat;
      rewrite_def = rewrite_def;
-     rewrite_defs = rewrite_defs_base } in
+     rewrite_ast = rewrite_ast_base } in
   let rewrite_def d =
     let d = rewriters.rewrite_def rewriters d in
     match d with
@@ -1213,7 +1213,7 @@ let rewrite_defs_remove_bitvector_pats env (Defs defs) =
 (* Rewrite literal number patterns to guarded patterns
    Those numeral patterns are not handled very well by Lem (or Isabelle)
  *)
-let rewrite_defs_remove_numeral_pats env =
+let rewrite_ast_remove_numeral_pats env =
   let p_lit outer_env = function
     | L_aux (L_num n, l) ->
        let id = fresh_id "l__" Parse_ast.Unknown in
@@ -1243,10 +1243,10 @@ let rewrite_defs_remove_numeral_pats env =
     FCL_aux (FCL_Funcl (id, fold_pexp exp_alg pexp), annot) in
   let rewrite_fun _ (FD_aux (FD_function (r_o, t_o, e_o, funcls), a)) =
     FD_aux (FD_function (r_o, t_o, e_o, List.map rewrite_funcl funcls), a) in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewriters_base with rewrite_exp = rewrite_exp; rewrite_fun = rewrite_fun }
 
-let rewrite_defs_vector_string_pats_to_bit_list env =
+let rewrite_ast_vector_string_pats_to_bit_list env =
   let rewrite_p_aux (pat, (annot : tannot annot)) =
     let env = env_of_annot annot in
     match pat with
@@ -1266,7 +1266,7 @@ let rewrite_defs_vector_string_pats_to_bit_list env =
   let rewrite_exp rw exp =
     fold_exp { id_exp_alg with e_aux = rewrite_e_aux; pat_alg = pat_alg } exp
   in
-  rewrite_defs_base { rewriters_base with rewrite_pat = rewrite_pat; rewrite_exp = rewrite_exp }
+  rewrite_ast_base { rewriters_base with rewrite_pat = rewrite_pat; rewrite_exp = rewrite_exp }
 
 let rewrite_bit_lists_to_lits env =
   (* TODO Make all rewriting passes support bitvector literals instead of
@@ -1299,7 +1299,7 @@ let rewrite_bit_lists_to_lits env =
     with _ -> rewrap e
   in
   let rewrite_exp rw = fold_exp { id_exp_alg with e_aux = e_aux; } in
-  rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp }
+  rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp }
 
 (* Remove pattern guards by rewriting them to if-expressions within the
    pattern expression. *)
@@ -1364,9 +1364,9 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd
      | _ -> funcls (* TODO is the empty list possible here? *) in
    FD_aux (FD_function(r,t,e,funcls),(l,fdannot))
 
-let rewrite_defs_guarded_pats env =
-  rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp_guarded_pats;
-                    rewrite_fun = rewrite_fun_guarded_pats }
+let rewrite_ast_guarded_pats env =
+  rewrite_ast_base { rewriters_base with rewrite_exp = rewrite_exp_guarded_pats;
+                     rewrite_fun = rewrite_fun_guarded_pats }
 
 
 let rec rewrite_lexp_to_rhs ((LEXP_aux(lexp,((l,_) as annot))) as le) =
@@ -1397,7 +1397,7 @@ let updates_vars exp =
   fst (fold_exp { (compute_exp_alg false (||)) with e_assign = e_assign } exp)
 
 
-(*Expects to be called after rewrite_defs; thus the following should not appear:
+(*Expects to be called after rewrite_ast; thus the following should not appear:
   internal_exp of any form
   lit vectors in patterns or expressions
  *)
@@ -1430,14 +1430,14 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
 
   | _ -> rewrite_base full_exp
 
-let rewrite_defs_exp_lift_assign env defs = rewrite_defs_base
+let rewrite_ast_exp_lift_assign env defs = rewrite_ast_base
     {rewrite_exp = rewrite_exp_lift_assign_intro;
      rewrite_pat = rewrite_pat;
      rewrite_let = rewrite_let;
      rewrite_lexp = rewrite_lexp (*_lift_assign_intro*);
      rewrite_fun = rewrite_fun;
      rewrite_def = rewrite_def;
-     rewrite_defs = rewrite_defs_base} defs
+     rewrite_ast = rewrite_ast_base} defs
 
 
 (* Rewrite assignments to register references into calls to a builtin function
@@ -1478,7 +1478,7 @@ let rewrite_register_ref_writes (Defs defs) =
    TODO: Maybe separate generic removal of redundant returns, and Lem-specific
    rewriting of early returns
  *)
-let rewrite_defs_early_return env (Defs defs) =
+let rewrite_ast_early_return env (Defs defs) =
   let is_unit (E_aux (exp, _)) = match exp with
   | E_lit (L_aux (L_unit, _)) -> true
   | _ -> false in
@@ -1649,7 +1649,7 @@ let rewrite_defs_early_return env (Defs defs) =
   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
+  rewrite_ast_base
     { rewriters_base with rewrite_fun = rewrite_fun_early_return }
     (Defs (early_ret_spec @ defs))
 
@@ -1998,7 +1998,7 @@ let rewrite_undefined mwords env =
     | _ -> exp
   in
   let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in
-  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) }
+  rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) }
 
 let rewrite_undefined_if_gen always_bitvector env defs =
   if !Initial_check.opt_undefined_gen
@@ -2077,7 +2077,7 @@ let rewrite_simple_types env (Defs defs) =
                                           rewrite_pat = (fun _ -> fold_pat simple_pat) }
   in
   let defs = Defs (List.map simple_def defs) in
-  rewrite_defs_base simple_defs defs
+  rewrite_ast_base simple_defs defs
 
 let rewrite_vector_concat_assignments env defs =
   let assign_tuple e_aux annot =
@@ -2137,7 +2137,7 @@ let rewrite_vector_concat_assignments env defs =
       e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot)
     } in
   let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
-  rewrite_defs_base assign_defs defs
+  rewrite_ast_base assign_defs defs
 
 let rewrite_tuple_assignments env defs =
   let assign_tuple e_aux annot =
@@ -2162,7 +2162,7 @@ let rewrite_tuple_assignments env defs =
       e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot)
     } in
   let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
-  rewrite_defs_base assign_defs defs
+  rewrite_ast_base assign_defs defs
 
 let rewrite_simple_assignments allow_fields env defs =
   let rec is_simple (LEXP_aux (aux, _)) =
@@ -2188,9 +2188,9 @@ let rewrite_simple_assignments allow_fields env defs =
       e_aux = (fun (e_aux, annot) -> assign_e_aux e_aux annot)
     } in
   let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
-  rewrite_defs_base assign_defs defs
+  rewrite_ast_base assign_defs defs
 
-let rewrite_defs_remove_blocks env =
+let rewrite_ast_remove_blocks env =
   let letbind_wild v body =
     let l = get_loc_exp v in
     let env = env_of v in
@@ -2212,14 +2212,14 @@ let rewrite_defs_remove_blocks env =
 
   let alg = { id_exp_alg with e_aux = e_aux } in
 
-  rewrite_defs_base
+  rewrite_ast_base
     {rewrite_exp = (fun _ -> fold_exp alg)
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
     ; rewrite_fun = rewrite_fun
     ; rewrite_def = rewrite_def
-    ; rewrite_defs = rewrite_defs_base
+    ; rewrite_ast = rewrite_ast_base
     }
 
 
@@ -2249,7 +2249,7 @@ let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list
   | [] -> k []
   | exp :: exps -> f exp (fun exp -> mapCont f exps (fun exps -> k (exp :: exps)))
 
-let rewrite_defs_letbind_effects env =
+let rewrite_ast_letbind_effects env =
 
   let rec value ((E_aux (exp_aux,_)) as exp) =
     not (effectful exp || updates_vars exp)
@@ -2528,17 +2528,17 @@ let rewrite_defs_letbind_effects env =
       DEF_internal_mutrec (List.map (rewrite_fun rewriters) fdefs)
     | d -> d
   in
-  rewrite_defs_base
+  rewrite_ast_base
     {rewrite_exp = rewrite_exp
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
     ; rewrite_fun = rewrite_fun
     ; rewrite_def = rewrite_def
-    ; rewrite_defs = rewrite_defs_base
+    ; rewrite_ast = rewrite_ast_base
     }
 
-let rewrite_defs_internal_lets env =
+let rewrite_ast_internal_lets env =
 
   let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with
     | LEXP_id id -> P_aux (P_id id, annot)
@@ -2581,14 +2581,14 @@ let rewrite_defs_internal_lets env =
       E_let (LB_aux (LB_val (P_aux (paux, annot), exp1), annot), exp2) in
 
   let alg = { id_exp_alg with e_let = e_let; e_var = e_var } in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewrite_exp = (fun _ exp -> fold_exp alg (propagate_exp_effect exp))
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
     ; rewrite_fun = rewrite_fun
     ; rewrite_def = rewrite_def
-    ; rewrite_defs = rewrite_defs_base
+    ; rewrite_ast = rewrite_ast_base
     }
 
 
@@ -2626,7 +2626,7 @@ let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot anno
 
 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) }
+  rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) }
 
 
 let stringappend_counter = ref 0
@@ -2862,7 +2862,7 @@ let construct_toplevel_string_append_func env f_id pat =
   let new_fun_def, env = Type_check.check_fundef env new_fun_def in
   List.flatten [new_val_spec; new_fun_def]
 
-let rewrite_defs_toplevel_string_append env (Defs defs) =
+let rewrite_ast_toplevel_string_append env (Defs defs) =
   let new_defs = ref ([] : tannot def list) in
   let rec rewrite_pexp (Pat_aux (pexp_aux, pexp_annot) as pexp) =
     (* merge cases of Pat_exp and Pat_when *)
@@ -2899,7 +2899,7 @@ let rewrite_defs_toplevel_string_append env (Defs defs) =
   Defs (List.map rewrite defs |> List.flatten)
 
 
-let rec rewrite_defs_pat_string_append env =
+let rec rewrite_ast_pat_string_append env =
   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
@@ -3147,7 +3147,7 @@ let fresh_mappingpatterns_id () =
   mappingpatterns_counter := !mappingpatterns_counter + 1;
   id
 
-let rewrite_defs_mapping_patterns env =
+let rewrite_ast_mapping_patterns env =
   let rec rewrite_pat env (pat, guards, expr) =
     let guards_ref = ref guards in
     let expr_ref = ref expr in
@@ -3302,7 +3302,7 @@ let rewrite_lit_ocaml (L_aux (lit, _)) = match lit with
   | L_num _ | L_string _ | L_hex _ | L_bin _ | L_real _ | L_unit -> false
   | _ -> true
 
-let rewrite_defs_pat_lits rewrite_lit env ast =
+let rewrite_ast_pat_lits rewrite_lit env ast =
   let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) =
     let guards = ref [] in
     let counter = ref 0 in
@@ -3352,7 +3352,7 @@ let rewrite_defs_pat_lits rewrite_lit env ast =
   in
 
   let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in
-  let Defs defs = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in
+  let Defs defs = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast in
   Defs (List.map rewrite_def defs)
 
 
@@ -3403,7 +3403,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
        let typ' = typ_of exp in
        add_e_cast (env_of exp) typ' (E_aux (expaux, swaptyp typ' annot))
     | _ ->
-       (* after rewrite_defs_letbind_effects there cannot be terms that have
+       (* after rewrite_ast_letbind_effects there cannot be terms that have
           effects/update local variables in "tail-position": check n_exp_term
           and where it is used. *)
        if overwrite then
@@ -3525,7 +3525,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
        else
          let e1 = rewrite_var_updates (add_vars overwrite e1 vars) in
          let e2 = rewrite_var_updates (add_vars overwrite e2 vars) in
-         (* after rewrite_defs_letbind_effects c has no variable updates *)
+         (* after rewrite_ast_letbind_effects c has no variable updates *)
          let env = env_of_annot annot in
          let typ = typ_of e1 in
          let eff = union_eff_exps [c;e1;e2] in
@@ -3534,7 +3534,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
     | E_case (e1,ps) | E_try (e1, ps) ->
        let is_case = match expaux with E_case _ -> true | _ -> false in
        let vars, varpats =
-         (* for E_case, e1 needs no rewriting after rewrite_defs_letbind_effects *)
+         (* for E_case, e1 needs no rewriting after rewrite_ast_letbind_effects *)
          ((if is_case then [] else [e1]) @
          List.map (fun (Pat_aux ((Pat_exp (_,e)|Pat_when (_,_,e)),_)) -> e) ps)
          |> List.map find_updated_vars
@@ -3601,7 +3601,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
             Same_vars (E_aux (E_cast (typ, exp'), annot))
        end
     | _ ->
-       (* after rewrite_defs_letbind_effects this expression is pure and updates
+       (* after rewrite_ast_letbind_effects this expression is pure and updates
        no variables: check n_exp_term and where it's used. *)
        Same_vars (E_aux (expaux,annot))  in
 
@@ -3673,7 +3673,7 @@ let remove_reference_types exp =
 
 
 
-let rewrite_defs_remove_superfluous_letbinds env =
+let rewrite_ast_remove_superfluous_letbinds env =
 
   let e_aux (exp,annot) = match exp with
     | E_let (LB_aux (LB_val (pat, exp1), _), exp2)
@@ -3708,18 +3708,18 @@ let rewrite_defs_remove_superfluous_letbinds env =
     | _ -> E_aux (exp,annot) in
 
   let alg = { id_exp_alg with e_aux = e_aux } in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewrite_exp = (fun _ -> fold_exp alg)
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
     ; rewrite_fun = rewrite_fun
     ; rewrite_def = rewrite_def
-    ; rewrite_defs = rewrite_defs_base
+    ; rewrite_ast = rewrite_ast_base
     }
 
 (* FIXME: We shouldn't allow nested not-patterns *)
-let rewrite_defs_not_pats env =
+let rewrite_ast_not_pats env =
   let rewrite_pexp (pexp_aux, annot) =
     let rewrite_pexp' pat exp orig_guard =
       let guards = ref [] in
@@ -3766,9 +3766,9 @@ let rewrite_defs_not_pats env =
        rewrite_pexp' pat exp (Some (strip_exp guard))
   in
   let rw_exp = { id_exp_alg with pat_aux = rewrite_pexp } in
-  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) }
+  rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) }
 
-let rewrite_defs_remove_superfluous_returns env =
+let rewrite_ast_remove_superfluous_returns env =
 
   let add_opt_cast typopt1 typopt2 annot exp =
     match typopt1, typopt2 with
@@ -3810,18 +3810,18 @@ let rewrite_defs_remove_superfluous_returns env =
     | _ -> E_aux (exp,annot) in
 
   let alg = { id_exp_alg with e_aux = e_aux } in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewrite_exp = (fun _ -> fold_exp alg)
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
     ; rewrite_fun = rewrite_fun
     ; rewrite_def = rewrite_def
-    ; rewrite_defs = rewrite_defs_base
+    ; rewrite_ast = rewrite_ast_base
     }
 
 
-let rewrite_defs_remove_e_assign env (Defs defs) =
+let rewrite_ast_remove_e_assign env (Defs defs) =
   let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs
     [("foreach#", "forall ('vars_in 'vars_out : Type). (int, int, int, bool, 'vars_in, 'vars_out) -> 'vars_out");
      ("while#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out");
@@ -3830,14 +3830,14 @@ let rewrite_defs_remove_e_assign env (Defs defs) =
      ("until#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out")]))) in
  let rewrite_exp _ e =
     replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewrite_exp = rewrite_exp
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
     ; rewrite_fun = rewrite_fun
     ; rewrite_def = rewrite_def
-    ; rewrite_defs = rewrite_defs_base
+    ; rewrite_ast = rewrite_ast_base
     } (Defs (loop_specs @ defs))
 
 let merge_funcls env (Defs defs) =
@@ -3899,7 +3899,7 @@ and pat_of_mpat (MP_aux (mpat, annot)) =
   | MP_typ (mpat, typ)              -> P_aux (P_typ (typ, pat_of_mpat mpat), annot)
   | MP_as (mpat, id)                -> P_aux (P_as (pat_of_mpat mpat, id), annot)
 
-let rewrite_defs_realise_mappings _ (Defs defs) =
+let rewrite_ast_realise_mappings _ (Defs defs) =
   let realise_mpexps forwards mpexp1 mpexp2 =
     let mpexp_pat, mpexp_exp =
       if forwards then mpexp1, mpexp2
@@ -4112,7 +4112,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
                 []
       end
     in
-    let has_def id = IdSet.mem id (ids_of_defs (Defs defs)) in
+    let has_def id = IdSet.mem id (ids_of_ast (Defs defs)) in
 
     (if has_def forwards_id then [] else forwards_fun)
     @ (if has_def backwards_id then [] else backwards_fun)
@@ -4483,14 +4483,14 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
 
 let rewrite env =
   let alg = { id_exp_alg with e_aux = rewrite_case } in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewrite_exp = (fun _ -> fold_exp alg)
     ; rewrite_pat = rewrite_pat
     ; rewrite_let = rewrite_let
     ; rewrite_lexp = rewrite_lexp
     ; rewrite_fun = rewrite_fun
     ; rewrite_def = rewrite_def
-    ; rewrite_defs = rewrite_defs_base
+    ; rewrite_ast = rewrite_ast_base
     }
 
 
@@ -4722,7 +4722,7 @@ let rewrite_loops_with_escape_effect env defs =
        in E_aux (E_loop (l,m,guard,body),ann)
     | _ -> exp
   in
-  rewrite_defs_base { rewriters_base with rewrite_exp } defs
+  rewrite_ast_base { rewriters_base with rewrite_exp } defs
 
 let recheck_defs env defs = Type_error.check initial_env defs
 let recheck_defs_without_effects env defs =
@@ -4853,7 +4853,7 @@ let rewrite_truncate_hex_literals _type_env defs =
        E_aux (E_lit (L_aux (L_bin truncation, l_ann)), annot)
     | _ -> E_aux (e, annot)
   in
-  rewrite_defs_base
+  rewrite_ast_base
     { rewriters_base with
       rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_aux = rewrite_aux }) }
     defs
@@ -4910,8 +4910,8 @@ let if_flag_env flag f env defs =
   if !flag then f env defs else defs, env
 
 type rewriter =
-  | Basic_rewriter of (Env.t -> tannot defs -> tannot defs)
-  | Checking_rewriter of (Env.t -> tannot defs -> tannot defs * Env.t)
+  | Basic_rewriter of (Env.t -> tannot ast -> tannot ast)
+  | Checking_rewriter of (Env.t -> tannot ast -> tannot ast * Env.t)
   | Bool_rewriter of (bool -> rewriter)
   | String_rewriter of (string -> rewriter)
   | Literal_rewriter of ((lit -> bool) -> rewriter)
@@ -4957,11 +4957,11 @@ let all_rewrites = [
     ("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);
+    ("realise_mappings", Basic_rewriter rewrite_ast_realise_mappings);
     ("remove_duplicate_valspecs", Basic_rewriter remove_duplicate_valspecs);
-    ("toplevel_string_append", Basic_rewriter rewrite_defs_toplevel_string_append);
-    ("pat_string_append", Basic_rewriter rewrite_defs_pat_string_append);
-    ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns);
+    ("toplevel_string_append", Basic_rewriter rewrite_ast_toplevel_string_append);
+    ("pat_string_append", Basic_rewriter rewrite_ast_pat_string_append);
+    ("mapping_builtins", Basic_rewriter rewrite_ast_mapping_patterns);
     ("truncate_hex_literals", Basic_rewriter rewrite_truncate_hex_literals);
     ("mono_rewrites", Basic_rewriter mono_rewrites);
     ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps);
@@ -4970,31 +4970,31 @@ let all_rewrites = [
     ("atoms_to_singletons", String_rewriter (fun target -> (Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons target))));
     ("add_bitvector_casts", Basic_rewriter Monomorphise.add_bitvector_casts);
     ("remove_impossible_int_cases", Basic_rewriter Constant_propagation.remove_impossible_int_cases);
-    ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_defs target)));
+    ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_ast 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);
-    ("remove_not_pats", Basic_rewriter rewrite_defs_not_pats);
-    ("pattern_literals", Literal_rewriter (fun f -> Basic_rewriter (rewrite_defs_pat_lits f)));
+    ("vector_string_pats_to_bit_list", Basic_rewriter rewrite_ast_vector_string_pats_to_bit_list);
+    ("remove_not_pats", Basic_rewriter rewrite_ast_not_pats);
+    ("pattern_literals", Literal_rewriter (fun f -> Basic_rewriter (rewrite_ast_pat_lits f)));
     ("vector_concat_assignments", Basic_rewriter rewrite_vector_concat_assignments);
     ("tuple_assignments", Basic_rewriter rewrite_tuple_assignments);
     ("simple_assignments", Basic_rewriter (rewrite_simple_assignments false));
     ("simple_struct_assignments", Basic_rewriter (rewrite_simple_assignments true));
-    ("remove_vector_concat", Basic_rewriter rewrite_defs_remove_vector_concat);
-    ("remove_bitvector_pats", Basic_rewriter rewrite_defs_remove_bitvector_pats);
-    ("remove_numeral_pats", Basic_rewriter rewrite_defs_remove_numeral_pats);
-    ("guarded_pats", Basic_rewriter rewrite_defs_guarded_pats);
+    ("remove_vector_concat", Basic_rewriter rewrite_ast_remove_vector_concat);
+    ("remove_bitvector_pats", Basic_rewriter rewrite_ast_remove_bitvector_pats);
+    ("remove_numeral_pats", Basic_rewriter rewrite_ast_remove_numeral_pats);
+    ("guarded_pats", Basic_rewriter rewrite_ast_guarded_pats);
     ("bit_lists_to_lits", Basic_rewriter rewrite_bit_lists_to_lits);
-    ("exp_lift_assign", Basic_rewriter rewrite_defs_exp_lift_assign);
-    ("early_return", Basic_rewriter rewrite_defs_early_return);
-    ("nexp_ids", Basic_rewriter rewrite_defs_nexp_ids);
+    ("exp_lift_assign", Basic_rewriter rewrite_ast_exp_lift_assign);
+    ("early_return", Basic_rewriter rewrite_ast_early_return);
+    ("nexp_ids", Basic_rewriter rewrite_ast_nexp_ids);
     ("fix_val_specs", Basic_rewriter rewrite_fix_val_specs);
-    ("remove_blocks", Basic_rewriter rewrite_defs_remove_blocks);
-    ("letbind_effects", Basic_rewriter rewrite_defs_letbind_effects);
-    ("remove_e_assign", Basic_rewriter rewrite_defs_remove_e_assign);
-    ("internal_lets", Basic_rewriter rewrite_defs_internal_lets);
-    ("remove_superfluous_letbinds", Basic_rewriter rewrite_defs_remove_superfluous_letbinds);
-    ("remove_superfluous_returns", Basic_rewriter rewrite_defs_remove_superfluous_returns);
+    ("remove_blocks", Basic_rewriter rewrite_ast_remove_blocks);
+    ("letbind_effects", Basic_rewriter rewrite_ast_letbind_effects);
+    ("remove_e_assign", Basic_rewriter rewrite_ast_remove_e_assign);
+    ("internal_lets", Basic_rewriter rewrite_ast_internal_lets);
+    ("remove_superfluous_letbinds", Basic_rewriter rewrite_ast_remove_superfluous_letbinds);
+    ("remove_superfluous_returns", Basic_rewriter rewrite_ast_remove_superfluous_returns);
     ("merge_function_clauses", Basic_rewriter merge_funcls);
     ("minimise_recursive_functions", Basic_rewriter minimise_recursive_functions);
     ("move_termination_measures", Basic_rewriter move_termination_measures);
@@ -5084,7 +5084,7 @@ let rewrites_coq = [
     ("minimise_recursive_functions", []);
     ("recheck_defs", []);
     ("exp_lift_assign", []);
-    (* ("remove_assert", rewrite_defs_remove_assert); *)
+    (* ("remove_assert", rewrite_ast_remove_assert); *)
     ("move_termination_measures", []);
     ("top_sort_defs", []);
     ("early_return", []);
@@ -5189,7 +5189,7 @@ let rewrites_target tgt =
   | _ ->
      raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Invalid target for rewriting: " ^ tgt))
 
-let rewrite_defs_target tgt =
+let rewrite_ast_target tgt =
   List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) (rewrites_target tgt)
 
 let rewrite_check_annot =
@@ -5216,9 +5216,9 @@ let rewrite_check_annot =
   let rewrite_exp = { id_exp_alg with
     e_aux = (fun (exp, annot) -> check_annot (E_aux (exp, annot)));
     pat_alg = { id_pat_alg with p_aux = (fun (pat, annot) -> check_pat (P_aux (pat, annot))) } } in
-  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp);
+  rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp);
                                           rewrite_pat = (fun _ -> check_pat) }
 
-let rewrite_defs_check = [
+let rewrite_ast_check = [
   ("check_annotations", fun env defs -> rewrite_check_annot defs, env);
   ]
diff --git a/src/rewrites.mli b/src/rewrites.mli
index 4212993e..91a3536c 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -65,17 +65,17 @@ val opt_dmono_continue : bool ref
 val fresh_id : string -> l -> id
 
 (* Move loop termination measures into loop AST nodes *)
-val move_loop_measures : 'a defs -> 'a defs
+val move_loop_measures : 'a ast -> 'a ast
 
 (* Re-write undefined to functions created by -undefined_gen flag *)
-val rewrite_undefined : bool -> Env.t -> tannot defs -> tannot defs
+val rewrite_undefined : bool -> Env.t -> tannot ast -> tannot ast
 
 (* Perform rewrites to create an AST supported for a specific target *)
-val rewrite_defs_target : string -> (string * (Env.t -> tannot defs -> tannot defs * Env.t)) list
+val rewrite_ast_target : string -> (string * (Env.t -> tannot ast -> tannot ast * Env.t)) list
 
 type rewriter =
-  | Basic_rewriter of (Env.t -> tannot defs -> tannot defs)
-  | Checking_rewriter of (Env.t -> tannot defs -> tannot defs * Env.t)
+  | Basic_rewriter of (Env.t -> tannot ast -> tannot ast)
+  | Checking_rewriter of (Env.t -> tannot ast -> tannot ast * Env.t)
   | Bool_rewriter of (bool -> rewriter)
   | String_rewriter of (string -> rewriter)
   | Literal_rewriter of ((lit -> bool) -> rewriter)
@@ -99,6 +99,6 @@ val opt_coq_warn_nonexhaustive : bool ref
 
 (* This is a special rewriter pass that checks AST invariants without
    actually doing any re-writing *)
-val rewrite_defs_check : (string * (Env.t -> tannot defs -> tannot defs * Env.t)) list
+val rewrite_ast_check : (string * (Env.t -> tannot ast -> tannot ast * Env.t)) list
 
 val simple_typ : typ -> typ
diff --git a/src/sail.ml b/src/sail.ml
index 53a5cc5d..0e9b8e27 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -481,7 +481,7 @@ let target name out_name ast type_envs =
        else
          (l, Type_check.replace_env (Type_check.Env.set_prover None (Type_check.env_of_tannot tannot)) tannot)
      in
-     Marshal.to_string (Ast_util.map_defs_annot remove_prover ast, Type_check.Env.set_prover None type_envs) [Marshal.Compat_32]
+     Marshal.to_string (Ast_util.map_ast_annot remove_prover ast, Type_check.Env.set_prover None type_envs) [Marshal.Compat_32]
      |> Base64.encode_string
      |> output_string f;
      close_out f
diff --git a/src/slice.mli b/src/slice.mli
index 58d2cf17..ffc6f3bd 100644
--- a/src/slice.mli
+++ b/src/slice.mli
@@ -65,8 +65,8 @@ module Node : sig
   val compare : node -> node -> int
 end
 
-val graph_of_ast : Type_check.tannot defs -> Graph.Make(Node).graph
+val graph_of_ast : Type_check.tannot ast -> Graph.Make(Node).graph
 
-val dot_of_ast : out_channel -> Type_check.tannot defs -> unit
+val dot_of_ast : out_channel -> Type_check.tannot ast -> unit
 
-val filter_ast : Set.Make(Node).t -> Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs
+val filter_ast : Set.Make(Node).t -> Graph.Make(Node).graph -> Type_check.tannot ast -> Type_check.tannot ast
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index a2ed74bf..b111f6f0 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -77,7 +77,7 @@ val is_within_machine64 : typ -> nexp_range list -> triple *)
 (* produce a new ordering for defs, limiting to those listed in the list, which respects dependencies *)
 (* val restrict_defs : 'a defs -> string list -> 'a defs *)
 
-val top_sort_defs : tannot defs -> tannot defs
+val top_sort_defs : tannot ast -> tannot ast
 
 (** Return the set of mutable variables assigned to in the given AST. *)
 val assigned_vars : 'a exp -> IdSet.t
diff --git a/src/specialize.ml b/src/specialize.ml
index b703d27a..3634b7bc 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -253,8 +253,8 @@ let rec instantiations_of spec id ast =
   let rewrite_pat = { id_pat_alg with p_aux = (fun (pat, annot) -> inspect_pat (P_aux (pat, annot))) } in
   let rewrite_exp = { id_exp_alg with pat_alg = rewrite_pat;
                                       e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in
-  let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp);
-                                                  rewrite_pat = (fun _ -> fold_pat rewrite_pat)} ast in
+  let _ = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp);
+                                                 rewrite_pat = (fun _ -> fold_pat rewrite_pat)} ast in
 
   !instantiations
 
@@ -279,7 +279,7 @@ let rec rewrite_polymorphic_calls spec id ast =
   in
 
   let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in
-  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast
+  rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast
 
 let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   match typ_aux with
@@ -368,7 +368,7 @@ let instantiate_constraints instantiation ncs =
   List.map (fun c -> List.fold_left (fun c (v, a) -> constraint_subst v a c) c (KBindings.bindings instantiation)) ncs
 
 let specialize_id_valspec spec instantiations id ast =
-  match split_defs (is_valspec id) ast with
+  match split_ast (is_valspec id) ast with
   | None -> Reporting.unreachable (id_loc id) __POS__ ("Valspec " ^ string_of_id id ^ " does not exist!")
   | Some (pre_ast, vs, post_ast) ->
      let typschm, externs, is_cast, annot = match vs with
@@ -450,7 +450,7 @@ let specialize_annotations instantiation fdef =
              annot)
 
 let specialize_id_fundef instantiations id ast =
-  match split_defs (is_fundef id) ast with
+  match split_ast (is_fundef id) ast with
   | None -> ast
   | Some (pre_ast, DEF_fundef fundef, post_ast) ->
      let spec_ids = ref IdSet.empty in
@@ -511,7 +511,7 @@ let remove_unused_valspecs env ast =
   in
 
   let rewrite_exp = { id_exp_alg with e_aux = (fun (exp, annot) -> inspect_exp (E_aux (exp, annot))) } in
-  let _ = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast in
+  let _ = rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp) } ast in
 
   let unused = IdSet.filter (fun vs_id -> not (IdSet.mem vs_id !calls)) vs_ids in
 
diff --git a/src/specialize.mli b/src/specialize.mli
index ae71bfcb..0d522189 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -73,7 +73,7 @@ val int_specialization_with_externs : specialization
    argument specifies what X should be - it should be one of:
    [is_int_kopt], [is_order_kopt], or [is_typ_kopt] from [Ast_util],
    or some combination of those. *)
-val polymorphic_functions : specialization -> 'a defs -> IdSet.t
+val polymorphic_functions : specialization -> 'a ast -> IdSet.t
 
 val add_initial_calls : IdSet.t -> unit
 
@@ -82,14 +82,14 @@ val add_initial_calls : IdSet.t -> unit
    AST with [Type_check.initial_env]. The env parameter is the
    environment to return if there is no polymorphism to remove, in
    which case specialize returns the AST unmodified. *)
-val specialize : specialization -> Env.t -> tannot defs -> tannot defs * Env.t
+val specialize : specialization -> Env.t -> tannot ast -> tannot ast * Env.t
 
 (** specialize' n performs at most n specialization passes. Useful for
    int_specialization which is not guaranteed to terminate. *)
-val specialize_passes : int -> specialization -> Env.t -> tannot defs -> tannot defs * Env.t
+val specialize_passes : int -> specialization -> Env.t -> tannot ast -> tannot ast * Env.t
 
 (** return all instantiations of a function id, with the
    instantiations filtered according to the specialization. *)
-val instantiations_of : specialization -> id -> tannot defs -> typ_arg KBindings.t list
+val instantiations_of : specialization -> id -> tannot ast -> typ_arg KBindings.t list
 
 val string_of_instantiation : typ_arg KBindings.t -> string
diff --git a/src/splice.ml b/src/splice.ml
index 6198a4c7..cb3307d9 100644
--- a/src/splice.ml
+++ b/src/splice.ml
@@ -46,7 +46,7 @@ let splice ast file =
   let parsed_ast = Process_file.parse_file file |> snd in
   let repl_ast = Initial_check.process_ast ~generate:false (Parse_ast.Defs [(file, parsed_ast)]) in
   let repl_ast = Rewrites.move_loop_measures repl_ast in
-  let repl_ast = map_defs_annot (fun (l,_) -> l,Type_check.empty_tannot) repl_ast in
+  let repl_ast = map_ast_annot (fun (l,_) -> l,Type_check.empty_tannot) repl_ast in
   let repl_ids, repl_specs = scan_defs repl_ast in
   let defs1, specs_found = filter_old_ast repl_ids repl_specs ast in
   let defs2 = filter_replacements specs_found repl_ast in
diff --git a/src/state.ml b/src/state.ml
index a598be92..3491afd3 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -63,7 +63,7 @@ let opt_type_grouped_regstate = ref false
 
 let defs_of_string = ast_of_def_string
 
-let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs))
+let is_defined defs name = IdSet.mem (mk_id name) (ids_of_ast (Defs defs))
 
 let has_default_order defs =
   List.exists (function DEF_default (DT_aux (DT_order _, _)) -> true | _ -> false) defs
@@ -375,7 +375,7 @@ let register_refs_lem mwords registers =
 (* TODO Generate well-typedness predicate for register states (and events),
    asserting that all lists representing non-bit-vectors have the right length. *)
 
-let generate_isa_lemmas mwords (Defs defs : tannot defs) =
+let generate_isa_lemmas mwords (Defs defs : tannot ast) =
   let rec drop_while f = function
     | x :: xs when f x -> drop_while f xs
     | xs -> xs
diff --git a/src/type_check.ml b/src/type_check.ml
index afe24bc6..ab860a79 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -5420,7 +5420,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
      Reporting.unreachable (id_loc id) __POS__
        "Loop termination measures should have been rewritten before type checking"
 
-and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t =
+and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot ast * Env.t =
   fun n total env defs ->
   match defs with
   | [] -> Defs [], env
@@ -5430,7 +5430,7 @@ and check_defs : 'a. int -> int -> Env.t -> 'a def list -> tannot defs * Env.t =
      let Defs defs, env = check_defs (n + 1) total env defs in
      Defs (def @ defs), env
 
-and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+and check : 'a. Env.t -> 'a ast -> tannot ast * Env.t =
   fun env (Defs defs) -> let total = List.length defs in check_defs 1 total env defs
 
 and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list =
diff --git a/src/type_check.mli b/src/type_check.mli
index 9c2cd236..74ad4441 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -480,7 +480,7 @@ Some invariants that will hold of a fully checked AST are:
    check throws type_errors rather than Sail generic errors from
    Reporting. For a function that uses generic errors, use
    Type_error.check *)
-val check : Env.t -> 'a defs -> tannot defs * Env.t
+val check : Env.t -> 'a ast -> tannot ast * Env.t
 
 (** The same as [check], but exposes the intermediate type-checking
    environments so we don't have to always re-check the entire AST *)
diff --git a/src/type_error.ml b/src/type_error.ml
index 3ae06c31..4faa774a 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -186,7 +186,7 @@ let rec collapse_errors = function
        Err_because (err1, l, err2)
   | err -> err
 
-let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
+let check : 'a. Env.t -> 'a ast -> tannot ast * Env.t =
   fun env defs ->
   try Type_check.check env defs with
   | Type_error (env, l, err) ->