summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEscherichia2024-04-03 17:36:09 +0200
committerEscherichia2024-04-03 17:36:09 +0200
commita2a219145587deb0ade9fa7d60171765cd722162 (patch)
tree69727a10478c7f258f18ac89ccca90819490e178
parent084480c807b58947b8487eb3a7c6a71bb388a832 (diff)
added extract_ty_errors and extract_texpression_errors to deal with the error case in their respective types
-rw-r--r--compiler/Extract.ml4
-rw-r--r--compiler/ExtractTypes.ml9
2 files changed, 10 insertions, 3 deletions
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)