diff options
-rw-r--r-- | checker/term.ml | 74 | ||||
-rw-r--r-- | checker/term.mli | 4 | ||||
-rw-r--r-- | checker/univ.ml | 39 | ||||
-rw-r--r-- | checker/univ.mli | 7 |
4 files changed, 0 insertions, 124 deletions
diff --git a/checker/term.ml b/checker/term.ml index 3438f497a..1b8177325 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -404,77 +404,6 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c -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 t with - | Sort (Type u) -> - let u' = fu u in - if u' == u then t else - (changed := true; Sort (Type u')) - | Const (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; Const (c, u')) - | Ind (i, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; Ind (i, u')) - | Construct (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; Construct (c, u')) - | _ -> map_constr 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_level_constr subst c = - if Univ.is_empty_level_subst subst then c - else - let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in - let changed = ref false in - let rec aux t = - match t with - | Const (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Const (c, u')) - | Ind (i, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Ind (i, u')) - | Construct (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Construct (c, u')) - | Sort (Type u) -> - let u' = Univ.subst_univs_level_universe subst u in - if u' == u then t else - (changed := true; Sort (Type u')) - | _ -> map_constr aux t - in - let c' = aux c in - if !changed then c' else c - -let subst_univs_level_context s = - map_rel_context (subst_univs_level_constr s) - let subst_instance_constr subst c = if Univ.Instance.is_empty subst then c else @@ -509,9 +438,6 @@ let subst_instance_constr subst c = let c' = aux c in if !changed then c' else c -(* let substkey = Profile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) - let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else map_rel_context (fun x -> subst_instance_constr s x) ctx diff --git a/checker/term.mli b/checker/term.mli index 3c4835dbb..ab488b2b7 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -53,10 +53,6 @@ val isArity : constr -> bool val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val eq_constr : constr -> constr -> bool -val subst_univs_constr : Univ.universe_subst -> constr -> constr -val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr -val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context - (** Instance substitution for polymorphism. *) val subst_instance_constr : Univ.universe_instance -> constr -> constr val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context diff --git a/checker/univ.ml b/checker/univ.ml index 04897e85c..a895021f0 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1299,14 +1299,7 @@ type universe_context = UContext.t (** Substitutions. *) -let make_universe_subst inst (ctx, csts) = - try Array.fold_left2 (fun acc c i -> LMap.add c i acc) - LMap.empty (Instance.to_array ctx) (Instance.to_array inst) - with Invalid_argument _ -> - anomaly (Pp.str "Mismatched instance and context when building universe substitution") - let is_empty_subst = LMap.is_empty - let empty_level_subst = LMap.empty let is_empty_level_subst = LMap.is_empty @@ -1322,20 +1315,6 @@ let subst_univs_level_universe subst u = let u' = Universe.smartmap f u in if u == u' then u else Universe.sort u' - -let subst_univs_level_constraint subst (u,d,v) = - let u' = subst_univs_level_level subst u - and v' = subst_univs_level_level subst v in - if d != Lt && Level.equal u' v' then None - else Some (u',d,v') - -let subst_univs_level_constraints subst csts = - Constraint.fold - (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) - csts Constraint.empty - -(* let instantiate_univ_context subst (_, csts) = *) -(* subst_univs_level_constraints subst csts *) (** Substitute instance inst for ctx in csts *) @@ -1395,24 +1374,6 @@ 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_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 - (** Pretty-printing *) let pr_arc = function diff --git a/checker/univ.mli b/checker/univ.mli index 27f4c9a6e..89dd64486 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -197,19 +197,12 @@ val is_empty_level_subst : universe_level_subst -> bool val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe -(** Make a universe level substitution: the instances must match. *) -val make_universe_subst : Instance.t -> universe_context -> universe_level_subst -(** Get the instantiated graph. *) -val instantiate_univ_context : universe_level_subst -> universe_context -> constraints - (** Level to universe substitutions. *) val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn val subst_univs_universe : universe_subst_fn -> universe -> universe -val subst_univs_constraints : universe_subst_fn -> constraints -> constraints - (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance |