Revert "RustExpr to separate pretty printing from traverse Agda inter…

…nals (#18)"

This reverts commit 2f56f9a.

agda2rust.cabal

@@ -28,10 +28,9 @@ common warnings
 library
   hs-source-dirs:      src
   exposed-modules:     Agda.Compiler.Rust.Backend
-                       Agda.Compiler.Rust.RustExpr
                        Agda.Compiler.Rust.CommonTypes
-                       Agda.Compiler.Rust.PrettyPrintRustExpr
-                       Agda.Compiler.Rust.AgdaToRustExpr
+                       Agda.Compiler.Rust.PrettyPrintingUtils
+                       Agda.Compiler.Rust.ToRustCompiler
                        Paths_agda2rust
   autogen-modules:     Paths_agda2rust
   build-depends:       base >= 4.10 && < 4.20,

src/Agda/Compiler/Rust/Backend.hs

@@ -3,7 +3,7 @@ module Agda.Compiler.Rust.Backend (
   backend,
   defaultOptions ) where
 
-import Control.Monad ( when )
+import Control.Monad ( unless )
 import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import Control.DeepSeq ( NFData(..) )
 import Data.Maybe ( fromMaybe )
@@ -23,8 +23,7 @@ import Agda.TypeChecking.Monad (
   setScope )
 
 import Agda.Compiler.Rust.CommonTypes ( Options(..), CompiledDef, ModuleEnv )
-import Agda.Compiler.Rust.AgdaToRustExpr ( compile, compileModule )
-import Agda.Compiler.Rust.PrettyPrintRustExpr ( prettyPrintRustExpr )
+import Agda.Compiler.Rust.ToRustCompiler ( compile, compileModule )
 
 runRustBackend :: IO ()
 runRustBackend = runAgda [Backend backend]
@@ -80,9 +79,9 @@ writeModule :: Options
 writeModule opts _ _ mName cdefs = do
   outDir <- compileDir
   compileLog $ "compiling " <> fileName
-  when (null cdefs) $ liftIO
+  unless (all null cdefs) $ liftIO
     $ writeFile (outFile outDir)
-    $ prettyPrintRustExpr (compileModule mName cdefs)
+    $ compileModule mName cdefs
   where
     fileName = rustFileName mName
     dirName outDir = fromMaybe outDir (optOutDir opts)

src/Agda/Compiler/Rust/CommonTypes.hs

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

src/Agda/Compiler/Rust/PrettyPrintingUtils.hs

@@ -0,0 +1,34 @@
+module Agda.Compiler.Rust.PrettyPrintingUtils (
+  argList,
+  bracket,
+  combineLines,
+  defsSeparator,
+  exprSeparator,
+  funReturnTypeSeparator,
+  indent,
+  typeSeparator
+) where
+
+bracket :: String -> String
+bracket str = "{\n" <> str <> "\n}"
+
+argList :: String -> String
+argList str = "(" <> str <> ")"
+
+indent :: String
+indent = "  "
+
+exprSeparator :: String
+exprSeparator = " "
+
+defsSeparator :: String
+defsSeparator = "\n"
+
+typeSeparator :: String
+typeSeparator = ":"
+
+funReturnTypeSeparator :: String
+funReturnTypeSeparator = "->"
+
+combineLines :: [String] -> String
+combineLines xs = unlines (filter (not . null) xs)

src/Agda/Compiler/Rust/AgdaToRustExpr.hs → src/Agda/Compiler/Rust/ToRustCompiler.hs

@@ -1,8 +1,9 @@
 {-# LANGUAGE LambdaCase, RecordWildCards #-}
 
-module Agda.Compiler.Rust.AgdaToRustExpr ( compile, compileModule ) where
+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 )
@@ -18,109 +19,142 @@ import Agda.TypeChecking.Monad
 import Agda.TypeChecking.CompiledClause ( CompiledClauses(..), CompiledClauses'(..) )
 
 import Agda.Compiler.Rust.CommonTypes ( Options, CompiledDef, ModuleEnv )
-import Agda.Compiler.Rust.RustExpr ( RustExpr(..), RustName, RustType, RustElem(..), FunBody )
+import Agda.Compiler.Rust.PrettyPrintingUtils (
+  argList,
+  bracket,
+  combineLines,
+  defsSeparator,
+  exprSeparator,
+  funReturnTypeSeparator,
+  indent,
+  typeSeparator )
 
 compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
 compile _ _ _ Defn{..}
   = withCurrentModule (qnameModule defName)
   $ getUniqueCompilerPragma "AGDA2RUST" defName >>= \case
-      Nothing -> return $ Unhandled "compile" ""
-      Just (CompilerPragma _ _) -> 
+      Nothing -> return []
+      Just (CompilerPragma _ _) ->
         return $ compileDefn defName theDef
 
-compileDefn :: QName -> Defn -> CompiledDef
+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
     _ ->
-      Unhandled "compileDefn" (show defName ++ " = " ++ show theDef)
+      "Unsupported compileDefn" <> showName defName <> " = " <> prettyShow theDef
 
 compileDataType :: QName -> [QName] -> CompiledDef
-compileDataType defName fields = TeEnum (showName defName) (map showName fields)
+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 = TeFun
-  (showName defName)
-  (RustElem (compileFunctionArgument fc) (compileFunctionArgType fc))
-  (compileFunctionResultType fc)
-  (compileFunctionBody funDef)
+compileFunction defName funDef fc = 
+  "pub fn" <> exprSeparator
+    <> showName defName
+    <> argList (
+      -- TODO handle multiple function clauses and arguments
+      compileFunctionArgument fc
+      <> typeSeparator <> exprSeparator
+      <> compileFunctionArgType fc )
+    <> exprSeparator <> funReturnTypeSeparator <> exprSeparator <> compileFunctionResultType fc
+    <> exprSeparator <> bracket (
+    -- TODO proper indentation for every line of function body
+    -- including nested expressions
+    -- build intermediate AST and pretty printer for it
+    indent
+    <> compileFunctionBody funDef)
+    <> defsSeparator
 
 -- TODO this is hacky way to reach find first argument name, assuming function has 1 argument
 -- TODO proper way is to handle deBruijn indices
--- TODO see `data Clause` in https://hackage.haskell.org/package/Agda-2.6.4.1/docs/Agda-Syntax-Internal.html
-compileFunctionArgument :: [Clause] -> RustName
+-- TODO read docs for `data Clause` section in https://hackage.haskell.org/package/Agda-2.6.4.1/docs/Agda-Syntax-Internal.html
+-- TODO start from uncommenting line below and figure out the path to match indices with name and type
+-- compileFunctionArgument fc = show fc
+compileFunctionArgument :: [Clause] -> CompiledDef
 compileFunctionArgument [] = ""
 compileFunctionArgument [fc] = fromDeBruijnPattern (namedThing (unArg (head (namedClausePats fc))))
-compileFunctionArgument xs = error "unsupported compileFunctionArgument" ++ (show xs) -- show xs
+compileFunctionArgument xs = error "unsupported compileFunctionArgument" ++ (show xs)
 
-compileFunctionArgType :: [Clause] -> RustType
+compileFunctionArgType :: [Clause] -> CompiledDef
 compileFunctionArgType [ Clause{clauseTel = ct} ] = fromTelescope ct
 compileFunctionArgType xs = error "unsupported compileFunctionArgType" ++ (show xs)
 
-fromTelescope :: Telescope -> RustName
+fromTelescope :: Telescope -> CompiledDef
 fromTelescope = \case
   ExtendTel a _ -> fromDom a
   other -> error ("unhandled fromType" ++ show other)
 
-fromDom :: Dom Type -> RustName
+fromDom :: Dom Type -> CompiledDef
 fromDom x = fromType (unDom x)
 
-compileFunctionResultType :: [Clause] -> RustType
+compileFunctionResultType :: [Clause] -> CompiledDef
 compileFunctionResultType [Clause{clauseType = ct}] = fromMaybeType ct
 compileFunctionResultType other = error ("unhandled compileFunctionResultType" ++ show other)
 
-fromMaybeType :: Maybe (Arg Type) -> RustName
+fromMaybeType :: Maybe (Arg Type) -> CompiledDef
 fromMaybeType (Just argType) = fromArgType argType
 fromMaybeType other = error ("unhandled fromMaybeType" ++ show other)
 
-fromArgType :: Arg Type -> RustName
+fromArgType :: Arg Type -> CompiledDef
 fromArgType arg = fromType (unArg arg)
 
-fromType :: Type -> RustName
+fromType :: Type -> CompiledDef
 fromType = \case
   a@(El _ ue) -> fromTerm ue
   other -> error ("unhandled fromType" ++ show other)
 
-fromTerm :: Term -> RustName
+fromTerm :: Term -> CompiledDef
 fromTerm = \case
   Def qname el -> fromQName qname
   other -> error ("unhandled fromTerm" ++ show other)
 
-fromQName :: QName -> RustName
+fromQName :: QName -> CompiledDef
 fromQName x = prettyShow (qnameName x)
 
-fromDeBruijnPattern :: DeBruijnPattern -> RustName
+fromDeBruijnPattern :: DeBruijnPattern -> CompiledDef
 fromDeBruijnPattern = \case
     VarP a b -> (dbPatVarName b)
     a@(ConP x y z) -> show a
     other -> error ("unhandled fromDeBruijnPattern" ++ show other)
 
 -- TODO this is wrong for function other than identity
 -- see asFriday in Hello.agda vs Hello.rs
-compileFunctionBody :: Maybe CompiledClauses -> FunBody
-compileFunctionBody (Just funDef) = fromCompiledClauses funDef
+compileFunctionBody :: Maybe CompiledClauses -> CompiledDef
+compileFunctionBody (Just funDef) = "return" <> exprSeparator <> fromCompiledClauses funDef
 compileFunctionBody funDef = error ("unhandled compileFunctionBody " ++ show funDef)
 
-fromCompiledClauses :: CompiledClauses -> FunBody
+fromCompiledClauses :: CompiledClauses -> CompiledDef
 fromCompiledClauses = \case
   (Done (x:xs) term) -> fromArgName x
   other               -> error ("unhandled fromCompiledClauses " ++ show other)
 
-fromArgName :: Arg ArgName -> FunBody
+fromArgName :: Arg ArgName -> CompiledDef
 fromArgName = unArg
 
-showName :: QName -> RustName
+showName :: QName -> CompiledDef
 showName = prettyShow . qnameName
 
-compileModule :: TopLevelModuleName -> [CompiledDef] -> CompiledDef
+compileModule :: TopLevelModuleName -> [CompiledDef] -> String
 compileModule mName cdefs =
-  TeMod (moduleName mName) cdefs
+  moduleHeader (moduleName mName)
+  <> bracket (combineLines (map prettyShow cdefs))
+  <> defsSeparator
 
 moduleName :: TopLevelModuleName -> String
 moduleName n = prettyShow (Nel.last (moduleNameParts n))
+
+moduleHeader :: String -> String
+moduleHeader mName = "mod" <> exprSeparator <> mName <> exprSeparator

test/RustBackendTest.hs

@@ -7,7 +7,7 @@ import Test.HUnit (
   , runTestTT)
 import System.Exit ( exitFailure , exitSuccess )
 import Agda.Compiler.Rust.Backend ( backend, defaultOptions )
-import Agda.Compiler.Rust.PrettyPrintRustExpr ( moduleHeader )
+import Agda.Compiler.Rust.ToRustCompiler ( moduleHeader )
 
 import Agda.Compiler.Backend ( isEnabled )