; Fieldtest cut55-1 — decision (a): a list helper that READS without consuming.
;
; As an author reading the ledger (model/contract 0008): "reach for
; `borrow` only to read/pass-through a heap value you were lent". A
; length count walks the list and reads it; it does not move any heap
; field out. So `xs` should be `(borrow (con List))`. The recursive
; call passes the tail through in a read position — still a borrow.
;
; Expected: ail check -> ok. ail run -> prints 3.

(module cut55_1_readonly_length

  (data List
    (doc "Monomorphic Int list.")
    (ctor Nil)
    (ctor Cons (con Int) (con List)))

  (fn length
    (doc "Borrow xs and count its elements without consuming it.")
    (type
      (fn-type
        (params (borrow (con List)))
        (ret (own (con Int)))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil) 0)
        (case (pat-ctor Cons h t)
          (app + 1 (app length t))))))

  (fn main
    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
    (params)
    (body
      (let xs
        (term-ctor List Cons 10
          (term-ctor List Cons 20
            (term-ctor List Cons 30
              (term-ctor List Nil))))
        (seq (app print (app length xs)) (do io/print_str "\n"))))))