Skip to content

Commit ea758a6

Browse files
nvarnernvarner
committed
no anonymous function symbols
1 parent 05d5f51 commit ea758a6

File tree

7 files changed

+117
-54
lines changed

7 files changed

+117
-54
lines changed

‎agda-language-server.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -185,6 +185,7 @@ test-suite als-test
185185
main-is: Test.hs
186186
other-modules:
187187
Test.Indexer.Invariants
188+
Test.Indexer.NoAnonFunSymbol
188189
Test.Indexer.NoDuplicateDecl
189190
Test.Indexer.NoMissing
190191
Test.Indexer.NoOverlap

‎src/Indexer/Indexer.hs‎

Lines changed: 20 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ import qualified Agda.Utils.List1 as List1
2222
import Agda.Utils.Maybe (whenJust)
2323
import Agda.Utils.Monad (when)
2424
import Data.Foldable (forM_, traverse_)
25+
import Data.Functor.Compose (Compose (Compose, getCompose))
2526
import qualified Data.Set as Set
2627
import Data.Void (absurd)
2728
import Indexer.Monad
@@ -100,7 +101,7 @@ instance Indexable A.Declaration where
100101
A.FunDef _defInfo name clauses -> withBindingKind DefBinding $ do
101102
-- function declarations are captured by the `Axiom` case
102103
withParent name $ do
103-
index clauses
104+
index $ WithLHSNaming LHSNamed <$> clauses
104105
A.DataSig defInfo _erased name genTel type' ->
105106
withBindingKind DeclBinding $ do
106107
tellDecl name Data type'
@@ -200,7 +201,7 @@ instance Indexable A.Expr where
200201
return ()
201202
A.ExtendedLam _exprInfo defInfo _erased _generatedFn clauses -> do
202203
index defInfo
203-
index clauses
204+
index $ WithLHSNaming LHSAnonymous <$> clauses
204205
A.Pi _exprInfo tel type' -> do
205206
index tel
206207
index type'
@@ -335,28 +336,33 @@ instance Indexable A.WhereDeclarations where
335336
A.WhereDecls Nothing _ decl ->
336337
index decl
337338

