diff options
| author | Son Ho | 2023-11-20 22:48:38 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-20 22:48:38 +0100 |
| commit | db58a6bcc95c66febc70e90af928feae7dddf56c (patch) | |
| tree | a1c671e56668080af93f94ca6245c081f2852212 /compiler | |
| parent | 5aa37b3a0a539f9ae37a119b9ce7c8dee504125e (diff) | |
Fix minor issues
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 8 | ||||
| -rw-r--r-- | compiler/Logging.ml | 3 | ||||
| -rw-r--r-- | compiler/Main.ml | 1 |
3 files changed, 9 insertions, 3 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 106451cc..2c3c8106 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -8,6 +8,8 @@ open Config open Charon.NameMatcher (* TODO: include? *) include ExtractName (* TODO: only open? *) +let log = Logging.builtin_log + (** Small utility to memoize some computations *) let mk_memoized (f : unit -> 'a) : unit -> 'a = let r = ref None in @@ -492,9 +494,9 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = in [ (* core::ops::Deref<alloc::boxed::Box<T>> *) - fmt "core::ops::Deref<Box<@T>>" (); - (* core::ops::Deref<alloc::boxed::Box<T>> *) - fmt "core::ops::Deref<Box<@T>>" (); + fmt "core::ops::deref::Deref<Box<@T>>" (); + (* core::ops::DerefMut<alloc::boxed::Box<T>> *) + fmt "core::ops::deref::DerefMut<Box<@T>>" (); (* core::ops::index::Index<[T], I> *) fmt "core::ops::index::Index<[@T], @I>" (); (* core::ops::index::IndexMut<[T], I> *) diff --git a/compiler/Logging.ml b/compiler/Logging.ml index f4ad87a9..9c20f32f 100644 --- a/compiler/Logging.ml +++ b/compiler/Logging.ml @@ -27,6 +27,9 @@ let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses" (** Logger for ExtractBase *) let extract_log = L.get_logger "MainLogger.ExtractBase" +(** Logger for ExtractBuiltin *) +let builtin_log = L.get_logger "MainLogger.Builtin" + (** Logger for Interpreter *) let interpreter_log = L.get_logger "MainLogger.Interpreter" diff --git a/compiler/Main.ml b/compiler/Main.ml index 94e50a08..0daf454d 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -38,6 +38,7 @@ let _ = symbolic_to_pure_log#set_level EL.Info; pure_micro_passes_log#set_level EL.Info; extract_log#set_level EL.Info; + builtin_log#set_level EL.Info; translate_log#set_level EL.Info; scc_log#set_level EL.Info; reorder_decls_log#set_level EL.Info |