diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Config.ml | 4 | ||||
| -rw-r--r-- | compiler/Extract.ml | 10 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 16 |
3 files changed, 24 insertions, 6 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 508746d9..62f6c300 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -339,3 +339,7 @@ let parameterize_trait_types = ref false trait associated types in the pure code. *) 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 diff --git a/compiler/Extract.ml b/compiler/Extract.ml index fe007d31..864d513f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -529,7 +529,15 @@ let type_decl_kind_to_qualif (kind : decl_kind) *) Some "with" | (Assumed | Declared), None -> Some "Axiom" - | _ -> raise (Failure "Unexpected")) + | SingleNonRec, None -> + (* This is for traits *) + Some "Record" + | _ -> + raise + (Failure + ("Unexpected: (" ^ show_decl_kind kind ^ ", " + ^ Print.option_to_string show_type_decl_kind type_kind + ^ ")"))) | Lean -> ( match kind with | SingleNonRec -> diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 6789b5b8..612cf359 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -78,6 +78,7 @@ type decl_kind = F*: [val x : Type0] Coq: [Axiom x : Type.] *) +[@@deriving show] (** Return [true] if the declaration is the last from its group of declarations. @@ -112,7 +113,7 @@ let decl_is_first_from_group (kind : decl_kind) : bool = let decl_is_not_last_from_group (kind : decl_kind) : bool = not (decl_is_last_from_group kind) -type type_decl_kind = Enum | Struct +type type_decl_kind = Enum | Struct [@@deriving show] (* TODO: this should be a module we give to a functor! *) @@ -533,7 +534,8 @@ let names_map_check_collision (id_to_string : id -> string) (id : id) | None -> () (* Ok *) | Some clash -> (* There is a clash: print a nice debugging message for the user *) - report_name_collision id_to_string clash id name + if !Config.extract_fail_hard then + report_name_collision id_to_string clash id name let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id) (name : string) (nm : names_map) : names_map = @@ -707,9 +709,12 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name | FunId (Assumed aid) -> A.show_assumed_fun_id aid - | TraitMethod _ -> + | TraitMethod (_, method_name, _) -> (* Shouldn't happen *) - raise (Failure "Unexpected") + if !Config.extract_fail_hard then raise (Failure "Unexpected") + else ( + log#serror ("Unexpected trait method: " ^ method_name); + method_name) in let lp_kind = @@ -899,7 +904,8 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string = if with_opaque_pre && is_opaque then ctx.fmt.opaque_pre () ^ s else s | None -> log#serror ("Could not find: " ^ id_to_string id ctx); - raise Not_found + if !Config.extract_fail_hard then raise (Failure "Not found") + else "(ERROR: \"" ^ id_to_string id ctx ^ "\")" let ctx_get_global (with_opaque_pre : bool) (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = |