AGI prompt

AGI_prompt.bend.py

# Bend prelude
# ------------

type Maybe<A: Set>:
  case @None:
  case @Some:
    value: A

type Result<F: Set, D: Set>:
  case @Done:
    d: D
  case @Fail:
    f: F

def String() -> Set:
  Char[]

def Not(A: Set) -> Set:
  A -> Empty

def Bool/or(a: Bool, b: Bool) -> Bool:
  match a:
    case True:
      True
    case False:
      b

def Nat/add(a: Nat, b: Nat) -> Nat:
  match a:
    case 0n:
      b
    case 1n + p:
      1n + Nat/add(p, b)

# Natural number equality function
def Nat/eql(a: Nat, b: Nat) -> Bool:
  match a b:
    case 0n 0n:
      return True
    case 1n+a 0n:
      return False
    case 0n 1n+b:
      return False
    case 1n+a 1n+b:
      return Nat/eql(a, b)

def Nat/show(a: Nat) -> String:
  match a:
    case 0n:
      "0"
    case 1n + p:
      '↑' <> Nat/show(p)

# Returns the element at index i
def List/get<A>(xs: A[], i: Nat) -> Maybe<A>:
  match xs i:
    case [] 0n:
      return @None
    case (x <> xs) 0n:
      return @Some{x}
    case [] 1n+i:
      return @None
    case (x <> xs) 1n+i:
      return List/get<A>(xs, i)

def List/append<A>(xs: A[], ys: A[]) -> A[]:
  match xs:
    case []:
      ys
    case x <> xs:
      x <> List/append<A>(xs, ys)

def List/flat<A>(xss: A[][]) -> A[]:
  match xss:
    case []:
      []
    case xs <> xss:
      List/append<A>(xs, List/flat<A>(xss))

def String/equal(a: String, b: String) -> Bool:
  match a:
    with b
    case []:
      match b:
        case []:
          True
        case y<>ys:
          False
    case x<>xs:
      match b:
        case []:
          False
        case y<>ys:
          (x === y) and String/equal(xs, ys)

def String/flat(xs: String[]) -> String:
  List/flat<Char>(xs)

# Type
# ----

type Term:
  # Variables
  case @Var: # x
    i: Nat
  case @Nam: # x
    s: String
  case @Sub: # x
    t: Term

  # Enumeration
  case @Low: # l - h
    l: Term
    h: Term

  # References
  case @Ref: # @Name : Term = value
    k: String
    f: Term
    t: Term

  # Definitions
  case @Let: # let x : T = v; f
    T: Term
    v: Term
    f: Term -> Term

  # Fixed Point
  case @Fix: # μx. f
    f: Term -> Term

  # Universe
  case @Set: # *

  # Function
  case @All: # ∀A.B
    a: Term
    b: Term
  case @Lam: # λx.f
    f: Term -> Term
  case @App: # (f x)
    f: Term
    x: Term

  # Empty
  case @Emp:  # ⊥
  case @EmpM: # λ{}

  # Unit
  case @Uni:  # ⊤
  case @One:  # ()
  case @UniM: # λ{ (): f }
    f: Term

  # Bit
  case @Bit:  # 𝔹
  case @Bt0:  # #0
  case @Bt1:  # #1
  case @BitM: # λ{ #0: f ; #1: t }
    f: Term
    t: Term

  # Nat
  case @Nat: # ℕ
  case @Zer: # 0
  case @Suc: # ↑n
    n: Term
  case @NatM: # λ{ 0: z ; ↑: s }
    z: Term
    s: Term

  # List
  case @Lst: # T[]
    t: Term
  case @Nil: # []
  case @Con: # h<>t
    h: Term
    t: Term
  case @LstM: # λ{ []: n ; <>: c }
    n: Term
    c: Term

  # Pair
  case @Sig: # ΣA.B
    a: Term
    b: Term
  case @Tup: # (a,b)
    a: Term
    b: Term
  case @SigM: # λ{ (,): f }
    f: Term

  # Equality
  case @Eql: # T{a == b}
    t: Term
    a: Term
    b: Term
  case @Rwt: # ~e : P ; f
    e: Term
    P: Term
    f: Term

