; Iter 16a — first program to use a nested constructor pattern.
; Without this iter, the inner `(pat-ctor Cons b _)` would be
; rejected by the checker as `nested-ctor-pattern-not-allowed`.
; prep.1 migration (kernel-extension-mechanics): bare List via
; `(import std_list)`; cross-module fns / ctors stay structurally
; identical (bare types now in scope).

(module nested_pat

  (import std_list)

  (fn first_two_sum
    (doc "Sum of the first two elements of an Int list, or 0 if shorter than two.")
    (type
      (fn-type
        (params (con List (con Int)))
        (ret (con Int))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Cons a (pat-ctor Cons b _))
          (app + a b))
        (case _ 0))))

  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (app print (app first_two_sum
        (term-ctor List Cons 10
          (term-ctor List Cons 20
            (term-ctor List Cons 30
              (term-ctor List Nil)))))))))