Use the same keyword 'type' for adt definitions

This commit is contained in:
imaqtkatt 2024-05-22 11:51:35 -03:00
parent 6fcee9fd94
commit 97f7a40907
102 changed files with 191 additions and 181 deletions

View File

@ -19,15 +19,15 @@
# 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 value of the number -1 # The `+` arm binds the `scrutinee`-1 variable to 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 type Option = (Some val) | None
data Bool = True | False type 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
@ -46,7 +46,7 @@ data Bool = True | False
} }
# Data types can store values # Data types can store values
data Boxed = (Box val) type 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))
@ -71,7 +71,7 @@ data Boxed = (Box val)
# 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))
let fst = (Tuple.fst tup) let fst = (Tuple.fst tup)

View File

@ -1,4 +1,4 @@
data Tree = Leaf | (Node l m r) type Tree = Leaf | (Node l m r)
# Parallel QuickSort # Parallel QuickSort
(Sort List/Nil) = Tree/Leaf (Sort List/Nil) = Tree/Leaf

View File

@ -1,5 +1,5 @@
data Map_ = Free | Used | (Both a b) type Map_ = Free | Used | (Both a b)
data Arr = Null | (Leaf x) | (Node a b) type Arr = Null | (Leaf x) | (Node a b)
(Swap s a b) = switch s { (Swap s a b) = switch s {
0: (Map_/Both a b) 0: (Map_/Both a b)

View File

@ -1,11 +1,11 @@
data String = (Nil) | (Cons head ~tail) type String = (Nil) | (Cons head ~tail)
data List = (Nil) | (Cons head ~tail) type List = (Nil) | (Cons head ~tail)
data Result = (Ok val) | (Err val) type Result = (Ok val) | (Err val)
data Nat = (Succ ~pred) | (Zero) type Nat = (Succ ~pred) | (Zero)
# MAP Impl # MAP Impl
data Map = (Node value ~left ~right) | (Leaf) type Map = (Node value ~left ~right) | (Leaf)
Map/empty = Map/Leaf Map/empty = Map/Leaf
@ -60,7 +60,7 @@ IO_GET_TIME_TAG = 5
IO_SLEEP_TAG = 6 IO_SLEEP_TAG = 6
IO_DRAW_IMAGE_TAG = 7 IO_DRAW_IMAGE_TAG = 7
data IO type IO
= (Done term) = (Done term)
| (PutText text cont) | (PutText text cont)
| (GetText cont) | (GetText cont)

View File

@ -66,17 +66,6 @@ impl<'a> TermParser<'a> {
while !self.is_eof() { while !self.is_eof() {
let ini_idx = *self.index(); let ini_idx = *self.index();
// Imp type definition
if self.try_parse_keyword("type") {
let mut prs = PyParser { input: self.input, index: *self.index() };
let (enum_, nxt_indent) = prs.parse_type(indent)?;
self.index = prs.index;
let end_idx = *self.index();
prs.add_type(enum_, &mut book, ini_idx, end_idx, builtin)?;
indent = nxt_indent;
last_rule = None;
continue;
}
// Imp record type definition // Imp record type definition
if self.try_parse_keyword("object") { if self.try_parse_keyword("object") {
let mut prs = PyParser { input: self.input, index: *self.index() }; let mut prs = PyParser { input: self.input, index: *self.index() };
@ -101,14 +90,31 @@ impl<'a> TermParser<'a> {
continue; continue;
} }
// Fun type definition // Fun/Imp type definition
if self.try_parse_keyword("data") { if self.try_parse_keyword("type") {
let (nam, adt) = self.parse_datatype(builtin)?; self.skip_trivia();
let end_idx = *self.index(); let rewind_index = self.index;
self.with_ctx(book.add_adt(nam, adt), ini_idx, end_idx)?;
indent = self.advance_newlines(); let _ = self.labelled(|p| p.parse_top_level_name(), "datatype name")?;
last_rule = None;
continue; if self.starts_with(":") {
let mut prs = PyParser { input: self.input, index: rewind_index };
let (r#enum, nxt_indent) = prs.parse_type(indent)?;
self.index = prs.index;
let end_idx = *self.index();
prs.add_type(r#enum, &mut book, ini_idx, end_idx, builtin)?;
indent = nxt_indent;
last_rule = None;
continue;
} else {
self.index = rewind_index;
let (nam, adt) = self.parse_datatype(builtin)?;
let end_idx = *self.index();
self.with_ctx(book.add_adt(nam, adt), ini_idx, end_idx)?;
indent = self.advance_newlines();
last_rule = None;
continue;
}
} }
// Fun function definition // Fun function definition

View File

@ -962,14 +962,7 @@ impl<'a> PyParser<'a> {
let mut variants = Vec::new(); let mut variants = Vec::new();
let mut nxt_indent = indent; let mut nxt_indent = indent;
while nxt_indent == indent { while nxt_indent == indent {
let ctr_name = self.parse_top_level_name()?; variants.push(self.parse_enum_variant(&typ_name)?);
let ctr_name = Name::new(format!("{typ_name}/{ctr_name}"));
let mut fields = Vec::new();
self.skip_trivia_inline();
if self.starts_with("{") {
fields = self.list_like(|p| p.parse_variant_field(), "{", "}", ",", true, 0)?;
}
variants.push(Variant { name: ctr_name, fields });
if !self.is_eof() { if !self.is_eof() {
self.consume_new_line()?; self.consume_new_line()?;
} }
@ -981,6 +974,17 @@ impl<'a> PyParser<'a> {
Ok((enum_, nxt_indent)) Ok((enum_, nxt_indent))
} }
pub fn parse_enum_variant(&mut self, typ_name: &Name) -> ParseResult<Variant> {
let ctr_name = self.parse_top_level_name()?;
let ctr_name = Name::new(format!("{typ_name}/{ctr_name}"));
let mut fields = Vec::new();
self.skip_trivia_inline();
if self.starts_with("{") {
fields = self.list_like(|p| p.parse_variant_field(), "{", "}", ",", true, 0)?;
}
Ok(Variant { name: ctr_name, fields })
}
pub fn parse_object(&mut self, indent: Indent) -> ParseResult<(Variant, Indent)> { pub fn parse_object(&mut self, indent: Indent) -> ParseResult<(Variant, Indent)> {
if indent != Indent::Val(0) { if indent != Indent::Val(0) {
let msg = "Indentation error. Types defined with 'object' must be at the start of the line."; let msg = "Indentation error. Types defined with 'object' must be at the start of the line.";

View File

@ -1,4 +1,4 @@
data Pair type Pair
= (Pair fst snd) = (Pair fst snd)
Pair.get f (Pair/Pair fst snd) = (f fst snd) Pair.get f (Pair/Pair fst snd) = (f fst snd)

View File

@ -1,4 +1,4 @@
data Nat_ = (Z) | (S nat) type Nat_ = (Z) | (S nat)
U60ToNat n = switch n { U60ToNat n = switch n {
0: Nat_/Z 0: Nat_/Z

View File

@ -1,3 +1,3 @@
data Boolean = True | False type Boolean = True | False
main = Boolean/True main = Boolean/True

View File

@ -1,5 +1,5 @@
data Map_ = Free | Used | (Both a b) type Map_ = Free | Used | (Both a b)
data Arr = Null | (Leaf x) | (Node a b) type Arr = Null | (Leaf x) | (Node a b)
(Swap s a b) = switch s { (Swap s a b) = switch s {
0: (Map_/Both a b) 0: (Map_/Both a b)

View File

@ -1,5 +1,5 @@
data Map_ = Free | Used | (Both a b) type Map_ = Free | Used | (Both a b)
data Arr = Null | (Leaf x) | (Node a b) type Arr = Null | (Leaf x) | (Node a b)
(Swap s a b) = switch s { (Swap s a b) = switch s {
0: (Map_/Both a b) 0: (Map_/Both a b)

View File

@ -1,3 +1,3 @@
Foo a a = a Foo a a = a
Main = (Foo a) Main = (Foo a)

View File

@ -1,4 +1,4 @@
data A = A type A = A
A/A = 0 A/A = 0
main = A/A main = A/A

File diff suppressed because one or more lines are too long

View File

@ -1 +1 @@
data type

View File

@ -1 +1 @@
data Adt type Adt

View File

@ -1 +1 @@
data Adt = type Adt =

View File

@ -1,5 +1,5 @@
data Pair = (Pair fst snd) type Pair = (Pair fst snd)
fst_fst (Pair/Pair (Pair/Pair fst) *) = fst fst_fst (Pair/Pair (Pair/Pair fst) *) = fst
main = (fst_fst (Pair/Pair (Pair/Pair 1 2) 3)) main = (fst_fst (Pair/Pair (Pair/Pair 1 2) 3))

View File

@ -1,4 +1,4 @@
data Tree = (node lft rgt) | (leaf val) type Tree = (node lft rgt) | (leaf val)
tail_recursive = @x (x @pred @acc (tail_recursive pred (+ 1 acc)) @acc 0) tail_recursive = @x (x @pred @acc (tail_recursive pred (+ 1 acc)) @acc 0)

View File

@ -1,4 +1,4 @@
data Boxed = (Box val) type Boxed = (Box val)
Bar (*, (Boxed/Box x y)) = x Bar (*, (Boxed/Box x y)) = x

View File

@ -1,4 +1,4 @@
data Tup = (pair a b) type Tup = (pair a b)
(foo Tup/pair) = pair (foo Tup/pair) = pair

View File

@ -1,4 +1,4 @@
data Option = (Some val) | None type Option = (Some val) | None
Option/and = @a @b match a { Option/and = @a @b match a {
Option/Some: match b { Option/Some: match b {

View File

@ -1,3 +1,3 @@
data String = S type String = S
main = String/S main = String/S

View File

@ -1,4 +1,4 @@
data bool = true | false type bool = true | false
and a bool/false = bool/false and a bool/false = bool/false
and a bool/true = a and a bool/true = a

View File

@ -1,4 +1,4 @@
data Expr type Expr
= (Var name) = (Var name)
| (Num val) | (Num val)
| (App fun arg) | (App fun arg)
@ -9,7 +9,7 @@ data Expr
| (Tup fst snd) | (Tup fst snd)
| (Op2 op fst snd) | (Op2 op fst snd)
data Op type Op
= Add = Add
| Sub | Sub
| Mul | Mul

View File

@ -1,5 +1,5 @@
data Bool = True | False type Bool = True | False
data List_ = (Cons head tail) | Nil type List_ = (Cons head tail) | Nil
If Bool/True then else = then If Bool/True then else = then
If Bool/False then else = else If Bool/False then else = else

View File

@ -1,4 +1,4 @@
data list = (cons h t) | nil type list = (cons h t) | nil
reverse (list/cons h t) = (concat (reverse t) (list/cons h list/nil)) reverse (list/cons h t) = (concat (reverse t) (list/cons h list/nil))
reverse list/nil = list/nil reverse list/nil = list/nil

View File

@ -1,4 +1,4 @@
data Maybe = (Some val) | None type Maybe = (Some val) | None
main = @maybe main = @maybe
match maybe { match maybe {

View File

@ -1,4 +1,4 @@
data Box = (Boxed val) type Box = (Boxed val)
Got = @a match a { Got = @a match a {
Box/Boxed: (a, a.val) Box/Boxed: (a, a.val)

View File

@ -1,4 +1,4 @@
data Bool = T | F type Bool = T | F
Bool.and Bool/T Bool/T = Bool/T Bool.and Bool/T Bool/T = Bool/T
Bool.and Bool/F Bool/F = Bool/F Bool.and Bool/F Bool/F = Bool/F

View File

@ -1,10 +1,10 @@
# 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 type b1 = f1 | t1
data b2 = f2 | t2 type b2 = f2 | t2
data b3 = f3 | t3 type b3 = f3 | t3
data b4 = f4 | t4 type b4 = f4 | t4
(foo b1/f1 b2/f2 b3/f3 b4/f4) = 0 (foo b1/f1 b2/f2 b3/f3 b4/f4) = 0
(foo b1/f1 b2/f2 b3/f3 b4/t4) = 1 (foo b1/f1 b2/f2 b3/f3 b4/t4) = 1

View File

@ -1,4 +1,4 @@
data Type = A | B | C | D type Type = A | B | C | D
Foo Type/A Type/B Type/C Type/D = 0 Foo Type/A Type/B Type/C Type/D = 0
Foo Type/A Type/B Type/D Type/D = 1 Foo Type/A Type/B Type/D Type/D = 1

View File

@ -1,4 +1,4 @@
data Tree = (Leaf a) | (Both a b) type Tree = (Leaf a) | (Both a b)
(Warp s (Tree/Leaf a) (Tree/Leaf b)) = 0 (Warp s (Tree/Leaf a) (Tree/Leaf b)) = 0
(Warp s (Tree/Both a b) (Tree/Both c d)) = 1 (Warp s (Tree/Both a b) (Tree/Both c d)) = 1

View File

@ -1,5 +1,5 @@
# 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 type bool = false | true
(Foo bool/false a) = 0 (Foo bool/false a) = 0
(Foo bool/true 0) = 0 (Foo bool/true 0) = 0

View File

@ -1,4 +1,4 @@
data Option = (Some val) | None type Option = (Some val) | None
Option/or = @a @b match a { Option/or = @a @b match a {
Option/Some: a Option/Some: a

View File

@ -1,4 +1,4 @@
data Weekday type Weekday
= Monday = Monday
| Tuesday | Tuesday
| Wednesday | Wednesday

View File

@ -1,5 +1,5 @@
data Tree = (Leaf a) | (Both a b) type Tree = (Leaf a) | (Both a b)
data Error = Err type Error = Err
# Atomic Swapper # Atomic Swapper
(Swap n a b) = switch n { (Swap n a b) = switch n {

View File

@ -1,4 +1,4 @@
data list = (cons h t) | nil type list = (cons h t) | nil
reverse (list/cons h t) = (concat (reverse t) (list/cons h list/nil)) reverse (list/cons h t) = (concat (reverse t) (list/cons h list/nil))
reverse list/nil = list/nil reverse list/nil = list/nil

View File

@ -1,4 +1,4 @@
data Tree = (Leaf x) | (Node x0 x1) type Tree = (Leaf x) | (Node x0 x1)
add = λa λb (+ a b) add = λa λb (+ a b)

View File

@ -1,4 +1,4 @@
data nat = (succ pred) | zero type nat = (succ pred) | zero
foo = @x match x { foo = @x match x {
nat/succ: x.pred nat/succ: x.pred

View File

@ -1,4 +1,4 @@
data Foo = A | B | C | D | E | F | G | H type Foo = A | B | C | D | E | F | G | H
Bar Foo/A Foo/A Foo/A = * Bar Foo/A Foo/A Foo/A = *

View File

@ -1,4 +1,4 @@
data Tuple = (Pair a b) type Tuple = (Pair a b)
(Foo (Tuple/Pair (Tuple/Pair a b) c)) = a (Foo (Tuple/Pair (Tuple/Pair a b) c)) = a
(Foo *) = 2 (Foo *) = 2

View File

@ -1,4 +1,4 @@
data Bool = T | F type Bool = T | F
And (Bool/T, Bool/T, Bool/T) = Bool/T And (Bool/T, Bool/T, Bool/T) = Bool/T
And * = Bool/F And * = Bool/F

View File

@ -1,4 +1,4 @@
data bool = true | false type bool = true | false
not bool/false = bool/true not bool/false = bool/true
not bool/true = bool/false not bool/true = bool/false

View File

@ -1,4 +1,4 @@
data Bool = T | F type Bool = T | F
foo (Bool/T, x) = x foo (Bool/T, x) = x
foo * = Bool/F foo * = Bool/F

View File

@ -1,4 +1,4 @@
data box = (new val) type box = (new val)
unbox (box/new val) = val unbox (box/new val) = val
unbox x = x unbox x = x

View File

@ -1,24 +1,24 @@
data Box type Box
= (Filled value) = (Filled value)
| Empty | Empty
data Option type Option
= (Some x) = (Some x)
| None | None
data Result_ type Result_
= (Ok a) = (Ok a)
| (Err b) | (Err b)
data List_ type List_
= (Cons x xs) = (Cons x xs)
| Nil | Nil
data Bool = True | False type Bool = True | False
data Light = Red | Yellow | Green type Light = Red | Yellow | Green
data Direction type Direction
= North = North
| South | South
| East | East

View File

@ -1,5 +1,5 @@
data Either = (Left value) | (Right value) type Either = (Left value) | (Right value)
data Bool = Bool/True | Bool/False type Bool = Bool/True | Bool/False
Foo (Either/Left Bool/False) (Either/Left Bool/False) = 1 Foo (Either/Left Bool/False) (Either/Left Bool/False) = 1
Foo (Either/Left Bool/False) (Either/Left Bool/True) = 1 Foo (Either/Left Bool/False) (Either/Left Bool/True) = 1

View File

@ -1,4 +1,4 @@
data Expr type Expr
= (Var name) = (Var name)
| (Num val) | (Num val)
| (App fun arg) | (App fun arg)
@ -9,7 +9,7 @@ data Expr
| (Tup fst snd) | (Tup fst snd)
| (Op2 op fst snd) | (Op2 op fst snd)
data Op type Op
= Add = Add
| Sub | Sub
| Mul | Mul

View File

@ -1,4 +1,4 @@
data Option = (Some x) | (None) type Option = (Some x) | (None)
some_some (Option/Some (Option/Some x)) = 1 some_some (Option/Some (Option/Some x)) = 1
some_some * = 0 some_some * = 0

View File

@ -1,5 +1,5 @@
data Bool = True | False type Bool = True | False
data List_ = (Cons head tail) | Nil type List_ = (Cons head tail) | Nil
If Bool/True then else = then If Bool/True then else = then
If Bool/False then else = else If Bool/False then else = else
@ -26,4 +26,4 @@ Merge cmp (List_/Cons xh xt) (List_/Cons yh yt) =
(List_/Cons xh (Merge cmp xt ys)) (List_/Cons xh (Merge cmp xt ys))
let xs = (List_/Cons xh xt) let xs = (List_/Cons xh xt)
(List_/Cons yh (Merge cmp xs yt)) (List_/Cons yh (Merge cmp xs yt))
) )

View File

@ -1,5 +1,5 @@
# 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 type bool = T | F
main = @x match x { main = @x match x {
Bool/T: @$x $x Bool/T: @$x $x

View File

@ -1,4 +1,4 @@
data Maybe = None | (Some val) type Maybe = None | (Some val)
main = (match x = (Maybe/Some 1) { main = (match x = (Maybe/Some 1) {
Maybe/None: @$x * Maybe/None: @$x *

View File

@ -1,4 +1,4 @@
data Maybe = None | (Some val) type Maybe = None | (Some val)
Foo = @$x match x = (Maybe/Some 1) { Foo = @$x match x = (Maybe/Some 1) {
Maybe/None: $x Maybe/None: $x

View File

@ -1,5 +1,5 @@
# Testing various forms of pattern matching # Testing various forms of pattern matching
data Result_ = (Ok val) | (Err err) type Result_ = (Ok val) | (Err err)
Parse state (String/Cons '(' xs) = (Result_/Ok ('(', xs, state)) Parse state (String/Cons '(' xs) = (Result_/Ok ('(', xs, state))
Parse state (String/Cons ')' xs) = (Result_/Ok (')', xs, state)) Parse state (String/Cons ')' xs) = (Result_/Ok (')', xs, state))

View File

@ -1,4 +1,4 @@
data List_ = (Cons x xs) | (Nil) type List_ = (Cons x xs) | (Nil)
head x = head x =
match x { match x {

View File

@ -1,4 +1,4 @@
data bool = true | false type bool = true | false
Foo x bool/false = x Foo x bool/false = x
Foo x bool/true = (Foo x x) Foo x bool/true = (Foo x x)

View File

@ -1,4 +1,4 @@
data MyType = (A a) | (B b) | (C c) | (D d1 d2) | (E e1 e2) type MyType = (A a) | (B b) | (C c) | (D d1 d2) | (E e1 e2)
Foo (MyType/A a) = 100 Foo (MyType/A a) = 100
Foo * = 200 Foo * = 200

View File

@ -1,4 +1,4 @@
data Bool = False | True type Bool = False | True
(Foo a b) = λf (f a) (Foo a b) = λf (f a)
(Foo a b) = b (Foo a b) = b

View File

@ -1,4 +1,4 @@
data Weekday type Weekday
= Monday = Monday
| Tuesday | Tuesday
| Wednesday | Wednesday

View File

@ -1,4 +1,4 @@
data Bool = True | False type Bool = True | False
(if_ 0 then else) = else (if_ 0 then else) = else
(if_ _ then else) = then (if_ _ then else) = then

View File

@ -1,3 +1,3 @@
A = 0 A = 0
data B = B type B = B
A = 1 A = 1

View File

@ -1,4 +1,4 @@
data Foo = A type Foo = A
data Foo = B type Foo = B
main = * main = *

View File

@ -1,4 +1,4 @@
data Opt = (Some x) | None type Opt = (Some x) | None
Opt/map = @opt @f Opt/map = @opt @f
match opt { match opt {

View File

@ -1,3 +1,3 @@
data Option = (Some val) | None type Option = (Some val) | None
main = λa #Option (a #wrong_tag λb b *) main = λa #Option (a #wrong_tag λb b *)

View File

@ -1,4 +1,4 @@
data Option = (Some val) | None type Option = (Some val) | None
main = @a @b match a { main = @a @b match a {
Option/Some: match b { Option/Some: match b {

View File

@ -1,3 +1,3 @@
data Option = (Some val) | None type Option = (Some val) | None
main = (@a #Option (a #wrong_tag @x x *)) main = (@a #Option (a #wrong_tag @x x *))

View File

@ -1,4 +1,4 @@
data bool = true | false type bool = true | false
and a bool/false = bool/false and a bool/false = bool/false
and a bool/true = a and a bool/true = a

View File

@ -1,5 +1,5 @@
# should return (a+b+c) * 2^depth # should return (a+b+c) * 2^depth
data Tree = (node ~lft ~rgt) | (leaf val) type Tree = (node ~lft ~rgt) | (leaf val)
main = main =
let depth = 2 let depth = 2

View File

@ -1,5 +1,5 @@
data Tree = (Leaf a) | (Both a b) type Tree = (Leaf a) | (Both a b)
data Error = Err type Error = Err
# Atomic Swapper # Atomic Swapper
(Swap n a b) = switch n { (Swap n a b) = switch n {

View File

@ -1,4 +1,4 @@
data _Box = (Box val) type _Box = (Box val)
Box.subst (_Box/Box x) cmp to = switch _ = (cmp x) { Box.subst (_Box/Box x) cmp to = switch _ = (cmp x) {
0: (_Box/Box x) 0: (_Box/Box x)

View File

@ -1,4 +1,4 @@
data bool = true | false type bool = true | false
go bool/true 0 = 1 go bool/true 0 = 1
go bool/false _ = 0 go bool/false _ = 0

View File

@ -1,4 +1,4 @@
data bool = true | false type bool = true | false
go 0 bool/true = 1 go 0 bool/true = 1
go 0 bool/false = 0 go 0 bool/false = 0

View File

@ -19,15 +19,15 @@
# 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 type Option = (Some val) | None
data Bool = True | False type 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
@ -46,7 +46,7 @@ data Bool = True | False
} }
# Data types can store values # Data types can store values
data Boxed = (Box val) type 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))
@ -71,7 +71,7 @@ data Boxed = (Box val)
# 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))
let fst = (Tuple.fst tup) let fst = (Tuple.fst tup)

View File

@ -1,4 +1,4 @@
data list = (cons h t) | nil type list = (cons h t) | nil
reverse (list/cons h t) = (concat (reverse t) (list/cons h list/nil)) reverse (list/cons h t) = (concat (reverse t) (list/cons h list/nil))
reverse list/nil = list/nil reverse list/nil = list/nil

View File

@ -1,5 +1,5 @@
# Testing various forms of pattern matching # Testing various forms of pattern matching
data Result_ = (Ok val) | (Err err) type Result_ = (Ok val) | (Err err)
Parse state (String/Cons '{' xs) = (Result_/Ok ('{', xs, state)) Parse state (String/Cons '{' xs) = (Result_/Ok ('{', xs, state))
Parse state (String/Cons '}' xs) = (Result_/Ok ('}', xs, state)) Parse state (String/Cons '}' xs) = (Result_/Ok ('}', xs, state))

View File

@ -1,12 +1,12 @@
data Tree = (Leaf x) | (Node x0 x1) type Tree = (Leaf x) | (Node x0 x1)
data List_ = Nil | (Cons h t) type List_ = Nil | (Cons h t)
sort (Tree/Leaf v) = (List_/Cons v List_/Nil) sort (Tree/Leaf v) = (List_/Cons v List_/Nil)
sort (Tree/Node a b) = (merge (sort a) (sort b)) sort (Tree/Node a b) = (merge (sort a) (sort b))
merge (List_/Nil) b = b merge (List_/Nil) b = b
merge (List_/Cons x xs) (List_/Nil) = (List_/Cons x xs) merge (List_/Cons x xs) (List_/Nil) = (List_/Cons x xs)
merge (List_/Cons x xs) (List_/Cons y ys) = merge (List_/Cons x xs) (List_/Cons y ys) =
let t = switch _ = (< x y) { let t = switch _ = (< x y) {
0: λaλbλcλt(t c a b) 0: λaλbλcλt(t c a b)
_: λaλbλcλt(t a b c) _: λaλbλcλt(t a b c)

View File

@ -2,7 +2,7 @@ type Bool:
True True
False False
data Tree = (node ~lft ~rgt) | (leaf val) type Tree = (node ~lft ~rgt) | (leaf val)
def tree_xor(tree): def tree_xor(tree):
fold tree: fold tree:
@ -21,6 +21,6 @@ main =
when (< n depth): when (< n depth):
(Tree/node (fork (+ n 1)) (fork (+ n 1))) (Tree/node (fork (+ n 1)) (fork (+ n 1)))
else: else:
if (% n 2) { (Tree/leaf Bool/True) } else { (Tree/leaf Bool/False) } if (% n 2) { (Tree/leaf Bool/True) } else { (Tree/leaf Bool/False) }
} }
(tree_xor tree) (tree_xor tree)

View File

@ -1,6 +1,6 @@
id cool-var-name = cool-var-name id cool-var-name = cool-var-name
data Done_ = (Done done-var) type Done_ = (Done done-var)
toZero n = toZero n =
switch n { switch n {

View File

@ -1,4 +1,4 @@
data Foo-Bar = (Baz-Qux field-hyph) type Foo-Bar = (Baz-Qux field-hyph)
fun-with-hyphen = 1 fun-with-hyphen = 1

View File

@ -1,4 +1,4 @@
data Pair = (new a b) type Pair = (new a b)
type State: type State:
new { a, b } new { a, b }
@ -10,4 +10,4 @@ def with_state(x, s):
main = main =
let x = (with_state @x x (State/new 1 2)) let x = (with_state @x x (State/new 1 2))
open Pair x; open Pair x;
{x.a x.b} {x.a x.b}

View File

@ -1,5 +1,5 @@
data Map_ = Free | Used | (Both a b) type Map_ = Free | Used | (Both a b)
data Arr = Null | (Leaf x) | (Node a b) type Arr = Null | (Leaf x) | (Node a b)
(Swap s a b) = switch s { (Swap s a b) = switch s {
0: (Map_/Both a b) 0: (Map_/Both a b)

View File

@ -1,5 +1,5 @@
# 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) type tup = (pair a b)
main = (List/Cons main = (List/Cons
(String/Cons 'a' (tup/pair 'b' (String/Cons 'c' String/Nil))) (String/Cons 'a' (tup/pair 'b' (String/Cons 'c' String/Nil)))

View File

@ -1,4 +1,4 @@
data Tree = (Leaf x) | (Node x0 x1) type Tree = (Leaf x) | (Node x0 x1)
add = λa λb (+ a b) add = λa λb (+ a b)
@ -13,4 +13,4 @@ sum = λt
Tree/Node: (add (sum t.x0) (sum t.x1)) Tree/Node: (add (sum t.x0) (sum t.x1))
} }
main = (sum (gen 8)) main = (sum (gen 8))

View File

@ -1,5 +1,5 @@
data N = (S pred) | Z type N = (S pred) | Z
data B = T | F type B = T | F
(Not B/T) = B/F (Not B/T) = B/F
(Not B/F) = B/T (Not B/F) = B/T

View File

@ -1,4 +1,4 @@
data Bool = T | F type Bool = T | F
main = @x match x { main = @x match x {
Bool/T : @$x * Bool/T : @$x *

View File

@ -8,6 +8,6 @@
# 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 type bool = t | f
main = @b match b { bool/t: 0; bool/f: 1} main = @b match b { bool/t: 0; bool/f: 1}

View File

@ -1,4 +1,4 @@
data Tuple = (Pair a b) type Tuple = (Pair a b)
(Foo (Tuple/Pair (Tuple/Pair a b) c)) = a (Foo (Tuple/Pair (Tuple/Pair a b) c)) = a
(Foo *) = 2 (Foo *) = 2

View File

@ -1,6 +1,6 @@
data Foo = CtrA | (CtrB x) type Foo = CtrA | (CtrB x)
data Bar = (CtrA1 a) | (CtrA2 a1 a2) | (CtrA3 a) type Bar = (CtrA1 a) | (CtrA2 a1 a2) | (CtrA3 a)
data Baz = (CtrB0) | (CtrB1 b) | (CtrB2 b) | (CtrB3 b) type Baz = (CtrB0) | (CtrB1 b) | (CtrB2 b) | (CtrB3 b)
Rule1 = λx x Rule1 = λx x

View File

@ -1,4 +1,4 @@
data Data/Bits = e | (o t) | (i t) type Data/Bits = e | (o t) | (i t)
Data.Bits.dec Data/Bits/e = (Data/Bits/e) Data.Bits.dec Data/Bits/e = (Data/Bits/e)
Data.Bits.dec (Data/Bits/o (Data/Bits/e)) = (Data/Bits/e) Data.Bits.dec (Data/Bits/o (Data/Bits/e)) = (Data/Bits/e)

View File

@ -1,11 +1,11 @@
data Tree = (Node lt rt rd ld) | (Leaf val) type Tree = (Node lt rt rd ld) | (Leaf val)
(map) = (map) =
λarg1 λarg2 use tree = arg2; λarg1 λarg2 use tree = arg2;
use f = arg1; use f = arg1;
match tree with f { match tree with f {
Tree/Node: (Tree/Node (map f tree.lt) (map f tree.rt) (map f tree.rd) (map f tree.ld)); Tree/Node: (Tree/Node (map f tree.lt) (map f tree.rt) (map f tree.rd) (map f tree.ld));
Tree/Leaf: (Tree/Leaf (f tree.val)); Tree/Leaf: (Tree/Leaf (f tree.val));
} }
main = map main = map

View File

@ -1,5 +1,5 @@
# 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) type Boxed = (Box x)
(DoubleUnbox (Boxed/Box (Boxed/Box x)) *) = x (DoubleUnbox (Boxed/Box (Boxed/Box x)) *) = x
(DoubleUnbox * x) = x (DoubleUnbox * x) = x

View File

@ -1,5 +1,5 @@
# 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 type Maybe = (Some x) | None
(DoubleUnwrap (Maybe/Some (Maybe/Some x)) *) = x (DoubleUnwrap (Maybe/Some (Maybe/Some x)) *) = x
(DoubleUnwrap * x) = x (DoubleUnwrap * x) = x

View File

@ -1,6 +1,6 @@
# 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) type A_t = (A b)
data B_t = B type B_t = B
(Foo 0 (A_t/A B_t/B)) = B_t/B (Foo 0 (A_t/A B_t/B)) = B_t/B
(Foo * *) = * (Foo * *) = *

View File

@ -1,5 +1,5 @@
# Testing linearization in different situations # Testing linearization in different situations
data ConsList = (Cons h t) | Nil type 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 {

View File

@ -1,6 +1,6 @@
data Foo = (CtrA a b) | (CtrB a) type Foo = (CtrA a b) | (CtrB a)
data Bar = (CtrB1 b) | (CtrB2 a b) type Bar = (CtrB1 b) | (CtrB2 a b)
data Baz = CtrC type Baz = CtrC
(Rule (Foo/CtrA a (Bar/CtrB1 b))) = (a b) (Rule (Foo/CtrA a (Bar/CtrB1 b))) = (a b)
(Rule (Foo/CtrA a (Bar/CtrB2 (Baz/CtrC) b))) = (a b) (Rule (Foo/CtrA a (Bar/CtrB2 (Baz/CtrC) b))) = (a b)

View File

@ -1,4 +1,4 @@
data list = (Cons head tail) | Nil type list = (Cons head tail) | Nil
Unpack cmp list/Nil = list/Nil Unpack cmp list/Nil = list/Nil
Unpack cmp (list/Cons h list/Nil) = h Unpack cmp (list/Cons h list/Nil) = h

View File

@ -6,4 +6,4 @@ input_file: tests/golden_tests/compile_file/just_data.bend
In tests/golden_tests/compile_file/just_data.bend : In tests/golden_tests/compile_file/just_data.bend :
- expected: datatype name - expected: datatype name
- detected: end of input - detected: end of input
 1 | data   1 | type 

View File

@ -6,4 +6,4 @@ input_file: tests/golden_tests/compile_file/missing_adt_eq.bend
In tests/golden_tests/compile_file/missing_adt_eq.bend : In tests/golden_tests/compile_file/missing_adt_eq.bend :
- expected: '=' - expected: '='
- detected: end of input - detected: end of input
 1 | data Adt   1 | type Adt 

View File

@ -6,4 +6,4 @@ input_file: tests/golden_tests/compile_file/missing_ctrs.bend
In tests/golden_tests/compile_file/missing_ctrs.bend : In tests/golden_tests/compile_file/missing_ctrs.bend :
- expected: datatype constructor name - expected: datatype constructor name
- detected: end of input - detected: end of input
 1 | data Adt =    1 | type Adt = 

Some files were not shown because too many files have changed in this diff Show More