# Errors
# ------

type Error:
  case @CantInfer:
    ctx : Term[]
  case @Mismatch:
    ctx : Term[]
    typ : Term
    gol : Term

# Arguments
# ---------

def Arg(n: Nat) -> Set:
  match n:
    case 0n:
      Term
    case 1n + p:
      Term -> Arg(p)

type LHS:
  case @LHS:
    skp: Nat
    arg: Arg<1n+skp>
    ars: Term[]

# Stringification
# ---------------

def name(n: Nat) -> String:
  ...

def show(d: Nat, term: Term) -> String:
  match term:
    case @Let{T, v, f}:
      return String/flat(["let ",name(d)," : ",show(d,T)," = ",show(d,v),"; ",show(1n+d,f(@Var{d}))])
    case @Var{i}:
      return name(i)
    case @Nam{k}:
      return k
    case @Sub{t}:
      return show(d,t)
    case @Low{l, h}:
      return String/flat([show(d,l),"-",show(d,h)])
    case @Ref{k, f, t}:
      return String/flat([k])
    case @Fix{f}:
      #return name(d)
      return String/flat(["μ",name(d),".",show(1n+d,f(@Var{d}))])
    case @Set:
      return "*"
    case @All{a, b}:
      return String/flat(["∀",show(d,a),".",show(d,b)])
    case @Lam{f}:
      return String/flat(["λ",name(d),".",show(1n+d,f(@Var{d}))])
    case @App{f, x}:
      return String/flat(["(",show(d,f)," ",show(d,x),")"])
    case @Emp:
      return "⊥"
    case @EmpM:
      return "λ{}"
    case @Uni:
      return "⊤"
    case @One:
      return "()"
    case @UniM{f}:
      return String/flat(["λ{():",show(d,f),"}"])
    case @Bit:
      return "𝔹"
    case @Bt0:
      return "#0"
    case @Bt1:
      return "#1"
    case @BitM{f, t}:
      return String/flat(["λ{#0:",show(d,f),";#1:",show(d,t),"}"])
    case @Nat:
      return "ℕ"
    case @Zer:
      return "0"
    case @Suc{n}:
      return String/flat(["↑",show(d,n)])
    case @NatM{z, s}:
      return String/flat(["λ{0:",show(d,z),";↑:",show(d,s),"}"])
    case @Lst{t}:
      return String/flat([show(d,t),"[]"])
    case @Nil:
      return "[]"
    case @Con{h, t}:
      return String/flat([show(d,h),"<>",show(d,t)])
    case @LstM{n, c}:
      return String/flat(["λ{[]:",show(d,n),";<>:",show(d,c),"}"])
    case @Sig{a, b}:
      return String/flat(["Σ",show(d,a),".",show(d,b)])
    case @Tup{a, b}:
      return String/flat(["(",show(d,a),",",show(d,b),")"])
    case @SigM{f}:
      return String/flat(["λ{(,):",show(d,f),"}"])
    case @Eql{t, a, b}:
      return String/flat([show(d,t),"{",show(d,a),"==",show(d,b),"}"])
    case @Rwt{e, P, f}:
      return String/flat(["~",show(d,e),":",show(d,P),";",show(d,f)])

def show_error(error: Error) -> String:
  match error:
    case @CantInfer{ctx}:
      String/flat(["CantInfer"])
    case @Mismatch{ctx, typ, gol}:
      String/flat(["TypeMismatch\n- goal: ", show(0n, normal(gol)), "\n- type: ", show(0n, normal(typ))])

def show_all(fns: Term[]) -> String:
  match fns:
    case []:
      ""
    case fn <> fns:
      # FIXME: bring back the formatting (lost on whnf_ref refactor)
      String/flat([show(0n, deref(fn)), " ", show_all(fns)])

# Evaluator
# ---------

