mirror of
https://github.com/HigherOrderCO/Bend.git
synced 2024-09-11 11:56:54 +03:00
Change comments to #
This commit is contained in:
parent
36cb14e7fd
commit
5b4524e4a7
50
README.md
50
README.md
@ -71,7 +71,7 @@ Bend programs consist of a series of function definitions, always starting with
|
|||||||
Functions can receive arguments both directly and using a lambda abstraction.
|
Functions can receive arguments both directly and using a lambda abstraction.
|
||||||
|
|
||||||
```py
|
```py
|
||||||
// These two are equivalent
|
# These two are equivalent
|
||||||
def add(x, y):
|
def add(x, y):
|
||||||
return x + y
|
return x + y
|
||||||
|
|
||||||
@ -90,22 +90,22 @@ def main:
|
|||||||
You can bundle multiple values into a single value using a tuple or a struct.
|
You can bundle multiple values into a single value using a tuple or a struct.
|
||||||
|
|
||||||
```py
|
```py
|
||||||
// With a tuple
|
# With a tuple
|
||||||
def Tuple.fst(x):
|
def Tuple.fst(x):
|
||||||
// This destructures the tuple into the two values it holds.
|
# This destructures the tuple into the two values it holds.
|
||||||
// '*' means that the value is discarded and not bound to any variable.
|
# '*' means that the value is discarded and not bound to any variable.
|
||||||
(fst, *) = x
|
(fst, *) = x
|
||||||
return fst
|
return fst
|
||||||
|
|
||||||
// With a struct
|
# With a struct
|
||||||
struct Pair(fst, snd):
|
struct Pair(fst, snd):
|
||||||
def Pair.fst(x):
|
def Pair.fst(x):
|
||||||
match x:
|
match x:
|
||||||
Pair:
|
Pair:
|
||||||
return x.fst
|
return x.fst
|
||||||
|
|
||||||
// We can also directly access the fields of a struct.
|
# We can also directly access the fields of a struct.
|
||||||
// This requires that we tell the compiler the type of the variable where it is defined.
|
# This requires that we tell the compiler the type of the variable where it is defined.
|
||||||
def Pair.fst_2(x: Pair):
|
def Pair.fst_2(x: Pair):
|
||||||
return x.fst
|
return x.fst
|
||||||
```
|
```
|
||||||
@ -124,7 +124,7 @@ We can then pattern match on the enum to perform different actions depending on
|
|||||||
def Maybe.or_default(x, default):
|
def Maybe.or_default(x, default):
|
||||||
match x:
|
match x:
|
||||||
Maybe/some:
|
Maybe/some:
|
||||||
// We can access the fields of the variant using 'matched.field'
|
# We can access the fields of the variant using 'matched.field'
|
||||||
return x.val
|
return x.val
|
||||||
Maybe/none:
|
Maybe/none:
|
||||||
return default
|
return default
|
||||||
@ -135,9 +135,9 @@ This allows us to easily create and consume these recursive data structures with
|
|||||||
|
|
||||||
```py
|
```py
|
||||||
def MyTree.sum(x):
|
def MyTree.sum(x):
|
||||||
// Sum all the values in the tree.
|
# Sum all the values in the tree.
|
||||||
fold x:
|
fold x:
|
||||||
// The fold is implicitly called for fields marked with '~' in their definition.
|
# The fold is implicitly called for fields marked with '~' in their definition.
|
||||||
Node:
|
Node:
|
||||||
return val + x.left + x.right
|
return val + x.left + x.right
|
||||||
Leaf:
|
Leaf:
|
||||||
@ -145,10 +145,10 @@ def MyTree.sum(x):
|
|||||||
|
|
||||||
def main:
|
def main:
|
||||||
bend val = 0 while val < 0:
|
bend val = 0 while val < 0:
|
||||||
// 'go' calls the bend recursively with the provided values.
|
# 'go' calls the bend recursively with the provided values.
|
||||||
x = Node(val=val, left=go(val + 1), right=go(val + 1))
|
x = Node(val=val, left=go(val + 1), right=go(val + 1))
|
||||||
then:
|
then:
|
||||||
// 'then' is the base case, when the condition fails.
|
# 'then' is the base case, when the condition fails.
|
||||||
x = Leaf
|
x = Leaf
|
||||||
|
|
||||||
return MyTree.sum(x)
|
return MyTree.sum(x)
|
||||||
@ -206,7 +206,7 @@ def foo(x):
|
|||||||
use result = bar(1, x)
|
use result = bar(1, x)
|
||||||
return (result, result)
|
return (result, result)
|
||||||
|
|
||||||
// Is equivalent to
|
# Is equivalent to
|
||||||
def foo(x):
|
def foo(x):
|
||||||
return (bar(1, x), bar(1, x))
|
return (bar(1, x), bar(1, x))
|
||||||
```
|
```
|
||||||
@ -231,11 +231,11 @@ Bend has native numbers and operations.
|
|||||||
|
|
||||||
```py
|
```py
|
||||||
def main:
|
def main:
|
||||||
a = 1 // A 24 bit unsigned integer.
|
a = 1 # A 24 bit unsigned integer.
|
||||||
b = +2 // A 24 bit signed integer.
|
b = +2 # A 24 bit signed integer.
|
||||||
c = -3 // Another signed integer, but with negative value.
|
c = -3 # Another signed integer, but with negative value.
|
||||||
d = 1.0 // A 24 bit floating point number.
|
d = 1.0 # A 24 bit floating point number.
|
||||||
e = +0.001 // Also a float.
|
e = +0.001 # Also a float.
|
||||||
return (a * 2, b - c, d / e)
|
return (a * 2, b - c, d / e)
|
||||||
```
|
```
|
||||||
|
|
||||||
@ -243,13 +243,13 @@ def main:
|
|||||||
|
|
||||||
```py
|
```py
|
||||||
switch x = 4:
|
switch x = 4:
|
||||||
// From '0' to n, ending with the default case '_'.
|
# From '0' to n, ending with the default case '_'.
|
||||||
0: "zero"
|
0: "zero"
|
||||||
1: "one"
|
1: "one"
|
||||||
2: "two"
|
2: "two"
|
||||||
// The default case binds the name <arg>-<n>
|
# The default case binds the name <arg>-<n>
|
||||||
// where 'arg' is the name of the argument and 'n' is the next number.
|
# where 'arg' is the name of the argument and 'n' is the next number.
|
||||||
// In this case, it's 'x-3', which will have value (4 - 3) = 1
|
# In this case, it's 'x-3', which will have value (4 - 3) = 1
|
||||||
_: String.concat("other: ", (String.from_num x-3))
|
_: String.concat("other: ", (String.from_num x-3))
|
||||||
```
|
```
|
||||||
|
|
||||||
@ -264,14 +264,14 @@ A string is desugared to a String data type containing two constructors, `String
|
|||||||
List also becomes a type with two constructors, `List.cons` and `List.nil`.
|
List also becomes a type with two constructors, `List.cons` and `List.nil`.
|
||||||
|
|
||||||
```rs
|
```rs
|
||||||
// These two are equivalent
|
# These two are equivalent
|
||||||
def StrEx:
|
def StrEx:
|
||||||
"Hello"
|
"Hello"
|
||||||
|
|
||||||
def ids:
|
def ids:
|
||||||
[1, 2, 3]
|
[1, 2, 3]
|
||||||
|
|
||||||
// These types are builtin.
|
# These types are builtin.
|
||||||
enum String:
|
enum String:
|
||||||
String.cons(head, tail)
|
String.cons(head, tail)
|
||||||
String.nil
|
String.nil
|
||||||
@ -287,7 +287,7 @@ def ids:
|
|||||||
Characters are delimited by `'` `'` and support Unicode escape sequences. They are encoded as a U24 with the unicode codepoint as their value.
|
Characters are delimited by `'` `'` and support Unicode escape sequences. They are encoded as a U24 with the unicode codepoint as their value.
|
||||||
|
|
||||||
```
|
```
|
||||||
// These two are equivalent
|
# These two are equivalent
|
||||||
def chars:
|
def chars:
|
||||||
['A', '\u{4242}', '🌎']
|
['A', '\u{4242}', '🌎']
|
||||||
|
|
||||||
|
@ -119,7 +119,7 @@ return "hello"
|
|||||||
Returns the expression that follows. The last statement of each branch of a function must be a `return`.
|
Returns the expression that follows. The last statement of each branch of a function must be a `return`.
|
||||||
|
|
||||||
```py
|
```py
|
||||||
// Allowed, all branches return
|
# Allowed, all branches return
|
||||||
def max(a, b):
|
def max(a, b):
|
||||||
if a > b:
|
if a > b:
|
||||||
return a
|
return a
|
||||||
@ -128,7 +128,7 @@ def max(a, b):
|
|||||||
```
|
```
|
||||||
|
|
||||||
```py
|
```py
|
||||||
// Not allowed, early return
|
# Not allowed, early return
|
||||||
def Foo(x):
|
def Foo(x):
|
||||||
if test_condition(x):
|
if test_condition(x):
|
||||||
return "err"
|
return "err"
|
||||||
@ -139,7 +139,7 @@ def Foo(x):
|
|||||||
```
|
```
|
||||||
|
|
||||||
```py
|
```py
|
||||||
// Not allowed, one of the branches doesn't return
|
# Not allowed, one of the branches doesn't return
|
||||||
def Foo(a, b):
|
def Foo(a, b):
|
||||||
if a < b:
|
if a < b:
|
||||||
return a
|
return a
|
||||||
@ -283,7 +283,7 @@ It's equivalent to pattern matching on the object, with the restriction that its
|
|||||||
open Point: p
|
open Point: p
|
||||||
...
|
...
|
||||||
|
|
||||||
// Equivalent to:
|
# Equivalent to:
|
||||||
match p:
|
match p:
|
||||||
Point:
|
Point:
|
||||||
...
|
...
|
||||||
@ -316,7 +316,7 @@ def Result/bind(res, nxt):
|
|||||||
Other statements are allowed inside the `do` block and it can both return a value at the end and bind a variable, like branching statements do.
|
Other statements are allowed inside the `do` block and it can both return a value at the end and bind a variable, like branching statements do.
|
||||||
|
|
||||||
```
|
```
|
||||||
// Also ok:
|
# Also ok:
|
||||||
do Result:
|
do Result:
|
||||||
x <- safe_div(2, 0);
|
x <- safe_div(2, 0);
|
||||||
y = x
|
y = x
|
||||||
@ -399,9 +399,9 @@ In case named arguments are used, they must come after the positional arguments
|
|||||||
|
|
||||||
eraser = *
|
eraser = *
|
||||||
|
|
||||||
*(41 + 1) // applies 41 + 1 to `*` erasing the number and returns `*`
|
*(41 + 1) # applies 41 + 1 to `*` erasing the number and returns `*`
|
||||||
|
|
||||||
* = 41 + 1 // erases 41 + 1
|
* = 41 + 1 # erases 41 + 1
|
||||||
```
|
```
|
||||||
|
|
||||||
The effect of an eraser is to free memory. Erasers behave like a `null`.
|
The effect of an eraser is to free memory. Erasers behave like a `null`.
|
||||||
@ -482,7 +482,7 @@ Only supports unicode codepoints up to `0xFFFFFF`.
|
|||||||
### Symbol Literal
|
### Symbol Literal
|
||||||
|
|
||||||
```python
|
```python
|
||||||
// Becomes 2146 (33 << 6 + 34)
|
# Becomes 2146 (33 << 6 + 34)
|
||||||
`hi`
|
`hi`
|
||||||
```
|
```
|
||||||
|
|
||||||
@ -811,7 +811,7 @@ ask y = (div 3 2)
|
|||||||
ask x = (rem y 0)
|
ask x = (rem y 0)
|
||||||
x
|
x
|
||||||
|
|
||||||
// Becomes
|
# Becomes
|
||||||
(Result/bind (div 3 2) λy (Result/bind (rem y 0) λx x))
|
(Result/bind (div 3 2) λy (Result/bind (rem y 0) λx x))
|
||||||
```
|
```
|
||||||
|
|
||||||
@ -857,7 +857,7 @@ Only supports unicode codepoints up to `0xFFFFFF`.
|
|||||||
### Symbol Literal
|
### Symbol Literal
|
||||||
|
|
||||||
```python
|
```python
|
||||||
// Becomes 2146 (33 << 6 + 34)
|
# Becomes 2146 (33 << 6 + 34)
|
||||||
`hi`
|
`hi`
|
||||||
```
|
```
|
||||||
|
|
||||||
|
@ -56,6 +56,6 @@ def sort(d, s, t):
|
|||||||
return flow(d, s, sort(d-1, 0, t.a), sort(d-1, 1, t.b))
|
return flow(d, s, sort(d-1, 0, t.a), sort(d-1, 1, t.b))
|
||||||
|
|
||||||
def main:
|
def main:
|
||||||
// Sorts the numbers from 0 to 2^depth.
|
# Sorts the numbers from 0 to 2^depth.
|
||||||
depth = 14
|
depth = 14
|
||||||
return sum(depth, sort(depth, 0, gen(depth, 0)))
|
return sum(depth, sort(depth, 0, gen(depth, 0)))
|
||||||
|
@ -1,18 +1,18 @@
|
|||||||
// Sorts a list
|
# Sorts a list
|
||||||
|
|
||||||
// sort : List -> List
|
# sort : List -> List
|
||||||
(Sort []) = []
|
(Sort []) = []
|
||||||
(Sort (List/Cons x xs)) = (Insert x (Sort xs))
|
(Sort (List/Cons x xs)) = (Insert x (Sort xs))
|
||||||
|
|
||||||
// Insert : U60 -> List -> List
|
# Insert : U60 -> List -> List
|
||||||
(Insert v []) = (List/Cons v [])
|
(Insert v []) = (List/Cons v [])
|
||||||
(Insert v (List/Cons x xs)) = (SwapGT (> v x) v x xs)
|
(Insert v (List/Cons x xs)) = (SwapGT (> v x) v x xs)
|
||||||
|
|
||||||
// SwapGT : U60 -> U60 -> U60 -> List -> List
|
# SwapGT : U60 -> U60 -> U60 -> List -> List
|
||||||
(SwapGT 0 v x xs) = (List/Cons v (List/Cons x xs))
|
(SwapGT 0 v x xs) = (List/Cons v (List/Cons x xs))
|
||||||
(SwapGT _ v x xs) = (List/Cons x (Insert v xs))
|
(SwapGT _ v x xs) = (List/Cons x (Insert v xs))
|
||||||
|
|
||||||
// Generates a random list
|
# Generates a random list
|
||||||
(Rnd 0 s) = List/Nil
|
(Rnd 0 s) = List/Nil
|
||||||
(Rnd n s) =
|
(Rnd n s) =
|
||||||
let s = (^ s (* s 0b10000000000000))
|
let s = (^ s (* s 0b10000000000000))
|
||||||
@ -20,7 +20,7 @@
|
|||||||
let s = (^ s (* s 0b100000))
|
let s = (^ s (* s 0b100000))
|
||||||
(List/Cons s (Rnd (- n 1) s))
|
(List/Cons s (Rnd (- n 1) s))
|
||||||
|
|
||||||
// Sums a list
|
# Sums a list
|
||||||
(Sum []) = 0
|
(Sum []) = 0
|
||||||
(Sum (List/Cons x xs)) = (+ x (Sum xs))
|
(Sum (List/Cons x xs)) = (+ x (Sum xs))
|
||||||
|
|
||||||
@ -28,5 +28,5 @@
|
|||||||
let n = 10
|
let n = 10
|
||||||
(Sum (Sort (Rnd 0x100 n)))
|
(Sum (Sort (Rnd 0x100 n)))
|
||||||
|
|
||||||
// Use an argument from cli
|
# Use an argument from cli
|
||||||
// (Main n) = (Sum (Sort (Rnd 0x100 n)))
|
# (Main n) = (Sum (Sort (Rnd 0x100 n)))
|
||||||
|
@ -1,15 +1,15 @@
|
|||||||
// This program is an example that shows how scopeless lambdas can be used.
|
# This program is an example that shows how scopeless lambdas can be used.
|
||||||
|
|
||||||
Seq a b = a
|
Seq a b = a
|
||||||
|
|
||||||
// Create a program capable of using `callcc`
|
# Create a program capable of using `callcc`
|
||||||
CC.lang = λprogram
|
CC.lang = λprogram
|
||||||
let callcc = λcallback (λ$garbage($hole) (callback λ$hole(0)));
|
let callcc = λcallback (λ$garbage($hole) (callback λ$hole(0)));
|
||||||
let result = (program callcc);
|
let result = (program callcc);
|
||||||
let garbage = $garbage; // Discard `$garbage`, which is the value returned by `callback`
|
let garbage = $garbage; # Discard `$garbage`, which is the value returned by `callback`
|
||||||
(Seq result garbage)
|
(Seq result garbage)
|
||||||
|
|
||||||
main = (CC.lang λcallcc
|
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`
|
# 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)))
|
(+ 10 (callcc λk(+ (k 42) 1729)))
|
||||||
)
|
)
|
||||||
|
@ -1,36 +1,36 @@
|
|||||||
// Write definitions like this
|
# Write definitions like this
|
||||||
(Def1) = ((λa a) (λb b))
|
(Def1) = ((λa a) (λb b))
|
||||||
|
|
||||||
// You can call a definition by just referencing its name
|
# You can call a definition by just referencing its name
|
||||||
// It will be substituted in place of the reference
|
# It will be substituted in place of the reference
|
||||||
(Def2) = ((λa a) Def1)
|
(Def2) = ((λa a) Def1)
|
||||||
|
|
||||||
// Definitions and variables can have names in upper and lower case and contain numbers
|
# Definitions and variables can have names in upper and lower case and contain numbers
|
||||||
// Names defined in a more inner position shadow names in an outer position
|
# Names defined in a more inner position shadow names in an outer position
|
||||||
(def3) = ((λDef1 Def1) (λx λx x))
|
(def3) = ((λDef1 Def1) (λx λx x))
|
||||||
|
|
||||||
// The language is affine, but if you use a variable more than once the compiler inserts duplications for you
|
# The language is affine, but if you use a variable more than once the compiler inserts duplications for you
|
||||||
// Of course you can always do them manually
|
# Of course you can always do them manually
|
||||||
(def4) = λz let {z1 z2} = z; (z1 ((λx (x x x x x)) z2))
|
(def4) = λz let {z1 z2} = z; (z1 ((λx (x x x x x)) z2))
|
||||||
|
|
||||||
// You can use machine numbers and some native numeric operations
|
# You can use machine numbers and some native numeric operations
|
||||||
// Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
|
# Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
|
||||||
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
|
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
|
||||||
|
|
||||||
// You can use numbers on the native match expression
|
# You can use numbers on the native match expression
|
||||||
// The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1
|
# The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1
|
||||||
(Num.pred) = λn
|
(Num.pred) = λn
|
||||||
switch n {
|
switch n {
|
||||||
0: 0
|
0: 0
|
||||||
_: n-1
|
_: n-1
|
||||||
}
|
}
|
||||||
|
|
||||||
// Write new data types like this
|
# Write new data types like this
|
||||||
data Option = (Some val) | None
|
data Option = (Some val) | None
|
||||||
data Bool = True | False
|
data Bool = True | False
|
||||||
|
|
||||||
// You can have pattern matching on definitions
|
# You can have pattern matching on definitions
|
||||||
// Use `*` to ignore a pattern
|
# Use `*` to ignore a pattern
|
||||||
(Option.unwrap_or (Option/Some val) *) = val
|
(Option.unwrap_or (Option/Some val) *) = val
|
||||||
(Option.unwrap_or Option/None or) = or
|
(Option.unwrap_or Option/None or) = or
|
||||||
|
|
||||||
@ -38,39 +38,39 @@ data Bool = True | False
|
|||||||
(Bool.or * Bool/True) = Bool/True
|
(Bool.or * Bool/True) = Bool/True
|
||||||
(Bool.or * *) = Bool/False
|
(Bool.or * *) = Bool/False
|
||||||
|
|
||||||
// Or using a match expression
|
# Or using a match expression
|
||||||
(Bool.not) = λbool
|
(Bool.not) = λbool
|
||||||
match bool {
|
match bool {
|
||||||
Bool/True: Bool/False
|
Bool/True: Bool/False
|
||||||
Bool/False: Bool/True
|
Bool/False: Bool/True
|
||||||
}
|
}
|
||||||
|
|
||||||
// Data types can store values
|
# Data types can store values
|
||||||
data Boxed = (Box val)
|
data Boxed = (Box val)
|
||||||
|
|
||||||
// Types with only one constructor can be destructured using `let` or a single matching definition
|
# Types with only one constructor can be destructured using `let` or a single matching definition
|
||||||
(Box.map (Boxed/Box val) f) = (Boxed/Box (f val))
|
(Box.map (Boxed/Box val) f) = (Boxed/Box (f val))
|
||||||
|
|
||||||
(Box.unbox) = λbox match box {
|
(Box.unbox) = λbox match box {
|
||||||
Boxed/Box: box.val
|
Boxed/Box: box.val
|
||||||
}
|
}
|
||||||
|
|
||||||
// Use tuples to store two values together without needing to create a new data type
|
# Use tuples to store two values together without needing to create a new data type
|
||||||
(Tuple.new fst snd) =
|
(Tuple.new fst snd) =
|
||||||
let pair = (fst, snd)
|
let pair = (fst, snd)
|
||||||
pair
|
pair
|
||||||
|
|
||||||
// Then you can destructure it inside the definition or using `let`
|
# Then you can destructure it inside the definition or using `let`
|
||||||
(Tuple.fst (fst, snd)) = fst
|
(Tuple.fst (fst, snd)) = fst
|
||||||
|
|
||||||
(Tuple.snd) = λpair
|
(Tuple.snd) = λpair
|
||||||
let (fst, snd) = pair
|
let (fst, snd) = pair
|
||||||
snd
|
snd
|
||||||
|
|
||||||
// All files must have a main definition to be run.
|
# All files must have a main definition to be run.
|
||||||
// You can execute a program in HVM with "cargo run -- run <path to file>"
|
# 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
|
# Other options are "check" (the default mode) to just see if the file is well formed
|
||||||
// and "compile" to output hvm-core code.
|
# and "compile" to output hvm-core code.
|
||||||
(main) =
|
(main) =
|
||||||
let tup = (Tuple.new Option/None (Num.pred 5))
|
let tup = (Tuple.new Option/None (Num.pred 5))
|
||||||
|
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
zero = λs λz z
|
zero = λs λz z
|
||||||
succ = λpred λs λz (s pred) // Creates a Scott number out of its predecessor
|
succ = λpred λs λz (s pred) # Creates a Scott number out of its predecessor
|
||||||
|
|
||||||
two = (succ (succ zero)) // λs λz (s λs λz (s λs λz z))
|
two = (succ (succ zero)) # λs λz (s λs λz (s λs λz z))
|
||||||
|
|
||||||
fusing_add = λa
|
fusing_add = λa
|
||||||
let case_succ = λa_pred λb (succ (fusing_add a_pred b))
|
let case_succ = λa_pred λb (succ (fusing_add a_pred b))
|
||||||
|
@ -2,11 +2,11 @@ true = λt λf t
|
|||||||
false = λt λf f
|
false = λt λf f
|
||||||
not = λboolean (boolean false true)
|
not = λboolean (boolean false true)
|
||||||
fusing_not = λboolean λt λf (boolean f t)
|
fusing_not = λboolean λt λf (boolean f t)
|
||||||
// Creates a Church numeral out of a native number
|
# Creates a Church numeral out of a native number
|
||||||
to_church n = switch n {
|
to_church n = switch n {
|
||||||
0: λf λx x
|
0: λf λx x
|
||||||
_: λf λx (f (to_church n-1 f x))
|
_: λf λx (f (to_church n-1 f x))
|
||||||
}
|
}
|
||||||
main =
|
main =
|
||||||
// Self-composes `not` 2^24 times and prints the result.
|
# 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?
|
||||||
|
@ -1,24 +1,24 @@
|
|||||||
// size = 1 << 8
|
# size = 1 << 8
|
||||||
|
|
||||||
Mul = λn λm λs (n (m s))
|
Mul = λn λm λs (n (m s))
|
||||||
|
|
||||||
// Church nat
|
# Church nat
|
||||||
C2 = λf λx (f (f x))
|
C2 = λf λx (f (f x))
|
||||||
|
|
||||||
// Church powers of two
|
# Church powers of two
|
||||||
P2 = (Mul C2 C2) // 4
|
P2 = (Mul C2 C2) # 4
|
||||||
P3 = (Mul C2 P2) // 8
|
P3 = (Mul C2 P2) # 8
|
||||||
P4 = (Mul C2 P3) // 16
|
P4 = (Mul C2 P3) # 16
|
||||||
P5 = (Mul C2 P4) // 32
|
P5 = (Mul C2 P4) # 32
|
||||||
P6 = (Mul C2 P5) // 64
|
P6 = (Mul C2 P5) # 64
|
||||||
P7 = (Mul C2 P6) // 128
|
P7 = (Mul C2 P6) # 128
|
||||||
P8 = (Mul C2 P7) // 256
|
P8 = (Mul C2 P7) # 256
|
||||||
|
|
||||||
// Booleans
|
# Booleans
|
||||||
True = λt λf t
|
True = λt λf t
|
||||||
False = λt λf f
|
False = λt λf f
|
||||||
Not = λb ((b False) True)
|
Not = λb ((b False) True)
|
||||||
Neg = λb λt λf (b f t)
|
Neg = λb λt λf (b f t)
|
||||||
|
|
||||||
// Negates 'true' 256 times: 'neg' is faster than 'not' because it fuses
|
# Negates 'true' 256 times: 'neg' is faster than 'not' because it fuses
|
||||||
Main = (P8 Neg True)
|
Main = (P8 Neg True)
|
||||||
|
@ -1,9 +1,9 @@
|
|||||||
// a binary tree
|
# a binary tree
|
||||||
type MyTree:
|
type MyTree:
|
||||||
Node { val, ~left, ~right }
|
Node { val, ~left, ~right }
|
||||||
Leaf { val }
|
Leaf { val }
|
||||||
|
|
||||||
// sums all values in a tree
|
# sums all values in a tree
|
||||||
def sum(tree):
|
def sum(tree):
|
||||||
fold tree:
|
fold tree:
|
||||||
case MyTree/Node:
|
case MyTree/Node:
|
||||||
@ -11,7 +11,7 @@ def sum(tree):
|
|||||||
case MyTree/Leaf:
|
case MyTree/Leaf:
|
||||||
return tree.val
|
return tree.val
|
||||||
|
|
||||||
// generates a binary tree of given depth
|
# generates a binary tree of given depth
|
||||||
def gen(depth):
|
def gen(depth):
|
||||||
bend val = 0:
|
bend val = 0:
|
||||||
when val < depth:
|
when val < depth:
|
||||||
@ -20,6 +20,6 @@ def gen(depth):
|
|||||||
tree = MyTree/Leaf { val: val }
|
tree = MyTree/Leaf { val: val }
|
||||||
return tree
|
return tree
|
||||||
|
|
||||||
// returns the sum of 0..2^16
|
# returns the sum of 0..2^16
|
||||||
def main:
|
def main:
|
||||||
return sum(gen(16))
|
return sum(gen(16))
|
||||||
|
@ -1,15 +1,15 @@
|
|||||||
// A cool trick involving HVM's scopeless lambdas is linear qs:
|
# A cool trick involving HVM's scopeless lambdas is linear qs:
|
||||||
|
|
||||||
// Qnew : Queue a
|
# Qnew : Queue a
|
||||||
Qnew = λx x
|
Qnew = λx x
|
||||||
|
|
||||||
// Qadd : a -> Queue a -> Queue a
|
# Qadd : a -> Queue a -> Queue a
|
||||||
Qadd = λx λq λk (q λc (c x k))
|
Qadd = λx λq λk (q λc (c x k))
|
||||||
|
|
||||||
// Qrem : Queue a -> Pair a (Queue a)
|
# Qrem : Queue a -> Pair a (Queue a)
|
||||||
Qrem = λq (q $k λx λxs λp(p x λ$k xs))
|
Qrem = λq (q $k λx λxs λp(p x λ$k xs))
|
||||||
|
|
||||||
// Output: [1, 2, 3]
|
# Output: [1, 2, 3]
|
||||||
main =
|
main =
|
||||||
let q = Qnew
|
let q = Qnew
|
||||||
let q = (Qadd 1 q)
|
let q = (Qadd 1 q)
|
||||||
|
@ -1,6 +1,6 @@
|
|||||||
data Tree = Leaf | (Node l m r)
|
data Tree = Leaf | (Node l m r)
|
||||||
|
|
||||||
// Parallel QuickSort
|
# Parallel QuickSort
|
||||||
(Sort List/Nil) = Tree/Leaf
|
(Sort List/Nil) = Tree/Leaf
|
||||||
(Sort (List/Cons x xs)) =
|
(Sort (List/Cons x xs)) =
|
||||||
((Part x xs) λmin λmax
|
((Part x xs) λmin λmax
|
||||||
@ -8,15 +8,15 @@ data Tree = Leaf | (Node l m r)
|
|||||||
let rgt = (Sort max)
|
let rgt = (Sort max)
|
||||||
(Tree/Node lft x rgt))
|
(Tree/Node lft x rgt))
|
||||||
|
|
||||||
// Partitions a list in two halves, less-than-p and greater-than-p
|
# 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/Nil) = λt (t List/Nil List/Nil)
|
||||||
(Part p (List/Cons x xs)) = (Push (> x p) x (Part p xs))
|
(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
|
# 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 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 _ x pair) = (pair λmin λmax λp (p min (List/Cons x max)))
|
||||||
|
|
||||||
// Generates a random list
|
# Generates a random list
|
||||||
(Rnd 0 s) = List/Nil
|
(Rnd 0 s) = List/Nil
|
||||||
(Rnd n s) =
|
(Rnd n s) =
|
||||||
let s = (^ s (* s 0b10000000000000))
|
let s = (^ s (* s 0b10000000000000))
|
||||||
@ -24,13 +24,13 @@ data Tree = Leaf | (Node l m r)
|
|||||||
let s = (^ s (* s 0b100000))
|
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
|
# Sums all elements in a concatenation tree
|
||||||
(Sum Tree/Leaf) = 0
|
(Sum Tree/Leaf) = 0
|
||||||
(Sum (Tree/Node l m r)) = (+ m (+ (Sum l) (Sum r)))
|
(Sum (Tree/Node l m r)) = (+ m (+ (Sum l) (Sum r)))
|
||||||
|
|
||||||
// Sorts and sums n random numbers
|
# Sorts and sums n random numbers
|
||||||
(Main) =
|
(Main) =
|
||||||
(Sum (Sort (Rnd 0x100 1)))
|
(Sum (Sort (Rnd 0x100 1)))
|
||||||
|
|
||||||
// Use an argument from cli
|
# Use an argument from cli
|
||||||
// (Main n) = (Sum (Sort (Rnd (<< 1 n) 1)))
|
# (Main n) = (Sum (Sort (Rnd (<< 1 n) 1)))
|
||||||
|
@ -6,15 +6,15 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
_: (Map_/Both b a)
|
_: (Map_/Both b a)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Sort : Arr -> Arr
|
# Sort : Arr -> Arr
|
||||||
(Sort t) = (ToArr 0 (ToMap t))
|
(Sort t) = (ToArr 0 (ToMap t))
|
||||||
|
|
||||||
// ToMap : Arr -> Map
|
# ToMap : Arr -> Map
|
||||||
(ToMap Arr/Null) = Map_/Free
|
(ToMap Arr/Null) = Map_/Free
|
||||||
(ToMap (Arr/Leaf a)) = (Radix a)
|
(ToMap (Arr/Leaf a)) = (Radix a)
|
||||||
(ToMap (Arr/Node a b)) = (Merge (ToMap a) (ToMap b))
|
(ToMap (Arr/Node a b)) = (Merge (ToMap a) (ToMap b))
|
||||||
|
|
||||||
// ToArr : U60 -> Map -> Arr
|
# ToArr : U60 -> Map -> Arr
|
||||||
(ToArr x Map_/Free) = Arr/Null
|
(ToArr x Map_/Free) = Arr/Null
|
||||||
(ToArr x Map_/Used) = (Arr/Leaf x)
|
(ToArr x Map_/Used) = (Arr/Leaf x)
|
||||||
(ToArr x (Map_/Both a b)) =
|
(ToArr x (Map_/Both a b)) =
|
||||||
@ -22,7 +22,7 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
let b = (ToArr (+ (* x 2) 1) b)
|
let b = (ToArr (+ (* x 2) 1) b)
|
||||||
(Arr/Node a b)
|
(Arr/Node a b)
|
||||||
|
|
||||||
// Merge : Map -> Map -> Map
|
# Merge : Map -> Map -> Map
|
||||||
(Merge Map_/Free Map_/Free) = Map_/Free
|
(Merge Map_/Free Map_/Free) = Map_/Free
|
||||||
(Merge Map_/Free Map_/Used) = Map_/Used
|
(Merge Map_/Free Map_/Used) = Map_/Used
|
||||||
(Merge Map_/Used Map_/Free) = Map_/Used
|
(Merge Map_/Used Map_/Free) = Map_/Used
|
||||||
@ -33,7 +33,7 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
(Merge (Map_/Both a b) Map_/Used) = *
|
(Merge (Map_/Both a b) Map_/Used) = *
|
||||||
(Merge Map_/Used (Map_/Both a b)) = *
|
(Merge Map_/Used (Map_/Both a b)) = *
|
||||||
|
|
||||||
// Radix : U60 -> Map
|
# Radix : U60 -> Map
|
||||||
(Radix n) =
|
(Radix n) =
|
||||||
let r = Map_/Used
|
let r = Map_/Used
|
||||||
let r = (Swap (& n 1) r Map_/Free)
|
let r = (Swap (& n 1) r Map_/Free)
|
||||||
@ -75,17 +75,17 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
r
|
r
|
||||||
|
|
||||||
|
|
||||||
// Reverse : Arr -> Arr
|
# Reverse : Arr -> Arr
|
||||||
(Reverse Arr/Null) = Arr/Null
|
(Reverse Arr/Null) = Arr/Null
|
||||||
(Reverse (Arr/Leaf a)) = (Arr/Leaf a)
|
(Reverse (Arr/Leaf a)) = (Arr/Leaf a)
|
||||||
(Reverse (Arr/Node a b)) = (Arr/Node (Reverse b) (Reverse a))
|
(Reverse (Arr/Node a b)) = (Arr/Node (Reverse b) (Reverse a))
|
||||||
|
|
||||||
// Sum : Arr -> U60
|
# Sum : Arr -> U60
|
||||||
(Sum Arr/Null) = 0
|
(Sum Arr/Null) = 0
|
||||||
(Sum (Arr/Leaf x)) = x
|
(Sum (Arr/Leaf x)) = x
|
||||||
(Sum (Arr/Node a b)) = (+ (Sum a) (Sum b))
|
(Sum (Arr/Node a b)) = (+ (Sum a) (Sum b))
|
||||||
|
|
||||||
// Gen : U60 -> Arr
|
# Gen : U60 -> Arr
|
||||||
(Gen n) = (Gen.go n 0)
|
(Gen n) = (Gen.go n 0)
|
||||||
(Gen.go n x) = switch n {
|
(Gen.go n x) = switch n {
|
||||||
0: (Arr/Leaf x)
|
0: (Arr/Leaf x)
|
||||||
|
@ -3,7 +3,7 @@ data List = (Cons head ~tail) | (Nil)
|
|||||||
data Result = (Ok val) | (Err val)
|
data Result = (Ok val) | (Err val)
|
||||||
data Nat = (Succ ~pred) | (Zero)
|
data Nat = (Succ ~pred) | (Zero)
|
||||||
|
|
||||||
// MAP Impl
|
# MAP Impl
|
||||||
|
|
||||||
data Map = (Node value ~left ~right) | (Leaf)
|
data Map = (Node value ~left ~right) | (Leaf)
|
||||||
|
|
||||||
@ -46,7 +46,7 @@ Map/set map key value =
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// IO Impl
|
# IO Impl
|
||||||
|
|
||||||
STRING_NIL_TAG = 0
|
STRING_NIL_TAG = 0
|
||||||
STRING_CONS_TAG = 1
|
STRING_CONS_TAG = 1
|
||||||
|
@ -682,6 +682,27 @@ impl<'a> Parser<'a> for TermParser<'a> {
|
|||||||
self.expected(format!("'{text}'").as_str())
|
self.expected(format!("'{text}'").as_str())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn skip_trivia(&mut self) {
|
||||||
|
while let Some(c) = self.peek_one() {
|
||||||
|
if c.is_ascii_whitespace() {
|
||||||
|
self.advance_one();
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
if c == '#' {
|
||||||
|
while let Some(c) = self.peek_one() {
|
||||||
|
if c != '\n' {
|
||||||
|
self.advance_one();
|
||||||
|
} else {
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
self.advance_one(); // Skip the newline character as well
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn is_name_char(c: char) -> bool {
|
pub fn is_name_char(c: char) -> bool {
|
||||||
@ -826,7 +847,7 @@ pub trait ParserCommons<'a>: Parser<'a> {
|
|||||||
char_count += 1;
|
char_count += 1;
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
if c == '/' && self.input().get(*self.index() ..).unwrap_or_default().starts_with("//") {
|
if c == '#' {
|
||||||
while let Some(c) = self.peek_one() {
|
while let Some(c) = self.peek_one() {
|
||||||
if c != '\n' {
|
if c != '\n' {
|
||||||
self.advance_one();
|
self.advance_one();
|
||||||
|
@ -58,6 +58,27 @@ impl<'a> Parser<'a> for PyParser<'a> {
|
|||||||
self.expected(format!("'{text}'").as_str())
|
self.expected(format!("'{text}'").as_str())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn skip_trivia(&mut self) {
|
||||||
|
while let Some(c) = self.peek_one() {
|
||||||
|
if c.is_ascii_whitespace() {
|
||||||
|
self.advance_one();
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
if c == '#' {
|
||||||
|
while let Some(c) = self.peek_one() {
|
||||||
|
if c != '\n' {
|
||||||
|
self.advance_one();
|
||||||
|
} else {
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
self.advance_one(); // Skip the newline character as well
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'a> PyParser<'a> {
|
impl<'a> PyParser<'a> {
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
// We want the nested calls in foo to be compiled as redexes written in outer to inner order
|
# We want the nested calls in foo to be compiled as redexes written in outer to inner order
|
||||||
// So they should compile to: @foo = root_tree & a ~ ... & b ~ ... & c ~ ...
|
# So they should compile to: @foo = root_tree & a ~ ... & b ~ ... & c ~ ...
|
||||||
foo = @x (a (b (c x)))
|
foo = @x (a (b (c x)))
|
||||||
foo2 = (a (b (c 0)))
|
foo2 = (a (b (c 0)))
|
||||||
|
|
||||||
|
@ -1,3 +1,3 @@
|
|||||||
// Fully parenthesized, this is (λa ((λb b) b)).
|
# Fully parenthesized, this is (λa ((λb b) b)).
|
||||||
// Since applications must have (), the second 'b' is not in scope
|
# Since applications must have (), the second 'b' is not in scope
|
||||||
main = λa (λb b b)
|
main = λa (λb b b)
|
||||||
|
@ -1,3 +1,3 @@
|
|||||||
// theoretically, this let could be elided and no dups would need to be emitted
|
# theoretically, this let could be elided and no dups would need to be emitted
|
||||||
// but this isn't legal in all cases, and it's unclear what heuristics could work here
|
# but this isn't legal in all cases, and it's unclear what heuristics could work here
|
||||||
main = @x let * = (+ x x); x
|
main = @x let * = (+ x x); x
|
||||||
|
@ -4,7 +4,7 @@ X = λx x
|
|||||||
let two = (λf1λx1 (f1 λf2λx2 (f2 λf0λx0 x0)));
|
let two = (λf1λx1 (f1 λf2λx2 (f2 λf0λx0 x0)));
|
||||||
let qua = (λs1λz1 (s1 λs2λz2 (s2 λs3λz3 (s3 λs4λz4 (s4 λs0λz0 z0)))));
|
let qua = (λs1λz1 (s1 λs2λz2 (s2 λs3λz3 (s3 λs4λz4 (s4 λs0λz0 z0)))));
|
||||||
X X (X two qua)
|
X X (X two qua)
|
||||||
// Because there is no parens around the return term, the lets are only in scope for the first X
|
# Because there is no parens around the return term, the lets are only in scope for the first X
|
||||||
// This test is to make sure that the affine checking and duping infering marks them as erased as we expect.
|
# This test is to make sure that the affine checking and duping infering marks them as erased as we expect.
|
||||||
// We expect an unbound variable error on two and qua.
|
# We expect an unbound variable error on two and qua.
|
||||||
)
|
)
|
||||||
|
@ -1,25 +1,25 @@
|
|||||||
// Write definitions like this
|
# Write definitions like this
|
||||||
(Def1) = (λa a λb b)
|
(Def1) = (λa a λb b)
|
||||||
|
|
||||||
// You can call a definition by just referencing its name
|
# You can call a definition by just referencing its name
|
||||||
// It will be substituted in place of the reference
|
# It will be substituted in place of the reference
|
||||||
(Def2) = (λa a Def1)
|
(Def2) = (λa a Def1)
|
||||||
|
|
||||||
// Definitions and variables can have names in upper and lower case and contain numbers
|
# Definitions and variables can have names in upper and lower case and contain numbers
|
||||||
// Names defined in a more inner position shadow names in an outer position
|
# Names defined in a more inner position shadow names in an outer position
|
||||||
(def3) = (λDef1 Def1 λx λx x)
|
(def3) = (λDef1 Def1 λx λx x)
|
||||||
|
|
||||||
// The language is affine, but if you use a variable more than once the compiler inserts duplications for you
|
# The language is affine, but if you use a variable more than once the compiler inserts duplications for you
|
||||||
// Of course you can always do them manually
|
# Of course you can always do them manually
|
||||||
(def4) = λz let {z1 z2} = z; (z1 (λx (x x x x x) z2))
|
(def4) = λz let {z1 z2} = z; (z1 (λx (x x x x x) z2))
|
||||||
|
|
||||||
// You can use machine numbers and some native numeric operations
|
# You can use machine numbers and some native numeric operations
|
||||||
// Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
|
# Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
|
||||||
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
|
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
|
||||||
|
|
||||||
// All files must have a main definition to be run.
|
# All files must have a main definition to be run.
|
||||||
// You can execute a program in HVM with "cargo run -- --run <path to file>"
|
# 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
|
# Other options are "--check" (the default mode) to just see if the file is well formed
|
||||||
// and "--compile" to output hvm-core code.
|
# and "--compile" to output hvm-core code.
|
||||||
// (main) = (Def2 1)
|
# (main) = (Def2 1)
|
||||||
(main) = (Def2 1)
|
(main) = (Def2 1)
|
||||||
|
@ -1,2 +1,2 @@
|
|||||||
// currently broken without lazy_mode
|
# currently broken without lazy_mode
|
||||||
main = ((λfλx (f (f x))) (λfλx (f (f x))))
|
main = ((λfλx (f (f x))) (λfλx (f (f x))))
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// We expect the inferred 'λn-1' from the match to be extracted which allows this recursive func
|
# We expect the inferred 'λn-1' from the match to be extracted which allows this recursive func
|
||||||
val = λn (switch n { 0: valZ; _: (valS n-1) })
|
val = λn (switch n { 0: valZ; _: (valS n-1) })
|
||||||
valZ = 0
|
valZ = 0
|
||||||
valS = λp (val p)
|
valS = λp (val p)
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
// There was a bug where it would say "Non-exhaustive pattern (foo f1 f2 f3 f3)",
|
# There was a bug where it would say "Non-exhaustive pattern (foo f1 f2 f3 f3)",
|
||||||
// repeating the missing constructor for the next args.
|
# repeating the missing constructor for the next args.
|
||||||
|
|
||||||
data b1 = f1 | t1
|
data b1 = f1 | t1
|
||||||
data b2 = f2 | t2
|
data b2 = f2 | t2
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// We had a bug where this gave the incorrect error: "Expected a number but found 'a' at definition 'Foo'."
|
# We had a bug where this gave the incorrect error: "Expected a number but found 'a' at definition 'Foo'."
|
||||||
data bool = false | true
|
data bool = false | true
|
||||||
|
|
||||||
(Foo bool/false a) = 0
|
(Foo bool/false a) = 0
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// `Foo` inside the term `{Foo Foo}` is not in a active position, tests that it is not unnecessarily extracted
|
# `Foo` inside the term `{Foo Foo}` is not in a active position, tests that it is not unnecessarily extracted
|
||||||
Foo = @a switch a { 0: {Foo Foo}; _: @* a-1 }
|
Foo = @a switch a { 0: {Foo Foo}; _: @* a-1 }
|
||||||
|
|
||||||
main = (Foo 0)
|
main = (Foo 0)
|
||||||
|
@ -1,44 +1,44 @@
|
|||||||
data Tree = (Leaf a) | (Both a b)
|
data Tree = (Leaf a) | (Both a b)
|
||||||
data Error = Err
|
data Error = Err
|
||||||
|
|
||||||
// Atomic Swapper
|
# Atomic Swapper
|
||||||
(Swap n a b) = switch n {
|
(Swap n a b) = switch n {
|
||||||
0: (Tree/Both a b)
|
0: (Tree/Both a b)
|
||||||
_: (Tree/Both b a)
|
_: (Tree/Both b a)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Swaps distant values in parallel; corresponds to a Red Box
|
# Swaps distant values in parallel; corresponds to a Red Box
|
||||||
(Warp s (Tree/Leaf a) (Tree/Leaf b)) = (Swap (^ (> a b) s) (Tree/Leaf a) (Tree/Leaf b))
|
(Warp s (Tree/Leaf a) (Tree/Leaf b)) = (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/Both a b) (Tree/Both c d)) = (Join (Warp s a c) (Warp s b d))
|
||||||
(Warp s a b) = Error/Err
|
(Warp s a b) = Error/Err
|
||||||
|
|
||||||
// Rebuilds the warped tree in the original order
|
# Rebuilds the warped tree in the original order
|
||||||
(Join (Tree/Both a b) (Tree/Both c d)) = (Tree/Both (Tree/Both a c) (Tree/Both b d))
|
(Join (Tree/Both a b) (Tree/Both c d)) = (Tree/Both (Tree/Both a c) (Tree/Both b d))
|
||||||
(Join a b) = Error/Err
|
(Join a b) = Error/Err
|
||||||
|
|
||||||
// Recursively warps each sub-tree; corresponds to a Blue/Green Box
|
# Recursively warps each sub-tree; corresponds to a Blue/Green Box
|
||||||
(Flow s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Flow s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Flow s (Tree/Both a b)) = (Down s (Warp s a b))
|
(Flow s (Tree/Both a b)) = (Down s (Warp s a b))
|
||||||
|
|
||||||
// Propagates Flow downwards
|
# Propagates Flow downwards
|
||||||
(Down s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Down s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Down s (Tree/Both a b)) = (Tree/Both (Flow s a) (Flow s b))
|
(Down s (Tree/Both a b)) = (Tree/Both (Flow s a) (Flow s b))
|
||||||
|
|
||||||
// Bitonic Sort
|
# Bitonic Sort
|
||||||
(Sort s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Sort s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Sort s (Tree/Both a b)) = (Flow s (Tree/Both (Sort 0 a) (Sort 1 b)))
|
(Sort s (Tree/Both a b)) = (Flow s (Tree/Both (Sort 0 a) (Sort 1 b)))
|
||||||
|
|
||||||
// Generates a tree of depth `n`
|
# Generates a tree of depth `n`
|
||||||
(Gen n x) = switch n {
|
(Gen n x) = switch n {
|
||||||
0: (Tree/Leaf x)
|
0: (Tree/Leaf x)
|
||||||
_: (Tree/Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
|
_: (Tree/Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
|
||||||
}
|
}
|
||||||
|
|
||||||
// Reverses a tree
|
# Reverses a tree
|
||||||
(Rev (Tree/Leaf x)) = (Tree/Leaf x)
|
(Rev (Tree/Leaf x)) = (Tree/Leaf x)
|
||||||
(Rev (Tree/Both a b)) = (Tree/Both (Rev b) (Rev a))
|
(Rev (Tree/Both a b)) = (Tree/Both (Rev b) (Rev a))
|
||||||
|
|
||||||
// Sums a tree
|
# Sums a tree
|
||||||
(Sum (Tree/Leaf x)) = x
|
(Sum (Tree/Leaf x)) = x
|
||||||
(Sum (Tree/Both a b)) = (+ (Sum a) (Sum b))
|
(Sum (Tree/Both a b)) = (+ (Sum a) (Sum b))
|
||||||
|
|
||||||
|
@ -1,25 +1,25 @@
|
|||||||
// We want the nested calls in foo to be compiled as redexes written in outer to inner order
|
# We want the nested calls in foo to be compiled as redexes written in outer to inner order
|
||||||
// So they should compile to: @foo = root_tree & a ~ ... & b ~ ... & c ~ ...
|
# So they should compile to: @foo = root_tree & a ~ ... & b ~ ... & c ~ ...
|
||||||
foo = @x (a (b (c x)))
|
foo = @x (a (b (c x)))
|
||||||
foo2 = (a (b (c 0)))
|
foo2 = (a (b (c 0)))
|
||||||
|
|
||||||
bar = (a (b (c 0) (c (d 1))) (b (c (d 2)) (c 3)))
|
bar = (a (b (c 0) (c (d 1))) (b (c (d 2)) (c 3)))
|
||||||
//bar = (
|
#bar = (
|
||||||
// (
|
# (
|
||||||
// a
|
# a
|
||||||
// (
|
# (
|
||||||
// (b (c 0))
|
# (b (c 0))
|
||||||
// (c (d 1))
|
# (c (d 1))
|
||||||
// )
|
# )
|
||||||
// )
|
# )
|
||||||
// (
|
# (
|
||||||
// (
|
# (
|
||||||
// b
|
# b
|
||||||
// (c (d 2))
|
# (c (d 2))
|
||||||
// )
|
# )
|
||||||
// (c 3)
|
# (c 3)
|
||||||
// )
|
# )
|
||||||
//)
|
#)
|
||||||
|
|
||||||
a = @x x
|
a = @x x
|
||||||
b = @x x
|
b = @x x
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Test manual linearization of a use term
|
# Test manual linearization of a use term
|
||||||
main =
|
main =
|
||||||
@x @y use z = (x y); @a @b @c switch a with z {
|
@x @y use z = (x y); @a @b @c switch a with z {
|
||||||
0: z
|
0: z
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// To check that flattening works with Era patterns.
|
# To check that flattening works with Era patterns.
|
||||||
(Fn1 (*,(a,*)) *) = a
|
(Fn1 (*,(a,*)) *) = a
|
||||||
|
|
||||||
(Fn2 (*,(*,(a,*)))) = a
|
(Fn2 (*,(*,(a,*)))) = a
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Test that we don't mess up with that unscoped lambda/var
|
# Test that we don't mess up with that unscoped lambda/var
|
||||||
data bool = T | F
|
data bool = T | F
|
||||||
|
|
||||||
main = @x match x {
|
main = @x match x {
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
// Given a match/switch term preceded by a sequence of terms with binds (lambda, let, use, etc),
|
# Given a match/switch term preceded by a sequence of terms with binds (lambda, let, use, etc),
|
||||||
// by default we linearize all bindings up to the first one that appears in the match "header".
|
# by default we linearize all bindings up to the first one that appears in the match "header".
|
||||||
|
|
||||||
switch_linearization =
|
switch_linearization =
|
||||||
@a
|
@a
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Testing various forms of pattern matching
|
# Testing various forms of pattern matching
|
||||||
data Result_ = (Ok val) | (Err err)
|
data Result_ = (Ok val) | (Err err)
|
||||||
|
|
||||||
Parse state (String/Cons '(' xs) = (Result_/Ok ('(', xs, state))
|
Parse state (String/Cons '(' xs) = (Result_/Ok ('(', xs, state))
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Impossible to extract/linearize so that it does not hang when running
|
# Impossible to extract/linearize so that it does not hang when running
|
||||||
Foo = @x (x ({Foo @$unscoped *} *) $unscoped)
|
Foo = @x (x ({Foo @$unscoped *} *) $unscoped)
|
||||||
|
|
||||||
main = (Foo *)
|
main = (Foo *)
|
||||||
|
@ -22,8 +22,8 @@ def inc(n):
|
|||||||
n += 1;
|
n += 1;
|
||||||
return n;
|
return n;
|
||||||
|
|
||||||
//def inc_list(list):
|
#def inc_list(list):
|
||||||
// return [x+1 for x in list];
|
# return [x+1 for x in list];
|
||||||
|
|
||||||
def lam():
|
def lam():
|
||||||
return lambda x, y: x;
|
return lambda x, y: x;
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// should return (a+b+c) * 2^depth
|
# should return (a+b+c) * 2^depth
|
||||||
data Tree = (node ~lft ~rgt) | (leaf val)
|
data Tree = (node ~lft ~rgt) | (leaf val)
|
||||||
|
|
||||||
main =
|
main =
|
||||||
|
@ -1,44 +1,44 @@
|
|||||||
data Tree = (Leaf a) | (Both a b)
|
data Tree = (Leaf a) | (Both a b)
|
||||||
data Error = Err
|
data Error = Err
|
||||||
|
|
||||||
// Atomic Swapper
|
# Atomic Swapper
|
||||||
(Swap n a b) = switch n {
|
(Swap n a b) = switch n {
|
||||||
0: (Tree/Both a b)
|
0: (Tree/Both a b)
|
||||||
_: (Tree/Both b a)
|
_: (Tree/Both b a)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Swaps distant values in parallel; corresponds to a Red Box
|
# Swaps distant values in parallel; corresponds to a Red Box
|
||||||
(Warp s (Tree/Leaf a) (Tree/Leaf b)) = (Swap (^ (> a b) s) (Tree/Leaf a) (Tree/Leaf b))
|
(Warp s (Tree/Leaf a) (Tree/Leaf b)) = (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/Both a b) (Tree/Both c d)) = (Join (Warp s a c) (Warp s b d))
|
||||||
(Warp s a b) = Error/Err
|
(Warp s a b) = Error/Err
|
||||||
|
|
||||||
// Rebuilds the warped tree in the original order
|
# Rebuilds the warped tree in the original order
|
||||||
(Join (Tree/Both a b) (Tree/Both c d)) = (Tree/Both (Tree/Both a c) (Tree/Both b d))
|
(Join (Tree/Both a b) (Tree/Both c d)) = (Tree/Both (Tree/Both a c) (Tree/Both b d))
|
||||||
(Join a b) = Error/Err
|
(Join a b) = Error/Err
|
||||||
|
|
||||||
// Recursively warps each sub-tree; corresponds to a Blue/Green Box
|
# Recursively warps each sub-tree; corresponds to a Blue/Green Box
|
||||||
(Flow s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Flow s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Flow s (Tree/Both a b)) = (Down s (Warp s a b))
|
(Flow s (Tree/Both a b)) = (Down s (Warp s a b))
|
||||||
|
|
||||||
// Propagates Flow downwards
|
# Propagates Flow downwards
|
||||||
(Down s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Down s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Down s (Tree/Both a b)) = (Tree/Both (Flow s a) (Flow s b))
|
(Down s (Tree/Both a b)) = (Tree/Both (Flow s a) (Flow s b))
|
||||||
|
|
||||||
// Bitonic Sort
|
# Bitonic Sort
|
||||||
(Sort s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Sort s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Sort s (Tree/Both a b)) = (Flow s (Tree/Both (Sort 0 a) (Sort 1 b)))
|
(Sort s (Tree/Both a b)) = (Flow s (Tree/Both (Sort 0 a) (Sort 1 b)))
|
||||||
|
|
||||||
// Generates a tree of depth `n`
|
# Generates a tree of depth `n`
|
||||||
(Gen n x) = switch n {
|
(Gen n x) = switch n {
|
||||||
0: (Tree/Leaf x)
|
0: (Tree/Leaf x)
|
||||||
_: (Tree/Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
|
_: (Tree/Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
|
||||||
}
|
}
|
||||||
|
|
||||||
// Reverses a tree
|
# Reverses a tree
|
||||||
(Rev (Tree/Leaf x)) = (Tree/Leaf x)
|
(Rev (Tree/Leaf x)) = (Tree/Leaf x)
|
||||||
(Rev (Tree/Both a b)) = (Tree/Both (Rev b) (Rev a))
|
(Rev (Tree/Both a b)) = (Tree/Both (Rev b) (Rev a))
|
||||||
|
|
||||||
// Sums a tree
|
# Sums a tree
|
||||||
(Sum (Tree/Leaf x)) = x
|
(Sum (Tree/Leaf x)) = x
|
||||||
(Sum (Tree/Both a b)) = (+ (Sum a) (Sum b))
|
(Sum (Tree/Both a b)) = (+ (Sum a) (Sum b))
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// data Tree = (Leaf x) | (Node x0 x1)
|
# data Tree = (Leaf x) | (Node x0 x1)
|
||||||
Leaf = λx λl λn (l x)
|
Leaf = λx λl λn (l x)
|
||||||
Node = λx0 λx1 λl λn (n x0 x1)
|
Node = λx0 λx1 λl λn (n x0 x1)
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Test that branching statements can end with an assignment
|
# Test that branching statements can end with an assignment
|
||||||
type Tree:
|
type Tree:
|
||||||
node { val, ~lft, ~rgt }
|
node { val, ~lft, ~rgt }
|
||||||
leaf
|
leaf
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Mixed contents in a `do` block should still work.
|
# Mixed contents in a `do` block should still work.
|
||||||
|
|
||||||
Result/bind r nxt = match r {
|
Result/bind r nxt = match r {
|
||||||
Result/Ok: (nxt r.val)
|
Result/Ok: (nxt r.val)
|
||||||
|
@ -1,36 +1,36 @@
|
|||||||
// Write definitions like this
|
# Write definitions like this
|
||||||
(Def1) = ((λa a) (λb b))
|
(Def1) = ((λa a) (λb b))
|
||||||
|
|
||||||
// You can call a definition by just referencing its name
|
# You can call a definition by just referencing its name
|
||||||
// It will be substituted in place of the reference
|
# It will be substituted in place of the reference
|
||||||
(Def2) = ((λa a) Def1)
|
(Def2) = ((λa a) Def1)
|
||||||
|
|
||||||
// Definitions and variables can have names in upper and lower case and contain numbers
|
# Definitions and variables can have names in upper and lower case and contain numbers
|
||||||
// Names defined in a more inner position shadow names in an outer position
|
# Names defined in a more inner position shadow names in an outer position
|
||||||
(def3) = ((λDef1 Def1) (λx λx x))
|
(def3) = ((λDef1 Def1) (λx λx x))
|
||||||
|
|
||||||
// The language is affine, but if you use a variable more than once the compiler inserts duplications for you
|
# The language is affine, but if you use a variable more than once the compiler inserts duplications for you
|
||||||
// Of course you can always do them manually
|
# Of course you can always do them manually
|
||||||
(def4) = λz let {z1 z2} = z; (z1 ((λx (x x x x x)) z2))
|
(def4) = λz let {z1 z2} = z; (z1 ((λx (x x x x x)) z2))
|
||||||
|
|
||||||
// You can use machine numbers and some native numeric operations
|
# You can use machine numbers and some native numeric operations
|
||||||
// Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
|
# Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
|
||||||
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
|
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
|
||||||
|
|
||||||
// You can use numbers on the native match expression
|
# You can use numbers on the native match expression
|
||||||
// The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1
|
# The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1
|
||||||
(Num.pred) = λn
|
(Num.pred) = λn
|
||||||
switch n {
|
switch n {
|
||||||
0: 0
|
0: 0
|
||||||
_: n-1
|
_: n-1
|
||||||
}
|
}
|
||||||
|
|
||||||
// Write new data types like this
|
# Write new data types like this
|
||||||
data Option = (Some val) | None
|
data Option = (Some val) | None
|
||||||
data Bool = True | False
|
data Bool = True | False
|
||||||
|
|
||||||
// You can have pattern matching on definitions
|
# You can have pattern matching on definitions
|
||||||
// Use `*` to ignore a pattern
|
# Use `*` to ignore a pattern
|
||||||
(Option.unwrap_or (Option/Some val) *) = val
|
(Option.unwrap_or (Option/Some val) *) = val
|
||||||
(Option.unwrap_or Option/None or) = or
|
(Option.unwrap_or Option/None or) = or
|
||||||
|
|
||||||
@ -38,39 +38,39 @@ data Bool = True | False
|
|||||||
(Bool.or * Bool/True) = Bool/True
|
(Bool.or * Bool/True) = Bool/True
|
||||||
(Bool.or * *) = Bool/False
|
(Bool.or * *) = Bool/False
|
||||||
|
|
||||||
// Or using a match expression
|
# Or using a match expression
|
||||||
(Bool.not) = λbool
|
(Bool.not) = λbool
|
||||||
match bool {
|
match bool {
|
||||||
Bool/True: Bool/False
|
Bool/True: Bool/False
|
||||||
Bool/False: Bool/True
|
Bool/False: Bool/True
|
||||||
}
|
}
|
||||||
|
|
||||||
// Data types can store values
|
# Data types can store values
|
||||||
data Boxed = (Box val)
|
data Boxed = (Box val)
|
||||||
|
|
||||||
// Types with only one constructor can be destructured using `let` or a single matching definition
|
# Types with only one constructor can be destructured using `let` or a single matching definition
|
||||||
(Box.map (Boxed/Box val) f) = (Boxed/Box (f val))
|
(Box.map (Boxed/Box val) f) = (Boxed/Box (f val))
|
||||||
|
|
||||||
(Box.unbox) = λbox match box {
|
(Box.unbox) = λbox match box {
|
||||||
Boxed/Box: box.val
|
Boxed/Box: box.val
|
||||||
}
|
}
|
||||||
|
|
||||||
// Use tuples to store two values together without needing to create a new data type
|
# Use tuples to store two values together without needing to create a new data type
|
||||||
(Tuple.new fst snd) =
|
(Tuple.new fst snd) =
|
||||||
let pair = (fst, snd)
|
let pair = (fst, snd)
|
||||||
pair
|
pair
|
||||||
|
|
||||||
// Then you can destructure it inside the definition or using `let`
|
# Then you can destructure it inside the definition or using `let`
|
||||||
(Tuple.fst (fst, snd)) = fst
|
(Tuple.fst (fst, snd)) = fst
|
||||||
|
|
||||||
(Tuple.snd) = λpair
|
(Tuple.snd) = λpair
|
||||||
let (fst, snd) = pair
|
let (fst, snd) = pair
|
||||||
snd
|
snd
|
||||||
|
|
||||||
// All files must have a main definition to be run.
|
# All files must have a main definition to be run.
|
||||||
// You can execute a program in HVM with "cargo run -- run <path to file>"
|
# 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
|
# Other options are "check" (the default mode) to just see if the file is well formed
|
||||||
// and "compile" to output hvm-core code.
|
# and "compile" to output hvm-core code.
|
||||||
(main) =
|
(main) =
|
||||||
let tup = (Tuple.new Option/None (Num.pred 5))
|
let tup = (Tuple.new Option/None (Num.pred 5))
|
||||||
|
|
||||||
|
@ -1,2 +1,2 @@
|
|||||||
// Requires different labels in the two duplications of f
|
# Requires different labels in the two duplications of f
|
||||||
main = ((λfλx (f (f x))) (λfλx (f (f x))))
|
main = ((λfλx (f (f x))) (λfλx (f (f x))))
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// We expect the lambda 'p' from the match to be extracted which allows this recursive func
|
# We expect the lambda 'p' from the match to be extracted which allows this recursive func
|
||||||
val = λn (switch n { 0: valZ; _: (valS n-1) })
|
val = λn (switch n { 0: valZ; _: (valS n-1) })
|
||||||
valZ = 0
|
valZ = 0
|
||||||
valS = λp (val p)
|
valS = λp (val p)
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Vectorizes if the adts are encoded with tagged scott encoding
|
# Vectorizes if the adts are encoded with tagged scott encoding
|
||||||
data Box = (New a)
|
data Box = (New a)
|
||||||
data Bool = T | F
|
data Bool = T | F
|
||||||
data List_ = (Cons x xs) | Nil
|
data List_ = (Cons x xs) | Nil
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
def main:
|
def main:
|
||||||
y = 1
|
y = 1
|
||||||
fold x = [0 0 0] with y:
|
fold x = [0 0 0] with y:
|
||||||
case List/cons:
|
case List/Cons:
|
||||||
return List/cons(x.head + y x.tail(y + 1))
|
return List/Cons(x.head + y x.tail(y + 1))
|
||||||
case List/nil:
|
case List/Nil:
|
||||||
return List/nil
|
return List/Nil
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
//WARNING: unsolved metas.
|
#WARNING: unsolved metas.
|
||||||
//WARNING: unsolved metas.
|
#WARNING: unsolved metas.
|
||||||
_Char = 0
|
_Char = 0
|
||||||
_List = λ_T 0
|
_List = λ_T 0
|
||||||
_List.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
|
_List.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Testing various forms of pattern matching
|
# Testing various forms of pattern matching
|
||||||
data Result_ = (Ok val) | (Err err)
|
data Result_ = (Ok val) | (Err err)
|
||||||
|
|
||||||
Parse state (String/Cons '{' xs) = (Result_/Ok ('{', xs, state))
|
Parse state (String/Cons '{' xs) = (Result_/Ok ('{', xs, state))
|
||||||
|
@ -1,18 +1,18 @@
|
|||||||
// A cool trick involving HVM's scopeless lambdas is linear qs:
|
# A cool trick involving HVM's scopeless lambdas is linear qs:
|
||||||
|
|
||||||
// Qnew : Queue a
|
# Qnew : Queue a
|
||||||
Qnew = λx x
|
Qnew = λx x
|
||||||
|
|
||||||
// Qadd : a -> Queue a -> Queue a
|
# Qadd : a -> Queue a -> Queue a
|
||||||
Qadd = λx λq λk (q λc (c x k))
|
Qadd = λx λq λk (q λc (c x k))
|
||||||
|
|
||||||
// Qrem : Queue a -> Pair a (Queue a)
|
# Qrem : Queue a -> Pair a (Queue a)
|
||||||
Qrem = λq (q $k λx λxs λp(p x λ$k xs))
|
Qrem = λq (q $k λx λxs λp(p x λ$k xs))
|
||||||
|
|
||||||
Nil = λc λn n
|
Nil = λc λn n
|
||||||
Cons = λh λt λc λn (c h t)
|
Cons = λh λt λc λn (c h t)
|
||||||
|
|
||||||
// Output: [1, 2, 3]
|
# Output: [1, 2, 3]
|
||||||
main =
|
main =
|
||||||
let q = Qnew
|
let q = Qnew
|
||||||
let q = ((Qadd) 1 q)
|
let q = ((Qadd) 1 q)
|
||||||
|
@ -6,15 +6,15 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
_: (Map_/Both b a)
|
_: (Map_/Both b a)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Sort : Arr -> Arr
|
# Sort : Arr -> Arr
|
||||||
(Sort t) = (ToArr 0 (ToMap t))
|
(Sort t) = (ToArr 0 (ToMap t))
|
||||||
|
|
||||||
// ToMap : Arr -> Map
|
# ToMap : Arr -> Map
|
||||||
(ToMap Arr/Null) = Map_/Free
|
(ToMap Arr/Null) = Map_/Free
|
||||||
(ToMap (Arr/Leaf a)) = (Radix a)
|
(ToMap (Arr/Leaf a)) = (Radix a)
|
||||||
(ToMap (Arr/Node a b)) = (Merge (ToMap a) (ToMap b))
|
(ToMap (Arr/Node a b)) = (Merge (ToMap a) (ToMap b))
|
||||||
|
|
||||||
// ToArr : U60 -> Map -> Arr
|
# ToArr : U60 -> Map -> Arr
|
||||||
(ToArr x Map_/Free) = Arr/Null
|
(ToArr x Map_/Free) = Arr/Null
|
||||||
(ToArr x Map_/Used) = (Arr/Leaf x)
|
(ToArr x Map_/Used) = (Arr/Leaf x)
|
||||||
(ToArr x (Map_/Both a b)) =
|
(ToArr x (Map_/Both a b)) =
|
||||||
@ -22,7 +22,7 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
let b = (ToArr (+ (* x 2) 1) b)
|
let b = (ToArr (+ (* x 2) 1) b)
|
||||||
(Arr/Node a b)
|
(Arr/Node a b)
|
||||||
|
|
||||||
// Merge : Map -> Map -> Map
|
# Merge : Map -> Map -> Map
|
||||||
(Merge Map_/Free Map_/Free) = Map_/Free
|
(Merge Map_/Free Map_/Free) = Map_/Free
|
||||||
(Merge Map_/Free Map_/Used) = Map_/Used
|
(Merge Map_/Free Map_/Used) = Map_/Used
|
||||||
(Merge Map_/Used Map_/Free) = Map_/Used
|
(Merge Map_/Used Map_/Free) = Map_/Used
|
||||||
@ -33,7 +33,7 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
(Merge (Map_/Both a b) Map_/Used) = *
|
(Merge (Map_/Both a b) Map_/Used) = *
|
||||||
(Merge Map_/Used (Map_/Both a b)) = *
|
(Merge Map_/Used (Map_/Both a b)) = *
|
||||||
|
|
||||||
// Radix : U60 -> Map
|
# Radix : U60 -> Map
|
||||||
(Radix n) =
|
(Radix n) =
|
||||||
let r = Map_/Used
|
let r = Map_/Used
|
||||||
let r = (Swap (& n 1) r Map_/Free)
|
let r = (Swap (& n 1) r Map_/Free)
|
||||||
@ -75,17 +75,17 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
r
|
r
|
||||||
|
|
||||||
|
|
||||||
// Reverse : Arr -> Arr
|
# Reverse : Arr -> Arr
|
||||||
(Reverse Arr/Null) = Arr/Null
|
(Reverse Arr/Null) = Arr/Null
|
||||||
(Reverse (Arr/Leaf a)) = (Arr/Leaf a)
|
(Reverse (Arr/Leaf a)) = (Arr/Leaf a)
|
||||||
(Reverse (Arr/Node a b)) = (Arr/Node (Reverse b) (Reverse a))
|
(Reverse (Arr/Node a b)) = (Arr/Node (Reverse b) (Reverse a))
|
||||||
|
|
||||||
// Sum : Arr -> U60
|
# Sum : Arr -> U60
|
||||||
(Sum Arr/Null) = 0
|
(Sum Arr/Null) = 0
|
||||||
(Sum (Arr/Leaf x)) = x
|
(Sum (Arr/Leaf x)) = x
|
||||||
(Sum (Arr/Node a b)) = (+ (Sum a) (Sum b))
|
(Sum (Arr/Node a b)) = (+ (Sum a) (Sum b))
|
||||||
|
|
||||||
// Gen : U60 -> Arr
|
# Gen : U60 -> Arr
|
||||||
(Gen n) = (Gen.go n 0)
|
(Gen n) = (Gen.go n 0)
|
||||||
(Gen.go n x) = switch n {
|
(Gen.go n x) = switch n {
|
||||||
0: (Arr/Leaf x)
|
0: (Arr/Leaf x)
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Check that the ctr in the middle are interpreted correctly
|
# Check that the ctr in the middle are interpreted correctly
|
||||||
data tup = (pair a b)
|
data tup = (pair a b)
|
||||||
|
|
||||||
main = (List/Cons
|
main = (List/Cons
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Tests that `(Foo 0)` is correctly extracted as a combinator, otherwise the file would hang when running
|
# Tests that `(Foo 0)` is correctly extracted as a combinator, otherwise the file would hang when running
|
||||||
Foo = @x (x (Foo 0) @y (Foo y))
|
Foo = @x (x (Foo 0) @y (Foo y))
|
||||||
|
|
||||||
main = (Foo 0)
|
main = (Foo 0)
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Tests that `({Foo @* a} 9)` is correctly extracted as a combinator, otherwise the file would hang when running
|
# Tests that `({Foo @* a} 9)` is correctly extracted as a combinator, otherwise the file would hang when running
|
||||||
Foo = @a switch a {
|
Foo = @a switch a {
|
||||||
0: (#a {Foo @* a} 9);
|
0: (#a {Foo @* a} 9);
|
||||||
_: a-1
|
_: a-1
|
||||||
|
@ -3,7 +3,7 @@
|
|||||||
(StrGo 0 str) = str
|
(StrGo 0 str) = str
|
||||||
(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
|
(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
|
||||||
|
|
||||||
// Old str encoding
|
# Old str encoding
|
||||||
Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))
|
Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))
|
||||||
|
|
||||||
main = (StrInc Hello)
|
main = (StrInc Hello)
|
||||||
|
@ -3,7 +3,7 @@
|
|||||||
(StrGo 0 (head, tail)) = (head, tail)
|
(StrGo 0 (head, tail)) = (head, tail)
|
||||||
(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
|
(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
|
||||||
|
|
||||||
// Old str encoding
|
# Old str encoding
|
||||||
Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))
|
Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))
|
||||||
|
|
||||||
main = (StrInc Hello)
|
main = (StrInc Hello)
|
||||||
|
@ -1,6 +1,6 @@
|
|||||||
X = λx x
|
X = λx x
|
||||||
|
|
||||||
// This leaves (b1 X) with an ERA in the return, but the DUP is kept with an unused var
|
# This leaves (b1 X) with an ERA in the return, but the DUP is kept with an unused var
|
||||||
main = (
|
main = (
|
||||||
(λa λb let {b1 b2} = b; (a (b1 X) (b2 X)))
|
(λa λb let {b1 b2} = b; (a (b1 X) (b2 X)))
|
||||||
(λa λb b)
|
(λa λb b)
|
||||||
|
@ -1,44 +1,44 @@
|
|||||||
data Tree = (Leaf a) | (Both a b)
|
data Tree = (Leaf a) | (Both a b)
|
||||||
data Error = Err
|
data Error = Err
|
||||||
|
|
||||||
// Atomic Swapper
|
# Atomic Swapper
|
||||||
(Swap n a b) = switch n {
|
(Swap n a b) = switch n {
|
||||||
0: (Tree/Both a b)
|
0: (Tree/Both a b)
|
||||||
_: (Tree/Both b a)
|
_: (Tree/Both b a)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Swaps distant values in parallel; corresponds to a Red Box
|
# Swaps distant values in parallel; corresponds to a Red Box
|
||||||
(Warp s (Tree/Leaf a) (Tree/Leaf b)) = (Swap (^ (> a b) s) (Tree/Leaf a) (Tree/Leaf b))
|
(Warp s (Tree/Leaf a) (Tree/Leaf b)) = (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/Both a b) (Tree/Both c d)) = (Join (Warp s a c) (Warp s b d))
|
||||||
(Warp s a b) = Error/Err
|
(Warp s a b) = Error/Err
|
||||||
|
|
||||||
// Rebuilds the warped tree in the original order
|
# Rebuilds the warped tree in the original order
|
||||||
(Join (Tree/Both a b) (Tree/Both c d)) = (Tree/Both (Tree/Both a c) (Tree/Both b d))
|
(Join (Tree/Both a b) (Tree/Both c d)) = (Tree/Both (Tree/Both a c) (Tree/Both b d))
|
||||||
(Join a b) = Error/Err
|
(Join a b) = Error/Err
|
||||||
|
|
||||||
// Recursively warps each sub-tree; corresponds to a Blue/Green Box
|
# Recursively warps each sub-tree; corresponds to a Blue/Green Box
|
||||||
(Flow s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Flow s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Flow s (Tree/Both a b)) = (Down s (Warp s a b))
|
(Flow s (Tree/Both a b)) = (Down s (Warp s a b))
|
||||||
|
|
||||||
// Propagates Flow downwards
|
# Propagates Flow downwards
|
||||||
(Down s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Down s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Down s (Tree/Both a b)) = (Tree/Both (Flow s a) (Flow s b))
|
(Down s (Tree/Both a b)) = (Tree/Both (Flow s a) (Flow s b))
|
||||||
|
|
||||||
// Bitonic Sort
|
# Bitonic Sort
|
||||||
(Sort s (Tree/Leaf a)) = (Tree/Leaf a)
|
(Sort s (Tree/Leaf a)) = (Tree/Leaf a)
|
||||||
(Sort s (Tree/Both a b)) = (Flow s (Tree/Both (Sort 0 a) (Sort 1 b)))
|
(Sort s (Tree/Both a b)) = (Flow s (Tree/Both (Sort 0 a) (Sort 1 b)))
|
||||||
|
|
||||||
// Generates a tree of depth `n`
|
# Generates a tree of depth `n`
|
||||||
(Gen n x) = switch n {
|
(Gen n x) = switch n {
|
||||||
0: (Tree/Leaf x)
|
0: (Tree/Leaf x)
|
||||||
_: (Tree/Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
|
_: (Tree/Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
|
||||||
}
|
}
|
||||||
|
|
||||||
// Reverses a tree
|
# Reverses a tree
|
||||||
(Rev (Tree/Leaf x)) = (Tree/Leaf x)
|
(Rev (Tree/Leaf x)) = (Tree/Leaf x)
|
||||||
(Rev (Tree/Both a b)) = (Tree/Both (Rev b) (Rev a))
|
(Rev (Tree/Both a b)) = (Tree/Both (Rev b) (Rev a))
|
||||||
|
|
||||||
// Sums a tree
|
# Sums a tree
|
||||||
(Sum (Tree/Leaf x)) = x
|
(Sum (Tree/Leaf x)) = x
|
||||||
(Sum (Tree/Both a b)) = (+ (Sum a) (Sum b))
|
(Sum (Tree/Both a b)) = (+ (Sum a) (Sum b))
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// data Tree = (Leaf x) | (Node x0 x1)
|
# data Tree = (Leaf x) | (Node x0 x1)
|
||||||
Leaf = λx #Tree λl #Tree λn (l x)
|
Leaf = λx #Tree λl #Tree λn (l x)
|
||||||
Node = λx0 λx1 #Tree λl #Tree λn (n x0 x1)
|
Node = λx0 λx1 #Tree λl #Tree λn (n x0 x1)
|
||||||
|
|
||||||
|
@ -1,36 +1,36 @@
|
|||||||
// Write definitions like this
|
# Write definitions like this
|
||||||
(Def1) = ((λa a) (λb b))
|
(Def1) = ((λa a) (λb b))
|
||||||
|
|
||||||
// You can call a definition by just referencing its name
|
# You can call a definition by just referencing its name
|
||||||
// It will be substituted in place of the reference
|
# It will be substituted in place of the reference
|
||||||
(Def2) = ((λa a) Def1)
|
(Def2) = ((λa a) Def1)
|
||||||
|
|
||||||
// Definitions and variables can have names in upper and lower case and contain numbers
|
# Definitions and variables can have names in upper and lower case and contain numbers
|
||||||
// Names defined in a more inner position shadow names in an outer position
|
# Names defined in a more inner position shadow names in an outer position
|
||||||
(def3) = ((λDef1 Def1) (λx λx x))
|
(def3) = ((λDef1 Def1) (λx λx x))
|
||||||
|
|
||||||
// The language is affine, but if you use a variable more than once the compiler inserts duplications for you
|
# The language is affine, but if you use a variable more than once the compiler inserts duplications for you
|
||||||
// Of course you can always do them manually
|
# Of course you can always do them manually
|
||||||
(def4) = λz let {z1 z2} = z; (z1 ((λx (x x x x x)) z2))
|
(def4) = λz let {z1 z2} = z; (z1 ((λx (x x x x x)) z2))
|
||||||
|
|
||||||
// You can use machine numbers and some native numeric operations
|
# You can use machine numbers and some native numeric operations
|
||||||
// Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
|
# Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything
|
||||||
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
|
(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1))
|
||||||
|
|
||||||
// You can use numbers on the native match expression
|
# You can use numbers on the native match expression
|
||||||
// The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1
|
# The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1
|
||||||
(Num.pred) = λn
|
(Num.pred) = λn
|
||||||
switch n {
|
switch n {
|
||||||
0: 0
|
0: 0
|
||||||
_: n-1
|
_: n-1
|
||||||
}
|
}
|
||||||
|
|
||||||
// Write new data types like this
|
# Write new data types like this
|
||||||
data Option = (Some val) | None
|
data Option = (Some val) | None
|
||||||
data Bool = True | False
|
data Bool = True | False
|
||||||
|
|
||||||
// You can have pattern matching on definitions
|
# You can have pattern matching on definitions
|
||||||
// Use `*` to ignore a pattern
|
# Use `*` to ignore a pattern
|
||||||
(Option.unwrap_or (Option/Some val) *) = val
|
(Option.unwrap_or (Option/Some val) *) = val
|
||||||
(Option.unwrap_or Option/None or) = or
|
(Option.unwrap_or Option/None or) = or
|
||||||
|
|
||||||
@ -38,39 +38,39 @@ data Bool = True | False
|
|||||||
(Bool.or * Bool/True) = Bool/True
|
(Bool.or * Bool/True) = Bool/True
|
||||||
(Bool.or * *) = Bool/False
|
(Bool.or * *) = Bool/False
|
||||||
|
|
||||||
// Or using a match expression
|
# Or using a match expression
|
||||||
(Bool.not) = λbool
|
(Bool.not) = λbool
|
||||||
match bool {
|
match bool {
|
||||||
Bool/True: Bool/False
|
Bool/True: Bool/False
|
||||||
Bool/False: Bool/True
|
Bool/False: Bool/True
|
||||||
}
|
}
|
||||||
|
|
||||||
// Data types can store values
|
# Data types can store values
|
||||||
data Boxed = (Box val)
|
data Boxed = (Box val)
|
||||||
|
|
||||||
// Types with only one constructor can be destructured using `let` or a single matching definition
|
# Types with only one constructor can be destructured using `let` or a single matching definition
|
||||||
(Box.map (Boxed/Box val) f) = (Boxed/Box (f val))
|
(Box.map (Boxed/Box val) f) = (Boxed/Box (f val))
|
||||||
|
|
||||||
(Box.unbox) = λbox match box {
|
(Box.unbox) = λbox match box {
|
||||||
Boxed/Box: box.val
|
Boxed/Box: box.val
|
||||||
}
|
}
|
||||||
|
|
||||||
// Use tuples to store two values together without needing to create a new data type
|
# Use tuples to store two values together without needing to create a new data type
|
||||||
(Tuple.new fst snd) =
|
(Tuple.new fst snd) =
|
||||||
let pair = (fst, snd)
|
let pair = (fst, snd)
|
||||||
pair
|
pair
|
||||||
|
|
||||||
// Then you can destructure it inside the definition or using `let`
|
# Then you can destructure it inside the definition or using `let`
|
||||||
(Tuple.fst (fst, snd)) = fst
|
(Tuple.fst (fst, snd)) = fst
|
||||||
|
|
||||||
(Tuple.snd) = λpair
|
(Tuple.snd) = λpair
|
||||||
let (fst, snd) = pair
|
let (fst, snd) = pair
|
||||||
snd
|
snd
|
||||||
|
|
||||||
// All files must have a main definition to be run.
|
# All files must have a main definition to be run.
|
||||||
// You can execute a program in HVM with "cargo run -- run <path to file>"
|
# 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
|
# Other options are "check" (the default mode) to just see if the file is well formed
|
||||||
// and "compile" to output hvm-core code.
|
# and "compile" to output hvm-core code.
|
||||||
(main) =
|
(main) =
|
||||||
let tup = (Tuple.new None (Num.pred 5))
|
let tup = (Tuple.new None (Num.pred 5))
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// We expect the lambda 'p' from the match to be extracted which allows this recursive func
|
# We expect the lambda 'p' from the match to be extracted which allows this recursive func
|
||||||
val = λn (switch n { 0: valZ; _: (valS n-1) })
|
val = λn (switch n { 0: valZ; _: (valS n-1) })
|
||||||
valZ = 0
|
valZ = 0
|
||||||
valS = λp (val p)
|
valS = λp (val p)
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Vectorizes if the adts are encoded with tagged scott encoding
|
# Vectorizes if the adts are encoded with tagged scott encoding
|
||||||
data Box = (New a)
|
data Box = (New a)
|
||||||
data Bool = T | F
|
data Bool = T | F
|
||||||
data List_ = (Cons x xs) | Nil
|
data List_ = (Cons x xs) | Nil
|
||||||
|
@ -1,18 +1,18 @@
|
|||||||
// A cool trick involving HVM's scopeless lambdas is linear qs:
|
# A cool trick involving HVM's scopeless lambdas is linear qs:
|
||||||
|
|
||||||
// Qnew : Queue a
|
# Qnew : Queue a
|
||||||
Qnew = λx x
|
Qnew = λx x
|
||||||
|
|
||||||
// Qadd : a -> Queue a -> Queue a
|
# Qadd : a -> Queue a -> Queue a
|
||||||
Qadd = λx λq λk (q λc (c x k))
|
Qadd = λx λq λk (q λc (c x k))
|
||||||
|
|
||||||
// Qrem : Queue a -> Pair a (Queue a)
|
# Qrem : Queue a -> Pair a (Queue a)
|
||||||
Qrem = λq (q $k λx λxs λp(p x λ$k xs))
|
Qrem = λq (q $k λx λxs λp(p x λ$k xs))
|
||||||
|
|
||||||
Nil = λc λn n
|
Nil = λc λn n
|
||||||
Cons = λh λt λc λn (c h t)
|
Cons = λh λt λc λn (c h t)
|
||||||
|
|
||||||
// Output: [1, 2, 3]
|
# Output: [1, 2, 3]
|
||||||
main =
|
main =
|
||||||
let q = Qnew
|
let q = Qnew
|
||||||
let q = ((Qadd) 1 q)
|
let q = ((Qadd) 1 q)
|
||||||
|
@ -6,15 +6,15 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
_: (Map_/Both b a)
|
_: (Map_/Both b a)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Sort : Arr -> Arr
|
# Sort : Arr -> Arr
|
||||||
(Sort t) = (ToArr 0 (ToMap t))
|
(Sort t) = (ToArr 0 (ToMap t))
|
||||||
|
|
||||||
// ToMap : Arr -> Map
|
# ToMap : Arr -> Map
|
||||||
(ToMap Arr/Null) = Map_/Free
|
(ToMap Arr/Null) = Map_/Free
|
||||||
(ToMap (Arr/Leaf a)) = (Radix a)
|
(ToMap (Arr/Leaf a)) = (Radix a)
|
||||||
(ToMap (Arr/Node a b)) = (Merge (ToMap a) (ToMap b))
|
(ToMap (Arr/Node a b)) = (Merge (ToMap a) (ToMap b))
|
||||||
|
|
||||||
// ToArr : U60 -> Map -> Arr
|
# ToArr : U60 -> Map -> Arr
|
||||||
(ToArr x Map_/Free) = Arr/Null
|
(ToArr x Map_/Free) = Arr/Null
|
||||||
(ToArr x Map_/Used) = (Arr/Leaf x)
|
(ToArr x Map_/Used) = (Arr/Leaf x)
|
||||||
(ToArr x (Map_/Both a b)) =
|
(ToArr x (Map_/Both a b)) =
|
||||||
@ -22,7 +22,7 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
let b = (ToArr (+ (* x 2) 1) b)
|
let b = (ToArr (+ (* x 2) 1) b)
|
||||||
(Arr/Node a b)
|
(Arr/Node a b)
|
||||||
|
|
||||||
// Merge : Map -> Map -> Map
|
# Merge : Map -> Map -> Map
|
||||||
(Merge Map_/Free Map_/Free) = Map_/Free
|
(Merge Map_/Free Map_/Free) = Map_/Free
|
||||||
(Merge Map_/Free Map_/Used) = Map_/Used
|
(Merge Map_/Free Map_/Used) = Map_/Used
|
||||||
(Merge Map_/Used Map_/Free) = Map_/Used
|
(Merge Map_/Used Map_/Free) = Map_/Used
|
||||||
@ -33,7 +33,7 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
(Merge (Map_/Both a b) Map_/Used) = *
|
(Merge (Map_/Both a b) Map_/Used) = *
|
||||||
(Merge Map_/Used (Map_/Both a b)) = *
|
(Merge Map_/Used (Map_/Both a b)) = *
|
||||||
|
|
||||||
// Radix : U60 -> Map
|
# Radix : U60 -> Map
|
||||||
(Radix n) =
|
(Radix n) =
|
||||||
let r = Map_/Used
|
let r = Map_/Used
|
||||||
let r = (Swap (& n 1) r Map_/Free)
|
let r = (Swap (& n 1) r Map_/Free)
|
||||||
@ -75,17 +75,17 @@ data Arr = Null | (Leaf x) | (Node a b)
|
|||||||
r
|
r
|
||||||
|
|
||||||
|
|
||||||
// Reverse : Arr -> Arr
|
# Reverse : Arr -> Arr
|
||||||
(Reverse Arr/Null) = Arr/Null
|
(Reverse Arr/Null) = Arr/Null
|
||||||
(Reverse (Arr/Leaf a)) = (Arr/Leaf a)
|
(Reverse (Arr/Leaf a)) = (Arr/Leaf a)
|
||||||
(Reverse (Arr/Node a b)) = (Arr/Node (Reverse b) (Reverse a))
|
(Reverse (Arr/Node a b)) = (Arr/Node (Reverse b) (Reverse a))
|
||||||
|
|
||||||
// Sum : Arr -> U60
|
# Sum : Arr -> U60
|
||||||
(Sum Arr/Null) = 0
|
(Sum Arr/Null) = 0
|
||||||
(Sum (Arr/Leaf x)) = x
|
(Sum (Arr/Leaf x)) = x
|
||||||
(Sum (Arr/Node a b)) = (+ (Sum a) (Sum b))
|
(Sum (Arr/Node a b)) = (+ (Sum a) (Sum b))
|
||||||
|
|
||||||
// Gen : U60 -> Arr
|
# Gen : U60 -> Arr
|
||||||
(Gen n) = (Gen.go n 0)
|
(Gen n) = (Gen.go n 0)
|
||||||
(Gen.go n x) = switch n {
|
(Gen.go n x) = switch n {
|
||||||
0: (Arr/Leaf x)
|
0: (Arr/Leaf x)
|
||||||
|
@ -3,7 +3,7 @@
|
|||||||
(StrGo 0 str) = str
|
(StrGo 0 str) = str
|
||||||
(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
|
(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
|
||||||
|
|
||||||
// Old str encoding
|
# Old str encoding
|
||||||
Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))
|
Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))
|
||||||
|
|
||||||
main = (StrInc Hello)
|
main = (StrInc Hello)
|
||||||
|
@ -3,7 +3,7 @@
|
|||||||
(StrGo 0 (head, tail)) = (head, tail)
|
(StrGo 0 (head, tail)) = (head, tail)
|
||||||
(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
|
(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
|
||||||
|
|
||||||
// Old str encoding
|
# Old str encoding
|
||||||
Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))
|
Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))
|
||||||
|
|
||||||
main = (StrInc Hello)
|
main = (StrInc Hello)
|
||||||
|
@ -1,6 +1,6 @@
|
|||||||
X = λx x
|
X = λx x
|
||||||
|
|
||||||
// This leaves (b1 X) with an ERA in the return, but the DUP is kept with an unused var
|
# This leaves (b1 X) with an ERA in the return, but the DUP is kept with an unused var
|
||||||
main = (
|
main = (
|
||||||
(λa λb let {b1 b2} = b; (a (b1 X) (b2 X)))
|
(λa λb let {b1 b2} = b; (a (b1 X) (b2 X)))
|
||||||
(λa λb b)
|
(λa λb b)
|
||||||
|
@ -1,12 +1,12 @@
|
|||||||
// The test below should not trigger this warning:
|
# The test below should not trigger this warning:
|
||||||
//
|
#
|
||||||
// In definition 'f':
|
# In definition 'f':
|
||||||
// Definition is unused.
|
# Definition is unused.
|
||||||
// In definition 't':
|
# In definition 't':
|
||||||
// Definition is unused.
|
# Definition is unused.
|
||||||
//
|
#
|
||||||
// This was happening because the prune algorithm was just collecting constructors
|
# This was happening because the prune algorithm was just collecting constructors
|
||||||
// by searching for tags.
|
# by searching for tags.
|
||||||
|
|
||||||
data bool = t | f
|
data bool = t | f
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Should notice that the second rule is redundant, not create flattened rule for it and not forward the second argument.
|
# Should notice that the second rule is redundant, not create flattened rule for it and not forward the second argument.
|
||||||
data Boxed = (Box x)
|
data Boxed = (Box x)
|
||||||
|
|
||||||
(DoubleUnbox (Boxed/Box (Boxed/Box x)) *) = x
|
(DoubleUnbox (Boxed/Box (Boxed/Box x)) *) = x
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// We want to make sure that the default value is not mistakenly erased in the first level of flattening.
|
# We want to make sure that the default value is not mistakenly erased in the first level of flattening.
|
||||||
data Maybe = (Some x) | None
|
data Maybe = (Some x) | None
|
||||||
|
|
||||||
(DoubleUnwrap (Maybe/Some (Maybe/Some x)) *) = x
|
(DoubleUnwrap (Maybe/Some (Maybe/Some x)) *) = x
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// The flattened rule should only have 1 arg, for matching 'B'
|
# The flattened rule should only have 1 arg, for matching 'B'
|
||||||
data A_t = (A b)
|
data A_t = (A b)
|
||||||
data B_t = B
|
data B_t = B
|
||||||
|
|
||||||
|
@ -1,31 +1,31 @@
|
|||||||
// Testing linearization in different situations
|
# Testing linearization in different situations
|
||||||
data ConsList = (Cons h t) | Nil
|
data ConsList = (Cons h t) | Nil
|
||||||
|
|
||||||
// Auto linearized on strict mode
|
# Auto linearized on strict mode
|
||||||
A = @a @b @c switch a {
|
A = @a @b @c switch a {
|
||||||
0: (b c)
|
0: (b c)
|
||||||
_: (a-1 b c)
|
_: (a-1 b c)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Manually linearized
|
# Manually linearized
|
||||||
B = @a @b @c switch c with a b {
|
B = @a @b @c switch c with a b {
|
||||||
0: (a b)
|
0: (a b)
|
||||||
_: (a b c-1)
|
_: (a b c-1)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Not linearized
|
# Not linearized
|
||||||
C = @a @b @c switch c {
|
C = @a @b @c switch c {
|
||||||
0: (a b)
|
0: (a b)
|
||||||
_: (a b c-1)
|
_: (a b c-1)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Auto linearized, one arg not used
|
# Auto linearized, one arg not used
|
||||||
D = @a @b @c switch a {
|
D = @a @b @c switch a {
|
||||||
0: c
|
0: c
|
||||||
_: (a-1 c)
|
_: (a-1 c)
|
||||||
}
|
}
|
||||||
|
|
||||||
// Pattern matching defs linearize all arguments
|
# Pattern matching defs linearize all arguments
|
||||||
E (ConsList/Cons a b) (ConsList/Cons c d) = (a b c d)
|
E (ConsList/Cons a b) (ConsList/Cons c d) = (a b c d)
|
||||||
E a b = (a b)
|
E a b = (a b)
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
// Should not create flattened rules for the 2 bottom rules and should properly erase the first arg.
|
# Should not create flattened rules for the 2 bottom rules and should properly erase the first arg.
|
||||||
(Fn2 * (*, (*, a))) = a
|
(Fn2 * (*, (*, a))) = a
|
||||||
(Fn2 0 *) = 0
|
(Fn2 0 *) = 0
|
||||||
(Fn2 a *) = (- a 1)
|
(Fn2 a *) = (- a 1)
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/compile_file/360_no_scope.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/compile_file/360_no_scope.bend :
|
In tests/golden_tests/compile_file/360_no_scope.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m '='
|
||||||
[0m 4 | let[4m[31m [0m#x{#y($e, $f) #y($g, $h)} = #y(#x{$d $f}, #x{$e, $g})[0m
|
[1m- detected:[0m end of input
|
||||||
|
[0m 6 | [4m[31m [0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/compile_file_o_all/tagged_dup.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/compile_file_o_all/tagged_dup.bend :
|
In tests/golden_tests/compile_file_o_all/tagged_dup.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m '='
|
||||||
[0m 2 | let[4m[31m [0m#i {a b} = @x x;[0m
|
[1m- detected:[0m
|
||||||
|
[0m 4 | [4m[31ml[0met #i {e f} = @x x;[0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/compile_file_o_all/tagged_lam.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/compile_file_o_all/tagged_lam.bend :
|
In tests/golden_tests/compile_file_o_all/tagged_lam.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m term
|
||||||
[0m 1 | main =[4m[31m [0m#foo ((#foo @x (+ x 1), #foo @x (* x x)) 2)[0m
|
[1m- detected:[0m end of input
|
||||||
|
[0m 2 | [4m[31m [0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/compile_file_o_all/tagged_sup.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/compile_file_o_all/tagged_sup.bend :
|
In tests/golden_tests/compile_file_o_all/tagged_sup.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m top-level definition
|
||||||
[0m 1 | a =[4m[31m [0m#i {λx x λx x}[0m
|
[1m- detected:[0m
|
||||||
|
[0m 2 | b [4m[31m=[0m #i {λx x λx x}[0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/run_file/360_no_scope.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/run_file/360_no_scope.bend :
|
In tests/golden_tests/run_file/360_no_scope.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m '='
|
||||||
[0m 4 | let[4m[31m [0m#x{#y($e, $f) #y($g, $h)} = #y(#x{$d $f}, #x{$e, $g})[0m
|
[1m- detected:[0m end of input
|
||||||
|
[0m 6 | [4m[31m [0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/run_file/adt_match_wrong_tag.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/run_file/adt_match_wrong_tag.bend :
|
In tests/golden_tests/run_file/adt_match_wrong_tag.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m term
|
||||||
[0m 3 | main = λa[4m[31m [0m#Option (a #wrong_tag λb b *)[0m
|
[1m- detected:[0m end of input
|
||||||
|
[0m 4 | [4m[31m [0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/run_file/adt_wrong_tag.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/run_file/adt_wrong_tag.bend :
|
In tests/golden_tests/run_file/adt_wrong_tag.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m term
|
||||||
[0m 3 | main = (@a[4m[31m [0m#Option (a #wrong_tag @x x *)) [0m
|
[1m- detected:[0m end of input
|
||||||
|
[0m 4 | [4m[31m [0m
|
||||||
|
@ -2,4 +2,4 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/run_file/fold_with_state.bend
|
input_file: tests/golden_tests/run_file/fold_with_state.bend
|
||||||
---
|
---
|
||||||
λa λ* (a 1 λb λ* (b 2 λc λ* (c 3 List/nil)))
|
λa λ* (a 1 λb λ* (b 2 λc λ* (c 3 List/Nil)))
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/run_file/match_sup.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/run_file/match_sup.bend :
|
In tests/golden_tests/run_file/match_sup.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m term
|
||||||
[0m 2 | let k =[4m[31m [0m#a{0 1};[0m
|
[1m- detected:[0m end of input
|
||||||
|
[0m 7 | [4m[31m [0m
|
||||||
|
@ -2,4 +2,8 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/run_file/nat_add.bend
|
input_file: tests/golden_tests/run_file/nat_add.bend
|
||||||
---
|
---
|
||||||
λa λ* (a λb λ* (b λc λ* (c λd λ* (d λe λ* (e λf λ* (f λg λ* (g λh λ* (h λi λ* (i λj λ* (j λk λ* (k λl λ* (l λm λ* (m λn λ* (n λo λ* (o λp λ* (p λq λ* (q λr λ* (r λs λ* (s λt λ* (t λu λ* (u λv λ* (v λw λ* (w λx λ* (x λy λ* (y (Nat/Succ (Nat/Succ (Nat/Succ (Nat/Succ (Nat/Succ (Nat/Succ (Nat/Succ (Nat/Succ (Nat/Succ Nat/Zero))))))))))))))))))))))))))))))))))
|
[4m[1m[31mErrors:[0m
|
||||||
|
In tests/golden_tests/run_file/nat_add.bend :
|
||||||
|
[1m- expected:[0m term
|
||||||
|
[1m- detected:[0m end of input
|
||||||
|
[0m 5 | [4m[31m [0m
|
||||||
|
@ -2,4 +2,8 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/run_file/nat_add_num.bend
|
input_file: tests/golden_tests/run_file/nat_add_num.bend
|
||||||
---
|
---
|
||||||
λa λ* (a λb λ* (b λc λ* (c λd λ* (d 0))))
|
[4m[1m[31mErrors:[0m
|
||||||
|
In tests/golden_tests/run_file/nat_add_num.bend :
|
||||||
|
[1m- expected:[0m term
|
||||||
|
[1m- detected:[0m end of input
|
||||||
|
[0m 5 | [4m[31m [0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/run_file/recursive_combinator_nested.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/run_file/recursive_combinator_nested.bend :
|
In tests/golden_tests/run_file/recursive_combinator_nested.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m term
|
||||||
[0m 3 | 0: ([4m[31m#[0ma {Foo @* a} 9);[0m
|
[1m- detected:[0m
|
||||||
|
[0m 4 | _[4m[31m:[0m a-1[0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/run_file/str_inc.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/run_file/str_inc.bend :
|
In tests/golden_tests/run_file/str_inc.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m ')'
|
||||||
[0m 1 | (StrInc (len, buf)) = (len,[4m[31m [0m#str λx (StrGo len #str (buf x)))[0m
|
[1m- detected:[0m
|
||||||
|
[0m 3 | (StrGo 0 str) [4m[31m=[0m str[0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/run_file/str_inc_eta.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/run_file/str_inc_eta.bend :
|
In tests/golden_tests/run_file/str_inc_eta.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m ')'
|
||||||
[0m 1 | (StrInc (len, buf)) = (len,[4m[31m [0m#str λx (StrGo len #str (buf x)))[0m
|
[1m- detected:[0m
|
||||||
|
[0m 3 | (StrGo 0 (head, tail)) [4m[31m=[0m (head, tail)[0m
|
||||||
|
@ -4,5 +4,6 @@ input_file: tests/golden_tests/run_file/tagged_lam.bend
|
|||||||
---
|
---
|
||||||
[4m[1m[31mErrors:[0m
|
[4m[1m[31mErrors:[0m
|
||||||
In tests/golden_tests/run_file/tagged_lam.bend :
|
In tests/golden_tests/run_file/tagged_lam.bend :
|
||||||
Tagged terms not supported for hvm32.
|
[1m- expected:[0m term
|
||||||
[0m 1 | main =[4m[31m [0m#foo ((#foo @x (+ x 1), #foo @x (* x x)) 2)[0m
|
[1m- detected:[0m end of input
|
||||||
|
[0m 2 | [4m[31m [0m
|
||||||
|
Loading…
Reference in New Issue
Block a user