; Iter 16b.4 — LetRec captures of match-arm pattern bindings.
; `count_below(p)` takes a `Pair Int Int` (threshold, n), pattern-
; matches on `(MkPair threshold n)`, and inside that match arm runs
; a recursive helper `loop` that captures BOTH match-arm bindings
; (`threshold` and `n`) and counts how many integers in 1..=n are
; strictly less than `threshold`.
;
; The 16b.2/16b.3 desugar passes cannot lift this LetRec — both
; `threshold` and `n` are bound by a `Pattern::Ctor` Var sub-
; pattern (`ScopeEntry::MatchArm`). Before 16b.4 this panicked at
; desugar time. Now the desugar pass leaves the LetRec in place;
; the post-typecheck `lift_letrecs` pass walks the enclosing match,
; resolves each pattern binding's type via constructor-field
; substitution against the matched ctor's declared field types
; (here: `Pair Int Int`'s ctor `MkPair` has fields `[Int, Int]`,
; and the scrutinee's `Type::Con.args` are also `[Int, Int]`, so
; substitution is a no-op and both bindings get type `Int`), and
; lifts to `loop$lr_0(i: Int, threshold: Int, n: Int) -> Int`.
;
; The match has a single ctor and no catch-all; the chain machinery
; treats the only arm as default-dominating since there's no `_`
; arm needed for an exhaustive single-ctor ADT (Pair has one ctor).
;
; Expected stdout (one per line):
;   count_below(MkPair 10 0)  = 0
;   count_below(MkPair 10 5)  = 5  (1..=5 all below 10)
;   count_below(MkPair 10 15) = 9  (1..=9 below 10, 10..=15 not)

(module local_rec_match_capture

  (data Pair (vars a b)
    (ctor MkPair a b))

  (fn count_below
    (doc "Match-arm captures `threshold` and `n`; inner LetRec captures both.")
    (type (fn-type (params (own (con Pair (con Int) (con Int)))) (ret (own (con Int)))))
    (params p)
    (body
      (match p
        (case (pat-ctor MkPair threshold n)
          (let-rec loop
            (params i)
            (type (fn-type (params (own (con Int))) (ret (own (con Int)))))
            (body
              (if (app gt i n)
                0
                (if (app lt i threshold)
                  (app + 1 (app loop (app + i 1)))
                  (app loop (app + i 1)))))
            (in (app loop 1)))))))

  (fn main
    (doc "Drive count_below at MkPair 10 {0,5,15}. Expected: 0, 5, 9.")
    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
    (params)
    (body
      (seq (seq (app print (app count_below (term-ctor Pair MkPair 10 0))) (do io/print_str "\n"))
      (seq (seq (app print (app count_below (term-ctor Pair MkPair 10 5))) (do io/print_str "\n"))
           (seq (app print (app count_below (term-ctor Pair MkPair 10 15))) (do io/print_str "\n")))))))