|
1 | 1 | -- Reads custom rewrite rules of the user from a YAML config file. |
2 | | -module Agda2Hs.Compile.Rewrites where |
| 2 | +module Agda2Hs.Compile.Rewrites (readConfigFile) where |
3 | 3 |
|
4 | 4 | import Data.Yaml.YamlLight |
5 | 5 | import qualified Data.Map as Map |
6 | 6 | import qualified Data.Text as Text |
7 | 7 | import Data.Text.Encoding (decodeUtf8, encodeUtf8) |
8 | 8 | import qualified Data.ByteString as ByteString |
| 9 | +import Data.Char (toLower) |
| 10 | +import Data.Maybe (isJust) |
9 | 11 |
|
10 | | --- There is already a RewriteRule identifier in Agda internals, hence the name. |
11 | | --- Elements: |
12 | | - -- the identifier to rewrite ("from") |
13 | | - -- the identifier with which we replace it ("to") |
14 | | - -- the import to use, if any ("importing") |
15 | | -data Rewrite = Rewrite {from :: String, to :: String, importing :: Maybe String} |
| 12 | +import Agda2Hs.Compile.Types |
16 | 13 |
|
17 | | -type Rewrites = [Rewrite] |
| 14 | +-- Conversions from String to ByteString and vice versa. |
| 15 | +-- We assume UTF-8. |
| 16 | +stringToByteString :: String -> ByteString.ByteString |
| 17 | +stringToByteString = encodeUtf8 . Text.pack |
| 18 | +byteStringToString :: ByteString.ByteString -> String |
| 19 | +byteStringToString = Text.unpack . decodeUtf8 |
| 20 | + |
| 21 | +-- A simple element consisting of the string given. Useful when looking up maps. |
| 22 | +stringElement :: String -> YamlLight |
| 23 | +stringElement = YStr . stringToByteString |
| 24 | + |
| 25 | +-- Read Prelude options from a YamlLight object. Fail if the format is incorrect. |
| 26 | +preludeOptionsFromYaml :: YamlLight -> Maybe PreludeOptions |
| 27 | +preludeOptionsFromYaml yaml = case lookupYL (stringElement "prelude") yaml of |
| 28 | + Nothing -> Nothing |
| 29 | + Just (YMap dmap) -> Just $ preludeOptionsFromMap dmap |
| 30 | + Just otherYaml -> error $ "Incorrect format for the rewrite rules file: the \"prelude\" element must be a map – " ++ show otherYaml |
| 31 | + where |
| 32 | + preludeOptionsFromMap :: Map.Map YamlLight YamlLight -> PreludeOptions |
| 33 | + preludeOptionsFromMap dmap = (impl, namesToImp) |
| 34 | + where |
| 35 | + impl :: Bool |
| 36 | + impl = case Map.lookup (stringElement "implicit") dmap of |
| 37 | + Nothing -> isJust $ Map.lookup (YStr $ stringToByteString "hiding") dmap |
| 38 | + Just (YStr bs) -> let str = map toLower $ byteStringToString bs in |
| 39 | + str == "true" || str == "yes" |
| 40 | + Just otherYaml -> error "Incorrect format for the rewrite rules file: \"implicit\" must be a boolean" |
18 | 41 |
|
19 | | --- Read rewrite rules from a given file. Fail if the format is incorrect (necessary fields are absent). |
20 | | -readRewritesFromFile :: FilePath -> IO Rewrites |
21 | | -readRewritesFromFile fname = rulesFromYaml <$> parseYamlFile fname |
| 42 | + namesToImp :: NamesToImport |
| 43 | + namesToImp = if impl then hidingNames else importingNames -- we search for different keys |
| 44 | + where |
| 45 | + hidingNames :: NamesToImport |
| 46 | + hidingNames = case Map.lookup (stringElement "hiding") dmap of |
| 47 | + Nothing -> Names [] -- then we import the whole Prelude |
| 48 | + Just (YSeq ls) -> Names $ map (parseElement "hiding") $ ls |
| 49 | + Just otherYaml -> error "Incorrect format for the rewrite rules file: \"hiding\" must be a sequence" |
| 50 | + |
| 51 | + importingNames :: NamesToImport |
| 52 | + importingNames = case Map.lookup (stringElement "using") dmap of |
| 53 | + Nothing -> Auto -- then we let agda2hs search for them |
| 54 | + Just (YSeq ls) -> Names $ map (parseElement "using") $ ls |
| 55 | + Just otherYaml -> error "Incorrect format for the rewrite rules file: \"\" must be a sequence" |
| 56 | + |
| 57 | + parseElement :: String -> YamlLight -> String |
| 58 | + parseElement seqName y = case (unStr y) of |
| 59 | + Nothing -> error "Incorrect format for the rewrite rules file: an element in \"" ++ seqName ++ "\" was not a string" |
| 60 | + Just bs -> byteStringToString bs |
22 | 61 |
|
23 | 62 | -- Read rewrite rules from a YamlLight object. Fail if the format is incorrect. |
24 | 63 | rulesFromYaml :: YamlLight -> Rewrites |
25 | | -rulesFromYaml y = case y of |
26 | | - YNil -> [] |
27 | | - YSeq ls -> map ruleFromElement ls |
28 | | - otherYaml -> error $ "Incorrect format for the rewrite rules file: must be a list of elements – " ++ show otherYaml |
| 64 | +rulesFromYaml y = case lookupYL (stringElement "rules") y of |
| 65 | + Nothing -> case y of -- maybe the root is the sequence |
| 66 | + YSeq ls -> map ruleFromElement ls |
| 67 | + _ -> [] |
| 68 | + Just YNil -> [] |
| 69 | + Just (YSeq ls) -> map ruleFromElement ls |
| 70 | + Just otherYaml -> error $ "Incorrect format for the rewrite rules file: \"rules\" must be a list of elements – " ++ show otherYaml |
29 | 71 | where |
30 | 72 | -- parsing a single element |
31 | 73 | ruleFromElement :: YamlLight -> Rewrite |
@@ -55,9 +97,11 @@ rulesFromYaml y = case y of |
55 | 97 | Just bytestr -> Right $ byteStringToString $ bytestr |
56 | 98 | Nothing -> Left $ "Not a string element: " ++ show yaml |
57 | 99 |
|
58 | | --- Conversions from String to ByteString and vice versa. |
59 | | --- We assume UTF-8. |
60 | | -stringToByteString :: String -> ByteString.ByteString |
61 | | -stringToByteString = encodeUtf8 . Text.pack |
62 | | -byteStringToString :: ByteString.ByteString -> String |
63 | | -byteStringToString = Text.unpack . decodeUtf8 |
| 100 | +-- The exported function to be used in Main.hs. |
| 101 | +readConfigFile :: FilePath -> IO Config |
| 102 | +readConfigFile fname = (,) <$> |
| 103 | + (preludeOptionsFromYaml <$> wholeYaml) <*> |
| 104 | + (rulesFromYaml <$> wholeYaml) |
| 105 | + where |
| 106 | + wholeYaml :: IO YamlLight |
| 107 | + wholeYaml = parseYamlFile fname |
0 commit comments