From 940b2f972c4b3f42850e36c721564b127d30e496 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 6 Mar 2018 13:41:37 +0100 Subject: An experimental 'Show Extraction' command (grant feature wish #4129) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms. --- plugins/extraction/extract_env.ml | 21 +++++++++++++++++++-- plugins/extraction/extract_env.mli | 4 ++++ plugins/extraction/extraction.ml | 29 +++++++++++++++++++++++++++-- plugins/extraction/extraction.mli | 2 +- plugins/extraction/g_extraction.ml4 | 6 ++++++ plugins/extraction/table.ml | 7 +++---- 6 files changed, 60 insertions(+), 9 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index e63d04196..c76b2f029 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -576,8 +576,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let reset () = Visit.reset (); reset_tables (); reset_renaming_tables Everything -let init ?(compute=false) modular library = - check_inside_section (); check_inside_module (); +let init ?(compute=false) ?(inner=false) modular library = + if not inner then (check_inside_section (); check_inside_module ()); set_keywords (descr ()).keywords; set_modular modular; set_library library; @@ -747,3 +747,20 @@ let extract_and_compile l = let base = Filename.chop_suffix f ".ml" in let () = remove (base^".cmo"); remove (base^".cmi") in Feedback.msg_notice (str "Extracted code successfully compiled") + +(* Show the extraction of the current ongoing proof *) + +let show_extraction () = + init ~inner:true false false; + let prf = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let trms = Proof.partial_proof prf in + let extr_term t = + let ast, ty = extract_constr env sigma t in + let mp = Lib.current_mp () in + let l = Label.of_id (Proof_global.get_current_proof_name ()) in + let fake_ref = ConstRef (Constant.make2 mp l) in + let decl = Dterm (fake_ref, ast, ty) in + print_one_decl [] mp decl + in + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl extr_term trms) diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 196fa08ee..80c4f2391 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -36,3 +36,7 @@ val print_one_decl : val structure_for_compute : Environ.env -> Evd.evar_map -> EConstr.t -> Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type + +(* Show the extraction of the current ongoing proof *) + +val show_extraction : unit -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a3cf5fbbe..815150f8e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -330,7 +330,21 @@ let rec extract_type env sg db j c args = else extract_type env sg db j (EConstr.mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown - | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false + | Evar _ | Meta _ -> Taxiom (* only possible during Show Extraction *) + | Var v -> + (* For Show Extraction *) + let open Context.Named.Declaration in + (match EConstr.lookup_named v env with + | LocalDef (_,body,_) -> + extract_type env sg db j (EConstr.applist (body,args)) [] + | LocalAssum (_,ty) -> + let r = VarRef v in + (match flag_of_type env sg ty with + | (Logic,_) -> assert false (* Cf. logical cases above *) + | (Info, TypeScheme) -> + extract_type_app env sg db (r, type_sign env sg ty) args + | (Info, Default) -> Tunknown)) + | Cast _ | LetIn _ | Construct _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], @@ -656,7 +670,18 @@ let rec extract_term env sg mle mlt c args = | CoFix (i,recd) -> extract_app env sg mle mlt (extract_fix env sg mle i recd) args | Cast (c,_,_) -> extract_term env sg mle mlt c args - | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false + | Evar _ | Meta _ -> MLaxiom + | Var v -> + (* Only during Show Extraction *) + let open Context.Named.Declaration in + let ty = match EConstr.lookup_named v env with + | LocalAssum (_,ty) -> ty + | LocalDef (_,_,ty) -> ty + in + let vty = extract_type env sg [] 0 ty [] in + let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in + extract_app env sg mle mlt extract_var args + | Ind _ | Prod _ | Sort _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 3a4ba0b34..ec39a2eae 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -29,7 +29,7 @@ val extract_fixpoint : val extract_inductive : env -> MutInd.t -> ml_ind -(** For extraction compute *) +(** For Extraction Compute and Show Extraction *) val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 4b6de58bd..8d268d27c 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -158,3 +158,9 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] -> [ extract_inductive x id idl o ] END +(* Show the extraction of the current proof *) + +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY +| [ "Show" "Extraction" ] + -> [ show_extraction () ] +END diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 5903733a6..730e7b395 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -36,14 +36,13 @@ module Refset' = Refset_env let occur_kn_in_ref kn = function | IndRef (kn',_) | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' - | ConstRef _ -> false - | VarRef _ -> assert false + | ConstRef _ | VarRef _ -> false let repr_of_r = function | ConstRef kn -> Constant.repr3 kn | IndRef (kn,_) | ConstructRef ((kn,_),_) -> MutInd.repr3 kn - | VarRef _ -> assert false + | VarRef v -> KerName.repr (Lib.make_kn v) let modpath_of_r r = let mp,_,_ = repr_of_r r in mp @@ -277,7 +276,7 @@ let safe_basename_of_global r = | ConstructRef ((kn,i),j) -> (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) with Not_found -> last_chance r) - | VarRef _ -> assert false + | VarRef v -> v let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r) -- cgit v1.2.3