unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-09-11 02:25:39 +03:00
Code Issues Projects Releases Wiki Activity

Port fix2243.md to projects

Browse Source
This commit is contained in:
Chris Penner 2024-06-26 11:12:15 -07:00
parent f71008b6a2
commit f3503cca97
2 changed files with 184 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
unison-src/transcripts/fix2254.md
View File

@ -1,6 +1,6 @@
```ucm:hide
scratch/main a> builtins.merge
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:
@ -35,11 +35,12 @@ g = cases
_ -> 43
```
We'll make our edits in a fork of the `a` namespace:
We'll make our edits in a new branch.
```ucm
scratch/main a> add
scratch/main> fork a a2
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.
@ -56,31 +57,29 @@ unique type A a b c d
Let's do the update now, and verify that the definitions all look good and there's nothing `todo`:
```ucm
.a2> update.old
.a2> view A NeedsA f f2 f3 g
.a2> todo
```
```ucm:hide
.a2> builtins.merge
scratch/a2> update.old
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:hide
.a3> builtins.merge
```
```ucm
.a3> add
scratch/r1> add
scratch/r1> branch r2
```
```unison
@ -90,7 +89,6 @@ structural type Rec = { uno : Nat, dos : Nat, tres : Text }
And checking that after updating this record, there's nothing `todo`:
```ucm
scratch/main> fork a3 a4
.a4> update.old
.a4> todo
scratch/r2> update.old
scratch/r2> todo
```

178
unison-src/transcripts/fix2254.output.md
View File

@ -31,13 +31,13 @@ g = cases
_ -> 43
```
We'll make our edits in a fork of the `a` namespace:
We'll make our edits in a new branch.
```ucm
scratch/main a> add
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
@ -45,22 +45,178 @@ scratch/main a> add
f3 : NeedsA Nat Nat -> Nat
g : A Nat Nat Nat Nat -> Nat
scratch/main> fork a a2
scratch/a> branch a2
⚠️
The namespace .__projects._ae607e42_8e50_43fc_bd62_57e211b16316.branches._04b92376_f428_4b46_8d52_c83ba75c6a15.a doesn't exist.
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.old
The transcript failed due to an error in the stanza above. The error is:
⍟ I've updated these names to your new definition:
type A a b c d
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
The namespace .__projects._ae607e42_8e50_43fc_bd62_57e211b16316.branches._04b92376_f428_4b46_8d52_c83ba75c6a15.a doesn't exist.
scratch/a2> todo
```
## 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.old
⍟ I've added these definitions:
Rec.tres : Rec -> Text
Rec.tres.modify : (Text ->{g} Text) -> Rec ->{g} Rec
Rec.tres.set : Text -> Rec -> Rec
⍟ I've updated these names 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
scratch/r2> todo
```