Mise en place de la possibilite d'unfolder des variables locales et des constantes qualifiees

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

3 files changed, 60 insertions, 15 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 909787074..46c4e907d 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -351,8 +351,13 @@ let last_of_cvt_flags (_,red) =
   (if (red_set red BETA) then [ope("Beta",[])]
    else [])@
   (let (n_unf,lconst) = red_get_const red in
-   let lqid = List.map (fun sp -> ast_of_qualid (Global.qualid_of_global 
-              (ConstRef sp))) lconst in
+   let lqid =
+     List.map
+       (function
+	  | EvalVarRef id -> nvar (string_of_id id)
+	  | EvalConstRef sp ->
+	      ast_of_qualid (Global.qualid_of_global (ConstRef sp)))
+       lconst in
    if lqid = [] then []
    else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)]
    else [ope("Delta",[]);ope("Unf",lqid)])@
@@ -368,7 +373,10 @@ let ast_of_cvt_redexp = function
   | Lazy flg -> ope("Lazy",last_of_cvt_flags flg)
   | Unfold l ->
     ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
-      [ast_of_qualid (Global.qualid_of_global (ConstRef sp))]
+      [match sp with
+	| EvalVarRef id -> nvar (string_of_id id)
+	| EvalConstRef sp -> 					
+	    ast_of_qualid (Global.qualid_of_global (ConstRef sp))]
       @(List.map num locc))) l)
   | Fold l ->
     ope("Fold",List.map (fun c -> ope ("COMMAND",
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 8f85384e1..3e81a9e14 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -182,19 +182,35 @@ let overwriting_interp_add (ast_typ,interp_fun) =
 let look_for_interp = Hashtbl.find interp_tab
 
 (* Globalizes the identifier *)
-let glob_const_nvar loc id =
-  let qid = make_qualid [] (string_of_id id) in
+let glob_const_nvar loc env qid =
+  try
+    (* We first look for a variable of the current proof *)
+    match repr_qualid qid with
+      | [],s ->
+	  let id = id_of_string s in
+	  (* lookup_value may raise Not_found *)
+	  (match Environ.lookup_named_value id env with
+	     | Some _ -> EvalVarRef id
+	     | None -> error (s^" does not denote an evaluable constant"))
+      | _ -> raise Not_found
+  with Not_found ->
   try
     match Nametab.locate qid with
-      | ConstRef sp when Environ.evaluable_constant (Global.env ()) sp -> sp
+      | ConstRef sp when Environ.evaluable_constant (Global.env ()) sp ->
+	  EvalConstRef sp
       | VarRef sp when
-	  Environ.evaluable_named_decl (Global.env ()) (basename sp) -> sp
+	  Environ.evaluable_named_decl (Global.env ()) (basename sp) ->
+	  EvalVarRef (basename sp)
       | _ -> error ((string_of_qualid qid) ^
 		    " does not denote an evaluable constant")
-  with
-    | Not_found ->
-	Pretype_errors.error_global_not_found_loc loc qid
+  with Not_found ->
+    Pretype_errors.error_global_not_found_loc loc qid
 
+let qid_interp = function
+  | Node (loc, "QUALIDARG", p) -> interp_qualid p
+  | ast -> 
+      anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",[<'sTR
+        "Unrecognizable qualid ast: "; print_ast ast>])
 
 (* Summary and Object declaration *)
 let mactab = ref Gmap.empty
@@ -1015,10 +1031,15 @@ and cvt_pattern (evc,env,lfun,lmatch,goalopt,debug) = function
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
 
 and cvt_unfold (evc,env,lfun,lmatch,goalopt,debug) = function
-  | Node(loc,"UNFOLD", com::nums) ->
+  | Node(_,"UNFOLD", com::nums) ->
+(*
     (List.map num_of_ast nums,
      glob_const_nvar loc (id_of_Identifier (unvarg (val_interp
        (evc,env,lfun,lmatch,goalopt,debug) com))))
+*)
+      let qid = qid_interp com in
+      (List.map num_of_ast nums, glob_const_nvar loc env qid)
+
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold")
 
 (* Interprets the arguments of Fold *)
@@ -1037,16 +1058,32 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf =
 	(match lf with
 	   | Node(loc,"Unf",l)::lf ->
                let idl=
-		 List.map
-		   (fun v -> glob_const_nvar loc (id_of_Identifier (unvarg
+		 List.fold_right
+		   (fun v red -> 
+		      match glob_const_nvar loc env (qid_interp v) with
+			| EvalVarRef id -> red_add red (VAR id)
+			| EvalConstRef sp -> red_add red (CONST [sp])) l red
+	       in add_flag red lf
+(*
+(id_of_Identifier (unvarg
 		   (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l
 	       in add_flag (red_add red (CONST idl)) lf
+*)
 	   | Node(loc,"UnfBut",l)::lf ->
                let idl=
+		 List.fold_right
+		   (fun v red -> 
+		      match glob_const_nvar loc env (qid_interp v) with
+			| EvalVarRef id -> red_add red (VARBUT id)
+			| EvalConstRef sp -> red_add red (CONSTBUT [sp])) l red
+	       in add_flag red lf
+
+(*
 		 List.map
 		   (fun v -> glob_const_nvar loc (id_of_Identifier (unvarg
                    (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l
                in add_flag (red_add red (CONSTBUT idl)) lf
+*)
 	   | _ -> add_flag (red_add red DELTA) lf)
     | Node(_,"Iota",[])::lf -> add_flag (red_add red IOTA) lf
     | Node(loc,("Unf"|"UnfBut"),l)::_ ->
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a7cf3b6cc..e6cfff531 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -71,8 +71,8 @@ val pf_reduce_to_mind : goal sigma -> constr -> inductive * constr * constr
 val pf_reduce_to_ind  :
   goal sigma  -> constr -> section_path * constr * constr
 val pf_compute        : goal sigma -> constr -> constr
-val pf_unfoldn        : (int list * section_path) list -> goal sigma 
-                        -> constr -> constr
+val pf_unfoldn    : (int list * Closure.evaluable_global_reference) list
+        -> goal sigma -> constr -> constr
 
 val pf_const_value : goal sigma -> constant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool