aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-06-21 18:02:40 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-06-22 13:09:15 +0200
commitd236c7362053c4fc8f1c7f3b59248b412b029fb8 (patch)
treeb1f4186bb493a9b91a36b3a29d29b4dfef040404
parent0f12f2334e6c921a13e2e2186c44b7fb017714c1 (diff)
Define and use UGraph.enforce_leq_alg for subtyping inference
Not sure if worth using in other places.
-rw-r--r--clib/cList.ml10
-rw-r--r--clib/cList.mli5
-rw-r--r--kernel/constr.ml6
-rw-r--r--kernel/reduction.ml4
-rw-r--r--kernel/uGraph.ml39
-rw-r--r--kernel/uGraph.mli3
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. *)