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

12 files changed, 149 insertions, 68 deletions

diff --git a/CHANGES b/CHANGES
index e87d107361..3b2dcacd4d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -3,9 +3,10 @@ Différences V7.0beta / V7.0
 - Ajout de déclarations locales aux Record (record à la Randy).
 - Correction de bugs (Identity Coercion; Rel not in scope of ?;
   implicits in inductive defs).
-- Prise en compte noms longs dans Hints et Coercions
+- Prise en compte noms longs dans Hints, Coercions et Unfold
 - Rétablissement des @Definition and co
 - Rétablissement des token extensibles et mélangeant symboles et lettres
+- Possibilité de déplier des définitions locales à un but
 
 Différences oubliées dans la V7.0beta :
 
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index c874e135a2..518b98006a 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -365,7 +365,9 @@ let coq_or = lazy (constant ["Init";"Logic"] "or")
 let coq_ex = lazy (constant ["Init";"Logic"] "ex")
 
 (* Section paths for unfold *)
-let make_coq_path dir s = make_path ("Coq"::dir) (id_of_string s) CCI
+open Closure
+let make_coq_path dir s =
+  EvalConstRef (make_path ("Coq"::dir) (id_of_string s) CCI)
 let sp_Zs = make_coq_path ["Zarith";"zarith_aux"] "Zs"
 let sp_Zminus = make_coq_path ["Zarith";"zarith_aux"] "Zminus"
 let sp_Zle = make_coq_path ["Zarith";"zarith_aux"] "Zle"
diff --git a/kernel/closure.ml b/kernel/closure.ml
index e61f949394..d6e4589ca4 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -29,54 +29,61 @@ let stop() =
 	   'sTR" zeta="; 'iNT !zeta; 'sTR" evar="; 'iNT !evar;
            'sTR" iota="; 'iNT !iota; 'sTR" prune="; 'iNT !prune; 'sTR"]" >]
 
+type evaluable_global_reference =
+  | EvalVarRef of identifier
+  | EvalConstRef of section_path
 
 (* [r_const=(true,cl)] means all constants but those in [cl] *)
 (* [r_const=(false,cl)] means only those in [cl] *)
 type reds = {
   r_beta : bool;
-  r_const : bool * constant_path list;
+  r_const : bool * constant_path list * identifier list;
   r_zeta : bool;
   r_evar : bool;
   r_iota : bool }
 
 let betadeltaiota_red = {
   r_beta = true;
-  r_const = true,[];
+  r_const = true,[],[];
   r_zeta = true;
   r_evar = true;
   r_iota = true } 
 
 let betaiota_red = {
   r_beta = true;
-  r_const = false,[];
+  r_const = false,[],[];
   r_zeta = false;
   r_evar = false;
   r_iota = true }
 		     
 let beta_red = {
   r_beta = true;
-  r_const = false,[];
+  r_const = false,[],[];
   r_zeta = false;
   r_evar = false;
   r_iota = false }
 
 let no_red = {
   r_beta = false;
-  r_const = false,[];
+  r_const = false,[],[];
   r_zeta = false;
   r_evar = false;
   r_iota = false }
 
 let betaiotazeta_red = {
   r_beta = true;
-  r_const = false,[];
+  r_const = false,[],[];
   r_zeta = true;
   r_evar = false;
   r_iota = true }
 
