|
sourcecode:
|
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)
---------------------------------------------------------------------------
|