Suite intégration de constr_pattern

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

3 files changed, 28 insertions, 9 deletions

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