agda2scala

Examples

are in ./examples

Working with source code

• Starting continuous compilation loop

ghcid

• Build

cabal build all

• Simple way to run Scala backend

cabal run -- agda2scala --help
cabal run -- agda2scala ./examples/adts.agda

• Generate Scala2 output

cabal run -- agda2scala --compile --no-main --out-dir=scala2/src/main/scala ./examples/adts.agda

• Generate Scala3 (dotty) output

cabal run -- agda2scala --compile --no-main --scala-dialect=Scala3 --out-dir=scala3/src/main/scala ./examples/adts.agda

cabal run -- agda2scala --help
cabal run -- agda2scala ./examples/adts.agda
cabal run -- agda2scala --compile --no-main --out-dir=scala2/src/main/scala ./examples/adts.agda

• Run tests

cabal test all

Resources

• Documentation for Agda as Haskell library on Hackage including
  • docs for Agda.Compiler.Backend
  • build-in JS backend
  • build-in Haskell backend
• external project with Agda backends
  • omelkonian/agda-minimal-backend
  • jespercockx/agda2scheme
  • omelkonian/agda2train
  • agda/agda2hs, (publication)
  • HectorPeeters/agda2rust, (publication)
  • lemastero/agda2rust