Port fix2254 to new update

This commit is contained in:
Chris Penner 2024-07-11 12:45:18 -07:00
parent 1e4f1abe73
commit 670b0868b9
2 changed files with 33 additions and 38 deletions

View File

@ -39,7 +39,7 @@ We'll make our edits in a new branch.
```ucm
scratch/a> add
scratch/a> branch a2
scratch/a> branch /a2
scratch/a2>
```
@ -57,7 +57,7 @@ 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
scratch/a2> update.old
scratch/a2> update
scratch/a2> view A NeedsA f f2 f3 g
scratch/a2> todo
```
@ -89,6 +89,6 @@ structural type Rec = { uno : Nat, dos : Nat, tres : Text }
And checking that after updating this record, there's nothing `todo`:
```ucm
scratch/r2> update.old
scratch/r2> update
scratch/r2> todo
```

View File

@ -44,7 +44,7 @@ scratch/a> add
f3 : NeedsA Nat Nat -> Nat
g : A Nat Nat Nat Nat -> Nat
scratch/a> branch a2
scratch/a> branch /a2
Done. I've created the a2 branch based off of a.
@ -66,11 +66,16 @@ 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
scratch/a2> update.old
scratch/a2> update
⍟ I've updated these names to your new definition:
type A a b c d
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
@ -85,33 +90,30 @@ scratch/a2> view A NeedsA f f2 f3 g
= NeedsA (A a b Nat Nat)
| Zoink Text
f : #re3rf9cedk Nat Nat Nat Nat -> Nat
f : A Nat Nat Nat Nat -> Nat
f = cases
#re3rf9cedk#1 n -> n
_ -> 42
A n -> n
_ -> 42
f2 : #re3rf9cedk Nat Nat Nat Nat -> Nat
f2 : A Nat Nat Nat Nat -> Nat
f2 a =
use Nat +
n = f a
n + 1
f3 : #oftm6ao9vp Nat Nat -> Nat
f3 : NeedsA Nat Nat -> Nat
f3 = cases
#oftm6ao9vp#0 a -> f a Nat.+ 20
_ -> 0
NeedsA a -> f a Nat.+ 20
_ -> 0
g : #re3rf9cedk Nat Nat Nat Nat -> Nat
g : A Nat Nat Nat Nat -> Nat
g = cases
#re3rf9cedk#0 n -> n
_ -> 43
D n -> n
_ -> 43
scratch/a2> todo
These types do not have any names in the current namespace:
1. #oftm6ao9vp
2. #re3rf9cedk
You have no pending todo items. Good work! ✅
```
## Record updates
@ -199,23 +201,16 @@ structural type Rec = { uno : Nat, dos : Nat, tres : Text }
And checking that after updating this record, there's nothing `todo`:
``` ucm
scratch/r2> update.old
scratch/r2> update
⍟ 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
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