Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Term

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

1 files changed, 1 insertions, 86 deletions

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 9930a690f..cf8b86b23 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -57,95 +57,10 @@ struct
 	(priority e1.pat) - (priority e2.pat)
 end
 
-(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed; Cast's,
-   application associativity, binders name and Cases annotations are
-   not taken into account *)
-
-let rec compare_list f l1 l2=
-  match l1,l2 with
-      [],[]-> 0
-    | [],_ -> -1
-    | _,[] -> 1
-    | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2
-
-let compare_array f v1 v2=
-  let l=Array.length v1 in
-  let c=l - Array.length v2 in
-    if c=0 then
-      let rec comp_aux i=
-	if i<0 then 0
-	else
-	  let ci=f v1.(i) v2.(i) in
-	    if ci=0 then
-	      comp_aux (i-1)
-	    else ci
-      in comp_aux (l-1)
-    else c
-
-let compare_constr_int f t1 t2 =
-  match kind_of_term t1, kind_of_term t2 with
-    | Rel n1, Rel n2 -> n1 - n2
-    | Meta m1, Meta m2 -> m1 - m2
-    | Var id1, Var id2 -> id_ord id1 id2
-    | Sort s1, Sort s2 -> Pervasives.compare s1 s2
-    | Cast (c1,_,_), _ -> f c1 t2
-    | _, Cast (c2,_,_) -> f t1 c2
-    | Prod (_,t1,c1), Prod (_,t2,c2)
-    | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
-	(f =? f) t1 t2 c1 c2
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
-	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
-    | App (_,_), App (_,_) ->
-	let c1,l1=decompose_app t1
-	and c2,l2=decompose_app t2 in
-	  (f =? (compare_list f)) c1 c2 l1 l2
-    | Evar (e1,l1), Evar (e2,l2) ->
-	((-) =? (compare_array f)) e1 e2 l1 l2
-    | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2)
-    | Ind (spx, ix), Ind (spy, iy) ->
-	let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c
-    | Construct ((spx, ix), jx), Construct ((spy, iy), jy) ->
-	let c = jx - jy in if c = 0 then
-	  (let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c)
-	else c
-    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-	((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2
-    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
-	ln1 ln2 tl1 tl2 bl1 bl2
-    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
-	ln1 ln2 tl1 tl2 bl1 bl2
-    | Var _, (Rel _)
-    | Meta _, (Rel _ | Var _)
-    | Evar _, (Rel _ | Var _ | Meta _)
-    | Sort _, (Rel _ | Var _ | Meta _ | Evar _)
-    | Prod _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _)
-    | Lambda _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _)
-    | LetIn _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _)
-    | App _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _)
-    | Const _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _)
-    | Ind _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _)
-    | Construct _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ | Ind _)
-    | Case _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ | Ind _ | Construct _)
-    | Fix _, (Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ | Ind _ | Construct _ | Case _)
-    | CoFix _, _
-      -> -1
-    | Rel _, _ | Var _, _ | Meta _, _ | Evar _, _
-    | Sort _, _ | Prod _, _
-    | Lambda _, _ | LetIn _, _ | App _, _
-    | Const _, _ | Ind _, _ | Construct _, _
-    | Case _, _| Fix _, _
-      -> 1
-
-let rec compare_constr m n=
-  compare_constr_int compare_constr m n
-
 module OrderedConstr=
 struct
   type t=constr
-  let compare=compare_constr
+  let compare=constr_ord
 end
 
 type h_item = global_reference * (int*constr) option