diff options
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 839bb5ae9..6111ec7ed 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -27,7 +27,7 @@ type t = { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *) - uctx_univ_variables : Universes.universe_opt_subst; + uctx_univ_variables : UnivSubst.universe_opt_subst; (** The local universes that are unification variables *) uctx_univ_algebraic : Univ.LSet.t; (** The subset of unification variables that can be instantiated with @@ -152,7 +152,8 @@ let drop_weak_constraints = ref false let process_universe_constraints ctx cstrs = let open Univ in - let open Universes in + let open UnivSubst in + let open UnivProblem in let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let weak = ref ctx.uctx_weak_constraints in @@ -203,7 +204,7 @@ let process_universe_constraints ctx cstrs = in let unify_universes cst local = let cst = nf_constraint cst in - if Constraints.is_trivial cst then local + if UnivProblem.is_trivial cst then local else match cst with | ULe (l, r) -> @@ -241,7 +242,7 @@ let process_universe_constraints ctx cstrs = | UEq (l, r) -> equalize_universes l r local in let local = - Constraints.fold unify_universes cstrs Univ.Constraint.empty + UnivProblem.Set.fold unify_universes cstrs Univ.Constraint.empty in !vars, !weak, local @@ -249,13 +250,14 @@ let add_constraints ctx cstrs = let univs, local = ctx.uctx_local in let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> let l = Univ.Universe.make l and r = Univ.Universe.make r in - let cstr' = match d with + let cstr' = let open UnivProblem in + match d with | Univ.Lt -> - Universes.ULe (Univ.Universe.super l, r) - | Univ.Le -> Universes.ULe (l, r) - | Univ.Eq -> Universes.UEq (l, r) - in Universes.Constraints.add cstr' acc) - cstrs Universes.Constraints.empty + ULe (Univ.Universe.super l, r) + | Univ.Le -> ULe (l, r) + | Univ.Eq -> UEq (l, r) + in UnivProblem.Set.add cstr' acc) + cstrs UnivProblem.Set.empty in let vars, weak, local' = process_universe_constraints ctx cstrs' in { ctx with @@ -549,11 +551,11 @@ let is_sort_variable uctx s = | _ -> None let subst_univs_context_with_def def usubst (ctx, cst) = - (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst) + (Univ.LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst) let normalize_variables uctx = let normalized_variables, undef, def, subst = - Universes.normalize_univ_variables uctx.uctx_univ_variables + UnivSubst.normalize_univ_variables uctx.uctx_univ_variables in let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in |