Update examples

This commit is contained in:
imaqtkatt 2024-05-10 16:59:13 -03:00
parent 6948e1b3fb
commit 912e1ae01a
9 changed files with 122 additions and 122 deletions

View File

@ -1,10 +1,10 @@
enum Bool:
Bool/true()
Bool/false()
true()
false()
enum Tree:
Tree/node(~lft, ~rgt)
Tree/leaf(val)
node(~lft, ~rgt)
leaf(val)
def and(a, b):
match a:

View File

@ -1,44 +1,44 @@
#flavor core
data Tree = (Leaf val) | (Both lft rgt)
(U60.swap 0 a b) = (Both a b)
(U60.swap n a b) = (Both b a)
(U60.swap 0 a b) = (Tree/Both a b)
(U60.swap n a b) = (Tree/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)))
(Warp s (Tree/Leaf a) (Tree/Leaf b)) = (U60.swap (^ (> a b) s) (Tree/Leaf a) (Tree/Leaf b))
(Warp s (Tree/Both a b) (Tree/Both c d)) = (Join (Warp s a c) (Warp s b d))
(Warp s (Tree/Leaf a) (Tree/Both c d)) = (Tree/Both (Warp s (Tree/Leaf a) c) (Warp s (Tree/Leaf a) d))
(Warp s (Tree/Both a b) (Tree/Leaf c)) = (Tree/Both (Warp s a (Tree/Leaf c)) (Warp s b (Tree/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))
(Join (Tree/Leaf a) (Tree/Leaf b)) = (Tree/Both a b)
(Join (Tree/Leaf a) (Tree/Both c d)) = (Tree/Both a (Tree/Both c d))
(Join (Tree/Both a b) (Tree/Leaf c)) = (Tree/Both (Tree/Both a b) c)
(Join (Tree/Both a b) (Tree/Both c d)) = (Tree/Both (Tree/Both a c) (Tree/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))
(Flow s (Tree/Leaf a)) = (Tree/Leaf a)
(Flow s (Tree/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))
(Down s (Tree/Leaf a)) = (Tree/Leaf a)
(Down s (Tree/Both a b)) = (Tree/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)))
(Sort s (Tree/Leaf a)) = (Tree/Leaf a)
(Sort s (Tree/Both a b)) = (Flow s (Tree/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)))
(Gen 0 x) = (Tree/Leaf x)
(Gen n x) = let m = (- n 1); (Tree/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))
(Rev (Tree/Leaf x)) = (Tree/Leaf x)
(Rev (Tree/Both a b)) = (Tree/Both (Rev b) (Rev a))
// Sums a tree
(Sum (Leaf x)) = x
(Sum (Both a b)) = (+ (Sum a) (Sum b))
(Sum (Tree/Leaf x)) = x
(Sum (Tree/Both a b)) = (+ (Sum a) (Sum b))
(Main) =
let n = 10

View File

@ -3,27 +3,27 @@
// sort : List -> List
(Sort []) = []
(Sort (List.cons x xs)) = (Insert x (Sort xs))
(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)
(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))
(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) = List.nil
(Rnd 0 s) = List/nil
(Rnd n s) =
let s = (^ s (* s 0b10000000000000))
let s = (^ s (/ s 0b100000000000000000))
let s = (^ s (* s 0b100000))
(List.cons s (Rnd (- n 1) s))
(List/cons s (Rnd (- n 1) s))
// Sums a list
(Sum []) = 0
(Sum (List.cons x xs)) = (+ x (Sum xs))
(Sum (List/cons x xs)) = (+ x (Sum xs))
(Main) =
let n = 10

View File

@ -13,4 +13,4 @@ CC.lang = λprogram
main = (CC.lang λcallcc
// This code calls `callcc`, then calls `k` to fill the hole with `42`. This means that the call to callcc returns `42`, and the program returns `52`
(+ 10 (callcc λk(+ (k 42) 1729)))
)
)

View File

@ -18,10 +18,10 @@
// Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
// You can use 'switch' to pattern match native numbers
// The `_` arm binds the `scrutinee`-1 variable to the the value of the number -1
(Num.pred) = λn
switch n {
// You can use numbers on the native match expression
// The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1
(Num.pred) = λn
switch n {
0: 0
_: n-1
}
@ -32,30 +32,29 @@ data Bool = True | False
// You can have pattern matching on definitions
// Use `*` to ignore a pattern
(Option.unwrap_or (Some val) *) = val
(Option.unwrap_or None or) = or
(Option.unwrap_or (Option/Some val) *) = val
(Option.unwrap_or Option/None or) = or
(Bool.or True *) = True
(Bool.or * True) = True
(Bool.or * *) = False
(Bool.or Bool/True *) = Bool/True
(Bool.or * Bool/True) = Bool/True
(Bool.or * *) = Bool/False
// Or using a match expression
(Bool.not) = λbool
match bool {
True: False
False: True
Bool/True: Bool/False
Bool/False: Bool/True
}
// Data types can store values
data Boxed = (Box val)
// Types with only one constructor can be destructured using `let` or a single matching definition
(Box.map (Box val) f) = (Box (f val))
(Box.map (Boxed/Box val) f) = (Boxed/Box (f val))
(Box.unbox) = λbox
match box {
Box: box.val
}
(Box.unbox) = λbox match box {
Boxed/Box: box.val
}
// Use tuples to store two values together without needing to create a new data type
(Tuple.new fst snd) =
@ -70,16 +69,16 @@ data Boxed = (Box val)
snd
// All files must have a main definition to be run.
// You can execute a program in HVM with "cargo run -- --run <path to file>"
// Other options are "--check" (the default mode) to just see if the file is well formed
// and "--compile" to output hvm-core code.
(main) =
let tup = (Tuple.new None (Num.pred 5))
// You can execute a program in HVM with "cargo run -- run <path to file>"
// Other options are "check" (the default mode) to just see if the file is well formed
// and "compile" to output hvm-core code.
(main) =
let tup = (Tuple.new Option/None (Num.pred 5))
let fst = (Tuple.fst tup)
let snd = (Tuple.snd tup)
let box = (Box fst)
let box = (Boxed/Box fst)
let map = (Box.map box Option.unwrap_or)
let unboxed = ((Box.unbox map) snd)

View File

@ -9,4 +9,4 @@ fusing_add = λa
let case_zero = λb b
(a case_succ case_zero)
Main = λx (fusing_add two x)
Main = λx (fusing_add two x)

View File

@ -10,4 +10,4 @@ to_church n = switch n {
}
main =
// Self-composes `not` 2^24 times and prints the result.
((to_church 0xFFFFFF) fusing_not) // try replacing this by not. Will it still work?
((to_church 0xFFFFFF) fusing_not) // try replacing this by not. Will it still work?

View File

@ -2,32 +2,32 @@
data Tree = Leaf | (Node l m r)
// Parallel QuickSort
(Sort List.nil) = Leaf
(Sort (List.cons x xs)) =
(Sort List/nil) = Tree/Leaf
(Sort (List/cons x xs)) =
((Part x xs) λmin λmax
let lft = (Sort min)
let rgt = (Sort max)
(Node lft x rgt))
(Tree/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))
(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)))
(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 0 s) = List/nil
(Rnd n s) =
let s = (^ s (* s 0b10000000000000))
let s = (^ s (/ s 0b100000000000000000))
let s = (^ s (* s 0b100000))
(List.cons s (Rnd (- n 1) s))
(List/cons s (Rnd (- n 1) s))
// Sums all elements in a concatenation tree
(Sum Leaf) = 0
(Sum (Node l m r)) = (+ m (+ (Sum l) (Sum r)))
(Sum Tree/Leaf) = 0
(Sum (Tree/Node l m r)) = (+ m (+ (Sum l) (Sum r)))
// Sorts and sums n random numbers
(Main) =

View File

