Suite intégration de constr_pattern

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

10 files changed, 71 insertions, 37 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index a096c833a0..4e556e877b 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -250,7 +250,7 @@ let check_capture s ty = function
 	[< 'sTR ("The variable "^s^" occurs in its type") >]
   | _ -> ()
 
-let dbize k sigma =
+let dbize k allow_soapp sigma =
   let rec dbrec env = function
     | Nvar(loc,s) -> fst (dbize_ref k sigma env loc s)
 	  
@@ -343,6 +343,11 @@ let dbize k sigma =
     | Node(loc,"CAST", [c1;c2]) ->	   
 	RCast (loc,dbrec env c1,dbrec env c2)
 
+    | Node(loc,"SOAPP", Num(locn,n)::args) when allow_soapp ->
+	(* Hack special pour l'interprétation des constr_pattern *)
+	if n<0 then error "Metavariable numbers must be positive" else
+	RApp (loc,RRef (locn,RMeta (-n)),List.map (dbrec env) args)
+
     | Node(loc,opn,tl) -> 
 	anomaly ("dbize found operator "^opn^" with "^
 		 (string_of_int (List.length tl))^" arguments")
@@ -372,7 +377,7 @@ let dbize k sigma =
 	RBinder(loc, oper, na, dbrec env ty,
 		(iterated_binder oper n ty (add_rel (na,()) env) body))
     | body -> dbrec env body
-	  
+
   and dbize_args env l args =
     let rec aux n l args = match (l,args) with 
       | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') ->
@@ -399,7 +404,8 @@ let dbize k sigma =
 (* constr_of_com takes an environment of typing assumptions,
  * and translates a command to a constr. *)
 
-let interp_rawconstr sigma env com = dbize CCI sigma (unitize_env (context env)) com
+let interp_rawconstr sigma env com =
+  dbize CCI false sigma (unitize_env (context env)) com
 
 (* Globalization of AST quotations (mainly used in command quotations
    to get statically bound idents in grammar or pretty-printing rules) *)
@@ -583,6 +589,9 @@ and pat_of_raw metas vars = function
   | RApp (_,c,cl) -> 
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
+  (* Petit hack pour ne pas réécrire une interprétation complète des patterns*)
+  | RApp (_,RRef (_,RMeta n),cl) when n<0 ->
+      PSoApp (-n, List.map (pat_of_raw metas vars) cl)
   | RBinder (_,bk,na,c1,c2) ->
       PBinder (bk, na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
@@ -593,6 +602,9 @@ and pat_of_raw metas vars = function
   | RCast (_,c,t) ->
       warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
+  | ROldCase (_,false,po,c,br) ->
+      PCase (option_app (pat_of_raw metas vars) po, pat_of_raw metas vars c,
+	     Array.map (pat_of_raw metas vars) br)
   | _ ->
       error "pattern_of_rawconstr: not implemented"
 
@@ -602,7 +614,7 @@ let pattern_of_rawconstr c =
   (!metas,p)
 
 let interp_constrpattern sigma env com = 
-  let c = interp_rawconstr sigma env com in
+  let c = dbize CCI true sigma (unitize_env (context env)) com in
   try 
     pattern_of_rawconstr c
   with e -> 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3e286462e8..5fa57bd39e 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -92,11 +92,15 @@ let fprtype_env env typ = fprterm_env env (incast_type typ)
 let fprtype = fprtype_env (gLOB nil_sign)
 *)
 
-let fprterm_env a = failwith "Fw printing not implemented"
-let fprterm = failwith "Fw printing not implemented"
-
-let fprtype_env env typ = failwith "Fw printing not implemented"
-let fprtype = failwith "Fw printing not implemented"
+let fprterm_env a =
+  warning "Fw printing not implemented, use CCI printing 1"; prterm_env a
+let fprterm a =
+  warning "Fw printing not implemented, use CCI printing 2"; prterm a
+
+let fprtype_env env typ =
+  warning "Fw printing not implemented, use CCI printing 3"; prtype_env env typ
+let fprtype a =
+  warning "Fw printing not implemented, use CCI printing 4"; prtype a
 
 (* For compatibility *)
 let fterm0 = fprterm_env
diff --git a/parsing/termast.ml b/parsing/termast.ml
index dda005f8bb..a044c741cb 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -766,7 +766,7 @@ let rec ast_of_pattern env = function
 
   | PSoApp (n,args) ->
       ope("SOAPP",(ope ("META",[num n])):: 
-		  (List.map (ast_of_constr false env) args))
+		  (List.map (ast_of_pattern env) args))
 
   | PBinder (BProd,Anonymous,t,c) ->
       ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index ec7b8d4f76..94f69474b7 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -27,12 +27,14 @@ let local_Constraints lc gs = refiner (Local_constraints lc) gs
 
 let on_wc f wc = ids_mod f wc
 
+let debug = ref true;;
+
 let startWalk gls =
   let evc = project_with_focus gls in
   let wc = (ids_mk evc) in 
   (wc,
    (fun wc' gls' ->
-      if ids_eq wc wc' & gls.it = gls'.it then
+      if !debug & ids_eq wc wc' & 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 (ids_it wc')}
         else
diff --git a/proofs/pattern.ml b/proofs/pattern.ml
index 56a9db7f28..14a1a8905a 100644
--- a/proofs/pattern.ml
+++ b/proofs/pattern.ml
@@ -12,7 +12,7 @@ type constr_pattern =
   | PRef of Term.constr array reference
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
-  | PSoApp of int * constr list
+  | PSoApp of int * constr_pattern list
   | PBinder of binder_kind * name * constr_pattern * constr_pattern
   | PLet of identifier * constr_pattern * constr_pattern * constr_pattern
   | PSort of rawsort
@@ -126,7 +126,7 @@ let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
 
 exception PatternMatchingFailure
 
-let matches_core convert = 
+let matches_core convert pat c = 
   let rec sorec stk sigma p t =
     let cT = whd_castapp t in
     match p,kind_of_term cT with
@@ -134,7 +134,7 @@ let matches_core convert =
 	  let relargs =
 	    List.map
 	      (function
-		 | Rel n -> n
+		 | PRel n -> n
 		 | _ -> error "Only bound indices are currently allowed in second order pattern matching")
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
@@ -195,8 +195,8 @@ let matches_core convert =
 
       | _ -> raise PatternMatchingFailure
 
-    in 
-    sorec [] []
+  in 
+  Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c)
 
 let matches = matches_core None
 
