From 35f7a77cce768eb730b0a1daa207c51f2a3fd767 Mon Sep 17 00:00:00 2001 From: imaqtkatt Date: Wed, 28 Feb 2024 15:29:08 -0300 Subject: [PATCH 1/4] Add pattern matching documentation --- README.md | 1 + docs/pattern-matching.md | 152 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 153 insertions(+) create mode 100644 docs/pattern-matching.md diff --git a/README.md b/README.md index 6e43c1d14..cb0142fc2 100644 --- a/README.md +++ b/README.md @@ -191,6 +191,7 @@ Other features are described in the following documentation files: - 📗 Lazy definitions: [Making recursive definitions lazy](docs/lazy-definitions.md) - 📗 Data types: [Defining data types](docs/defining-data-types.md) +- 📗 Pattern matching: [Pattern matching](docs/pattern-matching.md) - 📗 Native numbers and operations: [Native numbers](docs/native-numbers.md) - 📗 Builtin definitions: [Builtin definitions](docs/builtin-defs.md) - 📙 Duplications and superpositions: [Dups and sups](docs/dups-and-sups.md) diff --git a/docs/pattern-matching.md b/docs/pattern-matching.md new file mode 100644 index 000000000..4b3ff5c82 --- /dev/null +++ b/docs/pattern-matching.md @@ -0,0 +1,152 @@ +# Pattern Matching + +HVM-Lang offers pattern matching capabilities. You can use pattern matching in defining rules and with the `match` expression. + +In example, definitions are a syntax sugar to match expressions: +```rust +(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 = @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 numers has two forms. +With the successor pattern it will expect a sequence of numbers up to the `n+var` pattern: +```rust +match n { + 0: A + 1: B + ... + n+var: (N var) +} + +// Becomes: +match n { + 0: A + 1+p: match p { + ... + 1+var: (N var) + } +} +``` + +With the wildcard pattern you can use any number freely: +```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) + } +} +``` + +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) = (1, 2); 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) +``` + +Pattern matching on strings and lists desugars to a list of matches on List/String.cons and List.String.nil +```rust +Hi "hi" = 1 +Hi _ = 0 + +Foo [] = 0 +Foo [x] = x +Foo _ = 3 + +// Becomes: +Hi (String.cons 'h' (String.cons 'i' String.nil)) = 2 +Hi _ = 0 + +Foo List.nil = 0 +Foo (List.cons x List.nil) = x +Foo _ = 3 +``` + +Match on ADT constructors can change based on the current 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) +} + +// Becomes: +match tree { + (Node left right): match left { + (Leaf a): match right { + (Leaf b): (Combine a b) + _: (Merge left right) + } + _: (Merge left right) + } + (Leaf value): (Single value) +} +``` From bca59073c78b5c1afbeeeef44965d40ef8d3506f Mon Sep 17 00:00:00 2001 From: imaqtkatt Date: Wed, 28 Feb 2024 15:35:57 -0300 Subject: [PATCH 2/4] Fix typo and update word list --- cspell.json | 1 + docs/pattern-matching.md | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/cspell.json b/cspell.json index 7bd1f52e8..f62387d74 100644 --- a/cspell.json +++ b/cspell.json @@ -15,6 +15,7 @@ "ctrs", "datatypes", "desugared", + "desugars", "dref", "dups", "effectful", diff --git a/docs/pattern-matching.md b/docs/pattern-matching.md index 4b3ff5c82..c9acc47a1 100644 --- a/docs/pattern-matching.md +++ b/docs/pattern-matching.md @@ -17,7 +17,7 @@ Foo = @arg1 @arg2 @arg3 match arg1 arg2 arg3 { } ``` -Pattern matching on numers has two forms. +Pattern matching on numbers has two forms. With the successor pattern it will expect a sequence of numbers up to the `n+var` pattern: ```rust match n { From 09a6e1e8ce863d848afa97be9c4409680c9b434b Mon Sep 17 00:00:00 2001 From: imaqtkatt Date: Wed, 28 Feb 2024 17:50:52 -0300 Subject: [PATCH 3/4] WIP improve pattern matching docs --- docs/pattern-matching.md | 52 +++++++++++++++++++++++++++++++--------- 1 file changed, 41 insertions(+), 11 deletions(-) diff --git a/docs/pattern-matching.md b/docs/pattern-matching.md index c9acc47a1..bc541d679 100644 --- a/docs/pattern-matching.md +++ b/docs/pattern-matching.md @@ -1,15 +1,17 @@ # Pattern Matching -HVM-Lang offers pattern matching capabilities. You can use pattern matching in defining rules and with the `match` expression. +HVM-Lang offers pattern matching capabilities. You can use pattern matching in function definitions and with the `match` expression. + +Pattern matching definitions are just a syntax sugar to match expressions: -In example, definitions are a syntax sugar to match expressions: ```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 = @arg1 @arg2 @arg3 match arg1 arg2 arg3 { +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 @@ -18,8 +20,16 @@ Foo = @arg1 @arg2 @arg3 match arg1 arg2 arg3 { ``` Pattern matching on numbers has two forms. -With the successor pattern it will expect a sequence of numbers up to the `n+var` pattern: +With the successor pattern `n+var` it will expect to cover every case up to `n`: + ```rust +// Error: Case '2' not covered. +match n { + 1: B; + 0: A; + 3+: ...; +} + match n { 0: A 1: B @@ -38,6 +48,7 @@ match n { ``` With the wildcard pattern you can use any number freely: + ```rust match n { 23: A @@ -58,17 +69,27 @@ match (- n 32) { } ``` +Notice that this definition is valid, since `*` will cover both `1+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) = (1, 2); s +let (f, s) = x; s ``` Match on vars becomes a rebinding of the variable with a let expression. + ```rust match x { c: (Some c) @@ -78,7 +99,8 @@ match x { let c = x; (Some c) ``` -Pattern matching on strings and lists desugars to a list of matches on List/String.cons and List.String.nil +Pattern matching on strings and lists desugars to a list of matches on List/String.cons and List/String.nil + ```rust Hi "hi" = 1 Hi _ = 0 @@ -96,7 +118,8 @@ Foo (List.cons x List.nil) = x Foo _ = 3 ``` -Match on ADT constructors can change based on the current encoding. +Matches on ADT constructors are compiled to different expressions depending on the chosen encoding. + ```rust data Maybe = (Some val) | None @@ -109,10 +132,11 @@ match x { #Maybe (x #Maybe.Some.val λval val 0) // Otherwise, if the current encoding is 'adt-scott' it becomes: -(x @val val 0) +(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 @@ -129,6 +153,7 @@ match x { ``` Nested pattern matching allows for matching and deconstructing data within complex structures. + ```rust data Tree = (Leaf value) | (Node left right) @@ -138,14 +163,19 @@ match tree { Leaf: (Single tree.value) } -// Becomes: +// 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) - _: (Merge left right) } - _: (Merge left right) } (Leaf value): (Single value) } From 13b9036b9db5f1b3e43f6cbc7edc33b2a27b4bac Mon Sep 17 00:00:00 2001 From: imaqtkatt Date: Thu, 29 Feb 2024 09:38:33 -0300 Subject: [PATCH 4/4] WIP improve pattern matching docs --- docs/pattern-matching.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/docs/pattern-matching.md b/docs/pattern-matching.md index bc541d679..0fb3ce4ce 100644 --- a/docs/pattern-matching.md +++ b/docs/pattern-matching.md @@ -23,13 +23,6 @@ Pattern matching on numbers has two forms. With the successor pattern `n+var` it will expect to cover every case up to `n`: ```rust -// Error: Case '2' not covered. -match n { - 1: B; - 0: A; - 3+: ...; -} - match n { 0: A 1: B @@ -45,6 +38,13 @@ match n { 1+var: (N var) } } + +// Error: Case '2' not covered. +match n { + 1: B; + 0: A; + 3+: ...; +} ``` With the wildcard pattern you can use any number freely: