Skip to content

Commit

Permalink
Merge pull request #246 from HigherOrderCO/feature/sc-517/separate-nu…
Browse files Browse the repository at this point in the history
…m-matches-from-adt-matches

[sc-517] Use match and switch terms like Kind, remove complex pat-match expressions
  • Loading branch information
developedby authored Apr 1, 2024
2 parents 817aec9 + afd0f7d commit b382830
Show file tree
Hide file tree
Showing 209 changed files with 2,158 additions and 2,822 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
/target
*.snap.new
42 changes: 16 additions & 26 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

71 changes: 36 additions & 35 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ There are compiler options through the CLI. [Click here](docs/compiler-options.m

## Syntax

HVM-Lang files consists of a series of definitions, which bind a name to a term. Terms can be lambdas, applications, or other terms.
HVM-Lang files consists of a series of definitions, which bind a name to a term. Terms include lambda-calculus abstractions and applications, numbers, tuples, among others.

Here's a lambda where the body is the variable `x`:
```rs
Expand Down Expand Up @@ -104,6 +104,9 @@ let result = (+ 1 2); (* result result)
let {result_1 result_2} = (+ 1 2); (* result_1 result_2)
```

Duplications efficiently share the same value between two locations, only cloning a value when it's actually needed, but their exact behaviour is slightly more complicated than that and escapes normal lambda-calculus rules.
You can read more about it in [Dups and sups](docs/dups-and-sups.md).

It is possible to define tuples:
```rs
tup = (2, 2)
Expand Down Expand Up @@ -144,57 +147,55 @@ ListEx1 = [1, 2, 3]
data List = (List.cons head tail) | (List.nil)
ListEx2 = (List.cons 1 (List.cons 2 (List.cons 3 List.nil)))
```

It's possible to match different kinds of terms. These three forms are equivalent:
Hvm-lang supports pattern matching through `match` and `switch` terms.
`match` pattern matches on constructors declared with `data`.
```rs
match list {
(List.cons hd tl): (Some hd)
List.nil: None
data Option = (Some val) | None
// 'match' implicitly binds a variable for each field in the constructor.
// The name of the bound variable depends on the name of the argument.
map f x = match x {
Some: (Some (f x.val))
None: None
}

// If we don't provide field bindings, it will implicitly use
// the fields of the declared data type
match list {
List.cons: (Some list.head)
List.nil: None
}

match bind = list {
List.cons: (Some bind.head)
List.nil: None
}
// You can give a name to the match argument to access its fields.
TakeErr fallible_fn x errs =
match res = (fallible_fn x) {
// We can now access res.val.
// If no name is given, it will be inaccessible.
Result.ok: ((Some res.val), errs)
Result.err: (None, (List.cons res.val errs))
}
```

Match native numbers:
`switch` pattern matches on native numbers:
```rs
match 4 {
match x = 4 {
// From '0' to n, ending with the default case '_'.
0: "zero"
5: "five"
4: "four"
_: "other"
1: "one"
2: "two"
// The default case binds the name <arg>-<n>
// 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
_: (String.concat "other: " (String.from_num x-3))
}
```

Which is the equivalent of nesting match terms:
```rs
match 4 {
match x = 4 {
0: "zero"
1+a: match (- (+ a (+ 0 1)) 5) {
0: "five"
_: ...
_: match x-1 {
0: "one"
_: use x-2 = x-1-1; match x-2 {
0: "two"
_: use x-3 = x-2-1; (String.concat "other: " (String.from_num x-3))
}
}
}
```

Match multiple terms:
```rs
λa λb match a, b {
(Some True) (x, y): (Some (x, y))
(Some False) (x, y): (Some (y, x))
None *: None
}
```

### More features

Key:
Expand Down
13 changes: 11 additions & 2 deletions cspell.json
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,11 @@
"callcc",
"chumsky",
"combinators",
"concat",
"ctrs",
"Dall",
"datatypes",
"Deque",
"desugared",
"desugars",
"dref",
Expand Down Expand Up @@ -85,6 +87,13 @@
"walkdir",
"wopts"
],
"files": ["**/*.rs", "**/*.md"],
"ignoreRegExpList": ["HexValues", "/λ/g", "/-O/g"]
"files": [
"**/*.rs",
"**/*.md"
],
"ignoreRegExpList": [
"HexValues",
"/λ/g",
"/-O/g"
]
}
1 change: 1 addition & 0 deletions docs/automatic-vectorization-with-tagged-lambdas.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,5 +54,6 @@ This works because the `Bool`-tagged application in `not` passes through the `Li
The tagged lambda and applications are compiled to `inet` nodes with different tag values for each data type. This allows them to commute, read [HVM-Core](https://github.com/HigherOrderCO/hvm-core/tree/main#language) to learn more about it.

### Limitations
To be able to vectorize as described here:
- The function must not be recursive
- There must not be labels in common between the function and what you want to vectorize over
12 changes: 6 additions & 6 deletions docs/compiler-options.md
Original file line number Diff line number Diff line change
Expand Up @@ -142,20 +142,20 @@ When the `linearize-matches` option is used, linearizes only vars that are used

Example:
```rs
λa λb match a { 0: b; 1+: b }
λa λb switch a { 0: b; _: b }

// Is transformed to
λa λb (match a { 0: λc c; 1+: λd d } b)
λa λb (switch a { 0: λc c; _: λd d } b)
```

When the `linearize-matches-extra` option is used, linearizes all vars used in the arms.
When the `linearize-matches-extra` option is used, it linearizes all vars used in the arms.

example:
```rs
λa λb λc match a { 0: b; 1+: c }
λa λb λc switch a { 0: b; _: c }

// Is transformed to
λa λb λc (match a { 0: λd λ* d; 1+: λ* λe e } b c)
λa λb λc (switch a { 0: λd λ* d; _: λ* λe e } b c)
```

## float-combinators
Expand Down Expand Up @@ -224,7 +224,7 @@ If given the option, use another definition as entrypoint rather than `main` or
> By default, HVM-Lang searches for a function named either `main` or `Main` to use as entrypoint to a program, but it is possible to use a different entrypoint with the `-e --entrypoint` option.
Example:
```
```rust
// program
Main =x x λx x)

Expand Down
17 changes: 3 additions & 14 deletions docs/defining-data-types.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,7 @@ data Boxed = (Box val)
let (Box value) = boxed; value
```

For more complex types, there are two pattern syntaxes for matching data types.

One of them binds implicitly the matched variable name plus `.` and the field names on each constructor:

The fields of the constructor that is being destructured with the `match` are bound to the matched variable plus `.` and the field names.
```rs
Option.map = λoption λf
match option {
Expand All @@ -33,16 +30,6 @@ Option.map = λoption λf
}
```

And another one, which deconstructs the matched variable with explicit bindings:

```rs
Option.map = λoption λf
match option {
(Some value): (Some (f value))
(None): None
}
```

Rules can also have patterns.
They work like match expressions with explicit bindings:

Expand All @@ -60,4 +47,6 @@ data Boolean = True | False
(Option.is_both_some lft rgt) = False
```

You can read more about pattern matching rules in [Pattern matching](docs/pattern-matching.md).

In conclusion, the `data` keyword is very useful as it allows you to easily create data types and deconstruct them.
Loading

0 comments on commit b382830

Please sign in to comment.