Skip to content

Instantly share code, notes, and snippets.

@zoeyfyi
Created November 22, 2022 07:12
Show Gist options
  • Save zoeyfyi/8077e27688d8a4095660ba4bfc40f8e6 to your computer and use it in GitHub Desktop.
Save zoeyfyi/8077e27688d8a4095660ba4bfc40f8e6 to your computer and use it in GitHub Desktop.
Agda JSON backend
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 ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment