-
Notifications
You must be signed in to change notification settings - Fork 404
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
11 changed files
with
244 additions
and
96 deletions.
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
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
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,82 +1,80 @@ | ||
|
||
#// data Arr = Empty | (Single x) | (Concat x0 x1) | ||
#Empty = λempty λsingle λconcat empty | ||
#Single = λx λempty λsingle λconcat (single x) | ||
#Concat = λx0 λx1 λempty λsingle λconcat (concat x0 x1) | ||
# data Arr = Empty | (Single x) | (Concat x0 x1) | ||
Empty = λempty λsingle λconcat empty | ||
Single = λx λempty λsingle λconcat (single x) | ||
Concat = λx0 λx1 λempty λsingle λconcat (concat x0 x1) | ||
|
||
#// data Map = Free | Busy | (Node x0 x1) | ||
#Free = λfree λbusy λnode free | ||
#Busy = λfree λbusy λnode busy | ||
#Node = λx0 λx1 λfree λbusy λnode (node x0 x1) | ||
# data Map = Free | Busy | (Node x0 x1) | ||
Free = λfree λbusy λnode free | ||
Busy = λfree λbusy λnode busy | ||
Node = λx0 λx1 λfree λbusy λnode (node x0 x1) | ||
|
||
#// gen : u32 -> Arr | ||
#gen = λn switch n { | ||
#0: λx (Single x) | ||
#_: λx | ||
#let x0 = (* x 2) | ||
#let x1 = (+ x0 1) | ||
#(Concat (gen n-1 x1) (gen n-1 x0)) | ||
#} | ||
# gen : u32 -> Arr | ||
gen = λn switch n { | ||
0: λx (Single x) | ||
_: λx | ||
let x0 = (* x 2) | ||
let x1 = (+ x0 1) | ||
(Concat (gen n-1 x1) (gen n-1 x0)) | ||
} | ||
|
||
#// sum : Arr -> u32 | ||
#sum = λa | ||
#let a_empty = 0 | ||
#let a_single = λx x | ||
#let a_concat = λx0 λx1 (+ (sum x0) (sum x1)) | ||
#(a a_empty a_single a_concat) | ||
# sum : Arr -> u32 | ||
sum = λa | ||
let a_empty = 0 | ||
let a_single = λx x | ||
let a_concat = λx0 λx1 (+ (sum x0) (sum x1)) | ||
(a a_empty a_single a_concat) | ||
|
||
#// sort : Arr -> Arr | ||
#sort = λt (to_arr (to_map t) 0) | ||
# sort : Arr -> Arr | ||
sort = λt (to_arr (to_map t) 0) | ||
|
||
#// to_arr : Map -> u32 -> Arr | ||
#to_arr = λa | ||
#let a_free = λk Empty | ||
#let a_busy = λk (Single k) | ||
#let a_node = λx0 λx1 λk | ||
#let x0 = (to_arr x0 (+ (* k 2) 0)) | ||
#let x1 = (to_arr x1 (+ (* k 2) 1)) | ||
#(Concat x0 x1) | ||
#(a a_free a_busy a_node) | ||
# to_arr : Map -> u32 -> Arr | ||
to_arr = λa | ||
let a_free = λk Empty | ||
let a_busy = λk (Single k) | ||
let a_node = λx0 λx1 λk | ||
let x0 = (to_arr x0 (+ (* k 2) 0)) | ||
let x1 = (to_arr x1 (+ (* k 2) 1)) | ||
(Concat x0 x1) | ||
(a a_free a_busy a_node) | ||
|
||
#// to_map : Arr -> Map | ||
#to_map = λa | ||
#let a_empty = Free | ||
#let a_single = λx (radix 24 x 1 Busy) | ||
#let a_concat = λx0 λx1 (merge (to_map x0) (to_map x1)) | ||
#(a a_empty a_single a_concat) | ||
# to_map : Arr -> Map | ||
to_map = λa | ||
let a_empty = Free | ||
let a_single = λx (radix 24 x 1 Busy) | ||
let a_concat = λx0 λx1 (merge (to_map x0) (to_map x1)) | ||
(a a_empty a_single a_concat) | ||
|
||
#// merge : Map -> Map -> Map | ||
#merge = λa | ||
#let a_free = λb | ||
#let b_free = Free | ||
#let b_busy = Busy | ||
#let b_node = λb0 λb1 (Node b0 b1) | ||
#(b b_free b_busy b_node) | ||
#let a_busy = λb | ||
#let b_free = Busy | ||
#let b_busy = Busy | ||
#let b_node = λb0 λb1 0 | ||
#(b b_free b_busy b_node) | ||
#let a_node = λa0 λa1 λb | ||
#let b_free = λa0 λa1 (Node a0 a1) | ||
#let b_busy = λa0 λa1 0 | ||
#let b_node = λb0 λb1 λa0 λa1 (Node (merge a0 b0) (merge a1 b1)) | ||
#(b b_free b_busy b_node a0 a1) | ||
#(a a_free a_busy a_node) | ||
# merge : Map -> Map -> Map | ||
merge = λa | ||
let a_free = λb | ||
let b_free = Free | ||
let b_busy = Busy | ||
let b_node = λb0 λb1 (Node b0 b1) | ||
(b b_free b_busy b_node) | ||
let a_busy = λb | ||
let b_free = Busy | ||
let b_busy = Busy | ||
let b_node = λb0 λb1 0 | ||
(b b_free b_busy b_node) | ||
let a_node = λa0 λa1 λb | ||
let b_free = λa0 λa1 (Node a0 a1) | ||
let b_busy = λa0 λa1 0 | ||
let b_node = λb0 λb1 λa0 λa1 (Node (merge a0 b0) (merge a1 b1)) | ||
(b b_free b_busy b_node a0 a1) | ||
(a a_free a_busy a_node) | ||
|
||
#// radix : u32 -> Map | ||
#radix = λi λn λk λr switch i { | ||
#0: r | ||
#_: (radix i-1 n (* k 2) (swap (& n k) r Free)) | ||
#} | ||
# radix : u32 -> Map | ||
radix = λi λn λk λr switch i { | ||
0: r | ||
_: (radix i-1 n (* k 2) (swap (& n k) r Free)) | ||
} | ||
|
||
#// swap : u32 -> Map -> Map -> Map | ||
#swap = λn switch n { | ||
#0: λx0 λx1 (Node x0 x1) | ||
#_: λx0 λx1 (Node x1 x0) | ||
#} | ||
# swap : u32 -> Map -> Map -> Map | ||
swap = λn switch n { | ||
0: λx0 λx1 (Node x0 x1) | ||
_: λx0 λx1 (Node x1 x0) | ||
} | ||
|
||
#// main : u32 | ||
#main = (sum (sort (gen 16 0))) | ||
|
||
main = 42 | ||
# main : u32 | ||
main = (sum (sort (gen 16 0))) |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1,93 @@ | ||
@main = 42 | ||
@Busy = (* (a (* a))) | ||
|
||
@Concat = (a (b (* (* ((a (b c)) c))))) | ||
|
||
@Empty = (a (* (* a))) | ||
|
||
@Free = (a (* (* a))) | ||
|
||
@Node = (a (b (* (* ((a (b c)) c))))) | ||
|
||
@Single = (a (* ((a b) (* b)))) | ||
|
||
@gen = (?((@gen__C0 @gen__C1) a) a) | ||
|
||
@gen__C0 = a | ||
& @Single ~ a | ||
|
||
@gen__C1 = ({a d} ($([*2] {e $([+1] b)}) g)) | ||
& @Concat ~ (c (f g)) | ||
&! @gen ~ (a (b c)) | ||
&! @gen ~ (d (e f)) | ||
|
||
@main = a | ||
& @sum ~ (@main__C1 a) | ||
|
||
@main__C0 = a | ||
& @gen ~ (16 (0 a)) | ||
|
||
@main__C1 = a | ||
& @sort ~ (@main__C0 a) | ||
|
||
@merge = ((@merge__C5 (@merge__C4 (@merge__C3 a))) a) | ||
|
||
@merge__C0 = (b (e (a (d g)))) | ||
& @Node ~ (c (f g)) | ||
&! @merge ~ (a (b c)) | ||
&! @merge ~ (d (e f)) | ||
|
||
@merge__C1 = a | ||
& @Node ~ a | ||
|
||
@merge__C2 = a | ||
& @Node ~ a | ||
|
||
@merge__C3 = (a (b ((@merge__C1 ((* (* 0)) (@merge__C0 (a (b c))))) c))) | ||
|
||
@merge__C4 = ((@Busy (@Busy ((* (* 0)) a))) a) | ||
|
||
@merge__C5 = ((@Free (@Busy (@merge__C2 a))) a) | ||
|
||
@radix = (?(((* (* (a a))) @radix__C0) b) b) | ||
|
||
@radix__C0 = (a ({b $([&] $(d e))} ({$([*2] c) d} (f h)))) | ||
& @radix ~ (a (b (c (g h)))) | ||
& @swap ~ (e (f (@Free g))) | ||
|
||
@sort = (a c) | ||
& @to_arr ~ (b (0 c)) | ||
& @to_map ~ (a b) | ||
|
||
@sum = ((0 ((a a) (@sum__C0 b))) b) | ||
|
||
@sum__C0 = (a (b d)) | ||
&! @sum ~ (a $([+] $(c d))) | ||
&! @sum ~ (b c) | ||
|
||
@swap = (?((@swap__C0 @swap__C1) a) a) | ||
|
||
@swap__C0 = a | ||
& @Node ~ a | ||
|
||
@swap__C1 = (* (b (a c))) | ||
& @Node ~ (a (b c)) | ||
|
||
@to_arr = (((* @Empty) (@to_arr__C1 (@to_arr__C0 a))) a) | ||
|
||
@to_arr__C0 = (a (d ({$([*2] $([+1] e)) $([*2] $([+0] b))} g))) | ||
& @Concat ~ (c (f g)) | ||
&! @to_arr ~ (a (b c)) | ||
&! @to_arr ~ (d (e f)) | ||
|
||
@to_arr__C1 = a | ||
& @Single ~ a | ||
|
||
@to_map = ((@Free (@to_map__C1 (@to_map__C0 a))) a) | ||
|
||
@to_map__C0 = (a (c e)) | ||
& @merge ~ (b (d e)) | ||
&! @to_map ~ (a b) | ||
&! @to_map ~ (c d) | ||
|
||
@to_map__C1 = (a b) | ||
& @radix ~ (24 (a (1 (@Busy b)))) |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
@Tup8/New = (a (b (c (d (e (f (g (h ((0 (a (b (c (d (e (f (g (h i))))))))) i))))))))) | ||
|
||
@app = (?(((* (a a)) @app__C0) b) b) | ||
|
||
@app__C0 = (a ({b (c d)} (c e))) | ||
& @app ~ (a (b (d e))) | ||
|
||
@main = b | ||
& @app ~ (1234 (@rot (a b))) | ||
& @Tup8/New ~ (1 (2 (3 (4 (5 (6 (7 (8 a)))))))) | ||
|
||
@rot = ((@rot__C1 a) a) | ||
|
||
@rot__C0 = (h (a (b (c (d (e (f (g i)))))))) | ||
& @Tup8/New ~ (a (b (c (d (e (f (g (h i)))))))) | ||
|
||
@rot__C1 = (?((@rot__C0 *) a) a) |
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
This file was deleted.
Oops, something went wrong.
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
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
Oops, something went wrong.