; Iter it.2 positive (spec D1, DD-3): mutual structural recursion
; over one ADT family. `Tree` references `Forest` (the `Node` field)
; and `Forest` references `Tree` and `Forest` (the `Cons` fields), so
; the union-find of the ADT type-reference graph puts {Tree, Forest}
; in a single connected component. `tree_size` recurses into
; `forest_size` on the `Node`-bound `f` (structurally smaller); each
; `forest_size` self/cross call passes a `Cons`-bound sub-component.
; The whole mutual group is structural: pure, total, Diverge-free,
; no `tail-app` markers.

(module struct_rec_tree_forest

  (data Tree
    (ctor Node (con Int) (con Forest)))

  (data Forest
    (ctor FNil)
    (ctor FCons (con Tree) (con Forest)))

  (fn tree_size
    (doc "Node count of a tree; recurses into forest_size on the Node forest.")
    (type
      (fn-type
        (params (con Tree))
        (ret (con Int))))
    (params tr)
    (body
      (match tr
        (case (pat-ctor Node v f)
          (app + 1 (app forest_size f))))))

  (fn forest_size
    (doc "Node count of a forest; mutual with tree_size, self on the tail.")
    (type
      (fn-type
        (params (con Forest))
        (ret (con Int))))
    (params fo)
    (body
      (match fo
        (case (pat-ctor FNil) 0)
        (case (pat-ctor FCons t rest)
          (app + (app tree_size t) (app forest_size rest)))))))