def whnf(term: Term) -> Term:
  #log String/flat(["WHNF:", show(0n,term)])
  match term:
    case @Ref{k, f, t}:
      #whnf_ref(0n, k, f, λk.k, f)
      whnf_ref(k, f, @KL{0n, λk.k}, f)
    case @Let{T, v, f}:
      whnf_let(T, v, f)
    case @Fix{f}:
      whnf_fix(f)
    case @App{f, x}:
      whnf_app(f, x)
    case @Eql{t, a, b}:
      whnf_eql(t, a, b)
    case @Rwt{e, P, f}:
      whnf_rwt(e, P, f)
    case x:
      x

def whnf_let(T: Term, v: Term, f: Term -> Term) -> Term:
  whnf(f(v))

def whnf_fix(f: Term -> Term) -> Term:
  whnf(f(whnf(@Fix{f})))

def whnf_app(f: Term, x: Term) -> Term:
  match whnf(f):
    with x
    case @Lam{f}:
      whnf(f(whnf(x)))
    case @UniM{f}:
      whnf_uni(x, f)
    case @BitM{f, t}:
      whnf_bit(x, f, t)
    case @NatM{z, s}:
      whnf_nat(x, z, s)
    case @LstM{n, c}:
      whnf_lst(x, n, c)
    case @SigM{f}:
      whnf_sig(x, f)
    case f:
      @App{f, x}

def whnf_uni(x: Term, f: Term) -> Term:
  match whnf(x):
    with f
    case @One:
      whnf(f)
    case x:
      @App{@UniM{f}, x}

def whnf_bit(x: Term, f: Term, t: Term) -> Term:
  match whnf(x):
    with f
    with t
    case @Bt0:
      whnf(f)
    case @Bt1:
      whnf(t)
    case x:
      @App{@BitM{f, t}, x}

def whnf_nat(x: Term, z: Term, s: Term) -> Term:
  match whnf(x):
    with z
    with s
    case @Zer:
      whnf(z)
    case @Suc{n}:
      whnf(@App{s, whnf(n)})
    case x:
      @App{@NatM{z, s}, x}

def whnf_lst(x: Term, n: Term, c: Term) -> Term:
  match whnf(x):
    with n
    with c
    case @Nil:
      whnf(n)
    case @Con{h, t}:
      whnf(@App{@App{c, whnf(h)}, whnf(t)})
    case x:
      @App{@LstM{n, c}, x}

def whnf_sig(x: Term, f: Term) -> Term:
  match whnf(x):
    with f
    case @Tup{a, b}:
      whnf(@App{@App{f, whnf(a)}, whnf(b)})
    case x:
      @App{@SigM{f}, x}

def whnf_eql(T: Term, a: Term, b: Term) -> Term:
  match whnf(T):
    with a
    with b
    case @Uni:
      match a b:
        case @One @One:
          @Uni
        case a b:
          @Eql{@Bit, a, b}
    case @Bit:
      match whnf(a) whnf(b):
        case @Bt0 @Bt0:
          @Uni
        case @Bt1 @Bt1:
          @Uni
        case @Bt0 @Bt1:
          @Emp
        case @Bt1 @Bt0:
          @Emp
        case a b:
          @Eql{@Bit, a, b}
    case @Nat:
      match whnf(a) whnf(b):
        case @Zer @Zer:
          @Uni
        case @Zer @Suc{b}:
          @Emp
        case @Suc{a} @Zer:
          @Emp
        case @Suc{a} @Suc{b}:
          whnf(@Eql{@Nat, a, b})
        case a b:
          @Eql{@Nat, a, b}
    case @Lst{T}:
      match whnf(a) whnf(b):
        case @Nil @Nil:
          @Uni
        case @Nil @Con{bh,bt}:
          @Emp
        case @Con{ah,at} @Nil:
          @Emp
        case @Con{ah,at} @Con{bh,bt}:
          whnf(@Sig{@Eql{T, ah, bh}, @Lam{λ_. @Eql{@Lst{T}, at, bt}}})
        case a b:
          @Eql{@Lst{T}, a, b}
    case @Sig{X,Y}:
      match whnf(a) whnf(b):
        case @Tup{ax,ay} @Tup{bx,by}:
          whnf(@Sig{@Eql{X, ax, bx}, @Lam{λ_. @Eql{@App{Y, ax}, ay, by}}})
        case a b:
          @Eql{@Sig{X,Y}, a, b}
    case @All{X,Y}:
      @All{X, @Lam{λx. @Eql{@App{Y,x}, @App{a,x}, @App{b,x}}}}
    case T:
      @Eql{T, a, b}

