mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
220 lines
4.6 KiB
Markdown
220 lines
4.6 KiB
Markdown
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
|
|
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
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
type A a b c d
|
|
structural type NeedsA a b
|
|
f : A Nat Nat Nat Nat -> Nat
|
|
f2 : A Nat Nat Nat Nat -> Nat
|
|
f3 : NeedsA Nat Nat -> Nat
|
|
g : A Nat Nat Nat Nat -> Nat
|
|
|
|
scratch/a> branch /a2
|
|
|
|
Done. I've created the a2 branch based off of a.
|
|
|
|
Tip: To merge your work back into the a branch, first
|
|
`switch /a` then `merge /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
|
|
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
|
|
|
|
Okay, I'm searching the branch for code that needs to be
|
|
updated...
|
|
|
|
That's done. Now I'm making sure everything typechecks...
|
|
|
|
Everything typechecks, so I'm saving the results...
|
|
|
|
Done.
|
|
|
|
scratch/a2> view A NeedsA f f2 f3 g
|
|
|
|
type A a b c d
|
|
= A a
|
|
| D d
|
|
| E a d
|
|
| B b
|
|
| C c
|
|
|
|
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 Nat Nat Nat Nat -> Nat
|
|
f2 a =
|
|
use Nat +
|
|
n = f a
|
|
n + 1
|
|
|
|
f3 : NeedsA Nat Nat -> Nat
|
|
f3 = cases
|
|
NeedsA a -> f a Nat.+ 20
|
|
_ -> 0
|
|
|
|
g : A Nat Nat Nat Nat -> Nat
|
|
g = cases
|
|
D n -> n
|
|
_ -> 43
|
|
|
|
scratch/a2> todo
|
|
|
|
You have no pending todo items. Good work! ✅
|
|
|
|
```
|
|
## Record updates
|
|
|
|
Here's a test of updating a record:
|
|
|
|
``` unison
|
|
structural type Rec = { uno : Nat, dos : Nat }
|
|
|
|
combine r = uno r + dos r
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
structural type Rec
|
|
Rec.dos : Rec -> Nat
|
|
Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
|
|
Rec.dos.set : Nat -> Rec -> Rec
|
|
Rec.uno : Rec -> Nat
|
|
Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
|
|
Rec.uno.set : Nat -> Rec -> Rec
|
|
combine : Rec -> Nat
|
|
|
|
```
|
|
``` ucm
|
|
scratch/r1> add
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
structural type Rec
|
|
Rec.dos : Rec -> Nat
|
|
Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
|
|
Rec.dos.set : Nat -> Rec -> Rec
|
|
Rec.uno : Rec -> Nat
|
|
Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
|
|
Rec.uno.set : Nat -> Rec -> Rec
|
|
combine : Rec -> Nat
|
|
|
|
scratch/r1> branch r2
|
|
|
|
Done. I've created the r2 branch based off of r1.
|
|
|
|
Tip: To merge your work back into the r1 branch, first
|
|
`switch /r1` then `merge /r2`.
|
|
|
|
```
|
|
``` unison
|
|
structural type Rec = { uno : Nat, dos : Nat, tres : Text }
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
do an `add` or `update`, here's how your codebase would
|
|
change:
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
Rec.tres : Rec -> Text
|
|
Rec.tres.modify : (Text ->{g} Text) -> Rec ->{g} Rec
|
|
Rec.tres.set : Text -> Rec -> Rec
|
|
|
|
⍟ These names already exist. You can `update` them to your
|
|
new definition:
|
|
|
|
structural type Rec
|
|
Rec.dos : Rec -> Nat
|
|
Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
|
|
Rec.dos.set : Nat -> Rec -> Rec
|
|
Rec.uno : Rec -> Nat
|
|
Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
|
|
Rec.uno.set : Nat -> Rec -> Rec
|
|
|
|
```
|
|
And checking that after updating this record, there's nothing `todo`:
|
|
|
|
``` ucm
|
|
scratch/r2> update
|
|
|
|
Okay, I'm searching the branch for code that needs to be
|
|
updated...
|
|
|
|
That's done. Now I'm making sure everything typechecks...
|
|
|
|
Everything typechecks, so I'm saving the results...
|
|
|
|
Done.
|
|
|
|
scratch/r2> todo
|
|
|
|
You have no pending todo items. Good work! ✅
|
|
|
|
```
|