X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2FcicInspect.ml;h=a1e94e247649f4fd6e5cd3237d3f15a4fd918fa3;hb=9333fdbe385f6e80b272b194e88001f28dbc8d73;hp=3d5d65d59a48e0cbae302ee6d715cd3b653d1f50;hpb=72dae1a44bbed06ff9daeadf53671e109a1b882f;p=helm.git

diff --git a/components/cic/cicInspect.ml b/components/cic/cicInspect.ml
index 3d5d65d59..a1e94e247 100644
--- a/components/cic/cicInspect.ml
+++ b/components/cic/cicInspect.ml
@@ -109,3 +109,35 @@ let get_mutinds_of_uri u t =
    in
    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