Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...decl

29 files changed, 463 insertions, 459 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index ab7bcb4a..279430df 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -3,7 +3,7 @@ open Types
 open Values
 open Expressions
 
-module FunDefId = IdGen ()
+module FunDeclId = IdGen ()
 
 type var = {
   index : VarId.id;  (** Unique variable identifier *)
@@ -32,7 +32,7 @@ type assumed_fun_id =
       (** `core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>` *)
 [@@deriving show, ord]
 
-type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
+type fun_id = Local of FunDeclId.id | Assumed of assumed_fun_id
 [@@deriving show, ord]
 
 type assertion = { cond : operand; expected : bool } [@@deriving show]
@@ -169,8 +169,8 @@ and switch_targets =
         concrete = true;
       }]
 
-type fun_def = {
-  def_id : FunDefId.id;
+type fun_decl = {
+  def_id : FunDeclId.id;
   name : fun_name;
   signature : fun_sig;
   arg_count : int;
diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml
index 04d3e6b0..c694d61b 100644
--- a/src/CfimAstUtils.ml
+++ b/src/CfimAstUtils.ml
@@ -16,19 +16,19 @@ let statement_has_loops (st : statement) : bool =
     false
   with Found -> true
 
-(** Check if a [fun_def] contains loops *)
-let fun_def_has_loops (fd : fun_def) : bool = statement_has_loops fd.body
+(** Check if a [fun_decl] contains loops *)
+let fun_decl_has_loops (fd : fun_decl) : bool = statement_has_loops fd.body
 
-let lookup_fun_sig (fun_id : fun_id) (fun_defs : fun_def FunDefId.Map.t) :
+let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     fun_sig =
   match fun_id with
-  | Local id -> (FunDefId.Map.find id fun_defs).signature
+  | Local id -> (FunDeclId.Map.find id fun_decls).signature
   | Assumed aid -> Assumed.get_assumed_sig aid
 
-let lookup_fun_name (fun_id : fun_id) (fun_defs : fun_def FunDefId.Map.t) :
+let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     Identifiers.fun_name =
   match fun_id with
-  | Local id -> (FunDefId.Map.find id fun_defs).name
+  | Local id -> (FunDeclId.Map.find id fun_decls).name
   | Assumed aid -> Assumed.get_assumed_name aid
 
 (** Small utility: list the transitive parents of a region var group.
@@ -64,6 +64,6 @@ let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id)
   let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in
   parents
 
-let fun_def_get_input_vars (fdef : fun_def) : var list =
+let fun_decl_get_input_vars (fdef : fun_decl) : var list =
   let locals = List.tl fdef.locals in
   Collections.List.prefix fdef.arg_count locals
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 4c7fc58b..e78b157a 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -102,7 +102,7 @@ let type_id_of_json (js : json) : (T.type_id, string) result =
   combine_error_msgs js "type_id_of_json"
     (match js with
     | `Assoc [ ("Adt", id) ] ->
-        let* id = T.TypeDefId.id_of_json id in
+        let* id = T.TypeDeclId.id_of_json id in
         Ok (T.AdtId id)
     | `String "Tuple" -> Ok T.Tuple
     | `Assoc [ ("Assumed", aty) ] ->
@@ -168,8 +168,8 @@ let variant_of_json (js : json) : (T.variant, string) result =
         Ok { T.variant_name = name; fields }
     | _ -> Error "")
 
-let type_def_kind_of_json (js : json) : (T.type_def_kind, string) result =
-  combine_error_msgs js "type_def_kind_of_json"
+let type_decl_kind_of_json (js : json) : (T.type_decl_kind, string) result =
+  combine_error_msgs js "type_decl_kind_of_json"
     (match js with
     | `Assoc [ ("Struct", fields) ] ->
         let* fields = list_of_json field_of_json fields in
@@ -194,8 +194,8 @@ let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result
   combine_error_msgs js "region_var_group_of_json"
     (list_of_json region_var_group_of_json js)
 
-let type_def_of_json (js : json) : (T.type_def, string) result =
-  combine_error_msgs js "type_def_of_json"
+let type_decl_of_json (js : json) : (T.type_decl, string) result =
+  combine_error_msgs js "type_decl_of_json"
     (match js with
     | `Assoc
         [
@@ -206,11 +206,11 @@ let type_def_of_json (js : json) : (T.type_def, string) result =
           ("regions_hierarchy", regions_hierarchy);
           ("kind", kind);
         ] ->
-        let* def_id = T.TypeDefId.id_of_json def_id in
+        let* def_id = T.TypeDeclId.id_of_json def_id in
         let* name = name_of_json name in
         let* region_params = list_of_json region_var_of_json region_params in
         let* type_params = list_of_json type_var_of_json type_params in
-        let* kind = type_def_kind_of_json kind in
+        let* kind = type_decl_kind_of_json kind in
         let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
         Ok
           {
@@ -317,7 +317,7 @@ let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
   combine_error_msgs js "field_proj_kind_of_json"
     (match js with
     | `Assoc [ ("ProjAdt", `List [ def_id; opt_variant_id ]) ] ->
-        let* def_id = T.TypeDefId.id_of_json def_id in
+        let* def_id = T.TypeDeclId.id_of_json def_id in
         let* opt_variant_id =
           option_of_json T.VariantId.id_of_json opt_variant_id
         in
@@ -423,7 +423,7 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
     | `String "AggregatedTuple" -> Ok E.AggregatedTuple
     | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ]
       ->
-        let* id = T.TypeDefId.id_of_json id in
+        let* id = T.TypeDeclId.id_of_json id in
         let* opt_variant_id =
           option_of_json T.VariantId.id_of_json opt_variant_id
         in
@@ -479,7 +479,7 @@ let fun_id_of_json (js : json) : (A.fun_id, string) result =
   combine_error_msgs js "fun_id_of_json"
     (match js with
     | `Assoc [ ("Local", id) ] ->
-        let* id = A.FunDefId.id_of_json id in
+        let* id = A.FunDeclId.id_of_json id in
         Ok (A.Local id)
     | `Assoc [ ("Assumed", fid) ] ->
         let* fid = assumed_fun_id_of_json fid in
@@ -606,8 +606,8 @@ and switch_targets_of_json (js : json) : (A.switch_targets, string) result =
         Ok (A.SwitchInt (int_ty, tgts, otherwise))
     | _ -> Error "")
 
-let fun_def_of_json (js : json) : (A.fun_def, string) result =
-  combine_error_msgs js "fun_def_of_json"
+let fun_decl_of_json (js : json) : (A.fun_decl, string) result =
+  combine_error_msgs js "fun_decl_of_json"
     (match js with
     | `Assoc
         [
@@ -618,7 +618,7 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result =
           ("locals", locals);
           ("body", body);
         ] ->
-        let* def_id = A.FunDefId.id_of_json def_id in
+        let* def_id = A.FunDeclId.id_of_json def_id in
         let* name = fun_name_of_json name in
         let* signature = fun_sig_of_json signature in
         let* arg_count = int_of_json arg_count in
@@ -642,12 +642,12 @@ let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
 let type_declaration_group_of_json (js : json) :
     (M.type_declaration_group, string) result =
   combine_error_msgs js "type_declaration_group_of_json"
-    (g_declaration_group_of_json T.TypeDefId.id_of_json js)
+    (g_declaration_group_of_json T.TypeDeclId.id_of_json js)
 
 let fun_declaration_group_of_json (js : json) :
     (M.fun_declaration_group, string) result =
   combine_error_msgs js "fun_declaration_group_of_json"
-    (g_declaration_group_of_json A.FunDefId.id_of_json js)
+    (g_declaration_group_of_json A.FunDeclId.id_of_json js)
 
 let declaration_group_of_json (js : json) : (M.declaration_group, string) result
     =
@@ -675,7 +675,7 @@ let cfim_module_of_json (js : json) : (M.cfim_module, string) result =
         let* declarations =
           list_of_json declaration_group_of_json declarations
         in
-        let* types = list_of_json type_def_of_json types in
-        let* functions = list_of_json fun_def_of_json functions in
+        let* types = list_of_json type_decl_of_json types in
+        let* functions = list_of_json fun_decl_of_json functions in
         Ok { M.name; declarations; types; functions }
     | _ -> Error "")
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 97584639..b5431f0f 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -200,13 +200,13 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) :
   }
 
 type type_context = {
-  type_defs_groups : M.type_declaration_group TypeDefId.Map.t;
-  type_defs : type_def TypeDefId.Map.t;
+  type_decls_groups : M.type_declaration_group TypeDeclId.Map.t;
+  type_decls : type_decl TypeDeclId.Map.t;
   type_infos : TypesAnalysis.type_infos;
 }
 [@@deriving show]
 
-type fun_context = { fun_defs : fun_def FunDefId.Map.t } [@@deriving show]
+type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
 
 type eval_ctx = {
   type_context : type_context;
@@ -237,12 +237,12 @@ let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder =
   lookup ctx.env
 
 (** TODO: make this more efficient with maps *)
-let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def =
-  TypeDefId.Map.find tid ctx.type_context.type_defs
+let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
+  TypeDeclId.Map.find tid ctx.type_context.type_decls
 
 (** TODO: make this more efficient with maps *)
-let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def =
-  FunDefId.Map.find fid ctx.fun_context.fun_defs
+let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
+  FunDeclId.Map.find fid ctx.fun_context.fun_decls
 
 (** Retrieve a variable's value in an environment *)
 let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
@@ -370,8 +370,8 @@ let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs =
 let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs =
   env_lookup_abs ctx.env abs_id
 
-let ctx_type_def_is_rec (ctx : eval_ctx) (id : TypeDefId.id) : bool =
-  let decl_group = TypeDefId.Map.find id ctx.type_context.type_defs_groups in
+let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
+  let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
   match decl_group with M.Rec _ -> true | M.NonRec _ -> false
 
 (** Visitor to iterate over the values in the *current* frame *)
diff --git a/src/Expressions.ml b/src/Expressions.ml
index 199184ed..a118ca67 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -2,7 +2,7 @@ open Types
 open Values
 
 type field_proj_kind =
-  | ProjAdt of TypeDefId.id * VariantId.id option
+  | ProjAdt of TypeDeclId.id * VariantId.id option
   | ProjOption of VariantId.id
       (** Option is an assumed type, coming from the standard library *)
   | ProjTuple of int
@@ -119,7 +119,7 @@ type operand =
 type aggregate_kind =
   | AggregatedTuple
   | AggregatedAdt of
-      TypeDefId.id * VariantId.id option * erased_region list * ety list
+      TypeDeclId.id * VariantId.id option * erased_region list * ety list
 [@@deriving show]
 
 (* TODO: move the aggregate kind to operands *)
diff --git a/src/ExtractAst.ml b/src/ExtractAst.ml
index da88dc04..dd793291 100644
--- a/src/ExtractAst.ml
+++ b/src/ExtractAst.ml
@@ -45,7 +45,7 @@ type term =
           Otherwise, we can use `App` (with the record constructor).
        *)
 
-type fun_def = {
+type fun_decl = {
   name : string;
   inputs : pattern list;
       (** We can match over the inputs, hence the use of [pattern]. In practice,
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index c4323090..d8d14ddf 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -13,13 +13,13 @@ module F = Format
     Controls whether we should use `type ...` or `and ...` (for mutually
     recursive datatypes).
  *)
-type type_def_qualif = Type | And
+type type_decl_qualif = Type | And
 
 (** A qualifier for function definitions.
 
     Controls whether we should use `let ...`, `let rec ...` or `and ...`
  *)
-type fun_def_qualif = Let | LetRec | And
+type fun_decl_qualif = Let | LetRec | And
 
 (** Small helper to compute the name of an int type *)
 let fstar_int_name (int_ty : integer_type) =
@@ -275,7 +275,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
     fname ^ suffix
   in
 
-  let decreases_clause_name (_fid : FunDefId.id) (fname : fun_name) : string =
+  let decreases_clause_name (_fid : FunDeclId.id) (fname : fun_name) : string =
     let fname = get_fun_name fname in
     (* Converting to snake case should be a no-op, but it doesn't cost much *)
     let fname = to_snake_case fname in
@@ -306,7 +306,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
             | Assumed State -> "st"
             | AdtId adt_id ->
                 let def =
-                  TypeDefId.Map.find adt_id ctx.type_context.type_defs
+                  TypeDeclId.Map.find adt_id ctx.type_context.type_decls
                 in
                 (* We do the following:
                  * - convert to snake_case
@@ -424,10 +424,10 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     We need to do this preemptively, beforce extracting any definition,
     because of recursive definitions.
  *)
-let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) :
+let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
     extraction_ctx =
   (* Compute and register the type def name *)
-  let ctx = ctx_add_type_def def ctx in
+  let ctx = ctx_add_type_decl def ctx in
   (* Compute and register:
    * - the variant names, if this is an enumeration
    * - the field names, if this is a structure
@@ -451,8 +451,8 @@ let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) :
   (* Return *)
   ctx
 
-let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : type_def) (fields : field list) : unit =
+let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : type_decl) (fields : field list) : unit =
   (* We want to generate a definition which looks like this:
    * ```
    * type t = { x : int; y : bool; }
@@ -509,8 +509,8 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_space fmt ();
     F.pp_print_string fmt "}")
 
-let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : type_def) (def_name : string) (type_params : string list)
+let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : type_decl) (def_name : string) (type_params : string list)
     (variants : variant list) : unit =
   (* We want to generate a definition which looks like this:
    * ```
@@ -614,8 +614,8 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
     Note that all the names used for extraction should already have been
     registered.
  *)
-let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : type_def_qualif) (def : type_def) : unit =
+let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (qualif : type_decl_qualif) (def : type_decl) : unit =
   (* Retrieve the definition name *)
   let def_name = ctx_get_local_type def.def_id ctx in
   (* Add the type params - note that we need those bindings only for the
@@ -653,9 +653,9 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
   (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *)
   F.pp_close_box fmt ();
   (match def.kind with
-  | Struct fields -> extract_type_def_struct_body ctx_body fmt def fields
+  | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields
   | Enum variants ->
-      extract_type_def_enum_body ctx_body fmt def def_name type_params variants);
+      extract_type_decl_enum_body ctx_body fmt def def_name type_params variants);
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
@@ -664,7 +664,7 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
 (** Compute the names for all the pure functions generated from a rust function
     (forward function and backward functions).
  *)
-let extract_fun_def_register_names (ctx : extraction_ctx) (keep_fwd : bool)
+let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
     (has_decreases_clause : bool) (def : pure_fun_translation) : extraction_ctx
     =
   let fwd, back_ls = def in
@@ -673,11 +673,11 @@ let extract_fun_def_register_names (ctx : extraction_ctx) (keep_fwd : bool)
     if has_decreases_clause then ctx_add_decrases_clause fwd ctx else ctx
   in
   (* Register the forward function name *)
-  let ctx = ctx_add_fun_def (keep_fwd, def) fwd ctx in
+  let ctx = ctx_add_fun_decl (keep_fwd, def) fwd ctx in
   (* Register the backward functions' names *)
   let ctx =
     List.fold_left
-      (fun ctx back -> ctx_add_fun_def (keep_fwd, def) back ctx)
+      (fun ctx back -> ctx_add_fun_decl (keep_fwd, def) back ctx)
       ctx back_ls
   in
   (* Return *)
@@ -986,7 +986,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
     - the previous context augmented with bindings for the input values
  *)
 let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : fun_def) : extraction_ctx * extraction_ctx =
+    (def : fun_decl) : extraction_ctx * extraction_ctx =
   (* Add the type parameters - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, _ = ctx_add_type_params def.signature.type_params ctx in
@@ -1045,7 +1045,7 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
     ```
  *)
 let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : fun_def) : unit =
+    (def : fun_decl) : unit =
   (* Retrieve the function name *)
   let def_name = ctx_get_decreases_clause def.def_id ctx in
   (* Add a break before *)
@@ -1097,9 +1097,9 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
     equal to the definition to extract, if we extract a forward function) because
     it is useful for the decrease clause.
  *)
