From bc6de5aa4e00dfc19c4866de4876f6213546fa5c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 24 Mar 2017 11:31:50 +0100 Subject: Code cleaning in unification algorithm for universes. This patch is only moving code around and expliciting statically the invariants of the functions, so it should be 1:1 equivalent to the other one. Amongst other goodies, the unification function is not recursive anymore, which ensures that it will terminate. --- engine/uState.ml | 125 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 64 insertions(+), 61 deletions(-) (limited to 'engine') diff --git a/engine/uState.ml b/engine/uState.ml index c66af02bb9..353d8976db 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -131,84 +131,87 @@ let instantiate_variable l b v = exception UniversesDiffer let process_universe_constraints ctx cstrs = + let open Univ in let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let normalize = Universes.normalize_universe_opt_subst vars in - let rec unify_universes fo l d r local = + let is_local l = Univ.LMap.mem l !vars in + let varinfo x = + match Univ.Universe.level x with + | None -> Inl x + | Some l -> Inr l + in + let equalize_variables fo l l' r r' local = + (** Assumes l = [l',0] and r = [r',0] *) + let () = + if is_local l' then + instantiate_variable l' r vars + else if is_local r' then + instantiate_variable r' l vars + else if not (UGraph.check_eq univs l r) then + (* Two rigid/global levels, none of them being local, + one of them being Prop/Set, disallow *) + if Univ.Level.is_small l' || Univ.Level.is_small r' then + raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + else if fo then + raise UniversesDiffer + in + Univ.enforce_eq_level l' r' local + in + let equalize_universes l r local = match varinfo l, varinfo r with + | Inr l', Inr r' -> equalize_variables false l l' r r' local + | Inr l, Inl r | Inl r, Inr l -> + let alg = Univ.LSet.mem l ctx.uctx_univ_algebraic in + let inst = Univ.univ_level_rem l r r in + if alg then (instantiate_variable l inst vars; local) + else + let lu = Univ.Universe.make l in + if Univ.univ_level_mem l r then + Univ.enforce_leq inst lu local + else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) + | Inl _, Inl _ (* both are algebraic *) -> + if UGraph.check_eq univs l r then local + else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + in + let unify_universes (l, d, r) local = let l = normalize l and r = normalize r in if Univ.Universe.equal l r then local else - let varinfo x = - match Univ.Universe.level x with - | None -> Inl x - | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l ctx.uctx_univ_algebraic) - in - if d == Universes.ULe then + match d with + | Universes.ULe -> if UGraph.check_leq univs l r then (** Keep Prop/Set <= var around if var might be instantiated by prop or set later. *) - if Univ.Universe.is_level l then - match Univ.Universe.level r with - | Some r -> - Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local - | _ -> local - else local + match Univ.Universe.level l, Univ.Universe.level r with + | Some l, Some r -> + Univ.Constraint.add (l, Univ.Le, r) local + | _ -> local else - match Univ.Universe.level r with + begin match Univ.Universe.level r with | None -> error ("Algebraic universe on the right") - | Some rl -> - if Univ.Level.is_small rl then + | Some r' -> + if Univ.Level.is_small r' then let levels = Univ.Universe.levels l in - Univ.LSet.fold (fun l local -> - if Univ.Level.is_small l || Univ.LMap.mem l !vars then - unify_universes fo (Univ.Universe.make l) Universes.UEq r local - else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None))) - levels local + let fold l' local = + let l = Univ.Universe.make l' in + if Univ.Level.is_small l' || is_local l' then + equalize_variables false l l' r r' local + else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None)) + in + Univ.LSet.fold fold levels local else Univ.enforce_leq l r local - else if d == Universes.ULub then - match varinfo l, varinfo r with - | (Inr (l, true, _), Inr (r, _, _)) - | (Inr (r, _, _), Inr (l, true, _)) -> - instantiate_variable l (Univ.Universe.make r) vars; - Univ.enforce_eq_level l r local - | Inr (_, _, _), Inr (_, _, _) -> - unify_universes true l Universes.UEq r local + end + | Universes.ULub -> + begin match Universe.level l, Universe.level r with + | Some l', Some r' -> + equalize_variables true l l' r r' local | _, _ -> assert false - else (* d = Universes.UEq *) - match varinfo l, varinfo r with - | Inr (l', lloc, _), Inr (r', rloc, _) -> - let () = - if lloc then - instantiate_variable l' r vars - else if rloc then - instantiate_variable r' l vars - else if not (UGraph.check_eq univs l r) then - (* Two rigid/global levels, none of them being local, - one of them being Prop/Set, disallow *) - if Univ.Level.is_small l' || Univ.Level.is_small r' then - raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) - else - if fo then - raise UniversesDiffer - in - Univ.enforce_eq_level l' r' local - | Inr (l, loc, alg), Inl r - | Inl r, Inr (l, loc, alg) -> - let inst = Univ.univ_level_rem l r r in - if alg then (instantiate_variable l inst vars; local) - else - let lu = Univ.Universe.make l in - if Univ.univ_level_mem l r then - Univ.enforce_leq inst lu local - else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) - | _, _ (* One of the two is algebraic or global *) -> - if UGraph.check_eq univs l r then local - else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + end + | Universes.UEq -> equalize_universes l r local in let local = - Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) - cstrs Univ.Constraint.empty + Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty in !vars, local -- cgit v1.2.3 From 051f2c1be929a46a0713b47b072bb5be0a7558d0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 24 Mar 2017 15:50:21 +0100 Subject: Fast path when checking equality of universe levels in UState. We export the relevant level equality function in UGraph which is way faster than checking that each one is smaller than the other as universes. --- engine/uState.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/uState.ml b/engine/uState.ml index 353d8976db..e27d0536d6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -148,7 +148,7 @@ let process_universe_constraints ctx cstrs = instantiate_variable l' r vars else if is_local r' then instantiate_variable r' l vars - else if not (UGraph.check_eq univs l r) then + else if not (UGraph.check_eq_level univs l' r') then (* Two rigid/global levels, none of them being local, one of them being Prop/Set, disallow *) if Univ.Level.is_small l' || Univ.Level.is_small r' then -- cgit v1.2.3