diff --git a/parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs b/parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs index 2c7b9ae56e..77937c6d56 100644 --- a/parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs +++ b/parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs @@ -4,6 +4,8 @@ module Unison.PrettyPrintEnv.MonadPretty runPretty, addTypeVars, willCaptureType, + withBoundTerm, + withBoundTerms, ) where @@ -14,12 +16,15 @@ import Unison.Prelude import Unison.PrettyPrintEnv (PrettyPrintEnv) import Unison.Util.Set qualified as Set import Unison.Var (Var) +import Unison.Var qualified as Var type MonadPretty v m = (Var v, MonadReader (Env v) m) +-- See Note [Bound and free term variables] for an explanation of boundTerms/freeTerms data Env v = Env { boundTerms :: !(Set v), boundTypes :: !(Set v), + freeTerms :: !(Set v), ppe :: !PrettyPrintEnv } deriving stock (Generic) @@ -36,6 +41,14 @@ addTypeVars = modifyTypeVars . Set.union . Set.fromList willCaptureType :: (MonadPretty v m) => [v] -> m Bool willCaptureType vs = views #boundTypes (Set.intersects (Set.fromList vs)) +withBoundTerm :: (MonadPretty v m) => v -> m a -> m a +withBoundTerm v = + local (over #boundTerms (Set.insert (Var.reset v))) + +withBoundTerms :: (MonadPretty v m) => [v] -> m a -> m a +withBoundTerms vs = + local (over #boundTerms (Set.union (foldMap (Set.singleton . Var.reset) vs))) + runPretty :: (Var v) => PrettyPrintEnv -> Reader (Env v) a -> a runPretty ppe m = runReader @@ -43,5 +56,61 @@ runPretty ppe m = Env { boundTerms = Set.empty, boundTypes = Set.empty, + freeTerms = Set.empty, ppe } + +-- Note [Bound and free term variables] +-- +-- When rendering a Unison file, we render top-level bindings independently, which may end up referring to each +-- other after all are parsed together. Any individual term, therefore, may have free variables. For example, +-- +-- foo = ... bar ... +-- ^^^ +-- this "bar" variable is free in foo +-- +-- bar = ... +-- ^^^ +-- it's ultimately bound by a different top-level term rendering +-- +-- Therefore, we pass down all free variables of a top-level term binding, so that we can decide, when rendering one of +-- them, whether to add a leading dot. +-- +-- Now, when do we need to add a leading dot? Basically, any time a binder introduces a var that, when rendered reset, +-- clashes with the free var. +-- +-- Here are a few examples using a made-up Unison syntax in which we can see whether a let is recursive or +-- non-recursive, and using "%" to separate a var name from its unique id. +-- +-- Example 1 +-- +-- Made-up syntax Actual syntax +-- -------------- ---------------- +-- foo%0 = foo = +-- let bar%0 = bar%0 bar = #someref -- rendered as ".bar", then parsed as var "bar" +-- in 5 5 +-- +-- bar%0 = ... bar = ... +-- +-- In this example, we have a non-recursive let that binds a local variable called bar%0. The body of the bar%0 binding +-- can itself refer to a different bar%0, which isn't captured, since a non-recursive let binding body can't refer to +-- the binding. +-- +-- So, when rendering the free bar%0 in the right-hand side, we ask: should we add a leading dot? And the answer is: is +-- the var bar%0 in the set of all reset locally-bound vars {bar%0}? Yes? Then yes. +-- +-- Example 2 +-- +-- Made-up syntax Actual syntax +-- -------------- ---------------- +-- foo%0 = foo = +-- letrec bar%1 = do bar%0 hey%0 bar = do #someref hey -- rendered as ".bar", then parsed as var "bar" +-- hey%0 = do bar%1 hey = do bar +-- in 5 5 +-- +-- bar%0 = ... bar = ... +-- +-- In this example, we have a recursive let that binds a bar%1 variable, and refers to bar%0 from inside. Same +-- situation, but variable resetting is relevant, because when walking underneath binder bar%1, we want to add its reset +-- form (bar%0) to the set of bound variables to check against, when rendering a free var (which we assume to have +-- unique id 0). diff --git a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs index 717a7726d3..0135511fe1 100644 --- a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs +++ b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs @@ -217,12 +217,12 @@ pretty0 } term = specialCases term \case - Var' (Var.reset -> v) -> do + Var' v -> do env <- ask let name = - if Set.member v env.boundTerms + if Set.member v env.freeTerms && Set.member v env.boundTerms then HQ.fromName (Name.makeAbsolute (Name.unsafeParseVar v)) - else elideFQN im $ HQ.unsafeFromVar v + else elideFQN im $ HQ.unsafeFromVar (Var.reset v) pure . parenIfInfix name ic $ styleHashQualified'' (fmt S.Var) name Ref' r -> do env <- ask @@ -687,30 +687,21 @@ printLetBindings :: m [Pretty SyntaxText] printLetBindings context = \case LetBindings bindings -> traverse (printLetBinding context) bindings - LetrecBindings bindings -> traverse (printLetrecBinding context) bindings + LetrecBindings bindings -> + let boundVars = map fst bindings + in traverse (printLetrecBinding context boundVars) bindings printLetBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText) printLetBinding context (v, binding) | Var.isAction v = pretty0 context binding | otherwise = - -- For a non-recursive let binding like "let x = y in z", variable "x" is not bound in "y". Yet, "x" may be free - -- in "y" anyway, referring to some previous binding. - -- - -- In Unison we don't have a syntax, for non-recusrive let, though, we just have this: - -- - -- x = y - -- z - -- - -- So, render free "x" in "y" with a leading dot. This is because we happen to know that the only way to have - -- a free "x" in "y" is if "x" is a top-level binding. - renderPrettyBinding - <$> local (over #boundTerms (Set.insert v1)) (prettyBinding0' context (HQ.unsafeFromVar v1) binding) + renderPrettyBinding <$> withBoundTerm v (prettyBinding0' context (HQ.unsafeFromVar v1) binding) where v1 = Var.reset v -printLetrecBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText) -printLetrecBinding context (v, binding) = - renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar (Var.reset v)) binding +printLetrecBinding :: (MonadPretty v m) => AmbientContext -> [v] -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText) +printLetrecBinding context vs (v, binding) = + renderPrettyBinding <$> withBoundTerms vs (prettyBinding0' context (HQ.unsafeFromVar (Var.reset v)) binding) prettyPattern :: forall v loc. @@ -735,7 +726,7 @@ prettyPattern n c@AmbientContext {imports = im} p vs patt = case patt of Pattern.Unbound _ -> (fmt S.DelimiterChar $ l "_", vs) Pattern.Var _ -> case vs of - (v : tail_vs) -> (fmt S.Var $ l $ Var.nameStr v, tail_vs) + (v : tail_vs) -> (fmt S.Var $ l $ Var.nameStr (Var.reset v), tail_vs) _ -> error "prettyPattern: Expected at least one var" Pattern.Boolean _ b -> (fmt S.BooleanLiteral $ if b then l "true" else l "false", vs) Pattern.Int _ i -> (fmt S.NumericLiteral $ (if i >= 0 then l "+" else mempty) <> l (show i), vs) @@ -764,7 +755,7 @@ prettyPattern n c@AmbientContext {imports = im} p vs patt = case patt of case vs of (v : tail_vs) -> let (printed, eventual_tail) = prettyPattern n c Prefix tail_vs pat - in (paren (p >= Prefix) (fmt S.Var (l $ Var.nameStr v) <> fmt S.DelimiterChar (l "@") <> printed), eventual_tail) + in (paren (p >= Prefix) (fmt S.Var (l $ Var.nameStr (Var.reset v)) <> fmt S.DelimiterChar (l "@") <> printed), eventual_tail) _ -> error "prettyPattern: Expected at least one var" Pattern.EffectPure _ pat -> let (printed, eventual_tail) = prettyPattern n c Bottom vs pat @@ -827,7 +818,7 @@ groupCases :: (Ord v) => [MatchCase' () (Term3 v ann)] -> [([Pattern ()], [v], [(Maybe (Term3 v ann), Term3 v ann)])] -groupCases ms = go0 ms +groupCases = go0 where go0 [] = [] go0 ms@((p1, _, AbsN' vs1 _) : _) = go2 (p1, vs1) [] ms @@ -842,12 +833,11 @@ printCase :: DocLiteralContext -> [MatchCase' () (Term3 v PrintAnnotation)] -> m (Pretty SyntaxText) -printCase im doc ms0 = +printCase im doc ms = PP.orElse <$> (PP.lines . alignGrid True <$> grid) <*> (PP.lines . alignGrid False <$> grid) where - ms = groupCases ms0 justify rows = zip (fmap fst . PP.align' $ fmap alignPatterns rows) $ fmap gbs rows where @@ -876,19 +866,18 @@ printCase im doc ms0 = ) justified justified = PP.leftJustify $ fmap (\(g, b) -> (g, (arrow, b))) gbs - grid = traverse go ms - patLhs env vs pats = - case pats of - [pat] -> PP.group (fst (prettyPattern env (ac Annotation Block im doc) Bottom vs pat)) - pats -> PP.group - . PP.sep (PP.indentAfterNewline " " $ "," <> PP.softbreak) - . (`evalState` vs) - . for pats - $ \pat -> do - vs <- State.get - let (p, rem) = prettyPattern env (ac Annotation Block im doc) Bottom vs pat - State.put rem - pure p + grid = traverse go (groupCases ms) + patLhs ppe vs = \cases + [pat] -> PP.group (fst (prettyPattern ppe (ac Annotation Block im doc) Bottom vs pat)) + pats -> PP.group + . PP.sep (PP.indentAfterNewline " " $ "," <> PP.softbreak) + . (`evalState` vs) + . for pats + $ \pat -> do + vs <- State.get + let (p, rem) = prettyPattern ppe (ac Annotation Block im doc) Bottom vs pat + State.put rem + pure p arrow = fmt S.ControlKeyword "->" -- If there's multiple guarded cases for this pattern, prints as: -- MyPattern x y @@ -989,7 +978,7 @@ prettyBinding0 :: m PrettyBinding prettyBinding0 ac v tm = do env <- ask - prettyBinding0' ac v (printAnnotate env.ppe tm) + local (set #freeTerms (ABT.freeVars tm)) (prettyBinding0' ac v (printAnnotate env.ppe tm)) prettyBinding0' :: (MonadPretty v m) => diff --git a/unison-src/transcripts/idempotent/fix-5525.md b/unison-src/transcripts/idempotent/fix-5525.md new file mode 100644 index 0000000000..1d17b67466 --- /dev/null +++ b/unison-src/transcripts/idempotent/fix-5525.md @@ -0,0 +1,106 @@ +The original bug report identified the mishandling of this simple case involving shadowing, in which we previously +erroneously rendered "bar" with a leading dot. + +``` ucm +scratch/main> builtins.merge lib.builtin + + Done. +``` + +``` unison +foo = + bar = + match 5 with + 1 -> 2 + bar -> bar + bar +``` + +``` 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`: + + foo : Nat +``` + +``` ucm +scratch/main> add + + ⍟ I've added these definitions: + + foo : Nat + +scratch/main> view foo + + foo : Nat + foo = + bar = match 5 with + 1 -> 2 + bar -> bar + bar +``` + +``` ucm +scratch/main> project.delete scratch +``` + +There's a more complicated case that was also previously mishandled, though, which involves a top-level binding to which +for which we do need to add a leading dot in order to refer to. + +``` ucm +scratch/main> builtins.merge lib.builtin + + Done. +``` + +``` unison +foo = + bar = + match 5 with + 1 -> 2 + bar -> bar + .bar + bar + +bar = 17 +``` + +``` 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`: + + bar : Nat + foo : Nat +``` + +``` ucm +scratch/main> add + + ⍟ I've added these definitions: + + bar : Nat + foo : Nat + +scratch/main> view foo + + foo : Nat + foo = + use Nat + + bar = match 5 with + 1 -> 2 + bar1 -> bar + .bar + bar +``` + +``` ucm +scratch/main> project.delete scratch +```