-let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : fun_def_qualif) (has_decreases_clause : bool) (fwd_def : fun_def)
-    (def : fun_def) : unit =
+let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (qualif : fun_decl_qualif) (has_decreases_clause : bool) (fwd_def : fun_decl)
+    (def : fun_decl) : unit =
   (* Retrieve the function name *)
   let def_name = ctx_get_local_function def.def_id def.back_id ctx in
   (* (* Add the type parameters - note that we need those bindings only for the
@@ -1220,7 +1220,7 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
     ```
  *)
 let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : fun_def) : unit =
+    (def : fun_decl) : unit =
   (* We only insert unit tests for forward functions *)
   assert (def.back_id = None);
   (* Check if this is a unit function *)
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 91ad6843..d073c238 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -15,16 +15,16 @@ let log = L.interpreter_log
 
 let compute_type_fun_contexts (m : M.cfim_module) :
     C.type_context * C.fun_context =
-  let type_decls, _ = M.split_declarations m.declarations in
-  let type_defs, fun_defs = M.compute_defs_maps m in
-  let type_defs_groups, _funs_defs_groups =
+  let type_decls_list, _ = M.split_declarations m.declarations in
+  let type_decls, fun_decls = M.compute_defs_maps m in
+  let type_decls_groups, _funs_defs_groups =
     M.split_declarations_to_group_maps m.declarations
   in
   let type_infos =
-    TypesAnalysis.analyze_type_declarations type_defs type_decls
+    TypesAnalysis.analyze_type_declarations type_decls type_decls_list
   in
-  let type_context = { C.type_defs_groups; type_defs; type_infos } in
-  let fun_context = { C.fun_defs } in
+  let type_context = { C.type_decls_groups; type_decls; type_infos } in
+  let fun_context = { C.fun_decls } in
   (type_context, fun_context)
 
 let initialize_eval_context (type_context : C.type_context)
@@ -52,7 +52,7 @@ let initialize_eval_context (type_context : C.type_context)
       - the instantiated function signature
  *)
 let initialize_symbolic_context_for_fun (type_context : C.type_context)
-    (fun_context : C.fun_context) (fdef : A.fun_def) :
+    (fun_context : C.fun_context) (fdef : A.fun_decl) :
     C.eval_ctx * V.symbolic_value list * A.inst_fun_sig =
   (* The abstractions are not initialized the same way as for function
    * calls: they contain *loan* projectors, because they "provide" us
@@ -113,7 +113,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
     the synthesis (mostly by ending abstractions).
 *)
 let evaluate_function_symbolic_synthesize_backward_from_return
-    (config : C.config) (fdef : A.fun_def) (inst_sg : A.inst_fun_sig)
+    (config : C.config) (fdef : A.fun_decl) (inst_sg : A.inst_fun_sig)
     (back_id : T.RegionGroupId.id) (ctx : C.eval_ctx) : SA.expression option =
   (* We need to instantiate the function signature - to retrieve
    * the return type. Note that it is important to re-generate
@@ -189,7 +189,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
  *)
 let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
     (type_context : C.type_context) (fun_context : C.fun_context)
-    (fdef : A.fun_def) (back_id : T.RegionGroupId.id option) :
+    (fdef : A.fun_decl) (back_id : T.RegionGroupId.id option) :
     V.symbolic_value list * SA.expression option =
   (* Debug *)
   let name_to_string () =
@@ -252,9 +252,9 @@ module Test = struct
       environment.
    *)
   let test_unit_function (config : C.partial_config) (m : M.cfim_module)
-      (fid : A.FunDefId.id) : unit =
+      (fid : A.FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
-    let fdef = A.FunDefId.nth m.functions fid in
+    let fdef = A.FunDeclId.nth m.functions fid in
 
     (* Debug *)
     log#ldebug
@@ -291,7 +291,7 @@ module Test = struct
 
   (** Small helper: return true if the function is a unit function (no parameters,
     no arguments) - TODO: move *)
-  let fun_def_is_unit (def : A.fun_def) : bool =
+  let fun_decl_is_unit (def : A.fun_decl) : bool =
     def.A.arg_count = 0
     && List.length def.A.signature.region_params = 0
     && List.length def.A.signature.type_params = 0
@@ -300,8 +300,8 @@ module Test = struct
   (** Test all the unit functions in a list of function definitions *)
   let test_unit_functions (config : C.partial_config) (m : M.cfim_module) : unit
       =
-    let unit_funs = List.filter fun_def_is_unit m.functions in
-    let test_unit_fun (def : A.fun_def) : unit =
+    let unit_funs = List.filter fun_decl_is_unit m.functions in
+    let test_unit_fun (def : A.fun_decl) : unit =
       test_unit_function config m def.A.def_id
     in
     List.iter test_unit_fun unit_funs
@@ -309,7 +309,7 @@ module Test = struct
   (** Execute the symbolic interpreter on a function. *)
   let test_function_symbolic (config : C.partial_config) (synthesize : bool)
       (type_context : C.type_context) (fun_context : C.fun_context)
-      (fdef : A.fun_def) : unit =
+      (fdef : A.fun_decl) : unit =
     (* Debug *)
     log#ldebug
       (lazy ("test_function_symbolic: " ^ Print.fun_name_to_string fdef.A.name));
@@ -337,10 +337,10 @@ module Test = struct
   let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
       (m : M.cfim_module) : unit =
     let no_loop_funs =
-      List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) m.functions
+      List.filter (fun f -> not (CfimAstUtils.fun_decl_has_loops f)) m.functions
     in
     let type_context, fun_context = compute_type_fun_contexts m in
-    let test_fun (def : A.fun_def) : unit =
+    let test_fun (def : A.fun_decl) : unit =
       (* Execute the function - note that as the symbolic interpreter explores
        * all the path, some executions are expected to "panic": we thus don't
        * check the return value *)
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 85259b89..979ed780 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -220,16 +220,16 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
-    (kind : V.sv_kind) (def_id : T.TypeDefId.id)
+    (kind : V.sv_kind) (def_id : T.TypeDeclId.id)
     (regions : T.RegionId.id T.region list) (types : T.rty list)
     (ctx : C.eval_ctx) : V.symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
-  let def = C.ctx_lookup_type_def ctx def_id in
+  let def = C.ctx_lookup_type_decl ctx def_id in
   assert (List.length regions = List.length def.T.region_params);
   (* Retrieve, for every variant, the list of its instantiated field types *)
   let variants_fields_types =
-    Subst.type_def_get_instantiated_variants_fields_rtypes def regions types
+    Subst.type_decl_get_instantiated_variants_fields_rtypes def regions types
   in
   (* Check if there is strictly more than one variant *)
   if List.length variants_fields_types > 1 && not expand_enumerations then
@@ -677,7 +677,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
             (* [expand_symbolic_value_no_branching] checks if there are branchings,
              * but we prefer to also check it here - this leads to cleaner messages
              * and debugging *)
-            let def = C.ctx_lookup_type_def ctx def_id in
+            let def = C.ctx_lookup_type_decl ctx def_id in
             (match def.kind with
             | T.Struct _ | T.Enum ([] | [ _ ]) -> ()
             | T.Enum (_ :: _) ->
@@ -688,7 +688,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
                        [greedy_expand_symbolics_with_borrows] of [config]): "
                      ^ Print.name_to_string def.name)));
             (* Also, we need to check if the definition is recursive *)
-            if C.ctx_type_def_is_rec ctx def_id then
+            if C.ctx_type_decl_is_rec ctx def_id then
               raise
                 (Failure
                    ("Attempted to greedily expand a recursive definition \
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 9e4466b8..3043bc7a 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -89,9 +89,9 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety)
       let field_tys =
         match adt_id with
         | T.AdtId def_id ->
-            let def = C.ctx_lookup_type_def ctx def_id in
+            let def = C.ctx_lookup_type_decl ctx def_id in
             assert (def.region_params = []);
-            Subst.type_def_get_instantiated_field_etypes def variant_id
+            Subst.type_decl_get_instantiated_field_etypes def variant_id
               type_params
         | T.Tuple -> type_params
         | T.Assumed _ -> failwith "Unreachable"
@@ -601,8 +601,8 @@ let eval_rvalue_aggregate (config : C.config)
         cf aggregated ctx
     | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
         (* Sanity checks *)
-        let type_def = C.ctx_lookup_type_def ctx def_id in
-        assert (List.length type_def.region_params = List.length regions);
+        let type_decl = C.ctx_lookup_type_decl ctx def_id in
+        assert (List.length type_decl.region_params = List.length regions);
         let expected_field_types =
           Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id
             types
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index d8b1322b..826e8563 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -351,18 +351,18 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
   | Ok ctx -> ctx
 
 (** Compute an expanded ADT bottom value *)
-let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.Map.t)
-    (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
+let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
+    (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
     (regions : T.erased_region list) (types : T.ety list) : V.typed_value =
   (* Lookup the definition and check if it is an enumeration - it
      should be an enumeration if and only if the projection element
      is a field projection with *some* variant id. Retrieve the list
      of fields at the same time. *)
-  let def = T.TypeDefId.Map.find def_id tyctx in
+  let def = T.TypeDeclId.Map.find def_id tyctx in
   assert (List.length regions = List.length def.T.region_params);
   (* Compute the field types *)
   let field_types =
-    Subst.type_def_get_instantiated_field_etypes def opt_variant_id types
+    Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types
   in
   (* Initialize the expanded value *)
   let fields = List.map mk_bottom field_types in
@@ -444,7 +444,7 @@ let expand_bottom_value_from_projection (config : C.config)
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
         T.Adt (T.AdtId def_id', regions, types) ) ->
         assert (def_id = def_id');
-        compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id
+        compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id
           opt_variant_id regions types
     (* Option *)
     | Field (ProjOption variant_id, _), T.Adt (T.Assumed T.Option, [], [ ty ])
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index c3b60fa9..dc8fc7f7 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -233,7 +233,7 @@ let set_discriminant (config : C.config) (p : E.place)
               let bottom_v =
                 match type_id with
                 | T.AdtId def_id ->
-                    compute_expanded_bottom_adt_value ctx.type_context.type_defs
+                    compute_expanded_bottom_adt_value ctx.type_context.type_decls
                       def_id (Some variant_id) regions types
                 | T.Assumed T.Option ->
                     assert (regions = []);
@@ -247,7 +247,7 @@ let set_discriminant (config : C.config) (p : E.place)
         let bottom_v =
           match type_id with
           | T.AdtId def_id ->
-              compute_expanded_bottom_adt_value ctx.type_context.type_defs
+              compute_expanded_bottom_adt_value ctx.type_context.type_decls
                 def_id (Some variant_id) regions types
           | T.Assumed T.Option ->
               assert (regions = []);
@@ -997,20 +997,20 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
         call.type_params call.args call.dest
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
-and eval_local_function_call_concrete (config : C.config) (fid : A.FunDefId.id)
+and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
     (region_params : T.erased_region list) (type_params : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
   assert (region_params = []);
 
   (* Retrieve the (correctly instantiated) body *)
-  let def = C.ctx_lookup_fun_def ctx fid in
+  let def = C.ctx_lookup_fun_decl ctx fid in
   let tsubst =
     Subst.make_type_subst
       (List.map (fun v -> v.T.index) def.A.signature.type_params)
       type_params
   in
-  let locals, body = Subst.fun_def_substitute_in_body tsubst def in
+  let locals, body = Subst.fun_decl_substitute_in_body tsubst def in
 
   (* Evaluate the input operands *)
   assert (List.length args = def.A.arg_count);
@@ -1063,12 +1063,12 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDefId.id)
   cc cf ctx
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
-and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDefId.id)
+and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
     (region_params : T.erased_region list) (type_params : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
   (* Retrieve the (correctly instantiated) signature *)
-  let def = C.ctx_lookup_fun_def ctx fid in
+  let def = C.ctx_lookup_fun_decl ctx fid in
   let sg = def.A.signature in
   (* Instantiate the signature and introduce fresh abstraction and region ids
    * while doing so *)
@@ -1239,7 +1239,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
 
 (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
     [eval_statement]) *)
-and eval_local_function_call (config : C.config) (fid : A.FunDefId.id)
+and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
     (region_params : T.erased_region list) (type_params : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
   match config.mode with
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 0e4b1e23..78d7cb8d 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -410,7 +410,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.Adt av, T.Adt (T.AdtId def_id, regions, tys) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
-            let def = C.ctx_lookup_type_def ctx def_id in
+            let def = C.ctx_lookup_type_decl ctx def_id in
             (* Check the number of parameters *)
             assert (List.length regions = List.length def.region_params);
             assert (List.length tys = List.length def.type_params);
@@ -422,7 +422,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             | _ -> failwith "Erroneous typing");
             (* Check that the field types are correct *)
             let field_types =
-              Subst.type_def_get_instantiated_field_etypes def av.V.variant_id
+              Subst.type_decl_get_instantiated_field_etypes def av.V.variant_id
                 tys
             in
             let fields_with_types =
@@ -509,7 +509,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) ->
             (* Retrieve the definition to check the variant id, the number of
              * parameters, etc. *)
-            let def = C.ctx_lookup_type_def ctx def_id in
+            let def = C.ctx_lookup_type_decl ctx def_id in
             (* Check the number of parameters *)
             assert (List.length regions = List.length def.region_params);
             assert (List.length tys = List.length def.type_params);
@@ -521,7 +521,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             | _ -> failwith "Erroneous typing");
             (* Check that the field types are correct *)
             let field_types =
-              Subst.type_def_get_instantiated_field_rtypes def av.V.variant_id
+              Subst.type_decl_get_instantiated_field_rtypes def av.V.variant_id
                 regions tys
             in
             let fields_with_types =
diff --git a/src/Modules.ml b/src/Modules.ml
index 1199d74a..3ee4c9ed 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -4,9 +4,10 @@ open CfimAst
 type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
 [@@deriving show]
 
-type type_declaration_group = TypeDefId.id g_declaration_group [@@deriving show]
+type type_declaration_group = TypeDeclId.id g_declaration_group
+[@@deriving show]
 
-type fun_declaration_group = FunDefId.id g_declaration_group [@@deriving show]
+type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
 
 (** Module declaration *)
 type declaration_group =
@@ -17,22 +18,22 @@ type declaration_group =
 type cfim_module = {
   name : string;
   declarations : declaration_group list;
-  types : type_def list;
-  functions : fun_def list;
+  types : type_decl list;
+  functions : fun_decl list;
 }
-(** CFIM module *)
+(** LLBC module - TODO: rename to crate *)
 
 let compute_defs_maps (m : cfim_module) :
-    type_def TypeDefId.Map.t * fun_def FunDefId.Map.t =
+    type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t =
   let types_map =
     List.fold_left
-      (fun m (def : type_def) -> TypeDefId.Map.add def.def_id def m)
-      TypeDefId.Map.empty m.types
+      (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
+      TypeDeclId.Map.empty m.types
   in
   let funs_map =
     List.fold_left
-      (fun m (def : fun_def) -> FunDefId.Map.add def.def_id def m)
-      FunDefId.Map.empty m.functions
+      (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
+      FunDeclId.Map.empty m.functions
   in
   (types_map, funs_map)
 
@@ -54,8 +55,8 @@ let split_declarations (decls : declaration_group list) :
     declaration groups.
  *)
 let split_declarations_to_group_maps (decls : declaration_group list) :
-    type_declaration_group TypeDefId.Map.t
-    * fun_declaration_group FunDefId.Map.t =
+    type_declaration_group TypeDeclId.Map.t
+    * fun_declaration_group FunDeclId.Map.t =
   let module G (M : Map.S) = struct
     let add_group (map : M.key g_declaration_group M.t)
         (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
@@ -68,8 +69,8 @@ let split_declarations_to_group_maps (decls : declaration_group list) :
       List.fold_left add_group M.empty groups
   end in
   let types, funs = split_declarations decls in
-  let module TG = G (TypeDefId.Map) in
+  let module TG = G (TypeDeclId.Map) in
   let types = TG.create_map types in
-  let module FG = G (FunDefId.Map) in
+  let module FG = G (FunDeclId.Map) in
   let funs = FG.create_map funs in
   (types, funs)
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index e9d2dad1..925b82aa 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -24,7 +24,7 @@ let log = L.pre_passes_log
     ```
 
  *)
-let filter_drop_assigns (f : A.fun_def) : A.fun_def =
+let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
   (* The visitor *)
   let obj =
     object (self)
diff --git a/src/Print.ml b/src/Print.ml
index e64e7d73..64351e3e 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -48,7 +48,7 @@ module Types = struct
   type 'r type_formatter = {
     r_to_string : 'r -> string;
     type_var_id_to_string : T.TypeVarId.id -> string;
-    type_def_id_to_string : T.TypeDefId.id -> string;
+    type_decl_id_to_string : T.TypeDeclId.id -> string;
   }
 
   type stype_formatter = T.RegionVarId.id T.region type_formatter
