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
149
150
151
152
153
154
155
156
157
158
159
160

------------------------------------------------------------------------
--- This module contains some operations to define and manipulate
--- the names of contracts (i.e., specification and pre/postconditions)
--- in a Curry program.
---
--- @author Michael Hanus
--- @version April 2019
------------------------------------------------------------------------

module Contract.Names
  ( isSpecName, toSpecName, toSpecQName, fromSpecName
  , isPreCondName, toPreCondName, toPreCondQName, fromPreCondName
  , isPostCondName, toPostCondName, toPostCondQName, fromPostCondName
  , isNonFailName, toNonFailName, toNonFailQName, fromNonFailName
  , decodeContractQName, decodeContractName
  , encodeContractQName, encodeContractName
  )  where

import Data.Char  ( isAlphaNum )
import Data.List  ( isPrefixOf, isSuffixOf )
import Numeric    ( readHex )

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

--- Is this the name of a specification?
isSpecName :: String -> Bool
isSpecName f = "'spec" `isSuffixOf` f

--- Transform a name into a name of the corresponding specification
--- by adding the suffix "'spec".
toSpecName :: String -> String
toSpecName = (++"'spec")

--- Transform a qualified name into a name of the corresponding specification
--- by adding the suffix "'spec".
toSpecQName :: (String,String) -> (String,String)
toSpecQName (mn,fn) = (mn, toSpecName fn)

--- Drop the specification suffix "'spec" from the name:
fromSpecName :: String -> String
fromSpecName f =
  let rf = reverse f
   in reverse (drop (if take 5 rf == "ceps'" then 5 else 0) rf)

--- Is this the name of a precondition?
isPreCondName :: String -> Bool
isPreCondName f = "'pre" `isSuffixOf` f

--- Transform a name into a name of the corresponding precondition
--- by adding the suffix "'pre".
toPreCondName :: String -> String
toPreCondName = (++ "'pre")

--- Transform a qualified name into a name of the corresponding precondition
--- by adding the suffix "'pre".
toPreCondQName :: (String,String) -> (String,String)
toPreCondQName (mn,fn) = (mn, toPreCondName fn)

--- Drop the precondition suffix "'pre" from the name:
fromPreCondName :: String -> String
fromPreCondName f =
  let rf = reverse f
   in reverse (drop (if take 4 rf == "erp'" then 4 else 0) rf)

--- Is this the name of a precondition?
isPostCondName :: String -> Bool
isPostCondName f = "'post" `isSuffixOf` f

--- Transform a name into a name of the corresponding prostcondition
--- by adding the suffix "'post".
toPostCondName :: String -> String
toPostCondName = (++"'post")

--- Transform a qualified name into a name of the corresponding postcondition
--- by adding the suffix "'post".
toPostCondQName :: (String,String) -> (String,String)
toPostCondQName (mn,fn) = (mn, toPostCondName fn)

--- Drop the postcondition suffix "'post" from the name:
fromPostCondName :: String -> String
fromPostCondName f =
  let rf = reverse f
   in reverse (drop (if take 5 rf == "tsop'" then 5 else 0) rf)

--- Is this the name of a precondition?
isNonFailName :: String -> Bool
isNonFailName f = "'nonfail" `isSuffixOf` f

--- Transform a name into a name of the corresponding prostcondition
--- by adding the suffix "'post".
toNonFailName :: String -> String
toNonFailName = (++"'nonfail")

--- Transform a qualified name into a name of the corresponding postcondition
--- by adding the suffix "'post".
toNonFailQName :: (String,String) -> (String,String)
toNonFailQName (mn,fn) = (mn, toNonFailName fn)

--- Drop the postcondition suffix "'nonfail" from the name:
fromNonFailName :: String -> String
fromNonFailName f =
  let rf = reverse f
   in reverse (drop (if take 8 rf == "liafnon'" then 8 else 0) rf)

------------------------------------------------------------------------
--- Transforms a qualified operation name starting with `op_xh1...hn'`, where
--- each `hi` is a two digit hexadecimal number, into the name
--- of corresponding to the ord values of `h1...hn`.
--- For instance, `op_x263E'nonfail` is transformed into `&>'nonfail`.
decodeContractQName :: (String,String) -> (String,String)
decodeContractQName (mn,fn) = (mn, decodeContractName fn)

--- Transforms an operation name starting with `op_xh1...hn'`, where
--- each `hi` is a two digit hexadecimal number, into the name
--- of corresponding to the ord values of `h1...hn`.
--- For instance, `op_x263E'nonfail` is transformed into `&>'nonfail`.
decodeContractName :: String -> String
decodeContractName fn
  | "op_x" `isPrefixOf` fn && not (null fntail) = fromHex [] (drop 4 fnop)
  | otherwise                                   = fn
 where
  (fnop,fntail) = break (=='\'')fn

  fromHex s ""  = reverse s ++ fntail
  fromHex _ [_] = fn
  fromHex s (c1:c2:cs) = case readHex [c1,c2] of
    [(i,"")] -> fromHex (chr i : s) cs
    _        -> fn

--- Transforms a qualified operation name of the form `fn'tail` into a valid
--- identifier. Thus, if `fn` contains any non-alphanumeric characters,
--- the name will be transformed into `op_xh1...hn'`, where
--- each `hi` is the two digit hexadecimal number corresponding to the
--- i-th character of `fn`.
--- For instance, `&>'nonfail` is transformed into `op_x263E'nonfail`.
encodeContractQName :: (String,String) -> (String,String)
encodeContractQName (mn,fn) = (mn, encodeContractName fn)

--- Transforms an operation name of the form `fn'tail` into a valid
--- identifier. Thus, if `fn` contains any non-alphanumeric characters,
--- the name will be transformed into `op_xh1...hn'`, where
--- each `hi` is the two digit hexadecimal number corresponding to the
--- i-th character of `fn`.
--- For instance, `&>'nonfail` is transformed into `op_x263E'nonfail`.
encodeContractName :: String -> String
encodeContractName fn
  | null rop || null rsuf ||
    all (\c -> isAlphaNum c || c == '\''|| c == '_') rop
   = fn
  | otherwise
  = "op_x" ++ concatMap toHex (reverse (tail rop)) ++ '\'': reverse rsuf
 where
  (rsuf,rop) = break (=='\'')(reverse fn)

  toHex c = let n = ord c in [toHexDigit (n `div` 16), toHexDigit (n `mod` 16)]

  toHexDigit i = if i<10 then chr (ord '0' + i)
                    else chr (ord 'A' + i - 10)

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