diff options
| author | Gaëtan Gilbert | 2019-10-02 16:42:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-02 16:42:16 +0200 |
| commit | 92a55bf800a34b5ec283ce0419cde98f3312c9b8 (patch) | |
| tree | 0e7517a16ac6c0b98169225176d9c3ecfabc91a5 /engine | |
| parent | b6f77dc89b62bdb43f2f07ba31b181a10dfcfc39 (diff) | |
| parent | 08740d8e5a6974183e13b4cf372caade1c25f6fa (diff) | |
Merge PR #10809: Postpone the computation of relative constraints in universe unification
Reviewed-by: SkySkimmer
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/uState.ml | 34 |
1 files changed, 19 insertions, 15 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index cb40e6eadd..d93ccafcf0 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,21 @@ 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 + then (* l contains a +1 and r=r' small so l <= r impossible *) 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 +260,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 |