les variables existentielles contiennent maintenant un environnement (type

unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres
le module Environ.


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

6 files changed, 79 insertions, 65 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 37fce80b7e..e6f07410bd 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -26,39 +26,39 @@ let conv_leq_goal env sigma arg ty conclty =
   if not (is_conv_leq env sigma ty conclty) then 
     raise (RefinerError (BadType (arg,ty,conclty)))
 
-let type_of env hyps c =
+let type_of env c =
   failwith "TODO: typage avec VE"
 
 let execute_type env ty =
   failwith "TODO: typage type avec VE"
 
-let rec mk_refgoals env sigma goal goalacc conclty trm =
-  let hyps = goal.evar_hyps in
+let rec mk_refgoals sigma goal goalacc conclty trm =
+  let env = goal.evar_env in
   match trm with
     | DOP0(Meta mv) ->
 	if occur_meta conclty then
           error "Cannot refine to conclusions with meta-variables";
 	let ctxt = goal.evar_info in 
-	(mk_goal ctxt hyps (nf_betaiota env sigma conclty))::goalacc, conclty
+	(mk_goal ctxt env (nf_betaiota env sigma conclty))::goalacc, conclty
 
     | DOP2(Cast,t,ty) ->
-	let _ = type_of env hyps ty in
+	let _ = type_of env ty in
 	conv_leq_goal env sigma trm ty conclty;
-	mk_refgoals env sigma goal goalacc ty t
+	mk_refgoals sigma goal goalacc ty t
 
     | DOPN(AppL,cl) ->
-	let (acc',hdty) = mk_hdgoals env sigma goal goalacc (array_hd cl) in
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc (array_hd cl) in
 	let (acc'',conclty') = 
-	  mk_arggoals env sigma goal acc' hdty (array_list_of_tl cl) in
+	  mk_arggoals sigma goal acc' hdty (array_list_of_tl cl) in
 	let _ = conv_leq_goal env sigma trm conclty' conclty in
         (acc'',conclty')
 
     | DOPN(MutCase _,_) as mc -> 
 	let (_,p,c,lf) = destCase mc in
-	let (acc',lbrty,conclty') = mk_casegoals env sigma goal goalacc p c in
+	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
-            (fun lacc ty fi -> fst (mk_refgoals env sigma goal lacc ty fi))
+            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
             acc' lbrty lf 
 	in
 	let _ = conv_leq_goal env sigma trm conclty' conclty in 
@@ -66,49 +66,51 @@ let rec mk_refgoals env sigma goal goalacc conclty trm =
 
     | t -> 
 	if occur_meta t then raise (RefinerError (OccurMeta t));
-      	let t'ty = type_of env hyps t in
+      	let t'ty = type_of env t in
 	conv_leq_goal env sigma t t'ty conclty;
         (goalacc,t'ty)
 
 (* Same as mkREFGOALS but without knowing te type of the term. Therefore,
  * Metas should be casted. *)
 
-and mk_hdgoals env sigma goal goalacc trm =
-  let hyps = goal.evar_hyps in
+and mk_hdgoals sigma goal goalacc trm =
+  let env = goal.evar_env in
   match trm with
     | DOP2(Cast,DOP0(Meta mv),ty) ->
-	let _ = type_of env hyps ty in
+	let _ = type_of env ty in
 	let ctxt = goal.evar_info in  
-	(mk_goal ctxt hyps (nf_betaiota env sigma ty))::goalacc,ty
+	(mk_goal ctxt env (nf_betaiota env sigma ty))::goalacc,ty
 	  
     | DOPN(AppL,cl) ->
-	let (acc',hdty) = mk_hdgoals env sigma goal goalacc (array_hd cl) in
-	mk_arggoals env sigma goal acc' hdty (array_list_of_tl cl)
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc (array_hd cl) in
+	mk_arggoals sigma goal acc' hdty (array_list_of_tl cl)
 	
     | DOPN(MutCase _,_) as mc -> 
 	let (_,p,c,lf) = destCase mc in
-	let (acc',lbrty,conclty') = mk_casegoals env sigma goal goalacc p c in
+	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
-            (fun lacc ty fi -> fst (mk_refgoals env sigma goal lacc ty fi))
+            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
             acc' lbrty lf 
 	in
 	(acc'',conclty')
 
-    | t -> goalacc,type_of env hyps t
+    | t -> goalacc,type_of env t
 
-and mk_arggoals env sigma goal goalacc funty = function
+and mk_arggoals sigma goal goalacc funty = function
   | [] -> goalacc,funty
   | harg::tlargs ->
+      let env = goal.evar_env in
       (match whd_betadeltaiota env sigma funty with
 	 | DOP2(Prod,c1,b) ->
-	     let (acc',hargty) = mk_refgoals env sigma goal goalacc c1 harg in
-	     mk_arggoals env sigma goal acc' (sAPP b harg) tlargs
+	     let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
+	     mk_arggoals sigma goal acc' (sAPP b harg) tlargs
 	 | t -> raise (RefinerError (CannotApply (t,harg))))
 
-and mk_casegoals env sigma goal goalacc p c= 
-  let (acc',ct) = mk_hdgoals env sigma goal goalacc c in 
-  let (acc'',pt) = mk_hdgoals env sigma goal acc' p in
+and mk_casegoals sigma goal goalacc p c =
+  let env = goal.evar_env in
+  let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
+  let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let (_,lbrty,conclty) = type_case_branches env sigma ct pt p c in
   (acc'',lbrty,conclty)
 
@@ -209,8 +211,9 @@ let move_after with_dep toleft (left,htfrom,right) hto =
     
 (* Primitive tactics are handled here *)
 
-let prim_refiner r env sigma goal =
-  let sign = goal.evar_hyps in
+let prim_refiner r sigma goal =
+  let env = goal.evar_env in
+  let sign = get_globals (context env) in
   let cl = goal.evar_concl in
   let info = goal.evar_info in
   match r with
@@ -221,7 +224,7 @@ let prim_refiner r env sigma goal =
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mk_goal info (add_sign (id,a) sign) (sAPP b v) in 
+	       let sg = mk_goal info (push_var (id,a) env) (sAPP b v) in 
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
@@ -237,8 +240,8 @@ let prim_refiner r env sigma goal =
 		   "Can't introduce at that location: free variable conflict";
 	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mk_goal info 
-			  (add_sign_after whereid (id,a) sign) (sAPP b v) in 
+	       let env' = change_hyps (add_sign_after whereid (id,a)) env in
+	       let sg = mk_goal info env' (sAPP b v) in 
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
@@ -256,8 +259,8 @@ let prim_refiner r env sigma goal =
 		   "Can't introduce at that location: free variable conflict";
 	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mk_goal info (add_sign_replacing id (id,a) sign) 
-			  (sAPP b v) in
+	       let env' = change_hyps (add_sign_replacing id (id,a)) env in
+	       let sg = mk_goal info env' (sAPP b v) in
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
@@ -278,7 +281,7 @@ let prim_refiner r env sigma goal =
      	let _ = check_ind n cl in 
 	if mem_sign sign f then error "name already used in the environment";
         let a = mk_assumption env sign cl in
-        let sg = mk_goal info (add_sign (f,a) sign) cl in
+        let sg = mk_goal info (push_var (f,a) env) cl in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
@@ -307,7 +310,7 @@ let prim_refiner r env sigma goal =
 	      let a = mk_assumption env sign ar in
 	      mk_sign (add_sign (f,a) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
-	      List.map (mk_goal info sign) (cl::lar)
+	      List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
 	in 
 	mk_sign sign (cl::lar,lf,ln)
@@ -330,21 +333,21 @@ let prim_refiner r env sigma goal =
 		error "name already used in the environment";
 	      let a = mk_assumption env sign ar in
 	      mk_sign (add_sign (f,a) sign) (lar',lf')
-	  | ([],[]) -> List.map (mk_goal info sign) (cl::lar)
+	  | ([],[]) -> List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
 	mk_sign sign (cl::lar,lf)
 	  
     | { name = Refine; terms = [c] } ->
 	let c = new_meta_variables c in
-	let (sgl,cl') = mk_refgoals env sigma goal [] cl c in
+	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
 	sgl
 
     | { name = Convert_concl; terms = [cl'] } ->
     	let cl'ty = type_of env sign cl' in
 	if is_conv_leq env sigma cl' cl then
-          let sg = mk_goal info sign (DOP2(Cast,cl',cl'ty)) in
+          let sg = mk_goal info env (DOP2(Cast,cl',cl'ty)) in
           [sg]
 	else 
 	  error "convert-concl rule passed non-converting term"
@@ -353,7 +356,8 @@ let prim_refiner r env sigma goal =
       (* Faut-il garder la sorte d'origine ou celle du converti ?? *)
     	let tj = execute_type env (sign_before id sign) ty' in
 	if is_conv env sigma ty' (snd(lookup_sign id sign)).body then
-          [mk_goal info (modify_sign id tj sign) cl]
+	  let env' = change_hyps (modify_sign id tj) env in
+          [mk_goal info env' cl]
 	else 
 	  error "convert-hyp rule passed non-converting term"
 	    
@@ -376,7 +380,9 @@ let prim_refiner r env sigma goal =
             error ((string_of_id s) ^ " is used in the conclusion.");
           remove_pair s sign 
 	in
-     	let sg = mk_goal info (List.fold_left clear_aux sign ids) cl in
+	let env' = 
+	  change_hyps (fun sign -> List.fold_left clear_aux sign ids) env in
+     	let sg = mk_goal info env' cl in
      	[sg]
 
     | { name = Move withdep; hypspecs = ids } ->
@@ -386,7 +392,8 @@ let prim_refiner r env sigma goal =
   	let (left,right,typfrom,toleft) = split_sign hfrom hto hyps in
   	let hyps' = 
 	  move_after withdep toleft (left,(hfrom,typfrom),right) hto in
-  	[mk_goal info (make_sign hyps') cl]
+	let env' = change_hyps (fun _ -> make_sign hyps') env in
+  	[mk_goal info env' cl]
 	
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index cc9f108ee8..cbab2a90ca 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -9,7 +9,7 @@ open Environ
 open Proof_trees
 (*i*)
 
-val prim_refiner : prim_rule -> unsafe_env -> 'a evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
 
 val prim_extractor : 
   ((typed_type, constr) env -> proof_tree -> constr) -> 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index eb9bc00f83..d12dad6e25 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -7,6 +7,7 @@ open Term
 open Sign
 open Evd
 open Stamps
+open Environ
 
 type bindOcc = 
   | Dep of identifier
@@ -93,9 +94,8 @@ let lc_toList lc = Intset.elements lc
 
 (* Functions on goals *)
 
-let mk_goal ctxt sign cl = 
-  { evar_hyps = sign; evar_concl = cl; evar_body = Evar_empty;
-    evar_info = ctxt }
+let mk_goal ctxt env cl = 
+  { evar_env = env; evar_concl = cl; evar_body = Evar_empty; evar_info = ctxt }
 
 (* Functions on the information associated with existential variables  *)
 
@@ -167,7 +167,7 @@ type global_constraints  = evar_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  sign  : typed_type signature;
+  env   : unsafe_env;
   decls : evar_declarations }
 
 and readable_constraints = evar_recordty timestamped
@@ -175,21 +175,21 @@ and readable_constraints = evar_recordty timestamped
 (* Functions on readable constraints *)
 			     
 let mt_evcty lc gc = 
-  ts_mk { focus = lc; sign = nil_sign; decls = gc }
+  ts_mk { focus = lc; env = empty_env; decls = gc }
 
 let evc_of_evds evds gl = 
-  ts_mk { focus = (get_lc gl); sign = gl.evar_hyps ; decls = evds }
+  ts_mk { focus = (get_lc gl); env = gl.evar_env; decls = evds }
 
 let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl
 		       
 let rc_add evc (k,v) = 
   ts_mod
     (fun evc -> { focus = (Intset.add k evc.focus);
-                  sign  = evc.sign;
+                  env   = evc.env;
                   decls = Evd.add evc.decls k v })
     evc
 
-let get_hyps  evc = (ts_it evc).sign
+let get_env   evc = (ts_it evc).env
 let get_focus evc = (ts_it evc).focus
 let get_decls evc = (ts_it evc).decls
 let get_gc    evc = (ts_mk (ts_it evc).decls)
@@ -197,7 +197,7 @@ let get_gc    evc = (ts_mk (ts_it evc).decls)
 let remap evc (k,v) = 
   ts_mod
     (fun evc -> { focus = evc.focus;
-                  sign  = evc.sign;
+                  env   = evc.env;
                   decls = Evd.add evc.decls k v })
     evc
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 69bc496046..b2d59fe63c 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -8,6 +8,7 @@ open Names
 open Term
 open Sign
 open Evd
+open Environ
 (*i*)
 
 (* This module declares the structure of proof trees, global and
@@ -98,13 +99,13 @@ and ctxtty = {
 type evar_declarations = ctxtty evar_map
 
 
-val mk_goal : ctxtty -> typed_type signature -> constr -> goal
+val mk_goal : ctxtty -> unsafe_env -> constr -> goal
 
 val mt_ctxt    : local_constraints -> ctxtty
-val get_ctxt   : goal  -> ctxtty
+val get_ctxt   : goal -> ctxtty
 val get_pgm    : goal -> constr option
 val set_pgm    : constr option -> ctxtty -> ctxtty
-val get_mimick : goal ->  proof_tree option
+val get_mimick : goal -> proof_tree option
 val set_mimick : proof_tree option ->  ctxtty -> ctxtty
 val get_lc     : goal -> local_constraints
 
@@ -129,14 +130,14 @@ type global_constraints = evar_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  sign  : typed_type signature;
+  env  : unsafe_env;
   decls : evar_declarations }
 
 and readable_constraints = evar_recordty timestamped
 
 val rc_of_gc  : global_constraints -> goal -> readable_constraints
 val rc_add    : readable_constraints -> int * goal -> readable_constraints
-val get_hyps  : readable_constraints -> typed_type signature
+val get_env   : readable_constraints -> unsafe_env
 val get_focus : readable_constraints -> local_constraints
 val get_decls : readable_constraints -> evar_declarations
 val get_gc    : readable_constraints -> global_constraints
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 420af50ec9..4bd5836266 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -23,7 +23,7 @@ type validation_list = proof_tree list -> proof_tree list
 
 type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
 
-let hypotheses gl = gl.evar_hyps
+let hypotheses gl = gl.evar_env
 let conclusion gl = gl.evar_concl
 
 let sig_it x = x.it
@@ -132,9 +132,9 @@ let lookup_tactic s =
 let bad_subproof () =
   errorlabstrm "Refiner.refiner" [< 'sTR"Bad subproof in validation.">]
 
-let refiner env = function
+let refiner = function
   | Prim pr as r ->
-      let prim_fun = prim_refiner pr env in
+      let prim_fun = prim_refiner pr in
       (fun goal_sigma ->
          let sgl = prim_fun (ts_it goal_sigma.sigma) goal_sigma.it in 
 	 ({it=sgl; sigma = goal_sigma.sigma},
@@ -163,7 +163,7 @@ let refiner env = function
   | ((Context ctxt) as r) ->
       (fun goal_sigma ->
          let gl = goal_sigma.it in
-         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
+         let sg = mk_goal ctxt gl.evar_env gl.evar_concl in
          ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
 	     let pf = List.hd pfl in
@@ -179,7 +179,7 @@ let refiner env = function
       (fun goal_sigma ->
          let gl = goal_sigma.it  in
          let ctxt = gl.evar_info in 
-         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
+         let sg = mk_goal ctxt gl.evar_env gl.evar_concl in
 	 ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
 	     let pf = List.hd pfl in
@@ -228,14 +228,14 @@ let extract_open_proof sign pf =
                match lookup_id id vl with
 		 | GLOBNAME _ -> failwith "caught"
 		 | RELNAME(n,_) -> (n,id))
-            (ids_of_sign goal.evar_hyps) in
+            (ids_of_sign (evar_hyps goal)) 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)
+            (fun (_,id) concl ->
+	       let (_,ty) = lookup_sign id (evar_hyps goal) in
+	       mkNamedProd id (incast_type ty) concl)
             sorted_rels goal.evar_concl
 	in
 	let mv = new_meta() in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 3e0b202c26..871c43a3ee 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -2,6 +2,8 @@
 (* $Id$ *)
 
 (*i*)
+open Term
+open Sign
 open Proof_trees
 (*i*)
 
@@ -34,3 +36,7 @@ val hide_tactic :
 
 val overwrite_hidden_tactic : 
   string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
+
+val refiner : rule -> tactic
+
+val extract_open_proof : context -> proof_tree -> constr * (int * constr) list