@ -1,98 +1,99 @@
#flavor core
data Map = Free | Used | (Both a b)
data Map_ = Free | Used | (Both a b)
data Arr = Null | (Leaf x) | (Node a b)
(Swap s a b) = switch s {
0: (Both a b)
_: (Both b a)
0: (Map_/Both a b)
_: (Map_/Both b a)
}
// Sort : Arr -> Arr
(Sort t) = (ToArr 0 (ToMap t))
// ToMap : Arr -> Map
(ToMap Null) = Free
(ToMap (Leaf a)) = (Radix a)
(ToMap (Node a b)) = (Merge (ToMap a) (ToMap b))
(ToMap Arr/Null) = Map_/Free
(ToMap (Arr/Leaf a)) = (Radix a)
(ToMap (Arr/Node a b)) = (Merge (ToMap a) (ToMap b))
// ToArr : U60 -> Map -> Arr
(ToArr x Free) = Null
(ToArr x Used) = (Leaf x)
(ToArr x (Both a b)) =
(ToArr x Map_/Free) = Arr/Null
(ToArr x Map_/Used) = (Arr/Leaf x)
(ToArr x (Map_/Both a b)) =
let a = (ToArr (+ (* x 2) 0) a)
let b = (ToArr (+ (* x 2) 1) b)
(Node a b)
(Arr/Node a b)
// Merge : Map -> Map -> Map
(Merge Free Free) = Free
(Merge Free Used) = Used
(Merge Used Free) = Used
(Merge Used Used) = Used
(Merge Free (Both c d)) = (Both c d)
(Merge (Both a b) Free) = (Both a b)
(Merge (Both a b) (Both c d)) = (Both (Merge a c) (Merge b d))
(Merge (Both a b) Used) = *
(Merge Used (Both a b)) = *
(Merge Map_/Free Map_/Free) = Map_/Free
(Merge Map_/Free Map_/Used) = Map_/Used
(Merge Map_/Used Map_/Free) = Map_/Used
(Merge Map_/Used Map_/Used) = Map_/Used
(Merge Map_/Free (Map_/Both c d)) = (Map_/Both c d)
(Merge (Map_/Both a b) Map_/Free) = (Map_/Both a b)
(Merge (Map_/Both a b) (Map_/Both c d)) = (Map_/Both (Merge a c) (Merge b d))
(Merge (Map_/Both a b) Map_/Used) = *
(Merge Map_/Used (Map_/Both a b)) = *
// Radix : U60 -> Map
(Radix n) =
let r = Used
let r = (Swap (& n 0x1) r Free)
let r = (Swap (& n 0x2) r Free)
let r = (Swap (& n 0x4) r Free)
let r = (Swap (& n 0x8) r Free)
let r = (Swap (& n 0x10) r Free)
let r = Map_/Used
let r = (Swap (& n 1) r Map_/Free)
let r = (Swap (& n 2) r Map_/Free)
let r = (Swap (& n 4) r Map_/Free)
let r = (Swap (& n 8) r Map_/Free)
let r = (Swap (& n 16) r Map_/Free)
(Radix2 n r)
(Radix2 n r) =
let r = (Swap (& n 0x20) r Free)
let r = (Swap (& n 0x40) r Free)
let r = (Swap (& n 0x80) r Free)
let r = (Swap (& n 0x100) r Free)
let r = (Swap (& n 0x200) r Free)
let r = (Swap (& n 32) r Map_/Free)
let r = (Swap (& n 64) r Map_/Free)
let r = (Swap (& n 128) r Map_/Free)
let r = (Swap (& n 256) r Map_/Free)
let r = (Swap (& n 512) r Map_/Free)
(Radix3 n r)
(Radix3 n r) =
let r = (Swap (& n 0x400) r Free)
let r = (Swap (& n 0x800) r Free)
let r = (Swap (& n 0x1000) r Free)
let r = (Swap (& n 0x2000) r Free)
let r = (Swap (& n 0x4000) r Free)
let r = (Swap (& n 1024) r Map_/Free)
let r = (Swap (& n 2048) r Map_/Free)
let r = (Swap (& n 4096) r Map_/Free)
let r = (Swap (& n 8192) r Map_/Free)
let r = (Swap (& n 16384) r Map_/Free)
(Radix4 n r)
(Radix4 n r) =
let r = (Swap (& n 0x8000) r Free)
let r = (Swap (& n 0x10000) r Free)
let r = (Swap (& n 0x20000) r Free)
let r = (Swap (& n 0x40000) r Free)
let r = (Swap (& n 0x80000) r Free)
let r = (Swap (& n 32768) r Map_/Free)
let r = (Swap (& n 65536) r Map_/Free)
let r = (Swap (& n 131072) r Map_/Free)
let r = (Swap (& n 262144) r Map_/Free)
let r = (Swap (& n 524288) r Map_/Free)
(Radix5 n r)
(Radix5 n r) =
let r = (Swap (& n 0x100000) r Free)
let r = (Swap (& n 0x200000) r Free)
let r = (Swap (& n 0x400000) r Free)
let r = (Swap (& n 0x800000) r Free)
let r = (Swap (& n 1048576) r Map_/Free)
let r = (Swap (& n 2097152) r Map_/Free)
let r = (Swap (& n 4194304) r Map_/Free)
let r = (Swap (& n 8388608) r Map_/Free)
r
// Reverse : Arr -> Arr
(Reverse Null) = Null
(Reverse (Leaf a)) = (Leaf a)
(Reverse (Node a b)) = (Node (Reverse b) (Reverse a))
(Reverse Arr/Null) = Arr/Null
(Reverse (Arr/Leaf a)) = (Arr/Leaf a)
(Reverse (Arr/Node a b)) = (Arr/Node (Reverse b) (Reverse a))
// Sum : Arr -> U60
(Sum Null) = 0
(Sum (Leaf x)) = x
(Sum (Node a b)) = (+ (Sum a) (Sum b))
(Sum Arr/Null) = 0
(Sum (Arr/Leaf x)) = x
(Sum (Arr/Node a b)) = (+ (Sum a) (Sum b))
// Gen : U60 -> Arr
(Gen n) = (Gen.go n 0)
(Gen.go n x) = switch n {
0: (Leaf x)
0: (Arr/Leaf x)
_:
let a = (* x 2)
let b = (| (* x 2) 1)
(Node (Gen.go n-1 a) (Gen.go n-1 b))
(Arr/Node (Gen.go n-1 a) (Gen.go n-1 b))
}
Main = (Sum (Sort (Reverse (Gen 4))))