0N/ACopyright : (c) University of Cambridge, Cambridge, England
0N/A adaption (c) Till Mossakowski, Uni Bremen 2002-2005
0N/AMaintainer : maeder@tzi.de
0N/AStability : provisional
0N/APortability : portable
0N/Atranslate 'Id' to Isabelle strings
0N/A ( showIsaConstT, showIsaConstIT, showIsaTypeT, transConstStringT
0N/A , mkIsaConstT, mkIsaConstIT, transString, isaPrelude
------------------- Id translation functions -------------------
data IsaPreludes = IsaPreludes
isaPrelude :: IsaPreludes
isaPrelude = IsaPreludes {
[(HsHOLCF_thy, types holcfS), (MainHC_thy, types mainS),
(Main_thy, types mainS), (HOLCF_thy, types holcfS)],
[(HsHOLCF_thy,
Set.insert "fliftbin" (consts holcfS)),
["pApp","apt","app","defOp","pair"]),
(Main_thy, consts mainS), (HOLCF_thy, consts holcfS)]}
toAltSyntax :: Bool -> Int -> GlobalAnnos -> Int -> Id -> BaseSig
toAltSyntax prd over ga n i@(Id ms cs qs) thy = let
minPrec = if prd then 42 else 52
adjustPrec p = 2 * p + minPrec
minL = replicate n lowPrio
(fs, ps) = splitMixToken ms
nonPlaces = filter (not . isPlace) fs
over2 = if isSingle nonPlaces &&
Set.member (tokStr $ head nonPlaces)
newFs = if null fs || over2 < 2 then fs else
fs ++ [mkSimpleId $ let o1 = over2 - 1 in
if over2 < 4 then replicate o1 '\'' else '_' : show o1]
(hd : tl) = getTokenList newPlace $ Id (newFs ++ ps) cs qs
tts = (if endPlace i then init else id) $ concatMap convert tl
convert = \ Token { tokStr = s } -> if s == newPlace then s
(precList, erg) = if isInfix i then case
Map.lookup i precMap of
Nothing -> (q + 1, q + 1)
Just ARight -> (q + 1, q)
Nothing -> let q = adjustPrec $ mx + 1 in (q : minL2 ++ [q], minPrec)
else if begPlace i then let q = adjustPrec $ mx + 3 in (q : minL1 , q)
else if endPlace i then let q = adjustPrec $ mx + 2 in (minL1 ++ [q], q)
in if n == 0 then Just $ AltSyntax ts [] maxPrio
else if isMixfix i then Just $ AltSyntax
('(' : (if begPlace i then "_ " else ht)
++ tts ++ ")") precList erg
concat (replicate (n - 1) "_,/ ")
++ "_')") minL $ maxPrio - 1
quote :: String -> String
c : r -> (if c `elem` "_/'()" then '\'' : [c]
else if c `elem` "\\\"" then '\\' : [c] else [c]) ++ quote r
showIsaT1 :: (String -> String) -> Id -> String
rdru = reverse . dropWhile (== '_')
in if isInfix2 ide then "XX" ++ tr (rdru $ rdru str) else tr str
showIsaConstT :: Id -> BaseSig -> String
showIsaConstT ide thy = showIsaT1 (transConstStringT thy) ide
-- also pass number of arguments
mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> VName
mkIsaConstT = mkIsaConstVName 1 showIsaConstT
mkIsaConstVName :: Int -> (Id -> BaseSig -> String)
-> Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> VName
mkIsaConstVName over f prd ga n ide thy = VName
, altSyn = toAltSyntax prd over ga n ide thy }
showIsaTypeT :: Id -> BaseSig -> String
showIsaTypeT ide thy = showIsaT1 (transTypeStringT thy) ide
-- | add a number for overloading
showIsaConstIT :: Id -> Int -> BaseSig -> String
showIsaConstIT ide i thy = showIsaConstT ide thy ++ "_" ++ show i
mkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig -> VName
mkIsaConstIT prd ga n ide i thy =
{- if n == 0 || isPrefixOf "g__" (show ide)
then mkVName $ showIsaConstIT ide i thy
mkIsaConstVName i ( \ ide' -> showIsaConstIT ide' i) prd ga n ide thy
transIsaStringT m i s = let t = transString s in
transConstStringT :: BaseSig -> String -> String
transConstStringT = transIsaStringT $ preConsts isaPrelude
transTypeStringT :: BaseSig -> String -> String
transTypeStringT = transIsaStringT $ preTypes isaPrelude
-- | check for legal alphanumeric isabelle characters
isIsaChar :: Char -> Bool
isIsaChar c = isAlphaNum c && isAscii c || c `elem` "_'"
transString :: String -> String
replaceChar1 d | d == x = "YX" -- code out existing X!
| otherwise = replaceChar d ++ [x]
c : s -> let l = replaceChar1 c in
(if isDigit c || c `elem` "_'" then [x, c]
else l) ++ concatMap replaceChar1 s
-- | injective replacement of special characters
replaceChar :: Char -> String
replaceChar c = if isIsaChar c then [c] else let n = ord c in
if n <= 32 || n >= 127 && n < 160 || n > 255 then "Slash_" ++ show n