diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 331 |
1 files changed, 225 insertions, 106 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index bf519fb7..4a9466f4 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -277,15 +277,14 @@ end 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 : Univ.universes; (** The current graph extended with the local constraints *) - uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *) - } + 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 inferred types only. *) + uctx_universes : Univ.universes; (** The current graph extended with the local constraints *) + uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *) + } let empty_evar_universe_context = { uctx_names = UNameMap.empty, Univ.LMap.empty; @@ -310,6 +309,12 @@ let union_evar_universe_context ctx 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 -> Univ.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; @@ -317,12 +322,12 @@ let union_evar_universe_context ctx ctx' = 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 = ctx.uctx_initial_universes; + 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 - Univ.merge_constraints cstrsr ctx.uctx_universes } + Univ.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 = *) @@ -330,17 +335,38 @@ let union_evar_universe_context ctx ctx' = type 'a in_evar_universe_context = 'a * evar_universe_context -let evar_universe_context_set ctx = ctx.uctx_local +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 add_uctx_names s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l s names_rev) + +let evar_universe_context_of_binders b = + let ctx = empty_evar_universe_context in + let names = + List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc) + ctx.uctx_names b + in { ctx with uctx_names = names } + let instantiate_variable l b v = - (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *) - (* if Univ.univ_depends (Univ.Universe.make l) b then *) - (* error ("Occur-check in universe variable instantiation") *) - (* else *) v := Univ.LMap.add l (Some b) !v + v := Univ.LMap.add l (Some b) !v exception UniversesDiffer @@ -374,7 +400,7 @@ let process_universe_constraints univs vars alg cstrs = 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 - Univ.enforce_eq (Univ.Universe.make l) r local + 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 @@ -406,7 +432,16 @@ let process_universe_constraints univs vars alg cstrs = raise UniversesDiffer in Univ.enforce_eq_level l' r' local - | _, _ (* One of the two is algebraic or global *) -> + | 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 Univ.check_eq univs l r then local else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) in @@ -433,7 +468,7 @@ let add_constraints_context ctx cstrs = in { ctx with uctx_local = (univs, Univ.Constraint.union local local'); uctx_univ_variables = vars; - uctx_universes = Univ.merge_constraints cstrs ctx.uctx_universes } + uctx_universes = Univ.merge_constraints local' ctx.uctx_universes } (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) @@ -553,7 +588,7 @@ type evar_map = { (** Metas *) metas : clbinding Metamap.t; (** Interactive proofs *) - effects : Declareops.side_effects; + effects : Safe_typing.private_constants; future_goals : Evar.t list; (** list of newly created evars, to be eventually turned into goals if not solved.*) principal_future_goal : Evar.t option; (** if [Some e], [e] must be @@ -564,6 +599,7 @@ type evar_map = { name) of the evar which will be instantiated with a term containing [e]. *) + extras : Store.t; } (*** Lifting primitive from Evar.Map. ***) @@ -723,7 +759,7 @@ let cmap f evd = { evd with metas = Metamap.map (map_clb f) evd.metas; defn_evars = EvMap.map (map_evar_info f) evd.defn_evars; - undf_evars = EvMap.map (map_evar_info f) evd.defn_evars + undf_evars = EvMap.map (map_evar_info f) evd.undf_evars } (* spiwack: deprecated *) @@ -741,16 +777,17 @@ let empty = { conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; - effects = Declareops.no_seff; + effects = Safe_typing.empty_private_constants; evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; + extras = Store.empty; } -let from_env ?ctx e = - match ctx with - | None -> { empty with universes = evar_universe_context_from e } - | Some ctx -> { empty with universes = ctx } +let from_env e = + { empty with universes = evar_universe_context_from e } + +let from_ctx ctx = { empty with universes = ctx } let has_undefined evd = not (EvMap.is_empty evd.undf_evars) @@ -914,38 +951,6 @@ let evars_of_filtered_evar_info evi = (evars_of_named_context (evar_filtered_context evi))) (**********************************************************) -(* Side effects *) - -let emit_side_effects eff evd = - { evd with effects = Declareops.union_side_effects eff evd.effects; } - -let drop_side_effects evd = - { evd with effects = Declareops.no_seff; } - -let eval_side_effects evd = evd.effects - -(* Future goals *) -let declare_future_goal evk evd = - { evd with future_goals = evk::evd.future_goals } - -let declare_principal_goal evk evd = - match evd.principal_future_goal with - | None -> { evd with - future_goals = evk::evd.future_goals; - principal_future_goal=Some evk; } - | Some _ -> Errors.error "Only one main subgoal per instantiation." - -let future_goals evd = evd.future_goals - -let principal_future_goal evd = evd.principal_future_goal - -let reset_future_goals evd = - { evd with future_goals = [] ; principal_future_goal=None } - -let restore_future_goals evd gls pgl = - { evd with future_goals = gls ; principal_future_goal = pgl } - -(**********************************************************) (* Sort variables *) type rigid = @@ -960,19 +965,56 @@ let evar_universe_context d = d.universes let universe_context_set d = d.universes.uctx_local -let universe_context evd = - Univ.ContextSet.to_context evd.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, map, left = + List.fold_right + (fun (loc,id) (newinst, map, 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, (id, l) :: map, 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 + let inst = Univ.Instance.of_array (Array.of_list newinst) in + let ctx = Univ.UContext.make (inst, + Univ.ContextSet.constraints evd.universes.uctx_local) + in map, ctx + +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' } } + let universe_subst evd = evd.universes.uctx_univ_variables -let merge_uctx rigid uctx ctx' = +let merge_uctx sideff rigid uctx ctx' = let open Univ in - let uctx = + let levels = ContextSet.levels ctx' in + let uctx = if sideff then uctx else match rigid with | UnivRigid -> uctx | UnivFlexible b -> - let levels = ContextSet.levels ctx' in let fold u accu = if LMap.mem u accu then accu else LMap.add u None accu @@ -983,12 +1025,23 @@ let merge_uctx rigid uctx ctx' = uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } else { uctx with uctx_univ_variables = uvars' } in - let uctx_local = ContextSet.append ctx' uctx.uctx_local in - let uctx_universes = merge_constraints (ContextSet.constraints ctx') uctx.uctx_universes in - { uctx with uctx_local; uctx_universes } + 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 Univ.add_universe u false g + with Univ.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 = merge_constraints (ContextSet.constraints ctx') univs in + { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } -let merge_context_set rigid evd ctx' = - {evd with universes = merge_uctx rigid evd.universes ctx'} +let merge_context_set ?(sideff=false) rigid evd ctx' = + {evd with universes = merge_uctx 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 } @@ -999,41 +1052,61 @@ let merge_universe_subst evd subst = let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) -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 +let emit_universe_side_effects eff u = + let uctxs = Safe_typing.universes_of_private eff in + List.fold_left (merge_uctx true univ_rigid) u uctxs + +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' = + let uctx', pred = match rigid with - | UnivRigid -> uctx + | 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} - else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in + 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 = + Univ.add_universe u false uctx.uctx_initial_universes + in + let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u uctx.uctx_universes}, u - -let new_univ_level_variable ?name rigid evd = - let uctx', u = uctx_new_univ_variable rigid name evd.universes in + uctx_universes = Univ.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 ({evd with universes = uctx'}, u) -let new_univ_variable ?name rigid evd = - let uctx', u = uctx_new_univ_variable rigid name evd.universes in +let new_univ_variable ?name ?(predicative=true) rigid evd = + let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?name rigid d = - let (d', u) = new_univ_variable rigid ?name d in +let new_sort_variable ?name ?(predicative=true) rigid d = + let (d', u) = new_univ_variable rigid ?name ~predicative d in (d', Type u) +let add_global_univ d u = + let uctx = d.universes in + let initial = + Univ.add_universe u true uctx.uctx_initial_universes + in + let univs = + Univ.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 } } + 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 @@ -1050,6 +1123,16 @@ let make_flexible_variable evd b u = {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 + (****************************************) (* Operations on constants *) (****************************************) @@ -1213,12 +1296,16 @@ let refresh_undefined_univ_variables uctx = 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 + in + let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) + (Univ.ContextSet.levels ctx') g in + let initial = declare uctx.uctx_initial_universes in + let univs = declare Univ.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; uctx_local = ctx'; uctx_univ_variables = vars; uctx_univ_algebraic = alg; - uctx_universes = Univ.initial_universes; - uctx_initial_universes = uctx.uctx_initial_universes } in + uctx_universes = univs; + uctx_initial_universes = initial } in uctx', subst let refresh_undefined_universes evd = @@ -1232,8 +1319,7 @@ let normalize_evar_universe_context uctx = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic in - if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then - uctx + 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' = @@ -1271,9 +1357,18 @@ let add_universe_name evd s l = let universes evd = evd.universes.uctx_universes +let update_sigma_env evd env = + let univs = Environ.universes env in + let eunivs = + { evd.universes with uctx_initial_universes = univs; + uctx_universes = univs } + in + let eunivs = merge_uctx true univ_rigid eunivs eunivs.uctx_local in + { evd with universes = eunivs } + (* Conversion w.r.t. an evar map and its local universes. *) -let conversion_gen env evd pb t u = +let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> Reduction.trans_conv_universes @@ -1283,14 +1378,8 @@ let conversion_gen env evd pb t u = full_transparent_state ~evars:(existential_opt_value evd) env evd.universes.uctx_universes t u -(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *) -(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *) - -let conversion env d pb t u = - conversion_gen env d pb t u; d - let test_conversion env d pb t u = - try conversion_gen env d pb t u; true + try test_conversion_gen env d pb t u; true with _ -> false let eq_constr_univs evd t u = @@ -1304,8 +1393,38 @@ let e_eq_constr_univs evdref t u = let evd, b = eq_constr_univs !evdref t u in evdref := evd; b -let eq_constr_univs_test evd t u = - snd (eq_constr_univs evd t u) +(**********************************************************) +(* Side effects *) + +let emit_side_effects eff evd = + { evd with effects = Safe_typing.concat_private eff evd.effects; + universes = emit_universe_side_effects eff evd.universes } + +let drop_side_effects evd = + { evd with effects = Safe_typing.empty_private_constants; } + +let eval_side_effects evd = evd.effects + +(* Future goals *) +let declare_future_goal evk evd = + { evd with future_goals = evk::evd.future_goals } + +let declare_principal_goal evk evd = + match evd.principal_future_goal with + | None -> { evd with + future_goals = evk::evd.future_goals; + principal_future_goal=Some evk; } + | Some _ -> Errors.error "Only one main subgoal per instantiation." + +let future_goals evd = evd.future_goals + +let principal_future_goal evd = evd.principal_future_goal + +let reset_future_goals evd = + { evd with future_goals = [] ; principal_future_goal=None } + +let restore_future_goals evd gls pgl = + { evd with future_goals = gls ; principal_future_goal = pgl } (**********************************************************) (* Accessing metas *) @@ -1323,6 +1442,7 @@ let set_metas evd metas = { evar_names = evd.evar_names; future_goals = evd.future_goals; principal_future_goal = evd.principal_future_goal; + extras = evd.extras; } let meta_list evd = metamap_to_list evd.metas @@ -1471,6 +1591,12 @@ let dependent_evar_ident ev evd = | (_,Evar_kinds.VarInstance id) -> id | _ -> anomaly (str "Not an evar resulting of a dependent binding") +(**********************************************************) +(* Extra data *) + +let get_extra_data evd = evd.extras +let set_extra_data extras evd = { evd with extras } + (*******************************************************************) type pending = (* before: *) evar_map * (* after: *) evar_map @@ -1677,13 +1803,6 @@ let evar_dependency_closure n sigma = let has_no_evar sigma = EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars -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 pr_evd_level evd = pr_uctx_level evd.universes let pr_evar_universe_context ctx = |