diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 4 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 9 |
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) |