Make progress on the extraction

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 =