CurryCheck.curry 64.6 KB
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
-------------------------------------------------------------------------
--- This is the implementation of the currycheck tool.
--- It performs various checks on Curry programs:
---
--- * Correct usage of set functions, non-strict unification,
---   default rules, DET annotations, contracts
--- * All EasyCheck tests are extracted and checked
--- * For all functions declared as deterministic,
---   determinism properties are generated and checked.
--- * For functions with postconditions (f'post), checks for postconditions
---   are generated (together with possible preconditions)
--- * For functions with specification (f'spec), checks for satisfaction
---   of these specifications are generated
---   (together with possible preconditions).
---
--- @author Michael Hanus, Jan-Patrick Baye
17
--- @version October 2018
Michael Hanus 's avatar
Michael Hanus committed
18
19
20
-------------------------------------------------------------------------

import AnsiCodes
21
import Char                    ( toUpper )
Michael Hanus 's avatar
Michael Hanus committed
22
import Distribution
23
import FilePath                ( (</>), pathSeparator, takeDirectory )
Michael Hanus 's avatar
Michael Hanus committed
24
25
import GetOpt
import List
26
27
import Maybe                   ( fromJust, isJust )
import System                  ( system, exitWith, getArgs, getPID, getEnviron )
Michael Hanus 's avatar
Michael Hanus committed
28

29
30
31
32
import AbstractCurry.Types
import AbstractCurry.Files
import AbstractCurry.Select
import AbstractCurry.Build
Michael Hanus 's avatar
Michael Hanus committed
33
import qualified AbstractCurry.Pretty as ACPretty
34
35
import AbstractCurry.Transform ( renameCurryModule, trCTypeExpr
                               , updCProg, updQNamesInCProg )
36
import Analysis.Termination    ( Productivity(..) )
37
38
39
import qualified FlatCurry.Types as FC
import FlatCurry.Files
import qualified FlatCurry.Goodies as FCG
40
import Text.Pretty             ( pPrint )
41

42
43
import CC.AnalysisHelpers      ( getTerminationInfos, getProductivityInfos
                               , getUnsafeModuleInfos, dropPublicSuffix )
Michael Hanus 's avatar
Michael Hanus committed
44
45
import CC.Config               ( packagePath, packageVersion )
import CC.Options
46
import CheckDetUsage           ( checkDetUse, containsDetOperations)
Michael Hanus 's avatar
Michael Hanus committed
47
import ContractUsage
48
import DefaultRuleUsage        ( checkDefaultRules, containsDefaultRules )
Michael Hanus 's avatar
Michael Hanus committed
49
import PropertyUsage
50
import SimplifyPostConds       ( simplifyPostConditionsWithTheorems )
Michael Hanus 's avatar
Michael Hanus committed
51
import TheoremUsage
52
import UsageCheck              ( checkBlacklistUse, checkSetUse )
Michael Hanus 's avatar
Michael Hanus committed
53
54
55
56
57
58

-- Banner of this tool:
ccBanner :: String
ccBanner = unlines [bannerLine,bannerText,bannerLine]
 where
   bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++
59
                packageVersion ++ " of 08/10/2018)"
Michael Hanus 's avatar
Michael Hanus committed
60
61
62
63
   bannerLine = take (length bannerText) (repeat '-')

-- Help text
usageText :: String
Michael Hanus 's avatar
Michael Hanus committed
64
usageText = usageInfo ("Usage: curry-check [options] <module names>\n") options
Michael Hanus 's avatar
Michael Hanus committed
65

Michael Hanus 's avatar
Michael Hanus committed
66
67
68
--- Maximal arity of check functions and tuples currently supported:
maxArity :: Int
maxArity = 5
Michael Hanus 's avatar
Michael Hanus committed
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86

-------------------------------------------------------------------------
-- The names of suffixes added to specific tests.

defTypeSuffix :: String
defTypeSuffix = "_ON_BASETYPE"

postCondSuffix :: String
postCondSuffix = "SatisfiesPostCondition"

satSpecSuffix :: String
satSpecSuffix = "SatisfiesSpecification"

isDetSuffix :: String
isDetSuffix = "IsDeterministic"

-------------------------------------------------------------------------
-- Internal representation of tests extracted from a Curry module.
87
88
89
90
91
92
93
94
-- A test is
-- * a property test (with a name, type, source line number),
-- * an IO test (with a name and source line number), or
-- * an operation equivalence test (with a name, the names of both operations,
--   and their type, and the source line number).
data Test = PropTest  QName CTypeExpr Int
          | IOTest    QName Int
          | EquivTest QName QName QName CTypeExpr Int
Michael Hanus 's avatar
Michael Hanus committed
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

-- Is the test an IO test?
isIOTest :: Test -> Bool
isIOTest t = case t of IOTest _ _ -> True
                       _          -> False
-- Is the test a unit test?
isUnitTest :: Test -> Bool
isUnitTest t = case t of PropTest _ texp _ -> null (argTypes texp)
                         _                 -> False

-- Is the test a property test?
isPropTest :: Test -> Bool
isPropTest t = case t of PropTest _ texp _ -> not (null (argTypes texp))
                         _                 -> False

110
111
112
113
114
-- Is the test an equivalence test?
isEquivTest :: Test -> Bool
isEquivTest t = case t of EquivTest _ _ _ _ _ -> True
                          _                   -> False

115
116
117
118
119
-- Returns the names of the operations of an equivalence test.
equivTestOps :: Test -> [QName]
equivTestOps t = case t of EquivTest _ f1 f2 _ _ -> [f1,f2]
                           _                     -> []

Michael Hanus 's avatar
Michael Hanus committed
120
-- The name of a test:
121
122
123
124
testName :: Test -> QName
testName (PropTest  n _     _) = n
testName (IOTest    n       _) = n
testName (EquivTest n _ _ _ _) = n
Michael Hanus 's avatar
Michael Hanus committed
125
126

-- The line number of a test:
127
128
129
130
testLine :: Test -> Int
testLine (PropTest  _ _     n) = n
testLine (IOTest    _       n) = n
testLine (EquivTest _ _ _ _ n) = n
Michael Hanus 's avatar
Michael Hanus committed
131
132
133
134

-- Generates a useful error message for tests (with module and line number)
genTestMsg :: String -> Test -> String
genTestMsg file test =
135
136
137
138
139
140
141
142
  snd (testName test) ++
  " (module " ++ file ++ ", line " ++ show (testLine test) ++ ")"

-- Generates the name of a test in the main test module from the test name.
genTestName :: Test -> String
genTestName test =
  let (modName, fName) = testName test
  in fName ++ "_" ++ modNameToId modName
Michael Hanus 's avatar
Michael Hanus committed
143
144
145
146
147
148
149
150
151

-------------------------------------------------------------------------
-- Representation of the information about a module to be tested:
-- * the original name of the module to be tested
-- * the name of the transformed (public) test module
-- * static errors (e.g., illegal uses of set functions)
-- * test operations
-- * name of generators defined in this module (i.e., starting with "gen"
--   and of appropriate result type)
152
-- * the names of functions with preconditions defined in the test module
Michael Hanus 's avatar
Michael Hanus committed
153
154
155
156
157
158
data TestModule = TestModule
  { orgModuleName  :: String
  , testModuleName :: String
  , staticErrors   :: [String]
  , propTests      :: [Test]
  , generators     :: [QName]
159
  , preConditions  :: [QName]
Michael Hanus 's avatar
Michael Hanus committed
160
161
162
163
164
  }

-- A test module with only static errors.
staticErrorTestMod :: String -> [String] -> TestModule
staticErrorTestMod modname staterrs =
165
 TestModule modname modname staterrs [] [] []
Michael Hanus 's avatar
Michael Hanus committed
166
167
168
169
170
171

-- Is this a test module that should be tested?
testThisModule :: TestModule -> Bool
testThisModule tm = null (staticErrors tm) && not (null (propTests tm))

-- Extracts all user data types used as test data generators.
172
173
174
-- Each type has a flag which is `True` if the test data should contain
-- partial values (for checking equivalence of operations).
userTestDataOfModule :: TestModule -> [(QName,Bool)]
Michael Hanus 's avatar
Michael Hanus committed
175
176
177
userTestDataOfModule testmod = concatMap testDataOf (propTests testmod)
 where
  testDataOf (IOTest _ _) = []
178
179
180
181
182
183
184
185
186
187
188
189
190
  testDataOf (PropTest _ texp _) =
    map (\t -> (t,False)) (filter (\ (mn,_) -> mn /= preludeName)
                                  (unionOn tconsOf (argTypes texp)))
  testDataOf (EquivTest _ _ _ texp _) =
    map (\t -> (t,True)) (unionOn tconsOf (argTypes texp))

-- Extracts all result data types used in equivalence properties.
equivPropTypes :: TestModule -> [QName]
equivPropTypes testmod = concatMap equivTypesOf (propTests testmod)
 where
  equivTypesOf (IOTest _ _) = []
  equivTypesOf (PropTest _ _ _) = []
  equivTypesOf (EquivTest _ _ _ texp _) = tconsOf (resultType texp)
Michael Hanus 's avatar
Michael Hanus committed
191
192

-------------------------------------------------------------------------
193
194
-- Transform all tests of a module into operations that perform
-- appropriate calls to EasyCheck:
195
196
197
198
199
genTestFuncs :: Options -> (QName -> Bool) -> (QName -> Productivity) -> String
             -> TestModule -> IO [CFuncDecl]
genTestFuncs opts terminating productivity mainmod tm =
  liftM (filter (not . null . funcRules))
        (mapM genTestFunc (propTests tm))
Michael Hanus 's avatar
Michael Hanus committed
200
 where
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
  genTestFunc test = case test of
    PropTest  name t _       -> testFuncWithRules (propBody   name t test)
    IOTest    name   _       -> testFuncWithRules (ioTestBody name test)
    EquivTest name f1 f2 t _ ->
      -- if the test name has suffix "'TERMINATE" or the operations
      -- to be tested are terminating, the test for terminating
      -- operations is used:
      if "'TERMINATE" `isSuffixOf` map toUpper (snd name) ||
         (isTerminating f1 && isTerminating f2)
        then do putStrLnIfDebug opts $
                  "Generating equivalence test for TERMINATING " ++
                  "operations for test: " ++ snd name
                testFuncWithRules $ equivBodyTerm f1 f2 t test
        else
          -- if the test name has suffix "'PRODUCTIVE" or the
          -- operations to be tested are productive,
          -- the test for arbitrary operations is used
          -- (which limits the size of computed
          -- results but might find counter-examples later),
          -- otherwise the test is omitted if we are in the "safe"
          -- mode:
          if "'PRODUCTIVE" `isSuffixOf` map toUpper (snd name) ||
             optEquiv opts /= Safe ||
             (isProductive f1 && isProductive f2)
            then do putStrLnIfDebug opts $
                      "Generating equivalence test for PRODUCTIVE " ++
                      "operations for test: " ++ snd name
                    testFuncWithRules $ equivBodyAny f1 f2 t test
            else testFuncWithRules []
   where
     testFuncWithRules rs =
       return $ cfunc (mainmod, genTestName test) 0 Public
                      (emptyClassType (ioType (maybeType stringType))) rs
Michael Hanus 's avatar
Michael Hanus committed
234

235
236
237
238
  isTerminating f = terminating f || productivity f == Terminating
  
  isProductive f = productivity f `notElem` [NoInfo, Looping]
  
Michael Hanus 's avatar
Michael Hanus committed
239
240
241
  msgOf test = string2ac $ genTestMsg (orgModuleName tm) test

  testmname = testModuleName tm
Michael Hanus 's avatar
Michael Hanus committed
242

Michael Hanus 's avatar
Michael Hanus committed
243
244
245
246
247
248
  easyCheckFuncName arity =
    if arity>maxArity
    then error $ "Properties with more than " ++ show maxArity ++
                 " parameters are currently not supported!"
    else (easyCheckExecModule,"checkWithValues" ++ show arity)

249
250
  -- Operation equivalence test for terminating operations:
  equivBodyTerm f1 f2 texp test =
251
    let xvars = map (\i -> (i,"x"++show i)) [1 .. arityOfType texp]
252
253
        pvalOfFunc = ctype2pvalOf mainmod "pvalOf" (resultType texp)
    in propOrEquivBody (map (\t -> (t,True)) (argTypes texp)) test
254
         (cLambda (map CPVar xvars)
255
256
257
258
            (addPreCond (preConditions tm) [f1,f2] xvars
              (applyF (easyCheckModule,"<~>")
                      [applyE pvalOfFunc [applyF f1 (map CVar xvars)],
                       applyE pvalOfFunc [applyF f2 (map CVar xvars)]])))
259
260
261

  -- Operation equivalence test for arbitrary operations:
  equivBodyAny f1 f2 texp test =
262
263
    let xvars = map (\i -> (i,"x"++show i)) [1 .. arityOfType texp]
        pvar  = (2,"p")
264
265
266
267
268
        pvalOfFunc = ctype2pvalOf mainmod "peval" (resultType texp)
    in propOrEquivBody
         (map (\t -> (t,True)) (argTypes texp) ++
          [(ctype2BotType mainmod  (resultType texp), False)])
         test
269
         (CLambda (map CPVar xvars ++ [CPVar pvar])
270
271
272
273
            (addPreCond (preConditions tm) [f1,f2] xvars
              (applyF (easyCheckModule,"<~>")
                 [applyE pvalOfFunc [applyF f1 (map CVar xvars), CVar pvar],
                  applyE pvalOfFunc [applyF f2 (map CVar xvars), CVar pvar]])))
274
275
276
277
278
279

  propBody qname texp test =
    propOrEquivBody (map (\t -> (t,False)) (argTypes texp))
                    test (CSymbol (testmname,snd qname))

  propOrEquivBody argtypes test propexp =
Michael Hanus 's avatar
Michael Hanus committed
280
    [simpleRule [] $
281
282
283
284
      CLetDecl [CLocalPat (CPVar msgvar) (CSimpleRhs (msgOf test) [])]
               (applyF (easyCheckExecModule, "checkPropWithMsg")
                 [ CVar msgvar
                 , applyF (easyCheckFuncName (length argtypes)) $
Michael Hanus 's avatar
Michael Hanus committed
285
                    [configOpWithMaxFail, CVar msgvar] ++
286
                    (map (\ (t,genpart) ->
Michael Hanus 's avatar
Michael Hanus committed
287
288
                          applyF (easyCheckModule,"valuesOfSearchTree")
                            [if isPAKCS || useUserDefinedGen t || isFloatType t
289
                             then type2genop mainmod tm genpart t
Michael Hanus 's avatar
Michael Hanus committed
290
291
292
                             else applyF (searchTreeModule,"someSearchTree")
                                         [constF (pre "unknown")]])
                         argtypes) ++
293
294
                    [propexp]
                 ])]
Michael Hanus 's avatar
Michael Hanus committed
295
296
   where
    useUserDefinedGen texp = case texp of
Michael Hanus 's avatar
Michael Hanus committed
297
      CTVar _       -> error "No polymorphic generator!"
298
299
      CFuncType _ _ -> error $ "No generator for functional types:\n" ++
                               showCTypeExpr texp
Michael Hanus 's avatar
Michael Hanus committed
300
301
302
303
304
305
306
      CTApply _ _   ->
        maybe (error "No generator for type applications!")
              (\ ((_,tc),_) -> isJust
                         (find (\qn -> "gen"++tc == snd qn) (generators tm)))
              (tconsArgsOfType texp)
      CTCons (_,tc) -> isJust
                         (find (\qn -> "gen"++tc == snd qn) (generators tm))
Michael Hanus 's avatar
Michael Hanus committed
307
308
309
310
311
312

    configOpWithMaxTest =
      let n = optMaxTest opts
       in if n==0 then stdConfigOp
                  else applyF (easyCheckExecModule,"setMaxTest")
                              [cInt n, stdConfigOp]
Michael Hanus 's avatar
Michael Hanus committed
313

Michael Hanus 's avatar
Michael Hanus committed
314
315
316
317
318
    configOpWithMaxFail =
      let n = optMaxFail opts
       in if n==0 then configOpWithMaxTest
                  else applyF (easyCheckExecModule,"setMaxFail")
                              [cInt n, configOpWithMaxTest]
Michael Hanus 's avatar
Michael Hanus committed
319

Michael Hanus 's avatar
Michael Hanus committed
320
    msgvar = (0,"msg")
Michael Hanus 's avatar
Michael Hanus committed
321

Michael Hanus 's avatar
Michael Hanus committed
322
  stdConfigOp = constF (easyCheckConfig opts)
Michael Hanus 's avatar
Michael Hanus committed
323

Michael Hanus 's avatar
Michael Hanus committed
324
325
326
327
328
329
330
331
332
333
334
335
336
  ioTestBody (_, name) test =
    [simpleRule [] $ applyF (easyCheckExecModule,"checkPropIOWithMsg")
                            [stdConfigOp, msgOf test, CSymbol (testmname,name)]]

-- The configuration option for EasyCheck
easyCheckConfig :: Options -> QName
easyCheckConfig opts =
  (easyCheckExecModule,
   if isQuiet opts     then "quietConfig"   else
   if optVerb opts > 2 then "verboseConfig"
                       else "easyConfig")

-- Translates a type expression into calls to generator operations.
337
338
339
340
341
342
343
344
-- If the third argument is `True`, calls to partial generators are used.
type2genop :: String -> TestModule -> Bool -> CTypeExpr -> CExpr
type2genop _ _ _ (CTVar _)       = error "No polymorphic generator!"
type2genop _ _ _ te@(CFuncType _ _) =
  error $ "No generator for functional types:\n" ++ showCTypeExpr te
type2genop mainmod tm genpart (CTCons qt) =
  constF (typename2genopname mainmod (generators tm) genpart qt)
type2genop mainmod tm genpart te@(CTApply _ _) =
Michael Hanus 's avatar
Michael Hanus committed
345
  maybe (error "No generator for type applications!")
346
347
348
        (\ (qt,targs) ->
           applyF (typename2genopname mainmod (generators tm) genpart qt)
                  (map (type2genop mainmod tm genpart) targs))
Michael Hanus 's avatar
Michael Hanus committed
349
        (tconsArgsOfType te)
Michael Hanus 's avatar
Michael Hanus committed
350
351

isFloatType :: CTypeExpr -> Bool
Michael Hanus 's avatar
Michael Hanus committed
352
353
isFloatType texp = case texp of CTCons tc -> tc == (preludeName,"Float")
                                _         -> False
Michael Hanus 's avatar
Michael Hanus committed
354

355
356
357
358
359
360
361
362
363
-- Translates the name of a type constructor into the name of the
-- generator operation for values of this type.
-- The first argument is the name of the main module.
-- The second argument contains the user-defined generator operations.
-- If the third argument is `True`, generators for partial values are used.
typename2genopname :: String -> [QName] -> Bool -> QName -> QName
typename2genopname mainmod definedgenops genpart (mn,tc)
  | genpart  -- we use our own generator for partial values:
  = (mainmod, "gen_" ++ modNameToId mn ++ "_" ++ transQN tc ++ "_PARTIAL")
Michael Hanus 's avatar
Michael Hanus committed
364
365
  | isJust maybeuserdefined -- take user-defined generator:
  = fromJust maybeuserdefined
366
367
  | mn==preludeName
  = (generatorModule, "gen" ++ transQN tc)
Michael Hanus 's avatar
Michael Hanus committed
368
  | otherwise -- we use our own generator:
369
370
  = (mainmod, "gen_" ++ modNameToId mn ++ "_" ++ transQN tc ++
              if genpart then "_PARTIAL" else "")
Michael Hanus 's avatar
Michael Hanus committed
371
372
 where
  maybeuserdefined = find (\qn -> "gen"++tc == snd qn) definedgenops
Michael Hanus 's avatar
Michael Hanus committed
373

374
375
376
377
378
379
380
381
382
383
384
-- Transform a qualified (typ) constructor name into a name
-- with alpha-numeric characters.
transQN :: String -> String
transQN tcons | tcons == "[]"     = "List"
              | tcons == ":"      = "Cons"
              | tcons == "()"     = "Unit"
              | tcons == "(,)"    = "Pair"
              | tcons == "(,,)"   = "Triple"
              | tcons == "(,,,)"  = "Tuple4"
              | tcons == "(,,,,)" = "Tuple5"
              | otherwise         = tcons
Michael Hanus 's avatar
Michael Hanus committed
385
386
387
388
389

-------------------------------------------------------------------------
-- Turn all functions into public ones.
-- This ensures that all tests can be executed.
makeAllPublic :: CurryProg -> CurryProg
Michael Hanus 's avatar
Michael Hanus committed
390
391
392
393
makeAllPublic (CurryProg modname imports dfltdecl clsdecls instdecls
                         typedecls functions opdecls) =
  CurryProg modname stimports dfltdecl clsdecls instdecls
            typedecls publicFunctions opdecls
Michael Hanus 's avatar
Michael Hanus committed
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
 where
  stimports = if generatorModule `elem` imports &&
                 searchTreeModule `notElem` imports
              then searchTreeModule : imports -- just to be safe if module
                                              -- contains generator definitions
              else imports

  publicFunctions = map makePublic $ map ignoreComment functions

  -- since we create a copy of the module, we can ignore unnecessary data
  ignoreComment :: CFuncDecl -> CFuncDecl
  ignoreComment (CmtFunc _ name arity visibility typeExpr rules) =
    CFunc name arity visibility typeExpr rules
  ignoreComment x@(CFunc      _     _          _        _     _) = x

  makePublic :: CFuncDecl -> CFuncDecl
  makePublic (CFunc name arity _      typeExpr rules) =
              CFunc name arity Public typeExpr rules
  makePublic (CmtFunc cmt name arity _      typeExpr rules) =
              CmtFunc cmt name arity Public typeExpr rules

415
416
417
418
419
420
421
422
423
-- Classify the test represented by a function declaration
-- as either PropTest or IOTest.
classifyTest :: Options -> CurryProg -> CFuncDecl -> Test
classifyTest opts prog test =
  if isPropIOType (typeOfQualType (funcType test))
    then IOTest tname 0
    else maybe (PropTest tname (typeOfQualType (funcType test)) 0)
               expsToEquivTest
               (isEquivProperty test)
Michael Hanus 's avatar
Michael Hanus committed
424
 where
425
426
427
428
429
430
431
432
433
434
435
436
437
  tname = funcName test

  expsToEquivTest exps = case exps of
    (CSymbol f1,CSymbol f2) ->
      EquivTest tname f1 f2 (defaultingType (funcTypeOf f1)) 0
    (CTyped (CSymbol f1) qtexp, CSymbol f2) ->
      EquivTest tname f1 f2 (defaultingType qtexp) 0
    (CSymbol f1, CTyped (CSymbol f2) qtexp) ->
      EquivTest tname f1 f2 (defaultingType qtexp) 0
    (CTyped (CSymbol f1) qtexp, CTyped (CSymbol f2) _) ->
      EquivTest tname f1 f2 (defaultingType qtexp) 0
    (e1,e2) -> error $ "Illegal equivalence property:\n" ++
                       showCExpr e1 ++ " <=> " ++ showCExpr e2
438

Michael Hanus 's avatar
Michael Hanus committed
439
  defaultingType = poly2defaultType opts . typeOfQualType . defaultQualType
440
441
442
443
  
  funcTypeOf f = maybe (error $ "Cannot find type of " ++ show f ++ "!")
                       funcType
                       (find (\fd -> funcName fd == f) (functions prog))
Michael Hanus 's avatar
Michael Hanus committed
444
445
446

-- Extracts all tests from a given Curry module and transforms
-- all polymorphic tests into tests on a base type.
447
448
449
450
-- The result contains a tuple consisting of all actual tests,
-- all ignored tests, the name of all operations with defined preconditions
-- (needed to generate meaningful equivalence tests),
-- and the public version of the original module.
Michael Hanus 's avatar
Michael Hanus committed
451
transformTests :: Options -> String -> CurryProg
452
               -> IO ([CFuncDecl],[CFuncDecl],[QName],CurryProg)
Michael Hanus 's avatar
Michael Hanus committed
453
transformTests opts srcdir
Michael Hanus 's avatar
Michael Hanus committed
454
455
               prog@(CurryProg mname imps dfltdecl clsdecls instdecls
                               typeDecls functions opDecls) = do
Michael Hanus 's avatar
Michael Hanus committed
456
457
458
459
460
461
462
463
464
465
466
  theofuncs <- if optProof opts then getTheoremFunctions srcdir prog
                                else return []
  simpfuncs <- simplifyPostConditionsWithTheorems (optVerb opts) theofuncs funcs
  let preCondOps  = preCondOperations simpfuncs
      postCondOps = map ((\ (mn,fn) -> (mn, fromPostCondName fn)) . funcName)
                        (funDeclsWith isPostCondName simpfuncs)
      specOps     = map ((\ (mn,fn) -> (mn, fromSpecName fn)) . funcName)
                        (funDeclsWith isSpecName simpfuncs)
      -- generate post condition tests:
      postCondTests = concatMap (genPostCondTest preCondOps postCondOps) funcs
      -- generate specification tests:
467
468
      specOpTests   = concatMap (genSpecTest opts preCondOps specOps) funcs
      grSpecOpTests = if optEquiv opts == Ground then specOpTests else []
Michael Hanus 's avatar
Michael Hanus committed
469
470
471
472

      (realtests,ignoredtests) = partition fst $
        if not (optProp opts)
        then []
Michael Hanus 's avatar
Michael Hanus committed
473
        else concatMap (poly2default opts) $
Michael Hanus 's avatar
Michael Hanus committed
474
475
476
               -- ignore already proved properties:
               filter (\fd -> funcName fd `notElem` map funcName theofuncs)
                      usertests ++
477
478
479
               (if optSpec opts then grSpecOpTests ++ postCondTests else [])
  return (map snd realtests ++
          (if optSpec opts && optEquiv opts /= Ground then specOpTests else []),
Michael Hanus 's avatar
Michael Hanus committed
480
          map snd ignoredtests,
481
          preCondOps,
Michael Hanus 's avatar
Michael Hanus committed
482
483
          CurryProg mname
                    (nub (easyCheckModule:imps))
Michael Hanus 's avatar
Michael Hanus committed
484
                    dfltdecl clsdecls instdecls
Michael Hanus 's avatar
Michael Hanus committed
485
486
487
488
                    typeDecls
                    (simpfuncs ++ map snd (realtests ++ ignoredtests))
                    opDecls)
 where
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
  (rawusertests, funcs) = partition isProperty functions

  usertests = if optEquiv opts == Ground
                then map equivProp2Ground rawusertests
                else rawusertests

  -- transform an equivalence property (f1 <=> f2) into a property
  -- testing ground equivalence, i.e., f1 x1...xn <~> f2 x1...xn
  equivProp2Ground fdecl =
    maybe fdecl
          (\ _ -> case classifyTest opts prog fdecl of
            EquivTest _ f1 f2 texp _ ->
             let ar    = arityOfType texp
                 cvars = map (\i -> (i,"x"++show i)) [1 .. ar]
             in stFunc (funcName fdecl) ar Public (propResultType texp)
                  [simpleRule (map CPVar cvars)
                              (applyF (easyCheckModule,"<~>")
                                      [applyF f1 (map CVar cvars),
                                       applyF f2 (map CVar cvars)])]
            _ -> error "transformTests: internal error"
          )
          (isEquivProperty fdecl)
Michael Hanus 's avatar
Michael Hanus committed
511
512
513
514
515
516
517
518
519
520

-- Extracts all determinism tests from a given Curry module and
-- transforms deterministic operations back into non-deterministic operations
-- in order to test their determinism property.
-- The result contains a triple consisting of all actual determinism tests,
-- all ignored tests (since they are polymorphic), and the public version
-- of the transformed original module.
transformDetTests :: Options -> [String] -> CurryProg
                  -> ([CFuncDecl],[CFuncDecl],CurryProg)
transformDetTests opts prooffiles
Michael Hanus 's avatar
Michael Hanus committed
521
522
                  (CurryProg mname imports dfltdecl clsdecls instdecls
                             typeDecls functions opDecls) =
Michael Hanus 's avatar
Michael Hanus committed
523
524
525
  (map snd realtests, map snd ignoredtests,
   CurryProg mname
             (nub (easyCheckModule:imports))
Michael Hanus 's avatar
Michael Hanus committed
526
             dfltdecl clsdecls instdecls
Michael Hanus 's avatar
Michael Hanus committed
527
528
529
530
531
532
             typeDecls
             (map (revertDetOpTrans detOpNames) functions ++
              map snd (realtests ++ ignoredtests))
             opDecls)
 where
  preCondOps = preCondOperations functions
Michael Hanus 's avatar
Michael Hanus committed
533

Michael Hanus 's avatar
Michael Hanus committed
534
535
536
537
538
539
540
541
542
543
544
  -- generate determinism tests:
  detOpTests = genDetOpTests prooffiles preCondOps functions

  -- names of deterministic operations:
  detOpNames = map (stripIsDet . funcName) detOpTests

  stripIsDet (mn,fn) = (mn, take (length fn -15) fn)

  (realtests,ignoredtests) = partition fst $
    if not (optProp opts)
    then []
Michael Hanus 's avatar
Michael Hanus committed
545
    else concatMap (poly2default opts)
Michael Hanus 's avatar
Michael Hanus committed
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
                   (if optDet opts then detOpTests else [])

-- Get all operations with a defined precondition from a list of functions.
preCondOperations :: [CFuncDecl] -> [QName]
preCondOperations fdecls =
  map ((\ (mn,fn) -> (mn,fromPreCondName fn)) . funcName)
      (funDeclsWith isPreCondName fdecls)

-- Filter functions having a name satisfying a given predicate.
funDeclsWith :: (String -> Bool) -> [CFuncDecl] -> [CFuncDecl]
funDeclsWith pred = filter (pred . snd . funcName)

-- Transforms a function type into a property type, i.e.,
-- t1 -> ... -> tn -> t  is transformed into  t1 -> ... -> tn -> Prop
propResultType :: CTypeExpr -> CTypeExpr
propResultType te = case te of
  CFuncType from to -> CFuncType from (propResultType to)
  _                 -> baseType (easyCheckModule,"Prop")

-- Transforms a function declaration into a post condition test if
-- there is a post condition for this function (i.e., a relation named
-- f'post). The post condition test is of the form
-- fSatisfiesPostCondition x1...xn y = always (f'post x1...xn (f x1...xn))
genPostCondTest :: [QName] -> [QName] -> CFuncDecl -> [CFuncDecl]
genPostCondTest prefuns postops (CmtFunc _ qf ar vis texp rules) =
571
  genPostCondTest prefuns postops (CFunc qf ar vis texp rules)
Michael Hanus 's avatar
Michael Hanus committed
572
573
genPostCondTest prefuns postops
                (CFunc qf@(mn,fn) _ _ (CQualType clscon texp) _) =
Michael Hanus 's avatar
Michael Hanus committed
574
575
 if qf `notElem` postops then [] else
  [CFunc (mn, fn ++ postCondSuffix) ar Public
Michael Hanus 's avatar
Michael Hanus committed
576
    (CQualType clscon (propResultType texp))
Michael Hanus 's avatar
Michael Hanus committed
577
    [simpleRule (map CPVar cvars) $
578
       addPreCond prefuns [qf] cvars postprop ]]
Michael Hanus 's avatar
Michael Hanus committed
579
580
581
582
583
584
585
586
587
588
 where
  ar       = arityOfType texp
  cvars    = map (\i -> (i,"x"++show i)) [1 .. ar]
  rcall    = applyF qf (map CVar cvars)
  postprop = applyF (easyCheckModule,"always")
                    [applyF (mn,toPostCondName fn)
                            (map CVar cvars ++ [rcall])]

-- Transforms a function declaration into a specification test if
-- there is a specification for this function (i.e., an operation named
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
-- f'spec). The generated specification test has the form
--     fSatisfiesSpecification = f <=> f'spec
genSpecTest :: Options -> [QName] -> [QName] -> CFuncDecl -> [CFuncDecl]
genSpecTest opts prefuns specops (CmtFunc _ qf ar vis texp rules) =
  genSpecTest opts prefuns specops (CFunc qf ar vis texp rules)
genSpecTest opts prefuns specops
            (CFunc qf@(mn,fn) _ _ (CQualType clscon texp) _)
 | qf `notElem` specops
 = []
 | optEquiv opts == Ground
 = [genSpecGroundEquivTest prefuns qf clscon texp]
 | otherwise
 = [CFunc (mn, fn ++ satSpecSuffix) 0 Public
          (emptyClassType (propResultType unitType))
          [simpleRule [] (applyF (easyCheckModule,"<=>")
                                 [constF qf, constF (mn,toSpecName fn)])]]

-- Transforms a function declaration into a ground equivalence test
-- against the specification (i.e., an operation named `f'spec` exists).
-- The generated specification test is of the form
Michael Hanus 's avatar
Michael Hanus committed
609
610
-- fSatisfiesSpecification x1...xn =
--   f'pre x1...xn  ==> (f x1...xn <~> f'spec x1...xn)
611
612
613
genSpecGroundEquivTest :: [QName] -> QName -> CContext -> CTypeExpr -> CFuncDecl
genSpecGroundEquivTest prefuns qf@(mn,fn) clscon texp =
  CFunc (mn, fn ++ satSpecSuffix) ar Public
Michael Hanus 's avatar
Michael Hanus committed
614
    (CQualType (addShowContext clscon) (propResultType texp))
Michael Hanus 's avatar
Michael Hanus committed
615
    [simpleRule (map CPVar cvars) $
616
617
618
619
       addPreCond prefuns [qf,qfspec] cvars
         (applyF (easyCheckModule,"<~>")
                 [applyF qf (map CVar cvars),
                  applyF (mn,toSpecName fn) (map CVar cvars)])]
Michael Hanus 's avatar
Michael Hanus committed
620
 where
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
  ar     = arityOfType texp
  cvars  = map (\i -> (i,"x"++show i)) [1 .. ar]
  qfspec = (mn, toSpecName fn)

-- Adds the preconditions of operations (second argument), if they are
-- present in the list of functions with preconditions in the first argument,
-- on the given variables to the property expression `propexp`.
addPreCond :: [QName] -> [QName] -> [CVarIName] -> CExpr -> CExpr
addPreCond prefuns fs pvars propexp =
 let preconds = concatMap precondCall fs
 in if null preconds
      then propexp
      else applyF (easyCheckModule,"==>")
                  [foldr1 (\x y -> applyF (pre "&&") [x,y]) preconds, propexp]
 where
  precondCall qn@(mn,fn) =
    if qn `elem` prefuns
      then [applyF (mn, toPreCondName fn) (map CVar pvars)]
      else []
Michael Hanus 's avatar
Michael Hanus committed
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669

-- Revert the transformation for deterministic operations performed
-- by currypp, i.e., replace rule "f x = selectValue (set f_ORGNDFUN x)"
-- with "f = f_ORGNDFUN".
revertDetOpTrans :: [QName] -> CFuncDecl -> CFuncDecl
revertDetOpTrans  detops (CmtFunc _ qf ar vis texp rules) =
  revertDetOpTrans detops (CFunc qf ar vis texp rules)
revertDetOpTrans detops fdecl@(CFunc qf@(mn,fn) ar vis texp _) =
  if qf `elem` detops
  then CFunc qf ar vis texp [simpleRule [] (constF (mn,fn++"_ORGNDFUN"))]
  else fdecl

-- Look for operations named f_ORGNDFUN and create a determinism property
-- for f.
genDetOpTests :: [String] -> [QName] -> [CFuncDecl] -> [CFuncDecl]
genDetOpTests prooffiles prefuns fdecls =
  map (genDetProp prefuns) (filter isDetOrgOp fdecls)
 where
  isDetOrgOp fdecl =
   let fn = snd (funcName fdecl)
    in "_ORGNDFUN" `isSuffixOf` fn &&
       not (existsProofFor (determinismTheoremFor (take (length fn - 9) fn))
                           prooffiles)

-- Transforms a declaration of a deterministic operation f_ORGNDFUN
-- into a determinisim property test of the form
-- fIsDeterministic x1...xn = f x1...xn #< 2
genDetProp :: [QName] -> CFuncDecl -> CFuncDecl
genDetProp prefuns (CmtFunc _ qf ar vis texp rules) =
  genDetProp prefuns (CFunc qf ar vis texp rules)
Michael Hanus 's avatar
Michael Hanus committed
670
genDetProp prefuns (CFunc (mn,fn) ar _ (CQualType clscon texp) _) =
Michael Hanus 's avatar
Michael Hanus committed
671
  CFunc (mn, forg ++ isDetSuffix) ar Public
Michael Hanus 's avatar
Michael Hanus committed
672
   (CQualType (addShowContext clscon) (propResultType texp))
Michael Hanus 's avatar
Michael Hanus committed
673
   [simpleRule (map CPVar cvars) $
674
      addPreCond prefuns [(mn,forg)] cvars rnumcall ]
Michael Hanus 's avatar
Michael Hanus committed
675
676
677
678
679
680
681
682
 where
  forg     = take (length fn - 9) fn
  cvars    = map (\i -> (i,"x"++show i)) [1 .. ar]
  forgcall = applyF (mn,forg) (map CVar cvars)
  rnumcall = applyF (easyCheckModule,"#<") [forgcall, cInt 2]

-- Generates auxiliary (base-type instantiated) test functions for
-- polymorphically typed test function.
Michael Hanus 's avatar
Michael Hanus committed
683
684
-- The returned flag indicates whether the test function should actually
-- be passed to the test tool.
685
686
-- For instance, polymorphic proprerties are not tested, but only
-- their type-instantiated variants.
Michael Hanus 's avatar
Michael Hanus committed
687
688
689
690
poly2default :: Options -> CFuncDecl -> [(Bool,CFuncDecl)]
poly2default opts (CmtFunc _ name arity vis ftype rules) =
  poly2default opts (CFunc name arity vis ftype rules)
poly2default opts fdecl@(CFunc (mn,fname) arity vis qftype rs)
Michael Hanus 's avatar
Michael Hanus committed
691
692
  | isPolyType ftype
  = [(False,fdecl)
Michael Hanus 's avatar
Michael Hanus committed
693
    ,(True, CFunc (mn,fname++defTypeSuffix) arity vis
Michael Hanus 's avatar
Michael Hanus committed
694
                  (emptyClassType (poly2defaultType opts ftype))
Michael Hanus 's avatar
Michael Hanus committed
695
                  [simpleRule [] (applyF (mn,fname) [])])
Michael Hanus 's avatar
Michael Hanus committed
696
697
    ]
  | otherwise
Michael Hanus 's avatar
Michael Hanus committed
698
  = [(True, CFunc (mn,fname) arity vis (CQualType clscon ftype) rs)]
Michael Hanus 's avatar
Michael Hanus committed
699
 where
Michael Hanus 's avatar
Michael Hanus committed
700
  CQualType clscon ftype = defaultQualType qftype
Michael Hanus 's avatar
Michael Hanus committed
701

Michael Hanus 's avatar
Michael Hanus committed
702
703
poly2defaultType :: Options -> CTypeExpr -> CTypeExpr
poly2defaultType opts texp = p2dt texp 
704
 where
Michael Hanus 's avatar
Michael Hanus committed
705
  p2dt (CTVar _)         = baseType (pre (optDefType opts))
Michael Hanus 's avatar
Michael Hanus committed
706
  p2dt (CFuncType t1 t2) = CFuncType (p2dt t1) (p2dt t2)
Michael Hanus 's avatar
Michael Hanus committed
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
  p2dt (CTApply t1 t2)   = CTApply (p2dt t1) (p2dt t2)
  p2dt (CTCons ct)       = CTCons ct

-------------------------------------------------------------------------
-- Try to default a qualified type by replacing Num/Integral-constrained
-- types by Int and Fractional-constrained types by Float.
defaultQualType :: CQualTypeExpr -> CQualTypeExpr
defaultQualType (CQualType (CContext allclscon) ftype) =
  CQualType (CContext deffractxt) deffratype
 where
  (numcons,nonnumcons) =
    partition (\ (cls,te) -> (cls == pre "Num" || cls == pre "Integral")
                             && isTVar te)
              allclscon
  defnumtype = def2TConsInType numcons (pre "Int") ftype
  defnumctxt = removeNonTVarClassContexts
                 (map (\ (cls,con) ->
                                (cls, def2TConsInType numcons (pre "Int") con))
                      nonnumcons)

  (fracons,nonfracons) =
    partition (\ (cls,te) -> cls == pre "Fractional" && isTVar te) defnumctxt
  deffratype = def2TConsInType fracons (pre "Float") defnumtype
  deffractxt = removeNonTVarClassContexts
                 (map (\ (cls,con) ->
                              (cls, def2TConsInType fracons (pre "Float") con))
                      nonfracons)

  -- remove constant type class contexts
  removeNonTVarClassContexts = filter (\ (_,te) -> isTVar te)

  -- replace all type variables (occurring in the first list of class
  -- constraints) by the type constructor (second argument) in a given
  -- type expression (third argument)
  def2TConsInType clscons tcons texp =
    foldr (tvar2TCons tcons) texp (map snd clscons)

  -- substitute a type variable by type Int in a type
  tvar2TCons tcons texp = case texp of
    CTVar tv -> substTVar tv (CTCons tcons)
    _        -> id

  -- substitute a type variable by a type expression in a type expression:
  substTVar tvariname texp =
    trCTypeExpr (\tv -> if tv==tvariname then texp else CTVar tv)
                CTCons CFuncType CTApply

  isTVar te = case te of CTVar _ -> True
                         _       -> False

-- Add a "Show" class context to all types occurring in the context.
addShowContext :: CContext -> CContext
addShowContext (CContext clscons) =
  CContext (nub (clscons ++ (map (\t -> (pre "Show",t)) (map snd clscons))))

-------------------------------------------------------------------------
Michael Hanus 's avatar
Michael Hanus committed
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799

-- Transforms a possibly changed test name (like "test_ON_BASETYPE")
-- back to its original name.
orgTestName :: QName -> QName
orgTestName (mn,tname)
  | defTypeSuffix `isSuffixOf` tname
  = orgTestName (mn, stripSuffix tname defTypeSuffix)
  | isDetSuffix `isSuffixOf` tname
  = orgTestName (mn, take (length tname - 15) tname)
  | postCondSuffix `isSuffixOf` tname
  = orgTestName (mn, stripSuffix tname postCondSuffix)
  | satSpecSuffix `isSuffixOf` tname
  = orgTestName (mn, stripSuffix tname satSpecSuffix)
  | otherwise = (mn,tname)

-- This function implements the first phase of CurryCheck: it analyses
-- a module to be checked, i.e., it finds the tests, creates new tests
-- (e.g., for polymorphic properties, deterministic functions, post
-- conditions, specifications)
-- and generates a copy of the module appropriate for the main operation
-- of CurryCheck (e.g., all operations are made public).
-- If there are determinism tests, it also generates a second copy
-- where all deterministic functions are defined as non-deterministic
-- so that these definitions are tested.
analyseModule :: Options -> String -> IO [TestModule]
analyseModule opts modname = do
  putStrIfNormal opts $ withColor opts blue $
                        "Analyzing module '" ++ modname ++ "'...\n"
  catch (readCurryWithParseOptions modname (setQuiet True defaultParams) >>=
         analyseCurryProg opts modname)
        (\_ -> return [staticErrorTestMod modname
                         ["Module '"++modname++"': incorrect source program"]])

-- Analyse a Curry module for static errors:
staticProgAnalysis :: Options -> String -> String -> CurryProg
                   -> IO ([String],[(QName,String)])
staticProgAnalysis opts modname progtxt prog = do
800
  putStrIfDetails opts "Checking source code for static errors...\n"
Michael Hanus 's avatar
Michael Hanus committed
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
  useerrs <- if optSource opts then checkBlacklistUse prog else return []
  seterrs <- if optSource opts then readFlatCurry modname >>= checkSetUse
                               else return []
  let defruleerrs = if optSource opts then checkDefaultRules prog else []
  untypedprog <- readUntypedCurry modname
  let detuseerrs   = if optSource opts then checkDetUse untypedprog else []
      contracterrs = checkContractUse prog
      staticerrs = concat [seterrs,useerrs,defruleerrs,detuseerrs,contracterrs]
      missingCPP =
       if (containsDefaultRules prog || containsDetOperations untypedprog)
          && not (containsPPOptionLine progtxt)
       then ["'" ++ modname ++
           "' uses default rules or det. operations but not the preprocessor!",
           "Hint: insert line: {-# OPTIONS_CYMAKE -F --pgmF=currypp #-}"]
       else []
  return (missingCPP,staticerrs)

-- Analyse a Curry module and generate property tests:
analyseCurryProg :: Options -> String -> CurryProg -> IO [TestModule]
analyseCurryProg opts modname orgprog = do
  -- First we rename all references to Test.Prop into Test.EasyCheck
  let prog = renameProp2EasyCheck orgprog
  (topdir,srcfilename) <- lookupModuleSourceInLoadPath modname >>=
        return .
        maybe (error $ "Source file of module '"++modname++"' not found!") id
  let srcdir = takeDirectory srcfilename
827
  putStrLnIfDebug opts $ "Source file: " ++ srcfilename
Michael Hanus 's avatar
Michael Hanus committed
828
  prooffiles <- if optProof opts then getProofFiles srcdir else return []
829
  unless (null prooffiles) $ putStrIfDetails opts $
Michael Hanus 's avatar
Michael Hanus committed
830
831
832
833
834
    unlines ("Proof files found:" : map ("- " ++) prooffiles)
  progtxt <- readFile srcfilename
  (missingCPP,staticoperrs) <- staticProgAnalysis opts modname progtxt prog
  let words      = map firstWord (lines progtxt)
      staticerrs = missingCPP ++ map (showOpError words) staticoperrs
835
  putStrIfDetails opts "Generating property tests...\n"
836
  (rawTests,ignoredTests,preCondOps,pubmod) <-
Michael Hanus 's avatar
Michael Hanus committed
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
        transformTests opts srcdir . renameCurryModule (modname++"_PUBLIC")
                                   . makeAllPublic $ prog
  let (rawDetTests,ignoredDetTests,pubdetmod) =
        transformDetTests opts prooffiles
              . renameCurryModule (modname++"_PUBLICDET")
              . makeAllPublic $ prog
  unless (not (null staticerrs) || null rawTests && null rawDetTests) $
    putStrIfNormal opts $
      "Properties to be tested:\n" ++
      unwords (map (snd . funcName) (rawTests++rawDetTests)) ++ "\n"
  unless (not (null staticerrs) || null ignoredTests && null ignoredDetTests) $
    putStrIfNormal opts $
      "Properties ignored for testing:\n" ++
      unwords (map (snd . funcName) (ignoredTests++ignoredDetTests)) ++ "\n"
  let tm    = TestModule modname
                         (progName pubmod)
                         staticerrs
854
                         (addLinesNumbers words
855
                            (map (classifyTest opts pubmod) rawTests))
Michael Hanus 's avatar
Michael Hanus committed
856
                         (generatorsOfProg pubmod)
857
                         preCondOps
Michael Hanus 's avatar
Michael Hanus committed
858
859
860
      dettm = TestModule modname
                         (progName pubdetmod)
                         []
861
                         (addLinesNumbers words
862
                            (map (classifyTest opts pubdetmod) rawDetTests))
Michael Hanus 's avatar
Michael Hanus committed
863
                         (generatorsOfProg pubmod)
864
                         []
Michael Hanus 's avatar
Michael Hanus committed
865
866
867
868
869
870
871
872
873
874
875
  when (testThisModule tm) $ writeCurryProgram opts topdir pubmod ""
  when (testThisModule dettm) $ writeCurryProgram opts topdir pubdetmod ""
  return (if testThisModule dettm then [tm,dettm] else [tm])
 where
  showOpError words (qf,err) =
    snd qf ++ " (module " ++ modname ++ ", line " ++
    show (getLineNumber words qf) ++"): " ++ err

  addLinesNumbers words = map (addLineNumber words)

  addLineNumber :: [String] -> Test -> Test
876
  addLineNumber words (PropTest name texp _) =
Michael Hanus 's avatar
Michael Hanus committed
877
878
879
    PropTest   name texp $ getLineNumber words (orgTestName name)
  addLineNumber words (IOTest name _) =
    IOTest name $ getLineNumber words (orgTestName name)
880
881
  addLineNumber words (EquivTest name f1 f2 texp _) =
    EquivTest name f1 f2 texp $ getLineNumber words (orgTestName name)
Michael Hanus 's avatar
Michael Hanus committed
882
883
884
885
886
887
888
889
890

  getLineNumber :: [String] -> QName -> Int
  getLineNumber words (_, name) = maybe 0 (+1) (elemIndex name words)

-- Extracts all user-defined defined generators defined in a module.
generatorsOfProg :: CurryProg -> [QName]
generatorsOfProg = map funcName . filter isGen . functions
 where
   isGen fdecl = "gen" `isPrefixOf` snd (funcName fdecl) &&
Michael Hanus 's avatar
Michael Hanus committed
891
                 isSearchTreeType (resultType (typeOfQualType (funcType fdecl)))
Michael Hanus 's avatar
Michael Hanus committed
892

893
   isSearchTreeType (CTVar _)       = False
Michael Hanus 's avatar
Michael Hanus committed
894
   isSearchTreeType (CFuncType _ _) = False
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
   isSearchTreeType (CTCons _)       = False
   isSearchTreeType te@(CTApply _ _) =
     maybe False ((==searchTreeTC) . fst) (tconsArgsOfType te)

-------------------------------------------------------------------------
-- Auxiliaries to support equivalence checking of operations.

-- Create data type with explicit bottom constructors.
genBottomType :: String -> FC.TypeDecl -> CTypeDecl
genBottomType _ (FC.TypeSyn _ _ _ _) =
  error "genBottomType: cannot translate type synonyms"
genBottomType mainmod (FC.Type qtc@(_,tc) _ tvars consdecls) =
  CType (mainmod,t2bt tc) Public (map transTVar tvars)
        (simpleCCons (mainmod,"Bot_"++transQN tc) Public [] :
         if isBasicExtType qtc
           then [simpleCCons (mainmod,"Value_"++tc) Public [baseType qtc]]
           else map transConsDecl consdecls)
        [(pre "Eq"),(pre "Show")]
 where
  transConsDecl (FC.Cons (_,cons) _ _ argtypes) =
    simpleCCons (mainmod,t2bt cons) Public (map transTypeExpr argtypes)

  transTypeExpr (FC.TVar i) = CTVar (transTVar i)
  transTypeExpr (FC.FuncType t1 t2) =
    CFuncType (transTypeExpr t1) (transTypeExpr t2)
  transTypeExpr (FC.TCons (_,tcons) tes) =
    applyTC (mainmod,t2bt tcons) (map transTypeExpr tes)
  transTypeExpr (FC.ForallType _ _) =
    error "genBottomType: cannot handle forall types"

  transTVar i = (i,'a':show i)

-- Is the type name an external basic prelude type?
isBasicExtType :: QName -> Bool
isBasicExtType (mn,tc) = mn == preludeName && tc `elem` ["Int","Float","Char"]

-- Default value for external basic prelude types.
defaultValueOfBasicExtType :: String -> CLiteral
defaultValueOfBasicExtType qn
  | qn == "Int"   = CIntc   0
  | qn == "Float" = CFloatc 0.0
  | qn == "Char"  = CCharc  'A'
  | otherwise     = error $ "defaultValueOfBasicExtType: unknown type: "++qn
  
ctype2BotType :: String -> CTypeExpr -> CTypeExpr
ctype2BotType _ (CTVar i) = CTVar i
ctype2BotType mainmod (CFuncType t1 t2) =
  CFuncType (ctype2BotType mainmod t1) (ctype2BotType mainmod t2)
ctype2BotType mainmod (CTApply t1 t2) =
  CTApply (ctype2BotType mainmod t1) (ctype2BotType mainmod t2)
ctype2BotType mainmod (CTCons qtc) =
  CTCons (mainmod, t2bt (snd qtc))

-- Translate a type constructor name to its bottom type constructor name
t2bt :: String -> String
t2bt s = "P_" ++ transQN s

-- Create `peval_` operation for a data type with explicit bottom constructors
-- according to the following scheme:
{-
peval_AB :: AB -> P_AB -> P_AB
peval_AB _ Bot_AB = Bot_AB                 -- no evaluation
peval_AB A P_A    = P_A
peval_AB B P_B    = P_B

peval_C :: C -> P_C -> P_C
peval_C _     Bot_C   = Bot_C              -- no evaluation
peval_C (C x) (P_C y) = P_C (peval_AB x y)

f_equiv_g x p = peval_C (f x) p <~> peval_C (g x) p
-}
genPeval :: String -> FC.TypeDecl -> CFuncDecl
genPeval _ (FC.TypeSyn _ _ _ _) =
  error "genPeval: cannot translate type synonyms"
genPeval mainmod (FC.Type qtc@(_,tc) _ tvars consdecls) =
  cmtfunc ("Evaluate a `"++tc++"` value up to a partial approxmiation.")
    (mainmod,"peval_"++transQN tc) 1 Public
    (emptyClassType
      (foldr1 (~>) (map (\ (a,b) -> CTVar a ~> CTVar b ~> CTVar b)
                        (zip polyavars polyrvars) ++
                    [applyTC qtc (map CTVar polyavars),
                     applyTC (mainmod,t2bt tc) (map CTVar polyrvars),
                     applyTC (mainmod,t2bt tc) (map CTVar polyrvars)])))
    (simpleRule (map CPVar (polyavars ++ [(0,"_")]) ++ [CPComb botSym []])
                (constF botSym) :
     if isBasicExtType qtc
       then [valueRule]
       else map genConsRule consdecls)
 where
  botSym = (mainmod,"Bot_"++transQN tc) -- bottom constructor
  
  -- variables for polymorphic type arguments:
  polyavars = [ (i,"a"++show i) | i <- tvars]
  polyrvars = [ (i,"b"++show i) | i <- tvars]
  
  genConsRule (FC.Cons qc@(_,cons) _ _ argtypes) =
    let args  = [(i,"x"++show i) | i <- [0 .. length argtypes - 1]]
        pargs = [(i,"y"++show i) | i <- [0 .. length argtypes - 1]]
        pcons = (mainmod,t2bt cons)
    in simpleRule (map CPVar polyavars ++
                   [CPComb qc (map CPVar args), CPComb pcons (map CPVar pargs)])
         (applyF pcons
                 (map (\ (e1,e2,te) ->
                        applyE (ftype2pvalOf mainmod "peval" polyavars te)
                               [e1,e2])
                      (zip3 (map CVar args) (map CVar pargs) argtypes)))

  valueRule =
    let xvar    = (0,"x")
        yvar    = (1,"y")
        valcons = (mainmod,"Value_"++tc)
    in guardedRule [CPVar xvar, CPComb valcons [CPVar yvar]]
                   [(constF (pre "True"), --applyF (pre "=:=") [CVar xvar, CVar yvar],
                     applyF valcons [CVar xvar])]
                   []

-- Create `pvalOf` operation for a data type with explicit bottom constructors
-- according to the following scheme:
{-
pvalOf_AB :: AB -> P_AB
pvalOf_AB _ = Bot_AB
pvalOf_AB A = P_A
pvalOf_AB B = P_B

pvalOf_C :: C -> P_C
pvalOf_C _     = Bot_C
pvalOf_C (C x) = P_C (pvalOf_AB x)

f_equiv_g x = pvalOf_C (f x) <~> pvalOf_C (g x)
-}
genPValOf :: String -> FC.TypeDecl -> CFuncDecl
genPValOf _ (FC.TypeSyn _ _ _ _) =
  error "genPValOf: cannot translate type synonyms"
genPValOf mainmod (FC.Type qtc@(_,tc) _ tvars consdecls) =
  cmtfunc ("Map a `"++tc++"` value into all its partial approxmiations.")
    (mainmod,"pvalOf_"++transQN tc) 1 Public
    (emptyClassType
      (foldr1 (~>) (map (\ (a,b) -> CTVar a ~> CTVar b)
                        (zip polyavars polyrvars) ++
                    [applyTC qtc (map CTVar polyavars),
                     applyTC (mainmod,t2bt tc) (map CTVar polyrvars)])))
    (simpleRule (map CPVar (polyavars ++ [(0,"_")]))
                (constF (mainmod,"Bot_"++transQN tc)) :
     if isBasicExtType qtc
       then [valueRule]
       else map genConsRule consdecls)
 where
  -- variables for polymorphic type arguments:
  polyavars = [ (i,"a"++show i) | i <- tvars]
  polyrvars = [ (i,"b"++show i) | i <- tvars]
  
  genConsRule (FC.Cons qc@(_,cons) _ _ argtypes) =
    let args = [(i,"x"++show i) | i <- [0 .. length argtypes - 1]]
    in simpleRule (map CPVar polyavars ++ [CPComb qc (map CPVar args)])
         (applyF (mainmod,t2bt cons)
            (map (\ (e,te) ->
                   applyE (ftype2pvalOf mainmod "pvalOf" polyavars te) [e])
                 (zip (map CVar args) argtypes)))

  valueRule =
    let var = (0,"x")
    in simpleRule [CPVar var] (applyF (mainmod,"Value_"++tc) [CVar var])

-- Translate a FlatCurry type into a corresponding call to `pvalOf`:
ftype2pvalOf :: String -> String -> [(Int,String)] -> FC.TypeExpr -> CExpr
ftype2pvalOf mainmod pvalname polyvars (FC.TCons (_,tc) texps) =
  applyF (mainmod,pvalname++"_"++transQN tc)
         (map (ftype2pvalOf mainmod pvalname polyvars) texps)
ftype2pvalOf _ _ _ (FC.FuncType _ _) =
  error "genPValOf: cannot handle functional types in as constructor args"
ftype2pvalOf _ _ polyvars (FC.TVar i) =
  maybe (error "genPValOf: unbound type variable")
        CVar
        (find ((==i) . fst) polyvars)
ftype2pvalOf _ _ _ (FC.ForallType _ _) =
  error "genPValOf: forall type occurred"

-- Translate an AbstractCurry type into a corresponding call to `pvalOf`:
ctype2pvalOf :: String -> String -> CTypeExpr -> CExpr
ctype2pvalOf mainmod pvalname (CTCons (_,tc)) =
  constF (mainmod,pvalname++"_"++transQN tc)
ctype2pvalOf mainmod pvalname te@(CTApply _ _) =
  maybe (error "genPValOf: cannot handle type applications")
        (\ ((_,tc),targs) -> applyF (mainmod,pvalname++"_"++transQN tc)
                                    (map (ctype2pvalOf mainmod pvalname) targs))
        (tconsArgsOfType te)
ctype2pvalOf _ _ (CFuncType _ _) =
  error "genPValOf: cannot handle functional types in as constructor args"
ctype2pvalOf _ _ (CTVar _) = error "genPValOf: unbound type variable"


-- Translate an AbstractCurry type declaration into a FlatCurry type decl:
ctypedecl2ftypedecl :: CTypeDecl -> FC.TypeDecl
ctypedecl2ftypedecl (CTypeSyn _ _ _ _) =
  error "ctypedecl2ftypedecl: cannot translate type synonyms"
ctypedecl2ftypedecl (CNewType _ _ _ _ _) =
  error "ctypedecl2ftypedecl: cannot translate newtype"
ctypedecl2ftypedecl (CType qtc _ tvars consdecls _) =
  FC.Type qtc FC.Public (map fst tvars) (map transConsDecl consdecls)
 where
  transConsDecl (CCons _ _ qc _ argtypes) =
    FC.Cons qc (length argtypes) FC.Public (map transTypeExpr argtypes)
  transConsDecl (CRecord _ _ _ _ _) =
    error "ctypedecl2ftypedecl: cannot translate records"

  transTypeExpr (CTVar (i,_)) = FC.TVar i
  transTypeExpr (CFuncType t1 t2) =
    FC.FuncType (transTypeExpr t1) (transTypeExpr t2)
  transTypeExpr (CTCons qtcons) = FC.TCons qtcons []
  transTypeExpr te@(CTApply _ _) =
    maybe (error "ctypedecl2ftypedecl: cannot translate type applications")
          (\ (qtcons,tes) -> FC.TCons qtcons (map transTypeExpr tes))
          (tconsArgsOfType te)
Michael Hanus 's avatar
Michael Hanus committed
1108
1109
1110

-------------------------------------------------------------------------
-- Create the main test module containing all tests of all test modules as
1111
-- a Curry program with name `mainmod`.
Michael Hanus 's avatar
Michael Hanus committed
1112
1113
1114
1115
-- The main test module contains a wrapper operation for each test
-- and a main function to execute these tests.
-- Furthermore, if PAKCS is used, test data generators
-- for user-defined types are automatically generated.
1116
genMainTestModule :: Options -> String -> [TestModule] -> IO [Test]
1117
1118
1119
genMainTestModule opts mainmod orgtestmods = do
  let alltests     = concatMap propTests orgtestmods
      equivtestops = nub (concatMap equivTestOps alltests)
1120
  terminfos <- if optEquiv opts == Autoselect
Michael Hanus 's avatar
Michael Hanus committed
1121
                 then getTerminationInfos opts (nub (map fst equivtestops))
1122
                 else return (const False)
1123
  prodinfos <- if optEquiv opts == Safe
Michael Hanus 's avatar
Michael Hanus committed
1124
                 then getProductivityInfos opts (nub (map fst equivtestops))
1125
                 else return (const NoInfo)
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
  unsafeinfos <- if optIOTest opts
                   then return (const [])
                   else getUnsafeModuleInfos opts
                          (nub (map (fst . testName) alltests))
  let (testmods,rmtestnames) = removeNonExecTests opts unsafeinfos orgtestmods
      testtypes = nub (concatMap userTestDataOfModule testmods)
  unless (null rmtestnames) $ do
    putStrIfNormal opts $ unlines
      [withColor opts red $ "Properties not tested (due to I/O or unsafe):",
       unwords (map snd rmtestnames)]
1136
1137
1138
  (fcprogs,testtypedecls) <- collectAllTestTypeDecls opts [] [] testtypes
  equvtypedecls <- collectAllTestTypeDecls opts fcprogs []
                     (map (\t->(t,True))
1139
                          (nub (concatMap equivPropTypes testmods)))
1140
1141
1142
1143
                     >>= return . map fst . snd
  let bottypes  = map (genBottomType mainmod) equvtypedecls
      pevalfuns = map (genPeval mainmod) equvtypedecls
      pvalfuns  = map (genPValOf mainmod) equvtypedecls
1144
      generators   = map (genTestDataGenerator mainmod)
1145
1146
                         (testtypedecls ++
                          map (\td -> (ctypedecl2ftypedecl td,False)) bottypes)
1147
1148
1149
  testfuncs <- liftM concat
                 (mapM (genTestFuncs opts terminfos prodinfos mainmod) testmods)
  let mainFunction = genMainFunction opts mainmod testfuncs
Michael Hanus 's avatar
Michael Hanus committed
1150
1151
      imports      = nub $ [ easyCheckModule, easyCheckExecModule
                           , searchTreeModule, generatorModule
1152
1153
                           , "AnsiCodes","Maybe","System","Profile"] ++
                           map (fst . fst) testtypes ++
1154
                           map testModuleName testmods
Michael Hanus 's avatar
Michael Hanus committed
1155
1156
  appendix <- readFile (packagePath </> "src" </> "TestAppendix.curry")
  writeCurryProgram opts "."
1157
    (CurryProg mainmod imports Nothing [] [] bottypes
1158
1159
               (mainFunction : testfuncs ++ generators ++ pvalfuns ++ pevalfuns)
               [])
Michael Hanus 's avatar
Michael Hanus committed
1160
    appendix
1161
  let (finaltests,droppedtests) =
1162
1163
           partition ((`elem` map (snd . funcName) testfuncs) . genTestName)
                     (concatMap propTests testmods)
1164
1165
1166
1167
  unless (null droppedtests) $ putStrIfNormal opts $
    "\nPOSSIBLY NON-TERMINATING TESTS REMOVED: " ++
    unwords (map (snd . testName) droppedtests) ++ "\n"
  return finaltests
Michael Hanus 's avatar
Michael Hanus committed
1168
1169
1170

-- Generates the main function which executes all property tests
-- of all test modules.
1171
1172
genMainFunction :: Options -> String -> [CFuncDecl] -> CFuncDecl
genMainFunction opts testModule testfuncs =
Michael Hanus 's avatar
Michael Hanus committed
1173
1174
  CFunc (testModule, "main") 0 Public (emptyClassType (ioType unitType))
        [simpleRule [] body]
Michael Hanus 's avatar
Michael Hanus committed
1175
1176
1177
1178
1179
1180
1181
1182
1183
 where
  body = CDoExpr $
     (if isQuiet opts
        then []
        else [CSExpr (applyF (pre "putStrLn")
                             [string2ac "Executing all tests..."])]) ++
     [ CSPat (cpvar "x1") $ -- run all tests:
          applyF (testModule, "runPropertyTests")
                 [constF (pre (if optColor opts then "True" else "False")),
1184
                  constF (pre (if optTime  opts then "True" else "False")),
1185
                  list2ac $ map (constF . funcName) testfuncs]
Michael Hanus 's avatar
Michael Hanus committed
1186
1187
1188
1189
1190
     , CSExpr $ applyF (pre "when")
                  [applyF (pre "/=") [cvar "x1", cInt 0],
                   applyF ("System", "exitWith") [cvar "x1"]]
     ]

1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
-- Remove all tests that should not be executed.
-- Thus, if option --noiotest is set, IO tests and tests depending on unsafe
-- modules are removed.
-- Returns the test modules where tests are removed and the names of
-- the removed tests.
removeNonExecTests :: Options -> (QName -> [String]) -> [TestModule]
                   -> ([TestModule], [QName])
removeNonExecTests opts unsafeinfos testmods =
  (map removeTests testmods,
   concatMap (map testName . filter (not . isExecTest) . propTests) testmods)
 where
  removeTests tm = tm { propTests = filter isExecTest (propTests tm) }

  isExecTest test = optIOTest opts ||
                    (not (isIOTest test) && null (unsafeinfos (tmod,tmod)))
   where tmod = dropPublicSuffix (fst (testName test))

Michael Hanus 's avatar
Michael Hanus committed
1208
1209
1210
1211
-------------------------------------------------------------------------
-- Collect all type declarations for a given list of type
-- constructor names, including the type declarations which are
-- used in these type declarations.
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
-- To cache already read FlatCurry programs, it gets a list of
-- FlatCurry programs (second argument) and returns a list of
-- FlatCurry programs.
collectAllTestTypeDecls :: Options -> [FC.Prog] -> [(FC.TypeDecl,Bool)]
                        -> [(QName,Bool)]
                        -> IO ([FC.Prog],[(FC.TypeDecl,Bool)])
collectAllTestTypeDecls opts fcprogs tdecls testtypenames = do
  newprogs <- readFlatProgsIfNecessary fcprogs (map (fst . fst) testtypenames)
  let newtesttypedecls = map (findTypeDecl newprogs) testtypenames
      alltesttypedecls = tdecls ++ newtesttypedecls
      newtcons = filter (\ ((mn,_),genpart) -> genpart || mn /= preludeName)
                        (nub (concatMap allTConsOfType newtesttypedecls)
                         \\ map (\(t,p) -> (FCG.typeName t,p)) alltesttypedecls)
  if null newtcons
    then return (newprogs,alltesttypedecls)
    else collectAllTestTypeDecls opts newprogs alltesttypedecls newtcons
Michael Hanus 's avatar
Michael Hanus committed
1228
 where
1229
1230
1231
1232
  readFlatProgsIfNecessary progs [] = return progs
  readFlatProgsIfNecessary progs (mn:mns) =
    if mn `elem` map FCG.progName progs
      then readFlatProgsIfNecessary progs mns
1233
      else do putStrIfDetails opts $
1234
1235
1236
1237
                "Reading data types defined in module '" ++ mn ++ "'...\n"
              fprog <- readFlatCurry mn
              readFlatProgsIfNecessary (fprog:progs) mns
  
Michael Hanus 's avatar
Michael Hanus committed
1238
1239
  -- gets the type declaration for a given type constructor
  -- (could be improved by caching programs that are already read)
1240
  findTypeDecl :: [FC.Prog] -> (QName,Bool) -> (FC.TypeDecl,Bool)
1241
  findTypeDecl fcyprogs (qt@(mn,_),genpartial) =
1242
1243
    let fprog = maybe (error $ "Cannot find module " ++ mn)
                      id
1244
                      (find (\p -> FCG.progName p == mn) fcyprogs)
1245
1246
1247
1248
1249
1250
1251
    in maybe (error $ "Definition of type '" ++ FC.showQNameInModule "" qt ++
                      "' not found!")
             (\td -> (td,genpartial))
             (find (\t -> FCG.typeName t == qt) (FCG.progTypes fprog))

  allTConsOfType :: (FC.TypeDecl,Bool) -> [(QName,Bool)]
  allTConsOfType (td,genpart) = map (\t->(t,genpart)) (allTConsInDecl td)
Michael Hanus 's avatar
Michael Hanus committed
1252
1253
1254
1255
1256

  -- compute all type constructors used in a type declaration
  allTConsInDecl :: FC.TypeDecl -> [QName]
  allTConsInDecl = FCG.trType (\_ _ _ -> concatMap allTConsInConsDecl)
                              (\_ _ _ -> allTConsInTypeExpr)
Michael Hanus 's avatar
Michael Hanus committed
1257

Michael Hanus 's avatar
Michael Hanus committed
1258
1259
  allTConsInConsDecl :: FC.ConsDecl -> [QName]
  allTConsInConsDecl = FCG.trCons (\_ _ _ -> concatMap allTConsInTypeExpr)
Michael Hanus 's avatar
Michael Hanus committed
1260

Michael Hanus 's avatar
Michael Hanus committed
1261
1262
  allTConsInTypeExpr :: FC.TypeExpr -> [QName]
  allTConsInTypeExpr =
Michael Hanus 's avatar
Michael Hanus committed
1263
    FCG.trTypeExpr (\_ -> []) (\tc targs -> tc : concat targs) (++) (flip const)
Michael Hanus 's avatar
Michael Hanus committed
1264
1265

-- Creates a test data generator for a given type declaration.
1266
1267
-- If the flag of the type declaration is `True`, a generator
-- for partial values is created.
1268
1269
genTestDataGenerator :: String -> (FC.TypeDecl,Bool) -> CFuncDecl
genTestDataGenerator mainmod (tdecl,part) = type2genData tdecl
Michael Hanus 's avatar
Michael Hanus committed
1270
1271
1272
1273
1274
1275
 where
  qt       = FCG.typeName tdecl
  qtString = FC.showQNameInModule "" qt

  type2genData (FC.TypeSyn _ _ _ _) =
    error $ "Cannot create generator for type synonym " ++ qtString
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
  type2genData (FC.Type _ _ tvars cdecls)
    | null cdecls && (fst qt /= preludeName || not part)
    = error $ "Cannot create value generator for type '" ++ qtString ++
              "' without constructors!"
    | otherwise
    = cmtfunc
        ("Generator for " ++ (if part then "partial " else "") ++
         "`" ++ qtString ++ "` values.")
        (typename2genopname mainmod [] part qt) (length tvars) Public
        (emptyClassType
          (foldr (~>) (CTApply (CTCons searchTreeTC) (applyTC qt ctvars))
                      (map (\v -> applyTC searchTreeTC [v]) ctvars)))
        [simpleRule (map CPVar cvars)
          (let gencstrs =  foldr1 (\e1 e2 -> applyF choiceGen [e1,e2])
                                  (map cons2gen cdecls)
           in if part
                then applyF choiceGen
                            [ applyF (generatorModule, "genCons0")
                                     [constF (pre "failed")]
                            , if null cdecls
                                then constF (generatorModule,
                                             "gen" ++ transQN (snd qt))
                                else gencstrs ]
                else gencstrs)]
Michael Hanus 's avatar
Michael Hanus committed
1300
   where
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
    cons2gen (FC.Cons qn@(mn,cn) ar _ ctypes)
      | ar>maxArity
      = error $ "Test data constructors with more than " ++ show maxArity ++
                " arguments are currently not supported!"
      | not part && mn == mainmod && "Value_" `isPrefixOf` cn
        -- specific generator for bottom types of external basic types
        -- like Int (actually, do not generate values in order to reduce
        -- search space):
      = applyF (generatorModule, "genCons1")
               [CSymbol qn,
                applyF (searchTreeModule,"Value")
                       [CLit (defaultValueOfBasicExtType (drop 6 cn))]]
      | otherwise
      = applyF (generatorModule, "genCons" ++ show ar)
               ([CSymbol qn] ++ map type2gen ctypes)
Michael Hanus 's avatar
Michael Hanus committed
1316
1317
1318
1319
1320
1321

    type2gen (FC.TVar i) = CVar (i,"a"++show i)
    type2gen (FC.FuncType _ _) =
      error $ "Type '" ++ qtString ++
              "': cannot create value generators for functions!"
    type2gen (FC.TCons qtc argtypes) =
1322
      applyF (typename2genopname mainmod [] part qtc) (map type2gen argtypes)
Michael Hanus 's avatar
Michael Hanus committed
1323
1324
1325
    type2gen (FC.ForallType _ _) =
      error $ "Type '" ++ qtString ++
              "': cannot create value generators for forall types!"
Michael Hanus 's avatar
Michael Hanus committed
1326
1327
1328
1329
1330
1331
1332

    ctvars = map (\i -> CTVar (i,"a"++show i)) tvars
    cvars  = map (\i -> (i,"a"++show i)) tvars

-------------------------------------------------------------------------
-- remove the generated files (except if option "--keep" is set)
cleanup :: Options -> String -> [TestModule] -> IO ()
1333
cleanup opts mainmod modules =
Michael Hanus 's avatar
Michael Hanus committed
1334
  unless (optKeep opts) $ do
1335
    removeCurryModule mainmod
Michael Hanus 's avatar
Michael Hanus committed
1336
1337
    mapIO_ removeCurryModule (map testModuleName modules)
 where
Michael Hanus 's avatar
Michael Hanus committed
1338
1339
1340
1341
1342
1343
1344
  removeCurryModule modname =
    lookupModuleSourceInLoadPath modname >>=
    maybe done
          (\ (_,srcfilename) -> do
            system $ installDir </> "bin" </> "cleancurry" ++ " " ++ modname
            system $ "rm -f " ++ srcfilename
            done )
Michael Hanus 's avatar
Michael Hanus committed
1345
1346

-- Show some statistics about number of tests:
Michael Hanus 's avatar
Michael Hanus committed
1347
1348
showTestStatistics :: Options -> [Test] -> String
showTestStatistics opts tests =
1349
1350
1351
1352
1353
  let numtests  = sumOf (const True)
      unittests = sumOf isUnitTest  
      proptests = sumOf isPropTest  
      equvtests = sumOf isEquivTest 
      iotests   = sumOf isIOTest    
Michael Hanus 's avatar
Michael Hanus committed
1354
1355
   in "TOTAL NUMBER OF TESTS: " ++ show numtests ++
      " (UNIT: " ++ show unittests ++ ", PROPERTIES: " ++
1356
      show proptests ++ ", EQUIVALENCE: " ++ show equvtests ++
Michael Hanus 's avatar
Michael Hanus committed
1357
      (if optIOTest opts then ", IO: " ++ show iotests else "") ++ ")"
Michael Hanus 's avatar
Michael Hanus committed
1358
 where
1359
  sumOf p = length . filter p $ tests
Michael Hanus 's avatar
Michael Hanus committed
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369

-------------------------------------------------------------------------
main :: IO ()
main = do
  argv <- getArgs
  pid  <- getPID
  let (funopts, args, opterrors) = getOpt Permute options argv
  opts <- processOpts (foldl (flip id) defaultOptions funopts)
  unless (null opterrors)
         (putStr (unlines opterrors) >> putStrLn usageText >> exitWith 1)
Michael Hanus 's avatar
Michael Hanus committed
1370
  putStrIfNormal opts ccBanner
Michael Hanus 's avatar
Michael Hanus committed
1371
  when (null args || optHelp opts) (putStrLn usageText >> exitWith 1)
1372
1373
1374
  let mods = map stripCurrySuffix args
  mapIO_ checkModuleName mods
  testModules <- mapIO (analyseModule opts) mods
Michael Hanus 's avatar
Michael Hanus committed
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
  let staticerrs       = concatMap staticErrors (concat testModules)
      finaltestmodules = filter testThisModule (concat testModules)
      testmodname = if null (optMainProg opts)
                      then "TEST" ++ show pid
                      else optMainProg opts
  if not (null staticerrs)
   then do showStaticErrors opts staticerrs
           putStrLn $ withColor opts red "Testing aborted!"
           cleanup opts testmodname finaltestmodules
           exitWith 1
   else if null finaltestmodules then exitWith 0 else do
    putStrIfNormal opts $ withColor opts blue $
                          "Generating main test module '"++testmodname++"'..."
1388
    putStrIfDetails opts "\n"
1389
    finaltests <- genMainTestModule opts testmodname finaltestmodules
Michael Hanus 's avatar
Michael Hanus committed
1390
    showGeneratedModule opts "main test" testmodname
Michael Hanus 's avatar
Michael Hanus committed
1391
    putStrIfNormal opts $ withColor opts blue $ "and compiling it...\n"
1392
1393
1394
    ecurrypath <- getEnviron "CURRYPATH"
    let currypath = case ecurrypath of ':':_ -> '.':ecurrypath
                                       _     -> ecurrypath
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
    let runcmd = unwords $
                   [ installDir </> "bin" </> "curry"
                   , "--noreadline"
                   , ":set -time"
                   , ":set " ++ if optVerb opts > 3 then "v1" else "v0"
                   , ":set parser -Wnone"
                   , if null currypath then "" else ":set path " ++ currypath
                   , ":l "++testmodname,":eval main :q" ]
    putStrLnIfDebug opts $ "Executing command:\n" ++ runcmd
    ret <- system runcmd
Michael Hanus 's avatar
Michael Hanus committed
1405
1406
    cleanup opts testmodname finaltestmodules
    unless (isQuiet opts || ret /= 0) $
Michael Hanus 's avatar
Michael Hanus committed
1407
      putStrLn $ withColor opts green $ showTestStatistics opts finaltests
Michael Hanus 's avatar
Michael Hanus committed
1408
1409
1410
1411
    exitWith ret
 where
  showStaticErrors opts errs = putStrLn $ withColor opts red $
    unlines (line : "STATIC ERRORS IN PROGRAMS:" : errs) ++ line
1412
1413
1414
1415
1416
1417

  checkModuleName mn =
    when (pathSeparator `elem` mn) $ do
      putStrLn $ "Module names with path prefixes not allowed: " ++ mn
      exitWith 1

Michael Hanus 's avatar
Michael Hanus committed
1418
1419
  line = take 78 (repeat '=')

Michael Hanus 's avatar
Michael Hanus committed
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
showGeneratedModule :: Options -> String -> String -> IO ()
showGeneratedModule opts mkind modname = when (optVerb opts > 3) $ do
  putStrLn $ '\n' : line
  putStrLn $ "Generated " ++ mkind ++ " module `" ++ modname ++ ".curry':"
  putStrLn line
  readFile (modname ++ ".curry") >>= putStr
  putStrLn line
 where
  line = take 78 (repeat '=')

Michael Hanus 's avatar
Michael Hanus committed
1430
1431
1432
-------------------------------------------------------------------------
-- Auxiliaries

1433
-- Rename all module references to "Test.Prop" into "Test.EasyCheck"
Michael Hanus 's avatar
Michael Hanus committed
1434
1435
renameProp2EasyCheck :: CurryProg -> CurryProg
renameProp2EasyCheck prog =
Michael Hanus 's avatar
Michael Hanus committed
1436
  updCProg id (map rnmMod) id id id id id id
Michael Hanus 's avatar
Michael Hanus committed
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
           (updQNamesInCProg (\ (mod,n) -> (rnmMod mod,n)) prog)
 where
  rnmMod mod | mod == propModule = easyCheckModule
             | otherwise         = mod

-- Extracts the first word of a string
firstWord :: String -> String
firstWord = head . splitOn "\t" . head . splitOn " "

-- Strips a suffix from a string.
stripSuffix :: String -> String -> String
stripSuffix str suf = if suf `isSuffixOf` str
                      then take (length str - length suf) str
                      else str

-- Translate a module name to an identifier, i.e., replace '.' by '_':
modNameToId :: String -> String
modNameToId = intercalate "_" . split (=='.')

-- Computes the arity from a type expression.
arityOfType :: CTypeExpr -> Int
arityOfType = length . argTypes

--- Name of the SearchTree module.
searchTreeModule :: String
searchTreeModule = "SearchTree"

--- Name of SearchTree type constructor.
searchTreeTC :: QName
searchTreeTC = (searchTreeModule,"SearchTree")
Michael Hanus 's avatar
Michael Hanus committed
1467

Michael Hanus 's avatar
Michael Hanus committed
1468
1469
1470
1471
--- Name of the SearchTreeGenerator module.
generatorModule :: String
generatorModule = "SearchTreeGenerators"

1472
1473
1474
choiceGen :: QName
choiceGen = (generatorModule,"|||")

Michael Hanus 's avatar
Michael Hanus committed
1475
1476
1477
1478
-- Writes a Curry module (together with an appendix) to its file.
writeCurryProgram :: Options -> String -> CurryProg -> String -> IO ()
writeCurryProgram opts srcdir p appendix = do
  let progfile = srcdir </> modNameToPath (progName p) ++ ".curry"
1479
  putStrLnIfDebug opts $ "Writing program: " ++ progfile
Michael Hanus 's avatar
Michael Hanus committed
1480
  writeFile progfile
1481
            (ACPretty.showCProg p ++ "\n" ++ appendix ++ "\n")
Michael Hanus 's avatar
Michael Hanus committed
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492

isPAKCS :: Bool
isPAKCS = curryCompiler == "pakcs"

-- Does a program text contains a OPTIONS_CYMAKE line to call currypp?
containsPPOptionLine :: String -> Bool
containsPPOptionLine = any isOptionLine . lines
 where
   isOptionLine s = "{-# OPTIONS_CYMAKE " `isPrefixOf` s -- -}
                    && "currypp" `isInfixOf` s

1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
tconsOf :: CTypeExpr -> [QName]
tconsOf (CTVar _)           = []
tconsOf (CFuncType from to) = union (tconsOf from) (tconsOf to)
tconsOf (CTCons tc)         = [tc]
tconsOf (CTApply tc ta)     = union (tconsOf tc) (tconsOf ta)

unionOn :: Eq b => (a -> [b]) -> [a] -> [b]
unionOn f = foldr union [] . map f

-- Pretty print an AbstractCurry type expression:
showCTypeExpr :: CTypeExpr -> String
showCTypeExpr = pPrint . ACPretty.ppCTypeExpr ACPretty.defaultOptions

-- Pretty print an AbstractCurry expression:
showCExpr :: CExpr -> String
showCExpr = pPrint . ACPretty.ppCExpr ACPretty.defaultOptions

1510
1511
1512
1513
1514
1515
-- Builds a lambda abstraction. If the argument list is empty,
-- it builts an expression.
cLambda :: [CPattern] -> CExpr -> CExpr
cLambda pats body | null pats = body
                  | otherwise = CLambda pats body

Michael Hanus 's avatar
Michael Hanus committed
1516
-------------------------------------------------------------------------