diff options
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 108 |
1 files changed, 71 insertions, 37 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 6c8dbe3f..29cb3c9b 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -20,14 +20,14 @@ type uinfo = { uloc : Loc.t option; } -module UPairSet = Universes.UPairSet +module UPairSet = UnivMinim.UPairSet (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : Universes.universe_binders * uinfo Univ.LMap.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,11 +152,12 @@ 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 - let normalize = normalize_univ_variable_opt_subst vars in + let normalize u = normalize_univ_variable_opt_subst !vars u in let nf_constraint = function | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v) @@ -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 @@ -293,18 +295,30 @@ let constrain_variables diff ctx = in { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } -let reference_of_level uctx = +let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname) + try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> - Universes.reference_of_level l + UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_reference (reference_of_level uctx l) + Libnames.pr_qualid (qualid_of_level uctx l) + +type ('a, 'b) gen_universe_decl = { + univdecl_instance : 'a; (* Declared universes *) + univdecl_extensible_instance : bool; (* Can new universes be added *) + univdecl_constraints : 'b; (* Declared constraints *) + univdecl_extensible_constraints : bool (* Can new constraints be added *) } type universe_decl = - (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl + (lident list, Univ.Constraint.t) gen_universe_decl + +let default_univ_decl = + { univdecl_instance = []; + univdecl_extensible_instance = true; + univdecl_constraints = Univ.Constraint.empty; + univdecl_extensible_constraints = true } let error_unbound_universes left uctx = let open Univ in @@ -365,7 +379,6 @@ let check_implication uctx cstrs cstrs' = (str "Universe constraints are not implied by the ones declared.") let check_mono_univ_decl uctx decl = - let open Misctypes in let () = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in @@ -378,7 +391,6 @@ let check_mono_univ_decl uctx decl = uctx.uctx_local let check_univ_decl ~poly uctx decl = - let open Misctypes in let ctx = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in @@ -418,10 +430,17 @@ let univ_rigid = UnivRigid let univ_flexible = UnivFlexible false let univ_flexible_alg = UnivFlexible true -let merge ?loc sideff rigid uctx ctx' = +(** ~sideff indicates that it is ok to redeclare a universe. + ~extend also merges the universe context in the local constraint structures + and not only in the graph. This depends if the + context we merge comes from a side effect that is already inlined + or defined separately. In the later case, there is no extension, + see [emit_side_effects] for example. *) +let merge ?loc ~sideff ~extend rigid uctx ctx' = let open Univ in let levels = ContextSet.levels ctx' in - let uctx = if sideff then uctx else + let uctx = + if not extend then uctx else match rigid with | UnivRigid -> uctx | UnivFlexible b -> @@ -436,9 +455,8 @@ let merge ?loc sideff rigid uctx ctx' = else { uctx with uctx_univ_variables = uvars' } in let uctx_local = - if sideff then uctx.uctx_local - else ContextSet.append ctx' uctx.uctx_local - in + if not extend then uctx.uctx_local + else ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> try UGraph.add_universe u false g @@ -467,11 +485,11 @@ let merge_subst uctx s = let emit_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in - List.fold_left (merge true univ_rigid) u uctxs + List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level () in + let u = UnivGen.new_univ_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with @@ -549,14 +567,33 @@ 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 is_trivial_leq (l,d,r) = + Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) + +(* Prop < i <-> Set+1 <= i <-> Set < i *) +let translate_cstr (l,d,r as cstr) = + let open Univ in + if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then + (Level.set, d, r) + else cstr + +let refresh_constraints univs (ctx, cstrs) = + let cstrs', univs' = + Univ.Constraint.fold (fun c (cstrs', univs as acc) -> + let c = translate_cstr c in + if is_trivial_leq c then acc + else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs)) + cstrs (Univ.Constraint.empty, univs) + in ((ctx, cstrs'), univs') let normalize_variables uctx = - let normalized_variables, undef, def, subst = - Universes.normalize_univ_variables uctx.uctx_univ_variables + let normalized_variables, def, subst = + 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 + let ctx_local', univs = refresh_constraints uctx.uctx_initial_universes ctx_local in subst, { uctx with uctx_local = ctx_local'; uctx_univ_variables = normalized_variables; uctx_universes = univs } @@ -582,7 +619,7 @@ let fix_undefined_variables uctx = uctx_univ_algebraic = algs' } let refresh_undefined_univ_variables uctx = - let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in let subst_fn u = Univ.subst_univs_level_level subst u in let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc) uctx.uctx_univ_algebraic Univ.LSet.empty @@ -609,7 +646,7 @@ let refresh_undefined_univ_variables uctx = uctx', subst let minimize uctx = - let open Universes in + let open UnivMinim in let ((vars',algs'), us') = normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints @@ -637,11 +674,8 @@ let update_sigma_env uctx env = { uctx with uctx_initial_universes = univs; uctx_universes = univs } in - merge true univ_rigid eunivs eunivs.uctx_local + merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local let pr_weak prl {uctx_weak_constraints=weak} = let open Pp in prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak) - -(** Deprecated *) -let normalize = minimize |