diff --git a/proofs/pattern.mli b/proofs/pattern.mli
index a4685a4680..b725d90446 100644
--- a/proofs/pattern.mli
+++ b/proofs/pattern.mli
@@ -12,7 +12,7 @@ type constr_pattern =
   | PRef of constr array reference
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
-  | PSoApp of int * constr list
+  | PSoApp of int * constr_pattern list
   | PBinder of binder_kind * name * constr_pattern * constr_pattern
   | PLet of identifier * constr_pattern * constr_pattern * constr_pattern
   | PSort of Rawterm.rawsort
@@ -49,12 +49,29 @@ val pattern_of_constr : constr -> constr_pattern
 
 exception PatternMatchingFailure
 
+(* [matches pat c] matches [c] against [pat] and returns the resulting
+   assignment of metavariables; it raises [PatternMatchingFailure] if
+   not matchable; bindings are given in increasing order based on the
+   numbers given in the pattern *)
 val matches      :
   constr_pattern -> constr -> (int * constr) list
-val matches_conv :
-  env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
+
+(* [is_matching pat c] just tells if [c] matches against [pat] *)
+
 val is_matching      :
   constr_pattern -> constr -> bool
+
+(* [matches_conv env sigma] matches up to conversion in environment
+   [(env,sigma)] when constants in pattern are concerned; it raises
+   [PatternMatchingFailure] if not matchable; bindings are given in
+   increasing order based on the numbers given in the pattern *)
+
+val matches_conv :
+  env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
+
+(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
+   up to conversion for constants in patterns *)
+
 val is_matching_conv :
   env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 70297f5868..b8a004a586 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -38,7 +38,7 @@ let (pattern_stock : (int list * constr_pattern) Stock.stock) =
   Stock.make_stock { name = "PATTERN"; proc = parse_pattern }
 
 let put_pat = Stock.stock pattern_stock
-let get_pat = Stock.retrieve pattern_stock
+let get_pat tm = snd (Stock.retrieve pattern_stock tm)
 
 let make_module_marker = Stock.make_module_marker
 
@@ -55,7 +55,7 @@ let (squeleton_stock : (int list * constr) Stock.stock) =
 let put_squel = Stock.stock squeleton_stock
 let get_squel_core = Stock.retrieve squeleton_stock
 
