From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 May 2008 15:01:31 +0000 (+0000)
Subject: map_hash moved to HExtlib
X-Git-Tag: make_still_working~5214
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=57e94245e95dc71d1a0c1e0ef9270fdf643ba315;p=helm.git

map_hash moved to HExtlib
---

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