diff options
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | engine/engine.mllib | 1 | ||||
| -rw-r--r-- | engine/evd.ml | 528 | ||||
| -rw-r--r-- | engine/evd.mli | 4 | ||||
| -rw-r--r-- | engine/uState.ml | 484 | ||||
| -rw-r--r-- | engine/uState.mli | 83 |
6 files changed, 624 insertions, 477 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index f19edf1c8..b81fe151f 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -117,6 +117,7 @@ Miscops Universes Termops Namegen +UState Evd Glob_ops Redops diff --git a/engine/engine.mllib b/engine/engine.mllib index dc7ff2a64..befeaa147 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,5 +1,6 @@ Logic_monad Termops Namegen +UState Evd Proofview_monad diff --git a/engine/evd.ml b/engine/evd.ml index 79e73bda5..cfe9a3da4 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -259,221 +259,20 @@ let instantiate_evar_array info c args = | [] -> c | _ -> replace_vars inst c -module StringOrd = struct type t = string let compare = String.compare end -module UNameMap = struct - - include Map.Make(StringOrd) - - let union s t = - if s == t then s - else - merge (fun k l r -> - match l, r with - | Some _, _ -> l - | _, _ -> r) s t -end - -(* 2nd part used to check consistency on the fly. *) -type evar_universe_context = - { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; - uctx_local : Univ.universe_context_set; (** The local context of variables *) - uctx_univ_variables : Universes.universe_opt_subst; - (** The local universes that are unification variables *) - uctx_univ_algebraic : Univ.universe_set; - (** The subset of unification variables that - can be instantiated with algebraic universes as they appear in types - and universe instances only. *) - uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) - uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) - } - -let empty_evar_universe_context = - { uctx_names = UNameMap.empty, Univ.LMap.empty; - uctx_local = Univ.ContextSet.empty; - uctx_univ_variables = Univ.LMap.empty; - uctx_univ_algebraic = Univ.LSet.empty; - uctx_universes = UGraph.initial_universes; - uctx_initial_universes = UGraph.initial_universes } - -let evar_universe_context_from e = - let u = universes e in - {empty_evar_universe_context with - uctx_universes = u; uctx_initial_universes = u} - -let is_empty_evar_universe_context ctx = - Univ.ContextSet.is_empty ctx.uctx_local && - Univ.LMap.is_empty ctx.uctx_univ_variables - -let union_evar_universe_context ctx ctx' = - if ctx == ctx' then ctx - else if is_empty_evar_universe_context ctx' then ctx - else - let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in - let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in - let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) - (Univ.ContextSet.levels ctx.uctx_local) in - let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in - let declarenew g = - Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g - in - let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in - { uctx_names = (names, names_rev); - uctx_local = local; - uctx_univ_variables = - Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; - uctx_univ_algebraic = - Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; - uctx_initial_universes = declarenew ctx.uctx_initial_universes; - uctx_universes = - if local == ctx.uctx_local then ctx.uctx_universes - else - let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } - -(* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *) -(* let union_evar_universe_context = *) -(* Profile.profile2 union_evar_universe_context_key union_evar_universe_context;; *) - +type evar_universe_context = UState.t type 'a in_evar_universe_context = 'a * evar_universe_context -let evar_universe_context_set diff ctx = - let initctx = ctx.uctx_local in - let cstrs = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty - in - Univ.ContextSet.add_constraints cstrs initctx - -let evar_universe_context_constraints ctx = snd ctx.uctx_local -let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local - -let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx } -let evar_universe_context_subst ctx = ctx.uctx_univ_variables - -let instantiate_variable l b v = - v := Univ.LMap.add l (Some b) !v - -exception UniversesDiffer - -let process_universe_constraints univs vars alg cstrs = - let vars = ref vars in - let normalize = Universes.normalize_universe_opt_subst vars in - let rec unify_universes fo 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 alg) - in - if d == Universes.ULe then - 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 - else - match Univ.Universe.level r with - | None -> error ("Algebraic universe on the right") - | Some rl -> - if Univ.Level.is_small rl 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 - 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 - | _, _ -> 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)) - in - let local = - Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) - cstrs Univ.Constraint.empty - in - !vars, local - -let add_constraints_context 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' = - if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r) - else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r) - in Universes.Constraints.add cstr' acc) - cstrs Universes.Constraints.empty - in - let vars, local' = - process_universe_constraints ctx.uctx_universes - ctx.uctx_univ_variables ctx.uctx_univ_algebraic - cstrs' - in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } - -(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) -(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) - -let add_universe_constraints_context ctx cstrs = - let univs, local = ctx.uctx_local in - let vars, local' = - process_universe_constraints ctx.uctx_universes - ctx.uctx_univ_variables ctx.uctx_univ_algebraic - cstrs - in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } +let empty_evar_universe_context = UState.empty +let evar_universe_context_from = UState.from +let is_empty_evar_universe_context = UState.is_empty +let union_evar_universe_context = UState.union +let evar_universe_context_set = UState.context_set +let evar_universe_context_constraints = UState.constraints +let evar_context_universe_context = UState.context +let evar_universe_context_of = UState.of_context_set +let evar_universe_context_subst = UState.subst +let add_constraints_context = UState.add_constraints +let add_universe_constraints_context = UState.add_universe_constraints (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *) (* let add_universe_constraints_context = *) @@ -937,7 +736,7 @@ let evars_of_filtered_evar_info evi = (**********************************************************) (* Sort variables *) -type rigid = +type rigid = UState.rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) @@ -947,146 +746,32 @@ let univ_flexible_alg = UnivFlexible true let evar_universe_context d = d.universes -let universe_context_set d = d.universes.uctx_local - -let pr_uctx_level uctx = - let map, map_rev = uctx.uctx_names in - fun l -> - try str(Univ.LMap.find l map_rev) - with Not_found -> - Universes.pr_with_global_universes l - -let universe_context ?names evd = - match names with - | None -> Univ.ContextSet.to_context evd.universes.uctx_local - | Some pl -> - let levels = Univ.ContextSet.levels evd.universes.uctx_local in - let newinst, left = - List.fold_right - (fun (loc,id) (newinst, acc) -> - let l = - try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names) - with Not_found -> - user_err_loc (loc, "universe_context", - str"Universe " ++ pr_id id ++ str" is not bound anymore.") - in (l :: newinst, Univ.LSet.remove l acc)) - pl ([], levels) - in - if not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - errorlabstrm "universe_context" - (str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level evd.universes) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") - else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst), - Univ.ContextSet.constraints evd.universes.uctx_local) +let universe_context_set d = UState.context_set Univ.UContext.empty d.universes + +let pr_uctx_level = UState.pr_uctx_level +let universe_context ?names evd = UState.universe_context ?names evd.universes let restrict_universe_context evd vars = - let uctx = evd.universes in - let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in - { evd with universes = { uctx with uctx_local = uctx' } } - + { evd with universes = UState.restrict evd.universes vars } + let universe_subst evd = - evd.universes.uctx_univ_variables - -let merge_uctx sideff rigid uctx ctx' = - let open Univ in - let levels = ContextSet.levels ctx' in - let uctx = if sideff then uctx else - match rigid with - | UnivRigid -> uctx - | UnivFlexible b -> - let fold u accu = - if LMap.mem u accu then accu - else LMap.add u None accu - in - let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in - if b then - { uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } - 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 - let declare g = - LSet.fold (fun u g -> - try UGraph.add_universe u false g - with UGraph.AlreadyDeclared when sideff -> g) - levels g - in - let initial = declare uctx.uctx_initial_universes in - let univs = declare uctx.uctx_universes in - let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in - { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } + UState.subst evd.universes let merge_context_set ?(sideff=false) rigid evd ctx' = - {evd with universes = merge_uctx sideff rigid evd.universes ctx'} + {evd with universes = UState.merge sideff rigid evd.universes ctx'} -let merge_uctx_subst uctx s = - { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } - let merge_universe_subst evd subst = - {evd with universes = merge_uctx_subst evd.universes subst } + {evd with universes = UState.merge_subst evd.universes subst } let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) -let emit_universe_side_effects eff u = - Declareops.fold_side_effects - (fun acc eff -> - match eff with - | Declarations.SEscheme (l,s) -> - List.fold_left - (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx - in if cb.Declarations.const_polymorphic then acc - else - merge_uctx true univ_rigid acc - (Univ.ContextSet.of_context cb.Declarations.const_universes)) - acc l - | Declarations.SEsubproof _ -> acc) - u eff - -let add_uctx_names s l (names, names_rev) = - (UNameMap.add s l names, Univ.LMap.add l s names_rev) - -let uctx_new_univ_variable rigid name predicative - ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level (Global.current_dirpath ()) in - let ctx' = Univ.ContextSet.add_universe u ctx in - let uctx', pred = - match rigid with - | UnivRigid -> uctx, true - | UnivFlexible b -> - let uvars' = Univ.LMap.add u None uvars in - if b then {uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = Univ.LSet.add u avars}, false - else {uctx with uctx_univ_variables = uvars'}, false - in - let names = - match name with - | Some n -> add_uctx_names n u uctx.uctx_names - | None -> uctx.uctx_names - in - let initial = - UGraph.add_universe u false uctx.uctx_initial_universes - in - let uctx' = - {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = UGraph.add_universe u false uctx.uctx_universes; - uctx_initial_universes = initial} - in uctx', u - let new_univ_level_variable ?name ?(predicative=true) rigid evd = - let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in + let uctx', u = UState.new_univ_variable rigid name evd.universes in ({evd with universes = uctx'}, u) let new_univ_variable ?name ?(predicative=true) rigid evd = - let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in + let uctx', u = UState.new_univ_variable rigid name evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) let new_sort_variable ?name ?(predicative=true) rigid d = @@ -1094,42 +779,12 @@ let new_sort_variable ?name ?(predicative=true) rigid d = (d', Type u) let add_global_univ d u = - let uctx = d.universes in - let initial = - UGraph.add_universe u true uctx.uctx_initial_universes - in - let univs = - UGraph.add_universe u true uctx.uctx_universes - in - { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; - uctx_initial_universes = initial; - uctx_universes = univs } } - + { d with universes = UState.add_global_univ d.universes u } + let make_flexible_variable evd b u = - let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in - let uvars' = Univ.LMap.add u None uvars in - let avars' = - if b then - let uu = Univ.Universe.make u in - let substu_not_alg u' v = - Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v - in - if not (Univ.LMap.exists substu_not_alg uvars) - then Univ.LSet.add u avars else avars - else avars - in - {evd with universes = {ctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = avars'}} - -let make_evar_universe_context e l = - let uctx = evar_universe_context_from e in - match l with - | None -> uctx - | Some us -> - List.fold_left - (fun uctx (loc,id) -> - fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx)) - uctx us + { evd with universes = UState.make_flexible_variable evd.universes b u } + +let make_evar_universe_context = UState.make (****************************************) (* Operations on constants *) @@ -1152,20 +807,11 @@ let fresh_global ?(rigid=univ_flexible) ?names env evd gr = let whd_sort_variable evd t = t -let is_sort_variable evd s = - match s with - | Type u -> - (match Univ.universe_level u with - | Some l as x -> - let uctx = evd.universes in - if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x - else None - | None -> None) - | _ -> None +let is_sort_variable evd s = UState.is_sort_variable evd.universes s let is_flexible_level evd l = let uctx = evd.universes in - Univ.LMap.mem l uctx.uctx_univ_variables + Univ.LMap.mem l (UState.subst uctx) let is_eq_sort s1 s2 = if Sorts.equal s1 s2 then None @@ -1176,12 +822,12 @@ let is_eq_sort s1 s2 = else Some (u1, u2) let normalize_universe evd = - let vars = ref evd.universes.uctx_univ_variables in + let vars = ref (UState.subst evd.universes) in let normalize = Universes.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = - let vars = ref evd.universes.uctx_univ_variables in + let vars = ref (UState.subst evd.universes) in let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l @@ -1239,96 +885,28 @@ let set_leq_sort env evd s1 s2 = else evd let check_eq evd s s' = - UGraph.check_eq evd.universes.uctx_universes s s' + UGraph.check_eq (UState.ugraph evd.universes) s s' let check_leq evd s s' = - UGraph.check_leq evd.universes.uctx_universes s s' - -let subst_univs_context_with_def def usubst (ctx, cst) = - (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) + UGraph.check_leq (UState.ugraph evd.universes) s s' -let normalize_evar_universe_context_variables uctx = - let normalized_variables, undef, def, subst = - Universes.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 - subst, { uctx with uctx_local = ctx_local'; - uctx_univ_variables = normalized_variables; - uctx_universes = univs } +let normalize_evar_universe_context_variables = UState.normalize_variables (* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *) (* let normalize_evar_universe_context_variables = *) (* Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *) -let abstract_undefined_variables uctx = - let vars' = - Univ.LMap.fold (fun u v acc -> - if v == None then Univ.LSet.remove u acc - else acc) - uctx.uctx_univ_variables uctx.uctx_univ_algebraic - in { uctx with uctx_local = Univ.ContextSet.empty; - uctx_univ_algebraic = vars' } - -let fix_undefined_variables ({ universes = uctx } as evm) = - let algs', vars' = - Univ.LMap.fold (fun u v (algs, vars as acc) -> - if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) - else acc) - uctx.uctx_univ_variables - (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) - in - {evm with universes = - { uctx with uctx_univ_variables = vars'; - uctx_univ_algebraic = algs' } } +let abstract_undefined_variables = UState.abstract_undefined_variables - -let refresh_undefined_univ_variables uctx = - let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in - let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) - uctx.uctx_univ_algebraic Univ.LSet.empty - in - let vars = - Univ.LMap.fold - (fun u v acc -> - Univ.LMap.add (Univ.subst_univs_level_level subst u) - (Option.map (Univ.subst_univs_level_universe subst) v) acc) - uctx.uctx_univ_variables Univ.LMap.empty - in - let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) - (Univ.ContextSet.levels ctx') g in - let initial = declare uctx.uctx_initial_universes in - let univs = declare UGraph.initial_universes in - let uctx' = {uctx_names = uctx.uctx_names; - uctx_local = ctx'; - uctx_univ_variables = vars; uctx_univ_algebraic = alg; - uctx_universes = univs; - uctx_initial_universes = initial } in - uctx', subst +let fix_undefined_variables evd = + { evd with universes = UState.fix_undefined_variables evd.universes } let refresh_undefined_universes evd = - let uctx', subst = refresh_undefined_univ_variables evd.universes in + let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in evd', subst -let normalize_evar_universe_context uctx = - let rec fixpoint uctx = - let ((vars',algs'), us') = - Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables - uctx.uctx_univ_algebraic - in - if Univ.ContextSet.equal us' uctx.uctx_local then uctx - else - let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in - let uctx' = - { uctx_names = uctx.uctx_names; - uctx_local = us'; - uctx_univ_variables = vars'; - uctx_univ_algebraic = algs'; - uctx_universes = universes; - uctx_initial_universes = uctx.uctx_initial_universes } - in fixpoint uctx' - in fixpoint uctx +let normalize_evar_universe_context = UState.normalize let nf_univ_variables evd = let subst, uctx' = normalize_evar_universe_context_variables evd.universes in @@ -1346,14 +924,12 @@ let nf_constraints = Profile.profile1 nfconstrkey nf_constraints else nf_constraints -let universe_of_name evd s = - UNameMap.find s (fst evd.universes.uctx_names) +let universe_of_name evd s = UState.universe_of_name evd.universes s let add_universe_name evd s l = - let names' = add_uctx_names s l evd.universes.uctx_names in - {evd with universes = {evd.universes with uctx_names = names'}} + { evd with universes = UState.add_universe_name evd.universes s l } -let universes evd = evd.universes.uctx_universes +let universes evd = UState.ugraph evd.universes (* Conversion w.r.t. an evar map and its local universes. *) @@ -1362,10 +938,10 @@ let conversion_gen env evd pb t u = | Reduction.CONV -> Reduction.trans_conv_universes full_transparent_state ~evars:(existential_opt_value evd) env - evd.universes.uctx_universes t u + (UState.ugraph evd.universes) t u | Reduction.CUMUL -> Reduction.trans_conv_leq_universes full_transparent_state ~evars:(existential_opt_value evd) env - evd.universes.uctx_universes t u + (UState.ugraph evd.universes) t u (* let conversion_gen_key = Profile.declare_profile "conversion_gen" *) (* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *) @@ -1377,8 +953,10 @@ let test_conversion env d pb t u = try conversion_gen env d pb t u; true with _ -> false +exception UniversesDiffer = UState.UniversesDiffer + let eq_constr_univs evd t u = - let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in + let b, c = Universes.eq_constr_univs_infer (UState.ugraph evd.universes) t u in if b then try let evd' = add_universe_constraints evd c in evd', b with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false @@ -1393,7 +971,7 @@ let e_eq_constr_univs evdref t u = let emit_side_effects eff evd = { evd with effects = Declareops.union_side_effects eff evd.effects; - universes = emit_universe_side_effects eff evd.universes } + universes = UState.emit_side_effects eff evd.universes } let drop_side_effects evd = { evd with effects = Declareops.no_seff; } @@ -1760,11 +1338,11 @@ let pr_evar_universe_context ctx = if is_empty_evar_universe_context ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++ + h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set Univ.UContext.empty ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ - h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++ + h 0 (Univ.LSet.pr prl (UState.variables ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl()) + h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl()) let print_env_short env = let pr_body n = function diff --git a/engine/evd.mli b/engine/evd.mli index d659b8826..796f50374 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -119,7 +119,7 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info (** {6 Unification state} **) -type evar_universe_context +type evar_universe_context = UState.t (** The universe context associated to an evar map *) type evar_map @@ -464,7 +464,7 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map (** Rigid or flexible universe variables *) -type rigid = +type rigid = UState.rigid = | UnivRigid | UnivFlexible of bool (** Is substitution by an algebraic ok? *) diff --git a/engine/uState.ml b/engine/uState.ml new file mode 100644 index 000000000..2eb0519b7 --- /dev/null +++ b/engine/uState.ml @@ -0,0 +1,484 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Errors +open Util +open Names + +module StringOrd = struct type t = string let compare = String.compare end +module UNameMap = struct + + include Map.Make(StringOrd) + + let union s t = + if s == t then s + else + merge (fun k l r -> + match l, r with + | Some _, _ -> l + | _, _ -> r) s t +end + +(* 2nd part used to check consistency on the fly. *) +type t = + { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; + uctx_local : Univ.universe_context_set; (** The local context of variables *) + uctx_univ_variables : Universes.universe_opt_subst; + (** The local universes that are unification variables *) + uctx_univ_algebraic : Univ.universe_set; + (** The subset of unification variables that + can be instantiated with algebraic universes as they appear in types + and universe instances only. *) + uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) + uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) + } + +let empty = + { uctx_names = UNameMap.empty, Univ.LMap.empty; + uctx_local = Univ.ContextSet.empty; + uctx_univ_variables = Univ.LMap.empty; + uctx_univ_algebraic = Univ.LSet.empty; + uctx_universes = UGraph.initial_universes; + uctx_initial_universes = UGraph.initial_universes } + +let from e = + let u = Environ.universes e in + { empty with + uctx_universes = u; uctx_initial_universes = u} + +let is_empty ctx = + Univ.ContextSet.is_empty ctx.uctx_local && + Univ.LMap.is_empty ctx.uctx_univ_variables + +let union ctx ctx' = + if ctx == ctx' then ctx + else if is_empty ctx' then ctx + else + let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in + let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in + let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) + (Univ.ContextSet.levels ctx.uctx_local) in + let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in + let declarenew g = + Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g + in + let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in + { uctx_names = (names, names_rev); + uctx_local = local; + uctx_univ_variables = + Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; + uctx_univ_algebraic = + Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; + uctx_initial_universes = declarenew ctx.uctx_initial_universes; + uctx_universes = + if local == ctx.uctx_local then ctx.uctx_universes + else + let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in + UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } + +let context_set diff ctx = + let initctx = ctx.uctx_local in + let cstrs = + Univ.LSet.fold + (fun l cstrs -> + try + match Univ.LMap.find l ctx.uctx_univ_variables with + | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs + | None -> cstrs + with Not_found | Option.IsNone -> cstrs) + (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty + in + Univ.ContextSet.add_constraints cstrs initctx + +let constraints ctx = snd ctx.uctx_local + +let context ctx = Univ.ContextSet.to_context ctx.uctx_local + +let of_context_set ctx = { empty with uctx_local = ctx } + +let subst ctx = ctx.uctx_univ_variables + +let ugraph ctx = ctx.uctx_universes + +let variables ctx = ctx.uctx_univ_algebraic + +let instantiate_variable l b v = + v := Univ.LMap.add l (Some b) !v + +exception UniversesDiffer + +let process_universe_constraints univs vars alg cstrs = + let vars = ref vars in + let normalize = Universes.normalize_universe_opt_subst vars in + let rec unify_universes fo 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 alg) + in + if d == Universes.ULe then + 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 + else + match Univ.Universe.level r with + | None -> error ("Algebraic universe on the right") + | Some rl -> + if Univ.Level.is_small rl 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 + 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 + | _, _ -> 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)) + in + let local = + Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) + cstrs Univ.Constraint.empty + in + !vars, local + +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' = + if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r) + else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r) + in Universes.Constraints.add cstr' acc) + cstrs Universes.Constraints.empty + in + let vars, local' = + process_universe_constraints ctx.uctx_universes + ctx.uctx_univ_variables ctx.uctx_univ_algebraic + cstrs' + in + { ctx with uctx_local = (univs, Univ.Constraint.union local local'); + uctx_univ_variables = vars; + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } + +(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) +(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) + +let add_universe_constraints ctx cstrs = + let univs, local = ctx.uctx_local in + let vars, local' = + process_universe_constraints ctx.uctx_universes + ctx.uctx_univ_variables ctx.uctx_univ_algebraic + cstrs + in + { ctx with uctx_local = (univs, Univ.Constraint.union local local'); + uctx_univ_variables = vars; + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } + +let pr_uctx_level uctx = + let map, map_rev = uctx.uctx_names in + fun l -> + try str(Univ.LMap.find l map_rev) + with Not_found -> + Universes.pr_with_global_universes l + +let universe_context ?names ctx = + match names with + | None -> Univ.ContextSet.to_context ctx.uctx_local + | Some pl -> + let levels = Univ.ContextSet.levels ctx.uctx_local in + let newinst, left = + List.fold_right + (fun (loc,id) (newinst, acc) -> + let l = + try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) + with Not_found -> + user_err_loc (loc, "universe_context", + str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + in (l :: newinst, Univ.LSet.remove l acc)) + pl ([], levels) + in + if not (Univ.LSet.is_empty left) then + let n = Univ.LSet.cardinal left in + errorlabstrm "universe_context" + (str(CString.plural n "Universe") ++ spc () ++ + Univ.LSet.pr (pr_uctx_level ctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") + else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst), + Univ.ContextSet.constraints ctx.uctx_local) + +let restrict ctx vars = + let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in + { ctx with uctx_local = uctx' } + +type rigid = + | UnivRigid + | UnivFlexible of bool (** Is substitution by an algebraic ok? *) + +let univ_rigid = UnivRigid +let univ_flexible = UnivFlexible false +let univ_flexible_alg = UnivFlexible true + +let merge sideff rigid uctx ctx' = + let open Univ in + let levels = ContextSet.levels ctx' in + let uctx = if sideff then uctx else + match rigid with + | UnivRigid -> uctx + | UnivFlexible b -> + let fold u accu = + if LMap.mem u accu then accu + else LMap.add u None accu + in + let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in + if b then + { uctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } + 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 + let declare g = + LSet.fold (fun u g -> + try UGraph.add_universe u false g + with UGraph.AlreadyDeclared when sideff -> g) + levels g + in + let initial = declare uctx.uctx_initial_universes in + let univs = declare uctx.uctx_universes in + let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in + { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } + +let merge_subst uctx s = + { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } + +let emit_side_effects eff u = + Declareops.fold_side_effects + (fun acc eff -> + match eff with + | Declarations.SEscheme (l,s) -> + List.fold_left + (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (s, ctx) -> merge true univ_rigid acc ctx + in if cb.Declarations.const_polymorphic then acc + else + merge true univ_rigid acc + (Univ.ContextSet.of_context cb.Declarations.const_universes)) + acc l + | Declarations.SEsubproof _ -> acc) + u eff + +let add_uctx_names s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l s names_rev) + +let new_univ_variable rigid name + ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = + let u = Universes.new_univ_level (Global.current_dirpath ()) in + let ctx' = Univ.ContextSet.add_universe u ctx in + let uctx', pred = + match rigid with + | UnivRigid -> uctx, true + | UnivFlexible b -> + let uvars' = Univ.LMap.add u None uvars in + if b then {uctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = Univ.LSet.add u avars}, false + else {uctx with uctx_univ_variables = uvars'}, false + in + let names = + match name with + | Some n -> add_uctx_names n u uctx.uctx_names + | None -> uctx.uctx_names + in + let initial = + UGraph.add_universe u false uctx.uctx_initial_universes + in + let uctx' = + {uctx' with uctx_names = names; uctx_local = ctx'; + uctx_universes = UGraph.add_universe u false uctx.uctx_universes; + uctx_initial_universes = initial} + in uctx', u + +let add_global_univ uctx u = + let initial = + UGraph.add_universe u true uctx.uctx_initial_universes + in + let univs = + UGraph.add_universe u true uctx.uctx_universes + in + { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; + uctx_initial_universes = initial; + uctx_universes = univs } + +let make_flexible_variable ctx b u = + let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in + let uvars' = Univ.LMap.add u None uvars in + let avars' = + if b then + let uu = Univ.Universe.make u in + let substu_not_alg u' v = + Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v + in + if not (Univ.LMap.exists substu_not_alg uvars) + then Univ.LSet.add u avars else avars + else avars + in + {ctx with uctx_univ_variables = uvars'; + uctx_univ_algebraic = avars'} + +let make e l = + let uctx = from e in + match l with + | None -> uctx + | Some us -> + List.fold_left + (fun uctx (loc,id) -> + fst (new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) + uctx us + +let is_sort_variable uctx s = + match s with + | Sorts.Type u -> + (match Univ.universe_level u with + | Some l as x -> + if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x + else None + | None -> None) + | _ -> None + +let subst_univs_context_with_def def usubst (ctx, cst) = + (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) + +let normalize_variables uctx = + let normalized_variables, undef, def, subst = + Universes.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 + subst, { uctx with uctx_local = ctx_local'; + uctx_univ_variables = normalized_variables; + uctx_universes = univs } + +let abstract_undefined_variables uctx = + let vars' = + Univ.LMap.fold (fun u v acc -> + if v == None then Univ.LSet.remove u acc + else acc) + uctx.uctx_univ_variables uctx.uctx_univ_algebraic + in { uctx with uctx_local = Univ.ContextSet.empty; + uctx_univ_algebraic = vars' } + +let fix_undefined_variables uctx = + let algs', vars' = + Univ.LMap.fold (fun u v (algs, vars as acc) -> + if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) + else acc) + uctx.uctx_univ_variables + (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) + in + { uctx with uctx_univ_variables = vars'; + uctx_univ_algebraic = algs' } + +let refresh_undefined_univ_variables uctx = + let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in + let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) + uctx.uctx_univ_algebraic Univ.LSet.empty + in + let vars = + Univ.LMap.fold + (fun u v acc -> + Univ.LMap.add (Univ.subst_univs_level_level subst u) + (Option.map (Univ.subst_univs_level_universe subst) v) acc) + uctx.uctx_univ_variables Univ.LMap.empty + in + let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) + (Univ.ContextSet.levels ctx') g in + let initial = declare uctx.uctx_initial_universes in + let univs = declare UGraph.initial_universes in + let uctx' = {uctx_names = uctx.uctx_names; + uctx_local = ctx'; + uctx_univ_variables = vars; uctx_univ_algebraic = alg; + uctx_universes = univs; + uctx_initial_universes = initial } in + uctx', subst + +let normalize uctx = + let rec fixpoint uctx = + let ((vars',algs'), us') = + Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables + uctx.uctx_univ_algebraic + in + if Univ.ContextSet.equal us' uctx.uctx_local then uctx + else + let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in + let uctx' = + { uctx_names = uctx.uctx_names; + uctx_local = us'; + uctx_univ_variables = vars'; + uctx_univ_algebraic = algs'; + uctx_universes = universes; + uctx_initial_universes = uctx.uctx_initial_universes } + in fixpoint uctx' + in fixpoint uctx + +let universe_of_name uctx s = + UNameMap.find s (fst uctx.uctx_names) + +let add_universe_name uctx s l = + let names' = add_uctx_names s l uctx.uctx_names in + { uctx with uctx_names = names' } diff --git a/engine/uState.mli b/engine/uState.mli new file mode 100644 index 000000000..c3b28d0a6 --- /dev/null +++ b/engine/uState.mli @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Universe unification states *) + +open Names + +exception UniversesDiffer + +type t + +(** {5 Constructors} *) + +val empty : t + +val from : Environ.env -> t + +val make : Environ.env -> Id.t Loc.located list option -> t + +val is_empty : t -> bool + +val union : t -> t -> t + +val of_context_set : Univ.universe_context_set -> t + +(** {5 Projections} *) + +val context_set : Univ.universe_context -> t -> Univ.universe_context_set +val constraints : t -> Univ.constraints +val context : t -> Univ.universe_context +val subst : t -> Universes.universe_opt_subst +val ugraph : t -> UGraph.t +val variables : t -> Univ.LSet.t + +(** {5 Constraints handling} *) + +val add_constraints : t -> Univ.constraints -> t +val add_universe_constraints : t -> Universes.universe_constraints -> t + +(** {5 TODO: Document me} *) + +val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context + +val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds + +val restrict : t -> Univ.universe_set -> t + +type rigid = + | UnivRigid + | UnivFlexible of bool (** Is substitution by an algebraic ok? *) + +val univ_rigid : rigid +val univ_flexible : rigid +val univ_flexible_alg : rigid + +val merge : bool -> rigid -> t -> Univ.universe_context_set -> t +val merge_subst : t -> Universes.universe_opt_subst -> t +val emit_side_effects : Declareops.side_effects -> t -> t + +val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t +val add_global_univ : t -> Univ.Level.t -> t +val make_flexible_variable : t -> bool -> Univ.Level.t -> t + +val is_sort_variable : t -> Sorts.t -> Univ.Level.t option + +val normalize_variables : t -> Univ.universe_subst * t + +val abstract_undefined_variables : t -> t + +val fix_undefined_variables : t -> t + +val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst + +val normalize : t -> t + +val universe_of_name : t -> string -> Univ.Level.t + +val add_universe_name : t -> string -> Univ.Level.t -> t |