diff options
Diffstat (limited to 'engine')
-rw-r--r-- | engine/evd.ml | 2 | ||||
-rw-r--r-- | engine/uState.ml | 2 | ||||
-rw-r--r-- | engine/universes.ml | 78 | ||||
-rw-r--r-- | engine/universes.mli | 5 |
4 files changed, 81 insertions, 6 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index e33c851f6..0e9472158 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -855,7 +855,7 @@ let normalize_universe evd = let normalize_universe_instance evd l = let vars = ref (UState.subst evd.universes) in - let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in + let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l let normalize_sort evars s = diff --git a/engine/uState.ml b/engine/uState.ml index 6131f4c03..6f2b3c4b2 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -516,7 +516,7 @@ let is_sort_variable uctx s = | _ -> None let subst_univs_context_with_def def usubst (ctx, cst) = - (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) + (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst) let normalize_variables uctx = let normalized_variables, undef, def, subst = diff --git a/engine/universes.ml b/engine/universes.ml index 30490ec56..eaddf98a8 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -181,6 +181,30 @@ let enforce_eq_instances_univs strict x y c = (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) ax ay c +let enforce_univ_constraint (u,d,v) = + match d with + | Eq -> enforce_eq u v + | Le -> enforce_leq u v + | Lt -> enforce_leq (super u) v + +let subst_univs_level fn l = + try Some (fn l) + with Not_found -> None + +let subst_univs_constraint fn (u,d,v as c) cstrs = + let u' = subst_univs_level fn u in + let v' = subst_univs_level fn v in + match u', v' with + | None, None -> Constraint.add c cstrs + | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs + | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs + | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs + +let subst_univs_constraints subst csts = + Constraint.fold + (fun c cstrs -> subst_univs_constraint subst c cstrs) + csts Constraint.empty + let subst_univs_universe_constraint fn (u,d,v) = let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in if Universe.equal u' v' then None @@ -519,13 +543,60 @@ let choose_canonical ctx flexible algs s = let canon = LSet.choose algs in canon, (global, rigid, LSet.remove canon flexible) +let level_subst_of f = + fun l -> + try let u = f l in + match Universe.level u with + | None -> l + | Some l -> l + with Not_found -> l + +let subst_univs_fn_constr f c = + let changed = ref false in + let fu = Univ.subst_univs_universe f in + let fi = Univ.Instance.subst_fn (level_subst_of f) in + let rec aux t = + match kind t with + | Sort (Sorts.Type u) -> + let u' = fu u in + if u' == u then t else + (changed := true; mkSort (Sorts.sort_of_univ u')) + | Const (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkConstU (c, u')) + | Ind (i, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkIndU (i, u')) + | Construct (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkConstructU (c, u')) + | _ -> map aux t + in + let c' = aux c in + if !changed then c' else c + +let subst_univs_constr subst c = + if Univ.is_empty_subst subst then c + else + let f = Univ.make_subst subst in + subst_univs_fn_constr f c + +let subst_univs_constr = + if Flags.profile then + let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in + CProfile.profile2 subst_univs_constr_key subst_univs_constr + else subst_univs_constr + let subst_univs_fn_puniverses lsubst (c, u as cu) = let u' = Instance.subst_fn lsubst u in if u' == u then cu else (c, u') let nf_evars_and_universes_opt_subst f subst = let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in - let lsubst = Univ.level_subst_of subst in + let lsubst = level_subst_of subst in let rec aux c = match kind c with | Evar (evk, args) -> @@ -605,7 +676,7 @@ let normalize_opt_subst ctx = in !ectx type universe_opt_subst = Universe.t option universe_map - + let make_opt_subst s = fun x -> (match Univ.LMap.find x s with @@ -614,8 +685,7 @@ let make_opt_subst s = let subst_opt_univs_constr s = let f = make_opt_subst s in - Vars.subst_univs_fn_constr f - + subst_univs_fn_constr f let normalize_univ_variables ctx = let ctx = normalize_opt_subst ctx in diff --git a/engine/universes.mli b/engine/universes.mli index 1a98d969b..130dcf8bb 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -154,6 +154,11 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> module UF : Unionfind.PartitionSig with type elt = Level.t +val level_subst_of : universe_subst_fn -> universe_level_subst_fn +val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t + +val subst_univs_constr : universe_subst -> constr -> constr + type universe_opt_subst = Universe.t option universe_map val make_opt_subst : universe_opt_subst -> universe_subst_fn |