diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 24 |
1 files changed, 19 insertions, 5 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1f9c9117..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) @@ -2853,7 +2867,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "="; F.pp_print_space fmt (); let success = - ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx + ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx in F.pp_print_string fmt (success ^ " ())") | Coq -> @@ -2884,11 +2898,11 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "=="; F.pp_print_space fmt (); let success = - ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx + ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx in F.pp_print_string fmt (success ^ " ())") | HOL4 -> - F.pp_print_string fmt "val _ = assert_return ("; + F.pp_print_string fmt "val _ = assert_ok ("; F.pp_print_string fmt "“"; let fun_name = ctx_get_local_function def.meta def.def_id def.loop_id ctx |