Rewrite rules: specifiable imports from Prelude (#193)

* Now the handling of Prelude can be specified in the config file

* Updating documentation

Author: viktorcsimma

docs/source/features.md

@@ -891,7 +891,9 @@ testA = A.foo
 testB = A.foo
 ```
 
-# Rewrite rules
+# Rewrite rules and Prelude imports
+
+## Rewrite rules
 
 User-defined rewrite rules for names can be defined through YAML configuration files. These should be provided via the `--rewrite-rules` option.
 
@@ -1008,8 +1010,38 @@ denominatorMinus1 = fromIntegral . denominator
 
 See also `rewrite-rules-example.yaml` in the root of the repository.
 
-**Known issues:**
-- If you import something from Prelude, you have to state this explicitly.
-- Then, it will add an import like import Prelude (...), which shadows all the other functions in Prelude. This is not necessarily a problem; as we will probably not modify the generated Haskell files by hand, and so we won't add any new Prelude functions.
-- But this only works for things you do use, not for those that you only define. For example, if you write an instance of the Num class and define signum but do not use it, it will not get into Prelude's import list, and so GHC will complain.
+## Handling of Prelude
+
+By default, agda2hs handles Prelude like other modules: it collects all the identifiers it finds we use from Prelude, and adds them to Prelude's import list.
+
+In the config YAML, we can specify a different behaviour. The format is:
+
+```yaml
+# First, we specify how to handle Prelude.
+prelude:
+  implicit: true
+  hiding:           # if implicit is true
+    - seq
+
+  #using:           # if implicit is false
+  #  - +
+  #  - Num
+
+# Then the rules themselves.
+rules:
+
+  # The rational type.
+  - from: Data.Rational.Unnormalised.Base.ℚᵘ
+    to: Rational
+    importing: Data.Ratio
+  - [...]
+```
+
+If `implicit` is `true`, then everything gets imported from Prelude, except for those that are specified in the `hiding` list. This can cause clashes if you reuse names from Prelude, hence the opportunity for a `hiding` list. If there is no such list, then everything gets imported.
+
+If `implicit` is `false`, Prelude gets imported explicitly, and only those identifiers that are specified in the `using` list. If there is no such list, agda2hs reverts to the default behaviour (it tries to collect imports by itself).
+
+## Known issues
+
+- Rewrite rules only work for things you do use, not for those that you only define. This causes a problem with class instances: if you choose the default behaviour, then write an instance of the Num class and define signum but do not use it, it will not get into Prelude's import list, and so GHC will complain.
 - You cannot change to a version with arguments of different modality without getting useless code. So if you rewrite a function to a version which has some of its parameters erased, the parameters remain there; probably because rewriting happens only after compiling the type signature.

rewrite-rules-example.yaml

@@ -1,103 +1,104 @@
 # An example config file for the '--rewrite-rules' option.
 # Imagine a library which uses the Agda standard library extensively and let's suppose we would like to translate its operators to the Haskell equivalents. The library includes a Haskell.Prim.Num.Num instance.
 
-# We have to include this so that Num is written to the import list of Prelude.
-- from: Haskell.Prim.Num.Num
-  to: Num
-  importing: Prelude
-# And it doesn't see these by default either, if not included in Prelude's import list.
-- from: Haskell.Prim.Num.Num.fromInteger
-  to: fromInteger
-  importing: Prelude
-- from: Haskell.Prim.Num.Num.signum
-  to: signum
-  importing: Prelude
+# First, we specify how to handle Prelude.
+prelude:
+  implicit: true
+  hiding:           # if implicit is true
+    - seq
 
-# The rational type.
-- from: Data.Rational.Unnormalised.Base.ℚᵘ
-  to: Rational
-  importing: Data.Ratio
+  #using:           # if implicit is false
+  #  - +            # (+) should be given like that
+  #  - Num
 
-# Arithmetic operators.
-# Note: Prelude has to be specified too!
-- from: Agda.Builtin.Nat._+_
-  to: _+_
-  importing: Prelude
-- from: Agda.Builtin.Nat._*_
-  to: _*_
-  importing: Prelude
-- from: Agda.Builtin.Nat.-_
-  to: negate
-  importing: Prelude
-- from: Agda.Builtin.Nat._-_
-  to: _-_
-  importing: Prelude
-- from: Data.Nat.Base._⊔_
-  to: max
-  importing: Prelude
+#Then the rules themselves.
+rules:
 
-- from: Agda.Builtin.Integer._+_
-  to: _+_
-  importing: Prelude
-- from: Data.Integer.Base._*_
-  to: _*_
-  importing: Prelude
-- from: Agda.Builtin.Integer.-_
-  to: negate
-  importing: Prelude
-- from: Agda.Builtin.Integer._-_
-  to: _-_
-  importing: Prelude
+  # The rational type.
+  - from: Data.Rational.Unnormalised.Base.ℚᵘ
+    to: Rational
+    importing: Data.Ratio
 
-- from: Data.Rational.Unnormalised.Base._+_
-  to: _+_
-  importing: Prelude
-- from: Data.Rational.Unnormalised.Base._*_
-  to: _*_
-  importing: Prelude
-- from: Data.Rational.Unnormalised.Base.-_
-  to: negate
-  importing: Prelude
-- from: Data.Rational.Unnormalised.Base._-_
-  to: _-_
-  importing: Prelude
-- from: Data.Rational.Unnormalised.Base._/_
-  to: _%_
-  importing: Data.Ratio
-- from: Data.Rational.Unnormalised.Base._⊔_
-  to: max
-  importing: Prelude
-- from: Data.Rational.Unnormalised.Base._⊓_
-  to: min
-  importing: Prelude
-- from: Data.Rational.Unnormalised.Base.∣_∣
-  to: abs
-  importing: Prelude
-- from: Data.Integer.Base.∣_∣
-  to: intAbs
-  importing: Base
+  # Arithmetic operators.
+  # Note: Prelude has to be specified too!
+  - from: Agda.Builtin.Nat._+_
+    to: _+_
+    importing: Prelude
+  - from: Agda.Builtin.Nat._*_
+    to: _*_
+    importing: Prelude
+  - from: Agda.Builtin.Nat.-_
+    to: negate
+    importing: Prelude
+  - from: Agda.Builtin.Nat._-_
+    to: _-_
+    importing: Prelude
+  - from: Data.Nat.Base._⊔_
+    to: max
+    importing: Prelude
 
-# Standard library functions related to naturals and integers.
-- from: Agda.Builtin.Nat.Nat.suc
-  to: suc
-  importing: Base
-- from: Agda.Builtin.Int.Int.pos
-  to: toInteger
-  importing: Prelude
-- from: Data.Integer.DivMod._divℕ_
-  to: divNat
-  importing: Base
-- from: Data.Nat.DivMod._/_
-  to: div
-  importing: Prelude
+  - from: Agda.Builtin.Integer._+_
+    to: _+_
+    importing: Prelude
+  - from: Data.Integer.Base._*_
+    to: _*_
+    importing: Prelude
+  - from: Agda.Builtin.Integer.-_
+    to: negate
+    importing: Prelude
+  - from: Agda.Builtin.Integer._-_
+    to: _-_
+    importing: Prelude
 
-# Standard library functions related to rationals.
-- from: Data.Rational.Unnormalised.Base.ℚᵘ.numerator
-  to: numerator
-  importing: Data.Ratio
-- from: Data.Rational.Unnormalised.Base.ℚᵘ.denominator
-  to: denominatorNat
-  importing: Base       #the Base version returns a Natural
-- from: Data.Rational.Unnormalised.Base.ℚᵘ.denominator-1
-  to: denominatorMinus1
-  importing: Base
+  - from: Data.Rational.Unnormalised.Base._+_
+    to: _+_
+    importing: Prelude
+  - from: Data.Rational.Unnormalised.Base._*_
+    to: _*_
+    importing: Prelude
+  - from: Data.Rational.Unnormalised.Base.-_
+    to: negate
+    importing: Prelude
+  - from: Data.Rational.Unnormalised.Base._-_
+    to: _-_
+    importing: Prelude
+  - from: Data.Rational.Unnormalised.Base._/_
+    to: _%_
+    importing: Data.Ratio
+  - from: Data.Rational.Unnormalised.Base._⊔_
+    to: max
+    importing: Prelude
+  - from: Data.Rational.Unnormalised.Base._⊓_
+    to: min
+    importing: Prelude
+  - from: Data.Rational.Unnormalised.Base.∣_∣
+    to: abs
+    importing: Prelude
+  - from: Data.Integer.Base.∣_∣
+    to: intAbs
+    importing: Base
+
+  # Standard library functions related to naturals and integers.
+  - from: Agda.Builtin.Nat.Nat.suc
+    to: suc
+    importing: Base
+  - from: Agda.Builtin.Int.Int.pos
+    to: toInteger
+    importing: Prelude
+  - from: Data.Integer.DivMod._divℕ_
+    to: divNat
+    importing: Base
+  - from: Data.Nat.DivMod._/_
+    to: div
+    importing: Prelude
+
+  # Standard library functions related to rationals.
+  - from: Data.Rational.Unnormalised.Base.ℚᵘ.numerator
+    to: numerator
+    importing: Data.Ratio
+  - from: Data.Rational.Unnormalised.Base.ℚᵘ.denominator
+    to: denominatorNat
+    importing: Base       #the Base version returns a Natural
+  - from: Data.Rational.Unnormalised.Base.ℚᵘ.denominator-1
+    to: denominatorMinus1
+    importing: Base

src/Agda2Hs/Compile.hs

@@ -48,7 +48,7 @@ runC tlm rewrites = runWriterT
 
 compile :: Options -> ModuleEnv -> IsMain -> Definition ->
   TCM (CompiledDef, CompileOutput)
-compile opts tlm _ def = withCurrentModule (qnameModule $ defName def) $ runC tlm (rewriteRules opts) $
+compile opts tlm _ def = withCurrentModule (qnameModule $ defName def) $ runC tlm (optRewrites opts) $
   compileAndTag <* postCompile
   where
     tag code = [(nameBindingSite $ qnameName $ defName def, code)]

src/Agda2Hs/Compile/Imports.hs

@@ -1,5 +1,5 @@
 
-module Agda2Hs.Compile.Imports ( compileImports ) where
+module Agda2Hs.Compile.Imports ( compileImports, makeManualDecl ) where
 
 import Data.Char ( isUpper )
 import Data.List ( isPrefixOf )
@@ -60,7 +60,9 @@ compileImports top is0 = do
     makeImportDecl :: Hs.ModuleName () -> Qualifier -> ImportSpecMap -> Hs.ImportDecl ()
     makeImportDecl mod qual specs = Hs.ImportDecl ()
       mod (isQualified qual) False False Nothing (qualifiedAs qual)
-      (Just $ Hs.ImportSpecList () False $ map (uncurry makeImportSpec) $ Map.toList specs)
+      (Just $ Hs.ImportSpecList ()
+            False                                             -- whether the list should be a list of hidden identifiers ('hiding')
+            $ map (uncurry makeImportSpec) $ Map.toList specs)
 
     checkClashingImports :: Imports -> TCM ()
     checkClashingImports [] = return ()
@@ -76,3 +78,12 @@ compileImports top is0 = do
           ++ prettyShow (pp <$> p') ++ ")"
         -- TODO: no range information as we only have Haskell names at this point
 
+-- if the user has provided a "using" or "hiding" list in the config file
+-- used for Prelude
+makeManualDecl :: Hs.ModuleName () -> Qualifier -> Bool -> [String] -> Hs.ImportDecl ()
+makeManualDecl mod qual isImplicit namesToHide = Hs.ImportDecl ()
+       mod (isQualified qual) False False Nothing (qualifiedAs qual)
+      (Just $ Hs.ImportSpecList ()
+            isImplicit        -- whether the list should be a list of hidden identifiers ('hiding')
+            $ map (Hs.IVar() . (\str -> if validVarId str || validConId str then Hs.Ident() str else Hs.Symbol() str))    -- since we can only read strings from the config file, we have to do this
+            namesToHide) -- map (uncurry makeImportSpec) $ Map.toList specs)

src/Agda2Hs/Compile/Rewrites.hs

@@ -1,31 +1,73 @@
 -- Reads custom rewrite rules of the user from a YAML config file.
-module Agda2Hs.Compile.Rewrites where
+module Agda2Hs.Compile.Rewrites (readConfigFile) where
 
 import Data.Yaml.YamlLight
 import qualified Data.Map as Map
 import qualified Data.Text as Text
 import Data.Text.Encoding (decodeUtf8, encodeUtf8)
 import qualified Data.ByteString as ByteString
+import Data.Char (toLower)
+import Data.Maybe (isJust)
 
--- There is already a RewriteRule identifier in Agda internals, hence the name.
--- Elements:
-  -- the identifier to rewrite ("from")
-  -- the identifier with which we replace it ("to")
-  -- the import to use, if any ("importing")
-data Rewrite = Rewrite {from :: String, to :: String, importing :: Maybe String}
+import Agda2Hs.Compile.Types
 
-type Rewrites = [Rewrite]
+-- Conversions from String to ByteString and vice versa.
+-- We assume UTF-8.
+stringToByteString :: String -> ByteString.ByteString
+stringToByteString = encodeUtf8 . Text.pack
+byteStringToString :: ByteString.ByteString -> String
+byteStringToString = Text.unpack . decodeUtf8
+
+-- A simple element consisting of the string given. Useful when looking up maps.
+stringElement :: String -> YamlLight
+stringElement = YStr . stringToByteString
+
+-- Read Prelude options from a YamlLight object. Fail if the format is incorrect.
+preludeOptionsFromYaml :: YamlLight -> Maybe PreludeOptions
+preludeOptionsFromYaml yaml = case lookupYL (stringElement "prelude") yaml of
+  Nothing            -> Nothing
+  Just (YMap dmap)   -> Just $ preludeOptionsFromMap dmap
+  Just otherYaml     -> error $ "Incorrect format for the rewrite rules file: the \"prelude\" element must be a map – " ++ show otherYaml
+  where
+    preludeOptionsFromMap :: Map.Map YamlLight YamlLight -> PreludeOptions
+    preludeOptionsFromMap dmap = (impl, namesToImp)
+      where
+        impl :: Bool
+        impl = case Map.lookup (stringElement "implicit") dmap of
+          Nothing        -> isJust $ Map.lookup (YStr $ stringToByteString "hiding") dmap
+          Just (YStr bs) -> let str = map toLower $ byteStringToString bs in
+                             str == "true" || str == "yes"
+          Just otherYaml -> error "Incorrect format for the rewrite rules file: \"implicit\" must be a boolean"
 
--- Read rewrite rules from a given file. Fail if the format is incorrect (necessary fields are absent).
-readRewritesFromFile :: FilePath -> IO Rewrites
-readRewritesFromFile fname = rulesFromYaml <$> parseYamlFile fname
+        namesToImp :: NamesToImport
+        namesToImp = if impl then hidingNames else importingNames         -- we search for different keys
+          where
+            hidingNames :: NamesToImport
+            hidingNames = case Map.lookup (stringElement "hiding") dmap of
+              Nothing        -> Names []    -- then we import the whole Prelude
+              Just (YSeq ls) -> Names $ map (parseElement "hiding") $ ls
+              Just otherYaml -> error "Incorrect format for the rewrite rules file: \"hiding\" must be a sequence"
+
+            importingNames :: NamesToImport
+            importingNames = case Map.lookup (stringElement "using") dmap of
+              Nothing        -> Auto       -- then we let agda2hs search for them
+              Just (YSeq ls) -> Names $ map (parseElement "using") $ ls
+              Just otherYaml -> error "Incorrect format for the rewrite rules file: \"\" must be a sequence"
+
+            parseElement :: String -> YamlLight -> String
+            parseElement seqName y = case (unStr y) of
+              Nothing -> error "Incorrect format for the rewrite rules file: an element in \"" ++ seqName ++ "\" was not a string"
+              Just bs -> byteStringToString bs
 
 -- Read rewrite rules from a YamlLight object. Fail if the format is incorrect.
 rulesFromYaml :: YamlLight -> Rewrites
-rulesFromYaml y = case y of
-  YNil -> []
-  YSeq ls -> map ruleFromElement ls
-  otherYaml -> error $ "Incorrect format for the rewrite rules file: must be a list of elements – " ++ show otherYaml
+rulesFromYaml y = case lookupYL (stringElement "rules") y of
+  Nothing           -> case y of   -- maybe the root is the sequence
+                         YSeq ls -> map ruleFromElement ls
+                         _       -> []
+  Just YNil         -> []
+  Just (YSeq ls)    -> map ruleFromElement ls
+  Just otherYaml    -> error $ "Incorrect format for the rewrite rules file: \"rules\" must be a list of elements – " ++ show otherYaml
   where
     -- parsing a single element
     ruleFromElement :: YamlLight -> Rewrite
@@ -55,9 +97,11 @@ rulesFromYaml y = case y of
       Just bytestr -> Right $ byteStringToString $ bytestr
       Nothing      -> Left $ "Not a string element: " ++ show yaml
 
--- Conversions from String to ByteString and vice versa.
--- We assume UTF-8.
-stringToByteString :: String -> ByteString.ByteString
-stringToByteString = encodeUtf8 . Text.pack
-byteStringToString :: ByteString.ByteString -> String
-byteStringToString = Text.unpack . decodeUtf8
+-- The exported function to be used in Main.hs.
+readConfigFile :: FilePath -> IO Config
+readConfigFile fname = (,) <$>
+                       (preludeOptionsFromYaml <$> wholeYaml) <*>
+                       (rulesFromYaml <$> wholeYaml)
+  where
+    wholeYaml :: IO YamlLight
+    wholeYaml = parseYamlFile fname