@@ -73,7 +73,7 @@ module Types = struct
 
   let type_id_to_string (fmt : 'r type_formatter) (id : T.type_id) : string =
     match id with
-    | T.AdtId id -> fmt.type_def_id_to_string id
+    | T.AdtId id -> fmt.type_decl_id_to_string id
     | T.Tuple -> ""
     | T.Assumed aty -> (
         match aty with
@@ -130,8 +130,8 @@ module Types = struct
     ^ String.concat ", " (List.map (field_to_string fmt) v.fields)
     ^ ")"
 
-  let type_def_to_string (type_def_id_to_string : T.TypeDefId.id -> string)
-      (def : T.type_def) : string =
+  let type_decl_to_string (type_decl_id_to_string : T.TypeDeclId.id -> string)
+      (def : T.type_decl) : string =
     let regions = def.region_params in
     let types = def.type_params in
     let rid_to_string rid =
@@ -145,7 +145,7 @@ module Types = struct
       | Some tv -> type_var_to_string tv
       | None -> failwith "Unreachable"
     in
-    let fmt = { r_to_string; type_var_id_to_string; type_def_id_to_string } in
+    let fmt = { r_to_string; type_var_id_to_string; type_decl_id_to_string } in
     let name = name_to_string def.name in
     let params =
       if List.length regions + List.length types > 0 then
@@ -180,32 +180,32 @@ module Values = struct
     rvar_to_string : T.RegionVarId.id -> string;
     r_to_string : T.RegionId.id -> string;
     type_var_id_to_string : T.TypeVarId.id -> string;
-    type_def_id_to_string : T.TypeDefId.id -> string;
-    adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
+    type_decl_id_to_string : T.TypeDeclId.id -> string;
+    adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string;
     var_id_to_string : V.VarId.id -> string;
     adt_field_names :
-      T.TypeDefId.id -> T.VariantId.id option -> string list option;
+      T.TypeDeclId.id -> T.VariantId.id option -> string list option;
   }
 
   let value_to_etype_formatter (fmt : value_formatter) : PT.etype_formatter =
     {
       PT.r_to_string = PT.erased_region_to_string;
       PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
     }
 
   let value_to_rtype_formatter (fmt : value_formatter) : PT.rtype_formatter =
     {
       PT.r_to_string = PT.region_to_string fmt.r_to_string;
       PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
     }
 
   let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter =
     {
       PT.r_to_string = PT.region_to_string fmt.rvar_to_string;
       PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
     }
 
   let var_id_to_string (id : V.VarId.id) : string =
@@ -260,7 +260,7 @@ module Values = struct
             let adt_ident =
               match av.variant_id with
               | Some vid -> fmt.adt_variant_to_string def_id vid
-              | None -> fmt.type_def_id_to_string def_id
+              | None -> fmt.type_decl_id_to_string def_id
             in
             if List.length field_values > 0 then
               match fmt.adt_field_names def_id av.V.variant_id with
@@ -372,7 +372,7 @@ module Values = struct
             let adt_ident =
               match av.variant_id with
               | Some vid -> fmt.adt_variant_to_string def_id vid
-              | None -> fmt.type_def_id_to_string def_id
+              | None -> fmt.type_decl_id_to_string def_id
             in
             if List.length field_values > 0 then
               match fmt.adt_field_names def_id av.V.variant_id with
@@ -565,21 +565,22 @@ module Contexts = struct
   let ctx_to_rtype_formatter (fmt : ctx_formatter) : PT.rtype_formatter =
     PV.value_to_rtype_formatter fmt
 
-  let type_ctx_to_adt_variant_to_string_fun (ctx : T.type_def T.TypeDefId.Map.t)
-      : T.TypeDefId.id -> T.VariantId.id -> string =
+  let type_ctx_to_adt_variant_to_string_fun
+      (ctx : T.type_decl T.TypeDeclId.Map.t) :
+      T.TypeDeclId.id -> T.VariantId.id -> string =
    fun def_id variant_id ->
-    let def = T.TypeDefId.Map.find def_id ctx in
+    let def = T.TypeDeclId.Map.find def_id ctx in
     match def.kind with
     | Struct _ -> failwith "Unreachable"
     | Enum variants ->
         let variant = T.VariantId.nth variants variant_id in
         name_to_string def.name ^ "::" ^ variant.variant_name
 
-  let type_ctx_to_adt_field_names_fun (ctx : T.type_def T.TypeDefId.Map.t) :
-      T.TypeDefId.id -> T.VariantId.id option -> string list option =
+  let type_ctx_to_adt_field_names_fun (ctx : T.type_decl T.TypeDeclId.Map.t) :
+      T.TypeDeclId.id -> T.VariantId.id option -> string list option =
    fun def_id opt_variant_id ->
-    let def = T.TypeDefId.Map.find def_id ctx in
-    let fields = TU.type_def_get_fields def opt_variant_id in
+    let def = T.TypeDeclId.Map.find def_id ctx in
+    let fields = TU.type_decl_get_fields def opt_variant_id in
     (* There are two cases: either all the fields have names, or none of them
      * has names *)
     let has_names =
@@ -599,25 +600,25 @@ module Contexts = struct
       let v = C.lookup_type_var ctx vid in
       v.name
     in
-    let type_def_id_to_string def_id =
-      let def = C.ctx_lookup_type_def ctx def_id in
+    let type_decl_id_to_string def_id =
+      let def = C.ctx_lookup_type_decl ctx def_id in
       name_to_string def.name
     in
     let adt_variant_to_string =
-      type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs
+      type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls
     in
     let var_id_to_string vid =
       let bv = C.ctx_lookup_binder ctx vid in
       binder_to_string bv
     in
     let adt_field_names =
-      type_ctx_to_adt_field_names_fun ctx.type_context.type_defs
+      type_ctx_to_adt_field_names_fun ctx.type_context.type_decls
     in
     {
       rvar_to_string;
       r_to_string;
       type_var_id_to_string;
-      type_def_id_to_string;
+      type_decl_id_to_string;
       adt_variant_to_string;
       var_id_to_string;
       adt_field_names;
@@ -683,14 +684,14 @@ module CfimAst = struct
     rvar_to_string : T.RegionVarId.id -> string;
     r_to_string : T.RegionId.id -> string;
     type_var_id_to_string : T.TypeVarId.id -> string;
-    type_def_id_to_string : T.TypeDefId.id -> string;
-    adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
+    type_decl_id_to_string : T.TypeDeclId.id -> string;
+    adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string;
     adt_field_to_string :
-      T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string option;
+      T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option;
     var_id_to_string : V.VarId.id -> string;
     adt_field_names :
-      T.TypeDefId.id -> T.VariantId.id option -> string list option;
-    fun_def_id_to_string : A.FunDefId.id -> string;
+      T.TypeDeclId.id -> T.VariantId.id option -> string list option;
+    fun_decl_id_to_string : A.FunDeclId.id -> string;
   }
 
   let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
@@ -698,7 +699,7 @@ module CfimAst = struct
       PV.rvar_to_string = fmt.rvar_to_string;
       PV.r_to_string = fmt.r_to_string;
       PV.type_var_id_to_string = fmt.type_var_id_to_string;
-      PV.type_def_id_to_string = fmt.type_def_id_to_string;
+      PV.type_decl_id_to_string = fmt.type_decl_id_to_string;
       PV.adt_variant_to_string = fmt.adt_variant_to_string;
       PV.var_id_to_string = fmt.var_id_to_string;
       PV.adt_field_names = fmt.adt_field_names;
@@ -711,55 +712,57 @@ module CfimAst = struct
     {
       PT.r_to_string = PT.erased_region_to_string;
       PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
     }
 
   let ast_to_rtype_formatter (fmt : ast_formatter) : PT.rtype_formatter =
     {
       PT.r_to_string = PT.region_to_string fmt.r_to_string;
       PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
     }
 
   let ast_to_stype_formatter (fmt : ast_formatter) : PT.stype_formatter =
     {
       PT.r_to_string = PT.region_to_string fmt.rvar_to_string;
       PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
     }
 
-  let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def T.TypeDefId.Map.t) :
-      T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string option =
+  let type_ctx_to_adt_field_to_string_fun (ctx : T.type_decl T.TypeDeclId.Map.t)
+      :
+      T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option
+      =
    fun def_id opt_variant_id field_id ->
-    let def = T.TypeDefId.Map.find def_id ctx in
-    let fields = TU.type_def_get_fields def opt_variant_id in
+    let def = T.TypeDeclId.Map.find def_id ctx in
+    let fields = TU.type_decl_get_fields def opt_variant_id in
     let field = T.FieldId.nth fields field_id in
     field.T.field_name
 
   let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : ast_formatter =
     let ctx_fmt = PC.eval_ctx_to_ctx_formatter ctx in
     let adt_field_to_string =
-      type_ctx_to_adt_field_to_string_fun ctx.type_context.type_defs
+      type_ctx_to_adt_field_to_string_fun ctx.type_context.type_decls
     in
-    let fun_def_id_to_string def_id =
-      let def = C.ctx_lookup_fun_def ctx def_id in
+    let fun_decl_id_to_string def_id =
+      let def = C.ctx_lookup_fun_decl ctx def_id in
       fun_name_to_string def.name
     in
     {
       rvar_to_string = ctx_fmt.PV.rvar_to_string;
       r_to_string = ctx_fmt.PV.r_to_string;
       type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string;
-      type_def_id_to_string = ctx_fmt.PV.type_def_id_to_string;
+      type_decl_id_to_string = ctx_fmt.PV.type_decl_id_to_string;
       adt_variant_to_string = ctx_fmt.PV.adt_variant_to_string;
       var_id_to_string = ctx_fmt.PV.var_id_to_string;
       adt_field_names = ctx_fmt.PV.adt_field_names;
       adt_field_to_string;
-      fun_def_id_to_string;
+      fun_decl_id_to_string;
     }
 
-  let fun_def_to_ast_formatter (type_defs : T.type_def T.TypeDefId.Map.t)
-      (fun_defs : A.fun_def A.FunDefId.Map.t) (fdef : A.fun_def) : ast_formatter
-      =
+  let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t)
+      (fun_decls : A.fun_decl A.FunDeclId.Map.t) (fdef : A.fun_decl) :
+      ast_formatter =
     let rvar_to_string r =
       let rvar = T.RegionVarId.nth fdef.signature.region_params r in
       PT.region_var_to_string rvar
