Généralisation de with_occurrence (ex occurrence) et de red_expr pour permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern

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

6 files changed, 47 insertions, 49 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 60a00df3df..fc5fc82f7e 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -23,7 +23,7 @@ type let_clause_kind =
   | LETCLAUSE of
       (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
 
-let fail_default_value = Genarg.ArgArg 0
+let fail_default_value = ArgArg 0
 
 let out_letin_clause loc = function
   | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index dd04506ca1..9a4995c03a 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -121,8 +121,8 @@ GEXTEND Gram
   simple_intropattern;
 
   int_or_var:
-    [ [ n = integer  -> Genarg.ArgArg n
-      | id = identref -> Genarg.ArgVar id ] ]
+    [ [ n = integer  -> Rawterm.ArgArg n
+      | id = identref -> Rawterm.ArgVar id ] ]
   ;
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
@@ -155,11 +155,11 @@ GEXTEND Gram
   conversion:
     [ [ c = constr -> (None, c)
       | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
-      | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr ->
+      | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr ->
 	  (Some (nl,c1), c2) ] ]
   ;
   occurrences:
-    [ [ "at"; nl = LIST1 integer -> nl
+    [ [ "at"; nl = LIST1 int_or_var -> nl
       | -> [] ] ]
   ;
   pattern_occ:
@@ -240,7 +240,7 @@ GEXTEND Gram
     ] ]
   ;
   hypident_occ:
-    [ [ (id,l)=hypident; occs=occurrences -> (id,occs,l) ] ]
+    [ [ (id,l)=hypident; occs=occurrences -> ((occs,id),l) ] ]
   ;
   clause:
     [ [ "in"; "*"; occs=occurrences ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 9a6f379b3a..e51b1fecba 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -153,8 +153,8 @@ let pr_lname = function
   | lna -> pr_located pr_name lna
 
 let pr_or_var pr = function
-  | Genarg.ArgArg x -> pr x
-  | Genarg.ArgVar (loc,s) -> pr_lident (loc,s)
+  | ArgArg x -> pr x
+  | ArgVar (loc,s) -> pr_lident (loc,s)
 
 let pr_prim_token = function
   | Numeral n -> Bigint.pr_bigint n
@@ -625,15 +625,10 @@ let pr_cases_pattern_expr = pr_patt ltop
 
 let pr_binders = pr_undelimited_binders (pr ltop)
 
-let pr_pattern_occ prc = function
-    ([],c) -> prc c
-  | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++
-                     hov 0 (prlist_with_sep spc int nl))
-
-let pr_unfold_occ pr_ref = function
-    ([],qid) -> pr_ref qid
-  | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++
-                       hov 0 (prlist_with_sep spc int nl))
+let pr_with_occurrences pr = function
+    ([],c) -> pr c
+  | (nl,c) -> hov 1 (pr c ++ spc() ++ str"at " ++
+                     hov 0 (prlist_with_sep spc (pr_or_var int) nl))
 
 let pr_red_flag pr r =
   (if r.rBeta then pr_arg str "beta" else mt ()) ++
@@ -653,7 +648,7 @@ let pr_metaid id = str"?" ++ pr_id id
 let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | Red false -> str "red"
   | Hnf -> str "hnf"
-  | Simpl o -> str "simpl" ++ pr_opt (pr_pattern_occ pr_constr) o  
+  | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o  
   | Cbv f ->
       if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
 	str "compute"
@@ -663,11 +658,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
       hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
   | Unfold l ->
       hov 1 (str "unfold" ++ spc() ++
-             prlist_with_sep pr_coma (pr_unfold_occ pr_ref) l)
+             prlist_with_sep pr_coma (pr_with_occurrences pr_ref) l)
   | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
   | Pattern l ->
       hov 1 (str "pattern" ++
-        pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l)
+        pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l)
         
   | Red true -> error "Shouldn't be accessible from user"
   | ExtraRedExpr s -> str s
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index e7e8a4bbc0..1cafe28005 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -53,11 +53,13 @@ val pr_id : identifier -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
 
+val pr_with_occurrences :
+  ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
 val pr_red_expr :
-  ('a -> std_ppcmds) * ('a -> std_ppcmds) *  ('b -> std_ppcmds) ->
+  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
     ('a,'b) red_expr_gen -> std_ppcmds
 val pr_may_eval :
-  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+  ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> 
     ('a,'b) may_eval -> std_ppcmds
 
 val pr_rawsort : rawsort -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d5a94cd179..2f86ac94cf 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -142,8 +142,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
   | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x)
   | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_arg (pr_may_eval prc prlc prref)
