diff options
| -rw-r--r-- | compiler/SymbolicToPure.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 69ff4df1..6983a0e8 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -269,7 +269,11 @@ let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string = let env = bs_ctx_to_fmt_env ctx in Print.Types.ty_to_string env ty -let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = +let type_decl_to_string (ctx : bs_ctx) (def : T.type_decl) : string = + let env = bs_ctx_to_fmt_env ctx in + Print.Types.type_decl_to_string env def + +let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = let env = bs_ctx_to_pure_fmt_env ctx in PrintPure.type_decl_to_string env def @@ -476,6 +480,12 @@ let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind = *) let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : type_decl = + log#ldebug + (lazy + (let ctx = Print.Contexts.decls_ctx_to_fmt_env ctx in + "translate_type_decl:\n\n" + ^ Print.Types.type_decl_to_string ctx def + ^ "\n")); let env = Print.Contexts.decls_ctx_to_fmt_env ctx in let def_id = def.T.def_id in let llbc_name = def.name in |