Fix gen files (#21)

* fix broken file generation

* delete example file on CI

* update hello.agda

.github/workflows/haskell.yml

@@ -51,6 +51,9 @@ jobs:
 
       - name: Run tests
         run: cabal test all
+
+      - name: Remove hello.rs
+        run: rm -rf test/hello.rs
 
       - name: Compile Hello.agda to Rust
         run: cabal run -- agda2rust ./test/hello.agda
@@ -61,5 +64,5 @@ jobs:
             profile: minimal
             toolchain: stable
 
-      - name: Compile using Rust compiler output files
+      - name: Compile hello.rs using Rust compiler
         run: rustc --crate-type=lib test/hello.rs

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 )
@@ -24,6 +24,7 @@ import Agda.TypeChecking.Monad (
 
 import Agda.Compiler.Rust.CommonTypes ( Options(..), CompiledDef, ModuleEnv )
 import Agda.Compiler.Rust.AgdaToRustExpr ( compile, compileModule )
+import Agda.Compiler.Rust.RustExpr ( unHandled )
 import Agda.Compiler.Rust.PrettyPrintingUtils ( prettyPrintRustExpr )
 
 runRustBackend :: IO ()
@@ -80,7 +81,7 @@ writeModule :: Options
 writeModule opts _ _ mName cdefs = do
   outDir <- compileDir
   compileLog $ "compiling " <> fileName
-  when (null cdefs) $ liftIO
+  unless (all unHandled cdefs) $ liftIO
     $ writeFile (outFile outDir)
     $ prettyPrintRustExpr (compileModule mName cdefs)
   where

src/Agda/Compiler/Rust/PrettyPrintingUtils.hs

@@ -11,8 +11,9 @@ prettyPrintRustExpr def = case def of
       <> name
       <> exprSeparator
       <> bracket (
-        indent -- TODO this to siplistic indentation
+        indent -- TODO this is too simplistic indentation
         <> concat (intersperse ", " fields))
+      <> defsSeparator
   (TeFun fName (RustElem aName aType) resType fBody) ->
       "pub fn" <> exprSeparator
         <> fName
@@ -22,15 +23,17 @@ prettyPrintRustExpr def = case def of
           <> aType )
         <> exprSeparator <> funReturnTypeSeparator <> exprSeparator <> resType
         <> exprSeparator <> bracket (
-        -- TODO proper indentation for every line of function body
-        -- including nested expressions
-        indent
-        <> (prettyPrintFunctionBody fBody))
+        indent <> (prettyPrintFunctionBody fBody))
         <> defsSeparator
   (TeMod mName defs) ->
     moduleHeader mName
-    <> bracket (combineLines (map prettyPrintRustExpr defs))
-    <> defsSeparator
+    <> bracket (
+      defsSeparator -- empty line before first definition in module
+      <> combineLines (map prettyPrintRustExpr defs))
+    <> defsSeparator 
+  (Unhandled name payload) -> ""
+  -- XXX at the end there should be no Unhandled expression
+  -- other -> "unsupported prettyPrintRustExpr " ++ (show other)
 
 bracket :: String -> String
 bracket str = "{\n" <> str <> "\n}"

src/Agda/Compiler/Rust/RustExpr.hs

@@ -3,7 +3,8 @@ module Agda.Compiler.Rust.RustExpr (
   RustType,
   RustExpr(..),
   RustElem(..),
-  FunBody
+  FunBody,
+  unHandled
   ) where
 
 type RustName = String
@@ -19,3 +20,7 @@ data RustExpr
   | TeFun RustName RustElem RustType FunBody
   | Unhandled RustName String
   deriving ( Show )
+
+unHandled :: RustExpr -> Bool
+unHandled (Unhandled _ _) = True
+unHandled _               = False

test/hello.agda

@@ -1,22 +1,39 @@
 module test.hello where
 
--- simple record type
-data TheRgb : Set where
-  Red Green Blue : TheRgb
-{-# COMPILE AGDA2RUST TheRgb #-}
+-- simple sum type
+data Rgb : Set where
+  Red : Rgb
+  Green : Rgb
+  Blue : Rgb
+{-# COMPILE AGDA2RUST Rgb #-}
 
--- simple function
-idRgb : TheRgb → TheRgb
-idRgb rgbArg = rgbArg
-{-# COMPILE AGDA2RUST idRgb #-}
+data WeekDay : Set where
+  Monday Tuesday Wednesday Thursday Friday Saturday Sunday : WeekDay
+{-# COMPILE AGDA2RUST WeekDay #-}
 
-data TheWeekDay : Set where
-  Monday Tuesday Wednesday Thursday Friday Saturday Sunday : TheWeekDay
-{-# COMPILE AGDA2RUST TheWeekDay #-}
+-- identity function on concrete types
+id_rgb : Rgb → Rgb
+id_rgb x = x
+{-# COMPILE AGDA2RUST id_rgb #-}
 
--- asFriday : TheRgb → TheWeekDay
--- asFriday rgbArg = Friday -- TODO compile body
--- {-# COMPILE AGDA2RUST asFriday #-}
+-- product types
+
+-- record ThePair : Set where
+--   field
+--     pairFst : Rgb
+--     pairSnd : WeekDay
+-- {-# COMPILE AGDA2RUST ThePair #-}
+
+-- record Foo (A : Set) : Set where
+--   field
+--     foo : Pair A A
+
+-- TODO Data.Product as Rust tuple
+
+-- TODO function returning constant result
+-- as-friday : TheRgb → TheWeekDay
+-- as-friday rgbArg = Friday
+-- {-# COMPILE AGDA2RUST as-friday #-}
 
 -- TODO multiple clauses
 -- day-color : TheWeekDay → TheRgb
@@ -32,6 +49,8 @@ data TheWeekDay : Set where
 -- ≡Days? _ _ = red
 -- {-# COMPILE AGDA2RUST ≡Days? #-}
 
+-- TODO pattern matching
+
 -- TODO polymorphic types
 
 -- TODO Data.Bool
@@ -49,4 +68,4 @@ data TheWeekDay : Set where
 
 -- TODO Data.Sum
 
--- recursive functions
+-- TODO recursive functions

test/hello.rs

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