diff options
| -rw-r--r-- | clib/cList.ml | 10 | ||||
| -rw-r--r-- | clib/cList.mli | 5 | ||||
| -rw-r--r-- | kernel/constr.ml | 6 | ||||
| -rw-r--r-- | kernel/reduction.ml | 4 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 39 | ||||
| -rw-r--r-- | kernel/uGraph.mli | 3 |
6 files changed, 63 insertions, 4 deletions
diff --git a/clib/cList.ml b/clib/cList.ml index 2b627f745..de42886dc 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -122,6 +122,7 @@ sig val duplicates : 'a eq -> 'a list -> 'a list val uniquize : 'a list -> 'a list val sort_uniquize : 'a cmp -> 'a list -> 'a list + val min : 'a cmp -> 'a list -> 'a val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list val combinations : 'a list list -> 'a list list @@ -971,6 +972,15 @@ let rec uniquize_sorted cmp = function let sort_uniquize cmp l = uniquize_sorted cmp (List.sort cmp l) +let min cmp l = + let rec aux cur = function + | [] -> cur + | x :: l -> if cmp x cur < 0 then aux x l else aux cur l + in + match l with + | x :: l -> aux x l + | [] -> raise Not_found + let rec duplicates cmp = function | [] -> [] | x :: l -> diff --git a/clib/cList.mli b/clib/cList.mli index 13e069e94..42fae5ed3 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -376,6 +376,11 @@ sig (** Return a sorted version of a list without duplicates according to some comparison function. *) + val min : 'a cmp -> 'a list -> 'a + (** Return minimum element according to some comparison function. + + @raise Not_found on an empty list. *) + (** {6 Cartesian product} *) val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list diff --git a/kernel/constr.ml b/kernel/constr.ml index 418229330..e68f906ec 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -828,8 +828,10 @@ let leq_constr_univs_infer univs m n = let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if UGraph.check_leq univs u1 u2 then true else - (cstrs := Univ.enforce_leq u1 u2 !cstrs; - true) + (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in + cstrs := Univ.Constraint.union c !cstrs; + true + with Univ.UniverseInconsistency _ -> false) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f4af31386..2c61b7a01 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -693,8 +693,8 @@ let infer_eq (univs, cstrs as cuniv) u u' = let infer_leq (univs, cstrs as cuniv) u u' = if UGraph.check_leq univs u u' then cuniv else - let cstrs' = Univ.enforce_leq u u' cstrs in - univs, cstrs' + let cstrs', _ = UGraph.enforce_leq_alg u u' univs in + univs, Univ.Constraint.union cstrs cstrs' let infer_cmp_universes env pb s0 s1 univs = let open Sorts in diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4a9467de5..bc624ba56 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -747,6 +747,45 @@ let check_constraint g (l,d,r) = let check_constraints c g = Constraint.for_all (check_constraint g) c +let leq_expr (u,m) (v,n) = + let d = match m - n with + | 1 -> Lt + | diff -> assert (diff <= 0); Le + in + (u,d,v) + +let enforce_leq_alg u v g = + let enforce_one (u,v) = function + | Inr _ as orig -> orig + | Inl (cstrs,g) as orig -> + if check_smaller_expr g u v then orig + else + (let c = leq_expr u v in + match enforce_constraint c g with + | g -> Inl (Constraint.add c cstrs,g) + | exception (UniverseInconsistency _ as e) -> Inr e) + in + (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *) + let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in + let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in + (* We pick a best constraint: smallest number of constraints, not an error if possible. *) + let order x y = match x, y with + | Inr _, Inr _ -> 0 + | Inl _, Inr _ -> -1 + | Inr _, Inl _ -> 1 + | Inl (c,_), Inl (c',_) -> + Int.compare (Constraint.cardinal c) (Constraint.cardinal c') + in + match List.min order c with + | Inl x -> x + | Inr e -> raise e + +(* sanity check wrapper *) +let enforce_leq_alg u v g = + let _,g as cg = enforce_leq_alg u v g in + assert (check_leq g u v); + cg + (* Normalization *) (** [normalize_universes g] returns a graph where all edges point diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e6dd629e4..8c2d877b0 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -42,6 +42,9 @@ val merge_constraints : Constraint.t -> t -> t val check_constraint : t -> univ_constraint -> bool val check_constraints : Constraint.t -> t -> bool +(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *) +val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t + (** Adds a universe to the graph, ensuring it is >= or > Set. @raise AlreadyDeclared if the level is already declared in the graph. *) |