Initial commit

Author: omelkonian

.gitignore

@@ -0,0 +1,4 @@
+_build
+dist
+dist-newstyle
+*~

README.md

@@ -0,0 +1,4 @@
+# Minimal skeleton for developing a new Agda backend 
+
+- The backend is defined in `src/Main.hs`.
+- The `test/` directory contains an example compilation of `Test.agda` to `Test.txt`.

agda2min.cabal

@@ -0,0 +1,22 @@
+cabal-version:       2.2
+name:                agda2min
+version:             1.1
+author:              ???
+category:            Language, Compiler
+build-type:          Simple
+synopsis:            Compiling Agda code to ??.
+
+extra-doc-files:    README.md
+
+source-repository head
+  type:     git
+  location: https://github.com/omelkonian/agda-minimal-backend.git
+
+executable agda2min
+  hs-source-dirs:      src
+  main-is:             Main.hs
+  other-modules:       Paths_agda2min
+  autogen-modules:     Paths_agda2min
+  build-depends:       base >= 4.10 && < 4.18,
+                       Agda >= 2.6.4 && < 2.6.5,
+                       deepseq >= 1.4.4 && < 1.6

src/Main.hs

@@ -0,0 +1,86 @@
+{-# LANGUAGE LambdaCase, RecordWildCards #-}
+module Main where
+
+import Data.Maybe ( fromMaybe )
+import Control.Monad ( unless )
+import Control.Monad.IO.Class ( MonadIO(liftIO) )
+import Control.DeepSeq ( NFData(..) )
+
+import System.Console.GetOpt ( OptDescr(Option), ArgDescr(ReqArg) )
+
+import Data.Version ( showVersion )
+import Paths_agda2min ( version )
+
+import Agda.Syntax.Common.Pretty ( prettyShow )
+import Agda.Syntax.Internal ( qnameName, qnameModule )
+import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName, moduleNameToFileName )
+
+import Agda.Compiler.Common ( curIF, compileDir )
+import Agda.Compiler.Backend ( Backend(..), Backend'(..), Recompile(..), IsMain )
+
+import Agda.TypeChecking.Monad.Base ( Definition(..) )
+import Agda.TypeChecking.Monad
+  ( TCM, withCurrentModule, iInsideScope, setScope
+  , CompilerPragma(..), getUniqueCompilerPragma )
+
+import Agda.Main ( runAgda )
+
+main = runAgda [Backend backend]
+
+data Options = Options { optOutDir :: Maybe FilePath }
+
+instance NFData Options where
+  rnf _ = ()
+
+outdirOpt :: Monad m => FilePath -> Options -> m Options
+outdirOpt dir opts = return opts{ optOutDir = Just dir }
+
+defaultOptions :: Options
+defaultOptions = Options{ optOutDir = Nothing }
+
+type ModuleEnv = ()
+type ModuleRes = ()
+type CompiledDef = String
+
+backend :: Backend' Options Options ModuleEnv ModuleRes CompiledDef
+backend = Backend'
+  { backendName           = "agda2??"
+  , backendVersion        = Just (showVersion version)
+  , options               = defaultOptions
+  , commandLineFlags      =
+      [ Option ['o'] ["out-dir"] (ReqArg outdirOpt "DIR")
+        "Write output files to DIR. (default: project root)"
+      ]
+  , isEnabled             = \ _ -> True
+  , preCompile            = return
+  , postCompile           = \ _ _ _ -> return ()
+  , preModule             = moduleSetup
+  , postModule            = writeModule
+  , compileDef            = compile
+  , scopeCheckingSuffices = False
+  , mayEraseType          = \ _ -> return True
+  }
+
+moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath
+            -> TCM (Recompile ModuleEnv ModuleRes)
+moduleSetup _ _ m _ = do
+  setScope . iInsideScope =<< curIF
+  return $ Recompile ()
+
+compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
+compile opts tlm _ Defn{..}
+  = withCurrentModule (qnameModule defName)
+  $ getUniqueCompilerPragma "AGDA2??" defName >>= \case
+      Nothing -> return []
+      Just (CompilerPragma _ _) ->
+        return $ prettyShow (qnameName defName) <> " = " <> prettyShow theDef
+
+writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName -> [CompiledDef]
+            -> TCM ModuleRes
+writeModule opts _ _ m cdefs = do
+  outDir <- compileDir
+  liftIO $ putStrLn (moduleNameToFileName m "txt")
+  let outFile = fromMaybe outDir (optOutDir opts) <> "/" <> moduleNameToFileName m "txt"
+  unless (all null cdefs) $ liftIO
+    $ writeFile outFile
+    $ "*** module " <> prettyShow m <> " ***\n" <> unlines cdefs

test/Test.agda

@@ -0,0 +1,49 @@
+module _ where
+
+open import Agda.Builtin.Nat using (Nat; _+_; _*_)
+open import Agda.Builtin.List using (List; []; _∷_)
+
+variable a b : Set
+
+-- ** Datatypes & functions
+
+data Exp (v : Set) : Set where
+  Plus : Exp v → Exp v → Exp v
+  Int : Nat → Exp v
+  Var : v → Exp v
+{-# COMPILE AGDA2?? Exp #-}
+
+eval : (a → Nat) → Exp a → Nat
+eval env (Plus a b) = eval env a + eval env b
+eval env (Int n) = n
+eval env (Var x) = env x
+{-# COMPILE AGDA2?? eval #-}
+
+-- ** Natural numbers
+
+sum : List Nat → Nat
+sum []       = 0
+sum (x ∷ xs) = x + sum xs
+{-# COMPILE AGDA2?? sum #-}
+
+-- ** Polymorphic functions
+
+_++_ : List a → List a → List a
+[]       ++ ys = ys
+(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
+{-# COMPILE AGDA2?? _++_ #-}
+
+map : (a → b) → List a → List b
+map f [] = []
+map f (x ∷ xs) = f x ∷ map f xs
+{-# COMPILE AGDA2?? map #-}
+
+-- ** Lambdas
+
+plus3 : List Nat → List Nat
+plus3 = map (λ n → n + 3)
+{-# COMPILE AGDA2?? plus3 #-}
+
+doubleLambda : Nat → Nat → Nat
+doubleLambda = λ a b → a + 2 * b
+{-# COMPILE AGDA2?? doubleLambda #-}