From 57e94245e95dc71d1a0c1e0ef9270fdf643ba315 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 May 2008 15:01:31 +0000 Subject: [PATCH] map_hash moved to HExtlib --- .../components/ng_kernel/nCicSubstitution.ml | 6 +++--- .../components/ng_kernel/nCicTypeChecker.ml | 2 +- helm/software/components/ng_kernel/nCicUtils.ml | 16 ++-------------- helm/software/components/ng_kernel/nCicUtils.mli | 2 -- 4 files changed, 6 insertions(+), 20 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml index 67eb10a65..51e4244c0 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.ml +++ b/helm/software/components/ng_kernel/nCicSubstitution.ml @@ -21,7 +21,7 @@ let lift_from k n = | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t | NCic.Meta (i,(m,l)) -> let lctx = NCicUtils.expand_local_context l in - NCic.Meta (i, (m, NCic.Ctx (NCicUtils.sharing_map (liftaux (k-m)) lctx))) + NCic.Meta (i, (m, NCic.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx))) | NCic.Implicit _ -> (* was the identity *) assert false | t -> NCicUtils.map (fun _ k -> k + 1) k liftaux t in @@ -59,7 +59,7 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = let lctx = NCicUtils.expand_local_context l in (* 1-nargs < k-m, when <= 0 is still reasonable because we will * substitute args[ k-m ... k-m+nargs-1 > 0 ] *) - NCic.Meta (i,(m, NCic.Ctx (NCicUtils.sharing_map (substaux (k-m)) lctx))) + NCic.Meta (i,(m, NCic.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx))) | NCic.Implicit _ -> assert false (* was identity *) | NCic.Appl (he::tl) as t -> (* Invariant: no Appl applied to another Appl *) @@ -75,7 +75,7 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl' | _ -> if he == he' && args == tl then t else NCic.Appl (he'::args)) in - let tl = NCicUtils.sharing_map (substaux k) tl in + let tl = HExtlib.sharing_map (substaux k) tl in avoid (substaux k he) tl | t -> NCicUtils.map (fun _ k -> k + 1) k substaux t in diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 9db93f0e1..a62238cfb 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -107,7 +107,7 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context = let res = match t with | C.Meta (i,(s,C.Ctx l)) -> - let l1 = U.sharing_map (aux (k-s)) l in + let l1 = HExtlib.sharing_map (aux (k-s)) l in if l1 == l then t else C.Meta (i,(s,C.Ctx l1)) | C.Meta _ -> t | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml index b2312d101..3d3c2d90e 100644 --- a/helm/software/components/ng_kernel/nCicUtils.ml +++ b/helm/software/components/ng_kernel/nCicUtils.ml @@ -50,18 +50,6 @@ let fold g k f acc = function | NCic.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl ;; -let sharing_map f l = - let unchanged = ref true in - let rec aux b = function - | [] as t -> unchanged := b; t - | he::tl -> - let he1 = f he in - he1 :: aux (b && he1 == he) tl - in - let l1 = aux true l in - if !unchanged then l else l1 -;; - let map g k f = function | NCic.Meta _ -> assert false | NCic.Implicit _ @@ -70,7 +58,7 @@ let map g k f = function | NCic.Rel _ as t -> t | NCic.Appl [] | NCic.Appl [_] -> assert false | NCic.Appl l as orig -> - (match sharing_map (f k) l with + (match HExtlib.sharing_map (f k) l with | NCic.Appl l :: tl -> NCic.Appl (l@tl) | l1 when l == l1 -> orig | l1 -> NCic.Appl l1) @@ -85,7 +73,7 @@ let map g k f = function let b1 = f (g (n,NCic.Def (t,ty)) k) b in if ty1 == ty && t1 == t && b1 == b then orig else NCic.LetIn (n,ty1,t1,b1) | NCic.Match (r,oty,t,pl) as orig -> - let oty1 = f k oty in let t1 = f k t in let pl1 = sharing_map (f k) pl in + let oty1 = f k oty in let t1 = f k t in let pl1 = HExtlib.sharing_map (f k) pl in if oty1 == oty && t1 == t && pl1 == pl then orig else NCic.Match(r,oty1,t1,pl1) ;; diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli index 11eca58c0..c87dd6638 100644 --- a/helm/software/components/ng_kernel/nCicUtils.mli +++ b/helm/software/components/ng_kernel/nCicUtils.mli @@ -14,8 +14,6 @@ exception Subst_not_found of int exception Meta_not_found of int -val sharing_map: ('a -> 'a) -> 'a list -> 'a list - val expand_local_context : NCic.lc_kind -> NCic.term list val lookup_subst: int -> NCic.substitution -> NCic.subst_entry -- 2.39.2