def whnf_rwt(e: Term, P: Term, f: Term) -> Term:
  match whnf(e):
    with P
    with f
    case @Uni:
      whnf(f)
    case @Emp:
      *
    case e:
      @Rwt{e, P, f}

## Guarded Deref:
## Converts the Ref's body into a "guarded matcher" that eliminates received args
## until it either succeeds, or gets stuck against a var. This emulates Agda-like
## clauses, giving us recursive recursive Refs that don't unroll infinitely.
## FIXME: review. Only the Nat case was implemented, the rest are AI-generated.
#def whnf_ref(A: Nat, K: String, F: Term, xs: Term -> Arg<A>, body: Term) -> Term:
  #match A:
    #with K
    #with F
    #with xs
    #with body
    #case 0n:
      #match body:
        #with K
        #with F
        #with xs
        #case @EmpM:
          #@Lam{λx. @App{(xs @Nam{K}),x}}
        #case @UniM{f}:
          #@Lam{λx.
            #match x:
              #case @One:
                #whnf_ref(0n, K, F, λk.@App{(xs k),@One}, f)
              #case x:
                #@App{(xs @Nam{K}),x}}
        #case @BitM{f,t}:
          #@Lam{λx.
            #match x:
              #case @Bt0:
                #whnf_ref(0n, K, F, λk.@App{(xs k),@Bt0}, f)
              #case @Bt1:
                #whnf_ref(0n, K, F, λk.@App{(xs k),@Bt1}, t)
              #case x:
                #@App{(xs @Nam{K}),x}}
        #case @NatM{z,s}:
          #@Lam{λx.
            #match x:
              #case @Zer:
                #whnf_ref(0n, K, F, λk.@App{(xs k),@Zer}, z)
              #case @Suc{xp}:
                #@App{whnf_ref(1n, K, F, λxp.λk.@App{(xs k),@Suc{xp}}, s), xp}
              #case x:
                #@App{(xs @Nam{K}),x}}
        #case @LstM{n,c}:
          #@Lam{λx.
            #match x:
              #with xs
              #with F
              #case @Nil:
                #whnf_ref(0n, K, F, λk.@App{(xs k),@Nil}, n)
              #case @Con{h,t}:
                #@App{@App{whnf_ref(2n, K, F, λh.λt.λk.@App{(xs k),@Con{h,t}}, c), h}, t}
              #case x:
                #@App{(xs @Nam{K}),x}}
        #case @SigM{f}:
          #@Lam{λx.
            #match x:
              #case @Tup{a,b}:
                #@App{@App{whnf_ref(2n, K, F, λa.λb.λk.@App{(xs k),@Tup{a,b}}, f), a}, b}
              #case x:
                #@App{(xs @Nam{K}),x}}
        #case @Lam{f}:
          #@Lam{λx. whnf_ref(0n, K, F, λk.@App{(xs k),x}, f(@Emp))}
        #case body:
          #xs(F)
    #case 1n+A:
      #match body:
        #with K
        #with F
        #with xs
        #case @EmpM:
          #@Lam{λx. @App{whnf_ref(A, K, F, xs(x), @EmpM), x}}
        #case @UniM{f}:
          #@Lam{λx.
            #match x:
              #case @One:
                #whnf_ref(A, K, F, xs(@One), f)
              #case x:
                #whnf_ref(A, K, F, xs(x), @UniM{f})}
        #case @BitM{f,t}:
          #@Lam{λx.
            #match x:
              #case @Bt0:
                #whnf_ref(A, K, F, xs(@Bt0), f)
              #case @Bt1:
                #whnf_ref(A, K, F, xs(@Bt1), t)
              #case x:
                #whnf_ref(A, K, F, xs(x), @BitM{f,t})}
        #case @NatM{z,s}:
          #@Lam{λx.
            #match x:
              #case @Zer:
                #whnf_ref(A, K, F, xs(@Zer), z)
              #case @Suc{xp}:
                #@App{whnf_ref(1n+A, K, F, λk.(xs @Suc{k}), s), xp}
              #case x:
                #whnf_ref(A, K, F, xs(x), @NatM{z,s})}
        #case @LstM{n,c}:
          #@Lam{λx.
            #match x:
              #case @Nil:
                #whnf_ref(A, K, F, xs(@Nil), n)
              #case @Con{h,t}:
                #@App{@App{whnf_ref(2n+A, K, F, λh.λt.(xs @Con{h,t}), c), h}, t}
              #case x:
                #whnf_ref(A, K, F, xs(x), @LstM{n,c})}
        #case @SigM{f}:
          #@Lam{λx.
            #match x:
              #case @Tup{a,b}:
                #@App{@App{whnf_ref(2n+A, K, F, λa.λb.(xs @Tup{a,b}), f), a}, b}
              #case x:
                #whnf_ref(A, K, F, xs(x), @SigM{f})}
        #case @Lam{f}:
          #@Lam{λx. whnf_ref(A, K, F, xs(x), f(@Emp))}
        #case body:
          #@Lam{λx. whnf_ref(A, K, F, xs(x), body)}

