From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 May 2008 17:11:19 +0000 (+0000)
Subject: debruijn simplified. It could go in nCicUtils, but why should we do that?
X-Git-Tag: make_still_working~5206
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1441da29ab40f8c93cf1cae9ca3333867da57484;p=helm.git

debruijn simplified. It could go in nCicUtils, but why should we do that?
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 2f8f69a41..7995f5c87 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -102,20 +102,17 @@ let rec split_prods ~subst context n te =
    | (_, _) -> raise (AssertFailure (lazy "split_prods"))
 ;;
 
-let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context = 
+let debruijn uri number_of_types context = 
  let rec aux k t =
-  let res =
-   match t with
-    | C.Meta (i,(s,C.Ctx l)) ->
-       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))) 
-    | C.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
-       C.Rel (k + number_of_types - no)
-    | t -> U.map (fun _ k -> k+1) k aux t
-  in
-   cb t res; res
+  match t with
+   | C.Meta (i,(s,C.Ctx l)) ->
+      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))) 
+   | C.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
+      C.Rel (k + number_of_types - no)
+   | t -> U.map (fun _ k -> k+1) k aux t
  in
   aux (List.length context)
 ;;