Configure unit tests (#3)

* ignore generated *.agdai files

* export Backend from Main

* move Main from src => app

* change cabal config add library and test-suite

* fix warnings in Backend

* test if backend is enabled

* add tests to CI

* update README with info how to run tests

* changelog for 0.1.0.2

* add missing newline in Main.hs

.github/workflows/haskell.yml

@@ -49,5 +49,8 @@ jobs:
       - name: Build
         run: cabal build all
 
+      - name: Run tests
+        run: cabal test all
+
       - name: Run tests
         run: cabal run -- agda2rust ./test/Hello.agda

.gitignore

@@ -2,3 +2,4 @@ _build
 dist
 dist-newstyle
 *~
+**/*.agdai

CHANGELOG.md

@@ -11,3 +11,8 @@
 * change upper bound for base to 4.20 to fix CI
 * add CHANGELOG.md
 * document how to compile example
+
+## 0.1.0.2 -- 2023-12-14
+* reorganise to library and executable and tests
+* test if backend is enabled using HSpec
+* cleanup warnings

README.md

@@ -24,3 +24,8 @@ cabal run -- agda2rust --help
 cabal run -- agda2rust ./test/Hello.agda
 cabal run -- agda2rust ./test/Test.agda
 ```
+* Run tests
+
+```sh
+cabal test all
+```

agda2rust.cabal

@@ -1,6 +1,12 @@
-cabal-version:      2.2
+cabal-version:     3.8
+-- Further docs  http://haskell.org/cabal/users-guide/
 name:               agda2rust
-version:            0.1.0.1
+-- See the Haskell package versioning policy (PVP) for standards
+-- https://pvp.haskell.org
+-- PVP summary:     +-+------- breaking API changes
+--                  | | +----- non-breaking API additions
+--                  | | | +--- code changes with no API change
+version:            0.1.0.2
 description:        Allows to export Rust source files from formal specification in Agda
 license:            MIT
 license-file:       LICENSE
@@ -16,12 +22,37 @@ source-repository head
   type:     git
   location: https://github.com/lemastero/agda2rust.git
 
-executable agda2rust
+common warnings
+  ghc-options: -Wall
+
+library
   hs-source-dirs:      src
-  main-is:             Main.hs
-  other-modules:       Paths_agda2rust
+  exposed-modules:     Agda.Compiler.Rust.Backend Paths_agda2rust
   autogen-modules:     Paths_agda2rust
   build-depends:       base >= 4.10 && < 4.20,
                        Agda >= 2.6.4 && < 2.6.5,
-                       deepseq >= 1.4.4 && < 1.6 
+                       deepseq >= 1.4.4 && < 1.6
   default-language:    Haskell2010
+  import:              warnings
+
+executable agda2rust
+  hs-source-dirs:   app
+  main-is:          Main.hs
+  other-modules:    Paths_agda2rust
+  autogen-modules:  Paths_agda2rust
+  build-depends:    base >= 4.10 && < 4.20,
+                    Agda >= 2.6.4 && < 2.6.5,
+                    agda2rust
+  default-language: Haskell2010
+  import:           warnings
+
+test-suite agda2rust-test
+  import:           warnings
+  default-language: Haskell2010
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   test
+  main-is:          RustBackendTest.hs
+  build-depends:    base >=4.10 && < 4.20,
+                    Agda >= 2.6.4 && < 2.6.5,
+                    HUnit >= 1.6.2.0,
+                    agda2rust

app/Main.hs

@@ -0,0 +1,6 @@
+module Main where
+
+import Agda.Compiler.Rust.Backend ( runRustBackend )
+
+main :: IO ()
+main = runRustBackend

src/Main.hs → src/Agda/Compiler/Rust/Backend.hs

@@ -1,5 +1,8 @@
 {-# LANGUAGE LambdaCase, RecordWildCards #-}
-module Main where
+module Agda.Compiler.Rust.Backend (
+  runRustBackend,
+  backend,
+  defaultOptions ) where
 
 import Data.Maybe ( fromMaybe )
 import Control.Monad ( unless )
@@ -25,7 +28,8 @@ import Agda.TypeChecking.Monad
 
 import Agda.Main ( runAgda )
 
-main = runAgda [Backend backend]
+runRustBackend :: IO ()
+runRustBackend = runAgda [Backend backend]
 
 data Options = Options { optOutDir :: Maybe FilePath }
 
@@ -51,24 +55,24 @@ backend = Backend'
       [ Option ['o'] ["out-dir"] (ReqArg outdirOpt "DIR")
         "Write output files to DIR. (default: project root)"
       ]
-  , isEnabled             = \ _ -> True
+  , isEnabled             = const True
   , preCompile            = return
   , postCompile           = \ _ _ _ -> return ()
   , preModule             = moduleSetup
   , postModule            = writeModule
   , compileDef            = compile
   , scopeCheckingSuffices = False
-  , mayEraseType          = \ _ -> return True
+  , mayEraseType          = const $ return True
   }
 
 moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath
             -> TCM (Recompile ModuleEnv ModuleRes)
-moduleSetup _ _ m _ = do
+moduleSetup _ _ _ _ = do
   setScope . iInsideScope =<< curIF
   return $ Recompile ()
 
 compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
-compile opts tlm _ Defn{..}
+compile _ _ _ Defn{..}
   = withCurrentModule (qnameModule defName)
   $ getUniqueCompilerPragma "AGDA2RUST" defName >>= \case
       Nothing -> return []

test/RustBackendTest.hs

@@ -0,0 +1,22 @@
+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.Backend ( isEnabled )
+
+testIsEnabled :: Test
+testIsEnabled = TestCase
+  (assertEqual "isEnabled" (isEnabled backend defaultOptions) True)
+
+tests :: Test
+tests = TestList [TestLabel "rustBackend" testIsEnabled]
+
+main :: IO ()
+main = do
+    result <- runTestTT tests
+    if failures result > 0 then exitFailure else exitSuccess