agda2rust with CI (#1)

* AGDA2?? => AGDA2RUST

* agda2min => agda2rust

* file rename - agda2min.cabal => agda2rust.cabal

* file extension txt => rs

* add CI

* document how to compile example

* change upper bound for base to 4.20 to fix CI

* add CHANGELOG.md

.github/workflows/haskell.yml

@@ -0,0 +1,53 @@
+on: [push]
+name: build
+jobs:
+  runhaskell:
+    name: agda2rust
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checks-out repository
+        uses: actions/checkout@v4
+
+      - name: Set up GHC
+        uses: haskell-actions/setup@v2
+        id: setup
+        with:
+          ghc-version: '9.8.1'
+          cabal-version: '3.10.1.0'
+          cabal-update: true
+
+      - name: Configure the build
+        run: |
+          cabal configure --enable-tests --enable-benchmarks --disable-documentation
+          cabal build --dry-run
+        # The last step generates dist-newstyle/cache/plan.json for the cache key.
+
+      - name: Restore cached dependencies
+        uses: actions/cache/restore@v3
+        id: cache
+        env:
+          key: ${{ runner.os }}-ghc-${{ steps.setup.outputs.ghc-version }}-cabal-${{ steps.setup.outputs.cabal-version }}
+        with:
+          path: ${{ steps.setup.outputs.cabal-store }}
+          key: ${{ env.key }}-plan-${{ hashFiles('**/plan.json') }}
+          restore-keys: ${{ env.key }}-
+
+      - name: Install dependencies
+        # If we had an exact cache hit, the dependencies will be up to date.
+        if: ${{ steps.cache.outputs.cache-hit != 'true' }}
+        run: cabal build all --only-dependencies
+
+      # Cache dependencies already here, so that we do not have to rebuild them should the subsequent steps fail.
+      - name: Save cached dependencies
+        uses: actions/cache/save@v3
+        # If we had an exact cache hit, trying to save the cache would error because of key clash.
+        if: ${{ steps.cache.outputs.cache-hit != 'true' }}
+        with:
+          path: ${{ steps.setup.outputs.cabal-store }}
+          key: ${{ steps.cache.outputs.cache-primary-key }}
+
+      - name: Build
+        run: cabal build all
+
+      - name: Run tests
+        run: cabal run -- agda2rust ./test/Hello.agda

CHANGELOG.md

@@ -0,0 +1,13 @@
+# Revision history for agda2scala
+
+## 0.1.0.0 -- 2023-12-14
+
+* First version cloned from omelkonian/agda-minimal-backend
+
+## 0.1.0.1 -- 2023-12-14
+* add CI
+* rename agda2?? to agda2rust
+* add working example
+* change upper bound for base to 4.20 to fix CI
+* add CHANGELOG.md
+* document how to compile example

README.md

@@ -1,4 +1,26 @@
-# Minimal skeleton for developing a new Agda backend 
+# Agda backend for Rust 
 
-- The backend is defined in `src/Main.hs`.
-- The `test/` directory contains an example compilation of `Test.agda` to `Test.txt`.
+## Working with source code
+
+* Starting continuous compilation loop
+
+```sh
+ghcid
+```
+
+* Build
+
+```sh
+cabal build all
+```
+
+* Run
+
+The `test/` directory contains an example compilation of `Test.agda` to `Test.rs`
+and `Hello.agda` to `Hello.rs`:
+
+```sh
+cabal run -- agda2rust --help
+cabal run -- agda2rust ./test/Hello.agda
+cabal run -- agda2rust ./test/Test.agda
+```

agda2rust.cabal

@@ -0,0 +1,27 @@
+cabal-version:      2.2
+name:               agda2rust
+version:            0.1.0.1
+description:        Allows to export Rust source files from formal specification in Agda
+license:            MIT
+license-file:       LICENSE
+author:             lemastero
+maintainer:         [email protected]
+category:           Language, Compiler
+build-type:         Simple
+synopsis:           Compiling Agda code to Rust.
+
+extra-doc-files:    README.md, CHANGELOG.md
+
+source-repository head
+  type:     git
+  location: https://github.com/lemastero/agda2rust.git
+
+executable agda2rust
+  hs-source-dirs:      src
+  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,
+                       deepseq >= 1.4.4 && < 1.6 
+  default-language:    Haskell2010

src/Main.hs

@@ -9,7 +9,7 @@ import Control.DeepSeq ( NFData(..) )
 import System.Console.GetOpt ( OptDescr(Option), ArgDescr(ReqArg) )
 
 import Data.Version ( showVersion )
-import Paths_agda2min ( version )
+import Paths_agda2rust ( version )
 
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Internal ( qnameName, qnameModule )
@@ -44,7 +44,7 @@ type CompiledDef = String
 
 backend :: Backend' Options Options ModuleEnv ModuleRes CompiledDef
 backend = Backend'
-  { backendName           = "agda2??"
+  { backendName           = "agda2rust"
   , backendVersion        = Just (showVersion version)
   , options               = defaultOptions
   , commandLineFlags      =
@@ -70,7 +70,7 @@ moduleSetup _ _ m _ = do
 compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
 compile opts tlm _ Defn{..}
   = withCurrentModule (qnameModule defName)
-  $ getUniqueCompilerPragma "AGDA2??" defName >>= \case
+  $ getUniqueCompilerPragma "AGDA2RUST" defName >>= \case
       Nothing -> return []
       Just (CompilerPragma _ _) ->
         return $ prettyShow (qnameName defName) <> " = " <> prettyShow theDef
@@ -79,8 +79,8 @@ writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName -> [Compiled
             -> TCM ModuleRes
 writeModule opts _ _ m cdefs = do
   outDir <- compileDir
-  liftIO $ putStrLn (moduleNameToFileName m "txt")
-  let outFile = fromMaybe outDir (optOutDir opts) <> "/" <> moduleNameToFileName m "txt"
+  liftIO $ putStrLn (moduleNameToFileName m "rs")
+  let outFile = fromMaybe outDir (optOutDir opts) <> "/" <> moduleNameToFileName m "rs"
   unless (all null cdefs) $ liftIO
     $ writeFile outFile
     $ "*** module " <> prettyShow m <> " ***\n" <> unlines cdefs

test/Hello.agda

@@ -0,0 +1,12 @@
+module test.Hello where
+
+-- Type with two inhabitants
+data Bool : Set where
+  false true : Bool
+{-# COMPILE AGDA2RUST Bool #-}
+
+{- Logical connective not - negation -}
+not : Bool -> Bool
+not true  = false
+not false = true
+{-# COMPILE AGDA2RUST not #-}

test/Hello.rs

@@ -0,0 +1,45 @@
+*** module test.Hello ***
+Bool = Datatype {
+  dataPars       = 0
+  dataIxs        = 0
+  dataClause     = (nothing)
+  dataCons       =
+    [QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "test" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "test" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 13, posLine = 1, posCol = 13}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 2 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Hello" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Hello" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 13, posLine = 1, posCol = 13}, iEnd = Pn {srcFile = (), posPos = 18, posLine = 1, posCol = 18}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 4 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Bool" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Bool" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 60, posLine = 4, posCol = 6}, iEnd = Pn {srcFile = (), posPos = 64, posLine = 4, posCol = 10}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 6 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "false" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "false" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 79, posLine = 5, posCol = 3}, iEnd = Pn {srcFile = (), posPos = 84, posLine = 5, posCol = 8}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}},QName {qnameModule = MName {mnameToList = [Name {nameId = NameId 0 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "test" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "test" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 8, posLine = 1, posCol = 8}, iEnd = Pn {srcFile = (), posPos = 13, posLine = 1, posCol = 13}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 2 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Hello" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Hello" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 13, posLine = 1, posCol = 13}, iEnd = Pn {srcFile = (), posPos = 18, posLine = 1, posCol = 18}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False},Name {nameId = NameId 4 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Bool" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "Bool" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 60, posLine = 4, posCol = 6}, iEnd = Pn {srcFile = (), posPos = 64, posLine = 4, posCol = 10}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}]}, qnameName = Name {nameId = NameId 8 (ModuleNameHash 5806517176001440770), nameConcrete = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "true" :| []}, nameCanonical = Name {nameRange = NoRange, nameInScope = InScope, nameNameParts = Id "true" :| []}, nameBindingSite = Range (Just (RangeFile {rangeFilePath = AbsolutePath {textPath = "/Users/lemastero/work/agda2rust2/test/Hello.agda"}, rangeFileName = Just (TopLevelModuleName {moduleNameRange = NoRange, moduleNameId = ModuleNameHash 5806517176001440770, moduleNameParts = "test" :| ["Hello"]})})) (fromList [Interval {iStart = Pn {srcFile = (), posPos = 85, posLine = 5, posCol = 9}, iEnd = Pn {srcFile = (), posPos = 89, posLine = 5, posCol = 13}}]), nameFixity = Fixity' {theFixity = Fixity {fixityRange = NoRange, fixityLevel = Unrelated, fixityAssoc = NonAssoc}, theNotation = [], theNameRange = NoRange}, nameIsRecordName = False}}]
+  dataSort       = Set
+  dataMutual     = Nothing
+  dataAbstr      = <function>
+  }
+
+
+not = Function {
+  funClauses      =
+    |- test.Hello.Bool.true = test.Hello.Bool.false : test.Hello.Bool
+    |- test.Hello.Bool.false = test.Hello.Bool.true : test.Hello.Bool
+  funCompiled     =
+    case 0 of
+      test.Hello.Bool.false -> done[] test.Hello.Bool.true
+      test.Hello.Bool.true -> done[] test.Hello.Bool.false
+  funSplitTree    =
+    split at 0
+|
++- test.Hello.Bool.false -> done, 0 bindings
+|
+`- test.Hello.Bool.true -> done, 0 bindings
+
+  funTreeless     = (nothing)
+  funInv          =
+    Inverse
+      ConsHead test.Hello.Bool.false ->
+        [|- test.Hello.Bool.true = test.Hello.Bool.false : test.Hello.Bool]
+      ConsHead test.Hello.Bool.true ->
+        [|- test.Hello.Bool.false = test.Hello.Bool.true : test.Hello.Bool]
+  funMutual       = Just []
+  funAbstr        = ConcreteDef
+  funProjection   = MaybeProjection
+  funErasure      = False
+  funFlags        = fromList []
+  funTerminates   = Just True
+  funWith         = (nothing)
+  funIsKanOp      = (nothing)
+  funOpaque       = TransparentDef
+  }

test/Test.agda

@@ -11,39 +11,39 @@ data Exp (v : Set) : Set where
   Plus : Exp v → Exp v → Exp v
   Int : Nat → Exp v
   Var : v → Exp v
-{-# COMPILE AGDA2?? Exp #-}
+{-# COMPILE AGDA2RUST Exp #-}
 
 eval : (a → Nat) → Exp a → Nat
 eval env (Plus a b) = eval env a + eval env b
 eval env (Int n) = n
 eval env (Var x) = env x
-{-# COMPILE AGDA2?? eval #-}
+{-# COMPILE AGDA2RUST eval #-}
 
 -- ** Natural numbers
 
 sum : List Nat → Nat
 sum []       = 0
 sum (x ∷ xs) = x + sum xs
-{-# COMPILE AGDA2?? sum #-}
+{-# COMPILE AGDA2RUST sum #-}
 
 -- ** Polymorphic functions
 
 _++_ : List a → List a → List a
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
-{-# COMPILE AGDA2?? _++_ #-}
+{-# COMPILE AGDA2RUST _++_ #-}
 
 map : (a → b) → List a → List b
 map f [] = []
 map f (x ∷ xs) = f x ∷ map f xs
-{-# COMPILE AGDA2?? map #-}
+{-# COMPILE AGDA2RUST map #-}
 
 -- ** Lambdas
 
 plus3 : List Nat → List Nat
 plus3 = map (λ n → n + 3)
-{-# COMPILE AGDA2?? plus3 #-}
+{-# COMPILE AGDA2RUST plus3 #-}
 
 doubleLambda : Nat → Nat → Nat
 doubleLambda = λ a b → a + 2 * b
-{-# COMPILE AGDA2?? doubleLambda #-}
+{-# COMPILE AGDA2RUST doubleLambda #-}