Agda JSON backend

Main.hs

module Main (main) where

import Agda.Compiler.Backend (Backend (..), Backend' (..), Recompile (Recompile), callBackend, setTCLens)
import Agda.Compiler.Common (IsMain (..))
import Agda.Interaction.BasicOps (atTopLevel)
import Agda.Interaction.FindFile (SourceFile (..))
import Agda.Interaction.Imports (CheckResult (..), Mode (..), parseSource, typeCheckMain)
import Agda.Interaction.Options qualified as A (defaultOptions)
import Agda.Syntax.Abstract.Name qualified as A (ModuleName, QName (..))
import Agda.Syntax.Internal qualified as A (Name (..))
import Agda.Syntax.Scope.Base (publicNames)
import Agda.Syntax.Scope.Base qualified as A
import Agda.TypeChecking.Monad (TCErr, TCM, getScope, runTCMTop, stBackends)
import Agda.TypeChecking.Monad qualified as A (Definition (..))
import Agda.TypeChecking.Monad.Options (setCommandLineOptions)
import Agda.Utils.FileName (AbsolutePath, mkAbsolute)
import Control.Monad.IO.Class (MonadIO (liftIO))
import Conversion
import Data.Aeson (encode)
import Data.ByteString.Lazy.Char8 qualified as B (writeFile)
import Data.Map qualified as Map
import Data.Set qualified as Set
import System.Directory (canonicalizePath, getCurrentDirectory)
import System.Environment (getArgs)
import System.FilePath ((</>))

check :: AbsolutePath -> TCM CheckResult
check inputFile = typeCheckMain TypeCheck =<< parseSource (SourceFile inputFile)

runTCM :: TCM a -> IO (Either TCErr a)
runTCM = runTCMTop

indexerBackend :: Backend
indexerBackend = Backend indexerBackend'

indexerBackend' :: Backend' () () () [Def] (A.Name, Def)
indexerBackend' =
  Backend'
    { backendName = "indexer",
      backendVersion = Nothing,
      options = (),
      commandLineFlags = [],
      isEnabled = const True,
      preCompile = const $ return (),
      postCompile = postCompileIndexer,
      preModule = preModuleIndexer,
      postModule = postModuleIndexer,
      compileDef = compileDefIndexer,
      scopeCheckingSuffices = False,
      mayEraseType = const $ return False
    }

preModuleIndexer ::
  Applicative m =>
  () ->
  IsMain ->
  A.ModuleName ->
  Maybe FilePath ->
  m (Recompile () [Def])
preModuleIndexer _ _ mod _ = pure $ Recompile ()

postModuleIndexer ::
  () ->
  () ->
  IsMain ->
  A.ModuleName ->
  [(A.Name, Def)] ->
  TCM [Def]
postModuleIndexer _ _ _ _ defs = do
  topLevelNames <-
    atTopLevel $
      Set.map (A.qnameName . A.anameName) . publicNames <$> getScope
  -- filter out defintions that are not top-level
  return $
    map snd $
      filter (\d -> fst d `Set.member` topLevelNames) defs

compileDefIndexer ::
  () ->
  () ->
  IsMain ->
  A.Definition ->
  TCM (A.Name, Def)
compileDefIndexer _ _ _ d =
  -- convert type to a JSON encodable representation
  return (A.qnameName (A.defName d), convertDefinition d)

postCompileIndexer :: () -> IsMain -> Map.Map A.ModuleName [Def] -> TCM ()
postCompileIndexer _ _ m = do
  let defs :: [Def] = concat $ Map.elems m
  liftIO $ do
    putStrLn $ "compiled " <> show (length defs) <> " definitions"
    B.writeFile "output.json" $ encode defs
    putStrLn "Written output.json"

-- gets all definitions in scope of the file given
runIndexer :: AbsolutePath -> TCM ()
runIndexer path = do
  setCommandLineOptions A.defaultOptions
  stBackends `setTCLens` [indexerBackend] -- inject indexer backend
  res <- check path
  callBackend "indexer" IsMain res

main :: IO ()
main = do
  args <- getArgs
  cwd <- getCurrentDirectory
  testFilePath <- canonicalizePath $ cwd </> head args

  let path = mkAbsolute testFilePath
  putStrLn $ "Building index for " <> show path
  _ <- runTCM $ runIndexer path

  return ()