@@ -770,33 +773,33 @@ module CfimAst = struct
       let var = T.TypeVarId.nth fdef.signature.type_params vid in
       PT.type_var_to_string var
     in
-    let type_def_id_to_string def_id =
-      let def = T.TypeDefId.Map.find def_id type_defs in
+    let type_decl_id_to_string def_id =
+      let def = T.TypeDeclId.Map.find def_id type_decls in
       name_to_string def.name
     in
     let adt_variant_to_string =
-      PC.type_ctx_to_adt_variant_to_string_fun type_defs
+      PC.type_ctx_to_adt_variant_to_string_fun type_decls
     in
     let var_id_to_string vid =
       let var = V.VarId.nth fdef.locals vid in
       var_to_string var
     in
-    let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_defs in
-    let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_defs in
-    let fun_def_id_to_string def_id =
-      let def = A.FunDefId.Map.find def_id fun_defs in
+    let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in
+    let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in
+    let fun_decl_id_to_string def_id =
+      let def = A.FunDeclId.Map.find def_id fun_decls in
       fun_name_to_string def.name
     in
     {
       rvar_to_string;
       r_to_string;
       type_var_id_to_string;
-      type_def_id_to_string;
+      type_decl_id_to_string;
       adt_variant_to_string;
       var_id_to_string;
       adt_field_names;
       adt_field_to_string;
-      fun_def_id_to_string;
+      fun_decl_id_to_string;
     }
 
   let rec projection_to_string (fmt : ast_formatter) (inside : string)
@@ -907,7 +910,7 @@ module CfimAst = struct
         match akind with
         | E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")"
         | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) ->
-            let adt_name = fmt.type_def_id_to_string def_id in
+            let adt_name = fmt.type_decl_id_to_string def_id in
             let variant_name =
               match opt_variant_id with
               | None -> adt_name
@@ -959,7 +962,7 @@ module CfimAst = struct
         let args = "(" ^ String.concat ", " args ^ ")" in
         let name_params =
           match call.A.func with
-          | A.Local fid -> fmt.fun_def_id_to_string fid ^ params
+          | A.Local fid -> fmt.fun_decl_id_to_string fid ^ params
           | A.Assumed fid -> (
               match fid with
               | A.Replace -> "core::mem::replace" ^ params
@@ -1034,8 +1037,8 @@ module CfimAst = struct
   let var_to_string (v : A.var) : string =
     match v.name with None -> PV.var_id_to_string v.index | Some name -> name
 
-  let fun_def_to_string (fmt : ast_formatter) (indent : string)
-      (indent_incr : string) (def : A.fun_def) : string =
+  let fun_decl_to_string (fmt : ast_formatter) (indent : string)
+      (indent_incr : string) (def : A.fun_decl) : string =
     let sty_fmt = ast_to_stype_formatter fmt in
     let sty_to_string = PT.sty_to_string sty_fmt in
     let ety_fmt = ast_to_etype_formatter fmt in
@@ -1099,18 +1102,18 @@ module PA = CfimAst (* local module *)
 module Module = struct
   (** This function pretty-prints a type definition by using a definition
       context *)
-  let type_def_to_string (type_context : T.type_def T.TypeDefId.Map.t)
-      (def : T.type_def) : string =
-    let type_def_id_to_string (id : T.TypeDefId.id) : string =
-      let def = T.TypeDefId.Map.find id type_context in
+  let type_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
+      (def : T.type_decl) : string =
+    let type_decl_id_to_string (id : T.TypeDeclId.id) : string =
+      let def = T.TypeDeclId.Map.find id type_context in
       name_to_string def.name
     in
-    PT.type_def_to_string type_def_id_to_string def
+    PT.type_decl_to_string type_decl_id_to_string def
 
   (** Generate an [ast_formatter] by using a definition context in combination
       with the variables local to a function's definition *)
-  let def_ctx_to_ast_formatter (type_context : T.type_def T.TypeDefId.Map.t)
-      (fun_context : A.fun_def A.FunDefId.Map.t) (def : A.fun_def) :
+  let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t)
+      (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) :
       PA.ast_formatter =
     let rvar_to_string vid =
       let var = T.RegionVarId.nth def.signature.region_params vid in
@@ -1124,12 +1127,12 @@ module Module = struct
       let var = T.TypeVarId.nth def.signature.type_params vid in
       PT.type_var_to_string var
     in
-    let type_def_id_to_string def_id =
-      let def = T.TypeDefId.Map.find def_id type_context in
+    let type_decl_id_to_string def_id =
+      let def = T.TypeDeclId.Map.find def_id type_context in
       name_to_string def.name
     in
-    let fun_def_id_to_string def_id =
-      let def = A.FunDefId.Map.find def_id fun_context in
+    let fun_decl_id_to_string def_id =
+      let def = A.FunDeclId.Map.find def_id fun_context in
       fun_name_to_string def.name
     in
     let var_id_to_string vid =
@@ -1147,34 +1150,34 @@ module Module = struct
       rvar_to_string;
       r_to_string;
       type_var_id_to_string;
-      type_def_id_to_string;
+      type_decl_id_to_string;
       adt_variant_to_string;
       adt_field_to_string;
       var_id_to_string;
       adt_field_names;
-      fun_def_id_to_string;
+      fun_decl_id_to_string;
     }
 
   (** This function pretty-prints a function definition by using a definition
       context *)
-  let fun_def_to_string (type_context : T.type_def T.TypeDefId.Map.t)
-      (fun_context : A.fun_def A.FunDefId.Map.t) (def : A.fun_def) : string =
+  let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
+      (fun_context : A.fun_decl A.FunDeclId.Map.t) (def : A.fun_decl) : string =
     let fmt = def_ctx_to_ast_formatter type_context fun_context def in
-    PA.fun_def_to_string fmt "" "  " def
+    PA.fun_decl_to_string fmt "" "  " def
 
   let module_to_string (m : M.cfim_module) : string =
     let types_defs_map, funs_defs_map = M.compute_defs_maps m in
 
     (* The types *)
-    let type_defs = List.map (type_def_to_string types_defs_map) m.M.types in
+    let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in
 
     (* The functions *)
-    let fun_defs =
-      List.map (fun_def_to_string types_defs_map funs_defs_map) m.M.functions
+    let fun_decls =
+      List.map (fun_decl_to_string types_defs_map funs_defs_map) m.M.functions
     in
 
     (* Put everything together *)
-    let all_defs = List.append type_defs fun_defs in
+    let all_defs = List.append type_decls fun_decls in
     String.concat "\n\n" all_defs
 end
 
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index c1da7610..e96edeed 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -5,31 +5,31 @@ module T = Types
 module V = Values
 module E = Expressions
 module A = CfimAst
-module TypeDefId = T.TypeDefId
+module TypeDeclId = T.TypeDeclId
 module TypeVarId = T.TypeVarId
 module RegionId = T.RegionId
 module VariantId = T.VariantId
 module FieldId = T.FieldId
 module SymbolicValueId = V.SymbolicValueId
