From f99f6a20212140c233811edf537ca4ec74014a4c Mon Sep 17 00:00:00 2001 From: lemastero Date: Wed, 22 Nov 2023 14:00:40 +0100 Subject: [PATCH] expand backend definitions: commandLineFlags, scalaPostModule, scalaCompileDef --- src/Agda/Compiler/Scala/Backend.hs | 34 +++++++++++++++++++++++++----- 1 file changed, 29 insertions(+), 5 deletions(-) diff --git a/src/Agda/Compiler/Scala/Backend.hs b/src/Agda/Compiler/Scala/Backend.hs index b7146c0..fe19f79 100644 --- a/src/Agda/Compiler/Scala/Backend.hs +++ b/src/Agda/Compiler/Scala/Backend.hs @@ -5,7 +5,17 @@ module Agda.Compiler.Scala.Backend ( ) where import Agda.Main ( runAgda ) -import Agda.Compiler.Backend +import Agda.Compiler.Backend ( + Backend(..) + , Backend'(..) + , Definition + , Flag + , IsMain + , Recompile(..) + , TCM + ) +import Agda.Interaction.Options ( OptDescr ) +import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName ) runScalaBackend :: IO () runScalaBackend = runAgda [scalaBackend] @@ -21,16 +31,30 @@ type ScalaDefinition = () scalaBackend' :: Backend' ScalaFlags ScalaEnv ScalaModuleEnv ScalaModule ScalaDefinition scalaBackend' = Backend' - { backendName = "Scala" + { backendName = "agda2scala" , backendVersion = Just "0.1" , options = () - , commandLineFlags = [] + , commandLineFlags = scalaCmdLineFlags , isEnabled = const True , preCompile = \ opt -> return opt , postCompile = \ _ _ _ -> return () , preModule = \ _ _ _ _ -> return $ Recompile () - , postModule = \ _ _ _ _ _ -> return () - , compileDef = \ _ _ _ _ -> return () + , postModule = scalaPostModule + , compileDef = scalaCompileDef , scopeCheckingSuffices = False , mayEraseType = const $ return True } + +scalaCmdLineFlags :: [OptDescr (Flag ScalaFlags)] +scalaCmdLineFlags = [] + +scalaPostModule :: ScalaEnv + -> ScalaModuleEnv + -> IsMain + -> TopLevelModuleName + -> [ScalaDefinition] + -> TCM ScalaModule +scalaPostModule = \ _ _ _ _ _ -> return () + +scalaCompileDef :: ScalaEnv -> ScalaModuleEnv -> IsMain -> Definition -> TCM ScalaDefinition +scalaCompileDef = \ _ _ _ _ -> return ()