diff options
| author | Matthieu Sozeau | 2014-06-10 16:42:21 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-10 16:42:21 +0200 |
| commit | 7f5975e33804d1e527f879539dfd14025f52a156 (patch) | |
| tree | 36be085062a6bf99ddff17c037e6d79687cef5fc /kernel | |
| parent | b63dff21b99070e4936a799be6e2a575e42c74d4 (diff) | |
- Fix substitution of universes which needlessly hashconsed existing universes.
- More cleanup. remove unneeded functions in universes
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 22 | ||||
| -rw-r--r-- | kernel/univ.mli | 1 |
2 files changed, 13 insertions, 10 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index e038f46e72..5eea9561b9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1984,10 +1984,6 @@ type universe_subst_fn = universe_level -> universe let make_subst subst = fun l -> LMap.find l subst -let subst_univs_level fn l = - try fn l - with Not_found -> make l - let subst_univs_expr_opt fn (l,n) = Universe.addn n (fn l) @@ -2007,14 +2003,22 @@ let subst_univs_universe fn ul = List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) substs nosubst -let subst_univs_constraint fn (u,d,v) = - let u' = subst_univs_level fn u and v' = subst_univs_level fn v in - if d != Lt && Universe.equal u' v' then None - else Some (u',d,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,make v) cstrs + | None, Some v -> enforce_univ_constraint (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 -> Option.fold_right enforce_univ_constraint (subst_univs_constraint subst c)) + (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty (** Pretty-printing *) diff --git a/kernel/univ.mli b/kernel/univ.mli index e43b19d305..a5d66eecb7 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -412,7 +412,6 @@ val empty_subst : universe_subst val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn -val subst_univs_level : universe_subst_fn -> universe_level -> universe val subst_univs_universe : universe_subst_fn -> universe -> universe val subst_univs_constraints : universe_subst_fn -> constraints -> constraints |