Forked from VictorTaelin/optimal_affine_enumerator_superposed.hvm1.c
Created
June 22, 2024 04:30
-
-
Save enricozb/abdc5428e8a30e92640a9f139cf9a597 to your computer and use it in GitHub Desktop.
OPTIMAL AFFINE ENUMERATOR SUPERPOSED
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment