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

1 files changed, 42 insertions, 42 deletions

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.