Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 21 insertions, 160 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index ac4dd43a..4ee8001c 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,183 +6,44 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml,v 1.36.2.2 2004/08/03 21:37:27 herbelin Exp $ *)
+(* $Id: evar_refiner.ml 8654 2006-03-22 15:36:58Z msozeau $ *)
 
-open Pp
 open Util
 open Names
 open Term
-open Environ
 open Evd
 open Sign
-open Reductionops
-open Typing
-open Instantiate
-open Tacred
 open Proof_trees
-open Proof_type
-open Logic
 open Refiner
-open Tacexpr
-open Nameops
-
-
-type wc = named_context sigma (* for a better reading of the following *)
-
-let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
-let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
-
-type w_tactic = named_context sigma -> named_context sigma
-
-let startWalk gls =
-  let evc = project_with_focus gls in
-  (evc,
-   (fun wc' gls' ->
-      if not !Options.debug or (gls.it = gls'.it) then
-(*        if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then*)
-          tclIDTAC {it=gls'.it; sigma = (get_gc wc')}
-(*        else
-          (local_Constraints (get_focus (ids_it wc'))
-             {it=gls'.it; sigma = get_gc (ids_it wc')})*)
-      else error "Walking"))
-
-let extract_decl sp evc =
-  let evdmap = evc.sigma in
-  let evd = Evd.map evdmap sp in 
-    { it = evd.evar_hyps;
-      sigma = Evd.rmv evdmap sp }
-
-let restore_decl sp evd evc =
-  (rc_add evc (sp,evd))
-
-
-(* [w_Focusing sp wt wc]
- *
- * Focuses the walking context WC onto the declaration SP, given that
- * this declaration is UNDEFINED.  Then, it runs the walking_tactic,
- * WT, on this new context.  When the result is returned, we recover
- * the resulting focus (access list) and restore it to SP's declaration.
- *
- * It is an error to cause SP to change state while we are focused on it. *)
-
-(* let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
-                       (wc : named_context sigma) =
-  let hyps  = wc.it
-  and evd   = Evd.map wc.sigma sp in
-  let (wc' : named_context sigma) = extract_decl sp wc in
-  let (wc'',rslt) = wt wc' in 
-(*  if not (ids_eq wc wc'') then error "w_saving_focus"; *)
-  if wc'==wc'' then 
-    wt' rslt wc
-  else 
-    let wc''' = restore_decl sp evd wc'' in 
-    wt' rslt {it = hyps; sigma = wc'''.sigma} *)
-      
-let w_add_sign (id,t) (wc : named_context sigma) =
-  { it = Sign.add_named_decl (id,None,t) wc.it;
-    sigma = wc.sigma }
-
-let w_Focus sp wc = extract_decl sp wc
-
-let w_Underlying wc = wc.sigma
-let w_whd wc c      = Evarutil.whd_castappevar (w_Underlying wc) c
-let w_type_of wc c  =
-  type_of (Global.env_of_context wc.it) wc.sigma c
-let w_env     wc    = get_env wc
-let w_hyps    wc    = named_context (get_env wc)
-let w_defined_evar wc k      = Evd.is_defined (w_Underlying wc) k
-let w_const_value wc         = constant_value (w_env wc)
-let w_conv_x wc m n          = is_conv (w_env wc) (w_Underlying wc) m n
-let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c
-let w_hnf_constr wc c        = hnf_constr (w_env wc) (w_Underlying wc) c
-
-
-let w_Declare sp ty (wc : named_context sigma) =
-  let _ = w_type_of wc ty in (* Utile ?? *)
-  let sign = get_hyps wc in
-  let newdecl = mk_goal sign ty in 
-  ((rc_add wc (sp,newdecl)): named_context sigma)
-
-let w_Define sp c wc =
-  let spdecl = Evd.map (w_Underlying wc) sp in
-  let cty = 
-    try 
-      w_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl))
-    with 
-	Not_found -> error "Instantiation contains unlegal variables"
-      | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> 
-      errorlabstrm "w_Define"
-      (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ 
-       str (string_of_existential sp))
-  in 
-  match spdecl.evar_body with
-    | Evar_empty ->
-    	let spdecl' = { evar_hyps = spdecl.evar_hyps;
-                       	evar_concl = spdecl.evar_concl;
-                       	evar_body = Evar_defined c }
-    	in 
-	  Proof_trees.rc_add wc (sp,spdecl')
-    | _ -> error "define_evar"
-
 
 (******************************************)
 (* Instantiation of existential variables *)
 (******************************************)
 
-(* The instantiate tactic *)
+(* w_tactic pour instantiate *) 
 
-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 w_refine env ev rawc evd =
+  if Evd.is_defined (evars_of evd) ev then 
+    error "Instantiate called on already-defined evar";
+  let e_info = Evd.map (evars_of evd) ev in
+  let env = Evd.evar_env e_info in
+  let sigma,typed_c = 
+    Pretyping.Default.understand_tcc (evars_of evd) env 
+      ~expected_type:e_info.evar_concl rawc in
+  evar_define ev typed_c (evars_reset_evd sigma evd)
 
-let instantiate n c ido gl = 
-  let wc = Refiner.project_with_focus gl in
-  let evl = 
-    match ido with
-	None -> evars_of wc.sigma gl.it.evar_concl 
-      | Some (id,_,_) -> 
-	  let (_,_,typ)=Sign.lookup_named id gl.it.evar_hyps in
-	    evars_of wc.sigma typ in
-    if List.length evl < n then error "not enough evars";
-    let (n,_) as k = destEvar (List.nth evl (n-1)) in 
-      if Evd.is_defined wc.sigma n then 
-	error "Instantiate called on already-defined evar";
-      let wc' = w_Define n c wc in 
-	tclIDTAC {it = gl.it ; 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"
-*)
-
-(* vernac command existential *)
+(* vernac command Existential *)
 
 let instantiate_pf_com n com pfts = 
   let gls = top_goal_of_pftreestate pfts in
-  let wc = project_with_focus gls in
-  let sigma = (w_Underlying wc) in 
-  let (sp,evd) = 
+  let sigma = gls.sigma in 
+  let (sp,evi) (* as evc *) = 
     try
-      List.nth (Evd.non_instantiated sigma) (n-1) 
+      List.nth (Evarutil.non_instantiated sigma) (n-1) 
     with Failure _ -> 
-      error "not so many uninstantiated existential variables"
-      | Invalid_argument _ -> error "incorrect existential variable index"
-  in 
-  let c = Constrintern.interp_constr sigma (Evarutil.evar_env evd) com in     
-  let wc' = w_Define sp c wc in
-  let newgc = (w_Underlying wc') in
-  change_constraints_pftreestate newgc pfts
-
-
+      error "not so many uninstantiated existential variables" in 
+  let env = Evd.evar_env evi in
+  let rawc = Constrintern.intern_constr sigma env com in 
+  let evd = create_evar_defs sigma in
+  let evd' = w_refine env sp rawc evd in
+  change_constraints_pftreestate (evars_of evd') pfts