deuxieme vague de modifs: evar_defs fonctionnel

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

6 files changed, 35 insertions, 132 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 2b33d142f..27ae5ebd9 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -17,6 +17,7 @@ open Termops
 open Sign
 open Environ
 open Evd
+open Evarutil
 open Proof_type
 open Refiner
 open Proof_trees
@@ -69,29 +70,29 @@ let clenv_cast_meta clenv =
   crec
 
 
-let clenv_refine kONT clenv gls =
+let clenv_refine clenv gls =
   tclTHEN
-    (kONT clenv.hook) 
+    (tclEVARS clenv.hook.sigma) 
     (refine (clenv_instance_template clenv)) gls
 
-let clenv_refine_cast kONT clenv gls =
+let clenv_refine_cast clenv gls =
   tclTHEN
-    (kONT clenv.hook) 
+    (tclEVARS clenv.hook.sigma) 
     (refine (clenv_cast_meta clenv (clenv_instance_template clenv)))
     gls
 
-let res_pf kONT clenv gls =
-  clenv_refine kONT (clenv_unique_resolver false clenv gls) gls
+let res_pf clenv gls =
+  clenv_refine (clenv_unique_resolver false clenv gls) gls
     
-let res_pf_cast kONT clenv gls =
-  clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls
+let res_pf_cast clenv gls =
+  clenv_refine_cast (clenv_unique_resolver false clenv gls) gls
 
-let elim_res_pf kONT clenv allow_K gls =
-  clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls
+let elim_res_pf clenv allow_K gls =
+  clenv_refine_cast (clenv_unique_resolver allow_K clenv gls) gls
 
-let elim_res_pf_THEN_i kONT clenv tac gls =  
+let elim_res_pf_THEN_i clenv tac gls =  
   let clenv' = (clenv_unique_resolver true clenv gls) in
-  tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
+  tclTHENLASTn (clenv_refine clenv') (tac clenv') gls
 
 (* [clenv_pose_dependent_evars clenv]
  * For each dependent evar in the clause-env which does not have a value,
@@ -103,7 +104,7 @@ let clenv_pose_dependent_evars clenv =
   let dep_mvs = clenv_dependent false clenv in
   List.fold_left
     (fun clenv mv ->
-       let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in
+       let evar = Evarutil.new_evar_in_sign (get_env clenv.hook) in
        let (evar_n,_) = destEvar evar in
        let tY = clenv_instance_type clenv mv in
        let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in
@@ -111,8 +112,8 @@ let clenv_pose_dependent_evars clenv =
     clenv
     dep_mvs
 
-let e_res_pf kONT clenv gls =
-  clenv_refine kONT
+let e_res_pf clenv gls =
+  clenv_refine
     (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
 
 
@@ -125,9 +126,9 @@ let e_res_pf kONT clenv gls =
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unifyTerms m n gls = 
   let env = pf_env gls in
-  let sigma = project gls in
-  tclIDTAC {it = gls.it; 
-	    sigma = fst (Unification.w_unify false env CONV m n (sigma,Evd.Metamap.empty))}
+  let maps = (create_evar_defs (project gls), Evd.Metamap.empty) in
+  let maps' = Unification.w_unify false env CONV m n maps in
+  tclIDTAC {it = gls.it; sigma = evars_of (fst maps')}
 
 let unify m gls =
   let n = pf_concl gls in unifyTerms m n gls
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 1dd14e773..1695db2f5 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -20,10 +20,9 @@ open Proof_type
 
 (* Tactics *)
 val unify : constr -> tactic
-val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
-val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
-val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
-val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic
-val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
-val elim_res_pf_THEN_i : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
+val clenv_refine : wc clausenv -> tactic
+val res_pf      : wc clausenv -> tactic
+val res_pf_cast : wc clausenv -> tactic
+val elim_res_pf : wc clausenv -> bool -> tactic
+val e_res_pf : wc clausenv -> tactic
+val elim_res_pf_THEN_i : wc clausenv -> (wc clausenv -> tactic array) -> tactic
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d8dfb7d59..2e2060349 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -30,23 +30,10 @@ 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 
@@ -56,76 +43,12 @@ let extract_decl sp evc =
 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 _ = Typing.type_of (get_env wc) wc.sigma 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 *)
 (******************************************)
@@ -151,7 +74,7 @@ let w_refine ev rawc wc =
 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 sigma = wc.sigma in 
   let (sp,evd) (* as evc *) = 
     try
       List.nth (Evarutil.non_instantiated sigma) (n-1) 
@@ -162,5 +85,4 @@ let instantiate_pf_com n com pfts =
   let env = Evarutil.evar_env e_info in
   let rawc = Constrintern.interp_rawconstr sigma env com in 
   let wc' = w_refine sp rawc wc in
-  let newgc = (w_Underlying wc') in
-    change_constraints_pftreestate newgc pfts
+  change_constraints_pftreestate wc'.sigma pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 049c6594e..54646caf8 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -22,7 +22,6 @@ type wc = named_context sigma (* for a better reading of the following *)
 
 (* Refinement of existential variables. *)
 
-val rc_of_pfsigma : proof_tree sigma -> wc
 val rc_of_glsigma : goal sigma -> wc
 
 (* A [w_tactic] is a tactic which modifies the a set of evars of which
@@ -30,28 +29,11 @@ val rc_of_glsigma : goal sigma -> wc
    dependent goal *)
 type w_tactic = wc -> wc
 
-val startWalk : goal sigma -> wc * (wc -> tactic)
-
-val extract_decl : evar -> w_tactic
-val restore_decl : evar -> evar_info -> w_tactic
 val w_Declare    : evar -> types -> w_tactic
-val w_Define     : evar -> constr -> w_tactic
-
-val w_Underlying : wc -> evar_map
-val w_env        : wc -> env
-val w_hyps       : wc -> named_context
-val w_whd        : wc -> constr -> constr
-val w_type_of    : wc -> constr -> constr
-val w_add_sign   : (identifier * types) -> w_tactic
-
-val w_whd_betadeltaiota : wc -> constr -> constr
-val w_hnf_constr        : wc -> constr -> constr
-val w_conv_x            : wc -> constr -> constr -> bool
-val w_const_value       : wc -> constant -> constr
-val w_defined_evar      : wc -> existential_key -> bool
 
 val w_refine :  evar -> Rawterm.rawconstr  -> w_tactic
 
-val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
+val instantiate_pf_com :
+  int -> Topconstr.constr_expr -> pftreestate -> pftreestate
 
 (* the instantiate tactic was moved to tactics/evar_tactics.ml *) 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a0053d8a1..b2629013b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -257,12 +257,6 @@ let vernac_tactic (s,args) =
   let tacfun = lookup_tactic s args in
   abstract_extended_tactic s args tacfun
 
-(* [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 : proof_tree -> constr * (int * constr) list]
   takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
   where pfterm is the constr corresponding to the proof
@@ -1027,3 +1021,6 @@ let tclINFO (tac : tactic) gls =
     msgnl (hov 0 (str "Info failed to apply validation"))
   end;
   res
+
+(* Change evars *)
+let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index f9c0c71d5..f6f65ef93 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -68,6 +68,8 @@ val frontier_mapi :
 val tclIDTAC          : tactic
 val tclIDTAC_MESSAGE  : string -> tactic
 
+(* [tclEVARS sigma] changes the current evar map *)
+val tclEVARS : evar_map -> tactic
 
 (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)