From 5e0311d47c908ff76ddb6f89d01ed832356dcf43 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 9 Feb 2024 11:54:37 +0100 Subject: [PATCH] Fix certicoq eval w.r.t. backtracking in Coq --- benchmarks/certicoq_eval.v | 27 ++++++++++++-- plugin/certicoq.ml | 72 +++++++++++++++++++++----------------- plugin/certicoq.mli | 9 +++-- plugin/g_certicoq.mlg | 30 +++++++++------- 4 files changed, 87 insertions(+), 51 deletions(-) diff --git a/benchmarks/certicoq_eval.v b/benchmarks/certicoq_eval.v index 67900810..00383551 100644 --- a/benchmarks/certicoq_eval.v +++ b/benchmarks/certicoq_eval.v @@ -2,9 +2,27 @@ From Equations Require Import Equations. From Coq Require Import Uint63 Wf_nat ZArith Lia Arith. From CertiCoq Require Import CertiCoq. +Set CertiCoq Build Directory "_build". + (* This warns about uses of primitive operations, but we compile them fine *) Set Warnings "-primitive-turned-into-axiom". +From Coq Require Vector Fin. +Import Vector.VectorNotations. + +Program Definition long_vector n : Vector.t nat n := + Vector.of_list (List.repeat 1000 n). + Next Obligation. now rewrite List.repeat_length. Qed. + +Definition silent_long_vector := 0. + (* Vector.eqb _ Nat.eqb (long_vector 5000) (long_vector 5000). *) +(* Time Eval vm_compute in silent_long_vector. (* Blows up *) *) +(* 1.23s *) +(* Set Debug "certicoq-reify". *) +(* Set Debug "backtrace". *) +CertiCoq Eval -time -debug silent_long_vector. +CertiCoq Eval -time -debug silent_long_vector. +CertiCoq Eval -time -debug silent_long_vector. Definition inspect {A} (a : A) : {b | a = b} := exist _ a eq_refl. @@ -88,10 +106,13 @@ Definition vs_hard := (* Blows up *) Time Eval vm_compute in vs_hard. *) -CertiCoq Eval -time vs_hard. +(* CertiCoq Eval -time vs_hard. *) (* Executed in 0.06s *) -CertiCoq Eval -time vs_hard. +(* CertiCoq Eval -time vs_hard. *) -CertiCoq Eval -time vs_easy. +(* CertiCoq Eval -time vs_easy. *) (* Executed in 0.007s *) + + + diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index 78d47ea7..4a16cb2b 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -115,25 +115,28 @@ let certicoq_run_functions_name = "certicoq-run-functions-registration" let all_run_functions = ref CString.Set.empty -let cache_certicoq_run_function (s, fn) = +let cache_certicoq_run_function (s, s', fn) = let fns = !certicoq_run_functions in - all_run_functions := CString.Set.add s !all_run_functions; + all_run_functions := CString.Set.add s (CString.Set.add s' !all_run_functions); certicoq_run_functions := CString.Map.add s fn fns let certicoq_run_function_input = - let open Libobject in + let open Libobject in declare_object (global_object_nodischarge certicoq_run_functions_name ~cache:(fun r -> cache_certicoq_run_function r) ~subst:None) -let register_certicoq_run s fn = +let register_certicoq_run s s' fn = Feedback.msg_debug Pp.(str"Registering function " ++ str s ++ str " in certicoq_run"); - Lib.add_leaf (certicoq_run_function_input (s, fn)) + Lib.add_leaf (certicoq_run_function_input (s, s', fn)) let exists_certicoq_run s = - CString.Map.find_opt s !certicoq_run_functions - + Feedback.msg_debug Pp.(str"Looking up " ++ str s ++ str " in certicoq_run_functions"); + let res = CString.Map.find_opt s !certicoq_run_functions in + if Option.is_empty res then Feedback.msg_debug Pp.(str"Not found"); + res + let run_certicoq_run s = try CString.Map.find s !certicoq_run_functions with Not_found -> CErrors.user_err Pp.(str"Could not find certicoq run function associated to " ++ str s) @@ -580,14 +583,16 @@ module CompileFunctor (CI : CompilerInterface) = struct let open Declarations in let debug s = debug_reify Pp.(fun () -> str s) in let rec aux ty v = + Control.check_for_interrupt (); + let () = debug_reify Pp.(fun () -> str "Reifying value of type " ++ pr_reifyable_type env sigma ty) in match ty with | IsInductive (hd, u, args) -> let open Inductive in let open Inductiveops in let spec = lookup_mind_specif env hd in - let indfam = make_ind_family ((hd, u), args) in let npars = inductive_params spec in let params, _indices = CList.chop npars args in + let indfam = make_ind_family ((hd, u), params) in let cstrs = get_constructors env indfam in if Obj.is_block v then let ord = get_boxed_ordinal v in @@ -645,30 +650,30 @@ module CompileFunctor (CI : CompilerInterface) = struct flush chan; close_out chan; fname - let template_ocaml name = - Printf.sprintf "external %s : unit -> Obj.t = \"%s\"\nlet _ = Certicoq_plugin.Certicoq.register_certicoq_run \"%s\" (Obj.magic %s)" name name name name + let template_ocaml id filename name = + Printf.sprintf "external %s : unit -> Obj.t = \"%s\"\nlet _ = Certicoq_plugin.Certicoq.register_certicoq_run \"%s\" \"%s\" (Obj.magic %s)" name name id filename name - let write_ocaml_driver opts name = + let write_ocaml_driver id opts name = let fname = make_fname opts (opts.filename ^ "_wrapper.ml") in let chan = open_out fname in - output_string chan (template_ocaml name); + output_string chan (template_ocaml id opts.filename name); flush chan; close_out chan; fname - let certicoq_eval_named opts env sigma id c imports = + let certicoq_eval_named opts env sigma c global_id imports = let prog = quote_term opts env sigma c in let tyinfo = let ty = Retyping.get_type_of env sigma c in (* assert (Evd.is_empty sigma); *) check_reifyable env sigma ty in - let () = compile opts (Obj.magic prog) imports in + let id = opts.toplevel_name in + let () = compile { opts with toplevel_name = id ^ "_body" } (Obj.magic prog) imports in (* Write wrapping code *) let c_driver = write_c_driver opts id in - let ocaml_driver = write_ocaml_driver opts id in + let ocaml_driver = write_ocaml_driver global_id opts id in let imports = get_global_includes () @ imports in let debug = opts.debug in let suff = opts.ext in - let name = make_fname opts (id ^ suff) in let compiler = compiler_executable debug in let ocamlfind = ocamlfind_executable debug in let rt_dir = runtime_dir () in @@ -699,7 +704,7 @@ module CompileFunctor (CI : CompilerInterface) = struct let dontlink = "str,unix,dynlink,threads,zarith,coq-core,coq-core.plugins.ltac,coq-core.interp" in match Unix.system cmd with | Unix.WEXITED 0 -> - let shared_lib = name ^ ".cmxs" in + let shared_lib = make_fname opts opts.filename ^ suff ^ ".cmxs" in let linkcmd = Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \ -I %s -I plugin -o %s %s %s %s %s" @@ -709,12 +714,12 @@ module CompileFunctor (CI : CompilerInterface) = struct debug_msg debug (Printf.sprintf "Executing command: %s" linkcmd); (match Unix.system linkcmd with | Unix.WEXITED 0 -> - debug_msg debug (Printf.sprintf "Compilation ran fine, linking compiled code for %s" id); + debug_msg debug (Printf.sprintf "Compilation ran fine, linking compiled code for %s" global_id); Dynlink.loadfile_private shared_lib; - debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" id); + debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" global_id); let result = - if opts.time then time ~msg:(Pp.str id) (run_certicoq_run id) - else run_certicoq_run id () + if opts.time then time ~msg:(Pp.str id) (run_certicoq_run global_id) + else run_certicoq_run global_id () in debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); reify opts env sigma tyinfo result @@ -733,10 +738,15 @@ module CompileFunctor (CI : CompilerInterface) = struct Feedback.msg_debug Pp.(str "Found " ++ str freshs); freshs + let toplevel_name_of_filename s = + let comps = CString.split_on_char '.' s in + CString.uncapitalize_ascii (CString.concat "_" comps) + let certicoq_eval opts env sigma c imports = - let fresh_name = find_fresh opts.filename !all_run_functions in - let opts = { opts with toplevel_name = fresh_name ^ "_body"; filename = fresh_name } in - certicoq_eval_named opts env sigma fresh_name c imports + let global_id = opts.filename in + let fresh_name = find_fresh global_id !all_run_functions in + let opts = { opts with toplevel_name = toplevel_name_of_filename fresh_name; filename = fresh_name } in + certicoq_eval_named opts env sigma c global_id imports let run_existing opts env sigma c id run = let tyinfo = @@ -750,23 +760,21 @@ module CompileFunctor (CI : CompilerInterface) = struct debug_msg opts.debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); reify opts env sigma tyinfo result - let certicoq_eval opts env sigma c imports = + let eval opts env sigma c imports = match exists_certicoq_run opts.filename with | None -> certicoq_eval opts env sigma c imports | Some run -> debug_msg opts.debug (Printf.sprintf "Retrieved earlier compiled code for %s" opts.filename); run_existing opts env sigma c (Pp.str opts.filename) run - let compile_shared_C opts gr imports = + let eval_gr opts gr imports = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Evd.fresh_global env sigma gr in - let name = Names.Id.to_string (Nametab.basename_of_global gr) in - match exists_certicoq_run name with - | None -> - let opts = { opts with toplevel_name = name ^ "_body"; } in - certicoq_eval_named opts env sigma name c imports - | Some run -> run_existing opts env sigma c (Pp.str name) run + let filename = get_name gr in + let name = toplevel_name_of_filename filename in + let opts = { opts with toplevel_name = name; filename = filename } in + eval opts env sigma c imports let print_to_file (s : string) (file : string) = let f = open_out file in diff --git a/plugin/certicoq.mli b/plugin/certicoq.mli index 494c98b0..0e493721 100644 --- a/plugin/certicoq.mli +++ b/plugin/certicoq.mli @@ -69,14 +69,17 @@ end val compile_only : options -> Names.GlobRef.t -> import list -> unit val generate_glue_only : options -> Names.GlobRef.t -> unit val compile_C : options -> Names.GlobRef.t -> import list -> unit -val compile_shared_C : options -> Names.GlobRef.t -> import list -> Constr.t +val eval_gr : options -> Names.GlobRef.t -> import list -> Constr.t val show_ir : options -> Names.GlobRef.t -> unit val ffi_command : options -> Names.GlobRef.t -> unit val glue_command : options -> Names.GlobRef.t list -> unit -val certicoq_eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t +val eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t (* Support for running dynamically linked certicoq-compiled programs *) type certicoq_run_function = unit -> Obj.t -val register_certicoq_run : string -> certicoq_run_function -> unit +(* [register_certicoq_run global_id fresh_name function]. A same global_id + can be compiled multiple times with different definitions, fresh_name indicates + the version used this time *) +val register_certicoq_run : string -> string -> certicoq_run_function -> unit val run_certicoq_run : string -> certicoq_run_function diff --git a/plugin/g_certicoq.mlg b/plugin/g_certicoq.mlg index 4c73d4c6..1a4c9d74 100644 --- a/plugin/g_certicoq.mlg +++ b/plugin/g_certicoq.mlg @@ -110,18 +110,6 @@ VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY let opts = Certicoq.make_options l [] (get_name gr) in Certicoq.compile_C opts gr [] } -| [ "CertiCoq" "Eval" cargs_list(l) global(gr) "Extract" "Constants" "[" extract_cnst_list_sep(cs, ",") "]" "Include" "[" cinclude_list_sep(imps, ",") "]" ] -> { - let gr = Nametab.global gr in - let opts = Certicoq.make_options l cs (get_name gr) in - let result = Certicoq.compile_shared_C opts gr imps in - Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result) - } -| [ "CertiCoq" "Eval" cargs_list(l) global(gr) ] -> { - let gr = Nametab.global gr in - let opts = Certicoq.make_options l [] (get_name gr) in - let result = Certicoq.compile_shared_C opts gr [] in - Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result) - } | [ "CertiCoq" "Show" "IR" cargs_list(l) global(gr) ] -> { let gr = Nametab.global gr in let opts = Certicoq.make_options l [] (get_name gr) in @@ -147,6 +135,21 @@ VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY } END +VERNAC COMMAND EXTEND CertiCoq_Eval CLASSIFIED AS SIDEFF +| [ "CertiCoq" "Eval" cargs_list(l) global(gr) "Extract" "Constants" "[" extract_cnst_list_sep(cs, ",") "]" "Include" "[" cinclude_list_sep(imps, ",") "]" ] -> { + let gr = Nametab.global gr in + let opts = Certicoq.make_options l cs (get_name gr) in + let result = Certicoq.eval_gr opts gr imps in + Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result) + } +| [ "CertiCoq" "Eval" cargs_list(l) global(gr) ] -> { + let gr = Nametab.global gr in + let opts = Certicoq.make_options l [] (get_name gr) in + let result = Certicoq.eval_gr opts gr [] in + Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result) + } +END + TACTIC EXTEND CertiCoq_eval | [ "certicoq_eval" cargs_list(l) constr(c) tactic(tac) ] -> { (* quote and evaluate the given term, unquote, pass the result to t *) @@ -154,7 +157,8 @@ TACTIC EXTEND CertiCoq_eval let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let opts = Certicoq.make_options l [] "goal" in - let c' = Certicoq.certicoq_eval opts env sigma c [] in + let opts = Certicoq.{ opts with toplevel_name = "goal" } in + let c' = Certicoq.eval opts env sigma c [] in ltac_apply tac (List.map to_ltac_val [EConstr.of_constr c']) end } END