From c37ead06ee02b8abb023d1ade11b5de500217c6f Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Thu, 30 Jan 2025 15:12:12 -0500 Subject: [PATCH 1/3] Thread pattern variable ids through recursive pattern splitting Pattern compilation was causing variable captures in some particular corner cases. Rather than try to figure out exactly what situation was causing the capture, and how to avoid it, I've just changed the way the recursive splitting functions works to thread the fresh ids through the entire process. This means that sub-expressions never make up the same variables as parent expressions, and should mean that no further processing is needed to avoid captures. --- unison-runtime/src/Unison/Runtime/Pattern.hs | 47 +++++++++++--------- 1 file changed, 27 insertions(+), 20 deletions(-) diff --git a/unison-runtime/src/Unison/Runtime/Pattern.hs b/unison-runtime/src/Unison/Runtime/Pattern.hs index b783e9bf50..21999727a3 100644 --- a/unison-runtime/src/Unison/Runtime/Pattern.hs +++ b/unison-runtime/src/Unison/Runtime/Pattern.hs @@ -25,7 +25,7 @@ import Data.Set qualified as Set import Unison.ABT ( absChain', renames, - visitPure, + visit, pattern AbsN', ) import Unison.Builtin.Decls (builtinDataDecls, builtinEffectDecls) @@ -765,34 +765,41 @@ initialize :: PType -> Term v -> [MatchCase () (Term v)] -> - (Maybe v, (v, PType), PatternMatrix v) -initialize r sc cs = - ( lv, - (sv, r), - PM $ evalState (traverse (mkRow sv) cs) 1 - ) + State Word64 (Maybe v, (v, PType), PatternMatrix v) +initialize r sc cs = do + (lv, sv) <- vars + rs <- traverse (mkRow sv) cs + pure (lv, (sv, r), PM rs) where - (lv, sv) - | Var' v <- sc = (Nothing, v) - | pv <- freshenId 0 $ typed Pattern = - (Just pv, pv) + vars + | Var' v <- sc = pure (Nothing, v) + | otherwise = mkVars <$> grabId + mkVars n = (Just pv, pv) + where + pv = freshenId n $ typed Pattern + +grabId :: State Word64 Word64 +grabId = state $ \n -> (n, n+1) splitPatterns :: (Var v) => DataSpec -> Term v -> Term v -splitPatterns spec0 = visitPure $ \case +splitPatterns spec0 tm = evalState (splitPatterns0 spec tm) 0 + where + spec = Map.insert Rf.booleanRef (Right [0, 0]) spec0 + +splitPatterns0 :: (Var v) => DataSpec -> Term v -> State Word64 (Term v) +splitPatterns0 spec = visit $ \case Match' sc0 cs0 - | ty <- determineType $ p <$> cs0, - (lv, scrut, pm) <- initialize ty sc cs, - body <- compile spec (uncurry Map.singleton scrut) pm -> - Just $ case lv of + | ty <- determineType $ p <$> cs0 -> Just $ do + sc <- splitPatterns0 spec sc0 + cs <- (traverse . traverse) (splitPatterns0 spec) cs0 + (lv, scrut, pm) <- initialize ty sc cs + let body = compile spec (uncurry Map.singleton scrut) pm + pure $ case lv of Just v -> let1 False [(((), v), sc)] body _ -> body - where - sc = splitPatterns spec sc0 - cs = fmap (splitPatterns spec) <$> cs0 _ -> Nothing where p (MatchCase pp _ _) = pp - spec = Map.insert Rf.booleanRef (Right [0, 0]) spec0 builtinCase :: Set Reference builtinCase = From a353a71fd9b27fcbf632afe118070c001266c050 Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Thu, 30 Jan 2025 17:28:51 -0500 Subject: [PATCH 2/3] Add transcript test --- .../idempotent/fix-pattern-capture.md | 63 +++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 unison-src/transcripts/idempotent/fix-pattern-capture.md diff --git a/unison-src/transcripts/idempotent/fix-pattern-capture.md b/unison-src/transcripts/idempotent/fix-pattern-capture.md new file mode 100644 index 0000000000..293cca8019 --- /dev/null +++ b/unison-src/transcripts/idempotent/fix-pattern-capture.md @@ -0,0 +1,63 @@ +``` ucm :hide +scratch/main> builtins.merge +``` + +Checks a case that was resulting in variable capture when compiling +pattern matching. `y` was evidently getting captured by the variable +introduced for `confuser decoy` + +``` unison +type NatBox = NatBox Nat +type Decoy a = { confuser : Tres } + +type Tres = One | Two | Three + +xyzzy : NatBox -> Decoy a -> Nat +xyzzy box decoy = + (NatBox y) = box + (natty) = -- Note that these parentheses are required + match confuser decoy with + Tres.One -> y + Two -> y + 1 + Three -> 11 + natty + +> xyzzy (NatBox 1) (Decoy One) +> xyzzy (NatBox 1) (Decoy Two) +> xyzzy (NatBox 1) (Decoy Three) +``` + +``` ucm :added-by-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`: + + type Decoy a + type NatBox + type Tres + Decoy.confuser : Decoy a -> Tres + Decoy.confuser.modify : (Tres ->{g} Tres) + -> Decoy a1 + ->{g} Decoy a + Decoy.confuser.set : Tres -> Decoy a1 -> Decoy a + xyzzy : NatBox -> Decoy a -> Nat + + Now evaluating any watch expressions (lines starting with + `>`)... Ctrl+C cancels. + + 16 | > xyzzy (NatBox 1) (Decoy One) + ⧩ + 1 + + 17 | > xyzzy (NatBox 1) (Decoy Two) + ⧩ + 2 + + 18 | > xyzzy (NatBox 1) (Decoy Three) + ⧩ + 11 +``` From 3862b58677dc7e478dabf9cb4745a0ade8246fc2 Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Thu, 30 Jan 2025 17:39:19 -0500 Subject: [PATCH 3/3] Transcript whitespace --- unison-src/transcripts/idempotent/fix-pattern-capture.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unison-src/transcripts/idempotent/fix-pattern-capture.md b/unison-src/transcripts/idempotent/fix-pattern-capture.md index 293cca8019..9d181d77fb 100644 --- a/unison-src/transcripts/idempotent/fix-pattern-capture.md +++ b/unison-src/transcripts/idempotent/fix-pattern-capture.md @@ -35,7 +35,7 @@ xyzzy box decoy = change: ⍟ These new definitions are ok to `add`: - + type Decoy a type NatBox type Tres