# TODO: refactor the function above to use a modular KL structure

type KL:
  case @KL:
    K: Nat
    L: Term -> Arg<K>

def kl_ctr_new(L: Term -> Term, N: Nat, ctr: Arg<N>, k: Term) -> Arg<N>:
  match N:
    case 0n:
      log String/flat(["A0 - ctr is ", show(0n, ctr), " ; L(k) is ", show(0n, L(k))])
      @App{L(k), ctr}
    case 1n+Np:
      log "A1"
      λx. kl_ctr_new(L, Np, ctr(x), k)

def kl_ctr_ext(K: Nat, L: Term -> Arg<1n+K>, N: Nat, ctr: Arg<N>) -> Arg<1n+Nat/add(N,K)>:
  match N:
    case 0n:
      log "B0"
      L(ctr)
    case 1n+Np:
      log "B1"
      λx. kl_ctr_ext(K, L, Np, ctr(x))

def kl_ctr(kl: KL, N: Nat, ctr: Arg<N>) -> KL:
  @KL{K,L} = kl
  log String/flat(["kl_ctr N=", Nat/show(N), " K=", Nat/show(K)])
  match K:
    case 0n:
      log "X"
      @KL{N, kl_ctr_new(L, N, ctr)}
    case 1n+K:
      log "Y"
      @KL{Nat/add(N,K), kl_ctr_ext(K, L, N, ctr)}

### Guarded Deref:
### Converts the Ref's body into a "guarded matcher" that eliminates received args
### until it either succeeds, or gets stuck against a var. This emulates Agda-like
### clauses, giving us recursive recursive Refs that don't unroll infinitely.
#def whnf_ref(k: String, F: Term, kl: KL, body: Term) -> Term:
  #match body:
    #...
    #case @NatM{z,s}:
      #@Lam{λx.
        #match x:
          #case @Zer:
            #log "A"
            #whnf_ref(k, F, kl_ctr(kl, 0n, @Zer), z)
          #case @Suc{xp}:
            #log "B"
            #@App{whnf_ref(k, F, kl_ctr(kl, 1n, λp.@Suc{p}), s), xp}
          #case x:
            #log "C"
            #whnf_ref_undo(k, F, kl, @NatM{z,s}, x)}
    #...

# NOTE: the kl functions have been added. above we provide a draft of the
# updated whnf_ref. it is greatly simplified with this new format! sadly,
# our draft is incomplete. your goal is to complete it.
# GOAL: COMPLETE THE WHNF_REF DRAFT WITH *ALL* THE MISSING CASES.
# PRESERVE THE SAME OBSERVATIONAL BEHAVIOR AS THE ORIGINAL WHNF_REF.
# WRITE THE COMPLETE WHNF_REF FN BELOW:
# think carefully about the last cases. reason thoroughly to get them right.

# Guarded Deref:
# Converts the Ref's body into a "guarded matcher" that eliminates received args
# until it either succeeds, or gets stuck against a var. This emulates Agda-like
# clauses, giving us recursive recursive Refs that don't unroll infinitely.
def whnf_ref(k: String, F: Term, kl: KL, body: Term) -> Term:
  log String/flat(["whnf_ref ", show(0n,F), " - ", show(0n,body)])
  match body:
    case @EmpM:
      @KL{K,L} = kl
      match K:
        case 0n:
          L(@Nam{k})
        case 1n+K:
          @Lam{λx. whnf_ref(k, F, @KL{K, L(x)}, @EmpM)}
    case @UniM{f}:
      @Lam{λx.
        match x:
          case @One:
            whnf_ref(k, F, kl_ctr(kl, 0n, @One), f)
          case x:
            whnf_ref_undo(k, F, kl, @UniM{f}, x)}
    case @BitM{f,t}:
      @Lam{λx.
        match x:
          case @Bt0:
            whnf_ref(k, F, kl_ctr(kl, 0n, @Bt0), f)
          case @Bt1:
            whnf_ref(k, F, kl_ctr(kl, 0n, @Bt1), t)
          case x:
            whnf_ref_undo(k, F, kl, @BitM{f,t}, x)}
    case @NatM{z,s}:
      @Lam{λx.
        log String/flat(["... x is ", show(0n,x)])
        match x:
          case @Zer:
            log "... zer"
            whnf_ref(k, F, kl_ctr(kl, 0n, @Zer), z)
          case @Suc{xp}:
            log String/flat(["... suc ... xp is ", show(0n,xp)])
            @App{whnf_ref(k, F, kl_ctr(kl, 1n, λp.@Suc{p}), s), xp}
          case x:
            whnf_ref_undo(k, F, kl, @NatM{z,s}, x)}
    case @LstM{n,c}:
      @Lam{λx.
        match x:
          case @Nil:
            whnf_ref(k, F, kl_ctr(kl, 0n, @Nil), n)
          case @Con{h,t}:
            @App{@App{whnf_ref(k, F, kl_ctr(kl, 2n, λh.λt.@Con{h,t}), c), h}, t}
          case x:
            whnf_ref_undo(k, F, kl, @LstM{n,c}, x)}
    case @SigM{f}:
      @Lam{λx.
        match x:
          case @Tup{a,b}:
            @App{@App{whnf_ref(k, F, kl_ctr(kl, 2n, λa.λb.@Tup{a,b}), f), a}, b}
          case x:
            whnf_ref_undo(k, F, kl, @SigM{f}, x)}
    case @Lam{f}:
      @Lam{λx. whnf_ref(k, F, kl_ctr(kl, 0n, x), f(@Emp))}
    case body:
      @KL{K,L} = kl
      match K:
        case 0n:
          L(F)
        case 1n+K:
          @Lam{λx. whnf_ref(k, F, @KL{K, L(x)}, body)}

# When an Ref call gets stuck (in a var), keep its original form.
def whnf_ref_undo(k: String, f: Term, kl: KL, body: Term, x: Term) -> Term:
  @KL{K,L} = kl
  match K:
    case 0n:
      @App{L(@Nam{k}), x}
    case 1n+K:
      whnf_ref(k, f, @KL{K, L(x)}, body)

# Normalizer
# ----------

