From dde858e2647e94bb81ebf2f216bbbb5d805d0d19 Mon Sep 17 00:00:00 2001 From: Arya Irani Date: Tue, 21 Nov 2023 12:17:56 -0500 Subject: [PATCH] add test rewrites, and skip the cleanup of rewrites-tmp.u, to help debugging. we could alternatively move the creation and cleanup back into the Unison code, conditional on an environment variable we set to suppress cleanup. --- unison-src/transcripts-manual/rewrites.md | 67 ++++++----- .../transcripts-manual/rewrites.output.md | 110 ++++++++++++++---- 2 files changed, 124 insertions(+), 53 deletions(-) diff --git a/unison-src/transcripts-manual/rewrites.md b/unison-src/transcripts-manual/rewrites.md index 78dea1536c..33f368be82 100644 --- a/unison-src/transcripts-manual/rewrites.md +++ b/unison-src/transcripts-manual/rewrites.md @@ -7,10 +7,10 @@ ## Structural find and replace -Here's a scratch file with some rewrite rules: +Here's a scratch file with some rewrite rules: ```unison:hide /private/tmp/rewrites-tmp.u -ex1 = List.map (x -> x + 1) [1,2,3,4,5,6,7] +ex1 = List.map (x -> x + 1) [1,2,3,4,5,6,7] eitherToOptional e a = @rewrite @@ -25,17 +25,13 @@ Either.mapRight f = cases Left e -> Left e Right a -> Right (f a) -rule1 f x = @rewrite +rule1 f x = @rewrite term x + 1 ==> Nat.increment x term (a -> f a) ==> f -- eta reduction unique type Optional2 a = Some2 a | None2 rule2 x = @rewrite signature Optional ==> Optional2 - -cleanup = do - _ = IO.removeFile.impl "/private/tmp/rewrites-tmp.u" - () ``` Let's rewrite these: @@ -62,13 +58,13 @@ Another example, showing that we can rewrite to definitions that only exist in t unique ability Woot1 where woot1 : () -> Nat unique ability Woot2 where woot2 : () -> Nat -woot1to2 x = @rewrite +woot1to2 x = @rewrite term Woot1.woot1 ==> Woot2.woot2 term blah ==> blah2 - signature _ . Woot1 ==> Woot2 + signature _ . Woot1 ==> Woot2 -wootEx : Nat ->{Woot1} Nat -wootEx a = +wootEx : Nat ->{Woot1} Nat +wootEx a = _ = !woot1 blah @@ -90,17 +86,17 @@ Let's apply the rewrite `woot1to2`: After adding the rewritten form to the codebase, here's the rewritten `Woot1` to `Woot2`: ```ucm -.> view wootEx +.> view wootEx ``` This example shows that rewrite rules can to refer to term definitions that only exist in the file: ```unison:hide /private/tmp/rewrites-tmp.u -foo1 = +foo1 = b = "b" 123 -foo2 = +foo2 = a = "a" 233 @@ -109,7 +105,7 @@ rule = @rewrite term foo1 ==> foo2 case None ==> Left "89899" -sameFileEx = +sameFileEx = _ = "ex" foo1 ``` @@ -123,25 +119,25 @@ sameFileEx = After adding the rewritten form to the codebase, here's the rewritten definitions: ```ucm -.> view foo1 foo2 sameFileEx +.> view foo1 foo2 sameFileEx ``` ## Capture avoidance ```unison:hide /private/tmp/rewrites-tmp.u -bar1 = +bar1 = b = "bar" 123 -bar2 = - a = 39494 +bar2 = + a = 39494 233 rule bar2 = @rewrite case None ==> Left "oh no" term bar1 ==> bar2 -sameFileEx = +sameFileEx = _ = "ex" bar1 ``` @@ -161,13 +157,13 @@ Instead, it should be an unbound free variable, which doesn't typecheck: In this example, the `a` is locally bound by the rule, so it shouldn't capture the `a = 39494` binding which is in scope at the point of the replacement: ```unison:hide /private/tmp/rewrites-tmp.u -bar2 = - a = 39494 +bar2 = + a = 39494 233 rule a = @rewrite case None ==> Left "oh no" - term 233 ==> a + term 233 ==> a ``` ```ucm @@ -180,8 +176,23 @@ The `a` introduced will be freshened to not capture the `a` in scope, so it rema .> load /private/tmp/rewrites-tmp.u ``` -```ucm:hide -.> run cleanup +## Known issues + +```unison:hide /private/tmp/rewrites-tmp.u +test> foo = [] +rule = @rewrite term [] ==> [] +``` + +Apparently when we parse a test watch, we add a type annotation to it, even if it already has one. This should be fixed in this same PR +and this comment amended. + +```ucm +.> rewrite rule +.> load /private/tmp/rewrites-tmp.u +.> rewrite rule +``` +```ucm:error +.> load /private/tmp/rewrites-tmp.u ``` ## Structural find @@ -195,12 +206,12 @@ eitherEx = Left ("hello", "there") ``` ```unison:hide -findEitherEx x = @rewrite term Left ("hello", x) ==> Left ("hello" Text.++ x) -findEitherFailure = @rewrite signature a . Either Failure a ==> () +findEitherEx x = @rewrite term Left ("hello", x) ==> Left ("hello" Text.++ x) +findEitherFailure = @rewrite signature a . Either Failure a ==> () ``` ```ucm .> sfind findEitherEx .> sfind findEitherFailure .> find 1-5 -``` \ No newline at end of file +``` diff --git a/unison-src/transcripts-manual/rewrites.output.md b/unison-src/transcripts-manual/rewrites.output.md index c7ce565c00..345db1ca1d 100644 --- a/unison-src/transcripts-manual/rewrites.output.md +++ b/unison-src/transcripts-manual/rewrites.output.md @@ -1,13 +1,13 @@ ## Structural find and replace -Here's a scratch file with some rewrite rules: +Here's a scratch file with some rewrite rules: ```unison --- title: /private/tmp/rewrites-tmp.u --- -ex1 = List.map (x -> x + 1) [1,2,3,4,5,6,7] +ex1 = List.map (x -> x + 1) [1,2,3,4,5,6,7] eitherToOptional e a = @rewrite @@ -22,7 +22,7 @@ Either.mapRight f = cases Left e -> Left e Right a -> Right (f a) -rule1 f x = @rewrite +rule1 f x = @rewrite term x + 1 ==> Nat.increment x term (a -> f a) ==> f -- eta reduction @@ -30,10 +30,6 @@ unique type Optional2 a = Some2 a | None2 rule2 x = @rewrite signature Optional ==> Optional2 -cleanup = do - _ = IO.removeFile.impl "/private/tmp/rewrites-tmp.u" - () - ``` @@ -94,13 +90,13 @@ title: /private/tmp/rewrites-tmp.u unique ability Woot1 where woot1 : () -> Nat unique ability Woot2 where woot2 : () -> Nat -woot1to2 x = @rewrite +woot1to2 x = @rewrite term Woot1.woot1 ==> Woot2.woot2 term blah ==> blah2 - signature _ . Woot1 ==> Woot2 + signature _ . Woot1 ==> Woot2 -wootEx : Nat ->{Woot1} Nat -wootEx a = +wootEx : Nat ->{Woot1} Nat +wootEx a = _ = !woot1 blah @@ -125,7 +121,7 @@ Let's apply the rewrite `woot1to2`: After adding the rewritten form to the codebase, here's the rewritten `Woot1` to `Woot2`: ```ucm -.> view wootEx +.> view wootEx wootEx : Nat ->{Woot2} Nat wootEx a = @@ -139,11 +135,11 @@ This example shows that rewrite rules can to refer to term definitions that only --- title: /private/tmp/rewrites-tmp.u --- -foo1 = +foo1 = b = "b" 123 -foo2 = +foo2 = a = "a" 233 @@ -152,7 +148,7 @@ rule = @rewrite term foo1 ==> foo2 case None ==> Left "89899" -sameFileEx = +sameFileEx = _ = "ex" foo1 @@ -162,7 +158,7 @@ sameFileEx = After adding the rewritten form to the codebase, here's the rewritten definitions: ```ucm -.> view foo1 foo2 sameFileEx +.> view foo1 foo2 sameFileEx foo1 : Nat foo1 = @@ -186,19 +182,19 @@ After adding the rewritten form to the codebase, here's the rewritten definition --- title: /private/tmp/rewrites-tmp.u --- -bar1 = +bar1 = b = "bar" 123 -bar2 = - a = 39494 +bar2 = + a = 39494 233 rule bar2 = @rewrite case None ==> Left "oh no" term bar1 ==> bar2 -sameFileEx = +sameFileEx = _ = "ex" bar1 @@ -245,13 +241,13 @@ In this example, the `a` is locally bound by the rule, so it shouldn't capture t --- title: /private/tmp/rewrites-tmp.u --- -bar2 = - a = 39494 +bar2 = + a = 39494 233 rule a = @rewrite case None ==> Left "oh no" - term 233 ==> a + term 233 ==> a ``` @@ -287,6 +283,70 @@ The `a` introduced will be freshened to not capture the `a` in scope, so it rema +``` +## Known issues + +```unison +--- +title: /private/tmp/rewrites-tmp.u +--- +test> foo = [] +rule = @rewrite term [] ==> [] + +``` + + +Apparently when we parse a test watch, we add a type annotation to it, even if it already has one. This should be fixed in this same PR +and this comment amended. + +```ucm +.> rewrite rule + + ☝️ + + I found and replaced matches in these definitions: foo + + The rewritten file has been added to the top of /private/tmp/rewrites-tmp.u + +.> load /private/tmp/rewrites-tmp.u + + I found and typechecked these definitions in + /private/tmp/rewrites-tmp.u. If you do an `add` or `update`, + here's how your codebase would change: + + ⍟ These new definitions are ok to `add`: + + foo : [Result] + + ⍟ These names already exist. You can `update` them to your + new definition: + + rule : ∀ elem1 elem. + Rewrites (Tuple (RewriteTerm [elem1] [elem]) ()) + + Now evaluating any watch expressions (lines starting with + `>`)... Ctrl+C cancels. + + 4 | test> foo : [Result] + + +.> rewrite rule + + ☝️ + + I found and replaced matches in these definitions: foo + + The rewritten file has been added to the top of /private/tmp/rewrites-tmp.u + +``` +```ucm +.> load /private/tmp/rewrites-tmp.u + + offset=10: + unexpected : + 5 | foo : [Result] + + ``` ## Structural find @@ -295,8 +355,8 @@ eitherEx = Left ("hello", "there") ``` ```unison -findEitherEx x = @rewrite term Left ("hello", x) ==> Left ("hello" Text.++ x) -findEitherFailure = @rewrite signature a . Either Failure a ==> () +findEitherEx x = @rewrite term Left ("hello", x) ==> Left ("hello" Text.++ x) +findEitherFailure = @rewrite signature a . Either Failure a ==> () ``` ```ucm