Skip to content

Commit

Permalink
remove unnecessary agda2hs-mode deps
Browse files Browse the repository at this point in the history
and make more config fields optional
  • Loading branch information
flupe committed Nov 13, 2023
1 parent 65185fa commit a98df16
Show file tree
Hide file tree
Showing 4 changed files with 15 additions and 30 deletions.
4 changes: 2 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@ repl :
cabal new-repl # e.g. `:set args -itest -otest/build test/AllTests.agda ... main ... :r ... main`

test :
cabal new-install --overwrite-policy=always --installdir=test --install-method=copy
cabal new-install agda2hs --overwrite-policy=always --installdir=test --install-method=copy
make -C test

golden :
make -C test golden

docs :
cd docs && make html
cd docs && make html
22 changes: 4 additions & 18 deletions agda2hs.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ executable agda2hs
text >= 2.0.2 && < 2.1,
deepseq >= 1.4.4 && < 1.5,
yaml >= 0.11 && < 0.12,
aeson >= 2.2 && < 2.3
aeson >= 2.2 && < 2.3,
default-language: Haskell2010
default-extensions: LambdaCase,
RecordWildCards,
Expand All @@ -88,26 +88,12 @@ executable agda2hs-mode
main-is: Main.hs
other-modules: Paths_agda2hs
autogen-modules: Paths_agda2hs
build-depends: base >= 4.10 && < 4.18,
Agda >= 2.6.4 && < 2.6.5,
bytestring >= 0.11.5 && < 0.12,
containers >= 0.6 && < 0.7,
unordered-containers >= 0.2.19 && < 0.3,
mtl >= 2.2.2 && < 2.3,
build-depends: base >= 4.10 && < 4.18,
directory >= 1.2.6.2 && < 1.4,
filepath >= 1.4.1.0 && < 1.5,
haskell-src-exts >= 1.23 && < 1.25,
syb >= 0.7.2 && < 0.8,
text >= 2.0.2 && < 2.1,
deepseq >= 1.4.4 && < 1.5,
process >= 1.6.3.0 && < 1.7,
yaml >= 0.11 && < 0.12,
aeson >= 2.2 && < 2.3
filepath >= 1.4.1.0 && < 1.5,
process >= 1.6.3.0 && < 1.7,
default-language: Haskell2010
default-extensions: LambdaCase,
RecordWildCards,
FlexibleContexts,
MultiWayIf,
TupleSections,
ScopedTypeVariables
ghc-options: -Werror
17 changes: 9 additions & 8 deletions src/Agda2Hs/Config.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,9 @@ import Control.Monad.IO.Class ( MonadIO )
import GHC.Generics

import Data.Functor ( (<&>) )
import Data.Foldable ( fold )
import Data.Maybe ( fromMaybe )
import Data.Aeson ( FromJSON(parseJSON), withObject, (.:) )
import Data.Aeson ( FromJSON(parseJSON), withObject, (.:), (.:?), (.:?=) )
import qualified Data.Map.Strict as Map
import qualified Data.Yaml as Yaml ( decodeFileThrow )

Expand All @@ -18,33 +19,33 @@ import Agda.TypeChecking.Monad.Base (TCM)
-- | Config file data.
data Config = Config
{ cfgPrelude :: Maybe PreludeOptions
, cfgRewrites :: Rewrites
, cfgRewrites :: Maybe Rewrites
}

instance FromJSON Rewrite where
parseJSON = withObject "rewrite rule" $ \v ->
Rewrite <$> v .: "from"
<*> v .: "to"
<*> v .: "importing"
<*> v .:? "importing"

instance FromJSON PreludeOptions where
parseJSON = withObject "prelude options" $ \v ->
PreludeOpts <$> v .: "implicit"
<*> v .: "using"
<*> v .: "hiding"
<*> v .:? "using"
<*> v .:?= "hiding"

instance FromJSON Config where
parseJSON = withObject "config" $ \v ->
Config <$> v .: "prelude"
<*> v .: "rewrites"
Config <$> v .:? "prelude"
<*> v .:? "rewrites"

readConfigFile :: MonadIO m => FilePath -> m Config
readConfigFile = Yaml.decodeFileThrow

applyConfig :: Options -> Config -> Options
applyConfig opts cfg =
opts { optPrelude = fromMaybe (optPrelude opts) (cfgPrelude cfg)
, optRewrites = foldl addRewrite (optRewrites opts) (cfgRewrites cfg)
, optRewrites = foldl addRewrite (optRewrites opts) (fold $ cfgRewrites cfg)
}
where addRewrite :: SpecialRules -> Rewrite -> SpecialRules
addRewrite rules (Rewrite from to importing) = Map.insert from (toNameImport to importing) rules
Expand Down
2 changes: 0 additions & 2 deletions src/agda2hs-mode/Main.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
{-# LANGUAGE ScopedTypeVariables #-}

-- | A program which either tries to add setup code for Agda's Emacs
-- mode to the users .emacs file, or provides information to Emacs
-- about where the Emacs mode is installed.
Expand Down

0 comments on commit a98df16

Please sign in to comment.