X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicInspect.ml;h=7186fb1f1585bc901e0c3cc4a8e4f0f8aadee26b;hb=1b8fc00fe0bac1e6ba9382c9b5a7fe761dedda31;hp=a1e94e247649f4fd6e5cd3237d3f15a4fd918fa3;hpb=cf4301b669442bdd78984d3a3a1e38660db1f2ea;p=helm.git

diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml
index a1e94e247..7186fb1f1 100644
--- a/helm/software/components/cic/cicInspect.ml
+++ b/helm/software/components/cic/cicInspect.ml
@@ -56,9 +56,10 @@ let get_rels_from_premise h t =
 	 in
 	 List.fold_left map g ss
       | C.Cast (t1, t2)    -> aux d (aux d g t2) t1
-      | C.LetIn (_, t1, t2)
       | C.Lambda (_, t1, t2)
       | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
+      | C.LetIn (_, t1, ty, t2) ->
+         aux d (aux d (aux (succ d) g t2) ty) t1
       | C.MutCase (_, _, t1, t2, ss) ->
 	 aux d (aux d (List.fold_left (aux d) g ss) t2) t1
       | C.Fix (_, ss) ->
@@ -95,9 +96,9 @@ let get_mutinds_of_uri u t =
 	 in
 	 List.fold_left map g ss
       | C.Cast (t1, t2)              -> aux (aux g t2) t1
-      | C.LetIn (_, t1, t2)
       | C.Lambda (_, t1, t2)
-      | C.Prod (_, t1, t2)           -> aux (aux g t2) t1
+      | C.Prod (_, t1, t2) -> aux (aux g t2) t1
+      | C.LetIn (_, t1, ty, t2) -> aux (aux (aux g t2) ty) t1
       | C.MutCase (_, _, t1, t2, ss) ->
 	 aux (aux (List.fold_left aux g ss) t2) t1
       | C.Fix (_, ss)                ->
@@ -110,34 +111,37 @@ let get_mutinds_of_uri u t =
    let g a = a in
    aux g t S.empty
 
-let rec aux n = function
-   | C.Sort _
-   | C.Implicit _
-   | C.Rel _                      -> succ n
-   | C.Appl ts                    -> List.fold_left aux (succ n) ts
-   | C.Const (_, ss)
-   | C.MutConstruct (_, _, _, ss)
-   | C.MutInd (_, _, ss)
-   | C.Var (_, ss)                -> 
-      let map n (_, t) = aux n t in 
-      List.fold_left map (succ n) ss
-   | C.Meta (_, ss)               ->
-      let map n = function 
-	 | None   -> n
-	 | Some t -> aux n t
-      in
-      List.fold_left map (succ n) ss
-   | C.Cast (t1, t2)
-   | C.LetIn (_, t1, t2)
-   | C.Lambda (_, t1, t2)
-   | C.Prod (_, t1, t2)           -> aux (aux (succ n) t2) t1
-   | C.MutCase (_, _, t1, t2, ss) ->
-      aux (aux (List.fold_left aux (succ n) ss) t2) t1
-   | C.Fix (_, ss)                ->
-      let map n (_, _, t1, t2) = aux (aux n t2) t1 in
-      List.fold_left map (succ n) ss
-   | C.CoFix (_, ss)              ->
-      let map n (_, t1, t2) = aux (aux n t2) t1 in
-      List.fold_left map (succ n) ss
-
-let count_nodes = aux
+let count_nodes ~meta n t =
+   let offset = if meta then 1 else 0 in
+   let rec aux n = function
+      | C.Implicit _                 -> offset + n
+      | C.Sort _
+      | C.Rel _                      -> succ n
+      | C.Appl ts                    -> 
+         List.fold_left aux (List.length ts - 1 + n) ts
+      | C.Const (_, ss)
+      | C.MutConstruct (_, _, _, ss)
+      | C.MutInd (_, _, ss)
+      | C.Var (_, ss)                -> 
+         let map n (_, t) = aux n t in 
+         List.fold_left map (succ n) ss
+      | C.Meta (_, ss)               ->
+         let map n = function 
+	    | None   -> n
+	    | Some t -> aux n t
+         in
+         List.fold_left map (n + offset) ss
+      | C.Cast (t1, t2) -> aux (aux (offset + n) t2) t1
+      | C.Lambda (_, t1, t2)
+      | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
+      | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (offset + n) t2) ty) t1
+      | C.MutCase (_, _, t1, t2, ss) ->
+         aux (aux (List.fold_left aux (offset + 1 + n) ss) t2) t1
+      | C.Fix (_, ss)                ->
+         let map n (_, _, t1, t2) = aux (aux n t2) t1 in
+         List.fold_left map (2 + n) ss
+      | C.CoFix (_, ss)              ->
+         let map n (_, t1, t2) = aux (aux n t2) t1 in
+         List.fold_left map (2 + n) ss
+in
+aux n t