HigherOrderCO/Bend
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Bend.git synced 2024-09-11 11:56:54 +03:00
Code Issues Packages Projects Releases Wiki Activity

Update docs and examples for hvm32

Browse Source
This commit is contained in:
Nicolas Abril 2024-04-26 22:35:42 +02:00
parent 2cba162ded
commit f948c6106e
7 changed files with 6 additions and 270 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

140
docs/builtin-defs.md
View File

@ -1,140 +0,0 @@
# Builtin Definitions
HVM-lang includes some built-in definitions that can make certain tasks easier, such as debugging, benchmarking, etc. These definitions are "special", and can't be implemented using regular HVM code.
### On errors.
Some of the functions may error. `hvm-lang` defines a builtin `Result` ADT which looks like this:
```
data Result = (Ok val) | (Err val)
```
This allows hvm-lang to do basic error handling. Right now, `val` is meant to be opaque; `val`'s type is not stable and might change from one update to another.
## `HVM.log`
Reads back its first argument and displays it on stdout, then returns its second argument.
```rs
main = (HVM.log "Hi" "Hello world")
// Program output:
"Hi"
"Hello world"
```
This function can be very useful for debugging, however, it's somewhat limited. For example, `λx (HVM.log x 0)` won't readback correctly
```rs
main = λx(HVM.log x "Hello world")
// Program output:
Reached Root
<Invalid>
λ* 0
```
This will happen whenever there are free variables inside the logged term, or [scopeless lambdas](using-scopeless-lambdas.md) which bind variables that are used outside the logged term.
## `HVM.print`
This is very similar to `HVM.log`. However, it can only log strings. It prints these strings directly to stdout, without wrapping them in quotes or escaping them.
With `HVM.log`:
```rs
main = (HVM.log "Hi" "Hello world")
// Program output:
"Hi"
"Hello world"
```
However, with `HVM.print`:
```rs
main = (HVM.print "Hi" "Hello world")
// Program output:
Hi
"Hello world"
```
This can be very useful, for example, to print strings with newlines in multiple lines.
When the first argument is not a string `HVM.print` returns the second argument and no side effects are produced (In other words, it fails silently).
## `HVM.query`
`HVM.query` reads a line from standard input, and calls its argument with a `Result` that might contain a string containing the user's input. It expects the standard input to be valid utf-8.
Here's an example program using `HVM.query`
```rs
Join (String.nil) x = x
Join (String.cons head tail) x = (String.cons head (Join tail x))
main = (((HVM.print "What's your name?") HVM.query) λresult match result {
Result.ok: (HVM.print (Join "Hi, " (Join result.val "!")) *)
Result.err: result.val
})
```
This program also shows using the return value of `HVM.print` (which is the identity function) to block `HVM.query` from reducing too early. If we used a naive version of the program, which is this:
```rs
main = (HVM.print "What's your name?" (HVM.query λresult match result {
Result.ok: (HVM.print (Join "Hi, " (Join result.val "!")) *)
Result.err: result.val
}))
```
We would get asked our name after typing it in.
## `HVM.store`
`HVM.store` writes a string to a file, and calls its return value with a `Result` (the `Result`, if it's `Result.ok`, contains `ERA`).
Example:
```rs
main = (HVM.store "file.txt" "These are the file contents" λres match res {
Result.ok: "Return value of program"
Result.err: res.val
})
```
## `HVM.load`
`HVM.load`, given a filename, reads the file and passes a `Result` that might contain the contents of the file to its argument
```rs
Join (String.nil) x = x
Join (String.cons head tail) x = (String.cons head (Join tail x))
main = (HVM.load "file.txt" λres match res {
Result.ok: (HVM.print (Join "File contents: " res.val) "Program return value")
Result.err: res.val
})
```
## `HVM.exit`
`HVM.exit` terminates the processes with the status code determined by its argument.
```rs
main = (HVM.exit #42)
// Outputs nothing, but `hvml`'s status code will be 42.
```
On failure, it terminates the process with a -1 exit status code.
## `HVM.black_box`
`HVM.black_box` is simply the identity function, but it does not get [pre-reduced](compiler-options.md#pre-reduce). This makes it possible to prevent some redexes from getting pre-reduced.
Example without `HVM.black_box`
```rs
foo = (* 30 40)
// Compilation output
@foo = #1200
```
Example with `HVM.black-box`
```rs
foo = (* (HVM.black_box 30) 40) // This is normal form
// Compilation output
@foo = a & @HVM.black_box ~ (#30 <* #40 a>)
```

2
docs/compiler-options.md
View File

@ -89,7 +89,7 @@ main = (id also_id)
## Pre-reduce
Normalizes all functions except main, dereferencing definitions in active positions, and solving annihilations and commutations. It does not reduce [builtin definitions](builtin-defs.md), such as `HVM.log`.
Normalizes all functions except main, dereferencing definitions in active positions, and solving annihilations and commutations.
Example:
```rs

2
examples/callcc.hvm
View File

@ -9,7 +9,7 @@ CC.lang = λprogram
let garbage = $garbage; // Discard `$garbage`, which is the value returned by `callback`
(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`
(+ 10 (callcc λk(+ (k 42) 1729)))
)

6
examples/fusing_not.hvm
View File

@ -8,7 +8,5 @@ to_church n = switch n {
_: λf λx (f (to_church n-1 f x))
}
main =
let two = λf λx (f (f x))
let two_pow_512 = ((to_church 512) two) // Composition of church-encoded numbers is equivalent to exponentiation.
// Self-composes `not` 2^512 times and prints the result.
(two_pow_512 fusing_not) // try replacing this by not. Will it still work?
// Self-composes `not` 2^24 times and prints the result.
((to_church 0xFFFFFF) fusing_not) // try replacing this by not. Will it still work?

1
examples/hello_world.hvm
View File

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

4
examples/quick_sort.hvm
View File

@ -18,7 +18,7 @@ data Tree = Leaf | (Node l m r)
// Generates a random list
(Rnd 0 s) = (List.nil)
(Rnd n s) = (List.cons s (Rnd (- n 1) (% (+ (* s 1664525) 1013904223) 4294967296)))
(Rnd n s) = (List.cons s (Rnd (- n 1) (% (+ (* s 1664525) 1013904223) 4294967295)))
// Sums all elements in a concatenation tree
(Sum Leaf) = 0
@ -27,7 +27,7 @@ data Tree = Leaf | (Node l m r)
// Sorts and sums n random numbers
(Main) =
let n = 12
(Sum (Sort (Rnd (<< 1 n) 1)))
(Sum (Sort (Rnd (* 2 n) 1)))
// Use an argument from cli
// (Main n) = (Sum (Sort (Rnd (<< 1 n) 1)))

121
examples/sat_solver.hvm
View File

@ -1,121 +0,0 @@
// Bool/List constructors and functions
(Cons h t) = λcλn(c h (t c n))
Nil = λcλn(n)
T = λt λf t
F = λt λf f
(Id a) = a
(Not a) = λt λf (a f t)
(And a b) = (a λx(x) λx(F) b)
(Or a b) = (a λx(T) λx(x) b)
(Or3 a b c) = (Or a (Or b c))
// Pretty prints a bool
(Bool x) = (x 1 0)
// Converts a solution to a pretty-printed church-list singleton
(Log x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 xA xB xC xD xE xF x) = (x (Cons λt(t
(Bool x0) (Bool x1) (Bool x2) (Bool x3)
(Bool x4) (Bool x5) (Bool x6) (Bool x7)
(Bool x8) (Bool x9) (Bool xA) (Bool xB)
(Bool xC) (Bool xD) (Bool xE) (Bool xF)
) Nil) Nil)
// A random 3-SAT instance with 16 variables
(Foo x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 xA xB xC xD xE xF) =
(Log x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 xA xB xC xD xE xF
(And (Or3 xC x8 (Not xB))
(And (Or3 (Not xA) (Not x2) (Not x8))
(And (Or3 xB (Not x9) x4)
(And (Or3 xA x1 (Not x8))
(And (Or3 (Not x9) x0 x5)
(And (Or3 (Not x4) (Not x4) xD)
(And (Or3 (Not x1) (Not x4) xB)
(And (Or3 (Not x2) xE (Not xD))
(And (Or3 xD (Not x8) (Not x7))
(And (Or3 xD (Not x1) x7)
(And (Or3 (Not x8) x4 x8)
(And (Or3 x5 (Not x0) xC)
(And (Or3 x1 x0 (Not x3))
(And (Or3 x3 xE (Not xD))
(And (Or3 x9 (Not xC) (Not xB))
(And (Or3 x8 (Not xE) (Not x5))
(And (Or3 (Not x7) (Not x9) (Not xF))
(And (Or3 xF xB x2)
(And (Or3 (Not x2) (Not xE) (Not x7))
(And (Or3 (Not xE) x3 (Not x3))
(And (Or3 x3 (Not xF) x1)
(And (Or3 (Not x0) x0 xD)
(And (Or3 (Not x8) (Not x3) xC)
(And (Or3 xC (Not x1) x7)
(And (Or3 x2 (Not xE) (Not x0))
(And (Or3 x6 (Not x5) x1)
(And (Or3 (Not xC) x3 (Not x3))
(And (Or3 (Not x1) (Not xC) (Not x5))
(And (Or3 xB xA x6)
(And (Or3 xF x6 x9)
(And (Or3 (Not xF) x3 (Not x9))
(And (Or3 (Not xB) x1 x8)
(And (Or3 x9 (Not xE) xE)
(And (Or3 (Not xA) (Not x2) x2)
(And (Or3 x5 xE (Not x2))
(And (Or3 (Not xB) xC x2)
(And (Or3 x1 xB (Not x2))
(And (Or3 x8 (Not x6) (Not x7))
(And (Or3 xD x9 (Not xA))
(And (Or3 x0 x8 (Not x8))
(And (Or3 (Not xA) x9 (Not x0))
(And (Or3 (Not xE) (Not x7) (Not xC))
(And (Or3 x9 xC (Not xA))
(And (Or3 (Not x7) (Not xF) xD)
(And (Or3 x0 (Not x2) xD)
(And (Or3 xC (Not x9) (Not x0))
(And (Or3 (Not xA) x8 (Not x1))
(And (Or3 x4 x5 (Not xE))
(And (Or3 (Not x0) x5 (Not x7))
(And (Or3 (Not x1) (Not xC) xA)
(And (Or3 x0 xF x9)
(And (Or3 (Not xA) x3 (Not x2))
(And (Or3 (Not x7) (Not xF) x6)
(And (Or3 (Not x1) x4 (Not x5))
(And (Or3 xC (Not x8) x2)
(And (Or3 x4 x7 (Not x5))
(And (Or3 (Not x9) (Not x0) (Not xA))
(And (Or3 xC x1 (Not x2))
(And (Or3 xB xE (Not xB))
(And (Or3 xF x5 xA)
(And (Or3 (Not x6) xE x3)
(And (Or3 (Not xB) xB x1)
(And (Or3 (Not xF) x0 x7)
(Or3 xE (Not x3) (Not x2))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
// Collapsers (to retrieve solutions from superpositions) - credit to @Franchu
Join = λaλbλcλn(a c (b c n))
Col0 = λx let #A0{x0 x1} = x; (Join x0 x1)
Col1 = λx let #A1{x0 x1} = x; (Join x0 x1)
Col2 = λx let #A2{x0 x1} = x; (Join x0 x1)
Col3 = λx let #A3{x0 x1} = x; (Join x0 x1)
Col4 = λx let #A4{x0 x1} = x; (Join x0 x1)
Col5 = λx let #A5{x0 x1} = x; (Join x0 x1)
Col6 = λx let #A6{x0 x1} = x; (Join x0 x1)
Col7 = λx let #A7{x0 x1} = x; (Join x0 x1)
Col8 = λx let #A8{x0 x1} = x; (Join x0 x1)
Col9 = λx let #A9{x0 x1} = x; (Join x0 x1)
ColA = λx let #AA{x0 x1} = x; (Join x0 x1)
ColB = λx let #AB{x0 x1} = x; (Join x0 x1)
ColC = λx let #AC{x0 x1} = x; (Join x0 x1)
ColD = λx let #AD{x0 x1} = x; (Join x0 x1)
ColE = λx let #AE{x0 x1} = x; (Join x0 x1)
ColF = λx let #AF{x0 x1} = x; (Join x0 x1)
// Finds a solution by applying Foo to superposed inputs
Main =
(Col0 (Col1 (Col2 (Col3
(Col4 (Col5 (Col6 (Col7
(Col8 (Col9 (ColA (ColB
(ColC (ColD (ColE (ColF
(Foo
#A0{T F} #A1{T F} #A2{T F} #A3{T F}
#A4{T F} #A5{T F} #A6{T F} #A7{T F}
#A8{T F} #A9{T F} #AA{T F} #AB{T F}
#AC{T F} #AD{T F} #AE{T F} #AF{T F}
)))))))))))))))))