An experimental 'Show Extraction' command (grant feature wish #4129)

 Attempt to extract the current ongoing proof (request by
 Clément Pit-Claudel on coqdev, and also #4129).
 Evars are handled as axioms.

6 files changed, 60 insertions, 9 deletions

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)