Fix a small issue in AssociatedTypes

7 files changed, 21 insertions, 15 deletions

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index e4015903..581e218c 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -451,7 +451,7 @@ and ctx_normalize_trait_instance_id :
       | None ->
           (* This is actually a local clause *)
           assert (trait_instance_id_is_local_clause inst_id);
-          (ParentClause (inst_id, decl_id, clause_id), None)
+          (ItemClause (inst_id, decl_id, item_name, clause_id), None)
       | Some impl ->
           (* We figure out the item clause by doing the following:
              {[
diff --git a/compiler/Config.ml b/compiler/Config.ml
index cd0903b6..8483c879 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -333,6 +333,6 @@ let parameterize_trait_types = ref false
  *)
 let type_check_pure_code = ref false
 
-(** Shall we fail hard if there is an issue at code-generation time?
-    We may not want in case outputting a code with holes helps debugging *)
-let extract_fail_hard = ref false
+(** Shall we fail hard if we encounter an issue, or should we attempt to go
+    as far as possible while leaving "holes" in the generated code? *)
+let fail_hard = ref true
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index b660b5a5..14668632 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -41,7 +41,7 @@ let _ =
   pure_utils_log#set_level EL.Info;
   symbolic_to_pure_log#set_level EL.Info;
   pure_micro_passes_log#set_level EL.Info;
-  pure_to_extract_log#set_level EL.Info;
+  extract_log#set_level EL.Info;
   translate_log#set_level EL.Info;
   scc_log#set_level EL.Info;
   reorder_decls_log#set_level EL.Info
@@ -66,6 +66,9 @@ let () =
   (* Read the command line arguments *)
   let dest_dir = ref "" in
 
+  (* Print the imported llbc *)
+  let print_llbc = ref false in
+
   let spec =
     [
       ( "-backend",
@@ -118,6 +121,8 @@ let () =
       ( "-lean-default-lakefile",
         Arg.Clear lean_gen_lakefile,
         " Generate a default lakefile.lean (Lean only)" );
+      ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC");
+      ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error");
     ]
   in
 
@@ -131,6 +136,7 @@ let () =
   in
 
   if !extract_template_decreases_clauses then extract_decreases_clauses := true;
+  if !print_llbc then main_log#set_level EL.Debug;
 
   (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
   assert (!extract_decreases_clauses || not !extract_template_decreases_clauses);
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 8ad8a18d..b8cb38bb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -472,7 +472,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
       | Error (types, err) ->
           extract_generic_args ctx fmt TypeDeclId.Set.empty
             { generics with types };
-          if !Config.extract_fail_hard then raise (Failure err)
+          if !Config.fail_hard then raise (Failure err)
           else
             F.pp_print_string fmt
               "(\"ERROR: ill-formed builtin: invalid number of filtering \
@@ -1992,7 +1992,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
                         trans_fun.back_id
                   in
                   log#serror err;
-                  if !Config.extract_fail_hard then raise (Failure err)
+                  if !Config.fail_hard then raise (Failure err)
                   else (trans_fun.back_id, "%ERROR_BUILTIN_NAME_NOT_FOUND%")
             in
             let rg_with_name_list = List.map find trans_funs in
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 8ddb2ec6..55b1bca3 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -8,7 +8,7 @@ module F = Format
 open ExtractBuiltin
 
 (** The local logger *)
-let log = L.pure_to_extract_log
+let log = L.extract_log
 
 type region_group_info = {
   id : RegionGroupId.id;
@@ -488,7 +488,7 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
   in
   log#serror err;
   (* If we fail hard on errors, raise an exception *)
-  if !Config.extract_fail_hard then raise (Failure err)
+  if !Config.fail_hard then raise (Failure err)
 
 let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
   StringMap.find_opt name nm.name_to_id
@@ -522,7 +522,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
     in
     log#serror err;
     (* If we fail hard on errors, raise an exception *)
-    if !Config.extract_fail_hard then raise (Failure err));
+    if !Config.fail_hard then raise (Failure err));
   (* Insert *)
   names_map_add_unchecked id name nm
 
@@ -691,7 +691,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
             | FunId (Assumed aid) -> A.show_assumed_fun_id aid
             | TraitMethod (trait_ref, method_name, _) ->
                 (* Shouldn't happen *)
-                if !Config.extract_fail_hard then raise (Failure "Unexpected")
+                if !Config.fail_hard then raise (Failure "Unexpected")
                 else
                   "Trait method: decl: "
                   ^ TraitDeclId.to_string trait_ref.trait_decl_ref.trait_decl_id
@@ -903,7 +903,7 @@ let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) :
           ^ map_to_string m
         in
         log#serror err;
-        if !Config.extract_fail_hard then raise (Failure err)
+        if !Config.fail_hard then raise (Failure err)
         else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
   else
     let m = nm.names_map.id_to_name in
@@ -915,7 +915,7 @@ let names_maps_get (id_to_string : id -> string) (id : id) (nm : names_maps) :
           ^ map_to_string m
         in
         log#serror err;
-        if !Config.extract_fail_hard then raise (Failure err)
+        if !Config.fail_hard then raise (Failure err)
         else "(ERROR: \"" ^ id_to_string id ^ "\")"
 
 let ctx_get (id : id) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 7bd02381..699a0e96 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1374,7 +1374,7 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
   | Self ->
       (* This has a specific treatment depending on the item we're extracting
          (associated type, etc.). We should have caught this elsewhere. *)
-      if !Config.extract_fail_hard then
+      if !Config.fail_hard then
         raise (Failure "Unexpected occurrence of `Self`")
       else F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
   | TraitImpl id ->
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 59abbfc7..721655b8 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -22,7 +22,7 @@ let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
 let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses"
 
 (** Logger for ExtractBase *)
-let pure_to_extract_log = L.get_logger "MainLogger.ExtractBase"
+let extract_log = L.get_logger "MainLogger.ExtractBase"
 
 (** Logger for Interpreter *)
 let interpreter_log = L.get_logger "MainLogger.Interpreter"