Compile one argument identity function (#10)

* 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

* use bracket, rename handleX to compileX - fix unit tests

* use bracket, rename handleX to compileX - fix unit tests 2

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

* add typeSeparator and argList for pretty printing

* compile singe argument function - argument name, its argument, function result type and single variable result body

* compile singe argument function - add return

* compile singe argument function - update Hello example

* compile singe argument function - add comments for further improvements

* proper function return type; rename to be more in-line with Rust naming style

* fix function return types (broke during rebase)

* change to lowercase names

* remove empty lines

* fix use module name instead of first directory

* RustExpr to separate pretty printing from traverse Agda internals (#18)

* add RustExpr to separate pretty printing and creating expression from Agda internals

* rename after refactor to RustExpr

* rename after refactor to RustExpr - fix

* swap unless to when

* Revert "RustExpr to separate pretty printing from traverse Agda internals (#18)" (#19)

This reverts commit 2f56f9a.

.github/workflows/haskell.yml

@@ -55,11 +55,11 @@ jobs:
       - name: Compile Hello.agda to Rust
         run: cabal run -- agda2rust ./test/hello.agda
 
-      - name: Install Rust latest nightly
+      - name: Install Rust
         uses: actions-rs/toolchain@v1
         with:
             profile: minimal
             toolchain: stable
 
-      - name: Compile Hello
-        run: rustc --crate-type=lib test/Hello.rs
+      - name: Compile using Rust compiler output files
+        run: rustc --crate-type=lib test/hello.rs

README.md

@@ -5,15 +5,15 @@
 ```sh
 cabal run -- agda2rust --help
 
-cabal run -- agda2rust test/Hello.agda
-cabal run -- agda2rust test/Test.agda
+cabal run -- agda2rust test/hello.agda
+cabal run -- agda2rust test/test.agda
 ```
 
 * Testing compiled Rust code
 
 ```sh
-rustc --crate-type=lib test/Hello.rs
-rustc --crate-type=lib test/Test.rs
+rustc --crate-type=lib test/hello.rs
+rustc --crate-type=lib test/test.rs
 ```
 
 # Working with source code

src/Agda/Compiler/Rust/PrettyPrintingUtils.hs

@@ -1,13 +1,20 @@
 module Agda.Compiler.Rust.PrettyPrintingUtils (
+  argList,
   bracket,
-  indent,
+  combineLines,
+  defsSeparator,
   exprSeparator,
-  defsSeparator
+  funReturnTypeSeparator,
+  indent,
+  typeSeparator
 ) where
 
 bracket :: String -> String
 bracket str = "{\n" <> str <> "\n}"
 
+argList :: String -> String
+argList str = "(" <> str <> ")"
+
 indent :: String
 indent = "  "
 
@@ -16,3 +23,12 @@ 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/ToRustCompiler.hs

@@ -9,19 +9,25 @@ 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.Syntax.Common ( Arg(..), ArgName, Named(..), moduleNameParts )
+import Agda.Syntax.Internal (
+  Clause(..), DeBruijnPattern, DBPatVar(..), Dom(..), unDom, PatternInfo(..), Pattern'(..),
+  qnameName, qnameModule, Telescope, Tele(..), Term(..), Type, Type''(..) )
+import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName )
 import Agda.TypeChecking.Monad.Base ( Definition(..) )
 import Agda.TypeChecking.Monad
-import Agda.TypeChecking.CompiledClause ( CompiledClauses )
+import Agda.TypeChecking.CompiledClause ( CompiledClauses(..), CompiledClauses'(..) )
 
 import Agda.Compiler.Rust.CommonTypes ( Options, CompiledDef, ModuleEnv )
 import Agda.Compiler.Rust.PrettyPrintingUtils (
+  argList,
   bracket,
-  indent,
+  combineLines,
+  defsSeparator,
   exprSeparator,
-  defsSeparator )
+  funReturnTypeSeparator,
+  indent,
+  typeSeparator )
 
 compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
 compile _ _ _ Defn{..}
@@ -41,7 +47,7 @@ compileDefn defName theDef =
     Function{funCompiled = funDef, funClauses = fc} ->
       compileFunction defName funDef fc
     _ ->
-      "UNSUPPORTED " <> showName defName <> " = " <> prettyShow theDef
+      "Unsupported compileDefn" <> showName defName <> " = " <> prettyShow theDef
 
 compileDataType :: QName -> [QName] -> CompiledDef
 compileDataType defName fields = "enum" <> exprSeparator
@@ -58,35 +64,97 @@ compileFunction :: QName
 compileFunction defName funDef fc = 
   "pub fn" <> exprSeparator
     <> showName defName
-    <> "("
-    -- TODO handle multiple function clauses
-    <> compileFunctionArgument fc
-    <> ")" <> exprSeparator <>
-    bracket (
+    <> 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 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] = prettyShow fc
+compileFunctionArgument [fc] = fromDeBruijnPattern (namedThing (unArg (head (namedClausePats fc))))
 compileFunctionArgument xs = error "unsupported compileFunctionArgument" ++ (show xs)
 
+compileFunctionArgType :: [Clause] -> CompiledDef
+compileFunctionArgType [ Clause{clauseTel = ct} ] = fromTelescope ct
+compileFunctionArgType xs = error "unsupported compileFunctionArgType" ++ (show xs)
+
+fromTelescope :: Telescope -> CompiledDef
+fromTelescope = \case
+  ExtendTel a _ -> fromDom a
+  other -> error ("unhandled fromType" ++ show other)
+
+fromDom :: Dom Type -> CompiledDef
+fromDom x = fromType (unDom x)
+
+compileFunctionResultType :: [Clause] -> CompiledDef
+compileFunctionResultType [Clause{clauseType = ct}] = fromMaybeType ct
+compileFunctionResultType other = error ("unhandled compileFunctionResultType" ++ show other)
+
+fromMaybeType :: Maybe (Arg Type) -> CompiledDef
+fromMaybeType (Just argType) = fromArgType argType
+fromMaybeType other = error ("unhandled fromMaybeType" ++ show other)
+
+fromArgType :: Arg Type -> CompiledDef
+fromArgType arg = fromType (unArg arg)
+
+fromType :: Type -> CompiledDef
+fromType = \case
+  a@(El _ ue) -> fromTerm ue
+  other -> error ("unhandled fromType" ++ show other)
+
+fromTerm :: Term -> CompiledDef
+fromTerm = \case
+  Def qname el -> fromQName qname
+  other -> error ("unhandled fromTerm" ++ show other)
+
+fromQName :: QName -> CompiledDef
+fromQName x = prettyShow (qnameName x)
+
+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 -> CompiledDef
-compileFunctionBody funDef = prettyShow funDef
+compileFunctionBody (Just funDef) = "return" <> exprSeparator <> fromCompiledClauses funDef
+compileFunctionBody funDef = error ("unhandled compileFunctionBody " ++ show funDef)
+
+fromCompiledClauses :: CompiledClauses -> CompiledDef
+fromCompiledClauses = \case
+  (Done (x:xs) term) -> fromArgName x
+  other               -> error ("unhandled fromCompiledClauses " ++ show other)
+
+fromArgName :: Arg ArgName -> CompiledDef
+fromArgName = unArg
 
 showName :: QName -> CompiledDef
 showName = prettyShow . qnameName
 
 compileModule :: TopLevelModuleName -> [CompiledDef] -> String
 compileModule mName cdefs =
   moduleHeader (moduleName mName)
-  <> bracket (unlines (map prettyShow cdefs))
+  <> bracket (combineLines (map prettyShow cdefs))
   <> defsSeparator
 
 moduleName :: TopLevelModuleName -> String
-moduleName n = prettyShow (Nel.head (moduleNameParts n))
+moduleName n = prettyShow (Nel.last (moduleNameParts n))
 
 moduleHeader :: String -> String
 moduleHeader mName = "mod" <> exprSeparator <> mName <> exprSeparator

test/hello.agda

@@ -1,11 +1,52 @@
 module test.hello where
 
 -- simple record type
-data Rgb : Set where
-  Red Green Blue : Rgb
-{-# COMPILE AGDA2RUST Rgb #-}
+data TheRgb : Set where
+  Red Green Blue : TheRgb
+{-# COMPILE AGDA2RUST TheRgb #-}
 
 -- simple function
--- idRgb : Rgb → Rgb
--- idRgb x = x
--- {-# COMPILE AGDA2RUST idRgb #-}
+idRgb : TheRgb → TheRgb
+idRgb rgbArg = rgbArg
+{-# COMPILE AGDA2RUST idRgb #-}
+
+data TheWeekDay : Set where
+  Monday Tuesday Wednesday Thursday Friday Saturday Sunday : TheWeekDay
+{-# COMPILE AGDA2RUST TheWeekDay #-}
+
+-- asFriday : TheRgb → TheWeekDay
+-- asFriday rgbArg = Friday -- TODO compile body
+-- {-# COMPILE AGDA2RUST asFriday #-}
+
+-- TODO multiple clauses
+-- day-color : TheWeekDay → TheRgb
+-- day-color Saturday = green
+-- day-color Sunday   = blue
+-- day-color _        = red
+-- {-# COMPILE AGDA2RUST day-color #-}
+
+-- TODO multiple arguments
+-- ≡Days? : TheWeekDay → TheWeekDay → TheRgb
+-- ≡Days? Saturday Saturday = green
+-- ≡Days? Sunday Sunday = blue
+-- ≡Days? _ _ = red
+-- {-# COMPILE AGDA2RUST ≡Days? #-}
+
+-- TODO polymorphic types
+
+-- TODO Data.Bool
+-- TODO if expressions, and, or
+
+-- TODO Data.Nat
+-- TODO arithmetic expressions
+
+-- TODO Lists
+
+-- TODO Data.String
+-- TODO borrow types
+
+-- TODO Data.Product
+
+-- TODO Data.Sum
+
+-- recursive functions

test/hello.rs

@@ -0,0 +1,13 @@
+mod hello {
+enum TheRgb {
+  Red, Green, Blue
+}
+pub fn idRgb(rgbArg: TheRgb) -> TheRgb {
+  return rgbArg
+}
+
+enum TheWeekDay {
+  Monday, Tuesday, Wednesday, Thursday, Friday, Saturday, Sunday
+}
+
+}