diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 9 | ||||
| -rw-r--r-- | engine/evd.mli | 10 | ||||
| -rw-r--r-- | engine/uState.ml | 48 | ||||
| -rw-r--r-- | engine/uState.mli | 6 |
4 files changed, 38 insertions, 35 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 52bfc2d1d1..ce3e91db7f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -273,6 +273,7 @@ let evar_universe_context_subst = UState.subst let add_constraints_context = UState.add_constraints let add_universe_constraints_context = UState.add_universe_constraints let constrain_variables = UState.constrain_variables +let evar_universe_context_of_binders = UState.of_binders (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *) (* let add_universe_constraints_context = *) @@ -378,7 +379,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 @@ -579,7 +580,7 @@ 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; @@ -978,11 +979,11 @@ let e_eq_constr_univs evdref t u = (* Side effects *) let emit_side_effects eff evd = - { evd with effects = Declareops.union_side_effects eff evd.effects; + { evd with effects = Safe_typing.concat_private eff evd.effects; universes = UState.emit_side_effects eff evd.universes } let drop_side_effects evd = - { evd with effects = Declareops.no_seff; } + { evd with effects = Safe_typing.empty_private_constants; } let eval_side_effects evd = evd.effects diff --git a/engine/evd.mli b/engine/evd.mli index dc498ed42e..b295a431aa 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -259,10 +259,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t (** {5 Side-effects} *) -val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map +val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map (** Push a side-effect into the evar map. *) -val eval_side_effects : evar_map -> Declareops.side_effects +val eval_side_effects : evar_map -> Safe_typing.private_constants (** Return the effects contained in the evar map. *) val drop_side_effects : evar_map -> evar_map @@ -485,6 +485,9 @@ val evar_universe_context_subst : evar_universe_context -> Universes.universe_op val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val evar_universe_context_of_binders : + Universes.universe_binders -> evar_universe_context + val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map (** Raises Not_found if not a name for a universe in this map. *) @@ -532,7 +535,8 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context +val universe_context : ?names:(Id.t located) list -> evar_map -> + (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t diff --git a/engine/uState.ml b/engine/uState.ml index 227c4ad52b..61ab5a8fca 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -105,6 +105,16 @@ let constrain_variables diff ctx = with Not_found | Option.IsNone -> cstrs) diff Univ.Constraint.empty +let add_uctx_names s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l s names_rev) + +let of_binders b = + let ctx = empty 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 = v := Univ.LMap.add l (Some b) !v @@ -233,19 +243,19 @@ let pr_uctx_level uctx = let universe_context ?names ctx = match names with - | None -> Univ.ContextSet.to_context ctx.uctx_local + | None -> [], Univ.ContextSet.to_context ctx.uctx_local | Some pl -> let levels = Univ.ContextSet.levels ctx.uctx_local in - let newinst, left = + let newinst, map, left = List.fold_right - (fun (loc,id) (newinst, acc) -> + (fun (loc,id) (newinst, map, 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 (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 @@ -253,8 +263,11 @@ let universe_context ?names ctx = (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) + else + let inst = Univ.Instance.of_array (Array.of_list newinst) in + let ctx = Univ.UContext.make (inst, + Univ.ContextSet.constraints ctx.uctx_local) + in map, ctx let restrict ctx vars = let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in @@ -304,25 +317,8 @@ 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 uctxs = Safe_typing.universes_of_private eff in + List.fold_left (merge true univ_rigid) u uctxs let new_univ_variable rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = diff --git a/engine/uState.mli b/engine/uState.mli index 56e0fe14e5..6861035fac 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -28,6 +28,8 @@ val union : t -> t -> t val of_context_set : Univ.universe_context_set -> t +val of_binders : Universes.universe_binders -> t + (** {5 Projections} *) val context_set : t -> Univ.universe_context_set @@ -84,7 +86,7 @@ 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 emit_side_effects : Safe_typing.private_constants -> t -> t val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t val add_global_univ : t -> Univ.Level.t -> t @@ -106,7 +108,7 @@ val normalize : t -> t (** {5 TODO: Document me} *) -val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context +val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context (** {5 Pretty-printing} *) |