summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/AssociatedTypes.ml2
-rw-r--r--compiler/Config.ml6
-rw-r--r--compiler/Driver.ml8
-rw-r--r--compiler/Extract.ml4
-rw-r--r--compiler/ExtractBase.ml12
-rw-r--r--compiler/ExtractTypes.ml2
-rw-r--r--compiler/Logging.ml2
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"
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 08:04:09 +0000