Merge pull request #266 from HigherOrderCO/add-examples

Add examples

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))))

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)))

examples/hello_world.hvm

@@ -0,0 +1 @@
+(Main) = (HVM.print "Hello, World!" *)

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])))

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)))

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}
+  )))))))))))))))))

tests/snapshots/examples__bitonic_sort.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/bitonic_sort.hvm
+---
+523776

tests/snapshots/examples__bubble_sort.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/bubble_sort.hvm
+---
+188329834594

tests/snapshots/examples__hello_world.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/hello_world.hvm
+---
+*

tests/snapshots/examples__queue.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/queue.hvm
+---
+[1, 2, 3]

tests/snapshots/examples__quick_sort.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/quick_sort.hvm
+---
+8752462477312

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)))))))))