lambda encoded version

pseudo_metavar_factors.hvml

// Repeated Application
@rep(n f x) = ~ n {
  0: x
  p: !&0{f0 f1}=f (f0 @rep(p f1 x))
}

// Squared Application (with Bin)
@sqr(n f x) = ((n
  λnp λf λx !&0{f0 f1}=f @sqr(np λk(f0 (f1 k)) x)
  λnp λf λx !&0{fX f0}=f !&0{f1 f2}=fX @sqr(np λk(f0 (f1 k)) (f2 x))
  λf λx x) f x)

// If-Then-Else
@if(b t f) = ~b {
  0: f
  k: t
}

@O(p) = λo λi λe (o p)
@I(p) = λo λi λe (i p)
@E    = λo λi λe e

// Converts a Bin to an U32
@u32(b) = (b
  λp (+ (* 2 @u32(p)) 0)
  λp (+ (* 2 @u32(p)) 1)
  0)

// Converts an U32 to a Bin of given size
@bin(s n) = ~s{
  0: @E
  p: !&0{n0 n1}=n ~(% n0 2) {
    0: @O(@bin(p (/ n1 2)))
    k: @I(@bin(p (/ n1 2)))
  }
}

// Bin Equality
@eq(a b) = ((a
  λap λb (b
    λbp @eq(ap bp)
    λbp 0
    0)
  λap λb (b
    λbp 0
    λbp @eq(ap bp)
    0)
  λb (b 
    λbp 0
    λbp 0
    1)) b)

// Increments a Bin
@inc(a) = λo λi λe (a λp (i p) λp (o @inc(p)) e)

// Adds two Bins
@add(a b) = ((a
  λap λb λo λi λe ((b 
    λbp λap (o @add(ap bp))
    λbp λap (i @add(ap bp))
    λap e) ap)
  λap λb λo λi λe ((b
    λbp λap (i @add(ap bp))
    λbp λap (o @inc(@add(ap bp)))
    e) ap)
  λb @E) b)

// Adds by repeated incs
@addI(a b) = @sqr(a λx@inc(x) b)

// Muls two Bins
@mul(a b) = ((b
  λbp λa @O(@mul(a bp))
  λbp λa !&1{a0 a1}=a @add(a0 @O(@mul(a1 bp)))
  λa @E) a)

// Muls by repeated adds
@mulI(a b) =
  !&1{a0 a1}=a
  @sqr(a0 λx(@add(a1 x)) b)

// Bin Concatenation
@cat(a b) = (a
  λap(@O(@cat(ap b)))
  λap(@I(@cat(ap b)))
  b)

// Enums all Bins of given size (label 1)
@all1(s) = ~s{
  0: @E
  p: !&3{p0 p1}=p &3{
    @O(@all1(p0))
    @I(@all1(p1))
  }
}

// Enums all Bins of given size (label 2)
@all2(s) = ~s{
  0: @E
  p: !&4{p0 p1}=p &4{
    @O(@all2(p0))
    @I(@all2(p1))
  }
}

// 20:
//@K = 9
//@H = 10
//@S = 20
//@X = @cat(@all1(@H) @bin(@H 0))
//@Y = @cat(@all2(@H) @bin(@H 0))
//@P = @I(@I(@I(@I(@O(@I(@I(@O(@I(@I(@O(@O(@I(@O(@I(@O(@O(@O(@I(@I(@E))))))))))))))))))))

// 30:
@K = 14
@H = 15
@S = 30
@X = @cat(@all1(@H) @bin(@H 0))
@Y = @cat(@all2(@H) @bin(@H 0))
@P = @I(@I(@I(@O(@O(@O(@I(@I(@O(@I(@O(@I(@O(@O(@O(@O(@I(@O(@I(@I(@O(@O(@I(@O(@O(@I(@O(@I(@O(@I(@E))))))))))))))))))))))))))))))

@main = @if(@eq(@mul(@X @Y) @P) λt(t @u32(@X) @u32(@Y)) *)