diff options
| author | Pierre-Marie Pédrot | 2019-09-30 11:06:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-02 00:25:13 +0200 |
| commit | 004d7aeeca9f5ae4ceb9f109fa90a87e58457680 (patch) | |
| tree | f3658039f353f0e706d33c758e5845441dd9b786 /engine/uState.ml | |
| parent | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (diff) | |
Postpone the computation of relative constraints in universe unification.
Should be 1:1 equivalent to the previous code, this is semantics preserving
factorization.
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 34 |
1 files changed, 20 insertions, 14 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index cb40e6eadd..5ebac4b817 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -178,6 +178,7 @@ exception UniversesDiffer let drop_weak_constraints = ref false + let process_universe_constraints ctx cstrs = let open UnivSubst in let open UnivProblem in @@ -236,22 +237,23 @@ let process_universe_constraints ctx cstrs = else match cst with | ULe (l, r) -> - if UGraph.check_leq univs l r then - (* Keep Prop/Set <= var around if var might be instantiated by prop or set - later. *) - match Universe.level l, Universe.level r with - | Some l, Some r -> - Constraint.add (l, Le, r) local - | _ -> local - else - begin match Universe.level r with - | None -> user_err Pp.(str "Algebraic universe on the right") - | Some r' -> - if Level.is_small r' then + begin match Univ.Universe.level r with + | None -> + if UGraph.check_leq univs l r then local + else user_err Pp.(str "Algebraic universe on the right") + | Some r' -> + if Level.is_small r' then if not (Universe.is_levels l) then + if UGraph.check_leq univs l r then local + else raise (UniverseInconsistency (Le, l, r, None)) else + if UGraph.check_leq univs l r then match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> local + else let levels = Universe.levels l in let fold l' local = let l = Universe.make l' in @@ -260,8 +262,12 @@ let process_universe_constraints ctx cstrs = else raise (UniverseInconsistency (Le, l, r, None)) in LSet.fold fold levels local - else - enforce_leq l r local + else + match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> + if UGraph.check_leq univs l r then local else enforce_leq l r local end | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local |