unison/unison-src/transcripts/delete.md

184 lines
2.9 KiB
Markdown
Raw Permalink Normal View History

# Delete
```ucm:hide
2024-07-02 08:14:16 +03:00
scratch/main> builtins.merge lib.builtins
```
The delete command can delete both terms and types.
First, let's make sure it complains when we try to delete a name that doesn't
exist.
```ucm:error
2024-07-02 08:14:16 +03:00
scratch/main> delete.verbose foo
```
Now for some easy cases. Deleting an unambiguous term, then deleting an
unambiguous type.
2020-01-17 00:58:31 +03:00
```unison:hide
foo = 1
2022-04-07 00:12:07 +03:00
structural type Foo = Foo ()
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose foo
scratch/main> delete.verbose Foo
scratch/main> delete.verbose Foo.Foo
```
How about an ambiguous term?
2020-01-17 00:58:31 +03:00
```unison:hide
2024-07-02 08:14:16 +03:00
a.foo = 1
a.bar = 2
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> debug.alias.term.force a.bar a.foo
```
A delete should remove both versions of the term.
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> delete.verbose a.foo
scratch/main> ls a
```
Let's repeat all that on a type, for completeness.
2020-01-17 00:58:31 +03:00
```unison:hide
2024-07-02 08:14:16 +03:00
structural type a.Foo = Foo ()
structural type a.Bar = Bar
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> debug.alias.type.force a.Bar a.Foo
scratch/main> delete.verbose a.Foo
scratch/main> delete.verbose a.Foo.Foo
```
Finally, let's try to delete a term and a type with the same name.
2020-01-17 00:58:31 +03:00
```unison:hide
foo = 1
2022-04-07 00:12:07 +03:00
structural type foo = Foo ()
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose foo
```
2023-02-03 03:50:01 +03:00
We want to be able to delete multiple terms at once
```unison:hide
a = "a"
b = "b"
c = "c"
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose a b c
2023-02-03 03:50:01 +03:00
```
We can delete terms and types in the same invocation of delete
```unison:hide
structural type Foo = Foo ()
a = "a"
b = "b"
c = "c"
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose a b c Foo
scratch/main> delete.verbose Foo.Foo
2023-02-03 03:50:01 +03:00
```
We can delete a type and its constructors
```unison:hide
structural type Foo = Foo ()
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose Foo Foo.Foo
2023-02-03 03:50:01 +03:00
```
You should not be able to delete terms which are referenced by other terms
```unison:hide
a = 1
b = 2
c = 3
d = a + b + c
```
2023-02-03 04:15:30 +03:00
```ucm:error
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose a b c
2023-02-03 03:50:01 +03:00
```
But you should be able to delete all terms which reference each other in a single command
```unison:hide
e = 11
f = 12 + e
g = 13 + f
h = e + f + g
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose e f g h
2023-02-03 03:50:01 +03:00
```
You should be able to delete a type and all the functions that reference it in a single command
```unison:hide
structural type Foo = Foo Nat
incrementFoo : Foo -> Nat
incrementFoo = cases
(Foo.Foo n) -> n + 1
2023-02-03 03:50:01 +03:00
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose Foo Foo.Foo incrementFoo
2023-02-03 03:50:01 +03:00
```
If you mess up on one of the names of your command, delete short circuits
2023-02-03 03:50:01 +03:00
```unison:hide
e = 11
f = 12 + e
g = 13 + f
h = e + f + g
```
2023-02-03 04:15:30 +03:00
```ucm:error
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose e f gg
2023-02-03 03:50:01 +03:00
```
Cyclical terms which are guarded by a lambda are allowed to be deleted
```unison:hide
ping _ = 1 Nat.+ !pong
pong _ = 4 Nat.+ !ping
```
```ucm
2024-07-02 08:14:16 +03:00
scratch/main> add
scratch/main> delete.verbose ping
scratch/main> view pong
```