summaryrefslogtreecommitdiff
path: root/src/full/Agda/Compiler/MAlonzo/Encode.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Compiler/MAlonzo/Encode.hs')
-rw-r--r--src/full/Agda/Compiler/MAlonzo/Encode.hs77
1 files changed, 1 insertions, 76 deletions
diff --git a/src/full/Agda/Compiler/MAlonzo/Encode.hs b/src/full/Agda/Compiler/MAlonzo/Encode.hs
index 57b9576..7b804b2 100644
--- a/src/full/Agda/Compiler/MAlonzo/Encode.hs
+++ b/src/full/Agda/Compiler/MAlonzo/Encode.hs
@@ -4,28 +4,15 @@
module Agda.Compiler.MAlonzo.Encode
( encodeModuleName
- , tests
) where
import Data.Char
import Data.Function
import Data.List
-import qualified Language.Haskell.Exts.Syntax as HS
-import Test.QuickCheck
+import qualified Agda.Utils.Haskell.Syntax as HS
import Agda.Compiler.MAlonzo.Misc
-import Agda.Utils.QuickCheck
-import Agda.Utils.TestHelpers
-
--- | Can the character be used in a Haskell module name part
--- (@conid@)? This function is more restrictive than what the Haskell
--- report allows.
-
-isModChar :: Char -> Bool
-isModChar c =
- isLower c || isUpper c || isDigit c || c == '_' || c == '\''
-
-- | Haskell module names have to satisfy the Haskell (including the
-- hierarchical module namespace extension) lexical syntax:
--
@@ -80,65 +67,3 @@ encodeModuleName (HS.ModuleName s) = HS.ModuleName $ case stripPrefix mazstr s o
enc c r | isOK c = c : r
| otherwise = escapeChar : shows (fromEnum c) (escapeChar : r)
-
--- Note: This injectivity test is quite weak. A better, dedicated
--- generator could strengthen it.
-
-prop_encodeModuleName_injective :: M -> M -> Bool
-prop_encodeModuleName_injective (M s1) (M s2) =
- if encodeModuleName (HS.ModuleName s1) ==
- encodeModuleName (HS.ModuleName s2) then
- s1 == s2
- else
- True
-
-prop_encodeModuleName_OK :: M -> Bool
-prop_encodeModuleName_OK (M s') =
- s ~= unM (encodeModuleName (HS.ModuleName s))
- where
- s = mazstr ++ "." ++ s'
-
- "" ~= "" = True
- ('.' : s) ~= ('.' : s') = s ~= s'
- s ~= (c : s') = isUpper c && all isModChar s1' &&
- dropWhile (/= '.') s ~= s2'
- where (s1', s2') = span (/= '.') s'
- _ ~= _ = False
-
- unM (HS.ModuleName s) = s
-
-prop_encodeModuleName_preserved :: M -> Property
-prop_encodeModuleName_preserved (M m) =
- shouldBePreserved m ==>
- encodeModuleName (HS.ModuleName m) == HS.ModuleName m
- where
- shouldBePreserved m =
- not (m == mazstr || (mazstr ++ ".") `isPrefixOf` m)
-
--- | Agda module names. Used to test 'encodeModuleName'.
-
-newtype M = M String deriving (Show)
-
-instance Arbitrary M where
- arbitrary = do
- ms <- choose (0, 2)
- m <- vectorOf ms namePart
- return $ M (intercalate "." m)
- where
- namePart =
- oneof [ return mazstr
- , do cs <- choose (1, 2)
- vectorOf cs (elements "a_AQZ0'-∀")
- ]
-
-------------------------------------------------------------------------
--- All tests
-
--- | All the properties.
-
-tests :: IO Bool
-tests = runTests "Agda.Compiler.MAlonzo.Encode"
- [ quickCheck' prop_encodeModuleName_injective
- , quickCheck' prop_encodeModuleName_OK
- , quickCheck' prop_encodeModuleName_preserved
- ]