unison/unison-src/transcripts/fix2254.md

97 lines
1.5 KiB
Markdown
Raw Normal View History

2021-07-21 00:41:59 +03:00
```ucm:hide
2024-01-12 20:39:18 +03:00
.a> builtins.merge
2021-07-21 00:41:59 +03:00
```
2021-07-23 18:46:51 +03:00
This transcript checks that updates to data types propagate successfully to dependent types and dependent terms that do pattern matching. First let's create some types and terms:
2021-07-21 00:41:59 +03:00
```unison:hide
unique type A a b c d
2021-07-21 00:41:59 +03:00
= A a
| B b
| C c
| D d
2021-08-24 00:05:37 +03:00
structural type NeedsA a b = NeedsA (A a b Nat Nat)
2021-07-23 17:47:48 +03:00
| Zoink Text
2021-07-22 23:52:39 +03:00
2021-07-21 00:41:59 +03:00
f : A Nat Nat Nat Nat -> Nat
f = cases
A n -> n
_ -> 42
f2 a =
n = f a
n + 1
2021-07-22 23:52:39 +03:00
f3 : NeedsA Nat Nat -> Nat
f3 = cases
NeedsA a -> f a + 20
2021-07-23 17:47:48 +03:00
_ -> 0
2021-07-22 23:52:39 +03:00
2021-07-21 00:41:59 +03:00
g : A Nat Nat Nat Nat -> Nat
g = cases
D n -> n
_ -> 43
```
2021-07-23 18:46:51 +03:00
We'll make our edits in a fork of the `a` namespace:
2021-07-21 00:41:59 +03:00
```ucm
.a> add
.> fork a a2
```
2021-07-23 18:46:51 +03:00
First let's edit the `A` type, adding another constructor `E`. Note that the functions written against the old type have a wildcard in their pattern match, so they should work fine after the update.
```unison:hide
unique type A a b c d
2021-07-21 00:41:59 +03:00
= A a
| B b
| C c
| D d
| E a d
```
2021-07-23 18:46:51 +03:00
Let's do the update now, and verify that the definitions all look good and there's nothing `todo`:
2021-07-21 00:41:59 +03:00
```ucm
2023-11-08 19:54:50 +03:00
.a2> update.old
.a2> view A NeedsA f f2 f3 g
2021-07-21 00:41:59 +03:00
.a2> todo
```
2022-04-07 00:12:07 +03:00
```ucm:hide
.a2> builtins.merge
```
2021-07-23 18:46:51 +03:00
## Record updates
Here's a test of updating a record:
```unison
2021-08-24 00:05:37 +03:00
structural type Rec = { uno : Nat, dos : Nat }
combine r = uno r + dos r
```
2022-04-07 00:12:07 +03:00
```ucm:hide
.a3> builtins.merge
```
2024-01-12 20:39:18 +03:00
```ucm
.a3> add
```
```unison
2021-08-24 00:05:37 +03:00
structural type Rec = { uno : Nat, dos : Nat, tres : Text }
```
2021-07-23 18:46:51 +03:00
And checking that after updating this record, there's nothing `todo`:
```ucm
2021-07-23 18:46:51 +03:00
.> fork a3 a4
2023-11-08 19:54:50 +03:00
.a4> update.old
2021-07-23 18:46:51 +03:00
.a4> todo
```