WIP: Agda backend prototype

.gitignore

@@ -21,3 +21,4 @@ cabal.project.local
 .HTF/
 output/
 *.ibc
+*.agdai

frontend-test/agda/Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

frontend-test/agda/agda-grin.cabal

@@ -0,0 +1,31 @@
+-- Initial agda-grin.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                agda-grin
+version:             0.1.0.0
+-- synopsis:
+-- description:
+license:             BSD3
+license-file:        LICENSE
+author:              Philipp Hausmann
+maintainer:          ph_git@314.ch
+-- copyright:
+category:            Development
+build-type:          Simple
+extra-source-files:  ChangeLog.md
+cabal-version:       >=1.10
+
+executable agda-grin
+  default-language: Haskell2010
+  main-is:        Main.hs
+  hs-source-dirs: src
+
+  build-depends:  Agda
+                , base
+                , containers
+                , directory
+                , filepath
+                , mtl
+                , transformers
+                , grin
+                , ansi-wl-pprint

frontend-test/agda/default.nix

@@ -0,0 +1,15 @@
+{ mkDerivation, Agda, ansi-wl-pprint, base, containers, directory
+, filepath, grin, mtl, stdenv, transformers
+}:
+mkDerivation {
+  pname = "agda-grin";
+  version = "0.1.0.0";
+  src = ./.;
+  isLibrary = false;
+  isExecutable = true;
+  executableHaskellDepends = [
+    Agda ansi-wl-pprint base containers directory filepath grin mtl
+    transformers
+  ];
+  license = stdenv.lib.licenses.bsd3;
+}

frontend-test/agda/examples/Simple.agda

@@ -0,0 +1,9 @@
+
+data Nat : Set where
+  Z : Nat
+  S : Nat -> Nat
+
+_+_ : Nat -> Nat -> Nat
+x + Z = x
+Z + y = y
+S x + y = S (x + y)

frontend-test/agda/shell.nix

