Removing another bunch of generic equalities

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

2 files changed, 57 insertions, 46 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index cbd66e03d4..96055ca16c 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -317,9 +317,9 @@ let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
 let canonical_mind mind = snd mind
 let user_mind mind = fst mind
 let repr_mind mind = fst mind
-let mind_label mind= label (fst mind)
+let mind_label mind = label (fst mind)
 
-let eq_mind (_,kn1) (_,kn2) = kn1=kn2
+let eq_mind (_, kn1) (_, kn2) = kn_ord kn1 kn2 = 0
 
 let string_of_mind mind = string_of_kn (fst mind)
 let pr_mind mind = str (string_of_mind mind)
@@ -327,12 +327,14 @@ let debug_string_of_mind mind =
   "(" ^ string_of_kn (fst mind) ^ "," ^ string_of_kn (snd mind) ^ ")"
 let debug_pr_mind con = str (debug_string_of_mind con)
 
-let ith_mutual_inductive (kn,_) i = (kn,i)
-let ith_constructor_of_inductive ind i = (ind,i)
-let inductive_of_constructor (ind,i) = ind
-let index_of_constructor (ind,i) = i
-let eq_ind (kn1,i1) (kn2,i2) = i1=i2&&eq_mind kn1 kn2
-let eq_constructor (kn1,i1) (kn2,i2) = i1=i2&&eq_ind kn1 kn2
+let ith_mutual_inductive (kn, _) i = (kn, i)
+let ith_constructor_of_inductive ind i = (ind, i)
+let inductive_of_constructor (ind, i) = ind
+let index_of_constructor (ind, i) = i
+let eq_ind (kn1, i1) (kn2, i2) =
+  i1 - i2 = 0 && eq_mind kn1 kn2
+let eq_constructor (kn1, i1) (kn2, i2) =
+  i1 - i2 = 0 && eq_ind kn1 kn2
 
 module Mindmap = Map.Make(Canonical_ord)
 module Mindset = Set.Make(Canonical_ord)
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 4beaf5282c..0f8c011e20 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -47,7 +47,7 @@ type bound_ident_map = (identifier * identifier) list
 
 exception PatternMatchingFailure
 
-let constrain (n,(ids,m as x)) (names,terms as subst) =
+let constrain n (ids, m as x) (names, terms as subst) =
   try
     let (ids',m') = List.assoc n terms in
     if ids = ids' && eq_constr m m' then subst
@@ -79,30 +79,32 @@ let build_lambda toabstract stk (m : constr) =
   let rec buildrec m p_0 p_1 = match p_0,p_1 with
     | (_, []) -> m
     | (n, (_,na,t)::tl) ->
-	if List.mem n toabstract then
+	if Intset.mem n toabstract then
           buildrec (mkLambda (na,t,m)) (n+1) tl
         else
 	  buildrec (lift (-1) m) (n+1) tl
   in
   buildrec m 1 stk
 
-let rec list_insert f a = function
-  | [] -> [a]
-  | b::l when f a b -> a::b::l
-  | b::l when a = b -> raise PatternMatchingFailure
-  | b::l -> b :: list_insert f a l
+let rec list_insert a = function
+| [] -> [a]
+| b :: l ->
+  let ord = id_ord a b in
+  if ord < 0 then a :: b :: l
+  else if ord > 0 then b :: list_insert a l
+  else raise PatternMatchingFailure
 
 let extract_bound_vars =
   let rec aux k = function
   | ([],_) -> []
-  | (n::l,(na1,na2,_)::stk) when k = n ->
-      begin match na1,na2 with
-      | Name id1,Name _ -> list_insert (<) id1 (aux (k+1) (l,stk))
-      | Name _,Anonymous -> anomaly "Unnamed bound variable"
-      | Anonymous,_ -> raise PatternMatchingFailure
+  | (n :: l, (na1, na2, _) :: stk) when k - n = 0 ->
+      begin match na1, na2 with
+      | Name id1, Name _ -> list_insert id1 (aux (k + 1) (l, stk))
+      | Name _, Anonymous -> anomaly "Unnamed bound variable"
+      | Anonymous, _ -> raise PatternMatchingFailure
       end
