summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Extract.ml')
-rw-r--r--compiler/Extract.ml18
1 files changed, 16 insertions, 2 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 27e9a62c..6eeef772 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
^ string_of_int (List.length types)
^ " type arguments"
in
- log#serror err;
+ save_error __FILE__ __LINE__ None err;
Result.Error (types, err))
else
let types = List.combine filter types in
@@ -297,6 +297,13 @@ let lets_require_wrap_in_do (meta : Meta.meta)
- application argument: [f (exp)]
- match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
*)
+
+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"
+ | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
(fmt : F.formatter) (inside : bool) (e : texpression) : unit =
match e.e with
@@ -323,6 +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_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
@@ -1871,7 +1879,7 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
[{start,end}_gloabl_decl_group], contrary to {!extract_type_decl}
and {!extract_fun_decl}.
*)
-let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
(global : global_decl) (body : fun_decl) (interface : bool) : unit =
let meta = body.meta in
sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
@@ -1966,6 +1974,12 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break to insert lines between declarations *)
F.pp_print_break fmt 0 0
+let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+ (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
+ match global with
+ | Some global -> extract_global_decl_aux ctx fmt global body interface
+ | None -> ()
+
(** Similar to {!extract_trait_decl_register_names} *)
let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
(trait_decl : trait_decl)