; Iter 16b.3 — LetRec captures of `Term::Let`-bound names.
; `count_below(n)` returns how many integers in 1..=n are strictly
; less than a `threshold` computed locally from `n`. The recursive
; helper `loop` captures the let-bound name `threshold` from the
; enclosing scope; its type is only known after typecheck (the
; let-value is `(app + 5 5)` — an `Int` expression, but the desugar
; pass cannot resolve that without inference).
;
; The 16b.2 desugar pass cannot lift this LetRec (capture is Let-bound,
; not fn-param). Instead the desugar pass leaves the LetRec in place;
; the post-typecheck `lift_letrecs` pass in `ailang-check` resolves
; `threshold`'s type as `Int` from the typechecker's env and produces
; a synthetic top-level fn `loop$lr_0(i: Int, n: Int, threshold: Int)
; -> Int`, rewriting every `(app loop ARGS)` to `(app loop$lr_0 ARGS n
; threshold)`.
;
; Expected stdout (one per line):
;   count_below(0)  = 0   (empty range; loop's first call has i > n)
;   count_below(5)  = 5   (1..=5; threshold = 10; all 5 are < 10)
;   count_below(15) = 9   (1..=15; threshold = 10; 1..=9 are < 10)

(module local_rec_let_capture

  (fn count_below
    (doc "Count i in 1..=n with i < threshold, where threshold = 5+5.")
    (type (fn-type (params (con Int)) (ret (con Int))))
    (params n)
    (body
      (let threshold (app + 5 5)
        (let-rec loop
          (params i)
          (type (fn-type (params (con Int)) (ret (con Int))))
          (body
            (if (app > i n)
              0
              (if (app < 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 0, 5, 15. Expected (per line): 0, 5, 9.")
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (seq (do io/print_int (app count_below 0))
      (seq (do io/print_int (app count_below 5))
           (do io/print_int (app count_below 15)))))))
