1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148

------------------------------------------------------------------------
--- This module contains some operations to check the correct usage of
--- contracts (i.e., the occurrences and types of specification and
--- pre/postconditions) in a FlatCurry program.
---
--- @author Michael Hanus
--- @version May 2021
------------------------------------------------------------------------

module Contract.Usage ( checkContractUsage ) where

import Data.List         ( (\\), find )

import FlatCurry.Goodies   ( argTypes, resultType )
import FlatCurry.Types
import FlatCurry.Normalize ( normalizeTypeExpr )

import Contract.Names

--- Checks the intended usage of contracts, i.e., whether
--- contracts types correspond to types of functions.
--- The parameter are the module and the list of names and (FlatCurry) types
--- of all functions defined in this module.
--- The result is a list of error messages for qualified function names.
checkContractUsage :: String -> [(String,TypeExpr)] -> [(QName,String)]
checkContractUsage mn allopsforall =
  let allops       = map (\ (n,t) -> (n, stripForall t)) allopsforall
      allopsnames  = map fst allops
      specops      = map (\ (n,t) ->
                            (fromSpecName (decodeContractName n), t))
                         (filter (isSpecName . fst) allops)
      preops       = map (\ (n,t) ->
                            (fromPreCondName (decodeContractName n), t))
                         (filter (isPreCondName . fst) allops)
      postops      = map (\ (n,t) ->
                            (fromPostCondName (decodeContractName n), t))
                         (filter (isPostCondName . fst) allops)
      nonfailops   = map (\ (n,t) ->
                            (fromNonFailName (decodeContractName n), t))
                         (filter (isNonFailName . fst) allops)
      onlyprecond  = map fst preops     \\ allopsnames
      onlypostcond = map fst postops    \\ allopsnames
      onlyspec     = map fst specops    \\ allopsnames
      onlynonfail  = map fst nonfailops \\ allopsnames
      errmsg   = "No implementation for this "
      preerrs  = map (\ n -> ((mn, toPreCondName n), errmsg ++ "precondition"))
                     onlyprecond
      posterrs = map (\ n -> ((mn, toPostCondName n),errmsg ++ "postcondition"))
                     onlypostcond
      specerrs = map (\ n -> ((mn, toSpecName n), errmsg ++ "specification"))
                     onlyspec
      nferrs   = map (\ n -> ((mn, toNonFailName n),
                              errmsg ++ "non-fail condition"))
                     onlynonfail
   in preerrs ++ posterrs ++ specerrs ++ nferrs ++
      checkNonFailTypes  mn allops nonfailops ++
      checkPreTypes      mn allops preops ++
      checkPostTypes     mn allops postops ++
      checkSpecTypes     mn allops specops

checkNonFailTypes :: String -> [(String,TypeExpr)] -> [(String,TypeExpr)]
                  -> [(QName,String)]
checkNonFailTypes mn allops nfops = concatMap checkNonFailTypeOf nfops
 where
  checkNonFailTypeOf (n,t) =
    maybe (notFoundError "non-fail condition" (mn,n))
          (\ (_,ft) -> checkNonFailType n
                         (normalizeTypeExpr t) (normalizeTypeExpr ft))
          (find (\ (f,_) -> f == n) allops)

  checkNonFailType n pt ft
    | resultType pt /= TCons ("Prelude","Bool") []
    = illegalTypeError "Non-fail condition" (mn, toNonFailName n)
    | argTypes pt /= argTypes ft
    = wrongTypeError "non-fail condition" (mn, toNonFailName n)
    | otherwise
    = []

checkPreTypes :: String -> [(String,TypeExpr)] -> [(String,TypeExpr)]
              -> [(QName,String)]
checkPreTypes mn allops preops = concatMap checkPreTypeOf preops
 where
  checkPreTypeOf (n,t) =
    maybe (notFoundError "precondition" (mn,n))
          (\ (_,ft) -> checkPreType n
                         (normalizeTypeExpr t) (normalizeTypeExpr ft))
          (find (\ (f,_) -> f == n) allops)

  checkPreType n pt ft
    | resultType pt /= TCons ("Prelude","Bool") []
    = illegalTypeError "Precondition" (mn, toPreCondName n)
    | argTypes pt /= argTypes ft
    = wrongTypeError "precondition" (mn, toPreCondName n)
    | otherwise
    = []

checkPostTypes :: String -> [(String,TypeExpr)] -> [(String,TypeExpr)]
               -> [(QName,String)]
checkPostTypes mn allops postops = concatMap checkPostTypeOf postops
 where
  checkPostTypeOf (n,t) =
    maybe (notFoundError "postcondition" (mn,n))
          (\ (_,ft) -> checkPostType n
                         (normalizeTypeExpr t) (normalizeTypeExpr ft))
          (find (\ (f,_) -> f == n) allops)

  checkPostType n pt ft
    | resultType pt /= TCons ("Prelude","Bool") []
    = illegalTypeError "Postcondition" (mn, toPostCondName n)
    | argTypes pt /= argTypes ft ++ [resultType ft]
    = wrongTypeError "postcondition" (mn, toPostCondName n)
    | otherwise
    = []

checkSpecTypes :: String -> [(String,TypeExpr)] -> [(String,TypeExpr)]
               -> [(QName,String)]
checkSpecTypes mn allops specops = concatMap checkSpecTypeOf specops
 where
  checkSpecTypeOf (n,t) =
    maybe (notFoundError "specification" (mn,n))
          (\ (_,ft) -> checkSpecType n
                         (normalizeTypeExpr t) (normalizeTypeExpr ft))
          (find (\ (f,_) -> f == n) allops)

  checkSpecType n pt ft
    | pt /= ft
    = wrongTypeError "specification" (mn, toSpecName n)
    | otherwise
    = []

notFoundError :: String -> QName -> [(QName,String)]
notFoundError cond qn =
  [(qn, "Operation for " ++ cond ++ " not found!")]

illegalTypeError :: String -> QName -> [(QName,String)]
illegalTypeError cond qn = [(qn, cond ++ " has illegal type")]

wrongTypeError :: String -> QName -> [(QName,String)]
wrongTypeError cond qn = [(qn, "Type of " ++ cond ++ " does not match")]

-- Strip outermost `ForallType` since this quantification is not relevant
-- for our checks.
stripForall :: TypeExpr -> TypeExpr
stripForall texp = case texp of
  ForallType _ te  -> stripForall te
  _                -> texp

------------------------------------------------------------------------