-module FunDefId = A.FunDefId
+module FunDeclId = A.FunDeclId
 
 type type_formatter = {
   type_var_id_to_string : TypeVarId.id -> string;
-  type_def_id_to_string : TypeDefId.id -> string;
+  type_decl_id_to_string : TypeDeclId.id -> string;
 }
 
 type value_formatter = {
   type_var_id_to_string : TypeVarId.id -> string;
-  type_def_id_to_string : TypeDefId.id -> string;
-  adt_variant_to_string : TypeDefId.id -> VariantId.id -> string;
+  type_decl_id_to_string : TypeDeclId.id -> string;
+  adt_variant_to_string : TypeDeclId.id -> VariantId.id -> string;
   var_id_to_string : VarId.id -> string;
-  adt_field_names : TypeDefId.id -> VariantId.id option -> string list option;
+  adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
 }
 
 let value_to_type_formatter (fmt : value_formatter) : type_formatter =
   {
     type_var_id_to_string = fmt.type_var_id_to_string;
-    type_def_id_to_string = fmt.type_def_id_to_string;
+    type_decl_id_to_string = fmt.type_decl_id_to_string;
   }
 
 (* TODO: we need to store which variables we have encountered so far, and
@@ -37,19 +37,19 @@ let value_to_type_formatter (fmt : value_formatter) : type_formatter =
 *)
 type ast_formatter = {
   type_var_id_to_string : TypeVarId.id -> string;
-  type_def_id_to_string : TypeDefId.id -> string;
-  adt_variant_to_string : TypeDefId.id -> VariantId.id -> string;
+  type_decl_id_to_string : TypeDeclId.id -> string;
+  adt_variant_to_string : TypeDeclId.id -> VariantId.id -> string;
   var_id_to_string : VarId.id -> string;
   adt_field_to_string :
-    TypeDefId.id -> VariantId.id option -> FieldId.id -> string option;
-  adt_field_names : TypeDefId.id -> VariantId.id option -> string list option;
-  fun_def_id_to_string : A.FunDefId.id -> string;
+    TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option;
+  adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
+  fun_decl_id_to_string : A.FunDeclId.id -> string;
 }
 
 let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
   {
     type_var_id_to_string = fmt.type_var_id_to_string;
-    type_def_id_to_string = fmt.type_def_id_to_string;
+    type_decl_id_to_string = fmt.type_decl_id_to_string;
     adt_variant_to_string = fmt.adt_variant_to_string;
     var_id_to_string = fmt.var_id_to_string;
     adt_field_names = fmt.adt_field_names;
@@ -71,65 +71,65 @@ let integer_type_to_string = Print.Types.integer_type_to_string
 
 let scalar_value_to_string = Print.Values.scalar_value_to_string
 
-let mk_type_formatter (type_defs : T.type_def TypeDefId.Map.t)
+let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
     (type_params : type_var list) : type_formatter =
   let type_var_id_to_string vid =
     let var = T.TypeVarId.nth type_params vid in
     type_var_to_string var
   in
-  let type_def_id_to_string def_id =
-    let def = T.TypeDefId.Map.find def_id type_defs in
+  let type_decl_id_to_string def_id =
+    let def = T.TypeDeclId.Map.find def_id type_decls in
     name_to_string def.name
   in
-  { type_var_id_to_string; type_def_id_to_string }
+  { type_var_id_to_string; type_decl_id_to_string }
 
-(* TODO: there is a bit of duplication with Print.fun_def_to_ast_formatter.
+(* TODO: there is a bit of duplication with Print.fun_decl_to_ast_formatter.
 
    TODO: use the pure defs as inputs? Note that it is a bit annoying for the
    functions (there is a difference between the forward/backward functions...)
    while we only need those definitions to lookup proper names for the def ids.
 *)
-let mk_ast_formatter (type_defs : T.type_def TypeDefId.Map.t)
-    (fun_defs : A.fun_def FunDefId.Map.t) (type_params : type_var list) :
+let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
+    (fun_decls : A.fun_decl FunDeclId.Map.t) (type_params : type_var list) :
     ast_formatter =
   let type_var_id_to_string vid =
     let var = T.TypeVarId.nth type_params vid in
     type_var_to_string var
   in
-  let type_def_id_to_string def_id =
-    let def = T.TypeDefId.Map.find def_id type_defs in
+  let type_decl_id_to_string def_id =
+    let def = T.TypeDeclId.Map.find def_id type_decls in
     name_to_string def.name
   in
   let adt_variant_to_string =
-    Print.Contexts.type_ctx_to_adt_variant_to_string_fun type_defs
+    Print.Contexts.type_ctx_to_adt_variant_to_string_fun type_decls
   in
   let var_id_to_string vid =
     (* TODO: somehow lookup in the context *)
     "^" ^ VarId.to_string vid
   in
   let adt_field_names =
-    Print.Contexts.type_ctx_to_adt_field_names_fun type_defs
+    Print.Contexts.type_ctx_to_adt_field_names_fun type_decls
   in
   let adt_field_to_string =
-    Print.CfimAst.type_ctx_to_adt_field_to_string_fun type_defs
+    Print.CfimAst.type_ctx_to_adt_field_to_string_fun type_decls
   in
-  let fun_def_id_to_string def_id =
-    let def = A.FunDefId.Map.find def_id fun_defs in
+  let fun_decl_id_to_string def_id =
+    let def = A.FunDeclId.Map.find def_id fun_decls in
     fun_name_to_string def.name
   in
   {
     type_var_id_to_string;
-    type_def_id_to_string;
+    type_decl_id_to_string;
     adt_variant_to_string;
     var_id_to_string;
     adt_field_names;
     adt_field_to_string;
-    fun_def_id_to_string;
+    fun_decl_id_to_string;
   }
 
 let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
   match id with
-  | AdtId id -> fmt.type_def_id_to_string id
+  | AdtId id -> fmt.type_decl_id_to_string id
   | Tuple -> ""
   | Assumed aty -> (
       match aty with
@@ -167,7 +167,7 @@ let variant_to_string fmt (v : variant) : string =
   ^ String.concat ", " (List.map (field_to_string fmt) v.fields)
   ^ ")"
 
-let type_def_to_string (fmt : type_formatter) (def : type_def) : string =
+let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string =
   let types = def.type_params in
   let name = name_to_string def.name in
   let params =
@@ -245,7 +245,7 @@ let adt_g_value_to_string (fmt : value_formatter)
       let adt_ident =
         match variant_id with
         | Some vid -> fmt.adt_variant_to_string def_id vid
-        | None -> fmt.type_def_id_to_string def_id
+        | None -> fmt.type_decl_id_to_string def_id
       in
       if field_values <> [] then
         match fmt.adt_field_names def_id variant_id with
@@ -358,7 +358,7 @@ let inst_fun_sig_to_string (fmt : ast_formatter) (sg : inst_fun_sig) : string =
 let regular_fun_id_to_string (fmt : ast_formatter) (fun_id : A.fun_id) : string
     =
   match fun_id with
-  | A.Local fid -> fmt.fun_def_id_to_string fid
+  | A.Local fid -> fmt.fun_decl_id_to_string fid
   | A.Assumed fid -> (
       match fid with
       | A.Replace -> "core::mem::replace"
@@ -474,7 +474,7 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
       let branches = List.map branch_to_string branches in
       "match " ^ scrut ^ " with\n" ^ String.concat "\n" branches
 
-let fun_def_to_string (fmt : ast_formatter) (def : fun_def) : string =
+let fun_decl_to_string (fmt : ast_formatter) (def : fun_decl) : string =
   let type_fmt = ast_to_type_formatter fmt in
   let name = fun_name_to_string def.basename ^ fun_suffix def.back_id in
   let signature = fun_sig_to_string fmt def.signature in
diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml
index 25b39e2e..1679aa6c 100644
--- a/src/PrintSymbolicAst.ml
+++ b/src/PrintSymbolicAst.ml
@@ -20,7 +20,7 @@ module PT = Print.Types
 
 type formatting_ctx = {
   type_context : C.type_context;
-  fun_context : A.fun_def A.FunDefId.Map.t;
+  fun_context : A.fun_decl A.FunDeclId.Map.t;
   type_vars : T.type_var list;
 }
 
@@ -35,24 +35,24 @@ let formatting_ctx_to_formatter (ctx : formatting_ctx) : formatter =
     let v = T.TypeVarId.nth ctx.type_vars vid in
     v.name
   in
-  let type_def_id_to_string def_id =
-    let def = T.TypeDefId.Map.find def_id ctx.type_context.type_defs in
+  let type_decl_id_to_string def_id =
+    let def = T.TypeDeclId.Map.find def_id ctx.type_context.type_decls in
     P.name_to_string def.name
   in
   let adt_variant_to_string =
-    P.Contexts.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs
+    P.Contexts.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls
   in
   (* We shouldn't use [var_id_to_string] *)
   let var_id_to_string _ = failwith "Unexpected use of var_id_to_string" in
 
   let adt_field_names =
-    P.Contexts.type_ctx_to_adt_field_names_fun ctx.type_context.type_defs
+    P.Contexts.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls
   in
   {
     rvar_to_string;
     r_to_string;
     type_var_id_to_string;
-    type_def_id_to_string;
+    type_decl_id_to_string;
     adt_variant_to_string;
     var_id_to_string;
     adt_field_names;
diff --git a/src/Pure.ml b/src/Pure.ml
index 0f4280c3..b1c8e254 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -3,13 +3,13 @@ module T = Types
 module V = Values
 module E = Expressions
 module A = CfimAst
-module TypeDefId = T.TypeDefId
+module TypeDeclId = T.TypeDeclId
 module TypeVarId = T.TypeVarId
 module RegionGroupId = T.RegionGroupId
 module VariantId = T.VariantId
 module FieldId = T.FieldId
 module SymbolicValueId = V.SymbolicValueId
-module FunDefId = A.FunDefId
+module FunDeclId = A.FunDeclId
 
 module SynthPhaseId = IdGen ()
 (** We give an identifier to every phase of the synthesis (forward, backward
@@ -45,7 +45,7 @@ let option_some_id = T.option_some_id
 
 let option_none_id = T.option_none_id
 
-type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty
+type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
 [@@deriving show, ord]
 
 (** Ancestor for iter visitor for [ty] *)
@@ -115,16 +115,16 @@ type field = { field_name : string option; field_ty : ty } [@@deriving show]
 
 type variant = { variant_name : string; fields : field list } [@@deriving show]
 
-type type_def_kind = Struct of field list | Enum of variant list
+type type_decl_kind = Struct of field list | Enum of variant list
 [@@deriving show]
 
 type type_var = T.type_var [@@deriving show]
 
-type type_def = {
-  def_id : TypeDefId.id;
+type type_decl = {
+  def_id : TypeDeclId.id;
   name : name;
   type_params : type_var list;
-  kind : type_def_kind;
+  kind : type_decl_kind;
 }
 [@@deriving show]
 
@@ -595,8 +595,8 @@ type fun_sig = {
 
 type inst_fun_sig = { inputs : ty list; outputs : ty list }
 
-type fun_def = {
-  def_id : FunDefId.id;
+type fun_decl = {
+  def_id : FunDeclId.id;
   back_id : T.RegionGroupId.id option;
   basename : fun_name;
       (** The "base" name of the function.
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index f45c59bb..c1cacac5 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -157,7 +157,7 @@ type pn_ctx = string VarId.Map.t
       ```
    - TODO: inputs and end abstraction...
  *)
-let compute_pretty_names (def : fun_def) : fun_def =
+let compute_pretty_names (def : fun_decl) : fun_decl =
   (* Small helpers *)
   (* 
    * When we do branchings, we need to merge (the constraints saved in) the
@@ -322,7 +322,7 @@ let compute_pretty_names (def : fun_def) : fun_def =
   { def with body }
 
 (** Remove the meta-information *)
-let remove_meta (def : fun_def) : fun_def =
+let remove_meta (def : fun_decl) : fun_decl =
   let obj =
     object
       inherit [_] map_expression as super
@@ -360,7 +360,7 @@ let remove_meta (def : fun_def) : fun_def =
     pass (if they are useless).
  *)
 let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
-    (def : fun_def) : fun_def =
+    (def : fun_decl) : fun_decl =
   let obj =
     object (self)
       inherit [_] map_expression as super
@@ -504,7 +504,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (call0 : call)
                   (* We need to use the regions hierarchy *)
                   (* First, lookup the signature of the CFIM function *)
                   let sg =
-                    CfimAstUtils.lookup_fun_sig id0 ctx.fun_context.fun_defs
+                    CfimAstUtils.lookup_fun_sig id0 ctx.fun_context.fun_decls
                   in
                   (* Compute the set of ancestors of the function in call1 *)
                   let call1_ancestors =
@@ -585,7 +585,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (call0 : call)
 (** Filter the useless assignments (removes the useless variables, filters
     the function calls) *)
 let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
-    (def : fun_def) : fun_def =
+    (def : fun_decl) : fun_decl =
   (* We first need a transformation on *left-values*, which filters the useless
    * variables and tells us whether the value contains any variable which has
    * not been replaced by `_` (in which case we need to keep the assignment,
@@ -707,8 +707,8 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
     symbolic to pure. Here, we remove the definitions altogether, because they
     are now useless
   *)
-let filter_if_backward_with_no_outputs (config : config) (def : fun_def) :
-    fun_def option =
+let filter_if_backward_with_no_outputs (config : config) (def : fun_decl) :
+    fun_decl option =
   if
     config.filter_useless_functions && Option.is_some def.back_id
     && def.signature.outputs = []
@@ -745,7 +745,7 @@ let keep_forward (config : config) (trans : pure_fun_translation) : bool =
 (** Add unit arguments (optionally) to functions with no arguments, and
     change their output type to use `result`
   *)
-let to_monadic (config : config) (def : fun_def) : fun_def =
+let to_monadic (config : config) (def : fun_decl) : fun_decl =
   (* Update the body *)
   let obj =
     object
@@ -812,7 +812,7 @@ let to_monadic (config : config) (def : fun_def) : fun_def =
 
 (** Convert the unit variables to `()` if they are used as right-values or
     `_` if they are used as left values in patterns. *)
-let unit_vars_to_unit (def : fun_def) : fun_def =
+let unit_vars_to_unit (def : fun_decl) : fun_decl =
   (* The map visitor *)
   let obj =
     object
@@ -846,7 +846,7 @@ let unit_vars_to_unit (def : fun_def) : fun_def =
     function calls, and when translating end abstractions. Here, we can do
     something simpler, in one micro-pass.
  *)
-let eliminate_box_functions (_ctx : trans_ctx) (def : fun_def) : fun_def =
+let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
   (* The map visitor *)
   let obj =
     object
@@ -894,7 +894,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_def) : fun_def =
 
     See the explanations in [config].
  *)
-let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_def) : fun_def
+let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl
     =
   (* Set up the var id generator *)
   let cnt = get_expression_min_var_counter def.body.e in
@@ -937,7 +937,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_def) : fun_def
 
 (** Unfold the monadic let-bindings to explicit matches. *)
 let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
-    (def : fun_def) : fun_def =
+    (def : fun_decl) : fun_decl =
   (* We may need to introduce fresh variables for the state *)
   let var_cnt = get_expression_min_var_counter def.body.e in
   let _, fresh_var_id = VarId.mk_stateful_generator var_cnt in
@@ -1066,8 +1066,8 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
 
     [ctx]: used only for printing.
  *)
-let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
-    fun_def option =
+let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
+    fun_decl option =
   (* Debug *)
   log#ldebug
     (lazy
@@ -1080,7 +1080,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
   (* First, find names for the variables which are unnamed *)
   let def = compute_pretty_names def in
   log#ldebug
-    (lazy ("compute_pretty_name:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
+    (lazy ("compute_pretty_name:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
   (* TODO: we might want to leverage more the assignment meta-data, for
    * aggregates for instance. *)
@@ -1091,7 +1091,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
    * Rk.: some passes below use the fact that we removed the meta-data
    * (otherwise we would have to "unmeta" expressions before matching) *)
   let def = remove_meta def in
-  log#ldebug (lazy ("remove_meta:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
+  log#ldebug (lazy ("remove_meta:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
   (* Remove the backward functions with no outputs.
    * Note that the calls to those functions should already have been removed,
@@ -1108,13 +1108,13 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
        * TODO: this is not true with the state-error monad, unless we unfold the monadic binds.
        * Also, from now onwards, the outputs list has length 1. *)
       let def = to_monadic config def in
-      log#ldebug (lazy ("to_monadic:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
+      log#ldebug (lazy ("to_monadic:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
       (* Convert the unit variables to `()` if they are used as right-values or
        * `_` if they are used as left values. *)
       let def = unit_vars_to_unit def in
       log#ldebug
-        (lazy ("unit_vars_to_unit:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
+        (lazy ("unit_vars_to_unit:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
       (* Inline the useless variable reassignments *)
       let inline_named_vars = true in
@@ -1124,7 +1124,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
       in
       log#ldebug
         (lazy
-          ("inline_useless_var_assignments:\n\n" ^ fun_def_to_string ctx def
+          ("inline_useless_var_assignments:\n\n" ^ fun_decl_to_string ctx def
          ^ "\n"));
 
       (* Eliminate the box functions - note that the "box" types were eliminated
@@ -1132,12 +1132,12 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
       let def = eliminate_box_functions ctx def in
       log#ldebug
         (lazy
-          ("eliminate_box_functions:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
+          ("eliminate_box_functions:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
       (* Filter the useless variables, assignments, function calls, etc. *)
       let def = filter_useless config.filter_useless_monadic_calls ctx def in
       log#ldebug
-        (lazy ("filter_useless:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
+        (lazy ("filter_useless:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
       (* Decompose the monadic let-bindings - F* specific
        * TODO: remove? With the state-error monad, it is becoming completely
@@ -1149,7 +1149,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
           let def = decompose_monadic_let_bindings ctx def in
           log#ldebug
             (lazy
-              ("decompose_monadic_let_bindings:\n\n" ^ fun_def_to_string ctx def
+              ("decompose_monadic_let_bindings:\n\n" ^ fun_decl_to_string ctx def
              ^ "\n"));
           def)
         else (
@@ -1165,7 +1165,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
           let def = unfold_monadic_let_bindings config ctx def in
           log#ldebug
             (lazy
-              ("unfold_monadic_let_bindings:\n\n" ^ fun_def_to_string ctx def
+              ("unfold_monadic_let_bindings:\n\n" ^ fun_decl_to_string ctx def
              ^ "\n"));
           def)
         else (
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index ba638743..2c8a5a28 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -92,7 +92,7 @@ type formatter = {
             (`None` if forward function)
           TODO: use the fun id for the assumed functions.
        *)
-  decreases_clause_name : FunDefId.id -> fun_name -> string;
+  decreases_clause_name : FunDeclId.id -> fun_name -> string;
       (** Generates the name of the definition used to prove/reason about
           termination. The generated code uses this clause where needed,
           but its body must be defined by the user.
@@ -340,13 +340,13 @@ type extraction_ctx = {
 
 (** Debugging function *)
 let id_to_string (id : id) (ctx : extraction_ctx) : string =
-  let fun_defs = ctx.trans_ctx.fun_context.fun_defs in
-  let type_defs = ctx.trans_ctx.type_context.type_defs in
+  let fun_decls = ctx.trans_ctx.fun_context.fun_decls in
+  let type_decls = ctx.trans_ctx.type_context.type_decls in
   (* TODO: factorize the pretty-printing with what is in PrintPure *)
   let get_type_name (id : type_id) : string =
     match id with
     | AdtId id ->
-        let def = TypeDefId.Map.find id type_defs in
+        let def = TypeDeclId.Map.find id type_decls in
         Print.name_to_string def.name
     | Assumed aty -> show_assumed_ty aty
     | Tuple -> failwith "Unreachable"
@@ -356,7 +356,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       let fun_name =
         match fid with
         | A.Local fid ->
-            Print.fun_name_to_string (FunDefId.Map.find fid fun_defs).name
+            Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name
         | A.Assumed aid -> A.show_assumed_fun_id aid
       in
       let fun_kind =
@@ -369,7 +369,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       let fun_name =
         match fid with
         | A.Local fid ->
-            Print.fun_name_to_string (FunDefId.Map.find fid fun_defs).name
+            Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name
         | A.Assumed aid -> A.show_assumed_fun_id aid
       in
       "decreases clause for function: " ^ fun_name
@@ -390,7 +390,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
             else failwith "Unreachable"
         | Assumed Vec -> failwith "Unreachable"
         | AdtId id -> (
-            let def = TypeDefId.Map.find id type_defs in
+            let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
             | Struct _ -> failwith "Unreachable"
             | Enum variants ->
@@ -407,7 +407,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
             (* We can't directly have access to the fields of a vector *)
             failwith "Unreachable"
         | AdtId id -> (
-            let def = TypeDefId.Map.find id type_defs in
+            let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
             | Enum _ -> failwith "Unreachable"
             | Struct fields ->
@@ -444,7 +444,7 @@ let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get (FunId (id, rg)) ctx
 
-let ctx_get_local_function (id : FunDefId.id) (rg : RegionGroupId.id option)
+let ctx_get_local_function (id : FunDeclId.id) (rg : RegionGroupId.id option)
     (ctx : extraction_ctx) : string =
   ctx_get_function (A.Local id) rg ctx
 
@@ -452,7 +452,7 @@ let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
   assert (id <> Tuple);
   ctx_get (TypeId id) ctx
 
-let ctx_get_local_type (id : TypeDefId.id) (ctx : extraction_ctx) : string =
+let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
   ctx_get_type (AdtId id) ctx
 
 let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string =
@@ -475,7 +475,7 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
     (ctx : extraction_ctx) : string =
   ctx_get (VariantId (def_id, variant_id)) ctx
 
-let ctx_get_decreases_clause (def_id : FunDefId.id) (ctx : extraction_ctx) :
+let ctx_get_decreases_clause (def_id : FunDeclId.id) (ctx : extraction_ctx) :
     string =
   ctx_get (DecreasesClauseId (A.Local def_id)) ctx
 
@@ -520,57 +520,57 @@ let ctx_add_type_params (vars : type_var list) (ctx : extraction_ctx) :
     (fun ctx (var : type_var) -> ctx_add_type_var var.name var.index ctx)
     ctx vars
 
-let ctx_add_type_def_struct (def : type_def) (ctx : extraction_ctx) :
+let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) :
     extraction_ctx * string =
   let cons_name = ctx.fmt.struct_constructor def.name in
   let ctx = ctx_add (StructId (AdtId def.def_id)) cons_name ctx in
   (ctx, cons_name)
 
-let ctx_add_type_def (def : type_def) (ctx : extraction_ctx) : extraction_ctx =
+let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx =
   let def_name = ctx.fmt.type_name def.name in
   let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
   ctx
 
-let ctx_add_field (def : type_def) (field_id : FieldId.id) (field : field)
+let ctx_add_field (def : type_decl) (field_id : FieldId.id) (field : field)
     (ctx : extraction_ctx) : extraction_ctx * string =
   let name = ctx.fmt.field_name def.name field_id field.field_name in
   let ctx = ctx_add (FieldId (AdtId def.def_id, field_id)) name ctx in
   (ctx, name)
 
-let ctx_add_fields (def : type_def) (fields : (FieldId.id * field) list)
+let ctx_add_fields (def : type_decl) (fields : (FieldId.id * field) list)
     (ctx : extraction_ctx) : extraction_ctx * string list =
   List.fold_left_map
     (fun ctx (vid, v) -> ctx_add_field def vid v ctx)
     ctx fields
 
-let ctx_add_variant (def : type_def) (variant_id : VariantId.id)
+let ctx_add_variant (def : type_decl) (variant_id : VariantId.id)
     (variant : variant) (ctx : extraction_ctx) : extraction_ctx * string =
   let name = ctx.fmt.variant_name def.name variant.variant_name in
   let ctx = ctx_add (VariantId (AdtId def.def_id, variant_id)) name ctx in
   (ctx, name)
 
-let ctx_add_variants (def : type_def) (variants : (VariantId.id * variant) list)
+let ctx_add_variants (def : type_decl) (variants : (VariantId.id * variant) list)
     (ctx : extraction_ctx) : extraction_ctx * string list =
   List.fold_left_map
     (fun ctx (vid, v) -> ctx_add_variant def vid v ctx)
     ctx variants
 
-let ctx_add_struct (def : type_def) (ctx : extraction_ctx) :
+let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
     extraction_ctx * string =
   let name = ctx.fmt.struct_constructor def.name in
   let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in
   (ctx, name)
 
-let ctx_add_decrases_clause (def : fun_def) (ctx : extraction_ctx) :
+let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name = ctx.fmt.decreases_clause_name def.def_id def.basename in
   ctx_add (DecreasesClauseId (A.Local def.def_id)) name ctx
 
-let ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def)
+let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (def : fun_decl)
     (ctx : extraction_ctx) : extraction_ctx =
   (* Lookup the CFIM def to compute the region group information *)
   let def_id = def.def_id in
-  let cfim_def = FunDefId.Map.find def_id ctx.trans_ctx.fun_context.fun_defs in
+  let cfim_def = FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls in
   let sg = cfim_def.signature in
   let num_rgs = List.length sg.regions_hierarchy in
   let keep_fwd, (_, backs) = trans_group in
@@ -655,7 +655,7 @@ let initialize_names_map (init : names_map_init) : names_map =
   (* Return *)
   nm
 
-let compute_type_def_name (fmt : formatter) (def : type_def) : string =
+let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
   fmt.type_name def.name
 
 (** A helper function: generates a function suffix from a region group
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 26dc6294..aa8d1f53 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -101,7 +101,7 @@ let ty_as_integer (t : ty) : T.integer_type =
   match t with Integer int_ty -> int_ty | _ -> raise (Failure "Unreachable")
 
 (* TODO: move *)
-let type_def_is_enum (def : T.type_def) : bool =
+let type_decl_is_enum (def : T.type_decl) : bool =
   match def.kind with T.Struct _ -> false | Enum _ -> true
 
 let mk_state_ty : ty = Adt (Assumed State, [])
@@ -182,11 +182,11 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
   in
   fun id -> TypeVarId.Map.find id mp
 
-(** Retrieve the list of fields for the given variant of a [type_def].
+(** Retrieve the list of fields for the given variant of a [type_decl].
 
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
-let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
+let type_decl_get_fields (def : type_decl) (opt_variant_id : VariantId.id option)
     : field list =
   match (def.kind, opt_variant_id) with
   | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
@@ -199,15 +199,15 @@ let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
         (Invalid_argument
            ("The variant id should be [Some] if and only if the definition is \
              an enumeration:\n\
-             - def: " ^ show_type_def def ^ "\n- opt_variant_id: "
+             - def: " ^ show_type_decl def ^ "\n- opt_variant_id: "
           ^ opt_variant_id))
 
 (** Instantiate the type variables for the chosen variant in an ADT definition,
     and return the list of the types of its fields *)
-let type_def_get_instantiated_fields_types (def : type_def)
+let type_decl_get_instantiated_fields_types (def : type_decl)
     (opt_variant_id : VariantId.id option) (types : ty list) : ty list =
   let ty_subst = make_type_subst def.type_params types in
-  let fields = type_def_get_fields def opt_variant_id in
+  let fields = type_decl_get_fields def opt_variant_id in
   List.map (fun f -> ty_substitute ty_subst f.field_ty) fields
 
 let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) :
@@ -225,17 +225,17 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) :
     - if all functions only call functions we already explored, they are not
       mutually recursive
  *)
-let functions_not_mutually_recursive (funs : fun_def list) : bool =
+let functions_not_mutually_recursive (funs : fun_decl list) : bool =
   (* Compute the set of function identifiers in the group *)
   let ids =
     FunIdSet.of_list
       (List.map
-         (fun (f : fun_def) -> Regular (A.Local f.def_id, f.back_id))
+         (fun (f : fun_decl) -> Regular (A.Local f.def_id, f.back_id))
          funs)
   in
   let ids = ref ids in
   (* Explore every body *)
-  let body_only_calls_itself (fdef : fun_def) : bool =
+  let body_only_calls_itself (fdef : fun_decl) : bool =
     (* Remove the current id from the id set *)
     ids := FunIdSet.remove (Regular (A.Local fdef.def_id, fdef.back_id)) !ids;
 
@@ -271,7 +271,7 @@ let rec expression_requires_parentheses (e : texpression) : bool =
 
 (** Module to perform type checking - we use this for sanity checks only *)
 module TypeCheck = struct
-  type tc_ctx = { type_defs : type_def TypeDefId.Map.t }
+  type tc_ctx = { type_decls : type_decl TypeDeclId.Map.t }
 
   let check_constant_value (ty : ty) (v : constant_value) : unit =
     match (ty, v) with
@@ -290,8 +290,8 @@ module TypeCheck = struct
           tys
       | Adt (AdtId def_id, tys) ->
           (* "Regular" ADT *)
-          let def = TypeDefId.Map.find def_id ctx.type_defs in
-          type_def_get_instantiated_fields_types def variant_id tys
+          let def = TypeDeclId.Map.find def_id ctx.type_decls in
+          type_decl_get_instantiated_fields_types def variant_id tys
       | Adt (Assumed aty, tys) -> (
           (* Assumed type *)
           match aty with
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 62822785..4a1f42eb 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -102,7 +102,7 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
 
 (** Instantiate the type variables in an ADT definition, and return, for
     every variant, the list of the types of its fields *)
-let type_def_get_instantiated_variants_fields_rtypes (def : T.type_def)
+let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
     (regions : T.RegionId.id T.region list) (types : T.rty list) :
     (T.VariantId.id option * T.rty list) list =
   let r_subst =
@@ -130,7 +130,7 @@ let type_def_get_instantiated_variants_fields_rtypes (def : T.type_def)
 
 (** Instantiate the type variables in an ADT definition, and return the list
     of types of the fields for the chosen variant *)
-let type_def_get_instantiated_field_rtypes (def : T.type_def)
+let type_decl_get_instantiated_field_rtypes (def : T.type_decl)
     (opt_variant_id : T.VariantId.id option)
     (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list =
   let r_subst =
@@ -141,16 +141,16 @@ let type_def_get_instantiated_field_rtypes (def : T.type_def)
   let ty_subst =
     make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
   in
-  let fields = TU.type_def_get_fields def opt_variant_id in
+  let fields = TU.type_decl_get_fields def opt_variant_id in
   List.map (fun f -> ty_substitute r_subst ty_subst f.T.field_ty) fields
 
 (** Return the types of the properly instantiated ADT's variant, provided a
     context *)
 let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx)
-    (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
+    (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
     (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list =
-  let def = C.ctx_lookup_type_def ctx def_id in
-  type_def_get_instantiated_field_rtypes def opt_variant_id regions types
+  let def = C.ctx_lookup_type_decl ctx def_id in
+  type_decl_get_instantiated_field_rtypes def opt_variant_id regions types
 
 (** Return the types of the properly instantiated ADT value (note that
     here, ADT is understood in its broad meaning: ADT, assumed value or tuple) *)
@@ -181,12 +181,12 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
 
 (** Instantiate the type variables in an ADT definition, and return the list
     of types of the fields for the chosen variant *)
-let type_def_get_instantiated_field_etypes (def : T.type_def)
+let type_decl_get_instantiated_field_etypes (def : T.type_decl)
     (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list =
   let ty_subst =
     make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
   in
-  let fields = TU.type_def_get_fields def opt_variant_id in
+  let fields = TU.type_decl_get_fields def opt_variant_id in
   List.map
     (fun f -> erase_regions_substitute_types ty_subst f.T.field_ty)
     fields
@@ -194,10 +194,10 @@ let type_def_get_instantiated_field_etypes (def : T.type_def)
 (** Return the types of the properly instantiated ADT's variant, provided a
     context *)
 let ctx_adt_get_instantiated_field_etypes (ctx : C.eval_ctx)
-    (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
+    (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
     (types : T.ety list) : T.ety list =
-  let def = C.ctx_lookup_type_def ctx def_id in
-  type_def_get_instantiated_field_etypes def opt_variant_id types
+  let def = C.ctx_lookup_type_decl ctx def_id in
+  type_decl_get_instantiated_field_etypes def opt_variant_id types
 
 (** Apply a type substitution to a place *)
 let place_substitute (_tsubst : T.TypeVarId.id -> T.ety) (p : E.place) : E.place
@@ -320,8 +320,8 @@ and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety)
 
 (** Apply a type substitution to a function body. Return the local variables
     and the body. *)
-let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
-    (def : A.fun_def) : A.var list * A.statement =
+let fun_decl_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
+    (def : A.fun_decl) : A.var list * A.statement =
   let rsubst r = r in
   let locals =
     List.map
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 7f747a74..8f1eeb39 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -41,8 +41,8 @@ type config = {
 }
 
 type type_context = {
-  cfim_type_defs : T.type_def TypeDefId.Map.t;
-  type_defs : type_def TypeDefId.Map.t;
+  cfim_type_decls : T.type_decl TypeDeclId.Map.t;
+  type_decls : type_decl TypeDeclId.Map.t;
       (** We use this for type-checking (for sanity checks) when translating
           values and functions.
           This map is empty when we translate the types, then contains all
@@ -66,7 +66,7 @@ type fun_sig_named_outputs = {
 }
 
 type fun_context = {
-  cfim_fun_defs : A.fun_def FunDefId.Map.t;
+  cfim_fun_decls : A.fun_decl FunDeclId.Map.t;
   fun_sigs : fun_sig_named_outputs RegularFunIdMap.t;  (** *)
 }
 
@@ -83,7 +83,7 @@ type call_info = {
 type bs_ctx = {
   type_context : type_context;
   fun_context : fun_context;
-  fun_def : A.fun_def;
+  fun_decl : A.fun_decl;
   bid : T.RegionGroupId.id option;  (** TODO: rename *)
   ret_ty : ty;  (** The return type - we use it to translate `Panic` *)
   sv_to_var : var V.SymbolicValueId.Map.t;
@@ -106,34 +106,34 @@ type bs_ctx = {
 (** Body synthesis context *)
 
 let type_check_rvalue (ctx : bs_ctx) (v : typed_rvalue) : unit =
-  let ctx = { TypeCheck.type_defs = ctx.type_context.type_defs } in
+  let ctx = { TypeCheck.type_decls = ctx.type_context.type_decls } in
   TypeCheck.check_typed_rvalue ctx v
 
 let type_check_lvalue (ctx : bs_ctx) (v : typed_lvalue) : unit =
-  let ctx = { TypeCheck.type_defs = ctx.type_context.type_defs } in
+  let ctx = { TypeCheck.type_decls = ctx.type_context.type_decls } in
   TypeCheck.check_typed_lvalue ctx v
 
 (* TODO: move *)
 let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter =
-  Print.CfimAst.fun_def_to_ast_formatter ctx.type_context.cfim_type_defs
-    ctx.fun_context.cfim_fun_defs ctx.fun_def
+  Print.CfimAst.fun_decl_to_ast_formatter ctx.type_context.cfim_type_decls
+    ctx.fun_context.cfim_fun_decls ctx.fun_decl
 
 let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
-  let type_params = ctx.fun_def.signature.type_params in
-  let type_defs = ctx.type_context.cfim_type_defs in
-  let fun_defs = ctx.fun_context.cfim_fun_defs in
-  PrintPure.mk_ast_formatter type_defs fun_defs type_params
+  let type_params = ctx.fun_decl.signature.type_params in
+  let type_decls = ctx.type_context.cfim_type_decls in
+  let fun_decls = ctx.fun_context.cfim_fun_decls in
+  PrintPure.mk_ast_formatter type_decls fun_decls type_params
 
 let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let fmt = bs_ctx_to_pp_ast_formatter ctx in
   let fmt = PrintPure.ast_to_type_formatter fmt in
   PrintPure.ty_to_string fmt ty
 
-let type_def_to_string (ctx : bs_ctx) (def : type_def) : string =
+let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
   let type_params = def.type_params in
-  let type_defs = ctx.type_context.cfim_type_defs in
-  let fmt = PrintPure.mk_type_formatter type_defs type_params in
-  PrintPure.type_def_to_string fmt def
+  let type_decls = ctx.type_context.cfim_type_decls in
+  let fmt = PrintPure.mk_type_formatter type_decls type_params in
+  PrintPure.type_decl_to_string fmt def
 
 let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string =
   let fmt = bs_ctx_to_pp_ast_formatter ctx in
@@ -141,17 +141,17 @@ let typed_rvalue_to_string (ctx : bs_ctx) (v : typed_rvalue) : string =
 
 let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
   let type_params = sg.type_params in
-  let type_defs = ctx.type_context.cfim_type_defs in
-  let fun_defs = ctx.fun_context.cfim_fun_defs in
-  let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
+  let type_decls = ctx.type_context.cfim_type_decls in
+  let fun_decls = ctx.fun_context.cfim_fun_decls in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
   PrintPure.fun_sig_to_string fmt sg
 
-let fun_def_to_string (ctx : bs_ctx) (def : Pure.fun_def) : string =
+let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
   let type_params = def.signature.type_params in
-  let type_defs = ctx.type_context.cfim_type_defs in
-  let fun_defs = ctx.fun_context.cfim_fun_defs in
-  let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
-  PrintPure.fun_def_to_string fmt def
+  let type_decls = ctx.type_context.cfim_type_decls in
+  let fun_decls = ctx.fun_context.cfim_fun_decls in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
+  PrintPure.fun_decl_to_string fmt def
 
 (* TODO: move *)
 let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
@@ -173,15 +173,15 @@ let get_instantiated_fun_sig (fun_id : A.fun_id)
   (* Apply *)
   fun_sig_substitute tsubst sg
 
-let bs_ctx_lookup_cfim_type_def (id : TypeDefId.id) (ctx : bs_ctx) : T.type_def
+let bs_ctx_lookup_cfim_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) : T.type_decl
     =
-  TypeDefId.Map.find id ctx.type_context.cfim_type_defs
+  TypeDeclId.Map.find id ctx.type_context.cfim_type_decls
 
-let bs_ctx_lookup_cfim_fun_def (id : FunDefId.id) (ctx : bs_ctx) : A.fun_def =
-  FunDefId.Map.find id ctx.fun_context.cfim_fun_defs
+let bs_ctx_lookup_cfim_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl =
+  FunDeclId.Map.find id ctx.fun_context.cfim_fun_decls
 
 (* TODO: move *)
-let bs_ctx_lookup_local_function_sig (def_id : FunDefId.id)
+let bs_ctx_lookup_local_function_sig (def_id : FunDeclId.id)
     (back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
   let id = (A.Local def_id, back_id) in
   (RegularFunIdMap.find id ctx.fun_context.fun_sigs).sg
@@ -264,7 +264,7 @@ let translate_variants (vl : T.variant list) : variant list =
   List.map translate_variant vl
 
 (** Translate a type def kind to IM *)
-let translate_type_def_kind (kind : T.type_def_kind) : type_def_kind =
+let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
   match kind with
   | T.Struct fields -> Struct (translate_fields fields)
   | T.Enum variants -> Enum (translate_variants variants)
@@ -274,14 +274,14 @@ let translate_type_def_kind (kind : T.type_def_kind) : type_def_kind =
     TODO: this is not symbolic to pure but IM to pure. Still, I don't see the
     point of moving this definition for now.
  *)
-let translate_type_def (def : T.type_def) : type_def =
+let translate_type_decl (def : T.type_decl) : type_decl =
   (* Translate *)
   let def_id = def.T.def_id in
   let name = def.name in
   (* Can't translate types with regions for now *)
   assert (def.region_params = []);
   let type_params = def.type_params in
-  let kind = translate_type_def_kind def.T.kind in
+  let kind = translate_type_decl_kind def.T.kind in
   { def_id; name; type_params; kind }
 
 (** Translate a type, seen as an input/output of a forward function
@@ -1292,8 +1292,8 @@ and translate_expansion (config : config) (p : S.mplace option)
           match type_id with
           | T.AdtId adt_id ->
               (* Detect if this is an enumeration or not *)
-              let tdef = bs_ctx_lookup_cfim_type_def adt_id ctx in
-              let is_enum = type_def_is_enum tdef in
+              let tdef = bs_ctx_lookup_cfim_type_decl adt_id ctx in
+              let is_enum = type_decl_is_enum tdef in
               if is_enum then
                 (* This is an enumeration: introduce an [ExpandEnum] let-binding *)
                 let variant_id = Option.get variant_id in
@@ -1441,13 +1441,13 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression)
   let ty = next_e.ty in
   { e; ty }
 
-let translate_fun_def (config : config) (ctx : bs_ctx) (body : S.expression) :
-    fun_def =
-  let def = ctx.fun_def in
+let translate_fun_decl (config : config) (ctx : bs_ctx) (body : S.expression) :
+    fun_decl =
+  let def = ctx.fun_decl in
   let bid = ctx.bid in
   log#ldebug
     (lazy
-      ("SymbolicToPure.translate_fun_def: "
+      ("SymbolicToPure.translate_fun_decl: "
       ^ Print.fun_name_to_string def.A.name
       ^ " ("
       ^ Print.option_to_string T.RegionGroupId.to_string bid
@@ -1485,13 +1485,13 @@ let translate_fun_def (config : config) (ctx : bs_ctx) (body : S.expression) :
   (* Debugging *)
   log#ldebug
     (lazy
-      ("SymbolicToPure.translate_fun_def: translated:\n"
-     ^ fun_def_to_string ctx def));
+      ("SymbolicToPure.translate_fun_decl: translated:\n"
+     ^ fun_decl_to_string ctx def));
   (* return *)
   def
 
-let translate_type_defs (type_defs : T.type_def list) : type_def list =
-  List.map translate_type_def type_defs
+let translate_type_decls (type_decls : T.type_decl list) : type_decl list =
+  List.map translate_type_decl type_decls
 
 (** Translates function signatures.
 
diff --git a/src/Translate.ml b/src/Translate.ml
index 9b651288..3b42d13c 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -51,7 +51,7 @@ type symbolic_fun_translation = V.symbolic_value list * SA.expression
     for the forward function and the backward functions.
 *)
 let translate_function_to_symbolics (config : C.partial_config)
-    (trans_ctx : trans_ctx) (fdef : A.fun_def) :
+    (trans_ctx : trans_ctx) (fdef : A.fun_decl) :
     symbolic_fun_translation * symbolic_fun_translation list =
   (* Debug *)
   log#ldebug
@@ -91,7 +91,7 @@ let translate_function_to_symbolics (config : C.partial_config)
 let translate_function_to_pure (config : C.partial_config)
     (mp_config : Micro.config) (trans_ctx : trans_ctx)
     (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t)
-    (pure_type_defs : Pure.type_def Pure.TypeDefId.Map.t) (fdef : A.fun_def) :
+    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) :
     pure_fun_translation =
   (* Debug *)
   log#ldebug
@@ -122,12 +122,12 @@ let translate_function_to_pure (config : C.partial_config)
   let type_context =
     {
       SymbolicToPure.types_infos = type_context.type_infos;
-      cfim_type_defs = type_context.type_defs;
-      type_defs = pure_type_defs;
+      cfim_type_decls = type_context.type_decls;
+      type_decls = pure_type_decls;
     }
   in
   let fun_context =
-    { SymbolicToPure.cfim_fun_defs = fun_context.fun_defs; fun_sigs }
+    { SymbolicToPure.cfim_fun_decls = fun_context.fun_decls; fun_sigs }
   in
   let ctx =
     {
@@ -139,7 +139,7 @@ let translate_function_to_pure (config : C.partial_config)
       var_counter;
       type_context;
       fun_context;
-      fun_def = fdef;
+      fun_decl = fdef;
       forward_inputs = [];
       (* Empty for now *)
       backward_inputs = T.RegionGroupId.Map.empty;
@@ -152,7 +152,7 @@ let translate_function_to_pure (config : C.partial_config)
   in
 
   (* We need to initialize the input/output variables *)
-  let forward_input_vars = CfimAstUtils.fun_def_get_input_vars fdef in
+  let forward_input_vars = CfimAstUtils.fun_decl_get_input_vars fdef in
   let forward_input_varnames =
     List.map (fun (v : A.var) -> v.name) forward_input_vars
   in
@@ -175,13 +175,13 @@ let translate_function_to_pure (config : C.partial_config)
 
   (* Translate the forward function *)
   let pure_forward =
-    SymbolicToPure.translate_fun_def sp_config
+    SymbolicToPure.translate_fun_decl sp_config
       (add_forward_inputs (fst symbolic_forward) ctx)
       (snd symbolic_forward)
   in
 
   (* Translate the backward functions *)
-  let translate_backward (rg : T.region_var_group) : Pure.fun_def =
+  let translate_backward (rg : T.region_var_group) : Pure.fun_decl =
     (* For the backward inputs/outputs initialization: we use the fact that
      * there are no nested borrows for now, and so that the region groups
      * can't have parents *)
@@ -235,7 +235,7 @@ let translate_function_to_pure (config : C.partial_config)
     in
 
     (* Translate *)
-    SymbolicToPure.translate_fun_def sp_config ctx symbolic
+    SymbolicToPure.translate_fun_decl sp_config ctx symbolic
   in
   let pure_backwards =
     List.map translate_backward fdef.signature.regions_hierarchy
@@ -246,7 +246,7 @@ let translate_function_to_pure (config : C.partial_config)
 
 let translate_module_to_pure (config : C.partial_config)
     (mp_config : Micro.config) (m : M.cfim_module) :
-    trans_ctx * Pure.type_def list * (bool * pure_fun_translation) list =
+    trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
   (* Debug *)
   log#ldebug (lazy "translate_module_to_pure");
 
@@ -255,12 +255,12 @@ let translate_module_to_pure (config : C.partial_config)
   let trans_ctx = { type_context; fun_context } in
 
   (* Translate all the type definitions *)
-  let type_defs = SymbolicToPure.translate_type_defs m.types in
+  let type_decls = SymbolicToPure.translate_type_decls m.types in
 
   (* Compute the type definition map *)
-  let type_defs_map =
-    Pure.TypeDefId.Map.of_list
-      (List.map (fun (def : Pure.type_def) -> (def.def_id, def)) type_defs)
+  let type_decls_map =
+    Pure.TypeDeclId.Map.of_list
+      (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls)
   in
 
   (* Translate all the function *signatures* *)
@@ -272,11 +272,11 @@ let translate_module_to_pure (config : C.partial_config)
   in
   let local_sigs =
     List.map
-      (fun (fdef : A.fun_def) ->
+      (fun (fdef : A.fun_decl) ->
         ( A.Local fdef.def_id,
           List.map
             (fun (v : A.var) -> v.name)
-            (CfimAstUtils.fun_def_get_input_vars fdef),
+            (CfimAstUtils.fun_decl_get_input_vars fdef),
           fdef.signature ))
       m.functions
   in
@@ -289,7 +289,7 @@ let translate_module_to_pure (config : C.partial_config)
   let pure_translations =
     List.map
       (translate_function_to_pure config mp_config trans_ctx fun_sigs
-         type_defs_map)
+         type_decls_map)
       m.functions
   in
 
@@ -301,14 +301,14 @@ let translate_module_to_pure (config : C.partial_config)
   in
 
   (* Return *)
-  (trans_ctx, type_defs, pure_translations)
+  (trans_ctx, type_decls, pure_translations)
 
 type gen_ctx = {
   m : M.cfim_module;
   extract_ctx : PureToExtract.extraction_ctx;
-  trans_types : Pure.type_def Pure.TypeDefId.Map.t;
-  trans_funs : (bool * pure_fun_translation) Pure.FunDefId.Map.t;
-  functions_with_decreases_clause : Pure.FunDefId.Set.t;
+  trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
+  trans_funs : (bool * pure_fun_translation) Pure.FunDeclId.Map.t;
+  functions_with_decreases_clause : Pure.FunDeclId.Set.t;
 }
 (** Extraction context *)
 
@@ -316,7 +316,7 @@ type gen_config = {
   extract_types : bool;
   extract_decreases_clauses : bool;
   extract_template_decreases_clauses : bool;
-  extract_fun_defs : bool;
+  extract_fun_decls : bool;
   test_unit_functions : bool;
 }
 
@@ -327,15 +327,15 @@ type gen_config = {
 let extract_definitions (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) : unit =
   (* Export the definition groups to the file, in the proper order *)
-  let export_type (qualif : ExtractToFStar.type_def_qualif)
-      (id : Pure.TypeDefId.id) : unit =
-    let def = Pure.TypeDefId.Map.find id ctx.trans_types in
-    ExtractToFStar.extract_type_def ctx.extract_ctx fmt qualif def
+  let export_type (qualif : ExtractToFStar.type_decl_qualif)
+      (id : Pure.TypeDeclId.id) : unit =
+    let def = Pure.TypeDeclId.Map.find id ctx.trans_types in
+    ExtractToFStar.extract_type_decl ctx.extract_ctx fmt qualif def
   in
 
   (* Utility to check a function has a decrease clause *)
-  let has_decreases_clause (def : Pure.fun_def) : bool =
-    Pure.FunDefId.Set.mem def.def_id ctx.functions_with_decreases_clause
+  let has_decreases_clause (def : Pure.fun_decl) : bool =
+    Pure.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
   in
 
   (* In case of (non-mutually) recursive functions, we use a simple procedure to
@@ -364,7 +364,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
               fwd)
         pure_ls;
     (* Extract the function definitions *)
-    (if config.extract_fun_defs then
+    (if config.extract_fun_decls then
      (* Check if the functions are mutually recursive - this really works
       * to check if the forward and backward translations of a single
       * recursive function are mutually recursive *)
@@ -386,7 +386,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          let has_decr_clause =
            has_decreases_clause def && config.extract_decreases_clauses
          in
-         ExtractToFStar.extract_fun_def ctx.extract_ctx fmt qualif
+         ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif
            has_decr_clause fwd_def def)
        fls);
     (* Insert unit tests if necessary *)
@@ -413,14 +413,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
             ids
     | Fun (NonRec id) ->
         (* Lookup *)
-        let pure_fun = Pure.FunDefId.Map.find id ctx.trans_funs in
+        let pure_fun = Pure.FunDeclId.Map.find id ctx.trans_funs in
         (* Translate *)
         export_functions false [ pure_fun ]
     | Fun (Rec ids) ->
         (* General case of mutually recursive functions *)
         (* Lookup *)
         let pure_funs =
-          List.map (fun id -> Pure.FunDefId.Map.find id ctx.trans_funs) ids
+          List.map (fun id -> Pure.FunDeclId.Map.find id ctx.trans_funs) ids
         in
         (* Translate *)
         export_functions true pure_funs
@@ -494,7 +494,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
   (* We need to compute which functions are recursive, in order to know
    * whether we should generate a decrease clause or not. *)
   let rec_functions =
-    Pure.FunDefId.Set.of_list
+    Pure.FunDeclId.Set.of_list
       (List.concat
          (List.map
             (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> [])
@@ -507,7 +507,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
    * sure there are no name clashes. *)
   let ctx =
     List.fold_left
-      (fun ctx def -> ExtractToFStar.extract_type_def_register_names ctx def)
+      (fun ctx def -> ExtractToFStar.extract_type_decl_register_names ctx def)
       ctx trans_types
   in
 
@@ -516,9 +516,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
       (fun ctx (keep_fwd, def) ->
         (* Note that we generate a decrease clause for all the recursive functions *)
         let gen_decr_clause =
-          Pure.FunDefId.Set.mem (fst def).Pure.def_id rec_functions
+          Pure.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
         in
-        ExtractToFStar.extract_fun_def_register_names ctx keep_fwd
+        ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
           gen_decr_clause def)
       ctx trans_funs
   in
@@ -542,11 +542,11 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
 
   (* Put the translated definitions in maps *)
   let trans_types =
-    Pure.TypeDefId.Map.of_list
-      (List.map (fun (d : Pure.type_def) -> (d.def_id, d)) trans_types)
+    Pure.TypeDeclId.Map.of_list
+      (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
   in
   let trans_funs =
-    Pure.FunDefId.Map.of_list
+    Pure.FunDeclId.Map.of_list
       (List.map
          (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) ->
            (fd.def_id, (keep_fwd, (fd, bdl))))
@@ -571,7 +571,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
         extract_types = false;
         extract_decreases_clauses = config.extract_decreases_clauses;
         extract_template_decreases_clauses = false;
-        extract_fun_defs = false;
+        extract_fun_decls = false;
         test_unit_functions = false;
       }
     in
@@ -603,7 +603,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
     let fun_config =
       {
         base_gen_config with
-        extract_fun_defs = true;
+        extract_fun_decls = true;
         test_unit_functions = config.test_unit_functions;
       }
     in
@@ -618,7 +618,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
         extract_decreases_clauses = config.extract_decreases_clauses;
         extract_template_decreases_clauses =
           config.extract_template_decreases_clauses;
-        extract_fun_defs = true;
+        extract_fun_decls = true;
         test_unit_functions = config.test_unit_functions;
       }
     in
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index f74b552b..3a22d388 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -12,34 +12,34 @@ let log = L.translate_log
 
 type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context }
 
-type pure_fun_translation = Pure.fun_def * Pure.fun_def list
+type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list
 
-let type_def_to_string (ctx : trans_ctx) (def : Pure.type_def) : string =
+let type_decl_to_string (ctx : trans_ctx) (def : Pure.type_decl) : string =
   let type_params = def.type_params in
-  let type_defs = ctx.type_context.type_defs in
-  let fmt = PrintPure.mk_type_formatter type_defs type_params in
-  PrintPure.type_def_to_string fmt def
+  let type_decls = ctx.type_context.type_decls in
+  let fmt = PrintPure.mk_type_formatter type_decls type_params in
+  PrintPure.type_decl_to_string fmt def
 
-let type_id_to_string (ctx : trans_ctx) (def : Pure.type_def) : string =
+let type_id_to_string (ctx : trans_ctx) (def : Pure.type_decl) : string =
   let type_params = def.type_params in
-  let type_defs = ctx.type_context.type_defs in
-  let fmt = PrintPure.mk_type_formatter type_defs type_params in
-  PrintPure.type_def_to_string fmt def
+  let type_decls = ctx.type_context.type_decls in
+  let fmt = PrintPure.mk_type_formatter type_decls type_params in
+  PrintPure.type_decl_to_string fmt def
 
 let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
   let type_params = sg.type_params in
-  let type_defs = ctx.type_context.type_defs in
-  let fun_defs = ctx.fun_context.fun_defs in
-  let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
+  let type_decls = ctx.type_context.type_decls in
+  let fun_decls = ctx.fun_context.fun_decls in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
   PrintPure.fun_sig_to_string fmt sg
 
-let fun_def_to_string (ctx : trans_ctx) (def : Pure.fun_def) : string =
+let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
   let type_params = def.signature.type_params in
-  let type_defs = ctx.type_context.type_defs in
-  let fun_defs = ctx.fun_context.fun_defs in
-  let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
-  PrintPure.fun_def_to_string fmt def
+  let type_decls = ctx.type_context.type_decls in
+  let fun_decls = ctx.fun_context.fun_decls in
+  let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
+  PrintPure.fun_decl_to_string fmt def
 
-let fun_def_id_to_string (ctx : trans_ctx) (id : Pure.FunDefId.id) : string =
+let fun_decl_id_to_string (ctx : trans_ctx) (id : Pure.FunDeclId.id) : string =
   Print.fun_name_to_string
-    (Pure.FunDefId.Map.find id ctx.fun_context.fun_defs).name
+    (Pure.FunDeclId.Map.find id ctx.fun_context.fun_decls).name
diff --git a/src/Types.ml b/src/Types.ml
index b099e7a5..6393e0d8 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -2,7 +2,7 @@ open Identifiers
 
 module TypeVarId = IdGen ()
 
-module TypeDefId = IdGen ()
+module TypeDeclId = IdGen ()
 
 module VariantId = IdGen ()
 
@@ -101,7 +101,7 @@ let option_some_id = VariantId.of_int 1
     ADTs are very general in our encoding: they account for "regular" ADTs,
     tuples and also assumed types.
 *)
-type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty
+type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
 [@@deriving show, ord]
 
 (** Ancestor for iter visitor for [ty] *)
@@ -198,15 +198,15 @@ type field = { field_name : string option; field_ty : sty } [@@deriving show]
 
 type variant = { variant_name : string; fields : field list } [@@deriving show]
 
-type type_def_kind = Struct of field list | Enum of variant list
+type type_decl_kind = Struct of field list | Enum of variant list
 [@@deriving show]
 
-type type_def = {
-  def_id : TypeDefId.id;
+type type_decl = {
+  def_id : TypeDeclId.id;
   name : type_name;
   region_params : region_var list;
   type_params : type_var list;
-  kind : type_def_kind;
+  kind : type_decl_kind;
   regions_hierarchy : region_var_groups;
       (** Stores the hierarchy between the regions (which regions have the
           same lifetime, which lifetime should end before which other lifetime,
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index 5429d709..d8895b55 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -8,7 +8,7 @@ type subtype_info = {
 [@@deriving show]
 
 type type_param_info = subtype_info [@@deriving show]
-(** See [type_def_info] *)
+(** See [type_decl_info] *)
 
 type expl_info = subtype_info [@@deriving show]
 
@@ -31,7 +31,7 @@ type 'p g_type_info = {
 [@@deriving show]
 (** Generic definition *)
 
-type type_def_info = type_param_info list g_type_info [@@deriving show]
+type type_decl_info = type_param_info list g_type_info [@@deriving show]
 (** Information about a type definition. *)
 
 type ty_info = type_borrows_info [@@deriving show]
@@ -44,7 +44,7 @@ type partial_type_info = type_param_info list option g_type_info
     Allows us to factorize code: [analyze_full_ty] is used both to analyze
     type definitions and types. *)
 
-type type_infos = type_def_info TypeDefId.Map.t [@@deriving show]
+type type_infos = type_decl_info TypeDeclId.Map.t [@@deriving show]
 
 let expl_info_init = { under_borrow = false; under_mut_borrow = false }
 
@@ -59,17 +59,17 @@ let type_borrows_info_init : type_borrows_info =
 let initialize_g_type_info (param_infos : 'p) : 'p g_type_info =
   { borrows_info = type_borrows_info_init; param_infos }
 
-let initialize_type_def_info (def : type_def) : type_def_info =
+let initialize_type_decl_info (def : type_decl) : type_decl_info =
   let param_info = { under_borrow = false; under_mut_borrow = false } in
   let param_infos = List.map (fun _ -> param_info) def.type_params in
   initialize_g_type_info param_infos
 
-let type_def_info_to_partial_type_info (info : type_def_info) :
+let type_decl_info_to_partial_type_info (info : type_decl_info) :
     partial_type_info =
   { borrows_info = info.borrows_info; param_infos = Some info.param_infos }
 
-let partial_type_info_to_type_def_info (info : partial_type_info) :
-    type_def_info =
+let partial_type_info_to_type_decl_info (info : partial_type_info) :
+    type_decl_info =
   {
     borrows_info = info.borrows_info;
     param_infos = Option.get info.param_infos;
@@ -179,7 +179,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
           ty_info tys
     | Adt (AdtId adt_id, regions, tys) ->
         (* Lookup the information for this type definition *)
-        let adt_info = TypeDefId.Map.find adt_id infos in
+        let adt_info = TypeDeclId.Map.find adt_id infos in
         (* Update the type info with the information from the adt *)
         let ty_info = update_ty_info ty_info adt_info.borrows_info in
         (* Check if 'static appears in the region parameters *)
@@ -238,8 +238,8 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
   (* Explore *)
   analyze expl_info_init ty_info ty
 
-let analyze_type_def (updated : bool ref) (infos : type_infos) (def : type_def)
-    : type_infos =
+let analyze_type_decl (updated : bool ref) (infos : type_infos)
+    (def : type_decl) : type_infos =
   (* Retrieve all the types of all the fields of all the variants *)
   let fields_tys : sty list =
     match def.kind with
@@ -250,31 +250,31 @@ let analyze_type_def (updated : bool ref) (infos : type_infos) (def : type_def)
   in
   (* Explore the types and accumulate information *)
   let r_is_static r = r = Static in
-  let type_def_info = TypeDefId.Map.find def.def_id infos in
-  let type_def_info = type_def_info_to_partial_type_info type_def_info in
-  let type_def_info =
+  let type_decl_info = TypeDeclId.Map.find def.def_id infos in
+  let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in
+  let type_decl_info =
     List.fold_left
-      (fun type_def_info ty ->
-        analyze_full_ty r_is_static updated infos type_def_info ty)
-      type_def_info fields_tys
+      (fun type_decl_info ty ->
+        analyze_full_ty r_is_static updated infos type_decl_info ty)
+      type_decl_info fields_tys
   in
-  let type_def_info = partial_type_info_to_type_def_info type_def_info in
+  let type_decl_info = partial_type_info_to_type_decl_info type_decl_info in
   (* Update the information for the type definition we explored *)
-  let infos = TypeDefId.Map.add def.def_id type_def_info infos in
+  let infos = TypeDeclId.Map.add def.def_id type_decl_info infos in
   (* Return *)
   infos
 
-let analyze_type_declaration_group (type_defs : type_def TypeDefId.Map.t)
+let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
     (infos : type_infos) (decl : type_declaration_group) : type_infos =
   (* Collect the identifiers used in the declaration group *)
   let ids = match decl with NonRec id -> [ id ] | Rec ids -> ids in
   (* Retrieve the type definitions *)
-  let decl_defs = List.map (fun id -> TypeDefId.Map.find id type_defs) ids in
+  let decl_defs = List.map (fun id -> TypeDeclId.Map.find id type_decls) ids in
   (* Initialize the type information for the current definitions *)
   let infos =
     List.fold_left
       (fun infos def ->
-        TypeDefId.Map.add def.def_id (initialize_type_def_info def) infos)
+        TypeDeclId.Map.add def.def_id (initialize_type_decl_info def) infos)
       infos decl_defs
   in
   (* Analyze the types - this function simply computes a fixed-point *)
@@ -282,7 +282,7 @@ let analyze_type_declaration_group (type_defs : type_def TypeDefId.Map.t)
   let rec analyze (infos : type_infos) : type_infos =
     let infos =
       List.fold_left
-        (fun infos def -> analyze_type_def updated infos def)
+        (fun infos def -> analyze_type_decl updated infos def)
         infos decl_defs
     in
     if !updated then (
@@ -298,11 +298,11 @@ let analyze_type_declaration_group (type_defs : type_def TypeDefId.Map.t)
     
     Rk.: pay attention to the difference between type definitions and types!
  *)
-let analyze_type_declarations (type_defs : type_def TypeDefId.Map.t)
+let analyze_type_declarations (type_decls : type_decl TypeDeclId.Map.t)
     (decls : type_declaration_group list) : type_infos =
   List.fold_left
-    (fun infos decl -> analyze_type_declaration_group type_defs infos decl)
-    TypeDefId.Map.empty decls
+    (fun infos decl -> analyze_type_declaration_group type_decls infos decl)
+    TypeDeclId.Map.empty decls
 
 (** Analyze a type to check whether it contains borrows, etc., provided
     we have already analyzed the type definitions in the context.
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index db10ed47..e463fbc5 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -2,12 +2,12 @@ open Types
 open Utils
 module TA = TypesAnalysis
 
-(** Retrieve the list of fields for the given variant of a [type_def].
+(** Retrieve the list of fields for the given variant of a [type_decl].
 
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
-let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
-    : field list =
+let type_decl_get_fields (def : type_decl)
+    (opt_variant_id : VariantId.id option) : field list =
   match (def.kind, opt_variant_id) with
   | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
   | Struct fields, None -> fields
@@ -19,7 +19,7 @@ let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
         (Invalid_argument
            ("The variant id should be [Some] if and only if the definition is \
              an enumeration:\n\
-             - def: " ^ show_type_def def ^ "\n- opt_variant_id: "
+             - def: " ^ show_type_decl def ^ "\n- opt_variant_id: "
           ^ opt_variant_id))
 
 (** Return [true] if a [ty] is actually `unit` *)
@@ -37,7 +37,7 @@ let ty_as_adt (ty : 'r ty) : type_id * 'r list * 'r ty list =
 let ty_is_custom_adt (ty : 'r ty) : bool =
   match ty with Adt (AdtId _, _, _) -> true | _ -> false
 
-let ty_as_custom_adt (ty : 'r ty) : TypeDefId.id * 'r list * 'r ty list =
+let ty_as_custom_adt (ty : 'r ty) : TypeDeclId.id * 'r list * 'r ty list =
   match ty with
   | Adt (AdtId id, regions, tys) -> (id, regions, tys)
   | _ -> failwith "Unreachable"