Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish #4129)

1 files changed, 41 insertions, 19 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 722b3990c..a4e8c44cd 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -137,22 +137,25 @@ let check_arity env cb =
   let t = cb.const_type in
   if Reduction.is_arity env t then raise Impossible
 
-let check_fix env cb i =
+let get_body lbody =
+  EConstr.of_constr (Mod_subst.force_constr lbody)
+
+let check_fix env sg cb i =
   match cb.const_body with
     | Def lbody ->
-	(match Constr.kind (Mod_subst.force_constr lbody) with
-	  | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
+        (match EConstr.kind sg (get_body lbody) with
+          | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible)
     | Undef _ | OpaqueDef _ -> raise Impossible
 
-let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
+let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) =
   Array.equal Name.equal na1 na2 &&
-  Array.equal Constr.equal ca1 ca2 &&
-  Array.equal Constr.equal ta1 ta2
+  Array.equal (EConstr.eq_constr sg) ca1 ca2 &&
+  Array.equal (EConstr.eq_constr sg) ta1 ta2
 
-let factor_fix env l cb msb =
-  let _,recd as check = check_fix env cb 0 in
+let factor_fix env sg l cb msb =
+  let _,recd as check = check_fix env sg cb 0 in
   let n = Array.length (let fi,_,_ = recd in fi) in
   if Int.equal n 1 then [|l|], recd, msb
   else begin
@@ -163,9 +166,9 @@ let factor_fix env l cb msb =
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
-	       let check' = check_fix env cb' (j+1) in
-	       if not ((fst check : bool) == (fst check') &&
-		   prec_declaration_equal (snd check) (snd check'))
+              let check' = check_fix env sg cb' (j+1) in
+              if not ((fst check : bool) == (fst check') &&
+                        prec_declaration_equal sg (snd check) (snd check'))
 	       then raise Impossible;
 	       labels.(j+1) <- l;
 	   | _ -> raise Impossible) msb';
@@ -248,7 +251,9 @@ and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with
       let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in
       let env' = env_for_mtb_with_def env mp1 me_struct delta idl in
       let mt = extract_mexpr_spec env mp1 (None,me') in
-      (match extract_with_type env' c with (* cb may contain some kn *)
+      let sg = Evd.from_env env in
+      (match extract_with_type env' sg (EConstr.of_constr c) with
+       (* cb may contain some kn *)
 	 | None -> mt
 	 | Some (vl,typ) ->
             type_iter_references Visit.add_ref typ;
@@ -299,12 +304,13 @@ let rec extract_structure env mp reso ~all = function
   | [] -> []
   | (l,SFBconst cb) :: struc ->
       (try
-	 let vl,recd,struc = factor_fix env l cb struc in
+         let sg = Evd.from_env env in
+         let vl,recd,struc = factor_fix env sg l cb struc in
 	 let vc = Array.map (make_cst reso mp) vl in
 	 let ms = extract_structure env mp reso ~all struc in
 	 let b = Array.exists Visit.needed_cst vc in
 	 if all || b then
-	   let d = extract_fixpoint env vc recd in
+           let d = extract_fixpoint env sg vc recd in
 	   if (not b) && (logical_decl d) then ms
 	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms
@@ -572,8 +578,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;
@@ -701,10 +707,9 @@ let flatten_structure struc =
   and flatten_elems l = List.flatten (List.map flatten_elem l)
   in flatten_elems (List.flatten (List.map snd struc))
 
-let structure_for_compute c =
+let structure_for_compute env sg c =
   init false false ~compute:true;
-  let env = Global.env () in
-  let ast, mlt = Extraction.extract_constr env c in
+  let ast, mlt = Extraction.extract_constr env sg c in
   let ast = Mlutil.normalize ast in
   let refs = ref Refset.empty in
   let add_ref r = refs := Refset.add r !refs in
@@ -744,3 +749,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)