From 6390887ce1fd32c2180f373f1e701d9488c341f9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 5 Sep 2014 20:31:34 +0200 Subject: Remove unused substitution functions in checker. --- checker/univ.ml | 39 --------------------------------------- 1 file changed, 39 deletions(-) (limited to 'checker/univ.ml') 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 -- cgit v1.2.3