Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 55 insertions, 53 deletions

diff --git a/tactics/refine.ml b/tactics/refine.ml
index ff3f0887..cbca38d0 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refine.ml 13129 2010-06-13 14:23:55Z herbelin $ *)
+(* $Id$ *)
 
 (* JCF -- 6 janvier 1998  EXPERIMENTAL *)
 
@@ -16,19 +16,19 @@
  *  où les trous sont typés -- et que les sous-buts correspondants
  *  soient engendrés pour finir la preuve.
  *
- *  Exemple : 
+ *  Exemple :
  *    J'ai le but
- *        (x:nat) { y:nat | (minus y x) = x }
+ *        forall (x:nat), { y:nat | (minus y x) = x }
  *    et je donne la preuve incomplète
- *        [x:nat](exist nat [y:nat]((minus y x)=x) (plus x x) ?)
+ *        fun (x:nat) => exist nat [y:nat]((minus y x)=x) (plus x x) ?
  *    ce qui engendre le but
- *        (minus (plus x x) x)=x
+ *        (minus (plus x x) x) = x
  *)
 
 (*  Pour cela, on procède de la manière suivante :
  *
  *  1. Un terme de preuve incomplet est un terme contenant des variables
- *     existentielles Evar i.e. "?" en syntaxe concrète.
+ *     existentielles Evar i.e. "_" en syntaxe concrète.
  *     La résolution de ces variables n'est plus nécessairement totale
  *     (ise_resolve called with fail_evar=false) et les variables
  *     existentielles restantes sont remplacées par des méta-variables
@@ -38,8 +38,10 @@
  *  2. On met ensuite le terme "à plat" i.e. on n'autorise des MV qu'au
  *     permier niveau et pour chacune d'elles, si nécessaire, on donne
  *     à son tour un terme de preuve incomplet pour la résoudre.
- *     Exemple: le terme (f a ? [x:nat](e ?)) donne
- *         (f a ?1 ?2) avec ?2 => [x:nat]?3 et ?3 => (e ?4)
+ *     Exemple: le terme (f a _ (fun (x:nat) => e _)) donne
+ *         (f a ?1 ?2) avec:
+ *           - ?2 := fun (x:nat) => ?3
+ *           - ?3 := e ?4
  *         ?1 et ?4 donneront des buts
  *
  *  3. On écrit ensuite une tactique tcc qui engendre les sous-buts
@@ -51,6 +53,7 @@ open Util
 open Names
 open Term
 open Termops
+open Namegen
 open Tacmach
 open Sign
 open Environ
@@ -60,7 +63,7 @@ open Tactics
 open Tacticals
 open Printer
 
-type term_with_holes = TH of constr * metamap * sg_proofs
+type term_with_holes = TH of constr * meta_type_map * sg_proofs
 and  sg_proofs       = (term_with_holes option) list
 
 (* pour debugger *)
@@ -70,12 +73,12 @@ let rec pp_th (TH(c,mm,sg)) =
 			      (* pp_mm mm ++ fnl () ++ *)
 			   pp_sg sg) ++ str "]")
 and pp_mm l =
