-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.Lambda (_, t1, t2)
- | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
- | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) 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