; Iter 15g — fifth stdlib module: first 3-way cross-module fn set.
; Imports std_list, std_either, std_pair simultaneously. All three
; combinators dispatch over List<Either<e, a>>; partition_eithers
; additionally returns Pair<List<e>, List<a>>. Stresses
; monomorphisation across List × Either × Pair, cross-module ctor
; resolution at qualified term-ctor sites, and the 16a desugar
; layer at depth-2 nested Ctor patterns (in `lefts` / `rights`).

(module std_either_list

  (import std_list)
  (import std_either)
  (import std_pair)

  (fn lefts
    (doc "Project the Left payloads of a list of Eithers into a List<e>. Order-preserving. Uses the 16a nested-Ctor pattern to inline the inner Either dispatch within each Cons arm; the trailing wildcard arm seals the desugar's fall-through chain into a List<e> rather than the synthetic Unit fallback.")
    (type
      (forall (vars e a)
        (fn-type
          (params (con std_list.List (con std_either.Either e a)))
          (ret (con std_list.List e)))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Cons (pat-ctor Left l) t)
          (term-ctor std_list.List Cons l (app lefts t)))
        (case (pat-ctor Cons (pat-ctor Right _) t)
          (app lefts t))
        (case _ (term-ctor std_list.List Nil)))))

  (fn rights
    (doc "Project the Right payloads of a list of Eithers into a List<a>. Symmetric to lefts; same nested-Ctor + wildcard-tail pattern shape.")
    (type
      (forall (vars e a)
        (fn-type
          (params (con std_list.List (con std_either.Either e a)))
          (ret (con std_list.List a)))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Cons (pat-ctor Left _) t)
          (app rights t))
        (case (pat-ctor Cons (pat-ctor Right r) t)
          (term-ctor std_list.List Cons r (app rights t)))
        (case _ (term-ctor std_list.List Nil)))))

  (fn partition_eithers
    (doc "Partition a list of Eithers into a Pair<List<e>, List<a>>: lefts on the left, rights on the right. Single pass via direct recursion; head dispatch is a flat match on the recursive result's projections.")
    (type
      (forall (vars e a)
        (fn-type
          (params (con std_list.List (con std_either.Either e a)))
          (ret (con std_pair.Pair (con std_list.List e) (con std_list.List a))))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil)
          (term-ctor std_pair.Pair MkPair
            (term-ctor std_list.List Nil)
            (term-ctor std_list.List Nil)))
        (case (pat-ctor Cons h t)
          (let rest (app partition_eithers t)
            (match h
              (case (pat-ctor Left l)
                (term-ctor std_pair.Pair MkPair
                  (term-ctor std_list.List Cons l (app std_pair.fst rest))
                  (app std_pair.snd rest)))
              (case (pat-ctor Right r)
                (term-ctor std_pair.Pair MkPair
                  (app std_pair.fst rest)
                  (term-ctor std_list.List Cons r (app std_pair.snd rest)))))))))))