@@ -0,0 +1,75 @@
+{ fetchFromGitHub ? (import <nixpkgs> {}).fetchFromGitHub
+# peg nix packages to specific version
+, pkgs ?
+    import
+      ( fetchFromGitHub
+        {
+          owner = "NixOS";
+          repo = "nixpkgs-channels";
+          rev = "696c6bed4e8e2d9fd9b956dea7e5d49531e9d13f";
+          sha256 = "1v3yrpj542niyxp0h3kffsdjwlrkvj0mg4ljb85d142gyn3sdzd4";
+        }
+      ) {}
+}:
+let
+    # extract the Haskell dependencies of a package
+    extractHaskellDependencies = (hpkg:
+        with builtins;
+        let
+          isHaskellPkg = x: (isAttrs x) && (x ? pname) && (x ? version) && (x ? env);
+          packagesFromDrv = x:
+            let
+              inputs =
+                (x.buildInputs or []) ++
+                (x.nativeBuildInputs or []) ++
+                (x.propagatedBuildInputs or []) ++
+                (x.propagatedNativeBuildInputs or []);
+
+            in
+              (filter isHaskellPkg  inputs);
+          go1 = s: xs: foldl' go2 s xs;
+          go2 = s: x:
+            if s ? "${x.pname}"
+               then s
+               else go1 (s // {"${x.pname}" = x;}) (packagesFromDrv x);
+        in assert isAttrs hpkg; attrNames (go1 {} (packagesFromDrv hpkg)));
+
+    # Haskell custom overrides
+    haskellPackages = pkgs.haskell.packages.ghc822.override (old:
+    { overrides = self: super: with pkgs.haskell.lib;
+        {
+          free = self.callPackage ../../nix/free.nix {};
+          functor-infix = doJailbreak (super.functor-infix);
+          llvm-hs = self.callPackage ../../nix/llvm-hs.nix {llvm-config = pkgs.llvm_5;};
+          llvm-hs-pure = self.callPackage ../../nix/llvm-hs-pure.nix {};
+          llvm-hs-pretty = pkgs.haskell.lib.dontCheck (self.callPackage ../../nix/llvm-hs-pretty.nix {});
+          grin = dontHaddock (self.callPackage ../../grin/default.nix {});
+        };
+    });
+
+    # the grin package
+    agda-grin = haskellPackages.callPackage ./. {};
+    # grin's dependencies
+    agdaGrinDeps = extractHaskellDependencies agda-grin;
+    # use a GHC with all the Hakell dependencies and the documentation for them and a Hoogle server to search them
+    ghcWith = haskellPackages.ghcWithHoogle (hs: map (x: builtins.getAttr x hs) agdaGrinDeps);
+
+    llc5 = pkgs.runCommand "llc5"
+      {
+        buildInputs = [pkgs.llvm_5];
+      }
+      ''
+        mkdir -p $out/bin
+        cd $out/bin
+        ln -s ${pkgs.llvm_5}/bin/llc llc-5.0
+      '';
+in
+# environment setup with all the needed tools
+pkgs.runCommand "agda-grin-shell"
+      {
+        shellHook = ''
+          eval $(egrep ^export ${ghcWith}/bin/ghc)
+         '';
+        buildInputs = [ghcWith llc5 pkgs.llvm_5 haskellPackages.cabal-install];
+      }
+      "touch $out"

frontend-test/agda/src/Main.hs

@@ -0,0 +1,140 @@
+module Main where
+
+import Control.Monad.Trans
+import Control.Monad.Reader
+import Data.List
+
+import qualified Agda.Main as M
+import Agda.Compiler.Backend
+import Agda.Interaction.Options
+import Agda.Syntax.Common
+import Agda.Syntax.Literal
+import Agda.Syntax.Treeless as AT
+import Agda.TypeChecking.Pretty
+import Agda.TypeChecking.Monad
+
+import Agda.Utils.Maybe
+import Agda.Compiler.Common
+import Agda.Compiler.Treeless.NormalizeNames
+
+
+import Frontend.Lambda.Syntax as GL
+import Frontend.Lambda.Pretty as GP
+import qualified Text.PrettyPrint.ANSI.Leijen as PP
+
+backend = Backend backend'
+
+backend' :: Backend' Bool () () () (Maybe (String, GL.Exp))
+backend' = Backend'
+  { backendName = "Grin"
+  , backendVersion = Just "ZuriHac"
+  , options = False
+  , commandLineFlags = grinCommandLineFlags
+  , isEnabled = id
+  , preCompile = \_ -> return ()
+  , postCompile = \_ _ _ -> return ()
+  , preModule = \_ _ _ -> return $ Recompile ()
+  , postModule = \_ _ _ _ _ -> return ()
+  , compileDef = grinCompileDef
+  , scopeCheckingSuffices = False
+  }
+
+main :: IO ()
+main = M.runAgda [backend]
+
+type GM = ReaderT GEnv TCM
+
+data GEnv = GEnv
+  { env :: [String]
+  , freshNames :: [String]
+  }
+
+grinCommandLineFlags :: [OptDescr (Flag Bool)]
+grinCommandLineFlags =
+    [ Option []     ["grin"] (NoArg compileGrinFlag) "compile program using the Grin backend"
+    ]
+  where
+    compileGrinFlag o      = return $ True
+
+grinCompileDef :: () -> () -> Definition -> TCM (Maybe (String, GL.Exp))
+grinCompileDef env modEnv def = do
+  case theDef def of
+    Function{} -> do
+      caseMaybeM (toTreeless $ defName def) (pure Nothing) $ \treeless -> do
+        treeless <- normalizeNames treeless
+        reportSDoc "compile.grin" 15 $ text "Treeless: " <+> pretty treeless
+        grin <- runReaderT (toGrin treeless) initialEnv
+        lift $ PP.putDoc $ PP.pretty grin
+        n' <- qnameToG $ defName def
+        return $ Just (n', grin)
+    _ -> return Nothing
+  where initialEnv = GEnv [] ([[c] | c <- ['a'..'z']] ++ [ "z" ++ show i | i <- [0..]])
+
+extendEnv :: Int -> ([String] -> GM GL.Exp) -> GM GL.Exp
+extendEnv n f = do
+  (ns1,ns2) <- splitAt n <$> asks freshNames
+  local (\e -> e { freshNames = ns2, env = ns1 ++ (env e) }) (f ns1)
+
+toGrin :: AT.TTerm -> GM GL.Exp
+toGrin t = case t of
+  AT.TLam t -> extendEnv 1 $ \[nm] ->
+      GL.Lam nm <$> toGrin t
+  AT.TApp (AT.TDef n) ts -> GL.App <$> lift (qnameToG n) <*> traverse toGrin ts
+  AT.TApp (AT.TCon n) ts -> GL.Con <$> lift (qnameToG n) <*> traverse toGrin ts
+  AT.TApp t ts -> foldl GL.AppCore <$> (toGrin t) <*> (traverse toGrin ts)
+  AT.TCon n -> GL.Con <$> lift(qnameToG n) <*> pure []
+  AT.TPrim p -> pure $ GL.Var $ "PRIMMMMMM"
+  AT.TLit l -> pure $ GL.Lit $ litToGrin l
+  AT.TVar i -> GL.Var . (!! i) <$> asks env
+  AT.TLet t1 t2 -> do
+    t1' <- toGrin t1
+    extendEnv 1 $ \[nm] -> do
+      GL.Let [(nm, t1')] <$> toGrin t2
+  AT.TCase sc ct def alts -> do
+    sc' <- toGrin $ AT.TVar sc
+    alts' <- traverse altToGrin alts
+    alts' <- if AT.isUnreachable def then return alts' else do
+      def' <- toGrin def
+      return $ alts' ++ [GL.Alt GL.DefaultPat def']
+    return $ GL.Case sc' alts'
+  _ -> error $ show t
+
+  where
+    litToGrin l = case l of
+      LitNat _ n -> GL.LInt64 $ fromInteger n
+      _ -> undefined
+
+    altToGrin a = case a of
+      AT.TACon {aCon = n, aArity = ar, aBody = b} ->
+        extendEnv ar $ \nms -> do
+          n' <- lift $ qnameToG n
+          GL.Alt (GL.NodePat n' nms) <$> toGrin b
+
+
+qnameToG :: QName -> TCM String
+qnameToG q = do
+  modNm <- topLevelModuleName (qnameModule q)
+
+  let locName = intercalate "_" $ map show $ either id id $ unqualifyQ modNm q
+      modParts = intercalate "." $ map show $ mnameToList modNm
+      identName = locName ++ "_" ++ show idnum
+
+  return $ modParts ++ "." ++ identName
+  where
+    idnum = let (NameId x _) = nameId $ qnameName q in x
+
+-- | Returns the names inside a QName, with the module prefix stripped away.
+-- If the name is not module-qualified, returns the full name as left. (TODO investigate when this happens)
+unqualifyQ :: ModuleName -> QName -> Either [AT.Name] [AT.Name]
+unqualifyQ modNm qnm =
+  case stripPrefix modNs qnms of
+    -- not sure when the name doesn't have a module prefix... just force generation of a name for the time being
+    Nothing -> Left qnms
+    Just nm -> Right nm
+  where
+    modNs = mnameToList modNm
+    qnms = qnameToList qnm
+
+
+grinPostModule :: () -> () -> IsMain -> ModuleName -> [(String, GL.Exp)] -> TCM ()
+grinPostModule _ _ _ _ _ = return ()