diff --git a/unison-src/transcripts/cycle-update-5.md b/unison-src/transcripts/cycle-update-5.md deleted file mode 100644 index 60d283d55..000000000 --- a/unison-src/transcripts/cycle-update-5.md +++ /dev/null @@ -1,34 +0,0 @@ -Not yet working: properly updating nameless implicit terms. - -```ucm:hide -scratch/main> builtins.merge -``` - -```unison -inner.ping : 'Nat -inner.ping _ = !pong + 1 - -pong : 'Nat -pong _ = !inner.ping + 2 -``` - -```ucm -scratch/main> add -``` - -Here we queue up an update by saving in a namespace where `inner.ping` and `pong` both have names, but then apply the -update in a namespace where only `ping` has a name. - -```unison -inner.ping : 'Nat -inner.ping _ = !pong + 3 -``` - -```ucm -.inner> update.old -scratch/main> view inner.ping -``` - -The bug here is that `inner.ping` still refers to `pong` by name. But if we properly identified the nameless (in the -context that the update was applied) `pong` as an implicit term to include in the new `ping`'s cycle, then `ping` would -be left referring to a nameless thing (namely, `pong`, but updated to refer to the new `ping`). diff --git a/unison-src/transcripts/cycle-update-5.output.md b/unison-src/transcripts/cycle-update-5.output.md deleted file mode 100644 index a42ccbde5..000000000 --- a/unison-src/transcripts/cycle-update-5.output.md +++ /dev/null @@ -1,82 +0,0 @@ -Not yet working: properly updating nameless implicit terms. - -```unison -inner.ping : 'Nat -inner.ping _ = !pong + 1 - -pong : 'Nat -pong _ = !inner.ping + 2 -``` - -```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`: - - inner.ping : 'Nat - pong : 'Nat - -``` -```ucm -scratch/main> add - - ⍟ I've added these definitions: - - inner.ping : 'Nat - pong : 'Nat - -``` -Here we queue up an update by saving in a namespace where `inner.ping` and `pong` both have names, but then apply the -update in a namespace where only `ping` has a name. - -```unison -inner.ping : 'Nat -inner.ping _ = !pong + 3 -``` - -```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 names already exist. You can `update` them to your - new definition: - - inner.ping : 'Nat - -``` -```ucm - ☝️ The namespace .inner is empty. - -.inner> update.old - - ⍟ I've added these definitions: - - inner.ping : '##Nat - -scratch/main> view inner.ping - -<<<<<<< Conflict 1 of 1 -%%%%%%% Changes from base to side #1 - inner.ping : 'Nat - inner.ping _ = - use Nat + -- !pong + 1 -+ pong() + 1 -+++++++ Contents of side #2 - inner.inner.ping : '##Nat - inner.inner.ping _ = ##Nat.+ !#4t465jk908 3 ->>>>>>> Conflict 1 of 1 ends - -``` -The bug here is that `inner.ping` still refers to `pong` by name. But if we properly identified the nameless (in the -context that the update was applied) `pong` as an implicit term to include in the new `ping`'s cycle, then `ping` would -be left referring to a nameless thing (namely, `pong`, but updated to refer to the new `ping). diff --git a/unison-src/transcripts/fix2254.output.md b/unison-src/transcripts/fix2254.output.md index fa593731b..62c83c2fa 100644 --- a/unison-src/transcripts/fix2254.output.md +++ b/unison-src/transcripts/fix2254.output.md @@ -37,7 +37,7 @@ We'll make our edits in a new branch. 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 @@ -70,84 +70,95 @@ Let's do the update now, and verify that the definitions all look good and there scratch/a2> update.old ⍟ I've updated these names to your new definition: - + type A a b c d scratch/a2> view A NeedsA f f2 f3 g -<<<<<<< Conflict 1 of 5 -%%%%%%% Changes from base to side #1 - type A a b c d -- = B b -+ = A a - | D d - | E a d -+ | B b - | C c -- | A a - - structural type NeedsA a b -- = Zoink Text -- | NeedsA (A a b Nat Nat) -+ = 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 -+++++++ Contents of side #2 - type A a b c d = B b | D d | E a d | C c | A a ->>>>>>> Conflict 1 of 5 ends + 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 : #re3rf9cedk Nat Nat Nat Nat -> Nat + f = cases + #re3rf9cedk#1 n -> n + _ -> 42 + + f2 : #re3rf9cedk Nat Nat Nat Nat -> Nat + f2 a = + use Nat + + n = f a + n + 1 + + f3 : #oftm6ao9vp Nat Nat -> Nat + f3 = cases + #oftm6ao9vp#0 a -> f a Nat.+ 20 + _ -> 0 + + g : #re3rf9cedk Nat Nat Nat Nat -> Nat + g = cases + #re3rf9cedk#0 n -> n + _ -> 43 -<<<<<<< Conflict 2 of 5 -+++++++ Contents of side #1 scratch/a2> todo -%%%%%%% Changes from base to side #2 --.a2> todo -+ ⚠️ ->>>>>>> Conflict 2 of 5 ends - The following names were not found in the codebase. Check your spelling. - NeedsA - f - f2 - f3 - g + These types do not have any names in the current namespace: + + 1. #oftm6ao9vp + 2. #re3rf9cedk ``` +## 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 -.a2> update.old.a2> view A NeedsA f f2 f3 g.a2> todo + + 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 + ``` -<<<<<<< Conflict 3 of 5 -+++++++ Contents of side #1 ```ucm scratch/r1> add -%%%%%%% Changes from base to side #2 --```ucm --.a3> add ->>>>>>> Conflict 3 of 5 ends + ⍟ 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 -<<<<<<< Conflict 4 of 5 -+++++++ Contents of side #1 scratch/r1> branch r2 Done. I've created the r2 branch based off of r1. @@ -159,57 +170,56 @@ scratch/r1> branch r2 ```unison structural type Rec = { uno : Nat, dos : Nat, tres : Text } ``` -%%%%%%% Changes from base to side #2 --``` --```unison --structural type Rec = { uno : Nat, dos : Nat, tres : Text } --``` -+🛑 ->>>>>>> Conflict 4 of 5 ends -The transcript failed due to an error in the stanza above. The error is: +```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 - The following names were not found in the codebase. Check your spelling. - NeedsA - f - f2 - f3 - g +``` +And checking that after updating this record, there's nothing `todo`: -<<<<<<< Conflict 5 of 5 -%%%%%%% Changes from base to side #1 - ```ucm --.> fork a3 a4 -+scratch/r2> update.old - -- Done. -- --.a4> 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 - --.a4> todo -+scratch/r2> todo - - - - ``` -+++++++ Contents of side #2 ->>>>>>> Conflict 5 of 5 ends +```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 + + + +``` diff --git a/unison-src/transcripts/propagate.md b/unison-src/transcripts/propagate.md index b5eaf3ede..19576d8bb 100644 --- a/unison-src/transcripts/propagate.md +++ b/unison-src/transcripts/propagate.md @@ -78,47 +78,3 @@ type of `otherTerm` should remain the same. scratch/main> view preserve.someTerm scratch/main> view preserve.otherTerm ``` - -### Propagation only applies to the local branch - -Cleaning up a bit... - -```ucm -.subpath.lib> builtins.merge -``` - -Now, we make two terms, where one depends on the other. - -```unison -one.someTerm : Optional foo -> Optional foo -one.someTerm x = x - -one.otherTerm : Optional baz -> Optional baz -one.otherTerm y = someTerm y -``` - -We'll make two copies of this namespace. - -```ucm -.subpath> add -.subpath> fork one two -``` - -Now let's edit one of the terms... - -```unison -someTerm : Optional x -> Optional x -someTerm _ = None -``` - -... in one of the namespaces... - -```ucm -.subpath.one> update.old -``` - -The other namespace should be left alone. - -```ucm -.subpath> view two.someTerm -``` diff --git a/unison-src/transcripts/propagate.output.md b/unison-src/transcripts/propagate.output.md index 10f159d2a..694b99cd0 100644 --- a/unison-src/transcripts/propagate.output.md +++ b/unison-src/transcripts/propagate.output.md @@ -87,178 +87,91 @@ scratch/main> update.old ```ucm scratch/main> view fooToInt - ⚠️ - - The following names were not found in the codebase. Check your spelling. - fooToInt + fooToInt : Foo -> Int + fooToInt _ = +42 ``` +### Preserving user type variables + +We make a term that has a dependency on another term and also a non-redundant +user-provided type signature. + +```unison +preserve.someTerm : Optional foo -> Optional foo +preserve.someTerm x = x + +preserve.otherTerm : Optional baz -> Optional baz +preserve.otherTerm y = someTerm y +``` + +```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`: + + preserve.otherTerm : Optional baz -> Optional baz + preserve.someTerm : Optional foo -> Optional foo + +``` +Add that to the codebase: -<<<<<<< Conflict 1 of 2 -+++++++ Contents of side #1 ```ucm scratch/main> add -%%%%%%% Changes from base to side #2 --```ucm --.subpath> add ->>>>>>> Conflict 1 of 2 ends - -🛑 - -The transcript failed due to an error in the stanza above. The error is: - - - ⚠️ + ⍟ I've added these definitions: - The following names were not found in the codebase. Check your spelling. - fooToInt + preserve.otherTerm : Optional baz -> Optional baz + preserve.someTerm : Optional foo -> Optional foo -<<<<<<< Conflict 2 of 2 -%%%%%%% Changes from base to side #1 - ``` - Let's now edit the dependency: - - ```unison - preserve.someTerm : Optional x -> Optional x - preserve.someTerm _ = None - ``` - - ```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 names already exist. You can `update` them to your - new definition: - - preserve.someTerm : Optional x -> Optional x - - ``` - Update... - - ```ucm --.subpath> update.old -+scratch/main> update.old - - ⍟ I've updated these names to your new definition: - - preserve.someTerm : Optional x -> Optional x - - ``` - Now the type of `someTerm` should be `Optional x -> Optional x` and the - type of `otherTerm` should remain the same. - - ```ucm --.subpath> view preserve.someTerm -+scratch/main> view preserve.someTerm - - preserve.someTerm : Optional x -> Optional x - preserve.someTerm _ = None - --.subpath> view preserve.otherTerm -+scratch/main> view preserve.otherTerm - - preserve.otherTerm : Optional baz -> Optional baz - preserve.otherTerm y = someTerm y - - ``` - ### Propagation only applies to the local branch - - Cleaning up a bit... - - ```ucm --.> delete.namespace subpath -- -- Done. -- - ☝️ The namespace .subpath.lib is empty. - - .subpath.lib> builtins.merge - - Done. - - ``` - Now, we make two terms, where one depends on the other. - - ```unison - one.someTerm : Optional foo -> Optional foo - one.someTerm x = x - - one.otherTerm : Optional baz -> Optional baz - one.otherTerm y = someTerm y - ``` - - ```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`: - - one.otherTerm : Optional baz -> Optional baz - one.someTerm : Optional foo -> Optional foo - - ``` - We'll make two copies of this namespace. - - ```ucm - .subpath> add - - ⍟ I've added these definitions: - - one.otherTerm : Optional baz -> Optional baz - one.someTerm : Optional foo -> Optional foo - - .subpath> fork one two - - Done. - - ``` - Now let's edit one of the terms... - - ```unison - someTerm : Optional x -> Optional x - someTerm _ = None - ``` - - ```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`: - - someTerm : Optional x -> Optional x - - ``` - ... in one of the namespaces... - - ```ucm - .subpath.one> update.old - - ⍟ I've updated these names to your new definition: - - someTerm : #nirp5os0q6 x -> #nirp5os0q6 x - - ``` - The other namespace should be left alone. - - ```ucm - .subpath> view two.someTerm - - two.someTerm : Optional foo -> Optional foo - two.someTerm x = x - - ``` -+++++++ Contents of side #2 ->>>>>>> Conflict 2 of 2 ends +``` +Let's now edit the dependency: + +```unison +preserve.someTerm : Optional x -> Optional x +preserve.someTerm _ = None +``` + +```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 names already exist. You can `update` them to your + new definition: + + preserve.someTerm : Optional x -> Optional x + +``` +Update... + +```ucm +scratch/main> update.old + + ⍟ I've updated these names to your new definition: + + preserve.someTerm : Optional x -> Optional x + +``` +Now the type of `someTerm` should be `Optional x -> Optional x` and the +type of `otherTerm` should remain the same. + +```ucm +scratch/main> view preserve.someTerm + + preserve.someTerm : Optional x -> Optional x + preserve.someTerm _ = None + +scratch/main> view preserve.otherTerm + + preserve.otherTerm : Optional baz -> Optional baz + preserve.otherTerm y = someTerm y + +```