summaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /pretyping/evd.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r--pretyping/evd.ml331
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 =