From a0ccd7eb26567e3d9b1abf6403eacb71a369b123 Mon Sep 17 00:00:00 2001 From: imaqtkatt Date: Thu, 11 Apr 2024 14:17:46 -0300 Subject: [PATCH] Add more examples --- examples/bitonic_sort.hvm | 47 +++++++ examples/bubble_sort.hvm | 28 ++++ examples/hello_world.hvm | 1 + examples/queue.hvm | 21 +++ examples/quick_sort.hvm | 33 +++++ examples/sat_solver.hvm | 121 ++++++++++++++++++ .../snapshots/examples__bitonic_sort.hvm.snap | 5 + .../snapshots/examples__bubble_sort.hvm.snap | 5 + .../snapshots/examples__hello_world.hvm.snap | 5 + tests/snapshots/examples__queue.hvm.snap | 5 + tests/snapshots/examples__quick_sort.hvm.snap | 5 + tests/snapshots/examples__sat_solver.hvm.snap | 5 + 12 files changed, 281 insertions(+) create mode 100644 examples/bitonic_sort.hvm create mode 100644 examples/bubble_sort.hvm create mode 100644 examples/hello_world.hvm create mode 100644 examples/queue.hvm create mode 100644 examples/quick_sort.hvm create mode 100644 examples/sat_solver.hvm create mode 100644 tests/snapshots/examples__bitonic_sort.hvm.snap create mode 100644 tests/snapshots/examples__bubble_sort.hvm.snap create mode 100644 tests/snapshots/examples__hello_world.hvm.snap create mode 100644 tests/snapshots/examples__queue.hvm.snap create mode 100644 tests/snapshots/examples__quick_sort.hvm.snap create mode 100644 tests/snapshots/examples__sat_solver.hvm.snap diff --git a/examples/bitonic_sort.hvm b/examples/bitonic_sort.hvm new file mode 100644 index 000000000..28b02f889 --- /dev/null +++ b/examples/bitonic_sort.hvm @@ -0,0 +1,47 @@ +data Tree = (Leaf val) | (Both lft rgt) + +(U60.swap 0 a b) = (Both a b) +(U60.swap n a b) = (Both b a) + +// Swaps distant values in parallel; corresponds to a Red Box +(Warp s (Leaf a) (Leaf b)) = (U60.swap (^ (> a b) s) (Leaf a) (Leaf b)) +(Warp s (Both a b) (Both c d)) = (Join (Warp s a c) (Warp s b d)) +(Warp s (Leaf a) (Both c d)) = (Both (Warp s (Leaf a) c) (Warp s (Leaf a) d)) +(Warp s (Both a b) (Leaf c)) = (Both (Warp s a (Leaf c)) (Warp s b (Leaf c))) + +// Rebuilds the warped tree in the original order +(Join (Leaf a) (Leaf b)) = (Both a b) +(Join (Leaf a) (Both c d)) = (Both a (Both c d)) +(Join (Both a b) (Leaf c)) = (Both (Both a b) c) +(Join (Both a b) (Both c d)) = (Both (Both a c) (Both b d)) + +// Recursively warps each sub-tree; corresponds to a Blue/Green Box +(Flow s (Leaf a)) = (Leaf a) +(Flow s (Both a b)) = (Down s (Warp s a b)) + +// Propagates Flow downwards +(Down s (Leaf a)) = (Leaf a) +(Down s (Both a b)) = (Both (Flow s a) (Flow s b)) + +// Bitonic Sort +(Sort s (Leaf a)) = (Leaf a) +(Sort s (Both a b)) = (Flow s (Both (Sort 0 a) (Sort 1 b))) + +// Generates a tree of depth `n` +(Gen 0 x) = (Leaf x) +(Gen n x) = let m = (- n 1); (Both (Gen m (* x 2)) (Gen m (+ (* x 2) 1))) + +// Reverses a tree +(Rev (Leaf x)) = (Leaf x) +(Rev (Both a b)) = (Both (Rev b) (Rev a)) + +// Sums a tree +(Sum (Leaf x)) = x +(Sum (Both a b)) = (+ (Sum a) (Sum b)) + +(Main) = + let n = 10 + (Sum (Sort 0 (Rev (Gen n 0)))) + +// Use an argument from cli +// (Main n) = (Sum (Sort 0 (Rev (Gen n 0)))) diff --git a/examples/bubble_sort.hvm b/examples/bubble_sort.hvm new file mode 100644 index 000000000..4d5bfd67b --- /dev/null +++ b/examples/bubble_sort.hvm @@ -0,0 +1,28 @@ +// Sorts a list + +// sort : List -> List +(Sort []) = [] +(Sort (List.cons x xs)) = (Insert x (Sort xs)) + +// Insert : U60 -> List -> List +(Insert v []) = (List.cons v []) +(Insert v (List.cons x xs)) = (SwapGT (> v x) v x xs) + +// SwapGT : U60 -> U60 -> U60 -> List -> List +(SwapGT 0 v x xs) = (List.cons v (List.cons x xs)) +(SwapGT _ v x xs) = (List.cons x (Insert v xs)) + +// Generates a random list +(Rnd 0 s) = [] +(Rnd n s) = (List.cons s (Rnd (- n 1) (% (+ (* s 1664525) 1013904223) 4294967296))) + +// Sums a list +(Sum []) = 0 +(Sum (List.cons x xs)) = (+ x (Sum xs)) + +(Main) = + let n = 10 + (Sum (Sort (Rnd (* 2 50) n))) + +// Use an argument from cli +// (Main n) = (Sum (Sort (Rnd (* 2 50) n))) diff --git a/examples/hello_world.hvm b/examples/hello_world.hvm new file mode 100644 index 000000000..1897e97ee --- /dev/null +++ b/examples/hello_world.hvm @@ -0,0 +1 @@ +(Main) = (HVM.print "Hello, World!" *) diff --git a/examples/queue.hvm b/examples/queue.hvm new file mode 100644 index 000000000..339e53886 --- /dev/null +++ b/examples/queue.hvm @@ -0,0 +1,21 @@ +// A cool trick involving HVM's scopeless lambdas is linear qs: + +// Qnew : Queue a +Qnew = λx x + +// Qadd : a -> Queue a -> Queue a +Qadd = λx λq λk (q λc (c x k)) + +// Qrem : Queue a -> Pair a (Queue a) +Qrem = λq (q $k λx λxs λp(p x λ$k xs)) + +// Output: [1, 2, 3] +main = + let q = Qnew + let q = (Qadd 1 q) + let q = (Qadd 2 q) + let q = (Qadd 3 q) + ((Qrem q) λv0 λq + ((Qrem q) λv1 λq + ((Qrem q) λv2 λq + [1, 2, 3]))) diff --git a/examples/quick_sort.hvm b/examples/quick_sort.hvm new file mode 100644 index 000000000..bad549590 --- /dev/null +++ b/examples/quick_sort.hvm @@ -0,0 +1,33 @@ +data Tree = Leaf | (Node l m r) + +// Parallel QuickSort +(Sort List.nil) = Leaf +(Sort (List.cons x xs)) = + ((Part x xs) λmin λmax + let lft = (Sort min) + let rgt = (Sort max) + (Node lft x rgt)) + + // Partitions a list in two halves, less-than-p and greater-than-p + (Part p List.nil) = λt (t List.nil List.nil) + (Part p (List.cons x xs)) = (Push (> x p) x (Part p xs)) + + // Pushes a value to the first or second list of a pair + (Push 0 x pair) = (pair λmin λmax λp (p (List.cons x min) max)) + (Push _ x pair) = (pair λmin λmax λp (p min (List.cons x max))) + +// Generates a random list +(Rnd 0 s) = (List.nil) +(Rnd n s) = (List.cons s (Rnd (- n 1) (% (+ (* s 1664525) 1013904223) 4294967296))) + +// Sums all elements in a concatenation tree +(Sum Leaf) = 0 +(Sum (Node l m r)) = (+ m (+ (Sum l) (Sum r))) + +// Sorts and sums n random numbers +(Main) = + let n = 12 + (Sum (Sort (Rnd (<< 1 n) 1))) + +// Use an argument from cli +// (Main n) = (Sum (Sort (Rnd (<< 1 n) 1))) diff --git a/examples/sat_solver.hvm b/examples/sat_solver.hvm new file mode 100644 index 000000000..ccfd51aa5 --- /dev/null +++ b/examples/sat_solver.hvm @@ -0,0 +1,121 @@ +// Bool/List constructors and functions +(Cons h t) = λcλn(c h (t c n)) +Nil = λcλn(n) +T = λt λf t +F = λt λf f +(Id a) = a +(Not a) = λt λf (a f t) +(And a b) = (a λx(x) λx(F) b) +(Or a b) = (a λx(T) λx(x) b) +(Or3 a b c) = (Or a (Or b c)) + +// Pretty prints a bool +(Bool x) = (x 1 0) + +// Converts a solution to a pretty-printed church-list singleton +(Log x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 xA xB xC xD xE xF x) = (x (Cons λt(t + (Bool x0) (Bool x1) (Bool x2) (Bool x3) + (Bool x4) (Bool x5) (Bool x6) (Bool x7) + (Bool x8) (Bool x9) (Bool xA) (Bool xB) + (Bool xC) (Bool xD) (Bool xE) (Bool xF) +) Nil) Nil) + +// A random 3-SAT instance with 16 variables +(Foo x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 xA xB xC xD xE xF) = + (Log x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 xA xB xC xD xE xF + (And (Or3 xC x8 (Not xB)) + (And (Or3 (Not xA) (Not x2) (Not x8)) + (And (Or3 xB (Not x9) x4) + (And (Or3 xA x1 (Not x8)) + (And (Or3 (Not x9) x0 x5) + (And (Or3 (Not x4) (Not x4) xD) + (And (Or3 (Not x1) (Not x4) xB) + (And (Or3 (Not x2) xE (Not xD)) + (And (Or3 xD (Not x8) (Not x7)) + (And (Or3 xD (Not x1) x7) + (And (Or3 (Not x8) x4 x8) + (And (Or3 x5 (Not x0) xC) + (And (Or3 x1 x0 (Not x3)) + (And (Or3 x3 xE (Not xD)) + (And (Or3 x9 (Not xC) (Not xB)) + (And (Or3 x8 (Not xE) (Not x5)) + (And (Or3 (Not x7) (Not x9) (Not xF)) + (And (Or3 xF xB x2) + (And (Or3 (Not x2) (Not xE) (Not x7)) + (And (Or3 (Not xE) x3 (Not x3)) + (And (Or3 x3 (Not xF) x1) + (And (Or3 (Not x0) x0 xD) + (And (Or3 (Not x8) (Not x3) xC) + (And (Or3 xC (Not x1) x7) + (And (Or3 x2 (Not xE) (Not x0)) + (And (Or3 x6 (Not x5) x1) + (And (Or3 (Not xC) x3 (Not x3)) + (And (Or3 (Not x1) (Not xC) (Not x5)) + (And (Or3 xB xA x6) + (And (Or3 xF x6 x9) + (And (Or3 (Not xF) x3 (Not x9)) + (And (Or3 (Not xB) x1 x8) + (And (Or3 x9 (Not xE) xE) + (And (Or3 (Not xA) (Not x2) x2) + (And (Or3 x5 xE (Not x2)) + (And (Or3 (Not xB) xC x2) + (And (Or3 x1 xB (Not x2)) + (And (Or3 x8 (Not x6) (Not x7)) + (And (Or3 xD x9 (Not xA)) + (And (Or3 x0 x8 (Not x8)) + (And (Or3 (Not xA) x9 (Not x0)) + (And (Or3 (Not xE) (Not x7) (Not xC)) + (And (Or3 x9 xC (Not xA)) + (And (Or3 (Not x7) (Not xF) xD) + (And (Or3 x0 (Not x2) xD) + (And (Or3 xC (Not x9) (Not x0)) + (And (Or3 (Not xA) x8 (Not x1)) + (And (Or3 x4 x5 (Not xE)) + (And (Or3 (Not x0) x5 (Not x7)) + (And (Or3 (Not x1) (Not xC) xA) + (And (Or3 x0 xF x9) + (And (Or3 (Not xA) x3 (Not x2)) + (And (Or3 (Not x7) (Not xF) x6) + (And (Or3 (Not x1) x4 (Not x5)) + (And (Or3 xC (Not x8) x2) + (And (Or3 x4 x7 (Not x5)) + (And (Or3 (Not x9) (Not x0) (Not xA)) + (And (Or3 xC x1 (Not x2)) + (And (Or3 xB xE (Not xB)) + (And (Or3 xF x5 xA) + (And (Or3 (Not x6) xE x3) + (And (Or3 (Not xB) xB x1) + (And (Or3 (Not xF) x0 x7) + (Or3 xE (Not x3) (Not x2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +// Collapsers (to retrieve solutions from superpositions) - credit to @Franchu +Join = λaλbλcλn(a c (b c n)) +Col0 = λx let #A0{x0 x1} = x; (Join x0 x1) +Col1 = λx let #A1{x0 x1} = x; (Join x0 x1) +Col2 = λx let #A2{x0 x1} = x; (Join x0 x1) +Col3 = λx let #A3{x0 x1} = x; (Join x0 x1) +Col4 = λx let #A4{x0 x1} = x; (Join x0 x1) +Col5 = λx let #A5{x0 x1} = x; (Join x0 x1) +Col6 = λx let #A6{x0 x1} = x; (Join x0 x1) +Col7 = λx let #A7{x0 x1} = x; (Join x0 x1) +Col8 = λx let #A8{x0 x1} = x; (Join x0 x1) +Col9 = λx let #A9{x0 x1} = x; (Join x0 x1) +ColA = λx let #AA{x0 x1} = x; (Join x0 x1) +ColB = λx let #AB{x0 x1} = x; (Join x0 x1) +ColC = λx let #AC{x0 x1} = x; (Join x0 x1) +ColD = λx let #AD{x0 x1} = x; (Join x0 x1) +ColE = λx let #AE{x0 x1} = x; (Join x0 x1) +ColF = λx let #AF{x0 x1} = x; (Join x0 x1) + +// Finds a solution by applying Foo to superposed inputs +Main = + (Col0 (Col1 (Col2 (Col3 + (Col4 (Col5 (Col6 (Col7 + (Col8 (Col9 (ColA (ColB + (ColC (ColD (ColE (ColF + (Foo + #A0{T F} #A1{T F} #A2{T F} #A3{T F} + #A4{T F} #A5{T F} #A6{T F} #A7{T F} + #A8{T F} #A9{T F} #AA{T F} #AB{T F} + #AC{T F} #AD{T F} #AE{T F} #AF{T F} + ))))))))))))))))) diff --git a/tests/snapshots/examples__bitonic_sort.hvm.snap b/tests/snapshots/examples__bitonic_sort.hvm.snap new file mode 100644 index 000000000..c2ba41486 --- /dev/null +++ b/tests/snapshots/examples__bitonic_sort.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: examples/bitonic_sort.hvm +--- +523776 diff --git a/tests/snapshots/examples__bubble_sort.hvm.snap b/tests/snapshots/examples__bubble_sort.hvm.snap new file mode 100644 index 000000000..c30d64465 --- /dev/null +++ b/tests/snapshots/examples__bubble_sort.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: examples/bubble_sort.hvm +--- +188329834594 diff --git a/tests/snapshots/examples__hello_world.hvm.snap b/tests/snapshots/examples__hello_world.hvm.snap new file mode 100644 index 000000000..0c9ca9b3c --- /dev/null +++ b/tests/snapshots/examples__hello_world.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: examples/hello_world.hvm +--- +* diff --git a/tests/snapshots/examples__queue.hvm.snap b/tests/snapshots/examples__queue.hvm.snap new file mode 100644 index 000000000..815d8399d --- /dev/null +++ b/tests/snapshots/examples__queue.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: examples/queue.hvm +--- +[1, 2, 3] diff --git a/tests/snapshots/examples__quick_sort.hvm.snap b/tests/snapshots/examples__quick_sort.hvm.snap new file mode 100644 index 000000000..a65754188 --- /dev/null +++ b/tests/snapshots/examples__quick_sort.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: examples/quick_sort.hvm +--- +8752462477312 diff --git a/tests/snapshots/examples__sat_solver.hvm.snap b/tests/snapshots/examples__sat_solver.hvm.snap new file mode 100644 index 000000000..0e2cdbd2a --- /dev/null +++ b/tests/snapshots/examples__sat_solver.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: examples/sat_solver.hvm +--- +λa λb (a λc (c 1 0 0 1 1 1 1 0 0 1 0 0 1 1 0 1) (a λd (d 1 0 0 1 1 1 1 0 0 0 0 0 1 1 0 1) (a λe (e 1 0 0 1 1 1 1 0 0 0 0 0 0 1 0 1) (a λf (f 1 0 0 1 1 0 1 0 0 1 0 0 1 1 0 1) (a λg (g 1 0 0 1 1 0 1 0 0 0 0 0 1 1 0 1) (a λh (h 1 0 0 1 0 0 1 0 0 0 0 0 1 1 0 1) (a λi (i 1 0 0 1 0 0 1 0 0 0 0 0 1 0 0 1) (a λj (j 0 1 0 1 0 0 1 1 1 0 1 0 1 1 0 1) (a λk (k 0 0 0 0 1 1 1 0 1 1 1 1 1 1 1 0) b)))))))))