def normal(term: Term) -> Term:
  match whnf(term):
    case @Var{i}:
      @Var{i}
    case @Nam{k}:
      @Nam{k}
    case @Sub{t}:
      t
    case @Low{l,h}:
      @Low{normal(l),normal(h)}
    case @Ref{k,f,t}:
      @Ref{k,normal(f),normal(t)}
    case @Let{T,v,f}:
      @Let{normal(T),normal(v),λx.normal(f(@Sub{x}))}
    case @Fix{f}:
      #@Fix{f}
      @Fix{λx.normal(f(@Sub{x}))}
    case @Set:
      @Set
    case @All{a,b}:
      @All{normal(a),normal(b)}
    case @Lam{f}:
      #@Lam{f}
      @Lam{λx.normal(f(@Sub{x}))}
    case @App{f,x}:
      @App{normal_fun(f), normal(x)}
    case @Emp:
      @Emp
    case @EmpM:
      @EmpM
    case @Uni:
      @Uni
    case @One:
      @One
    case @UniM{f}:
      @UniM{normal(f)}
    case @Bit:
      @Bit
    case @Bt0:
      @Bt0
    case @Bt1:
      @Bt1
    case @BitM{f,t}:
      @BitM{normal(f),normal(t)}
    case @Nat:
      @Nat
    case @Zer:
      @Zer
    case @Suc{n}:
      @Suc{normal(n)}
    case @NatM{z,s}:
      @NatM{normal(z),normal(s)}
    case @Lst{t}:
      @Lst{normal(t)}
    case @Nil:
      @Nil
    case @Con{h,t}:
      @Con{normal(h),normal(t)}
    case @LstM{n,c}:
      @LstM{normal(n),normal(c)}
    case @Sig{a,b}:
      @Sig{normal(a),normal(b)}
    case @Tup{a,b}:
      @Tup{normal(a),normal(b)}
    case @SigM{f}:
      @SigM{normal(f)}
    case @Eql{t,a,b}:
      @Eql{normal(t),normal(a),normal(b)}
    case @Rwt{e,P,f}:
      @Rwt{normal(e),normal(P),normal(f)}
      
def normal_fun(f: Term) -> Term:
  match f:
    case @App{f,x}:
      @App{normal_fun(f), normal(x)}
    case f:
      f

# To (Low/High)
# -------------

...

# Equal
# -----

...

# API
# ---

...

def DEF(name: String, ty: Term, tm: Term -> Term) -> Term:
  @Fix{λF. @Ref{name, tm(F), ty}}

def GEN(name: String, ty: Term, ctx: Ctx) -> Term:
  synth(name, ty, ctx)

...

# Tests
# ------

def mul2 : Term =
  @Ref{"mul2",
    @NatM{@Zer,@Lam{λap.@Suc{@Suc{@App{mul2,ap}}}}},
    @All{@Nat,@Lam{λx.@Nat}}}

def main : String =
  show(0n, normal(@App{mul2,@Suc{@Zer}}))




#########################################

PROBLEM: when running the file above, I get:

```sh
whnf_ref λ{0:0;↑:λa.↑↑(mul2 a)} - λ{0:0;↑:λa.↑↑(mul2 a)}
... x is ↑0
... suc ... xp is 0
whnf_ref λ{0:0;↑:λa.↑↑(mul2 a)} - λa.↑↑(mul2 a)
whnf_ref λ{0:0;↑:λa.↑↑(mul2 a)} - ↑↑(mul2 ⊥)
kl_ctr N=↑0 K=0
X
kl_ctr N=0 K=↑0
Y
B0
A1
A0 - ctr is ↑λ{0:0;↑:λa.↑↑(mul2 a)} ; L(k) is 0
whnf_ref λ{0:0;↑:λa.↑↑(mul2 a)} - λ{0:0;↑:λa.↑↑(mul2 a)}
... x is a
"(0 ↑λ{0:0;↑:λa.↑↑(mul2 a)})"
```

which is wrong. the final output is `(0 ↑λ{0:0;↑:λa.↑↑(mul2 a)})` rather than
`↑↑0`. previously, with the old whnf_ref, this example worked fine. this
suggests there is some error on the new, simplified whnf_ref function, which
causes it to malfunction.

your goal is to study this file and then answer what is the *specific error*
that causes this test to output the expression above, rather than ↑↑0. point
the exact part of the code that is incorrect, and propose a simple fix that
will solve this issue, and make it output ↑↑0, as desired.