-  hov 0 (prlist_with_sep (fun _ -> (fnl ())) 
+  hov 0 (prlist_with_sep (fun _ -> (fnl ()))
 	   (fun (n,c) -> (int n ++ str" --> " ++ pr_lconstr c)) l)
 and pp_sg sg =
   hov 0 (prlist_with_sep (fun _ -> (fnl ()))
 	   (function None -> (str"None") | Some th -> (pp_th th)) sg)
-     
+
 (*  compute_metamap : constr -> 'a evar_map -> term_with_holes
  *  réalise le 2. ci-dessus
  *
@@ -84,7 +87,7 @@ and pp_sg sg =
  *  par un terme de preuve incomplet (Some c).
  *
  *  On a donc l'INVARIANT suivant : le terme c rendu est "de niveau 1"
- *  -- i.e. à plat -- et la meta_map contient autant d'éléments qu'il y 
+ *  -- i.e. à plat -- et la meta_map contient autant d'éléments qu'il y
  *  a de meta-variables dans c. On suppose de plus que l'ordre dans la
  *  meta_map correspond à celui des buts qui seront engendrés par le refine.
  *)
@@ -101,11 +104,14 @@ let replace_by_meta env sigma = function
 	| Lambda (Anonymous,c1,c2) when isCast c2 ->
 	    let _,_,t = destCast c2 in mkArrow c1 t
 	| _ -> (* (App _ | Case _) -> *)
-	    Retyping.get_type_of_with_meta env sigma mm c
+	    let sigma' =
+	      List.fold_right (fun (m,t) sigma -> Evd.meta_declare m t sigma)
+		mm sigma in
+	    Retyping.get_type_of env sigma' c
 	(*
 	| Fix ((_,j),(v,_,_)) ->
 	    v.(j) (* en pleine confiance ! *)
-	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" 
+	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
         *)
       in
       if occur_meta ty then
@@ -119,28 +125,28 @@ let replace_in_array keep_length env sigma a =
     raise NoMeta;
   let a' = Array.map (function
 			| (TH (c,mm,[])) when not keep_length -> c,mm,[]
-			| th -> replace_by_meta env sigma th) a 
+			| th -> replace_by_meta env sigma th) a
   in
   let v' = Array.map pi1 a' in
   let mm = Array.fold_left (@) [] (Array.map pi2 a') in
   let sgp = Array.fold_left (@) [] (Array.map pi3 a') in
   v',mm,sgp
-    
+
 let fresh env n =
   let id = match n with Name x -> x | _ -> id_of_string "_H" in
-  next_global_ident_away true id (ids_of_named_context (named_context env))
+  next_ident_away_in_goal id (ids_of_named_context (named_context env))
 
 let rec compute_metamap env sigma c = match kind_of_term c with
   (* le terme est directement une preuve *)
   | (Const _ | Evar _ | Ind _ | Construct _ |
-    Sort _ | Var _ | Rel _) -> 
+    Sort _ | Var _ | Rel _) ->
       TH (c,[],[])
 
   (* le terme est une mv => un but *)
   | Meta n ->
       TH (c,[],[None])
 
-  | Cast (m,_, ty) when isMeta m -> 
+  | Cast (m,_, ty) when isMeta m ->
       TH (c,[destMeta m,ty],[None])
 
 
@@ -153,7 +159,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
       begin match compute_metamap env' sigma (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
-	(* terme de preuve incomplet *)    
+	(* terme de preuve incomplet *)
 	| th ->
 	    let m,mm,sgp = replace_by_meta env' sigma th in
 	    TH (mkLambda (Name v,c1,m), mm, sgp)
@@ -167,13 +173,13 @@ let rec compute_metamap env sigma c = match kind_of_term c with
       begin match th1,th2 with
 	(* terme de preuve complet *)
 	| TH (_,_,[]), TH (_,_,[]) -> TH (c,[],[])
-	(* terme de preuve incomplet *)    
+	(* terme de preuve incomplet *)
 	| TH (c1,mm1,sgp1), TH (c2,mm2,sgp2) ->
 	    let m1,mm1,sgp1 =
-              if sgp1=[] then (c1,mm1,[]) 
+              if sgp1=[] then (c1,mm1,[])
               else replace_by_meta env sigma th1 in
 	    let m2,mm2,sgp2 =
-              if sgp2=[] then (c2,mm2,[]) 
+              if sgp2=[] then (c2,mm2,[])
               else replace_by_meta env' sigma th2 in
 	    TH (mkNamedLetIn v m1 t1 m2, mm1@mm2, sgp1@sgp2)
       end
@@ -214,7 +220,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
       let env' = push_named_rec_types (fi',ai,v) env in
       let a = Array.map
 		(compute_metamap env' sigma)
-		(Array.map (substl (List.map mkVar (Array.to_list vi))) v) 
+		(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
       in
       begin
 	try
@@ -224,12 +230,12 @@ let rec compute_metamap env sigma c = match kind_of_term c with
 	with NoMeta ->
 	  TH (c,[],[])
       end
-	      
+
   (* Cast. Est-ce bien exact ? *)
   | Cast (c,_,t) -> compute_metamap env sigma c
       (*let TH (c',mm,sgp) = compute_metamap sign c in
 	TH (mkCast (c',t),mm,sgp) *)
-      
+
   (* Produit. Est-ce bien exact ? *)
   | Prod (_,_,_) ->
       if occur_meta c then
@@ -244,7 +250,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
       let env' = push_named_rec_types (fi',ai,v) env in
       let a = Array.map
 		(compute_metamap env' sigma)
-		(Array.map (substl (List.map mkVar (Array.to_list vi))) v) 
+		(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
       in
       begin
 	try
@@ -257,7 +263,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
 
 
 (*  tcc_aux : term_with_holes -> tactic
- * 
+ *
  *  Réalise le 3. ci-dessus
  *)
 
@@ -270,11 +276,11 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 
     | Cast (c,_,_), _ when isMeta c ->
 	tclIDTAC gl
-	  
+
     (* terme pur => refine *)
     | _,[] ->
 	refine c gl
-	
+
     (* abstraction => intro *)
     | Lambda (Name id,_,m), _ ->
 	assert (isMeta (strip_outer_cast m));
@@ -282,18 +288,18 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 	  | [None] -> intro_mustbe_force id gl
 	  | [Some th] ->
               tclTHEN (introduction id)
-                (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)) gl
+                (onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)) gl
 	  | _ -> assert false
 	end
 
     | Lambda (Anonymous,_,m), _ -> (* if anon vars are allowed in evars *)
         assert (isMeta (strip_outer_cast m));
 	begin match sgp with
-	  | [None] -> tclTHEN intro (onLastHyp (fun id -> clear [id])) gl
+	  | [None] -> tclTHEN intro (onLastHypId (fun id -> clear [id])) gl
 	  | [Some th] ->
               tclTHEN
                 intro
-                (onLastHyp (fun id -> 
+                (onLastHypId (fun id ->
                   tclTHEN
                     (clear [id])
                     (tcc_aux (mkVar (*dummy*) id::subst) th))) gl
@@ -304,29 +310,29 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
     | LetIn (Name id,c1,t1,c2), _ when not (isMeta (strip_outer_cast c1)) ->
 	let c = pf_concl gl in
 	let newc = mkNamedLetIn id c1 t1 c in
-	tclTHEN 
-	  (change_in_concl None newc) 
-	  (match sgp with 
+	tclTHEN
+	  (change_in_concl None newc)
+	  (match sgp with
 	     | [None] -> introduction id
 	     | [Some th] ->
                  tclTHEN (introduction id)
-                   (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th))
-	     | _ -> assert false) 
+                   (onLastHypId (fun id -> tcc_aux (mkVar id::subst) th))
+	     | _ -> assert false)
 	  gl
 
     (* let in with holes in the body => unable to handle dependency
        because of evars limitation, use non dependent assert instead *)
     | LetIn (Name id,c1,t1,c2), _ ->
 	tclTHENS
-          (assert_tac (Name id) t1) 
-	  [(match List.hd sgp with 
+          (assert_tac (Name id) t1)
+	  [(match List.hd sgp with
 	     | None -> tclIDTAC
-	     | Some th -> onLastHyp (fun id -> tcc_aux (mkVar id::subst) th));
-           (match List.tl sgp with 
+	     | Some th -> onLastHypId (fun id -> tcc_aux (mkVar id::subst) th));
+           (match List.tl sgp with
 	     | [] -> refine (subst1 (mkVar id) c2)  (* a complete proof *)
 	     | [None] -> tclIDTAC                   (* a meta *)
 	     | [Some th] ->                         (* a partial proof *)
-                 onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)
+                 onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)
              | _ -> assert false)]
           gl
 
@@ -339,10 +345,9 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 	let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
 	let firsts,lasts = list_chop j (Array.to_list fixes) in
 	tclTHENS
-	  (mutual_fix_with_index 
-	    (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
+	  (mutual_fix (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
-		       | None -> tclIDTAC 
+		       | None -> tclIDTAC
 		       | Some th -> tcc_aux subst th) sgp)
 	  gl
 
@@ -355,9 +360,9 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 	let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
 	let firsts,lasts = list_chop j (Array.to_list cofixes) in
 	tclTHENS
-	  (mutual_cofix_with_index (out_name fi.(j)) (firsts@List.tl lasts) j)
+	  (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
-		       | None -> tclIDTAC 
+		       | None -> tclIDTAC
 		       | Some th -> tcc_aux subst th) sgp)
 	  gl
 
@@ -374,13 +379,10 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 
 let refine (evd,c) gl =
   let sigma = project gl in
-  let evd = Evd.evars_of (Typeclasses.resolve_typeclasses
-			     ~onlyargs:true ~fail:false (pf_env gl) 
-			     (Evd.create_evar_defs evd)) 
-  in
+  let evd = Typeclasses.resolve_typeclasses ~onlyargs:true (pf_env gl) evd in
   let c = Evarutil.nf_evar evd c in
   let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
-  (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise 
+  (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
      complicated to update meta types when passing through a binder *)
   let th = compute_metamap (pf_env gl) evd c in
   tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl