diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-04 00:52:24 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-13 14:10:04 +0200 |
commit | c097b83dc9a33a2410e61b8d2aa667229fbd411c (patch) | |
tree | 99d59f20fc255d39ce1827486f79a457e6ce5e4e | |
parent | 0099a8f8e1a77a224ff133fc211d5a8b983a7dcc (diff) |
univ minimization: let-lift [not_lower]
-rw-r--r-- | engine/universes.ml | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 727e50d6b..7aaeee244 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -789,6 +789,27 @@ let _pr_constraints_map (cmap:constraints_map) = let remove_alg l (ctx, us, algs, insts, cstrs) = (ctx, us, LSet.remove l algs, insts, cstrs) +let not_lower lower (d,l) = + (* We're checking if (d,l) is already implied by the lower + constraints on some level u. If it represents l < u (d is Lt + or d is Le and i > 0, the i < 0 case is impossible due to + invariants of Univ), and the lower constraints only have l <= + u then it is not implied. *) + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it. *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + exception UpperBoundedAlg let minimize_univ_variables ctx us algs left right cstrs = @@ -820,28 +841,7 @@ let minimize_univ_variables ctx us algs left right cstrs = lower_add l d newlow, lower_union lower lower') (acc, [], LMap.empty, LMap.empty) l in - let not_lower (d,l) = - (* We're checking if (d,l) is already implied by the lower - constraints on some level u. If it represents l < u (d is Lt - or d is Le and i > 0, the i < 0 case is impossible due to - invariants of Univ), and the lower constraints only have l <= - u then it is not implied. *) - Univ.Universe.exists - (fun (l,i) -> - let d = - if i == 0 then d - else match d with - | Le -> Lt - | d -> d - in - try let d' = LMap.find l lower in - (* If d is stronger than the already implied lower - * constraints we must keep it. *) - compare_constraint_type d d' > 0 - with Not_found -> - (** No constraint existing on l *) true) l - in - let left = List.uniquize (List.filter not_lower left) in + let left = List.uniquize (List.filter (not_lower lower) left) in (acc, left, LMap.union newlow lower) in let instantiate_lbound lbound = |