Handle Rust enums and modules (#4)

* test existing code creating moduleHeader

* module header is proper Rust comment

* fix non-compiling Test.agda example - add test.Test module

* handle module name and brackets

* handle function name, brackets around body, raw body

* handle data type definition as enum - name, brackets and raw clauses

* update examples Hello and Test with new handling of functions and data types

* simplify Hello.agda enum + function on enum

* extract functions for hande functions, handle data type, handle module

* handle enums

* use bracket, rename handleX to compileX

* extract PrettyPrintingUtils and ToRustCompiler; common types between ToRustCompiler and Backed are in CommonTypes

* drop Test

* comment out function in Hello

* ignore Rust compile output, IntelliJ files and MacOS DS_Store

* move options to explicit variable

* ignore iml files

* get module name without namespace

* uppercase enums cases to have more idiomatic Rust output

* rename Hello.agda to hello.agda

* Update haskell.yml

.github/workflows/haskell.yml

@@ -53,4 +53,4 @@ jobs:
         run: cabal test all
 
       - name: Run tests
-        run: cabal run -- agda2rust ./test/Hello.agda
+        run: cabal run -- agda2rust ./test/hello.agda

.gitignore

@@ -2,4 +2,11 @@ _build
 dist
 dist-newstyle
 *~
+
 **/*.agdai
+
+**/*.rlib
+
+.idea/
+.DS_Store
+*.iml

agda2rust.cabal

@@ -27,7 +27,11 @@ common warnings
 
 library
   hs-source-dirs:      src
-  exposed-modules:     Agda.Compiler.Rust.Backend Paths_agda2rust
+  exposed-modules:     Agda.Compiler.Rust.Backend
+                       Agda.Compiler.Rust.CommonTypes
+                       Agda.Compiler.Rust.PrettyPrintingUtils
+                       Agda.Compiler.Rust.ToRustCompiler
+                       Paths_agda2rust
   autogen-modules:     Paths_agda2rust
   build-depends:       base >= 4.10 && < 4.20,
                        Agda >= 2.6.4 && < 2.6.5,

src/Agda/Compiler/Rust/Backend.hs

@@ -1,90 +1,94 @@
-{-# LANGUAGE LambdaCase, RecordWildCards #-}
 module Agda.Compiler.Rust.Backend (
   runRustBackend,
   backend,
   defaultOptions ) 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.Maybe ( fromMaybe )
 import Data.Version ( showVersion )
 import Paths_agda2rust ( version )
-
-import Agda.Syntax.Common.Pretty ( prettyShow )
-import Agda.Syntax.Internal ( qnameName, qnameModule )
-import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName, moduleNameToFileName )
+import System.Console.GetOpt ( OptDescr(Option), ArgDescr(ReqArg) )
 
 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.Interaction.Options ( Flag )
 import Agda.Main ( runAgda )
+import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName, moduleNameToFileName )
+import Agda.TypeChecking.Monad (
+  TCM,
+  TCMT,
+  iInsideScope,
+  setScope )
+
+import Agda.Compiler.Rust.CommonTypes ( Options(..), CompiledDef, ModuleEnv )
+import Agda.Compiler.Rust.ToRustCompiler ( compile, compileModule )
 
 runRustBackend :: IO ()
 runRustBackend = runAgda [Backend backend]
 
-data Options = Options { optOutDir :: Maybe FilePath }
-
 instance NFData Options where
   rnf _ = ()
 
+cmdLineFlags :: [OptDescr (Flag Options)]
+cmdLineFlags = [
+  Option ['o'] ["out-dir"] (ReqArg outdirOpt "DIR")
+         "Write output files to DIR. (default: project root)"
+  ]
+
 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           = "agda2rust"
   , backendVersion        = Just (showVersion version)
   , options               = defaultOptions
-  , commandLineFlags      =
-      [ Option ['o'] ["out-dir"] (ReqArg outdirOpt "DIR")
-        "Write output files to DIR. (default: project root)"
-      ]
+  , commandLineFlags      = cmdLineFlags
   , isEnabled             = const True
   , preCompile            = return
-  , postCompile           = \ _ _ _ -> return ()
+  , postCompile           = const $ const $ const $ return ()
   , preModule             = moduleSetup
   , postModule            = writeModule
   , compileDef            = compile
   , scopeCheckingSuffices = False
   , mayEraseType          = const $ return True
   }
 
-moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath
-            -> TCM (Recompile ModuleEnv ModuleRes)
+moduleSetup :: Options
+  -> IsMain
+  -> TopLevelModuleName
+  -> Maybe FilePath
+  -> TCM (Recompile ModuleEnv ModuleRes)
 moduleSetup _ _ _ _ = do
   setScope . iInsideScope =<< curIF
   return $ Recompile ()
 
-compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
-compile _ _ _ Defn{..}
-  = withCurrentModule (qnameModule defName)
-  $ getUniqueCompilerPragma "AGDA2RUST" 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
+writeModule :: Options
+  -> ModuleEnv
+  -> IsMain
+  -> TopLevelModuleName
+  -> [CompiledDef]
+  -> TCM ModuleRes
+writeModule opts _ _ mName cdefs = do
   outDir <- compileDir
-  liftIO $ putStrLn (moduleNameToFileName m "rs")
-  let outFile = fromMaybe outDir (optOutDir opts) <> "/" <> moduleNameToFileName m "rs"
+  compileLog $ "compiling " <> fileName
   unless (all null cdefs) $ liftIO
-    $ writeFile outFile
-    $ "*** module " <> prettyShow m <> " ***\n" <> unlines cdefs
+    $ writeFile (outFile outDir)
+    $ compileModule mName cdefs
+  where
+    fileName = rustFileName mName
+    dirName outDir = fromMaybe outDir (optOutDir opts)
+    outFile outDir = (dirName outDir) <> "/" <> fileName
+
+rustFileName :: TopLevelModuleName -> FilePath
+rustFileName mName = moduleNameToFileName mName "rs" 
+
+compileLog :: String -> TCMT IO ()
+compileLog msg = liftIO $ putStrLn msg

src/Agda/Compiler/Rust/CommonTypes.hs

@@ -0,0 +1,10 @@
+module Agda.Compiler.Rust.CommonTypes (
+  Options(..),
+  CompiledDef,
+  ModuleEnv ) where
+
+data Options = Options { optOutDir :: Maybe FilePath }
+
+type CompiledDef = String
+
+type ModuleEnv = ()

src/Agda/Compiler/Rust/PrettyPrintingUtils.hs

@@ -0,0 +1,18 @@
+module Agda.Compiler.Rust.PrettyPrintingUtils (
+  bracket,
+  indent,
+  exprSeparator,
+  defsSeparator
+) where
+
+bracket :: String -> String
+bracket str = "{\n" <> str <> "\n}"
+
+indent :: String
+indent = "  "
+
+exprSeparator :: String
+exprSeparator = " "
+
+defsSeparator :: String
+defsSeparator = "\n"

src/Agda/Compiler/Rust/ToRustCompiler.hs

