← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Compiler/MAlonzo/Encode.hs

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-05 23:43:20 UTC
  • mfrom: (1.1.1 upstream)
  • Revision ID: james.westby@ubuntu.com-20100105234320-6ksc0sdsfhtweknu
Tags: 2.2.6-1
http://bugs.debian.org/559197
* New upstream release 2.2.6, for headlines please see:
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6
* debian/control
  + Bump standards-version to 3.8.3, no changes
  + Fix Vcs-Git to point to correct URL
  + Update build-depends for new upstream release
  + Undo arch/indep split per current pkg-haskell practice
  + Add Homepage field
* debian/copyright: Fix encoding to UTF-8 (thanks Lintian) 
* debian/README.source: Remove, no repacking so not necessary any more 
* debian/50agda.el:
  + Only load file if it exists, prevents a non-intrusive emacs warning
    where 50agda.el is left on system when package is removed. 
    (Closes: #559197). 
  + Do not load file on XEmacs — agda-mode is not compatible with XEmacs.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Compiler/MAlonzo/Encode.hs
13
13
import Language.Haskell.Syntax
14
14
import Test.QuickCheck
15
15
 
 
16
import Agda.Compiler.MAlonzo.Misc
 
17
 
16
18
import Agda.Utils.QuickCheck
17
19
import Agda.Utils.TestHelpers
18
20
 
30
32
--   @modid -> [modid.] large {small | large | digit | ' }@
31
33
--
32
34
-- 'encodeModuleName' is an injective function into the set of module
 
35
-- names defined by @modid@. The function preserves @.@s, and it also
 
36
-- preserves module names whose first name part is not 'mazstr'.
33
37
--
34
38
-- Precondition: The input must not start or end with @.@, and no two
35
39
-- @.@s may be adjacent.
36
40
 
37
41
encodeModuleName :: Module -> Module
38
 
encodeModuleName (Module s) = Module (concatMap encNamePart $ splitUp s)
 
42
encodeModuleName (Module s) = Module $ case splitUp s of
 
43
  p : ps | p == mazstr -> concat (p : map encNamePart ps)
 
44
  _                    -> s
39
45
  where
40
46
  -- splitUp ".apa.bepa." == [".","apa",".","bepa","."]
41
47
  splitUp = groupBy ((&&) `on` (/= '.'))
46
50
  encNamePart s   = ensureFirstCharLarge s ++ concatMap enc s
47
51
 
48
52
  ensureFirstCharLarge s = case s of
49
 
    c : cs | isUpper c -> ""
50
 
    _                  -> "M"
51
 
 
52
 
  isOK c = c /= 'Z' && isModChar c
 
53
    c : cs | isUpper c && c /= largeChar -> ""
 
54
    _                                    -> [largeChar]
 
55
 
 
56
  largeChar  = 'Q'
 
57
  escapeChar = 'Z'
 
58
 
 
59
  isOK c = c /= escapeChar && isModChar c
53
60
 
54
61
  enc c | isOK c    = [c]
55
 
        | otherwise = "Z" ++ show (fromEnum c) ++ "Z"
 
62
        | otherwise = [escapeChar] ++ show (fromEnum c) ++ [escapeChar]
56
63
 
57
64
-- Note: This injectivity test is quite weak. A better, dedicated
58
65
-- generator could strengthen it.
63
70
   else
64
71
    True
65
72
 
66
 
prop_encodeModuleName_OK (M s) =
 
73
prop_encodeModuleName_OK (M s') =
67
74
  s ~= unM (encodeModuleName (Module s))
68
75
  where
 
76
  s = mazstr ++ "." ++ s'
 
77
 
69
78
  ""        ~= ""         = True
70
79
  ('.' : s) ~= ('.' : s') = s ~= s'
71
80
  s         ~= (c : s')   = isUpper c && all isModChar s1' &&
75
84
 
76
85
  unM (Module s) = s
77
86
 
 
87
prop_encodeModuleName_preserved (M m) =
 
88
  shouldBePreserved m ==>
 
89
    encodeModuleName (Module m) == Module m
 
90
  where
 
91
  shouldBePreserved m =
 
92
    not (m == mazstr || (mazstr ++ ".") `isPrefixOf` m)
 
93
 
78
94
-- | Agda module names. Used to test 'encodeModuleName'.
79
95
 
80
96
newtype M = M String deriving (Show)
85
101
    m <- vectorOf ms namePart
86
102
    return $ M (intercalate "." m)
87
103
    where
88
 
    namePart = do
89
 
      cs <- choose (1, 2)
90
 
      vectorOf cs (elements "a_AZ0'-∀")
 
104
    namePart =
 
105
      oneof [ return mazstr
 
106
            , do cs <- choose (1, 2)
 
107
                 vectorOf cs (elements "a_AQZ0'-∀")
 
108
            ]
91
109
 
92
110
------------------------------------------------------------------------
93
111
-- All tests
98
116
tests = runTests "Agda.Compiler.MAlonzo.Encode"
99
117
  [ quickCheck' prop_encodeModuleName_injective
100
118
  , quickCheck' prop_encodeModuleName_OK
 
119
  , quickCheck' prop_encodeModuleName_preserved
101
120
  ]