Last active
September 3, 2024 11:35
-
-
Save VictorTaelin/5d6c019bcde429ce0e71ce2ce9be9b34 to your computer and use it in GitHub Desktop.
This file contains 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
(Switch 0 z s) = z | |
(Switch n z s) = (s (- n 1)) | |
// (λx(bod) arg) | |
// ------------- APP-LAM | |
// x <- arg | |
// bod | |
(APP (Lam bod) arg) = | |
(bod arg) | |
// (#i{g,h} arg) | |
// ----------------- APP-SUP | |
// dup #i{a,b} = arg | |
// #i{(g a) (h b)} | |
(APP (Sup i g h) arg) = | |
(DUP i arg λaλb | |
(Sup i (APP g a) (APP h b))) | |
// ((dup #i{x,y} = val; bod) arg) | |
// ------------------------------ APP-DUP | |
// (dup #i{x,y} = val; (bod arg)) | |
(APP (Dup i val bod) arg) = | |
(DUP i val λaλb(APP (bod a b) arg)) | |
// (fun arg) | |
// --------- APP | |
// (fun arg) | |
(APP fun arg) = | |
(App fun arg) | |
// dup #i{k0,k1} = λx(f); bod | |
// -------------------------- DUP-LAM | |
// dup #i{f0,f1} = f | |
// x <- #i{x0,x1} | |
// k0 <- λx0(f0) | |
// k1 <- λx1(f1) | |
// bod | |
(DUP i (Lam f) bod) = | |
(DUP i (f (Sup i $x0 $x1)) λf0λf1 | |
(bod (Lam λ$x0(f0)) (Lam λ$x1(f1)))) | |
// dup #i{k0,k1} = #j{fst,snd}; bod | |
// -------------------------------- DUP-SUP | |
// if #i == #j: | |
// k0 <- fst | |
// k1 <- snd | |
// bod | |
// else: | |
// k0 <- #j{a0,a1} | |
// k1 <- #j{b0,b1} | |
// dup #i{a0,a1} = fst | |
// dup #i{b0,b1} = snd | |
// cont | |
(DUP i (Sup j fst snd) bod) = | |
(Switch (== i j) | |
(DUP_SUP_NE i j fst snd bod) | |
(DUP_SUP_EQ i j fst snd bod)) | |
// dup #i{k0,k1} = (dup #j{r0,r1} = v; f); bod | |
// ------------------------------------------- DUP-DUP | |
// dup #j{r0,r1} = v | |
// dup #i{k0,k1} = f | |
// bod | |
(DUP i (Dup j v f) bod) = | |
(DUP j v λr0λr1 | |
(DUP i (f r0 r1) bod)) | |
// dup #i{k0,k1} = val; bod | |
// ---------------------- DUP | |
// dup #i{k0,k1} = val; bod | |
(DUP i val bod) = | |
(Dup i val bod) | |
(DUP_SUP_EQ i j fst snd bod) = | |
(bod fst snd) | |
(DUP_SUP_NE i j fst snd bod) = | |
(DUP i fst λa0λa1 | |
(DUP i snd λb0λb1 | |
(bod (Sup j a0 a1) | |
(Sup j b0 b1)))) | |
C2a = (Lam λf(Lam λx(DUP 0 f λf0λf1(APP f0 (APP f1 x))))) | |
C2b = (Lam λf(Lam λx(DUP 1 f λf0λf1(APP f0 (APP f1 x))))) | |
Not = (Lam λb(Lam λt(Lam λf(APP (APP b f) t)))) | |
(Quote (Lam bod) dep) = (Lam λx(Quote (bod (Var dep)) (+ dep 1))) | |
(Quote (App fun arg) dep) = (App (Quote fun dep) (Quote arg dep)) | |
(Quote (Sup lab fst snd) dep) = (Sup lab (Quote fst dep) (Quote snd dep)) | |
(Quote (Dup lab val bod) dep) = (Dup lab (Quote val dep) λx(Quote (bod x) (+ dep 1))) | |
(Quote (Var idx) dep) = (Var dep) | |
//Main = (Quote (Lam λx(x)) 0) | |
Main = (Quote (APP C2a C2b) 0) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment