From 848874a4eb5d29742f7afa2567bc424871b1c7ef Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 3 Mar 2022 11:47:26 +0100 Subject: Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...decl --- src/SymbolicToPure.ml | 84 +++++++++++++++++++++++++-------------------------- 1 file changed, 42 insertions(+), 42 deletions(-) (limited to 'src/SymbolicToPure.ml') 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. -- cgit v1.2.3