aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/term.ml65
-rw-r--r--kernel/term.mli1
-rw-r--r--plugins/firstorder/sequent.ml87
3 files changed, 67 insertions, 86 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index 0bf6b9a89..624db718e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -595,6 +595,71 @@ let rec eq_constr m n =
let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
+let constr_ord_int f t1 t2 =
+ let (=?) f g i1 i2 j1 j2=
+ let c=f i1 i2 in
+ if c=0 then g j1 j2 else c in
+ let (==?) fg h i1 i2 j1 j2 k1 k2=
+ let c=fg i1 i2 j1 j2 in
+ if c=0 then h k1 k2 else c in
+ 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 =? (list_compare f)) c1 c2 l1 l2
+ | Evar (e1,l1), Evar (e2,l2) ->
+ ((-) =? (array_compare 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) ==? (array_compare f)) p1 p2 c1 c2 bl1 bl2
+ | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
+ ((Pervasives.compare =? (array_compare f)) ==? (array_compare f))
+ ln1 ln2 tl1 tl2 bl1 bl2
+ | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
+ ((Pervasives.compare =? (array_compare f)) ==? (array_compare 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 constr_ord m n=
+ constr_ord_int constr_ord m n
+
(***************************************************************************)
(* Type of assumptions *)
(***************************************************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 0854655c1..0a1f2e32e 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -618,6 +618,7 @@ val iter_constr_with_binders :
val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+val constr_ord : constr -> constr -> int
val hash_constr : constr -> int
(*********************************************************************)
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