more evar stuff

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

6 files changed, 117 insertions, 8 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
new file mode 100644
index 000000000..7efa9299e
--- /dev/null
+++ b/tactics/evar_tactics.ml
@@ -0,0 +1,70 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Util
+open Evar_refiner
+open Tacmach
+open Tacexpr
+open Proof_type
+open Evd
+
+(* The instantiate tactic *)
+
+let evars_of evc c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
+    | _ -> fold_constr evrec acc c
+  in 
+    evrec [] c
+let instantiate n rawc ido gl = 
+  let wc = Refiner.project_with_focus gl in
+  let evl = 
+    match ido with
+	ConclLocation () -> evars_of wc.sigma gl.it.evar_concl 
+      | HypLocation (id,hloc) ->
+	  let decl = Sign.lookup_named id gl.it.evar_hyps in
+	    match hloc with
+		InHyp ->  
+		  (match decl with 
+		       (_,None,typ) -> evars_of wc.sigma typ
+		     | _ -> error 
+			 "please be more specific : in type or value ?")
+	      | InHypTypeOnly ->
+		  let (_, _, typ) = decl in evars_of wc.sigma typ
+	      | InHypValueOnly ->
+		  (match decl with 
+		       (_,Some body,_) -> evars_of wc.sigma body
+		     | _ -> error "not a let .. in  hypothesis") in
+    if List.length evl < n then error "not enough uninstantiated evars";
+    let ev,_ =  destEvar (List.nth evl (n-1)) in
+    let wc' = w_refine ev rawc wc in
+      Tacticals.tclIDTAC {gl with sigma = wc'.sigma}
+	
+(*
+let pfic gls c =
+  let evc = gls.sigma in 
+  Constrintern.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
+
+let instantiate_tac = function
+  | [Integer n; Command com] ->
+      (fun gl -> instantiate n (pfic gl com) gl)
+  | [Integer n; Constr c] ->
+      (fun gl -> instantiate n c gl)
+  | _ -> invalid_arg "Instantiate called with bad arguments"
+*)
+
+let let_evar nam typ gls =
+  let wc = Refiner.project_with_focus gls in
+  let sp = Evarutil.new_evar () in
+  let wc' = w_Declare sp typ wc in
+  let ngls = {gls with sigma = wc'.sigma} in
+    Tactics.forward true nam (mkEvar(sp,[||])) ngls 
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
new file mode 100644
index 000000000..df3da392c
--- /dev/null
+++ b/tactics/evar_tactics.mli
@@ -0,0 +1,22 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Tacmach
+open Names
+open Tacexpr
+
+val instantiate : int -> Rawterm.rawconstr -> 
+  (identifier * hyp_location_flag, unit) location -> tactic
+
+(*
+val instantiate_tac : tactic_arg list -> tactic
+*)
+
+val let_evar : name -> Term.types -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index daf3bb465..e55df2bf1 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -231,6 +231,17 @@ TACTIC EXTEND Subst
 | [ "Subst" ] -> [ subst_all ]
 END
 
+open Evar_tactics
+
+(* evar creation *)
+
+TACTIC EXTEND Evar
+ [ "Evar" "(" ident(id) ":" constr(typ) ")" ] ->
+    [ let_evar (Names.Name id) typ ]
+| [ "Evar" constr(typ) ] ->
+    [ let_evar Names.Anonymous typ ]
+END
+
 (** Nijmegen "step" tactic for setoid rewriting *)
 
 open Tacticals
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 21f7d43fc..8afdae999 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -47,8 +47,8 @@ let h_generalize cl  = abstract_tactic (TacGeneralize cl) (generalize cl)
 let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
 let h_let_tac na c cl =
   abstract_tactic (TacLetTac (na,c,cl)) (letin_tac true na c cl)
-let h_instantiate n c cls = 
-(Evar_refiner.instantiate n c (simple_clause_of cls))
+let h_instantiate n c ido = 
+(Evar_tactics.instantiate n c ido)
   (* abstract_tactic (TacInstantiate (n,c,cls))
     (Evar_refiner.instantiate n c (simple_clause_of cls)) *)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 90a2d1b3c..f03e4b755 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -50,8 +50,8 @@ val h_generalize      : constr list -> tactic
 val h_generalize_dep  : constr -> tactic 
 val h_forward         : bool -> name -> constr -> tactic 
 val h_let_tac         : name -> constr -> Tacticals.clause -> tactic
-val h_instantiate     : int -> Rawterm.rawconstr -> 
-  Tacticals.clause -> tactic
+val h_instantiate     : int -> Rawterm.rawconstr ->
+  (identifier * hyp_location_flag, unit) location -> tactic
 
 (* Derived basic tactics *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3c2e05f0a..2b2f39e1e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -663,9 +663,12 @@ let rec intern_atomic lf ist x =
       let na = intern_name lf ist na in
       TacLetTac (na,intern_constr ist c,
                  (clause_app (intern_hyp_location ist) cls))
-  | TacInstantiate (n,c,cls) -> 
+  | TacInstantiate (n,c,idh) -> 
       TacInstantiate (n,intern_constr ist c,
-		      (clause_app (intern_hyp_location ist) cls))
+		      (match idh with
+			   ConclLocation () -> ConclLocation ()
+			 | HypLocation (id,hloc) -> 
+			      HypLocation(intern_hyp_or_metaid ist id,hloc)))
 
   (* Automation tactics *)
   | TacTrivial l -> TacTrivial l
@@ -1714,9 +1717,12 @@ and interp_atomic ist gl = function
   | TacLetTac (na,c,clp) ->
       let clp = interp_clause ist gl clp in
       h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp
-  | TacInstantiate (n,c,ido) -> h_instantiate n (fst c) 
+  | TacInstantiate (n,c,idh) -> h_instantiate n (fst c) 
       (* pf_interp_constr ist gl c *)
-      (clause_app (interp_hyp_location ist gl) ido)
+      (match idh with
+	   ConclLocation () -> ConclLocation ()
+	 | HypLocation (id,hloc) -> 
+	     HypLocation(interp_hyp ist gl id,hloc))
 
   (* Automation tactics *)
   | TacTrivial l -> Auto.h_trivial l