-
+(*
 let dest_somatch n pat =
   let _,m = get_pat pat in
   matches m n
@@ -71,7 +71,7 @@ let dest_somatch_conv env sigma n pat =
 let somatches_conv env sigma n pat =
   let _,m = get_pat pat in
   is_matching_conv env sigma m n
-
+*)
 let soinstance squel arglist =
   let mvs,c = get_squel_core squel in
   let mvb = List.combine mvs arglist in 
@@ -199,8 +199,8 @@ let match_with_equation  t =
         let constr_types = Global.mind_lc_without_abstractions ind in 
         let nconstr = Global.mind_nconstr ind in
 	if nconstr = 1 &&
-           (somatches constr_types.(0) refl_rel_pat1 ||
-            somatches constr_types.(0) refl_rel_pat2) 
+           (is_matching (get_pat refl_rel_pat1) constr_types.(0) ||
+            is_matching (get_pat refl_rel_pat2) constr_types.(0)) 
         then 
 	  Some (hdapp,args)
         else 
@@ -213,10 +213,10 @@ let arrow_pat = put_pat mmk "(?1 -> ?2)"
 
 let match_with_nottype t =
   try
-    let sigma = dest_somatch t arrow_pat in
-    let arg = List.assoc 1 sigma in
-    let mind = List.assoc 2 sigma in
-    if is_empty_type mind then Some (mind,arg) else None
+    match matches (get_pat arrow_pat) t with
+      |	[(1,arg);(2,mind)] ->
+	  if is_empty_type mind then Some (mind,arg) else None
+      | _ -> anomaly "Incorrect pattern matching" 
   with PatternMatchingFailure -> None  
 
 let is_nottype t = op2bool (match_with_nottype t)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 0235fa79f2..ddba560af5 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -7,6 +7,7 @@ open Names
 open Term
 open Sign
 open Evd
+open Pattern
 open Proof_trees
 (*i*)
 
@@ -55,8 +56,7 @@ val make_module_marker : string list -> module_mark
 
 type marked_pattern
 val put_pat            : module_mark -> string -> marked_pattern
-(*val get_pat            : marked_pattern -> constr*)
-
+val get_pat            : marked_pattern -> constr_pattern
 
 (* [put_squel mmk s] declares an open term [s] to be parsed using the
    definitions in the modules associated to the key [mmk] *)
@@ -99,7 +99,6 @@ val dest_somatch : constr -> marked_pattern -> constr list
 (* [somatches c pat] just tells if [c] matches against [pat] *)
 
 val somatches    : constr -> marked_pattern -> bool
-*)
 
 (* [dest_somatch_conv env sigma] matches up to conversion in
    environment [(env,sgima)] when constants in pattern are concerned;
@@ -113,6 +112,7 @@ val dest_somatch_conv :
 
 val somatches_conv :
   Environ.env -> 'a evar_map -> constr -> marked_pattern -> bool
+*)
 
 val soinstance   : marked_term -> constr list -> constr 
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6169847c16..6e7831b1cb 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -118,13 +118,12 @@ let clause_type cls gl =
 
 (* Functions concerning matching of clausal environments *)
 
-let gl_is_matching gls pat n =
+let pf_is_matching gls pat n =
   let (wc,_) = startWalk gls in 
   is_matching_conv (w_env wc) (w_Underlying wc) pat n
 
-let gl_matches gls pat n =
-  let (wc,_)  = startWalk gls in
-  matches_conv (w_env wc) (w_Underlying wc) pat n
+let pf_matches gls pat n =
+  matches_conv (sig_it gls).Evd.evar_env (Stamps.ts_it (sig_sig gls)) pat n
 
 (* [OnCL clausefinder clausetac]
  * executes the clausefinder to find the clauses, and then executes the
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ac118b6d1b..24b705ac72 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -52,8 +52,8 @@ val clause_type : clause -> goal sigma -> constr
 val matches      : goal sigma -> constr -> marked_term -> bool
 val dest_match   : goal sigma -> constr -> marked_term -> constr list
 *)
-val gl_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
-val gl_is_matching : goal sigma -> constr_pattern -> constr -> bool
+val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
+val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
 val allHyps    : goal sigma -> clause list
 val afterHyp   : identifier -> goal sigma -> clause list