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

[sc-517] Update docs, fix not checking fn arity, refactor match def checks

Browse Source
This commit is contained in:
Nicolas Abril 2024-03-29 10:43:47 +01:00
parent 58f1f53a7d
commit b18df385a2
22 changed files with 279 additions and 416 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
Cargo.lock generated
View File

@ -98,9 +98,9 @@ dependencies = [
[[package]]
name = "clap"
version = "4.5.3"
version = "4.5.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "949626d00e063efc93b6dca932419ceb5432f99769911c0b995f7e884c778813"
checksum = "90bc066a67923782aa8515dbaea16946c5bcc5addbd668bb80af688e53e548a0"
dependencies = [
"clap_builder",
"clap_derive",
@ -120,9 +120,9 @@ dependencies = [
[[package]]
name = "clap_derive"
version = "4.5.3"
version = "4.5.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "90239a040c80f5e14809ca132ddc4176ab33d5e17e49691793296e3fcb34d72f"
checksum = "528131438037fd55894f62d6e9f068b8f45ac57ffa77517819645d10aed04f64"
dependencies = [
"heck",
"proc-macro2",
@ -207,8 +207,8 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
[[package]]
name = "hvm-core"
version = "0.2.20"
source = "git+https://github.com/HigherOrderCO/hvm-core.git#acbc4295283472925426eee97a2f85e4686adba2"
version = "0.2.21"
source = "git+https://github.com/HigherOrderCO/hvm-core.git#f92475b7102d514311e24a41492ae8f1e6a9b2d3"
dependencies = [
"arrayvec",
"clap",
@ -236,9 +236,9 @@ dependencies = [
[[package]]
name = "indexmap"
version = "2.2.5"
version = "2.2.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7b0b929d511467233429c45a44ac1dcaa21ba0f5ba11e4879e6ed28ddb4f9df4"
checksum = "168fb715dda47215e360912c096649d23d58bf392ac62f73919e831745e40f26"
dependencies = [
"equivalent",
"hashbrown 0.14.3",
@ -246,15 +246,14 @@ dependencies = [
[[package]]
name = "insta"
version = "1.36.1"
version = "1.38.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0a7c22c4d34ef4788c351e971c52bfdfe7ea2766f8c5466bc175dd46e52ac22e"
checksum = "3eab73f58e59ca6526037208f0e98851159ec1633cf17b6cd2e1f2c3fd5d53cc"
dependencies = [
"console",
"lazy_static",
"linked-hash-map",
"similar",
"yaml-rust",
]
[[package]]
@ -364,9 +363,9 @@ dependencies = [
[[package]]
name = "regex-syntax"
version = "0.8.2"
version = "0.8.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f"
checksum = "adad44e29e4c806119491a7f06f03de4d1af22c3a680dd47f1e6e179439d1f56"
[[package]]
name = "same-file"
@ -379,9 +378,9 @@ dependencies = [
[[package]]
name = "similar"
version = "2.4.0"
version = "2.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "32fea41aca09ee824cc9724996433064c89f7777e60762749a4170a14abbfa21"
checksum = "fa42c91313f1d05da9b26f267f931cf178d4aba455b4c4622dd7355eb80c6640"
[[package]]
name = "stacker"
@ -410,9 +409,9 @@ checksum = "5ee073c9e4cd00e28217186dbe12796d692868f432bf2e97ee73bed0c56dfa01"
[[package]]
name = "syn"
version = "2.0.53"
version = "2.0.55"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7383cd0e49fff4b6b90ca5670bfd3e9d6a733b3f90c686605aa7eec8c4996032"
checksum = "002a1b3dbf967edfafc32655d0f377ab0bb7b994aa1d32c8cc7e9b8bf3ebb8f0"
dependencies = [
"proc-macro2",
"quote",
@ -544,15 +543,6 @@ version = "0.52.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8"
[[package]]
name = "yaml-rust"
version = "0.4.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "56c1936c4cc7a1c9ab21a1ebb602eb942ba868cbd44a99cb7cdc5892335e1c85"
dependencies = [
"linked-hash-map",
]
[[package]]
name = "zerocopy"
version = "0.7.32"

71
README.md
View File

@ -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
@ -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)
@ -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:

1
docs/automatic-vectorization-with-tagged-lambdas.md
View File

@ -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
docs/compiler-options.md
View File

@ -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
@ -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)

17
docs/defining-data-types.md
View File

@ -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 {
@ -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:
@ -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.

258
docs/pattern-matching.md
View File

@ -1,102 +1,139 @@
# Pattern Matching
HVM-Lang offers pattern matching capabilities. You can use pattern matching in function definitions and with the `match` expression.
Switches on many numbers are compiled to sequences of simple switch expressions:
```rust
// These two are equivalent
switch n {
0: A
1: B
2: C
_: (D n-3)
}
Pattern matching definitions are just a syntax sugar to match expressions:
switch n {
0: A
_: switch n-1 = n-1 {
0: B
_: switch n-2 = n-1-1 {
0: C
_: use n-3 = n-2-1; (D n-3)
}
}
}
```
Matches on ADT constructors are compiled to different expressions depending on the chosen encoding:
```rust
data Maybe = (Some val) | None
UnwrapOrZero x = match x {
Some: x.val
None: 0
}
// If the current encoding is 'adt-tagged-scott' it becomes:
Some = λval #Maybe λSome #Maybe λNone #Maybe(Some val)
None = #Maybe λSome #Maybe λNone None
UnwrapOrZero x = #Maybe (x #Maybe λx.val x.val 0)
// Otherwise, if the current encoding is 'adt-scott' it becomes:
Some = λval λSome λNone (Some val)
None = λSome λNone None
UnwrapOrZero x = (x λx.val x.val 0)
```
Currently, if you want to readback the adt constructors and matches after running a program as constructors and matches and not as lambda terms, you have to use `-Oadt-tagged-scott`.
The tags are used to decode which ADT the lambda term refers to, but having them means that if you want to write your own function to operate on these tagged structures your functions have to either use the `match` syntax or use the tags correctly themselves.
You can read more about tagged lambdas and applications in [Automatic vectorization with tagged lambdas](docs/automatic-vectorization-with-tagged-lambdas.md).
### Pattern Matching functions
Besides `match`and `switch` terms, hvm-lang also supports equational-style pattern matching functions.
```rust
And True b = b
And False * = False
```
There are advantages and disadvantages to using this syntax.
They offer more advanced pattern matching capabilities and also take care linearizing variables to make sure that recursive definitions work correctly in strict evaluation mode, but take away your control of how the pattern matching is implemented and can be a bit more resource intensive in some cases.
Pattern matching equations are transformed into a tree of `match` and `switch` terms from left to right.
```rust
// These two are equivalent
(Foo 0 false (Cons h1 (Cons h2 t))) = (A h1 h2 t)
(Foo 0 * *) = B
(Foo 1+n false *) = n
(Foo 1+n true *) = 0
(Foo n false *) = n
(Foo * true *) = 0
Foo = λarg1 λarg2 λarg3 match arg1 arg2 arg3 {
(Foo 0 false (Cons h1 (Cons h2 t))): (A h1 h2 t)
(Foo 0 * *): B
(Foo 1+n false *): n
(Foo 1+n true *): 0
}
```
Pattern matching on numbers has two forms.
With the successor pattern `n+var` it will expect to cover every case up to `n`:
```rust
match n {
0: A
1: B
...
n+var: (N var)
}
// Becomes:
match n {
0: A
1+p: match p {
...
1+var: (N var)
Foo = λarg1 λarg2 λarg3 (switch arg1 {
0: λarg2 λarg3 match arg2 {
true: λarg3 B
false: λarg3 match arg3 {
Cons: (match arg3.tail {
Cons: λarg3.head (A arg3.head arg3.tail.head arg3.tail.tail)
Nil: λarg3.head B
} arg3.head)
Nil: B
}
}
}
_: λarg2 λarg3 (match arg2 {
true: λarg1-1 0
false: λarg1-1 (+ arg1-1 0)
} arg1-1)
} arg2 arg3)
```
Besides the compilation of complex pattern matching into simple `match` and `switch` expressions, this example also shows how some arguments are pushed inside the match.
When compiling for strict evaluation, by default any variables that are used inside a match get linearized by adding a lambda in each arm and an application passing its value inwards.
To ensure that recursive pattern matching functions don't loop in strict mode, it's necessary to make the match arms combinators, so that they can be converted into separate functions and a lazy reference is used in the match arm.
```rust
// This is what the Foo function actually compiles to.
// With -Olinearize-matches-extra and -Ofloat-combinators (default on strict mode)
(Foo) = λa λb λc (switch a { 0: Foo$C5; _: Foo$C8 } b c)
// Error: Case '2' not covered.
match n {
1: B;
0: A;
3+: ...;
}
(Foo$C5) = λd λe (d Foo$C0 Foo$C4 e) // Foo.case_0
(Foo$C0) = λ* B // Foo.case_0.case_true
(Foo$C4) = λg (g Foo$C3 B) // Foo.case_0.case_false
(Foo$C3) = λh λi (i Foo$C1 Foo$C2 h) // Foo.case_0.case_false.case_cons
(Foo$C1) = λj λk λl (A l j k) // Foo.case_0.case_false.case_cons.case_cons
(Foo$C2) = λ* B // Foo.case_0.case_false.case_cons.case_nil
(Foo$C8) = λn λo λ* (o Foo$C6 Foo$C7 n) // Foo.case_+
(Foo$C6) = λ* 0 // Foo.case_+.case_true
(Foo$C7) = λr (+ r 1) // Foo.case_+.case_false
```
With the wildcard pattern you can use any number freely:
Pattern matching equations also support matching on non-consecutive numbers:
```rust
match n {
23: A
6343: B
0: C
...
var: (N var)
}
// Becomes:
match (- n 32) {
0: A
1+n:
let n = (+ (+ n 1) 23); match (- n 6453) {
...
1+var: let n = (+ (+ n 1) N-1); (N var)
Parse '(' = Token.LParen
Parse ')' = Token.RParen
Parse 'λ' = Token.Lambda
Parse n = (Token.Name n)
```
This is compiled to a cascade of `switch` expressions, from smallest value to largest.
```rust
Parse = λarg0 switch matched = (- arg0 '(') {
0: Token.LParen
// ')' + 1 - '(' is resolved during compile time
_: switch matched = (- matched-1 ( ')'-1-'(' ) {
0: Token.RParen
_: switch matched = (- matched-1 ( 'λ'-1-')' ) {
0: Token.Lambda
_: use n = (+ 1 matched-1); (Token.Name n)
}
}
}
```
Unlike with `switch`, with pattern matching equations you can't access the value of the predecessor of the matched value directly, but instead you can match on a variable.
Notice how in the example above, `n` is bound to `(+ 1 matched-1)`.
Notice that this definition is valid, since `*` will cover both `1+p` and `0` cases when the first argument is `False`.
Notice that this definition is valid, since `*` will cover both `p` and `0` cases when the first argument is `False`.
```rust
pred_if False * if_false = if_false
pred_if True 1+p * = p
pred_if True 0 * = 0
```
Match on tuples become let tuple destructors, which are compiled to a native tuple destructor in hvm-core.
```rust
match x {
(f, s): s
}
// Becomes:
let (f, s) = x; s
```
Match on vars becomes a rebinding of the variable with a let expression.
```rust
match x {
c: (Some c)
}
// Becomes:
let c = x; (Some c)
pred_if False * if_false = if_false
pred_if True p * = (- p 1)
pred_if True 0 * = 0
```
Pattern matching on strings and lists desugars to a list of matches on List/String.cons and List/String.nil
@ -117,66 +154,3 @@ Foo List.nil = 0
Foo (List.cons x List.nil) = x
Foo _ = 3
```
Matches on ADT constructors are compiled to different expressions depending on the chosen encoding.
```rust
data Maybe = (Some val) | None
match x {
(Some val): val
None: 0
}
// If the current encoding is 'adt-tagged-scott' it becomes:
#Maybe (x #Maybe.Some.val λval val 0)
// Otherwise, if the current encoding is 'adt-scott' it becomes:
(x λval val 0)
```
If constructor fields are not specified, we implicitly bind them based on the name given in the ADT declaration.
```rust
data Maybe = (Some value) | None
match x {
Some: x.value
None: 0
}
// Becomes:
match x {
(Some x.value): x.value
(None): 0
}
```
Nested pattern matching allows for matching and deconstructing data within complex structures.
```rust
data Tree = (Leaf value) | (Node left right)
match tree {
(Node (Leaf a) (Leaf b)): (Combine a b)
(Node left right): (Merge left right)
Leaf: (Single tree.value)
}
// Which is roughly equivalent to:
match tree {
(Node left right): match left {
(Node left.left left.right):
let left = (Node left.left left.right);
(Merge left right)
(Leaf a): match right {
(Node right.left right.right):
let left = (Leaf a);
let right = (Node right.left right.right);
(Merge left right)
(Leaf b): (Combine a b)
}
}
(Leaf value): (Single value)
}
```

4
src/lib.rs
View File

@ -71,9 +71,7 @@ pub fn desugar_book(
ctx.book.encode_adts(opts.adt_encoding);
ctx.book.resolve_ctrs_in_pats();
ctx.check_unbound_ctr()?;
ctx.check_ctrs_arities()?;
ctx.fix_match_defs()?;
ctx.apply_args(args)?;
ctx.book.apply_use();

78
src/term/check/ctrs_arities.rs
View File

@ -1,78 +0,0 @@
use std::collections::HashMap;
use crate::{
diagnostics::{Diagnostics, ToStringVerbose},
term::{Book, Ctx, Name, Pattern},
};
pub struct CtrArityMismatchErr {
ctr_name: Name,
expected: usize,
found: usize,
}
impl Ctx<'_> {
/// Checks if every constructor pattern of every definition rule
/// has the same arity from the defined adt constructor.
///
/// Constructors should be already resolved.
pub fn check_ctrs_arities(&mut self) -> Result<(), Diagnostics> {
self.info.start_pass();
let arities = self.book.ctr_arities();
for (def_name, def) in self.book.defs.iter() {
for rule in def.rules.iter() {
for pat in rule.pats.iter() {
let res = pat.check_ctrs_arities(&arities);
self.info.take_rule_err(res, def_name.clone());
}
}
}
self.info.fatal(())
}
}
impl Book {
/// Returns a hashmap of the constructor name to its arity.
pub fn ctr_arities(&self) -> HashMap<Name, usize> {
let mut arities = HashMap::new();
for adt in self.adts.values() {
for (ctr_name, fields) in adt.ctrs.iter() {
arities.insert(ctr_name.clone(), fields.len());
}
}
arities
}
}
impl Pattern {
fn check_ctrs_arities(&self, arities: &HashMap<Name, usize>) -> Result<(), CtrArityMismatchErr> {
let mut to_check = vec![self];
while let Some(pat) = to_check.pop() {
if let Pattern::Ctr(ctr_name, args) = pat {
let expected = arities.get(ctr_name).unwrap();
let found = args.len();
if *expected != found {
return Err(CtrArityMismatchErr { ctr_name: ctr_name.clone(), found, expected: *expected });
}
}
for child in pat.children() {
to_check.push(child);
}
}
Ok(())
}
}
impl ToStringVerbose for CtrArityMismatchErr {
fn to_string_verbose(&self, _verbose: bool) -> String {
format!(
"Constructor arity mismatch in pattern matching. Constructor '{}' expects {} fields, found {}.",
self.ctr_name, self.expected, self.found
)
}
}

2
src/term/check/mod.rs
View File

@ -1,5 +1,3 @@
pub mod ctrs_arities;
pub mod set_entrypoint;
pub mod shared_names;
pub mod unbound_ctrs;
pub mod unbound_vars;

56
src/term/check/unbound_ctrs.rs
View File

@ -1,56 +0,0 @@
use crate::{
diagnostics::{Diagnostics, ToStringVerbose},
term::{Ctx, Name, Pattern},
};
use std::collections::HashSet;
#[derive(Debug, Clone)]
pub struct UnboundCtrErr(Name);
impl Ctx<'_> {
/// Check if the constructors in rule patterns are defined.
/// Match terms are not checked since unbounds there are treated as vars.
pub fn check_unbound_ctr(&mut self) -> Result<(), Diagnostics> {
self.info.start_pass();
let is_ctr = |nam: &Name| self.book.ctrs.contains_key(nam);
for (def_name, def) in self.book.defs.iter() {
for rule in &def.rules {
for pat in &rule.pats {
let res = pat.check_unbounds(&is_ctr);
self.info.take_rule_err(res, def_name.clone());
}
}
}
self.info.fatal(())
}
}
impl Pattern {
pub fn check_unbounds(&self, is_ctr: &impl Fn(&Name) -> bool) -> Result<(), UnboundCtrErr> {
let unbounds = self.unbound_pats(is_ctr);
if let Some(unbound) = unbounds.iter().next() { Err(UnboundCtrErr(unbound.clone())) } else { Ok(()) }
}
/// Given a possibly nested rule pattern, return a set of all used but not declared constructors.
pub fn unbound_pats(&self, is_ctr: &impl Fn(&Name) -> bool) -> HashSet<Name> {
let mut unbounds = HashSet::new();
let mut check = vec![self];
while let Some(pat) = check.pop() {
if let Pattern::Ctr(nam, _) = pat {
if !is_ctr(nam) {
unbounds.insert(nam.clone());
}
}
check.extend(pat.children());
}
unbounds
}
}
impl ToStringVerbose for UnboundCtrErr {
fn to_string_verbose(&self, _verbose: bool) -> String {
format!("Unbound constructor '{}'.", self.0)
}
}

6
src/term/mod.rs
View File

@ -860,6 +860,12 @@ impl Name {
}
}
impl Default for Name {
fn default() -> Self {
Self::from("")
}
}
impl From<&str> for Name {
fn from(value: &str) -> Self {
Name(STRINGS.get(value))

3
src/term/transform/desugar_match_defs.rs
View File

@ -1,9 +1,8 @@
use std::collections::{BTreeSet, HashSet};
use crate::{
diagnostics::{Diagnostics, ToStringVerbose, WarningType},
term::{builtins, Adts, Constructors, Ctx, Definition, Name, NumCtr, Pattern, Rule, Term},
};
use std::collections::{BTreeSet, HashSet};
pub enum DesugarMatchDefErr {
AdtNotExhaustive { adt: Name, ctr: Name },

74
src/term/transform/fix_match_defs.rs Normal file
View File

@ -0,0 +1,74 @@
use crate::{
diagnostics::Diagnostics,
term::{Adts, Constructors, Ctx, Pattern},
};
impl Ctx<'_> {
/// Makes every pattern matching definition have correct a left-hand side.
///
/// Does not check exhaustiveness of rules and type mismatches. (Inter-ctr/type proprieties)
pub fn fix_match_defs(&mut self) -> Result<(), Diagnostics> {
self.info.start_pass();
for def in self.book.defs.values_mut() {
let mut errs = vec![];
let def_arity = def.arity();
for rule in &mut def.rules {
if rule.arity() != def_arity {
errs.push(format!(
"Incorrect pattern matching rule arity. Expected {} args, found {}.",
def_arity,
rule.arity()
));
}
for pat in &mut rule.pats {
pat.resolve_pat(&self.book.ctrs);
pat.check_good_ctr(&self.book.ctrs, &self.book.adts, &mut errs);
}
}
for err in errs {
self.info.add_rule_error(err, def.name.clone());
}
}
self.info.fatal(())
}
}
impl Pattern {
/// If a var pattern actually refers to an ADT constructor, convert it into a constructor pattern.
fn resolve_pat(&mut self, ctrs: &Constructors) {
if let Pattern::Var(Some(nam)) = self {
if ctrs.contains_key(nam) {
*self = Pattern::Ctr(std::mem::take(nam), vec![]);
}
}
for child in self.children_mut() {
child.resolve_pat(ctrs);
}
}
/// Check that ADT constructor pats are correct, meaning defined in a `data` and with correct arity.
fn check_good_ctr(&self, ctrs: &Constructors, adts: &Adts, errs: &mut Vec<String>) {
if let Pattern::Ctr(nam, args) = self {
if let Some(adt) = ctrs.get(nam) {
let expected_arity = adts[adt].ctrs[nam].len();
let found_arity = args.len();
if expected_arity != found_arity {
errs.push(format!(
"Incorrect arity for constructor '{}' of type '{}' in pattern matching rule. Expected {} fields, found {}",
nam, adt, expected_arity, found_arity
));
}
} else {
errs.push(format!("Unbound constructor '{nam}' in pattern matching rule."));
}
}
for child in self.children() {
child.check_good_ctr(ctrs, adts, errs);
}
}
}

2
src/term/transform/mod.rs
View File

@ -6,12 +6,12 @@ pub mod desugar_match_defs;
pub mod encode_adts;
pub mod encode_match_terms;
pub mod eta_reduction;
pub mod fix_match_defs;
pub mod fix_match_terms;
pub mod float_combinators;
pub mod inline;
pub mod linearize_matches;
pub mod linearize_vars;
pub mod resolve_ctrs_in_pats;
pub mod resolve_refs;
pub mod resugar_adts;
pub mod resugar_builtins;

37
src/term/transform/resolve_ctrs_in_pats.rs
View File

@ -1,37 +0,0 @@
use crate::term::{Book, Name, Pattern};
impl Book {
/// Resolve Constructor names inside rule patterns and match patterns,
/// converting `Pattern::Var(Some(nam))` into `Pattern::Ctr(nam, vec![])`
/// when the name is that of a constructor.
///
/// When parsing a rule we don't have all the constructors yet, so no way to
/// know if a particular name belongs to a constructor or is a matched variable.
/// Therefore we must do it later, here.
pub fn resolve_ctrs_in_pats(&mut self) {
let is_ctr = |nam: &Name| self.ctrs.contains_key(nam);
for def in self.defs.values_mut() {
for rule in &mut def.rules {
for pat in &mut rule.pats {
pat.resolve_ctrs(&is_ctr);
}
}
}
}
}
impl Pattern {
pub fn resolve_ctrs(&mut self, is_ctr: &impl Fn(&Name) -> bool) {
let mut to_resolve = vec![self];
while let Some(pat) = to_resolve.pop() {
if let Pattern::Var(Some(nam)) = pat {
if is_ctr(nam) {
*pat = Pattern::Ctr(nam.clone(), vec![]);
}
}
to_resolve.extend(pat.children_mut());
}
}
}

10
tests/golden_tests.rs
View File

@ -219,9 +219,8 @@ fn simplify_matches() {
ctx.check_shared_names();
ctx.set_entrypoint();
ctx.book.encode_adts(AdtEncoding::TaggedScott);
ctx.book.resolve_ctrs_in_pats();
ctx.check_unbound_ctr()?;
ctx.check_ctrs_arities()?;
ctx.fix_match_defs()?;
ctx.book.apply_use();
ctx.book.encode_builtins();
ctx.resolve_refs()?;
ctx.fix_match_terms()?;
@ -254,9 +253,8 @@ fn encode_pattern_match() {
ctx.check_shared_names();
ctx.set_entrypoint();
ctx.book.encode_adts(adt_encoding);
ctx.book.resolve_ctrs_in_pats();
ctx.check_unbound_ctr()?;
ctx.check_ctrs_arities()?;
ctx.fix_match_defs()?;
ctx.book.apply_use();
ctx.book.encode_builtins();
ctx.resolve_refs()?;
ctx.fix_match_terms()?;

2
tests/golden_tests/simplify_matches/wrong_fn_arity.hvm Normal file
View File

@ -0,0 +1,2 @@
(Foo a b c) = 0
(Foo) = 1

6
tests/snapshots/cli__debug_u60_to_nat.hvm.snap
View File

@ -4,11 +4,7 @@ input_file: tests/golden_tests/cli/debug_u60_to_nat.hvm
---
(λa (U60ToNat a) 4)
---------------------------------------
(λa switch a { 0: Z; _: (S (U60ToNat a-1)) } 4)
---------------------------------------
let b = 4; switch b { 0: Z; _: (S (U60ToNat b-1)) }
---------------------------------------
(λa λb (S (U60ToNat b)) * 3)
(U60ToNat 4)
---------------------------------------
(λa (S (U60ToNat a)) 3)
---------------------------------------

2
tests/snapshots/compile_file__nested_ctr_wrong_arity.hvm.snap
View File

@ -4,4 +4,4 @@ input_file: tests/golden_tests/compile_file/nested_ctr_wrong_arity.hvm
---
Errors:
In definition 'fst_fst':
Constructor arity mismatch in pattern matching. Constructor 'Pair' expects 2 fields, found 1.
Incorrect arity for constructor 'Pair' of type 'Pair' in pattern matching rule. Expected 2 fields, found 1

2
tests/snapshots/compile_file__wrong_ctr_arity.hvm.snap
View File

@ -4,4 +4,4 @@ input_file: tests/golden_tests/compile_file/wrong_ctr_arity.hvm
---
Errors:
In definition 'Bar':
Constructor arity mismatch in pattern matching. Constructor 'Box' expects 1 fields, found 2.
Incorrect arity for constructor 'Box' of type 'Boxed' in pattern matching rule. Expected 1 fields, found 2

2
tests/snapshots/compile_file__wrong_ctr_var_arity.hvm.snap
View File

@ -4,4 +4,4 @@ input_file: tests/golden_tests/compile_file/wrong_ctr_var_arity.hvm
---
Errors:
In definition 'foo':
Constructor arity mismatch in pattern matching. Constructor 'pair' expects 2 fields, found 0.
Incorrect arity for constructor 'pair' of type 'Tup' in pattern matching rule. Expected 2 fields, found 0

8
tests/snapshots/simplify_matches__wrong_fn_arity.hvm.snap Normal file
View File

@ -0,0 +1,8 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/simplify_matches/wrong_fn_arity.hvm
---
Errors:
File has no 'main' definition.
In definition 'Foo':
Incorrect pattern matching rule arity. Expected 3 args, found 0.