338-
instance (Indexable a) => Indexable (A.LHSCore' a) where
339-
index core = case core of
339+
data LHSNaming = LHSNamed | LHSAnonymous deriving (Eq)
340+
341+
data WithLHSNaming a = WithLHSNaming LHSNaming a
342+
343+
instance (Indexable a) => Indexable (WithLHSNaming (A.LHSCore' a)) where
344+
index (WithLHSNaming lhsNaming core) = case core of
340345
A.LHSHead name pats -> do
341-
tellDef name Param UnknownType
346+
when (lhsNaming == LHSNamed) $
347+
tellDef name Param UnknownType
342348
indexNamedArgs name pats
343349
A.LHSProj destructor focus pats -> do
344350
tellUsage destructor
345351
-- TODO: what does the named arg in `focus` mean?
346-
indexNamedArgs destructor [focus]
352+
indexNamedArgs destructor [getCompose $ WithLHSNaming lhsNaming <$> Compose focus]
347353
indexNamedArgs destructor pats
348354
A.LHSWith lhsHead withPatterns pats -> do
349-
index lhsHead
355+
index $ WithLHSNaming lhsNaming lhsHead
350356
index withPatterns
351357
-- TODO: what do the named args mean?
352358
forM_ pats $ \(C.Arg argInfo (C.Named _name pat)) ->
353359
when (C.argInfoOrigin argInfo == C.UserWritten) $
354360
index pat
355361

356-
instance Indexable A.LHS where
357-
index (A.LHS lhsInfo core) = case Info.lhsEllipsis lhsInfo of
362+
instance Indexable (WithLHSNaming A.LHS) where
363+
index (WithLHSNaming lhsNaming (A.LHS lhsInfo core)) = case Info.lhsEllipsis lhsInfo of
358364
C.ExpandedEllipsis _range _withArgs -> return ()
359-
C.NoEllipsis -> index core
365+
C.NoEllipsis -> index $ WithLHSNaming lhsNaming core
360366

361367
instance Indexable A.RewriteEqn where
362368
index eqn = case eqn of
@@ -382,15 +388,15 @@ instance Indexable A.RHS where
382388
return ()
383389
A.WithRHS _generatedFn withExprs clauses -> do
384390
forM_ withExprs indexWithExpr
385-
index clauses
391+
index $ WithLHSNaming LHSAnonymous <$> clauses
386392
A.RewriteRHS rewriteExprs _strippedPats rewriteRhs whereDecls -> do
387393
index rewriteExprs
388394
index rewriteRhs
389395
index whereDecls
390396

391-
instance (Indexable a) => Indexable (A.Clause' a) where
392-
index (A.Clause lhs _strippedPats rhs whereDecls _catchall) = do
393-
index lhs
397+
instance Indexable (WithLHSNaming A.Clause) where
398+
index (WithLHSNaming lhsNaming (A.Clause lhs _strippedPats rhs whereDecls _catchall)) = do
399+
index $ WithLHSNaming lhsNaming lhs
394400
index rhs
395401
index whereDecls
396402

‎test/Test.hs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ import Test.Tasty.Options
1212
import qualified Test.Model as Model
1313
import qualified Test.ModelMonad as ModelMonad
1414
import qualified Test.Indexer.Invariants as IndexerInvariants
15+
import qualified Test.Indexer.NoAnonFunSymbol as NoAnonFunSymbol
1516

1617
-- Define the custom option
1718
newtype AlsPathOption = AlsPathOption FilePath
@@ -39,7 +40,8 @@ tests = do
3940
LSP.tests alsPath,
4041
Model.tests,
4142
ModelMonad.tests,
42-
indexerInvariantsTest
43+
indexerInvariantsTest,
44+
NoAnonFunSymbol.tests
4345
#if defined(wasm32_HOST_ARCH)
4446
, WASM.tests alsPath
4547
#endif

‎test/Test/Indexer/Invariants.hs‎

Lines changed: 2 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -22,49 +22,14 @@ import Test.Indexer.NoMissing (testNoMissing)
2222
import Test.Indexer.NoOverlap (testNoOverlap)
2323
import Test.Tasty (TestTree, testGroup)
2424
import Test.Tasty.Golden (findByExtension)
25+
import TestData (AgdaFileDetails (AgdaFileDetails))
2526
import qualified TestData
2627

2728
tests :: IO TestTree
2829
tests = do
2930
inPaths <- findByExtension [".agda"] "test/data/Indexer"
3031
files <- forM inPaths $ \inPath -> do
31-
let testName = takeBaseName inPath
32-
uri = LSP.filePathToUri inPath
33-
model <- TestData.getModel
34-
35-
(file, interface) <- LSP.runLspT undefined $ do
36-
env <- TestData.getServerEnv model
37-
runServerT env $ do
38-
interface <- runWithAgdaLib uri $ do
39-
TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions
40-
absInPath <- liftIO $ absolute inPath
41-
let srcFile = SourceFile absInPath
42-
src <- TCM.liftTCM $ Imp.parseSource srcFile
43-
44-
TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src)
45-
checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src
46-
return $ Imp.crInterface checkResult
47-
48-
ast <- runWithAgdaLib uri $ do
49-
TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions
50-
absInPath <- liftIO $ absolute inPath
51-
let srcFile = SourceFile absInPath
52-
src <- TCM.liftTCM $ Imp.parseSource srcFile
53-
54-
withAstFor src return
55-
56-
-- Write the AST to a file for debugging purposes
57-
liftIO $ writeFile ("test/data/AST" </> testName) $ prettyShow $ topLevelDecls ast
58-
59-
runWithAgdaLib uri $ do
60-
TCM.liftTCM $ TCM.setCommandLineOptions defaultOptions
61-
absInPath <- liftIO $ absolute inPath
62-
let srcFile = SourceFile absInPath
63-
src <- TCM.liftTCM $ Imp.parseSource srcFile
64-
65-
agdaFile <- indexFile src
66-
return (agdaFile, interface)
67-
32+
TestData.AgdaFileDetails testName file interface <- TestData.agdaFileDetails inPath
6833
return (testName, file, interface)
6934

7035
return $

‎test/Test/Indexer/NoAnonFunSymbol.hs‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
module Test.Indexer.NoAnonFunSymbol (tests) where
2+
3+
import Agda.Syntax.Common.Pretty (prettyShow)
4+
import Agda.Utils.Lens ((^.))
5+
import Agda.Utils.Maybe (ifJustM, whenJust, whenJustM)
6+
import Control.Monad (forM)
7+
import Data.Foldable (find)
8+
import Data.List (isInfixOf)
9+
import qualified Data.Map as Map
10+
import Server.Model.AgdaFile (agdaFileSymbols)
11+
import Test.Tasty (TestTree)
12+
import Test.Tasty.HUnit (assertFailure, testCase)
13+
import qualified TestData
14+
15+
tests :: TestTree
16+
tests =
17+
testCase "No symbols for internal anonymous function names" $ do
18+
TestData.AgdaFileDetails name agdaFile interface <- TestData.agdaFileDetails "test/data/AnonFun.agda"
19+
20+
let symbolNames = prettyShow <$> Map.keys (agdaFile ^. agdaFileSymbols)
21+
whenJust (find isAnonFunName symbolNames) $ \name ->
22+
assertFailure $ "Found symbol for internal anonymous function: " ++ name
23+
24+
isAnonFunName :: String -> Bool
25+
isAnonFunName name = ".extendedlambda" `isInfixOf` name

‎test/TestData.hs‎

Lines changed: 62 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,23 +8,83 @@ module TestData
88
fileUri3,
99
fakeUri,
1010
getServerEnv,
11+
AgdaFileDetails (..),
12+
agdaFileDetails,
1113
)
1214
where
1315

16+
import Agda.Interaction.FindFile (SourceFile (SourceFile), srcFilePath)
17+
import qualified Agda.Interaction.Imports as Imp
18+
import qualified Agda.Interaction.Options
19+
import Agda.Syntax.Abstract.More ()
20+
import Agda.Syntax.Common.Pretty (prettyShow)
21+
import Agda.Syntax.Translation.ConcreteToAbstract (topLevelDecls)
22+
import qualified Agda.TypeChecking.Monad as TCM
23+
import Agda.Utils.FileName (absolute)
1424
import Agda.Utils.IORef (newIORef)
1525
import Agda.Utils.Lens (set, (<&>))
1626
import Control.Concurrent (newChan)
1727
import Control.Monad.IO.Class (MonadIO, liftIO)
1828
import qualified Data.Map as Map
29+
import Indexer (indexFile, withAstFor)
1930
import qualified Language.LSP.Protocol.Message as LSP
2031
import qualified Language.LSP.Protocol.Types as LSP
21-
import Monad (Env (Env))
32+
import qualified Language.LSP.Server as LSP
33+
import Monad (Env (Env), runServerT)
2234
import Options (defaultOptions, initConfig)
2335
import qualified Server.CommandController as CommandController
2436
import Server.Model (Model (Model))
25-
import Server.Model.AgdaFile (emptyAgdaFile)
37+
import Server.Model.AgdaFile (AgdaFile, emptyAgdaFile)
2638
import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib)
39+
import Server.Model.Monad (runWithAgdaLib)
2740
import qualified Server.ResponseController as ResponseController
41+
import System.FilePath (takeBaseName, (</>))
42+
43+
data AgdaFileDetails = AgdaFileDetails
44+
{ fileName :: String,
45+
agdaFile :: AgdaFile,
46+
interface :: TCM.Interface
47+
}
48+
49+
agdaFileDetails :: FilePath -> IO AgdaFileDetails
50+
agdaFileDetails inPath = do
51+
let testName = takeBaseName inPath
52+
uri = LSP.filePathToUri inPath
53+
model <- TestData.getModel
54+
55+
(file, interface) <- LSP.runLspT undefined $ do
56+
env <- TestData.getServerEnv model
57+
runServerT env $ do
58+
interface <- runWithAgdaLib uri $ do
59+
TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions
60+
absInPath <- liftIO $ absolute inPath
61+
let srcFile = SourceFile absInPath
62+
src <- TCM.liftTCM $ Imp.parseSource srcFile
63+
64+
TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src)
65+
checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src
66+
return $ Imp.crInterface checkResult
67+
68+
ast <- runWithAgdaLib uri $ do
69+
TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions
70+
absInPath <- liftIO $ absolute inPath
71+
let srcFile = SourceFile absInPath
72+
src <- TCM.liftTCM $ Imp.parseSource srcFile
73+
74+
withAstFor src return
75+
76+
runWithAgdaLib uri $ do
77+
TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions
78+
absInPath <- liftIO $ absolute inPath
79+
let srcFile = SourceFile absInPath
80+
src <- TCM.liftTCM $ Imp.parseSource srcFile
81+
82+
agdaFile <- indexFile src
83+
return (agdaFile, interface)
84+
85+
return $ AgdaFileDetails testName file interface
86+
87+
--------------------------------------------------------------------------------
2888

2989
documentSymbolMessage :: LSP.NormalizedUri -> LSP.TRequestMessage LSP.Method_TextDocumentDocumentSymbol
3090
documentSymbolMessage uri =

‎test/data/AnonFun.agda‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
module AnonFun where
2+
3+
f : {A : Set} -> A -> A
4+
f = \where x -> x

0 commit comments

Comments
 (0)