mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 10:35:57 +03:00
95 lines
1.6 KiB
Markdown
95 lines
1.6 KiB
Markdown
|
|
```ucm:hide
|
|
scratch/a> builtins.merge lib.builtins
|
|
```
|
|
|
|
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:
|
|
|
|
```unison:hide
|
|
unique type A a b c d
|
|
= A a
|
|
| B b
|
|
| C c
|
|
| D d
|
|
|
|
structural type NeedsA a b = NeedsA (A a b Nat Nat)
|
|
| Zoink Text
|
|
|
|
f : A Nat Nat Nat Nat -> Nat
|
|
f = cases
|
|
A n -> n
|
|
_ -> 42
|
|
|
|
f2 a =
|
|
n = f a
|
|
n + 1
|
|
|
|
f3 : NeedsA Nat Nat -> Nat
|
|
f3 = cases
|
|
NeedsA a -> f a + 20
|
|
_ -> 0
|
|
|
|
g : A Nat Nat Nat Nat -> Nat
|
|
g = cases
|
|
D n -> n
|
|
_ -> 43
|
|
```
|
|
|
|
We'll make our edits in a new branch.
|
|
|
|
```ucm
|
|
scratch/a> add
|
|
scratch/a> branch /a2
|
|
scratch/a2>
|
|
```
|
|
|
|
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
|
|
= A a
|
|
| B b
|
|
| C c
|
|
| D d
|
|
| E a d
|
|
```
|
|
|
|
Let's do the update now, and verify that the definitions all look good and there's nothing `todo`:
|
|
|
|
```ucm
|
|
scratch/a2> update
|
|
scratch/a2> view A NeedsA f f2 f3 g
|
|
scratch/a2> todo
|
|
```
|
|
|
|
## Record updates
|
|
|
|
Here's a test of updating a record:
|
|
|
|
```ucm:hide
|
|
scratch/r1> builtins.merge lib.builtins
|
|
```
|
|
|
|
|
|
```unison
|
|
structural type Rec = { uno : Nat, dos : Nat }
|
|
|
|
combine r = uno r + dos r
|
|
```
|
|
|
|
```ucm
|
|
scratch/r1> add
|
|
scratch/r1> branch r2
|
|
```
|
|
|
|
```unison
|
|
structural type Rec = { uno : Nat, dos : Nat, tres : Text }
|
|
```
|
|
|
|
And checking that after updating this record, there's nothing `todo`:
|
|
|
|
```ucm
|
|
scratch/r2> update
|
|
scratch/r2> todo
|
|
```
|