-  | (l,_::stk) -> aux (k+1) (l,stk)
-  | (_,[]) -> assert false
+  | (l, _ :: stk) -> aux (k + 1) (l, stk)
+  | (_, []) -> assert false
   in aux 1
 
 let dummy_constr = mkProp
@@ -131,11 +133,11 @@ let merge_binding allow_bound_rels stk n cT subst =
 	let canonically_ordered_vars = extract_bound_vars (frels,stk) in
 	let renaming = make_renaming canonically_ordered_vars stk in
 	(canonically_ordered_vars, substl renaming cT)
-      else if frels = [] then
-	([],lift (-depth) cT)
-      else
-	raise PatternMatchingFailure in
-  constrain (n,c) subst
+      else match frels with
+      | [] -> ([], lift (- depth) cT)
+      | _ -> raise PatternMatchingFailure
+  in
+  constrain n c subst
 
 let matches_core convert allow_partial_app allow_bound_rels pat c =
   let conv = match convert with
@@ -145,29 +147,28 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
     let cT = strip_outer_cast t in
     match p,kind_of_term cT with
       | PSoApp (n,args),m ->
-	  let relargs =
-	    List.map
-	      (function
-		 | PRel n -> n
-		 | _ -> error "Only bound indices allowed in second order pattern matching.")
-	      args in
-	  let frels = Intset.elements (free_rels cT) in
-	  if List.subset frels relargs then
-	    constrain (n,([],build_lambda relargs stk cT)) subst
-	  else
-	    raise PatternMatchingFailure
+        let fold accu = function
+        | PRel n -> Intset.add n accu
+        | _ -> error "Only bound indices allowed in second order pattern matching."
+        in
+        let relargs = List.fold_left fold Intset.empty args in
+        let frels = free_rels cT in
+        if Intset.subset frels relargs then
+          constrain n ([], build_lambda relargs stk cT) subst
+        else
+          raise PatternMatchingFailure
 
       | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst
 
       | PMeta None, m -> subst
 
-      | PRef (VarRef v1), Var v2 when v1 = v2 -> subst
+      | PRef (VarRef v1), Var v2 when id_ord v1 v2 = 0 -> subst
 
-      | PVar v1, Var v2 when v1 = v2 -> subst
+      | PVar v1, Var v2 when id_ord v1 v2 = 0 -> subst
 
       | PRef ref, _ when conv (constr_of_global ref) cT -> subst
 
-      | PRel n1, Rel n2 when n1 = n2 -> subst
+      | PRel n1, Rel n2 when n1 - n2 = 0 -> subst
 
       | PSort GProp, Sort (Prop Null) -> subst
 
@@ -182,7 +183,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
 
       | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app ->
           let p = Array.length args2 - Array.length args1 in
-          if p>=0 then
+          if p >= 0 then
             let args21, args22 = Array.chop p args2 in
 	    let c = mkApp(c2,args21) in
             let subst = merge_binding allow_bound_rels stk n c subst in
@@ -222,9 +223,17 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
 
       | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
 	  let n2 = Array.length br2 in
-	  if (ci1.cip_ind <> None && ci1.cip_ind <> Some ci2.ci_ind) ||
-	     (not ci1.cip_extensible && List.length br1 <> n2)
-	  then raise PatternMatchingFailure;
+          let () = match ci1.cip_ind with
+          | None -> ()
+          | Some ind1 ->
+            (** ppedrot: Something spooky going here. The comparison used to be
+                the generic one, so I may have broken something. *)
+            if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure
+          in
+          let () =
+            if not ci1.cip_extensible && List.length br1 <> n2
+            then raise PatternMatchingFailure
+          in
 	  let chk_branch subst (j,n,c) =
 	    (* (ind,j+1) is normally known to be a correct constructor
 	       and br2 a correct match over the same inductive *)
@@ -240,7 +249,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
 
   in
   let names,terms = sorec [] ([],[]) pat c in
-  (names,Sort.list (fun (a,_) (b,_) -> a<b) terms)
+  (names, List.sort (fun (a, _) (b, _) -> id_ord a b) terms)
 
 let matches_core_closed convert allow_partial_app pat c =
   let names,subst = matches_core convert allow_partial_app false pat c in