@@ -0,0 +1,92 @@
+{-# LANGUAGE LambdaCase, RecordWildCards #-}
+
+module Agda.Compiler.Rust.ToRustCompiler ( compile, compileModule, moduleHeader ) where
+
+import Control.Monad.IO.Class ( MonadIO(liftIO) )
+import Data.List ( intersperse )
+import qualified Data.List.NonEmpty as Nel
+
+import Agda.Compiler.Backend ( IsMain )
+import Agda.Syntax.Abstract.Name ( QName )
+import Agda.Syntax.Common.Pretty ( prettyShow )
+import Agda.Syntax.Internal ( Clause )
+import Agda.Syntax.Internal ( qnameName, qnameModule )
+import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName, moduleNameParts )
+import Agda.TypeChecking.Monad.Base ( Definition(..) )
+import Agda.TypeChecking.Monad
+import Agda.TypeChecking.CompiledClause ( CompiledClauses )
+
+import Agda.Compiler.Rust.CommonTypes ( Options, CompiledDef, ModuleEnv )
+import Agda.Compiler.Rust.PrettyPrintingUtils (
+  bracket,
+  indent,
+  exprSeparator,
+  defsSeparator )
+
+compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
+compile _ _ _ Defn{..}
+  = withCurrentModule (qnameModule defName)
+  $ getUniqueCompilerPragma "AGDA2RUST" defName >>= \case
+      Nothing -> return []
+      Just (CompilerPragma _ _) ->
+        return $ compileDefn defName theDef
+
+compileDefn :: QName
+  -> Defn
+  -> CompiledDef
+compileDefn defName theDef =
+  case theDef of 
+    Datatype{dataCons = fields} ->
+      compileDataType defName fields
+    Function{funCompiled = funDef, funClauses = fc} ->
+      compileFunction defName funDef fc
+    _ ->
+      "UNSUPPORTED " <> showName defName <> " = " <> prettyShow theDef
+
+compileDataType :: QName -> [QName] -> CompiledDef
+compileDataType defName fields = "enum" <> exprSeparator
+  <> showName defName
+  <> exprSeparator
+  <> bracket (
+    indent
+    <> concat (intersperse ", " (map showName fields)))
+
+compileFunction :: QName
+  -> Maybe CompiledClauses
+  -> [Clause]
+  -> CompiledDef
+compileFunction defName funDef fc = 
+  "pub fn" <> exprSeparator
+    <> showName defName
+    <> "("
+    -- TODO handle multiple function clauses
+    <> compileFunctionArgument fc
+    <> ")" <> exprSeparator <>
+    bracket (
+    -- TODO proper indentation for every line of function body
+    indent
+    <> compileFunctionBody funDef)
+    <> defsSeparator
+
+compileFunctionArgument :: [Clause] -> CompiledDef
+compileFunctionArgument [] = ""
+compileFunctionArgument [fc] = prettyShow fc
+compileFunctionArgument xs = error "unsupported compileFunctionArgument" ++ (show xs)
+
+compileFunctionBody :: Maybe CompiledClauses -> CompiledDef
+compileFunctionBody funDef = prettyShow funDef
+
+showName :: QName -> CompiledDef
+showName = prettyShow . qnameName
+
+compileModule :: TopLevelModuleName -> [CompiledDef] -> String
+compileModule mName cdefs =
+  moduleHeader (moduleName mName)
+  <> bracket (unlines (map prettyShow cdefs))
+  <> defsSeparator
+
+moduleName :: TopLevelModuleName -> String
+moduleName n = prettyShow (Nel.head (moduleNameParts n))
+
+moduleHeader :: String -> String
+moduleHeader mName = "mod" <> exprSeparator <> mName <> exprSeparator

test/Hello.rs

@@ -1,7 +1,9 @@
-mod hello {
-
+mod test {
 enum Rgb {
   Red, Green, Blue
 }
 
+
+
+
 }

test/RustBackendTest.hs

@@ -1,20 +1,29 @@
 module Main (main) where
 
-import Agda.Compiler.Rust.Backend ( backend, defaultOptions )
 import Test.HUnit (
   Test(..)
   , assertEqual
   , failures
   , runTestTT)
 import System.Exit ( exitFailure , exitSuccess )
+import Agda.Compiler.Rust.Backend ( backend, defaultOptions )
+import Agda.Compiler.Rust.ToRustCompiler ( moduleHeader )
+
 import Agda.Compiler.Backend ( isEnabled )
 
 testIsEnabled :: Test
 testIsEnabled = TestCase
   (assertEqual "isEnabled" (isEnabled backend defaultOptions) True)
+
+testModuleHeader :: Test
+testModuleHeader = TestCase
+  (assertEqual "moduleHeader" (moduleHeader "foo") "mod foo ")
 
 tests :: Test
-tests = TestList [TestLabel "rustBackend" testIsEnabled]
+tests = TestList [
+    TestLabel "rust Backend is enabled" testIsEnabled,
+    TestLabel "produces Rust module header" testModuleHeader
+  ]
 
 main :: IO ()
 main = do

test/Test.agda

@@ -1,4 +1,4 @@
-module _ where
+module test.Test where
 
 open import Agda.Builtin.Nat using (Nat; _+_; _*_)
 open import Agda.Builtin.List using (List; []; _∷_)

test/hello.agda

@@ -0,0 +1,11 @@
+module test.hello where
+
+-- simple record type
+data Rgb : Set where
+  Red Green Blue : Rgb
+{-# COMPILE AGDA2RUST Rgb #-}
+
+-- simple function
+-- idRgb : Rgb → Rgb
+-- idRgb x = x
+-- {-# COMPILE AGDA2RUST idRgb #-}