From a2a219145587deb0ade9fa7d60171765cd722162 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 17:36:09 +0200
Subject: added extract_ty_errors and extract_texpression_errors to deal with
 the error case in their respective types

---
 compiler/Extract.ml      | 4 ++--
 compiler/ExtractTypes.ml | 9 ++++++++-
 2 files changed, 10 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index ef5d5dce..af0bf98d 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -298,7 +298,7 @@ let lets_require_wrap_in_do (meta : Meta.meta)
     - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
  *)
 
-let extract_errors (fmt : F.formatter) =
+let extract_texpression_errors (fmt : F.formatter) =
   match !Config.backend with
   | FStar | Coq -> F.pp_print_string fmt "admit"
   | Lean -> F.pp_print_string fmt "sorry"
@@ -330,7 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
   | Loop _ ->
       (* The loop nodes should have been eliminated in {!PureMicroPasses} *)
       craise __FILE__ __LINE__ meta "Unreachable"
-  | EError (_, _) -> extract_errors fmt
+  | EError (_, _) -> extract_texpression_errors fmt
 
 (* Extract an application *or* a top-level qualif (function extraction has
  * to handle top-level qualifiers, so it seemed more natural to merge the
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 350866e9..1c3657a3 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -433,6 +433,13 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
       End
     ]}
  *)
+
+let extract_ty_errors (fmt : F.formatter) : unit =
+  match !Config.backend with
+  | FStar | Coq -> F.pp_print_string fmt "admit"
+  | Lean -> F.pp_print_string fmt "sorry"
+  | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
 let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
   let extract_rec = extract_ty meta ctx fmt no_params_tys in
@@ -566,7 +573,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
               "Trait types are not supported yet when generating code for HOL4";
             extract_trait_ref meta ctx fmt no_params_tys false trait_ref;
             F.pp_print_string fmt ("." ^ add_brackets type_name))
-  | Error -> craise __FILE__ __LINE__ meta "TODO: Error message?"
+  | Error -> extract_ty_errors fmt
 
 and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx)
     (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
-- 
cgit v1.2.3