Skip to content

Commit

Permalink
Note var mentions so we can align symbol ids with their location then…
Browse files Browse the repository at this point in the history
… tie that to their type.
  • Loading branch information
ChrisPenner committed Jan 13, 2025
1 parent 27494d7 commit 5fe41c2
Show file tree
Hide file tree
Showing 5 changed files with 55 additions and 36 deletions.
6 changes: 3 additions & 3 deletions parser-typechecker/src/Unison/Typechecker.hs
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ data Env v loc = Env
-- a function to resolve the type of @Ref@ constructors
-- contained in that term.
synthesize ::
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc, Semigroup loc) =>
PrettyPrintEnv ->
Context.PatternMatchCoverageCheckAndKindInferenceSwitch ->
Env v loc ->
Expand Down Expand Up @@ -353,7 +353,7 @@ typeDirectedNameResolution ppe oldNotes oldType env = do
-- contained in the term. Returns @typ@ if successful,
-- and a note about typechecking failure otherwise.
check ::
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) =>
(Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc, Semigroup loc) =>
PrettyPrintEnv ->
Env v loc ->
Term v loc ->
Expand All @@ -376,7 +376,7 @@ check ppe env term typ =
-- tweak (Type.ForallNamed' v body) = Type.forall() v (tweak body)
-- tweak t = Type.arrow() t t
-- | Returns `True` if the expression is well-typed, `False` otherwise
wellTyped :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> Term v loc -> f Bool
wellTyped :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc, Semigroup loc) => PrettyPrintEnv -> Env v loc -> Term v loc -> f Bool
wellTyped ppe env term = go <$> runResultT (synthesize ppe Context.PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled env term)
where
go (may, _) = isJust may
Expand Down
45 changes: 26 additions & 19 deletions parser-typechecker/src/Unison/Typechecker/Context.hs
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,8 @@ data InfoNote v loc
-- shadowing.
-- This is used in the LSP.
VarBinding v (Type.Type v loc)
| -- | The usage of a particular variable. We report the variable and its location so we can match a given source location with a specific symbol later in the LSP.
VarMention v loc
deriving (Show)

topLevelComponent :: (Var v) => [(v, Type.Type v loc, RedundantTypeAnnotation)] -> InfoNote v loc
Expand Down Expand Up @@ -1004,7 +1006,7 @@ withEffects handled act = do
pruneWanted [] want handled

synthesizeApps ::
(Foldable f, Var v, Ord loc) =>
(Foldable f, Var v, Ord loc, Semigroup loc) =>
Term v loc ->
Type v loc ->
f (Term v loc) ->
Expand All @@ -1022,7 +1024,7 @@ synthesizeApps fun ft args =
-- the process.
-- e.g. in `(f:t) x` -- finds the type of (f x) given t and x.
synthesizeApp ::
(Var v, Ord loc) =>
(Var v, Ord loc, Semigroup loc) =>
Term v loc ->
Type v loc ->
(Term v loc, Int) ->
Expand Down Expand Up @@ -1094,7 +1096,7 @@ generalizeExistentials' t =
isExistential _ = False

noteTopLevelType ::
(Ord loc, Var v) =>
(Ord loc, Var v, Semigroup loc) =>
ABT.Subst f v a ->
Term v loc ->
Type v loc ->
Expand Down Expand Up @@ -1124,8 +1126,12 @@ noteTopLevelType e binding typ = case binding of
noteVarBinding :: (Var v) => v -> Type.Type v loc -> M v loc ()
noteVarBinding v t = btw $ VarBinding v t

noteVarMention :: (Var v) => v -> loc -> M v loc ()
noteVarMention v loc = do
btw $ VarMention v loc

