; Iter 14b design exhibit — Decision 6 form (A).
; Companion to box.ailx. Same hash-equivalence gate in Iter 14c.

(module list_map_poly

  (data List (vars a)
    (doc "Singly-linked polymorphic list.")
    (ctor Nil)
    (ctor Cons a (con List a)))

  (fn inc
    (type (fn-type (params (con Int)) (ret (con Int))))
    (params x)
    (body (app + x 1)))

  (fn map
    (doc "Apply f to every element. Recursive on the tail.")
    (type
      (forall (vars a b)
        (fn-type
          (params (fn-type (params a) (ret b))
                  (con List a))
          (ret (con List b)))))
    (params f xs)
    (body
      (match xs
        (case (pat-ctor Nil)
          (term-ctor List Nil))
        (case (pat-ctor Cons h t)
          (term-ctor List Cons
            (app f h)
            (app map f t))))))

  (fn print_list
    (type
      (fn-type
        (params (con List (con Int)))
        (ret (con Unit))
        (effects IO)))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil)
          (lit-unit))
        (case (pat-ctor Cons h t)
          (seq
            (do io/print_int h)
            (app print_list t))))))

  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (app print_list
        (app map inc
          (term-ctor List Cons 1
            (term-ctor List Cons 2
              (term-ctor List Cons 3
                (term-ctor List Nil)))))))))