-        (out_gen rawwit_constr_may_eval x)
+      pr_arg (pr_may_eval prc prlc prref) (out_gen rawwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
@@ -186,7 +185,8 @@ let rec pr_glob_generic prc prlc prtac x =
   | ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
   | ConstrMayEvalArgType ->
       pr_arg (pr_may_eval prc prlc
-        (pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x)
+        (pr_or_var (pr_and_short_name pr_evaluable_reference)))
+        (out_gen globwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
   | RedExprArgType ->
@@ -381,17 +381,14 @@ let pr_by_tactic prt = function
   | TacId [] -> mt ()
   | tac -> spc() ++ str "by " ++ prt tac
 
-let pr_occs pp = function
-    [] -> pp
-  | nl -> hov 1 (pp ++ spc() ++ str"at " ++
-                 hov 0 (prlist_with_sep spc int nl))
-
 let pr_hyp_location pr_id = function
-  | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs
-  | id, occs, InHypTypeOnly ->
-      spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs
-  | id, occs, InHypValueOnly ->
-      spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs
+  | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+  | occs, InHypTypeOnly ->
+      spc () ++ 
+      pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
+  | occs, InHypValueOnly ->
+      spc () ++ 
+      pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
 
 let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
 
@@ -401,11 +398,11 @@ let pr_simple_clause pr_id = function
 
 let pr_clauses pr_id = function
     { onhyps=None; onconcl=true; concl_occs=nl } ->
-      pr_in (pr_occs (str " *") nl)
+      pr_in (pr_with_occurrences (fun () -> str " *") (nl,()))
   | { onhyps=None; onconcl=false } -> pr_in (str " * |-")
   | { onhyps=Some l; onconcl=true; concl_occs=nl } -> 
       pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l
-             ++ pr_occs (str" |- *") nl)
+             ++ pr_with_occurrences (fun () -> str" |- *") (nl,()))
   | { onhyps=Some l; onconcl=false } ->
       pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l)
 
@@ -779,7 +776,8 @@ and pr_atom1 env = function
         | Some([],c1) -> hov 1 (pr_constr env c1 ++ spc() ++ str "with ")
         | Some(ocl,c1) ->
             hov 1 (pr_constr env c1 ++ spc() ++
-	           str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++
+	           str "at " ++ prlist_with_sep spc (pr_or_var int) ocl) ++
+                   spc() ++
 	           str "with ") ++
       pr_constr env c ++ pr_clauses pr_ident h)
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index b05895666f..2cc30f5edd 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -77,20 +77,22 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
 let mlexpr_of_loc loc = <:expr< $dloc$ >>
 
 let mlexpr_of_or_var f = function
-  | Genarg.ArgArg x -> <:expr< Genarg.ArgArg $f x$ >>
-  | Genarg.ArgVar id -> <:expr< Genarg.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
+  | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >>
+  | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
 
 let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
 
-let mlexpr_of_occs = mlexpr_of_list mlexpr_of_int
+let mlexpr_of_occs = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)
+
+let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
 
 let mlexpr_of_hyp_location = function
-  | id, occs, Tacexpr.InHyp ->
-      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHyp) >>
-  | id, occs, Tacexpr.InHypTypeOnly ->
-      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypTypeOnly) >>
-  | id, occs, Tacexpr.InHypValueOnly ->
-      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypValueOnly) >>
+  | occs, Tacexpr.InHyp ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHyp) >>
+  | occs, Tacexpr.InHypTypeOnly ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypTypeOnly) >>
+  | occs, Tacexpr.InHypValueOnly ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypValueOnly) >>
 
 let mlexpr_of_clause cl =
   <:expr< {Tacexpr.onhyps=
@@ -140,7 +142,8 @@ let rec mlexpr_of_constr = function
   | _ -> failwith "mlexpr_of_constr: TODO"
 
 let mlexpr_of_occ_constr =
-  mlexpr_of_pair (mlexpr_of_list mlexpr_of_int) mlexpr_of_constr
+  mlexpr_of_pair (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int))
+    mlexpr_of_constr
 
 let mlexpr_of_red_expr = function
   | Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >>
@@ -151,7 +154,7 @@ let mlexpr_of_red_expr = function
   | Rawterm.Lazy f ->
       <:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >>
   | Rawterm.Unfold l ->
-      let f1 = mlexpr_of_list mlexpr_of_int in
+      let f1 = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) in
       let f2 = mlexpr_of_reference in
       let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in
       <:expr< Rawterm.Unfold $f l$ >>