synthesizeTop ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Term v loc ->
M v loc (Type v loc)
Expand All @@ -1146,7 +1152,7 @@ synthesizeTop tm = do
-- the process. Also collect wanted abilities.
-- | Figure 11 from the paper
synthesize ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Term v loc ->
M v loc (Type v loc, Wanted v loc)
Expand Down Expand Up @@ -1179,11 +1185,12 @@ wantRequest loc ty =
-- The return value is the synthesized type together with a list of
-- wanted abilities.
synthesizeWanted ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Term v loc ->
M v loc (Type v loc, Wanted v loc)
synthesizeWanted (Term.Var' v) =
synthesizeWanted trm@(Term.Var' v) = do
noteVarMention v (ABT.annotation trm)
getContext >>= \ctx ->
case lookupAnn ctx v of -- Var
Nothing -> compilerCrash $ UndeclaredTermVariable v ctx
Expand Down Expand Up @@ -1415,7 +1422,7 @@ synthesizeWanted _e = compilerCrash PatternMatchFailure
-- can be refined later. This is a bit unusual for the algorithm we
-- use, but it seems like it should be safe.
synthesizeBinding ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Bool ->
Term v loc ->
Expand Down Expand Up @@ -1556,7 +1563,7 @@ ensurePatternCoverage theMatch _theMatchType _scrutinee scrutineeType cases = do
checkUncovered *> checkRedundant

checkCases ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Type v loc ->
Type v loc ->
Expand Down Expand Up @@ -1621,7 +1628,7 @@ requestType ps =

checkCase ::
forall v loc.
(Var v, Ord loc) =>
(Var v, Ord loc, Semigroup loc) =>
Type v loc ->
Type v loc ->
Term.MatchCase loc (Term v loc) ->
Expand Down Expand Up @@ -1845,7 +1852,7 @@ resetContextAfter x a = do
-- their type. Also returns the freshened version of `body`.
-- See usage in `synthesize` and `check` for `LetRec'` case.
annotateLetRecBindings ::
(Var v, Ord loc) =>
(Var v, Ord loc, Semigroup loc) =>
loc ->
Term.IsTop ->
((v -> M v loc v) -> M v loc ([(v, Term v loc)], Term v loc)) ->
Expand Down Expand Up @@ -2146,7 +2153,7 @@ variableP _ = Nothing
-- See its usage in `synthesize` and `annotateLetRecBindings`.
checkScoped ::
forall v loc.
(Var v, Ord loc) =>
(Var v, Ord loc, Semigroup loc) =>
Term v loc ->
Type v loc ->
M v loc (Type v loc, Wanted v loc)
Expand All @@ -2163,7 +2170,7 @@ checkScoped e t = do
(t,) <$> check e t

checkScopedWith ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Term v loc ->
Type v loc ->
Expand Down Expand Up @@ -2425,7 +2432,7 @@ relax' nonArrow v t
tv = Type.var loc (TypeVar.Existential B.Blank v)

checkWantedScoped ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Wanted v loc ->
Term v loc ->
Expand All @@ -2435,7 +2442,7 @@ checkWantedScoped want m ty =
scope (InCheck m ty) $ checkWanted want m ty

checkWanted ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Wanted v loc ->
Term v loc ->
Expand Down Expand Up @@ -2497,7 +2504,7 @@ checkWanted want e t = do
-- `m` has type `t` with abilities `es`,
-- updating the context in the process.
checkWithAbilities ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
[Type v loc] ->
Term v loc ->
Expand All @@ -2513,7 +2520,7 @@ checkWithAbilities es m t = do
-- `m` has type `t`
-- updating the context in the process.
check ::
(Var v) =>
(Var v, Semigroup loc) =>
(Ord loc) =>
Term v loc ->
Type v loc ->
Expand Down Expand Up @@ -3219,7 +3226,7 @@ verifyDataDeclarations decls = forM_ (Map.toList decls) $ \(_ref, decl) -> do

-- | public interface to the typechecker
synthesizeClosed ::
(BuiltinAnnotation loc, Var v, Ord loc, Show loc) =>
(BuiltinAnnotation loc, Var v, Ord loc, Show loc, Semigroup loc) =>
PrettyPrintEnv ->
PatternMatchCoverageCheckAndKindInferenceSwitch ->
[Type v loc] ->
Expand Down Expand Up @@ -3308,7 +3315,7 @@ run ppe pmcSwitch datas effects m =
$ Env 1 context0

synthesizeClosed' ::
(Var v, Ord loc) =>
(Var v, Ord loc, Semigroup loc) =>
[Type v loc] ->
Term v loc ->
M v loc (Type v loc)
Expand Down
29 changes: 22 additions & 7 deletions unison-cli/src/Unison/LSP/FileAnalysis.hs
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,6 @@ import Unison.Referent qualified as Referent
import Unison.Result (Note)
import Unison.Result qualified as Result
import Unison.Symbol (Symbol)
import Unison.Symbol qualified as Symbol
import Unison.Syntax.HashQualifiedPrime qualified as HQ' (toText)
import Unison.Syntax.Lexer.Unison qualified as L
import Unison.Syntax.Name qualified as Name
Expand Down Expand Up @@ -107,20 +106,36 @@ checkFile doc = runMaybeT do
Result.Result _ (Just parsedFile) -> do
typecheckingEnv <- computeTypecheckingEnvironment (ShouldUseTndr'Yes parsingEnv) cb ambientAbilities parsedFile
let Result.Result typecheckingNotes maybeTypecheckedFile = FileParsers.synthesizeFile typecheckingEnv parsedFile
localBindings <-
for maybeTypecheckedFile \tf -> do
let parsedVars =
UF.terms parsedFile
& foldMap (ABT.allVars . snd)
let typeCheckvars =
UF.hashTermsId tf
& foldMap (\(_a, _tr, _wk, trm, _typ) -> ABT.allVars trm)
Debug.debugM Debug.Temp "Parsed Vars" $ parsedVars
Debug.debugM Debug.Temp "Typecheck Vars" $ typeCheckvars

symbolTypes <-
typecheckingNotes
& Foldable.toList
& reverse -- Type notes that come later in typechecking have more information filled in.
& foldMap \case
Result.TypeInfo (Context.VarBinding (Symbol.Symbol _ (Var.User n)) typ) ->
Map.singleton (Symbol.Symbol 0 (Var.User n)) typ
Result.TypeInfo (Context.VarBinding v typ) -> Map.singleton v typ
_ -> mempty
& pure
let localBindings =
typecheckingNotes
& Foldable.toList
& reverse -- Type notes that come later in typechecking have more information filled in.
& foldMap \case
Result.TypeInfo (Context.VarMention v loc) ->
case Map.lookup v symbolTypes of
Just typ -> (annToInterval loc) & foldMap \interval -> (IM.singleton interval typ)
_ -> mempty
_ -> mempty
pure (localBindings, typecheckingNotes, Just parsedFile, maybeTypecheckedFile)

Debug.debugM Debug.Temp "BEFORE Local Bindings" ()
Debug.debugM Debug.Temp "My Local Bindings" localBindingTypes
Debug.debugM Debug.Temp "AFTER Local Bindings" ()
filePPED <- lift $ ppedForFileHelper parsedFile typecheckedFile
(errDiagnostics, codeActions) <- lift $ analyseFile fileUri srcText filePPED notes
let codeActionRanges =
Expand Down
4 changes: 2 additions & 2 deletions unison-cli/src/Unison/LSP/Hover.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module Unison.LSP.Hover where

import Control.Lens hiding (List)
import Control.Monad.Reader
import Data.Map qualified as Map
import Data.IntervalMap.Lazy qualified as IM
import Data.Text qualified as Text
import Language.LSP.Protocol.Lens
import Language.LSP.Protocol.Message qualified as Msg
Expand Down Expand Up @@ -139,7 +139,7 @@ hoverInfo uri pos =
FileAnalysis {localBindingTypes} <- FileAnalysis.getFileAnalysis uri
Debug.debugM Debug.Temp "pos" pos
Debug.debugM Debug.Temp "localBindingTypes" localBindingTypes
typ <- hoistMaybe $ Map.lookup localVar localBindingTypes
(_range, typ) <- hoistMaybe $ IM.lookupMin $ IM.intersecting localBindingTypes (IM.ClosedInterval pos pos)
pped <- lift $ ppedForFile uri
let varName = case localVar of
(Symbol.Symbol _ (Var.User name)) -> name
Expand Down
7 changes: 2 additions & 5 deletions unison-cli/src/Unison/LSP/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -124,11 +124,8 @@ data FileAnalysis = FileAnalysis
notes :: Seq (Note Symbol Ann),
diagnostics :: IntervalMap Position [Diagnostic],
codeActions :: IntervalMap Position [CodeAction],
-- | The types of local variable bindings keyed by the span that they're valid.
-- There may be many mentions of the same symbol in the file, and their may be several
-- bindings which shadow each other, use this map to find the smallest spanning position
-- which contains the symbol you're interested in.
localBindingTypes :: Map Symbol (Type Symbol Ann),
-- | The types of local variable bindings keyed by the mention's location.
localBindingTypes :: IntervalMap Position (Type Symbol Ann),
typeSignatureHints :: Map Symbol TypeSignatureHint,
fileSummary :: Maybe FileSummary
}
Expand Down

0 comments on commit 5fe41c2

Please sign in to comment.