enumerating binary trees with 1 label

enum_bin_tree.hvm

// Enumerating Binary Trees with 1 label
// -------------------------------------

data Tree { #L #N{a b} }

// Recursive: requires label forking

@sp0(x) = (+ 0 (* x 2))
@sp1(x) = (+ 1 (* x 2))

@enum(&L) =
  &L{
    #L
    #N{@enum(@sp0(L)) @enum(@sp1(L))}
  }

@main = @enum(1)

// Builder: one label suffices

@enum(N T) =
  ~ N !T {
    0: 
      T
    1+N:
      ! &1{N0 N1} = N
      ! &1{T0 T1} = T
      &1{
        @enum(N0 (T0 #L))
        @enum((+ 2 N1) λx.λy.(T1 #N{x y}))
      }
  }

@main = @enum(1 λk.k)