-let unfold_red sp = {
+let unfold_red sp =
+  let c = match sp with
+    | EvalVarRef id -> false,[],[id]
+    | EvalConstRef sp -> false,[sp],[]
+  in {
   r_beta = true;
-  r_const = false,[sp];
+  r_const = c;
   r_zeta = true;   (* false for finer behaviour ? *)
   r_evar = false;
   r_iota = true }
@@ -90,25 +97,40 @@ let unfold_red sp = {
 type red_kind =
     BETA | DELTA | ZETA | EVAR | IOTA
   | CONST of constant_path list | CONSTBUT of constant_path list
-  | VAR of identifier
+  | VAR of identifier | VARBUT of identifier
 
 let rec red_add red = function
   | BETA -> { red with r_beta = true }
   | DELTA ->
-      if snd red.r_const <> [] then error "Conflict in the reduction flags";
-      { red with r_const = true,[]; r_zeta = true; r_evar = true }
+      (match red.r_const with
+	| _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags"
+	| _ -> { red with r_const = true,[],[]; r_zeta = true; r_evar = true })
   | CONST cl ->
-      if fst red.r_const then error "Conflict in the reduction flags";
-      { red with r_const = false, list_union cl (snd red.r_const) }
+      (match red.r_const with
+	| true,_,_ -> error "Conflict in the reduction flags"
+	| _,l1,l2 -> { red with r_const = false, list_union cl l1, l2 })
   | CONSTBUT cl ->
-      if not (fst red.r_const) & snd red.r_const <> [] then
-	error "Conflict in the reduction flags";
-      { red with r_const = true, list_union cl (snd red.r_const);
-	  r_zeta = true; r_evar = true }
+      (match red.r_const with
+	| false,_::_,_ | false,_,_::_ ->
+			   error "Conflict in the reduction flags"
+	| _,l1,l2 ->
+	    { red with r_const = true, list_union cl l1, l2;
+		r_zeta = true; r_evar = true })
   | IOTA -> { red with r_iota = true }
   | EVAR -> { red with r_evar = true }
   | ZETA -> { red with r_zeta = true }
-  | VAR id -> red_add red (CONST [make_path [] id CCI])
+  | VAR id ->
+      (match red.r_const with
+	| true,_,_ -> error "Conflict in the reduction flags"
+	| _,l1,l2 -> { red with r_const = false, l1, list_union [id] l2 })
+  | VARBUT cl ->
+      (match red.r_const with
+	| false,_::_,_ | false,_,_::_ ->
+			   error "Conflict in the reduction flags"
+	| _,l1,l2 ->
+	    { red with r_const = true, l1, list_union [cl] l2;
+		r_zeta = true; r_evar = true })
+
 
 let incr_cnt red cnt =
   if red then begin
@@ -117,32 +139,35 @@ let incr_cnt red cnt =
   end else 
     false
 
-let red_local_const red = fst red.r_const
+let red_delta_set red =
+  let b,_,_ = red.r_const in b
+
+let red_local_const = red_delta_set
 
 (* to know if a redex is allowed, only a subset of red_kind is used ... *)
 let red_set red = function
   | BETA -> incr_cnt red.r_beta beta
   | CONST [sp] -> 
-      let (b,l) = red.r_const in
+      let (b,l,_) = red.r_const in
       let c = List.mem sp l in
       incr_cnt ((b & not c) or (c & not b)) delta
   | VAR id -> (* En attendant d'avoir des sp pour les Var *)
-      let (b,l) = red.r_const in
-      let c = List.exists (fun sp -> basename sp = id) l in
+      let (b,_,l) = red.r_const in
+      let c = List.mem id l in
       incr_cnt ((b & not c) or (c & not b)) delta
   | ZETA -> incr_cnt red.r_zeta zeta
   | EVAR -> incr_cnt red.r_zeta evar
   | IOTA -> incr_cnt red.r_iota iota
-  | DELTA -> fst red.r_const  (* Used for Rel/Var defined in context *)
+  | DELTA -> red_delta_set red (*Used for Rel/Var defined in context*)
   (* Not for internal use *)
-  | CONST _ | CONSTBUT _ | VAR _ -> failwith "not implemented"
+  | CONST _ | CONSTBUT _ | VAR _ | VARBUT _ -> failwith "not implemented"
 
 (* Gives the constant list *)
 let red_get_const red =
-  if (fst red.r_const) then
-    (true,snd red.r_const)
-  else
-    (false,snd red.r_const)
+  let b,l1,l2 = red.r_const in
+  let l1' = List.map (fun x -> EvalConstRef x) l1 in
+  let l2' = List.map (fun x -> EvalVarRef x) l2 in
+  b, l1' @ l2'
 
 (* specification of the reduction function *)
 
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 8bb25554b2..e3476db218 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -13,7 +13,9 @@ open Environ
 val stats : bool ref
 val share : bool ref
 
-
+type evaluable_global_reference =
+  | EvalVarRef of identifier
+  | EvalConstRef of section_path
 
 (*s Delta implies all consts (both global (= by
   [section_path]) and local (= by [Rel] or [Var])), all evars, and letin's.
@@ -29,6 +31,7 @@ type red_kind =
   | CONST of section_path list
   | CONSTBUT of section_path list
   | VAR of identifier
+  | VARBUT of identifier
 
 (* Sets of reduction kinds. *)
 type reds
@@ -37,7 +40,7 @@ val no_red : reds
 val beta_red : reds
 val betaiota_red : reds
 val betadeltaiota_red : reds
-val unfold_red : section_path -> reds
+val unfold_red : evaluable_global_reference -> reds
 
 (* Tests if a reduction kind is set *)
 val red_set : reds -> red_kind -> bool
@@ -46,7 +49,7 @@ val red_set : reds -> red_kind -> bool
 val red_add : reds -> red_kind -> reds
 
 (* Gives the constant list *)
-val red_get_const : reds -> bool * (section_path list)
+val red_get_const : reds -> bool * (evaluable_global_reference list)
 
 (*s Reduction function specification. *)
 
@@ -70,7 +73,7 @@ val betaiota : flags
 val betadeltaiota : flags
 
 val hnf_flags : flags
-val unfold_flags : section_path -> flags
+val unfold_flags : evaluable_global_reference -> flags
 
 (*s Explicit substitutions of type ['a]. [ESID n] = %n~END = bounded identity. 
   [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 18a9da82b3..3f8ddf287c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -142,9 +142,9 @@ GEXTEND Gram
     [ [ c = constrarg; l = constrarg_list -> c :: l | -> [] ] ]
   ;
   unfold_occ:
-    [ [ nl = LIST1 pure_numarg; c = identarg ->
+    [ [ nl = LIST1 pure_numarg; c = qualidarg ->
          <:ast< (UNFOLD $c ($LIST $nl)) >>
-      | c = identarg -> <:ast< (UNFOLD $c) >> ] ]
+      | c = qualidarg -> <:ast< (UNFOLD $c) >> ] ]
   ;
   ne_unfold_occ_list:
     [ [ p = unfold_occ; l = ne_unfold_occ_list -> p :: l
@@ -154,8 +154,8 @@ GEXTEND Gram
     [ [ IDENT "Beta" -> <:ast< (Beta) >>
       | IDENT "Delta" -> <:ast< (Delta) >>
       | IDENT "Iota" -> <:ast< (Iota) >>
-      | "["; idl = ne_identarg_list; "]" -> <:ast< (Unf ($LIST idl)) >>
-      | "-"; "["; idl = ne_identarg_list; "]" ->
+      | "["; idl = ne_qualidarg_list; "]" -> <:ast< (Unf ($LIST idl)) >>
+      | "-"; "["; idl = ne_qualidarg_list; "]" ->
           <:ast< (UnfBut ($LIST idl)) >> ] ]
   ;
   red_tactic:
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 715cb798a0..0c5dc14e03 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -482,13 +482,12 @@ let whd_nf env sigma c =
 
 let nf env sigma c = strong whd_nf env sigma c
 
-
 (* linear substitution (following pretty-printer) of the value of name in c.
  * n is the number of the next occurence of name.
  * ol is the occurence list to find. *)
 let rec substlin env name n ol c =
   match kind_of_term c with
-    | IsConst (sp,_ as const) when sp = name ->
+    | IsConst (sp,_ as const) when EvalConstRef sp = name ->
         if List.hd ol = n then
           try 
 	    (n+1, List.tl ol, constant_value env const)
@@ -499,13 +498,13 @@ let rec substlin env name n ol c =
         else 
 	  ((n+1), ol, c)
 
-    | IsVar id when id = basename name ->
+    | IsVar id when EvalVarRef id = name ->
         if List.hd ol = n then
           match lookup_named_value id env with
 	    | Some c -> (n+1, List.tl ol, c)
 	    | None -> 
 		errorlabstrm "substlin"
-		  [< pr_sp name; 'sTR " is not a defined constant" >]
+		  [< pr_id id; 'sTR " is not a defined constant" >]
         else 
 	  ((n+1), ol, c)
 
@@ -586,6 +585,9 @@ let rec substlin env name n ol c =
 let unfold env sigma name =
   clos_norm_flags (unfold_flags name) env sigma
 
+let string_of_evaluable_ref = function
+  | EvalVarRef id -> string_of_id id
+  | EvalConstRef sp -> string_of_qualid (qualid_of_sp sp)
 
 (* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
@@ -597,10 +599,9 @@ let unfoldoccs env sigma (occl,name) c =
     | l -> 
         match substlin env name 1 (Sort.list (<) l) c with
           | (_,[],uc) -> nf_betaiota env sigma uc
-          | (1,_,_) -> error ((string_of_qualid (qualid_of_sp name))
-			      ^" does not occur")
+          | (1,_,_) -> error ((string_of_evaluable_ref name)^" does not occur")
           | _ -> error ("bad occurrence numbers of "
-			^(string_of_qualid (qualid_of_sp name)))
+			^(string_of_evaluable_ref name))
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c = 
@@ -653,7 +654,7 @@ type red_expr =
   | Simpl
   | Cbv of Closure.flags
   | Lazy of Closure.flags
-  | Unfold of (int list * section_path) list
+  | Unfold of (int list * evaluable_global_reference) list
   | Fold of constr list
   | Pattern of (int list * constr * constr) list
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index e17db58c63..df3a0b9736 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -7,6 +7,7 @@ open Term
 open Environ
 open Evd
 open Reduction
+open Closure
 (*i*)
 
 (*s Reduction functions associated to tactics. \label{tacred} *)
@@ -23,7 +24,8 @@ val hnf_constr : 'a reduction_function
 val nf : 'a reduction_function
 
 (* Unfold *)
-val unfoldn : (int list * section_path) list -> 'a reduction_function
+val unfoldn : 
+  (int list * evaluable_global_reference) list -> 'a reduction_function
 
 (* Fold *)
 val fold_commands : constr list -> 'a reduction_function
@@ -53,7 +55,7 @@ type red_expr =
   | Simpl
   | Cbv of Closure.flags
   | Lazy of Closure.flags
-  | Unfold of (int list * section_path) list
+  | Unfold of (int list * evaluable_global_reference) list
   | Fold of constr list
   | Pattern of (int list * constr * constr) list
 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 9097870743..46c4e907d9 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 8f85384e1a..3e81a9e141 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 a7cf3b6ccc..e6cfff5315 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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1080b95092..f532166d05 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -222,8 +222,8 @@ let dyn_reduce = function
 (* Unfolding occurrences of a constant *)
 
 let unfold_constr = function 
-  | ConstRef sp -> unfold_in_concl [[],sp]
-  | VarRef sp -> unfold_in_concl [[],sp]
+  | ConstRef sp -> unfold_in_concl [[],Closure.EvalConstRef sp]
+  | VarRef sp -> unfold_in_concl [[],Closure.EvalVarRef (basename sp)]
   | _ -> errorlabstrm "unfold_constr" [< 'sTR "Cannot unfold a non-constant.">]
 
 (*******************************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9caeafde6e..3d5cf9bad0 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -116,11 +116,13 @@ val simpl_option      : identifier option -> tactic
 val normalise_in_concl: tactic
 val normalise_in_hyp  : identifier        -> tactic
 val normalise_option  : identifier option -> tactic
-val unfold_in_concl   : (int list * section_path) list -> tactic
+val unfold_in_concl   : (int list * Closure.evaluable_global_reference) list
+  -> tactic
 val unfold_in_hyp     : 
-  (int list * section_path) list -> identifier -> tactic
+  (int list * Closure.evaluable_global_reference) list -> identifier -> tactic
 val unfold_option     : 
-  (int list * section_path) list -> identifier option -> tactic
+  (int list * Closure.evaluable_global_reference) list -> identifier option
+    -> tactic
 val reduce            : red_expr -> identifier list -> tactic
 val dyn_reduce        : tactic_arg list -> tactic
 val dyn_change        : tactic_arg list -> tactic