mise en place module Refiner

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@107 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 86 insertions, 16 deletions

diff --git a/lib/util.ml b/lib/util.ml
index be6f67dc16..440acd6ba2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -125,6 +125,8 @@ let list_for_all_i p =
 
 let list_except x l = List.filter (fun y -> not (x = y)) l
 
+let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
+
 (* Arrays *)
 
 let array_exists f v = 
@@ -262,6 +264,13 @@ let option_app f = function
   | None -> None
   | Some x -> Some (f x)
 
+let map_succeed f = 
+  let rec map_f = function 
+    | [] -> []
+    |  h::t -> try (let x = f h in x :: map_f t) with Failure _ -> map_f t
+  in 
+  map_f 
+
 (* Pretty-printing *)
   
 let pr_spc () = [< 'sPC >];;
diff --git a/lib/util.mli b/lib/util.mli
index 484b2d61e7..ef56afeb27 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -40,6 +40,7 @@ val list_index : 'a -> 'a list -> int
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
+val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 
 (*s Arrays. *)
 
@@ -78,6 +79,8 @@ module Intmap : Map.S with type key = int
 val out_some : 'a option -> 'a
 val option_app : ('a -> 'b) -> 'a option -> 'b option
 
+val map_succeed : ('a -> 'b) -> 'a list -> 'b list
+
 (*s Pretty-printing. *)
 
 val pr_spc : unit -> std_ppcmds
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6125dec8be..420af50ec9 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -4,7 +4,11 @@
 open Pp
 open Util
 open Stamps
+open Generic
+open Term
+open Sign
 open Evd
+open Environ
 open Proof_trees
 open Logic
 
@@ -128,34 +132,29 @@ let lookup_tactic s =
 let bad_subproof () =
   errorlabstrm "Refiner.refiner" [< 'sTR"Bad subproof in validation.">]
 
-let refiner = function
-  | Prim pr ->
-      let prim_fun = prim_refiner pr in
+let refiner env = function
+  | Prim pr as r ->
+      let prim_fun = prim_refiner pr env in
       (fun goal_sigma ->
-         let sgl = 
-           (try prim_fun (ts_it goal_sigma.sigma) goal_sigma.it
-            with UserError _ as e -> raise e
-              | e -> (mSGNL(Errors.explain_user_exn e);
-                      Errors.reraise_user_exn e))
-	 in 
+         let sgl = prim_fun (ts_it goal_sigma.sigma) goal_sigma.it in 
 	 ({it=sgl; sigma = goal_sigma.sigma},
           (fun pfl ->
-             if not (for_all2eq (fun g pf -> g = pf.goal) sgl pfl) then
+             if not (list_for_all2eq (fun g pf -> g = pf.goal) sgl pfl) then
 	       bad_subproof ();
              { status = and_status (List.map pf_status pfl);
                goal = goal_sigma.it;
                subproof = None;
                ref = Some(r,pfl) })))
       
-  | Tactic(s,targs) ->
+  | Tactic(s,targs) as r ->
       let tacfun = lookup_tactic s targs in
       (fun goal_sigma ->
          let (sgl_sigma,v) = tacfun goal_sigma in
          let hidden_proof = v (List.map leaf sgl_sigma.it) in
          (sgl_sigma,
           fun spfl ->
-            if not (for_all2eq (fun g pf -> g=pf.goal) sgl_sigma.it spfl) then
-	      bad_subproof ();
+            if not (list_for_all2eq (fun g pf -> g=pf.goal) sgl_sigma.it spfl)
+	    then bad_subproof ();
             { status = and_status (List.map pf_status spfl);
               goal = goal_sigma.it;
               subproof = Some hidden_proof;
@@ -164,7 +163,7 @@ let refiner = function
   | ((Context ctxt) as r) ->
       (fun goal_sigma ->
          let gl = goal_sigma.it in
-         let sg = mk_goal ctxt gl.hyps gl.concl in
+         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
          ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
 	     let pf = List.hd pfl in
@@ -179,8 +178,8 @@ let refiner = function
   | ((Local_constraints lc) as r) ->
       (fun goal_sigma ->
          let gl = goal_sigma.it  in
-         let ctxt = outSOME gl.info in 
-         let sg = mkGOAL ctxt gl.hyps gl.concl in
+         let ctxt = gl.evar_info in 
+         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
 	 ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
 	     let pf = List.hd pfl in
@@ -189,3 +188,62 @@ let refiner = function
                goal = gl;
                subproof = None;
                ref = Some(r,[pf]) })))
+
+(* rc_of_pfsigma : proof sigma -> readable_constraints *)
+let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
+
+(* rc_of_glsigma : proof sigma -> readable_constraints *)
+let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
+
+(* extract_open_proof : constr signature -> proof
+  -> constr * (int * constr) list
+  takes a constr signature corresponding to global definitions
+  and a (not necessarly complete) proof
+  and gives a pair (pfterm,obl)
+  where pfterm is the constr corresponding to the proof
+  and obl is an int*constr list [ (m1,c1) ; ... ; (mn,cn)]
+  where the mi are metavariables numbers, and ci are their types.
+  Their proof should be completed in order to complete the initial proof *)
+
+let extract_open_proof sign pf =
+  let open_obligations = ref [] in
+  let rec proof_extractor vl = function
+    | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
+	  
+    | {ref=Some(Tactic _,spfl); subproof=Some hidden_proof} ->
+	let sgl,v = frontier hidden_proof in
+	let flat_proof = v spfl in
+	proof_extractor vl flat_proof
+	  
+    | {ref=Some(Context ctxt,[pf])} -> (proof_extractor vl) pf
+	  
+    | {ref=Some(Local_constraints lc,[pf])} -> (proof_extractor vl) pf
+	  
+    | {ref=None;goal=goal} ->
+	let rel_env = get_rels vl in
+	let n_rels = List.length rel_env in
+	let visible_rels =
+          map_succeed
+            (fun id ->
+               match lookup_id id vl with
+		 | GLOBNAME _ -> failwith "caught"
+		 | RELNAME(n,_) -> (n,id))
+            (ids_of_sign goal.evar_hyps) in
+	let sorted_rels = 
+	  Sort.list (fun (n1,_) (n2,_) -> n1>n2) visible_rels in
+	let abs_concl =
+          List.fold_right
+            (fun (_,id) concl -> 
+	       mkNamedProd id (incast_type (snd(lookup_sign id goal.evar_hyps))) 
+		 concl)
+            sorted_rels goal.evar_concl
+	in
+	let mv = new_meta() in
+	open_obligations := (mv,abs_concl):: !open_obligations;
+	applist(DOP0(Meta mv),List.map (fun (n,_) -> Rel n) sorted_rels) 
+	  
+    | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
+  in
+  let pfterm = proof_extractor (gLOB sign) pf in
+  (pfterm, List.rev !open_obligations)
+