diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-29 13:02:23 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-29 13:02:23 +0000 |
| commit | 278517722988d040cb8da822e319d723670ac519 (patch) | |
| tree | 92316184aec004570c6567f0d585167e47dd52ae /kernel/univ.ml | |
| parent | 0699ef2ffba984e7b7552787894b142dd924f66a (diff) | |
Removed many calls to OCaml generic equality. This was done by
writing our own comparison functions, and enforcing monomorphization
in many places. This should be more efficient, btw. Still a work
in progress.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 39cb6bc10..635991494 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -53,11 +53,12 @@ module UniverseLevel = struct | Level (i1, dp1), Level (i2, dp2) -> if i1 < i2 then -1 else if i1 > i2 then 1 - else compare dp1 dp2) + else Names.dir_path_ord dp1 dp2) let equal u v = match u,v with | Set, Set -> true - | Level (i1, dp1), Level (i2, dp2) -> i1 = i2 && dp1 = dp2 + | Level (i1, dp1), Level (i2, dp2) -> + i1 = i2 && (Names.dir_path_ord dp1 dp2 = 0) | _ -> false let to_string = function @@ -272,6 +273,15 @@ let between g arcu arcv = type constraint_type = Lt | Le | Eq type explanation = (constraint_type * universe) list +let constraint_type_ord c1 c2 = match c1, c2 with +| Lt, Lt -> 0 +| Lt, _ -> -1 +| Le, Lt -> 1 +| Le, Le -> 0 +| Le, Eq -> -1 +| Eq, Eq -> 0 +| Eq, _ -> 1 + (* Assuming the current universe has been reached by [p] and [l] correspond to the universes in (direct) relation [rel] with it, make a list of canonical universe, updating the relation with @@ -527,7 +537,7 @@ module Constraint = Set.Make( struct type t = univ_constraint let compare (u,c,v) (u',c',v') = - let i = Pervasives.compare c c' in + let i = constraint_type_ord c c' in if i <> 0 then i else let i' = UniverseLevel.compare u u' in |