2019-12-08 23:24:17 +03:00
|
|
|
# Delete
|
|
|
|
|
2020-07-27 03:38:03 +03:00
|
|
|
The delete command can delete both terms and types.
|
2019-12-08 23:24:17 +03:00
|
|
|
|
|
|
|
First, let's make sure it complains when we try to delete a name that doesn't
|
|
|
|
exist.
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
|
|
|
⚠️
|
|
|
|
|
2023-02-03 09:50:11 +03:00
|
|
|
The following names were not found in the codebase. Check your spelling.
|
|
|
|
foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
|
|
|
```
|
|
|
|
Now for some easy cases. Deleting an unambiguous term, then deleting an
|
|
|
|
unambiguous type.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2019-12-08 23:24:17 +03:00
|
|
|
foo = 1
|
2022-04-07 00:20:44 +03:00
|
|
|
structural type Foo = Foo ()
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2019-12-08 23:24:17 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
2021-08-24 00:05:37 +03:00
|
|
|
structural type Foo
|
2019-12-08 23:24:17 +03:00
|
|
|
foo : Nat
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2022-12-07 22:46:32 +03:00
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. foo : Nat
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2019-12-15 05:47:15 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose Foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2022-12-07 22:46:32 +03:00
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. structural type Foo
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2019-12-15 05:47:15 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose Foo.Foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2022-12-07 22:46:32 +03:00
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. Foo.Foo : '#089vmor9c5
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2019-12-15 05:47:15 +03:00
|
|
|
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
|
|
|
How about an ambiguous term?
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2024-07-02 08:14:16 +03:00
|
|
|
a.foo = 1
|
|
|
|
a.bar = 2
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2019-12-08 23:24:17 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
a.bar : Nat
|
|
|
|
a.foo : Nat
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> debug.alias.term.force a.bar a.foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2024-06-27 18:12:21 +03:00
|
|
|
Done.
|
2023-05-17 20:36:58 +03:00
|
|
|
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
2020-07-27 03:38:03 +03:00
|
|
|
A delete should remove both versions of the term.
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose a.foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2022-12-07 22:46:32 +03:00
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. a.foo#gjmq673r1v : Nat
|
|
|
|
|
|
|
|
Name changes:
|
|
|
|
|
|
|
|
Original Changes
|
2024-06-27 18:12:21 +03:00
|
|
|
2. a.bar ┐ 3. a.foo#dcgdua2lj6 (removed)
|
2022-12-07 22:46:32 +03:00
|
|
|
4. a.foo#dcgdua2lj6 ┘
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2019-12-15 05:47:15 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> ls a
|
2020-03-10 05:27:01 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
1. bar (Nat)
|
2020-03-10 05:27:01 +03:00
|
|
|
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
|
|
|
Let's repeat all that on a type, for completeness.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2024-07-02 08:14:16 +03:00
|
|
|
structural type a.Foo = Foo ()
|
|
|
|
structural type a.Bar = Bar
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2019-12-08 23:24:17 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
structural type a.Bar
|
|
|
|
(also named lib.builtins.Unit)
|
|
|
|
structural type a.Foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> debug.alias.type.force a.Bar a.Foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2024-06-27 18:12:21 +03:00
|
|
|
Done.
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose a.Foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2022-12-07 22:46:32 +03:00
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. structural type a.Foo#089vmor9c5
|
|
|
|
|
|
|
|
Name changes:
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
Original Changes
|
|
|
|
2. a.Bar ┐ 3. a.Foo#00nv2kob8f (removed)
|
|
|
|
4. lib.builtins.Unit │
|
|
|
|
5. a.Foo#00nv2kob8f ┘
|
2022-12-07 22:46:32 +03:00
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2019-12-15 05:47:15 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose a.Foo.Foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2022-12-07 22:46:32 +03:00
|
|
|
Removed definitions:
|
|
|
|
|
2024-06-27 18:12:21 +03:00
|
|
|
1. a.Foo.Foo : '#089vmor9c5
|
2022-12-07 22:46:32 +03:00
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2019-12-15 05:47:15 +03:00
|
|
|
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
|
|
|
Finally, let's try to delete a term and a type with the same name.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2019-12-08 23:24:17 +03:00
|
|
|
foo = 1
|
2022-04-07 00:20:44 +03:00
|
|
|
structural type foo = Foo ()
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2019-12-08 23:24:17 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
2021-08-24 00:05:37 +03:00
|
|
|
structural type foo
|
2019-12-08 23:24:17 +03:00
|
|
|
foo : Nat
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose foo
|
2019-12-08 23:24:17 +03:00
|
|
|
|
2022-12-07 22:46:32 +03:00
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. structural type foo
|
|
|
|
2. foo : Nat
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2019-12-15 05:47:15 +03:00
|
|
|
|
2019-12-08 23:24:17 +03:00
|
|
|
```
|
2023-02-03 03:50:01 +03:00
|
|
|
We want to be able to delete multiple terms at once
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-02-03 03:50:01 +03:00
|
|
|
a = "a"
|
|
|
|
b = "b"
|
|
|
|
c = "c"
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
a : Text
|
|
|
|
b : Text
|
|
|
|
c : Text
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose a b c
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. a : Text
|
|
|
|
2. b : Text
|
|
|
|
3. c : Text
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
```
|
|
|
|
We can delete terms and types in the same invocation of delete
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-02-03 03:50:01 +03:00
|
|
|
structural type Foo = Foo ()
|
|
|
|
a = "a"
|
|
|
|
b = "b"
|
|
|
|
c = "c"
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
structural type Foo
|
|
|
|
a : Text
|
|
|
|
b : Text
|
|
|
|
c : Text
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose a b c Foo
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. structural type Foo
|
|
|
|
2. a : Text
|
|
|
|
3. b : Text
|
|
|
|
4. c : Text
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2023-02-03 03:50:01 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose Foo.Foo
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
Name changes:
|
|
|
|
|
|
|
|
Original Changes
|
|
|
|
1. Foo.Foo ┐ 2. Foo.Foo (removed)
|
|
|
|
3. foo.Foo ┘
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
```
|
|
|
|
We can delete a type and its constructors
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-02-03 03:50:01 +03:00
|
|
|
structural type Foo = Foo ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
structural type Foo
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose Foo Foo.Foo
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. structural type Foo
|
|
|
|
|
|
|
|
Name changes:
|
|
|
|
|
|
|
|
Original Changes
|
|
|
|
2. Foo.Foo ┐ 3. Foo.Foo (removed)
|
|
|
|
4. foo.Foo ┘
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
```
|
|
|
|
You should not be able to delete terms which are referenced by other terms
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-02-03 03:50:01 +03:00
|
|
|
a = 1
|
|
|
|
b = 2
|
|
|
|
c = 3
|
|
|
|
d = a + b + c
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
a : Nat
|
|
|
|
b : Nat
|
2024-06-27 18:12:21 +03:00
|
|
|
(also named a.bar)
|
2023-02-03 03:50:01 +03:00
|
|
|
c : Nat
|
|
|
|
d : Nat
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose a b c
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
⚠️
|
|
|
|
|
|
|
|
I didn't delete the following definitions because they are
|
|
|
|
still in use:
|
|
|
|
|
|
|
|
Dependency Referenced In
|
|
|
|
c 1. d
|
|
|
|
|
|
|
|
a 2. d
|
|
|
|
|
|
|
|
```
|
2023-02-03 09:50:11 +03:00
|
|
|
But you should be able to delete all terms which reference each other in a single command
|
2023-02-03 03:50:01 +03:00
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-02-03 09:50:11 +03:00
|
|
|
e = 11
|
|
|
|
f = 12 + e
|
|
|
|
g = 13 + f
|
|
|
|
h = e + f + g
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
e : Nat
|
|
|
|
f : Nat
|
|
|
|
g : Nat
|
|
|
|
h : Nat
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose e f g h
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. e : Nat
|
|
|
|
2. f : Nat
|
|
|
|
3. g : Nat
|
|
|
|
4. h : Nat
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
```
|
|
|
|
You should be able to delete a type and all the functions that reference it in a single command
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-02-03 09:50:11 +03:00
|
|
|
structural type Foo = Foo Nat
|
2023-02-03 03:50:01 +03:00
|
|
|
|
2023-02-03 09:50:11 +03:00
|
|
|
incrementFoo : Foo -> Nat
|
|
|
|
incrementFoo = cases
|
2024-08-26 20:37:19 +03:00
|
|
|
(Foo.Foo n) -> n + 1
|
2023-02-03 09:50:11 +03:00
|
|
|
```
|
2023-02-03 03:50:01 +03:00
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2023-02-03 03:50:01 +03:00
|
|
|
|
2023-02-03 09:50:11 +03:00
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
structural type Foo
|
|
|
|
incrementFoo : Foo -> Nat
|
2023-02-03 03:50:01 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose Foo Foo.Foo incrementFoo
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. structural type Foo
|
2024-07-11 22:03:09 +03:00
|
|
|
2. Foo.Foo : Nat -> Foo
|
|
|
|
3. incrementFoo : Foo -> Nat
|
2023-02-03 09:50:11 +03:00
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
```
|
|
|
|
If you mess up on one of the names of your command, delete short circuits
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-02-03 09:50:11 +03:00
|
|
|
e = 11
|
|
|
|
f = 12 + e
|
|
|
|
g = 13 + f
|
|
|
|
h = e + f + g
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
e : Nat
|
|
|
|
f : Nat
|
|
|
|
g : Nat
|
|
|
|
h : Nat
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose e f gg
|
2023-02-03 03:50:01 +03:00
|
|
|
|
|
|
|
⚠️
|
|
|
|
|
2023-02-03 09:50:11 +03:00
|
|
|
The following names were not found in the codebase. Check your spelling.
|
|
|
|
gg
|
|
|
|
|
|
|
|
```
|
|
|
|
Cyclical terms which are guarded by a lambda are allowed to be deleted
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-02-03 09:50:11 +03:00
|
|
|
ping _ = 1 Nat.+ !pong
|
|
|
|
pong _ = 4 Nat.+ !ping
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> add
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
2023-02-03 03:50:01 +03:00
|
|
|
|
2023-02-03 09:50:11 +03:00
|
|
|
ping : 'Nat
|
|
|
|
pong : 'Nat
|
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> delete.verbose ping
|
2023-02-03 03:50:01 +03:00
|
|
|
|
2023-02-03 09:50:11 +03:00
|
|
|
Removed definitions:
|
|
|
|
|
|
|
|
1. ping : 'Nat
|
|
|
|
|
2024-07-23 00:36:51 +03:00
|
|
|
Tip: You can use `undo` or use a hash from `reflog` to undo
|
|
|
|
this change.
|
2023-02-03 09:50:11 +03:00
|
|
|
|
2024-07-02 08:14:16 +03:00
|
|
|
scratch/main> view pong
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
pong : 'Nat
|
|
|
|
pong _ =
|
|
|
|
use Nat +
|
2024-06-21 00:52:57 +03:00
|
|
|
4 + #l9uq1dpl5v.1()
|
2023-02-03 09:50:11 +03:00
|
|
|
|
|
|
|
```
|