Skip to content

Instantly share code, notes, and snippets.

@VictorTaelin
Last active September 3, 2024 11:35
Show Gist options
  • Save VictorTaelin/5d6c019bcde429ce0e71ce2ce9be9b34 to your computer and use it in GitHub Desktop.
Save VictorTaelin/5d6c019bcde429ce0e71ce2ce9be9b34 to your computer and use it in GitHub Desktop.
(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