diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 32 | ||||
| -rw-r--r-- | kernel/univ.mli | 9 | ||||
| -rw-r--r-- | kernel/vars.ml | 43 | ||||
| -rw-r--r-- | kernel/vars.mli | 6 |
4 files changed, 5 insertions, 85 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index fee431ff43..f72f6f26a9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -686,12 +686,6 @@ let enforce_leq u v c = let enforce_leq_level u v c = if Level.equal u v then c else Constraint.add (u,Le,v) 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 - (* Miscellaneous functions to remove or test local univ assumed to occur in a universe *) @@ -718,14 +712,6 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -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 - module Instance : sig type t = Level.t array @@ -1128,24 +1114,6 @@ let subst_univs_universe fn ul = List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u)) substs nosubst -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 cstrs -> subst_univs_constraint subst c cstrs) - csts Constraint.empty - let make_instance_subst i = let arr = Instance.to_array i in Array.fold_left_i (fun i acc l -> diff --git a/kernel/univ.mli b/kernel/univ.mli index 324167890a..63bef1b81b 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -238,8 +238,6 @@ type universe_level_subst_fn = Level.t -> Level.t type universe_subst = Universe.t universe_map type universe_level_subst = Level.t universe_map -val level_subst_of : universe_subst_fn -> universe_level_subst_fn - (** {6 Universe instances} *) module Instance : @@ -461,18 +459,21 @@ val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t -val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t +(** Only user in the kernel is template polymorphism. Ideally we get rid of + this code if it goes away. *) (** Substitution of instances *) val subst_instance_instance : Instance.t -> Instance.t -> Instance.t val subst_instance_universe : Instance.t -> Universe.t -> Universe.t val make_instance_subst : Instance.t -> universe_level_subst +(** Creates [u(0) ↦ 0; ...; u(n-1) ↦ n - 1] out of [u(0); ...; u(n - 1)] *) + val make_inverse_instance_subst : Instance.t -> universe_level_subst val abstract_universes : UContext.t -> Instance.t * AUContext.t - val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t +(** TODO: move universe abstraction out of the kernel *) val make_abstract_instance : AUContext.t -> Instance.t diff --git a/kernel/vars.ml b/kernel/vars.ml index eae917b5a2..b3b3eff628 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -235,49 +235,6 @@ let subst_vars subst c = substn_vars 1 subst c (** Universe substitutions *) open Constr -let subst_univs_fn_puniverses fn = - let f = Univ.Instance.subst_fn fn in - fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') - -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 (Univ.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_level_constr subst c = if Univ.is_empty_level_subst subst then c else diff --git a/kernel/vars.mli b/kernel/vars.mli index 964de4e958..b74d25260f 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -129,12 +129,6 @@ val subst_var : Id.t -> constr -> constr open Univ -val subst_univs_fn_constr : universe_subst_fn -> constr -> constr -val subst_univs_fn_puniverses : universe_level_subst_fn -> - 'a puniverses -> 'a puniverses - -val subst_univs_constr : universe_subst -> constr -> constr - (** Level substitutions for polymorphism. *) val subst_univs_level_constr : universe_level_subst -> constr -> constr |