Skip to content

Commit

Permalink
move options to explicit variable
Browse files Browse the repository at this point in the history
  • Loading branch information
lemastero committed Dec 17, 2023
1 parent df2598c commit 73fdbf5
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 10 deletions.
19 changes: 10 additions & 9 deletions src/Agda/Compiler/Rust/Backend.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,16 @@ import Control.Monad ( unless )
import Control.Monad.IO.Class ( MonadIO(liftIO) )
import Control.DeepSeq ( NFData(..) )
import Data.Maybe ( fromMaybe )

import System.Console.GetOpt ( OptDescr(Option), ArgDescr(ReqArg) )

import Data.Version ( showVersion )
import Paths_agda2rust ( version )
import System.Console.GetOpt ( OptDescr(Option), ArgDescr(ReqArg) )

import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName, moduleNameToFileName )
import Agda.Compiler.Common ( curIF, compileDir )
import Agda.Compiler.Backend ( Backend(..), Backend'(..), Recompile(..), IsMain )
import Agda.Interaction.Options ( Flag )
import Agda.Main ( runAgda )
import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName, moduleNameToFileName )
import Agda.TypeChecking.Monad (
CompilerPragma(..),
TCM,
TCMT,
iInsideScope,
Expand All @@ -33,6 +31,12 @@ runRustBackend = runAgda [Backend backend]
instance NFData Options where
rnf _ = ()

cmdLineFlags :: [OptDescr (Flag Options)]
cmdLineFlags = [
Option ['o'] ["out-dir"] (ReqArg outdirOpt "DIR")
"Write output files to DIR. (default: project root)"
]

outdirOpt :: Monad m => FilePath -> Options -> m Options
outdirOpt dir opts = return opts{ optOutDir = Just dir }

Expand All @@ -46,10 +50,7 @@ backend = Backend'
{ backendName = "agda2rust"
, backendVersion = Just (showVersion version)
, options = defaultOptions
, commandLineFlags =
[ Option ['o'] ["out-dir"] (ReqArg outdirOpt "DIR")
"Write output files to DIR. (default: project root)"
]
, commandLineFlags = cmdLineFlags
, isEnabled = const True
, preCompile = return
, postCompile = const $ const $ const $ return ()
Expand Down
2 changes: 1 addition & 1 deletion src/Agda/Compiler/Rust/ToRustCompiler.hs
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ compileDefn defName theDef =

compileDataType :: QName -> [QName] -> CompiledDef
compileDataType defName fields = "enum" <> exprSeparator
<> showName defName
<> showName defName
<> exprSeparator
<> bracket (
indent
Expand Down

0 comments on commit 73fdbf5

Please sign in to comment.