mirror of
https://github.com/HigherOrderCO/Bend.git
synced 2024-09-11 11:56:54 +03:00
Merge pull request #599 from HigherOrderCO/578-add-user-friendly-file-io-functions
#578 Add File IO utility functions
This commit is contained in:
commit
a0aa467b73
@ -17,6 +17,7 @@ and this project does not currently adhere to a particular versioning scheme.
|
||||
### Fixed
|
||||
|
||||
- Fix readback of numeric operations. ([#467][gh-467])
|
||||
- Propagate the "builtin" attribute of definitions when extracting functions from `bend` and `fold` syntax.
|
||||
|
||||
### Added
|
||||
|
||||
@ -26,6 +27,10 @@ and this project does not currently adhere to a particular versioning scheme.
|
||||
- Add `IO/sleep` builtin function to sleep for a given amount of seconds as a float. ([#581][gh-581])
|
||||
- Add primitive file IO functions `IO/FS/{read, write, seek, open, close}`. ([#573][gh-573])
|
||||
- Add encoding/decoding builtin functions `Bytes/{decode_utf8, decode_ascii} String/{encode_ascii, decode_ascii} Utf8/{decode_character, REPLACEMENT_CHARACTER}`. ([#580][gh-580])
|
||||
- Add `IO/print` function to print to stdout. ([#579][gh-579])
|
||||
- Add `IO/input` function to read a line of input from stdin. ([#579][gh-579])
|
||||
- Add file IO utilities `IO/FS/{read_file, write_file, read_line, read_to_end}`. ([#578][gh-578])
|
||||
- Add list utilities `List/{length, reverse, flatten, concat}`.
|
||||
- Add `elif` chains to functional syntax. ([#596][gh-596])
|
||||
|
||||
## [0.2.35] - 2024-06-06
|
||||
@ -350,6 +355,8 @@ and this project does not currently adhere to a particular versioning scheme.
|
||||
[gh-528]: https://github.com/HigherOrderCO/Bend/issues/528
|
||||
[gh-581]: https://github.com/HigherOrderCO/Bend/issues/581
|
||||
[gh-573]: https://github.com/HigherOrderCO/Bend/issues/573
|
||||
[gh-578]: https://github.com/HigherOrderCO/Bend/issues/578
|
||||
[gh-579]: https://github.com/HigherOrderCO/Bend/issues/579
|
||||
[gh-580]: https://github.com/HigherOrderCO/Bend/issues/580
|
||||
[gh-582]: https://github.com/HigherOrderCO/Bend/issues/582
|
||||
[gh-583]: https://github.com/HigherOrderCO/Bend/issues/583
|
||||
|
@ -38,6 +38,52 @@ A List of values can be written using `[ ]`, it can have multiple values inside,
|
||||
["This", "List", "Has", "Multiple", "Values"]
|
||||
```
|
||||
|
||||
### Functions
|
||||
|
||||
#### List/length
|
||||
|
||||
```python
|
||||
def List/length(list: [a]) -> (length: u24, list: [a])
|
||||
```
|
||||
|
||||
Returns a tuple containing the length and the list itself.
|
||||
|
||||
#### List/reverse
|
||||
|
||||
```python
|
||||
def List/reverse(list: [a]) -> [a]
|
||||
```
|
||||
|
||||
Reverses the elements of a list.
|
||||
|
||||
#### List/flatten
|
||||
|
||||
```python
|
||||
def List/flatten(list: [[a]]) -> [a]
|
||||
```
|
||||
|
||||
Returns a flattened list from a list of lists. Example:
|
||||
|
||||
```python
|
||||
List/flatten([[1], [2, 3], [4]])
|
||||
|
||||
# Result: [1, 2, 3, 4]
|
||||
```
|
||||
|
||||
#### List/concat
|
||||
|
||||
```python
|
||||
def List/concat(xs: [a], ys: [a]) -> [a]
|
||||
```
|
||||
|
||||
Appends two lists together. Example:
|
||||
|
||||
```python
|
||||
List/concat([1, 2], [4, 5])
|
||||
|
||||
# Result: [1, 2, 4, 5]
|
||||
```
|
||||
|
||||
## Tree
|
||||
|
||||
```python
|
||||
@ -266,6 +312,24 @@ The basic builtin IO functions are under development and will be stable in the n
|
||||
|
||||
Here is the current list of functions, but be aware that they may change in the near future.
|
||||
|
||||
### Printing
|
||||
|
||||
```python
|
||||
def IO/print(text)
|
||||
```
|
||||
|
||||
Prints the string `text` to the standard output, encoded with utf-8.
|
||||
|
||||
### Input
|
||||
|
||||
```python
|
||||
def IO/input() -> String
|
||||
```
|
||||
|
||||
Reads characters from the standard input until a newline is found.
|
||||
|
||||
Returns the read input as a String decoded with utf-8.
|
||||
|
||||
### File IO
|
||||
|
||||
#### File open
|
||||
@ -311,6 +375,25 @@ Reads `num_bytes` bytes from the file with the given `file` descriptor.
|
||||
|
||||
Returns a list of U24 with each element representing a byte read from the file.
|
||||
|
||||
```python
|
||||
def IO/FS/read_line(file)
|
||||
```
|
||||
Reads a line from the file with the given `file` descriptor.
|
||||
|
||||
Returns a list of U24 with each element representing a byte read from the file.
|
||||
|
||||
```python
|
||||
def IO/FS/read_until_end(file)
|
||||
```
|
||||
Reads until the end of the file with the given `file` descriptor.
|
||||
|
||||
Returns a list of U24 with each element representing a byte read from the file.
|
||||
|
||||
```python
|
||||
def IO/FS/read_file(path)
|
||||
```
|
||||
Reads an entire file with the given `path` and returns a list of U24 with each element representing a byte read from the file.
|
||||
|
||||
#### File write
|
||||
|
||||
```python
|
||||
@ -321,6 +404,12 @@ Writes `bytes`, a list of U24 with each element representing a byte, to the file
|
||||
|
||||
Returns nothing (`*`).
|
||||
|
||||
```python
|
||||
def IO/FS/write_file(path, bytes)
|
||||
```
|
||||
|
||||
Writes `bytes`, a list of U24 with each element representing a byte, as the entire content of the file with the given `path`.
|
||||
|
||||
#### File seek
|
||||
|
||||
```python
|
||||
@ -381,7 +470,7 @@ def to_i24(x: any number) -> i24
|
||||
|
||||
Casts any native number to an i24.
|
||||
|
||||
## Encoding functions
|
||||
## String encoding / decoding
|
||||
|
||||
### Bytes/decode_utf8
|
||||
|
||||
|
@ -1184,7 +1184,7 @@ The Tree literals `![]` and `!` are used to create values of the built-in type `
|
||||
The syntax above is desugared to:
|
||||
|
||||
```
|
||||
(Nat.succ (Nat.succ (Nat.succ List.nil)))
|
||||
(Nat/succ (Nat/succ (Nat/succ Nat/zero)))
|
||||
```
|
||||
|
||||
# Native HVM definitions
|
||||
|
@ -14,22 +14,21 @@
|
||||
# List clear:
|
||||
# List l -> list l
|
||||
# clears all elements from list l. This is equivalent to initializing an empty list.
|
||||
List/clear = @l
|
||||
[]
|
||||
clear = @l []
|
||||
|
||||
# List concat:
|
||||
# List l -> List l
|
||||
# combines two lists (l1, l2) from left to right.
|
||||
List/concat = @l1 @l2
|
||||
concat = @l1 @l2
|
||||
match l1 {
|
||||
List/Cons: (List/Cons l1.head (List/concat l1.tail l2))
|
||||
List/Cons: (List/Cons l1.head (concat l1.tail l2))
|
||||
List/Nil: l2
|
||||
}
|
||||
|
||||
# List add_front:
|
||||
# List l -> List l
|
||||
# adds a non-List element e to the front of list l.
|
||||
List/add_front = @l @e
|
||||
add_front = @l @e
|
||||
match l {
|
||||
List/Cons: (List/Cons e l)
|
||||
List/Nil: (List/Cons e List/Nil)
|
||||
@ -38,62 +37,62 @@ List/add_front = @l @e
|
||||
# List append (add_back):
|
||||
# List l -> List l
|
||||
# adds a non-list element e to the back of list l.
|
||||
List/append = @l @e
|
||||
(List/concat l (List/Cons e List/Nil))
|
||||
append = @l @e
|
||||
(concat l (List/Cons e List/Nil))
|
||||
|
||||
# list sum:
|
||||
# List l -> uint
|
||||
# returns the sum of all items in the list.
|
||||
List/sum = @l
|
||||
sum = @l
|
||||
match l {
|
||||
List/Cons: (+ l.head (List/sum l.tail))
|
||||
List/Cons: (+ l.head (sum l.tail))
|
||||
List/Nil: 0
|
||||
}
|
||||
|
||||
# List reverse:
|
||||
# List l -> List l
|
||||
# reverses the order of elements in list l.
|
||||
List/reverse/aux = @acc @l
|
||||
reverse.aux = @acc @l
|
||||
match l {
|
||||
List/Nil: acc
|
||||
List/Cons: (List/reverse/aux (List/Cons l.head acc) l.tail)
|
||||
List/Cons: (reverse.aux (List/Cons l.head acc) l.tail)
|
||||
}
|
||||
List/reverse = @l
|
||||
(List/reverse/aux [] l)
|
||||
reverse = @l
|
||||
(reverse.aux [] l)
|
||||
|
||||
# List length:
|
||||
# List l -> uint
|
||||
# returns the number of elements in list l.
|
||||
List/len = @l
|
||||
len = @l
|
||||
match l {
|
||||
List/Nil: 0
|
||||
List/Cons: (+ 1 (List/len l.tail))
|
||||
List/Cons: (+ 1 (len l.tail))
|
||||
}
|
||||
|
||||
# List count:
|
||||
# List l -> uint -> uint
|
||||
# returns the number of instances of Some s in list l.
|
||||
List/count/aux = @acc @l @s
|
||||
count.aux = @acc @l @s
|
||||
match l {
|
||||
List/Nil: acc
|
||||
List/Cons: use acc = switch (== l.head s) {
|
||||
0: acc;
|
||||
_: (+ acc 1);
|
||||
}
|
||||
(List/count/aux acc l.tail s)
|
||||
(count.aux acc l.tail s)
|
||||
}
|
||||
List/count = @l @s
|
||||
(List/count/aux 0 l s)
|
||||
count = @l @s
|
||||
(count.aux 0 l s)
|
||||
|
||||
# List index:
|
||||
# List l -> Some s
|
||||
# returns the value of a specific list index i, or * if the index doesn't exist.
|
||||
List/index = @l @i
|
||||
index = @l @i
|
||||
match l {
|
||||
List/Cons:
|
||||
switch i {
|
||||
0: l.head
|
||||
_: (List/index l.tail (i-1))
|
||||
_: (index l.tail (i-1))
|
||||
}
|
||||
List/Nil: *
|
||||
}
|
||||
@ -101,7 +100,7 @@ List/index = @l @i
|
||||
# List head:
|
||||
# List l -> Some s
|
||||
# returns the first item in the list, or [] if the list is empty.
|
||||
List/head = @l
|
||||
head = @l
|
||||
match l {
|
||||
List/Cons: l.head
|
||||
List/Nil: []
|
||||
@ -111,7 +110,7 @@ List/head = @l
|
||||
# List l -> List l
|
||||
# removes and discards the first item of list l.
|
||||
# The new list is returned, or [] if the list is empty.
|
||||
List/pop_front = @l
|
||||
pop_front = @l
|
||||
match l {
|
||||
List/Cons: l.tail
|
||||
List/Nil: []
|
||||
@ -120,18 +119,18 @@ List/pop_front = @l
|
||||
# List pop_back:
|
||||
# List l -> List l
|
||||
# removes and discards the the last item of list l.
|
||||
List/pop_back (List/Nil) = List/Nil
|
||||
List/pop_back (List/Cons x List/Nil) = List/Nil
|
||||
List/pop_back (List/Cons head tail) = (List/Cons head (List/pop_back tail))
|
||||
pop_back (List/Nil) = List/Nil
|
||||
pop_back (List/Cons x List/Nil) = List/Nil
|
||||
pop_back (List/Cons head tail) = (List/Cons head (pop_back tail))
|
||||
|
||||
# List remove:
|
||||
# List l -> Some s -> List l
|
||||
# removes the first occurence of element e from list l.
|
||||
List/remove = @l @s
|
||||
remove = @l @s
|
||||
match l {
|
||||
List/Cons:
|
||||
switch (== l.head s) {
|
||||
0: (List/Cons l.head (List/remove l.tail s))
|
||||
0: (List/Cons l.head (remove l.tail s))
|
||||
_: l.tail
|
||||
}
|
||||
List/Nil: List/Nil
|
||||
@ -141,32 +140,33 @@ List/remove = @l @s
|
||||
# list l -> uint i -> (List l, list l)
|
||||
# splits list l into two lists (l1, l2) at index i.
|
||||
# the second list takes the element at index i during the split.
|
||||
List/split/aux = @acc @l @i
|
||||
split = @l @i (split.aux [] l i)
|
||||
|
||||
split.aux = @acc @l @i
|
||||
match l {
|
||||
List/Cons:
|
||||
switch i {
|
||||
0: (acc, l)
|
||||
_: (List/split/aux (List/append acc l.head) l.tail i-1)
|
||||
_: (split.aux (append acc l.head) l.tail i-1)
|
||||
}
|
||||
List/Nil: *
|
||||
}
|
||||
List/split = @l @i
|
||||
(List/split/aux [] l i)
|
||||
|
||||
|
||||
#################################
|
||||
|
||||
def main:
|
||||
return List/head([5, 4, 3, 2, 1])
|
||||
# return List/sum([1, 2, 3])
|
||||
# return List/split([1, 2, 3, 4, 5, 6, 7], 3)
|
||||
# return List/remove([1, 2, 1, 3], 1)
|
||||
# return List/pop_back([1, 2, 3, 4])
|
||||
# return List/pop_front([1, 2, 3])
|
||||
# return List/index([5, 3, 6, 8, 2], 0)
|
||||
# return List/clear([0, 2, 3])
|
||||
# return List/count([1, 2, 3, 3, 3, 4, 4, 5, 3, 1000], 4)
|
||||
# return List/len([1, 2, 3, 4, 4, 4])
|
||||
# return List/reverse([1, 2, 3, 4, 5])
|
||||
# return List/append([1, 2], 3)
|
||||
# return List/add_front([2, 3], 1)
|
||||
# return List/concat([1, 2], [3, 4])
|
||||
return head([5, 4, 3, 2, 1])
|
||||
# return sum([1, 2, 3])
|
||||
# return split([1, 2, 3, 4, 5, 6, 7], 3)
|
||||
# return remove([1, 2, 1, 3], 1)
|
||||
# return pop_back([1, 2, 3, 4])
|
||||
# return pop_front([1, 2, 3])
|
||||
# return index([5, 3, 6, 8, 2], 0)
|
||||
# return clear([0, 2, 3])
|
||||
# return count([1, 2, 3, 3, 3, 4, 4, 5, 3, 1000], 4)
|
||||
# return len([1, 2, 3, 4, 4, 4])
|
||||
# return reverse([1, 2, 3, 4, 5])
|
||||
# return append([1, 2], 3)
|
||||
# return add_front([2, 3], 1)
|
||||
# return concat([1, 2], [3, 4])
|
@ -1,8 +1,26 @@
|
||||
type String = (Nil) | (Cons head ~tail)
|
||||
|
||||
type List = (Nil) | (Cons head ~tail)
|
||||
type List = (Nil) | (Cons head ~tail)
|
||||
|
||||
type Nat = (Succ ~pred) | (Zero)
|
||||
List/length xs = fold xs with len=0, acc=[] {
|
||||
List/Nil: (len, (List/reverse acc))
|
||||
List/Cons: (xs.tail (+ len 1) (List/Cons xs.head acc))
|
||||
}
|
||||
|
||||
List/reverse xs = fold xs with acc=[] {
|
||||
List/Nil: acc
|
||||
List/Cons: (xs.tail (List/Cons xs.head acc))
|
||||
}
|
||||
|
||||
List/flatten (List/Cons x xs) = (List/concat x (List/flatten xs))
|
||||
List/flatten (List/Nil) = (List/Nil)
|
||||
|
||||
List/concat (List/Cons x xs) ys = (List/Cons x (List/concat xs ys))
|
||||
List/concat (List/Nil) ys = ys
|
||||
|
||||
type Nat = (Succ ~pred) | (Zero)
|
||||
|
||||
type Result = (Ok val) | (Err val)
|
||||
|
||||
type Tree:
|
||||
Node { ~left, ~right }
|
||||
@ -125,16 +143,96 @@ IO/FS/SEEK_CUR = +1
|
||||
IO/FS/SEEK_END = +2
|
||||
|
||||
### File utilities
|
||||
#read_file path = (IO/Call IO/MAGIC "GET_FILE" path @x (IO/Done IO/MAGIC x))
|
||||
#write_file path text = (IO/Call IO/MAGIC "PUT_FILE" (path, text) @x (IO/Done IO/MAGIC x))
|
||||
# Reads an entire file, returning a list of bytes.
|
||||
# def IO/FS/read_file(path: String) -> IO [u24]
|
||||
def IO/FS/read_file(path):
|
||||
with IO:
|
||||
fd <- IO/FS/open(path, "r")
|
||||
bytes <- IO/FS/read_to_end(fd)
|
||||
* <- IO/FS/close(fd)
|
||||
return wrap(bytes)
|
||||
|
||||
# Reads the remaining contents of a file, returning a list of read bytes.
|
||||
# def IO/FS/read_to_end(fd: u24) -> IO [u24]
|
||||
def IO/FS/read_to_end(fd):
|
||||
return IO/FS/read_to_end.read_chunks(fd, [])
|
||||
|
||||
def IO/FS/read_to_end.read_chunks(fd, chunks):
|
||||
with IO:
|
||||
# Read file in 1MB chunks
|
||||
chunk <- IO/FS/read(fd, 1048576)
|
||||
match chunk:
|
||||
case List/Nil:
|
||||
return wrap(List/flatten(chunks))
|
||||
case List/Cons:
|
||||
return IO/FS/read_to_end.read_chunks(fd, List/Cons(chunk, chunks))
|
||||
|
||||
# Reads a single line from a file, returning a list of bytes.
|
||||
# def IO/FS/read_line(fd: u24) -> IO [u24]
|
||||
def IO/FS/read_line(fd):
|
||||
return IO/FS/read_line.read_chunks(fd, [])
|
||||
|
||||
def IO/FS/read_line.read_chunks(fd, chunks):
|
||||
with IO:
|
||||
# Read line in 1kB chunks
|
||||
chunk <- IO/FS/read(fd, 1024)
|
||||
match res = Bytes/split_once(chunk, '\n'):
|
||||
case Result/Ok:
|
||||
(line, rest) = res.val
|
||||
(length, *) = List/length(rest)
|
||||
* <- IO/FS/seek(fd, to_i24(length) * -1, IO/FS/SEEK_CUR)
|
||||
chunks = List/Cons(line, chunks)
|
||||
bytes = List/flatten(chunks)
|
||||
return wrap(bytes)
|
||||
case Result/Err:
|
||||
line = res.val
|
||||
chunks = List/Cons(line, chunks)
|
||||
return IO/FS/read_line.read_chunks(fd, chunks)
|
||||
|
||||
# Writes a list of bytes to a file given by a path.
|
||||
# def IO/FS/write_file(path: String, bytes: [u24]) -> IO *
|
||||
def IO/FS/write_file(path, bytes):
|
||||
with IO:
|
||||
f <- IO/FS/open(path, "w")
|
||||
* <- IO/FS/write(f, bytes)
|
||||
* <- IO/FS/close(f)
|
||||
return wrap(bytes)
|
||||
|
||||
Bytes/split_once xs cond = (Bytes/split_once.go xs cond @x x)
|
||||
Bytes/split_once.go List/Nil cond acc = (Result/Err (acc List/Nil))
|
||||
Bytes/split_once.go (List/Cons x xs) cond acc =
|
||||
if (== cond x) {
|
||||
(Result/Ok ((acc List/Nil), xs))
|
||||
} else {
|
||||
(Bytes/split_once.go xs cond @y (acc (List/Cons x y)))
|
||||
}
|
||||
|
||||
### Standard input and output utilities
|
||||
|
||||
# TODO: Encode with utf-8
|
||||
IO/print text = (IO/FS/write IO/FS/STDOUT text)
|
||||
# Prints a string to stdout, encoding it with utf-8.
|
||||
# def IO/print(text: String) -> IO *
|
||||
IO/print text = (IO/FS/write IO/FS/STDOUT (String/encode_utf8 text))
|
||||
|
||||
# TODO: Should read any length of input
|
||||
IO/input = (IO/FS/read IO/FS/STDIN 1024)
|
||||
# Read characters from stdin until a newline is found.
|
||||
# Returns the read input decoded as utf-8.
|
||||
# def IO/input() -> IO String
|
||||
IO/input = (IO/input.go @x x)
|
||||
def IO/input.go(acc):
|
||||
# TODO: This is slow and inefficient, should be done in hvm using fgets.
|
||||
with IO:
|
||||
byte <- IO/FS/read(IO/FS/STDIN, 1)
|
||||
match byte:
|
||||
case List/Nil:
|
||||
# Nothing read, try again (to simulate blocking a read)
|
||||
return IO/input.go(acc)
|
||||
case List/Cons:
|
||||
if byte.head == '\n':
|
||||
bytes = acc(List/Nil)
|
||||
text = Bytes/decode_utf8(bytes)
|
||||
return wrap(text)
|
||||
else:
|
||||
acc = lambda x: acc(List/Cons(byte.head, x))
|
||||
return IO/input.go(acc)
|
||||
|
||||
# Lazy thunks
|
||||
# We can defer the evaluation of a function by wrapping it in a thunk
|
||||
@ -176,7 +274,7 @@ hvm to_u24:
|
||||
hvm to_i24:
|
||||
($([i24] ret) ret)
|
||||
|
||||
# Encoding
|
||||
# String Encoding and Decoding
|
||||
|
||||
Utf8/REPLACEMENT_CHARACTER = '\u{FFFD}'
|
||||
|
||||
@ -249,9 +347,9 @@ Utf8/decode_character (List/Cons a (List/Cons b (List/Cons c (List/Cons d rest))
|
||||
|
||||
String/encode_utf8 (String/Nil) = (List/Nil)
|
||||
String/encode_utf8 (String/Cons x xs) =
|
||||
use Utf8/rune1max = (- (<< 1 7) 1)
|
||||
use Utf8/rune2max = (- (<< 1 11) 1)
|
||||
use Utf8/rune3max = (- (<< 1 16) 1)
|
||||
use Utf8/rune1max = 0b01111111
|
||||
use Utf8/rune2max = 0b00000111_11111111
|
||||
use Utf8/rune3max = 0b11111111_11111111
|
||||
use Utf8/tx = 0b10000000
|
||||
use Utf8/t2 = 0b11000000
|
||||
use Utf8/t3 = 0b11100000
|
||||
|
@ -14,7 +14,7 @@ impl Ctx<'_> {
|
||||
for def in self.book.defs.values_mut() {
|
||||
let mut fresh = 0;
|
||||
for rule in def.rules.iter_mut() {
|
||||
if let Err(err) = rule.body.desugar_bend(&def.name, &mut fresh, &mut new_defs) {
|
||||
if let Err(err) = rule.body.desugar_bend(&def.name, &mut fresh, &mut new_defs, def.builtin) {
|
||||
self.info.add_rule_error(err, def.name.clone());
|
||||
break;
|
||||
}
|
||||
@ -35,11 +35,12 @@ impl Term {
|
||||
def_name: &Name,
|
||||
fresh: &mut usize,
|
||||
new_defs: &mut Vec<Definition>,
|
||||
builtin: bool,
|
||||
) -> Result<(), String> {
|
||||
maybe_grow(|| {
|
||||
// Recursively encode bends in the children
|
||||
for child in self.children_mut() {
|
||||
child.desugar_bend(def_name, fresh, new_defs)?;
|
||||
child.desugar_bend(def_name, fresh, new_defs, builtin)?;
|
||||
}
|
||||
|
||||
// Convert a bend into a new recursive function and call it.
|
||||
@ -87,8 +88,7 @@ impl Term {
|
||||
let body = Term::rfold_lams(body, free_vars.iter().cloned().map(Some));
|
||||
|
||||
// Make a definition from the new function
|
||||
let def =
|
||||
Definition { name: new_nam.clone(), rules: vec![Rule { pats: vec![], body }], builtin: false };
|
||||
let def = Definition { name: new_nam.clone(), rules: vec![Rule { pats: vec![], body }], builtin };
|
||||
new_defs.push(def);
|
||||
|
||||
// Call the new function in the original term.
|
||||
|
@ -34,8 +34,14 @@ impl Ctx<'_> {
|
||||
for def in self.book.defs.values_mut() {
|
||||
let mut fresh = 0;
|
||||
for rule in def.rules.iter_mut() {
|
||||
let res =
|
||||
rule.body.desugar_fold(&def.name, &mut fresh, &mut new_defs, &self.book.ctrs, &self.book.adts);
|
||||
let res = rule.body.desugar_fold(
|
||||
&def.name,
|
||||
&mut fresh,
|
||||
&mut new_defs,
|
||||
&self.book.ctrs,
|
||||
&self.book.adts,
|
||||
def.builtin,
|
||||
);
|
||||
if let Err(e) = res {
|
||||
self.info.add_rule_error(e, def.name.clone());
|
||||
}
|
||||
@ -56,10 +62,11 @@ impl Term {
|
||||
new_defs: &mut Vec<Definition>,
|
||||
ctrs: &Constructors,
|
||||
adts: &Adts,
|
||||
builtin: bool,
|
||||
) -> Result<(), String> {
|
||||
maybe_grow(|| {
|
||||
for child in self.children_mut() {
|
||||
child.desugar_fold(def_name, fresh, new_defs, ctrs, adts)?;
|
||||
child.desugar_fold(def_name, fresh, new_defs, ctrs, adts, builtin)?;
|
||||
}
|
||||
|
||||
if let Term::Fold { .. } = self {
|
||||
@ -113,8 +120,7 @@ impl Term {
|
||||
let body = Term::rfold_lams(body, with_bnd.iter().cloned());
|
||||
let body = Term::rfold_lams(body, free_vars.iter().map(|nam| Some(nam.clone())));
|
||||
let body = Term::lam(Pattern::Var(Some(x_nam)), body);
|
||||
let def =
|
||||
Definition { name: new_nam.clone(), rules: vec![Rule { pats: vec![], body }], builtin: false };
|
||||
let def = Definition { name: new_nam.clone(), rules: vec![Rule { pats: vec![], body }], builtin };
|
||||
new_defs.push(def);
|
||||
|
||||
// Call the new function
|
||||
|
@ -1,8 +1 @@
|
||||
type Result = (Ok val) | (Err val)
|
||||
|
||||
Result/bind r nxt = match r {
|
||||
Result/Ok: (nxt r.val)
|
||||
Result/Err: r
|
||||
}
|
||||
|
||||
main = ask x = (Result/Ok x); x
|
||||
|
@ -1,5 +1,3 @@
|
||||
type Result = (Ok val) | (Err val)
|
||||
|
||||
Result/bind (Result/Ok val) f = ((undefer f) val)
|
||||
Result/bind err _ = err
|
||||
|
||||
|
@ -1,6 +1,4 @@
|
||||
# Mixed contents in a `do` block should still work.
|
||||
type Result = (Ok val) | (Err val)
|
||||
|
||||
Result/bind r nxt = match r {
|
||||
Result/Ok: ((undefer nxt) r.val)
|
||||
Result/Err: r
|
||||
|
@ -1,5 +1,3 @@
|
||||
type Result = (Ok val) | (Err val)
|
||||
|
||||
Result/bind (Result/Ok val) f = ((undefer f) val)
|
||||
Result/bind err _ = err
|
||||
|
||||
|
@ -1,6 +1,4 @@
|
||||
# This will only work if we make the call to `(Result/foo a b)` lazy (by converting it to a combinator).
|
||||
type Result = (Ok val) | (Err val)
|
||||
|
||||
Result/bind = @val @nxt match val {
|
||||
Result/Ok: ((undefer nxt) val.val)
|
||||
Result/Err: (Result/Err val.val)
|
||||
|
Loading…
Reference in New Issue
Block a user