mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-19 06:17:33 +03:00
move rewrites transcript to transcripts-manual, run after diff check
This commit is contained in:
Paul Chiusano
parent
387695764f
commit
b6abc956a7
2
.github/workflows/ci.yaml
vendored
2
.github/workflows/ci.yaml
vendored
@ -231,6 +231,8 @@ jobs:
|
||||
git diff --cached --ignore-cr-at-eol --exit-code
|
||||
- name: prettyprint-round-trip
|
||||
run: stack --no-terminal exec unison transcript unison-src/transcripts-round-trip/main.md
|
||||
- name: structured-find-replace
|
||||
run: stack --no-terminal exec unison transcript unison-src/transcripts-manual/rewrites.md
|
||||
- name: cli-integration-tests
|
||||
run: stack --no-terminal exec cli-integration-tests
|
||||
- name: Cache Racket dependencies
|
||||
|
||||
@ -1,236 +0,0 @@
|
||||
|
||||
```unison
|
||||
---
|
||||
title: rewrites-tmp.u
|
||||
---
|
||||
ex1 = List.map (x -> x + 1) [1,2,3,4,5,6,7]
|
||||
|
||||
eitherToOptional e a =
|
||||
@rewrite
|
||||
term Left e ==> None
|
||||
term Right a ==> Some a
|
||||
case Left e ==> None
|
||||
case Right a ==> Some a
|
||||
signature e a . Either e a ==> Optional a
|
||||
|
||||
Either.mapRight : (a ->{g} b) -> Either e a ->{g} Either e b
|
||||
Either.mapRight f = cases
|
||||
Left e -> Left e
|
||||
Right a -> Right (f a)
|
||||
|
||||
rule1 f x = @rewrite
|
||||
term x + 1 ==> Nat.increment x
|
||||
term (a -> f a) ==> f -- eta reduction
|
||||
|
||||
d = {{
|
||||
|
||||
Here's the rewritten source of {ex1}:
|
||||
|
||||
@source{ex1}
|
||||
|
||||
And here's the rewritten source of {Either.mapRight},
|
||||
with {type Either} replaced by {type Optional}:
|
||||
|
||||
@source{Either.mapRight}
|
||||
|
||||
Lastly, here's the source of the rewrite blocks (demonstrating
|
||||
the pretty-printing syntax):
|
||||
|
||||
@source{rule1, eitherToOptional}
|
||||
}}
|
||||
|
||||
cleanup = do
|
||||
_ = IO.removeFile.impl "rewrites-tmp.u"
|
||||
()
|
||||
|
||||
```
|
||||
|
||||
|
||||
```ucm
|
||||
.> rewrite rule1
|
||||
|
||||
☝️
|
||||
|
||||
I found and replaced matches in these definitions: ex1
|
||||
|
||||
The rewritten file has been added to the top of /Users/pchiusano/unison/rewrites-tmp.u
|
||||
|
||||
.> rewrite eitherToOptional
|
||||
|
||||
☝️
|
||||
|
||||
I found and replaced matches in these definitions:
|
||||
Either.mapRight
|
||||
|
||||
The rewritten file has been added to the top of /Users/pchiusano/unison/rewrites-tmp.u
|
||||
|
||||
.> load rewrites-tmp.u
|
||||
|
||||
I found and typechecked these definitions in rewrites-tmp.u.
|
||||
If you do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
Either.mapRight : (a ->{g} b)
|
||||
-> Optional a
|
||||
->{g} Optional b
|
||||
cleanup : '{IO} ()
|
||||
d : Doc2
|
||||
eitherToOptional : ∀ e1 a e a1 a2 a3 b a4 a5 b1.
|
||||
e1
|
||||
-> a1
|
||||
-> Rewrites
|
||||
( RewriteTerm
|
||||
(Either e1 b1) (Optional a5),
|
||||
RewriteTerm
|
||||
(Either a4 a1) (Optional a1),
|
||||
RewriteCase
|
||||
(Either e1 b) (Optional a3),
|
||||
RewriteCase
|
||||
(Either a2 a1) (Optional a1),
|
||||
RewriteSignature
|
||||
(Either e a) (Optional a))
|
||||
ex1 : [Nat]
|
||||
rule1 : ∀ o g i g1.
|
||||
(i ->{g} o)
|
||||
-> Nat
|
||||
-> Rewrites
|
||||
( RewriteTerm Nat Nat,
|
||||
RewriteTerm
|
||||
(i ->{g, g1} o) (i ->{g} o))
|
||||
|
||||
.> display d
|
||||
|
||||
Here's the rewritten source of ex1:
|
||||
|
||||
ex1 : [Nat]
|
||||
ex1 = List.map Nat.increment [1, 2, 3, 4, 5, 6, 7]
|
||||
|
||||
And here's the rewritten source of Either.mapRight, with
|
||||
Either replaced by Optional:
|
||||
|
||||
Either.mapRight :
|
||||
(a ->{g} b) -> Optional a ->{g} Optional b
|
||||
Either.mapRight f = cases
|
||||
None -> None
|
||||
Some a -> Some (f a)
|
||||
|
||||
Lastly, here's the source of the rewrite blocks (demonstrating
|
||||
the pretty-printing syntax):
|
||||
|
||||
eitherToOptional :
|
||||
∀ e1 a e a1 a2 a3 b a4 a5 b1.
|
||||
e1
|
||||
-> a1
|
||||
-> Rewrites
|
||||
( RewriteTerm (Either e1 b1) (Optional a5),
|
||||
RewriteTerm (Either a4 a1) (Optional a1),
|
||||
RewriteCase (Either e1 b) (Optional a3),
|
||||
RewriteCase (Either a2 a1) (Optional a1),
|
||||
RewriteSignature (Either e a) (Optional a))
|
||||
eitherToOptional e a =
|
||||
@rewrite
|
||||
term Left e ==> None
|
||||
term Right a ==> Some a
|
||||
case Left e ==> None
|
||||
case Right a ==> Some a
|
||||
signature e a . Either e a ==> Optional a
|
||||
|
||||
rule1 :
|
||||
∀ o g i g1.
|
||||
(i ->{g} o)
|
||||
-> Nat
|
||||
-> Rewrites
|
||||
( RewriteTerm Nat Nat,
|
||||
RewriteTerm (i ->{g, g1} o) (i ->{g} o))
|
||||
rule1 f x =
|
||||
use Nat +
|
||||
@rewrite
|
||||
term x + 1 ==> Nat.increment x
|
||||
term a -> f a ==> f
|
||||
|
||||
.> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
Either.mapRight : (a ->{g} b)
|
||||
-> Optional a
|
||||
->{g} Optional b
|
||||
cleanup : '{IO} ()
|
||||
d : Doc2
|
||||
eitherToOptional : ∀ e1 a e a1 a2 a3 b a4 a5 b1.
|
||||
e1
|
||||
-> a1
|
||||
-> Rewrites
|
||||
( RewriteTerm
|
||||
(Either e1 b1) (Optional a5),
|
||||
RewriteTerm
|
||||
(Either a4 a1) (Optional a1),
|
||||
RewriteCase
|
||||
(Either e1 b) (Optional a3),
|
||||
RewriteCase
|
||||
(Either a2 a1) (Optional a1),
|
||||
RewriteSignature
|
||||
(Either e a) (Optional a))
|
||||
ex1 : [Nat]
|
||||
rule1 : ∀ o g i g1.
|
||||
(i ->{g} o)
|
||||
-> Nat
|
||||
-> Rewrites
|
||||
( RewriteTerm Nat Nat,
|
||||
RewriteTerm
|
||||
(i ->{g, g1} o) (i ->{g} o))
|
||||
|
||||
.> run cleanup
|
||||
|
||||
()
|
||||
|
||||
```
|
||||
```unison
|
||||
eitherEx = Left ("hello", "there")
|
||||
```
|
||||
|
||||
```unison
|
||||
findEitherEx x = @rewrite term Left ("hello", x) ==> Left ("hello" Text.++ x)
|
||||
findEitherFailure = @rewrite signature a . Either Failure a ==> ()
|
||||
```
|
||||
|
||||
```ucm
|
||||
.> sfind findEitherEx
|
||||
|
||||
🔎
|
||||
|
||||
These definitions from the current namespace (excluding `lib`) have matches:
|
||||
|
||||
1. eitherEx
|
||||
|
||||
Tip: Try `edit 1` to bring this into your scratch file.
|
||||
|
||||
.> sfind findEitherFailure
|
||||
|
||||
🔎
|
||||
|
||||
These definitions from the current namespace (excluding `lib`) have matches:
|
||||
|
||||
1. toEither
|
||||
2. reraise
|
||||
3. printText
|
||||
4. toEither.handler
|
||||
5. catch
|
||||
|
||||
Tip: Try `edit 1` or `edit 1-5` to bring these into your
|
||||
scratch file.
|
||||
|
||||
.> find 1-5
|
||||
|
||||
1. Exception.catch : '{g, Exception} a ->{g} Either Failure a
|
||||
2. Exception.reraise : Either Failure a ->{Exception} a
|
||||
3. Exception.toEither : '{ε, Exception} a
|
||||
->{ε} Either Failure a
|
||||
4. Exception.toEither.handler : Request {Exception} a
|
||||
-> Either Failure a
|
||||
5. printText : Text ->{IO} Either Failure ()
|
||||
|
||||
|
||||
```
|
||||
Loading…
Reference in New Issue
Block a user