; Iter 15f — fourth stdlib module: product types.
; Pair<a, b> is the canonical 2-type-var, single-ctor product. No
; recursion in the data def or any combinator. Combinators here
; build on the new (Iter 16a) nested-Ctor-pattern support: `swap`
; flattens via `(pat-ctor MkPair x y)` and the eliminator `pair`
; matches the same shape directly without an outer var-binding.

(module std_pair

  (data Pair (vars a b)
    (doc "Polymorphic product: a single ctor MkPair holding one value of each parameter.")
    (ctor MkPair a b))

  (fn fst
    (doc "First projection. Returns the `a` payload.")
    (type
      (forall (vars a b)
        (fn-type
          (params (con Pair a b))
          (ret a))))
    (params p)
    (body
      (match p
        (case (pat-ctor MkPair x _) x))))

  (fn snd
    (doc "Second projection. Returns the `b` payload.")
    (type
      (forall (vars a b)
        (fn-type
          (params (con Pair a b))
          (ret b))))
    (params p)
    (body
      (match p
        (case (pat-ctor MkPair _ y) y))))

  (fn swap
    (doc "Exchange the components: Pair<a, b> -> Pair<b, a>.")
    (type
      (forall (vars a b)
        (fn-type
          (params (con Pair a b))
          (ret (con Pair b a)))))
    (params p)
    (body
      (match p
        (case (pat-ctor MkPair x y)
          (term-ctor Pair MkPair y x)))))

  (fn map_first
    (doc "Apply f to the first component, leave the second intact.")
    (type
      (forall (vars a b c)
        (fn-type
          (params (fn-type (params a) (ret c))
                  (con Pair a b))
          (ret (con Pair c b)))))
    (params f p)
    (body
      (match p
        (case (pat-ctor MkPair x y)
          (term-ctor Pair MkPair (app f x) y)))))

  (fn map_second
    (doc "Apply f to the second component, leave the first intact.")
    (type
      (forall (vars a b c)
        (fn-type
          (params (fn-type (params b) (ret c))
                  (con Pair a b))
          (ret (con Pair a c)))))
    (params f p)
    (body
      (match p
        (case (pat-ctor MkPair x y)
          (term-ctor Pair MkPair x (app f y)))))))