OPTIMAL AFFINE ENUMERATOR SUPERPOSED

optimal_affine_enumerator_superposed.hvm1.c

// This file enumerates `Tree -> Tree` functions, where:
// data Tree = (C Tree Tree) | L

// It works by creating a superposed tree of all algorithms with a given
// pattern-match count. For example, for count=0, we create:
// λt (t
//   // case C:
//   λx λy
//     #0{
//       (C <var> <var>)
//       (L)
//     }
//   // case L:
//     #1{
//       (C <var> <var>)
//       (L)
//     }
// )
// Here, <var> will be filled with variables in context, in a affine, scopeless
// fashion. That means that, for any given full collapse of the tree, no var
// will occur twice. That's the main contribution of this file! To do this, we
// use a simple trick: when making a choice during the enumerator (say, among
// `C` and `L` constructor), we use a superposition with a given label N. Then,
// we use *that same label* to clone the affine context. This allows us to keep
// a "affine" context for each universe, allowing us to use each variable only
// once *per universe*, not per all universes. This was a complication I was
// having previously, so, I'm saving this file to record this insight!
// 
// This demo file has many limitations:
// - We only consider functions with a fixed pattern-match count
// - Constructors are always created once on every pattern-match
// - No recursion yet
// 
// But it has all the building blocks necessary to build an affine enumerator!

// Enumerates all `Tree -> Tree` functions with given pattern-match count
//(All 0   lvl ctx) = λret (ret (SEL ctx) 0 lvl Nil)
(All 0   lvl ctx) = (Sel 0   lvl ctx)
(All mat lvl ctx) = (Mat mat lvl ctx)
  
// Selects a variable from context (superposition of all options)
(Sel mat lvl Nil)          = λret (ret L  mat lvl Nil) // unreachable?
(Sel mat lvl (Ext tm Nil)) = λret (ret tm mat lvl Nil)
(Sel mat lvl (Ext tm ctx)) =
  let lab = lvl
  let lvl = (+ lvl 1)
  (HVM.DUP lab ctx λctxT λctxH
  (HVM.DUP lab tm  λtmT  λtmH
  (HVM.SUP lab 
    // select there
    ((Sel mat lvl ctxT) λtm λmat λlvl λctxT
    λret (ret tm mat lvl (Ext tmT ctxT)))
    // select here
    λret (ret tmH mat lvl ctxH)
  )))

// Pattern-matches a context variable (split on C/L cases)
(Mat 0   lvl ctx) = ERROR
(Mat mat lvl ctx) =
  let mat = (- mat 1)
  ((Sel mat lvl ctx)                   λval λmat λlvl λctx // selects a scrutinee to match
  ((Ctr mat lvl (Ext $y (Ext $x ctx))) λifC λmat λlvl λctx // constructs the C case
  ((Ctr mat lvl ctx)                   λifL λmat λlvl λctx
  λret (ret (val λ$xλ$y(ifC) ifL) mat lvl ctx))))
  
// Emits a constructor out (superposition of C/L ctrs)
(Ctr mat lvl ctx) =
  let lab = lvl
  let lvl = (+ lvl 1)
  (HVM.DUP lab ctx λctxL λctxC
  ((All mat lvl ctxC) λvx λmat λlvl λctxC
  ((All mat lvl ctxC) λvy λmat λlvl λctxC
  (HVM.SUP lab
    // emit L
    λret (ret L mat lvl ctxL)
    // emit C
    λret (ret (C vx vy) mat lvl ctxC)
  ))))

(Pick lv E      t) = t
(Pick lv (O xs) t) = (HVM.DUP lv t λt0 λt1 (Pick (+ lv 1) xs t0))
(Pick lv (I xs) t) = (HVM.DUP lv t λt0 λt1 (Pick (+ lv 1) xs t1))

Main = 
  let all = λx((All 1 0 (Ext x Nil)) λval λmat λlvl λctx (val))
  let sel = (Pick 0 (I (I (I (I E)))) all)
  all

// FLAT:
// λx0 #1{#0{#3{#2{(x0 λx1 λx2 (L) (L)) (x0 λx1 λx2 (L) (C x1 x2))} #2{(x0 λx1 λx2 (L) (L)) (x0 λx1 λx2 (L) (C x2 x1))}} #2{(x0 λx1 λx2 (C x1 x2) (L)) (x0 λx1 λx2 (C x1 x2) (C (L) (L)))}} #0{#3{#2{(x0 λx1 λx2 (L) (L)) (x0 λx1 λx2 (L) (C x1 x2))} #2{(x0 λx1 λx2 (L) (L)) (x0 λx1 λx2 (L) (C x2 x1))}} #2{(x0 λx1 λx2 (C x2 x1) (L)) (x0 λx1 λx2 (C x2 x1) (C (L) (L)))}}}
// TABS:
// λx0
// #1{
//   #0{
//     #3{
//       #2{
//         (x0 λx1 λx2 (L) (L))
//         (x0 λx1 λx2 (L) (C x1 x2))
//       }
//       #2{
//         (x0 λx1 λx2 (L) (L))
//         (x0 λx1 λx2 (L) (C x2 x1))
//       }
//     }
//     #2{
//       (x0 λx1 λx2 (C x1 x2) (L))
//       (x0 λx1 λx2 (C x1 x2) (C (L) (L)))
//     }
//   }
//   #0{
//     #3{
//       #2{
//         (x0 λx1 λx2 (L) (L))
//         (x0 λx1 λx2 (L) (C x1 x2))
//       }
//       #2{
//         (x0 λx1 λx2 (L) (L))
//         (x0 λx1 λx2 (L) (C x2 x1))
//       }
//     }
//     #2{
//       (x0 λx1 λx2 (C x2 x1) (L))
//       (x0 λx1 λx2 (C x2 x1) (C (L) (L)))
//     }
//   }
// }

// λx0 (x0 λ*  λ*  (L)       (L))         // OIOI
// λx0 (x0 λ*  λ*  (L)       (L))         // OIOO
// λx0 (x0 λ*  λ*  (L)       (L))         // OOOI
// λx0 (x0 λ*  λ*  (L)       (L))         // OOOO
// λx0 (x0 λx1 λx2 (C x1 x2) (C (L) (L))) // IOII
// λx0 (x0 λx1 λx2 (C x1 x2) (C (L) (L))) // IOIO
// λx0 (x0 λx1 λx2 (C x1 x2) (L))         // IOOI
// λx0 (x0 λx1 λx2 (C x1 x2) (L))         // IOOO
// λx0 (x0 λx1 λx2 (C x2 x1) (C (L) (L))) // IIII
// λx0 (x0 λx1 λx2 (C x2 x1) (C (L) (L))) // IIIO
// λx0 (x0 λx1 λx2 (C x2 x1) (L))         // IIOI
// λx0 (x0 λx1 λx2 (C x2 x1) (L))         // IIOO
// λx0 (x0 λx1 λx2 (L)       (C x1  x2))  // OIIO
// λx0 (x0 λx1 λx2 (L)       (C x1  x2))  // OOIO
// λx0 (x0 λx1 λx2 (L)       (C x2  x1))  // OIII
// λx0 (x0 λx1 λx2 (L)       (C x2  x1))  // OOII