697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder{- |

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederModule : $Header$

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederDescription : create legal Isabelle mixfix identifier

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederCopyright : (c) University of Cambridge, Cambridge, England

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu adaption (c) Till Mossakowski, Uni Bremen 2002-2005

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederMaintainer : Christian.Maeder@dfki.de

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederStability : provisional

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederPortability : portable

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maedertranslate 'Id' to Isabelle strings

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder-}

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maedermodule Isabelle.Translate

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ( showIsaConstT, showIsaConstIT, showIsaTypeT, transConstStringT

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder , transTypeStringT

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder , mkIsaConstT, mkIsaConstIT, transString, isaPrelude

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder , IsaPreludes (..)

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder , getConstIsaToks ) where

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder

8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maederimport Common.AS_Annotation

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Common.GlobalAnnotations

a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian Maederimport Common.Id

8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maederimport Common.ProofUtils

8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maederimport Common.Utils

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maederimport qualified Common.Lib.Rel as Rel

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzimport qualified Data.Map as Map

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzimport qualified Data.Set as Set

0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder

0789323dfca89bae8f710da5bba20220b9af2feaChristian Maederimport Data.Char

0789323dfca89bae8f710da5bba20220b9af2feaChristian Maederimport Data.Maybe

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maederimport Data.List

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder

0789323dfca89bae8f710da5bba20220b9af2feaChristian Maederimport Isabelle.IsaSign

0789323dfca89bae8f710da5bba20220b9af2feaChristian Maederimport Isabelle.IsaConsts

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maederimport Isabelle.IsaStrings

248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder

5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder-- ----------------- Id translation functions -------------------

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maederdata IsaPreludes = IsaPreludes

5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder { preTypes :: Map.Map BaseSig (Set.Set String)

248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder , preConsts :: Map.Map BaseSig (Set.Set String) }

0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder

0789323dfca89bae8f710da5bba20220b9af2feaChristian MaederisaKeyset :: Set.Set String

0789323dfca89bae8f710da5bba20220b9af2feaChristian MaederisaKeyset = Set.fromList isaKeywords

0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian MaedermkPreludeMap :: [(BaseSig, Set.Set String)] -> Map.Map BaseSig (Set.Set String)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedermkPreludeMap = Map.fromList . map (\ (b, s) -> (b, Set.union s isaKeyset))

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder

6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulzhc2isaNames :: [String]

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maederhc2isaNames =

6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz [ defOpS, "mapSnd", "mapFst", "lift2partial", "lift2bool"

6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz , "lift2unit", "liftUnit", "liftUnit2partial", "liftUnit2bool"

6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz , "liftUnit2unit", "bool2partial", "curryOp", "uncurryOp", "unpack2bool"

6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz , "partial2bool", "unpack2partial", "unpackBool", "unpackPartial"

6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz , "resOp", "whenElseOp", "exEqualOp", "existEqualOp", "ifImplOp", "flip"

6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz , "makePartial", "makeTotal", "noneOp", "strongEqualOp", "restrictOp"]

6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz

5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaederisaPrelude :: IsaPreludes

5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaederisaPrelude = IsaPreludes

5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder { preTypes = mkPreludeMap

5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder [ (HsHOL_thy, types mainS)

5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder , (HsHOLCF_thy, types holcfS)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder , (MainHC_thy, types mainS)

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder , (MainHCPairs_thy, types mainS)

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder , (Main_thy, types mainS)

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder , (HOLCF_thy, types holcfS)]

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder , preConsts = mkPreludeMap

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder [ (HsHOL_thy, consts mainS)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder , (HsHOLCF_thy, Set.insert fliftbinS (consts holcfS))

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder , (MainHC_thy, foldr Set.insert (consts mainS)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder $ [ pAppS, aptS, appS, pairC ] ++ hc2isaNames)

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder , (MainHCPairs_thy, foldr Set.insert (consts mainS) hc2isaNames)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder , (Main_thy, consts mainS), (HOLCF_thy, consts holcfS)]}

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedergetAltTokenList :: String -> Int -> Id -> BaseSig -> [Token]

b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian MaedergetAltTokenList newPlace over i@(Id ms cs qs) thy = let

b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder (fs, ps) = splitMixToken ms

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder nonPlaces = filter (not . isPlace) fs

b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder constSet = Map.findWithDefault Set.empty thy $ preConsts isaPrelude

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder over2 = isSingle nonPlaces && Set.member (tokStr $ head nonPlaces)

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder constSet || Set.member (show i) constSet

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder o1 = if over2 && over == 0 then over + 1 else over

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder newFs =

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder let (fps, rts) = span isPlace fs in case rts of

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder hd : tl | o1 > 0 -> fps ++ mkSimpleId (tokStr hd ++

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder if o1 < 3 then replicate o1 '\'' else '_' : show o1)

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder : tl

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder _ -> fs

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder in getTokenList newPlace $ Id (newFs ++ ps) cs qs

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedertoAltSyntax :: Bool -> Int -> GlobalAnnos -> Int -> Id -> BaseSig

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder -> Set.Set String -> Maybe AltSyntax

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedertoAltSyntax prd over ga n i thy toks = let

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder (precMap, mx) = Rel.toPrecMap $ prec_annos ga

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder minPrec = if prd then 42 else 52

429df04296fa571432f62cbfad6855e1420e0fd6Christian Maeder adjustPrec p = 2 * p + minPrec

429df04296fa571432f62cbfad6855e1420e0fd6Christian Maeder br = "/ "

429df04296fa571432f62cbfad6855e1420e0fd6Christian Maeder newPlace = br ++ "_"

429df04296fa571432f62cbfad6855e1420e0fd6Christian Maeder minL = replicate n lowPrio

fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst Schulz minL1 = tail minL

fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst Schulz minL2 = tail minL1

fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst Schulz ni = placeCount i

a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian Maeder atoks@(hd : tl) = getAltTokenList newPlace over i thy

fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst Schulz compoundToks = map (: []) ",[]{}"

fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst Schulz convert Token { tokStr = s } =

b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder if elem s $ newPlace : compoundToks then s else br ++ quote s

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder tts = concatMap convert tl

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ht = let chd = convert hd in

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder if isPrefixOf br chd then drop (length br) chd else chd

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ts = ht ++ tts

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder (precList, erg)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder | isInfix i = case Map.lookup i precMap of

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder Just p -> let

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder q = adjustPrec p

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder (l, r) = case Map.lookup i $ assoc_annos ga of

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder Nothing -> (q + 1, q + 1)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder Just ALeft -> (q, q + 1)

92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder Just ARight -> (q + 1, q)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder in (l : minL2 ++ [r], q)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder Nothing -> let q = adjustPrec $ mx + 1 in (q : minL2 ++ [q], minPrec)

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder | begPlace i = let q = adjustPrec $ mx + 3 in (q : minL1 , q)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder | endPlace i = let q = adjustPrec $ mx + 2 in (minL1 ++ [q], q)

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder | otherwise = (minL, maxPrio - 1)

14d7908303969441ba30c2748de45f20345c6b31Christian Maeder in if n < 0 || ni > 1 && ni /= n

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder || any (flip Set.member toks . tokStr) atoks then Nothing

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder else if n == 0 then Just $ AltSyntax ts [] maxPrio

b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder else if isMixfix i then Just $ AltSyntax

b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder ('(' : ts ++ ")") precList erg

b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder else Just $ AltSyntax

b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder (ts ++ "/'(" ++

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder concat (replicate (n - 1) "_,/ ")

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder ++ "_')") (replicate n 3) $ maxPrio - 1

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maederquote :: String -> String

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maederquote l = case l of

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder [] -> l

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder c : r -> (if elem c "_/'()" then '\'' : [c]

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder else if elem c "\\\"" then '\\' : [c] else [c]) ++ quote r

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedershowIsaT1 :: (String -> String) -> Id -> String

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedershowIsaT1 tr ide = let

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder str = tr $ show ide

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder in if null str then error "showIsaT1" else if

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder elem (last str) "_" then str ++ "X" else str

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedershowIsaConstT :: Id -> BaseSig -> String

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedershowIsaConstT ide thy = showIsaT1 (transConstStringT thy) ide

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder

248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder-- also pass number of arguments

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedermkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set.Set String

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder -> VName

a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian MaedermkIsaConstT = mkIsaConstVName 0 showIsaConstT

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedermkIsaConstVName :: Int -> (Id -> BaseSig -> String) -> Bool -> GlobalAnnos

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder -> Int -> Id -> BaseSig -> Set.Set String -> VName

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedermkIsaConstVName over f prd ga n ide thy toks =

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder let s = f ide thy

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder a = toAltSyntax prd over ga n ide thy toks

54a535fb81b928ac8f99a11bdcfa8998533204a5Christian Maeder in if n == 0 && case a of

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz Just (AltSyntax as [] _) -> as == s

e2e5830e2562de2f9a7daa31704fca25285180f0Ewaryst Schulz _ -> False then VName { new = s, altSyn = Nothing }

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz else VName

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz { new = (if n < 0 || isMixfix ide || s /= show ide then id else ("X_" ++)) s

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz , altSyn = a }

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz

9029484754c7b2037321e7cbd077580866845265Christian MaedershowIsaTypeT :: Id -> BaseSig -> String

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst SchulzshowIsaTypeT ide thy = showIsaT1 (transTypeStringT thy) ide

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz

e2e5830e2562de2f9a7daa31704fca25285180f0Ewaryst Schulz-- | add a number for overloading

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst SchulzshowIsaConstIT :: Id -> Int -> BaseSig -> String

e2e5830e2562de2f9a7daa31704fca25285180f0Ewaryst SchulzshowIsaConstIT ide i thy = showIsaConstT ide thy ++ "X" ++ show i

e2e5830e2562de2f9a7daa31704fca25285180f0Ewaryst Schulz

e2e5830e2562de2f9a7daa31704fca25285180f0Ewaryst SchulzmkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz -> Set.Set String -> VName

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst SchulzmkIsaConstIT prd ga n ide i =

9029484754c7b2037321e7cbd077580866845265Christian Maeder mkIsaConstVName i (`showIsaConstIT` i) prd ga n ide

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz{- | get the tokens of the alternative syntax that should not be used

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz as variables -}

8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaedergetConstIsaToks :: Id -> Int -> BaseSig -> Set.Set String

8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaedergetConstIsaToks ide i thy = if i < 2 then

8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder Set.union (getConstIsaToksAux ide 0 thy) (getConstIsaToksAux ide 1 thy)

8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder else getConstIsaToksAux ide i thy

8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder

8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaedergetConstIsaToksAux :: Id -> Int -> BaseSig -> Set.Set String

8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaedergetConstIsaToksAux ide i =

8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder foldr (Set.insert . tokStr)

8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder Set.empty . getAltTokenList "" i ide

transIsaInternalName :: String -> String

transIsaInternalName s = if last s == '_' then s ++ "X" else s

transIsaStringT :: Map.Map BaseSig (Set.Set String) -> BaseSig

-> String -> String

transIsaStringT m i s = let t = transStringAux False s in

transIsaInternalName $ if Set.member t

$ fromMaybe (error "Isabelle.transIsaStringT") $ Map.lookup i m

then transIsaStringT m i $ '_' : s else t

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 || elem c "_'"

-- | translate to a valid Isabelle string possibly non-injectively

transString :: String -> String

transString = transStringAux True

-- | if true don't try to be injective

transStringAux :: Bool -> String -> String

transStringAux b str = let

x = 'X'

replaceChar1 d | not b && d == x = [x, x] -- code out existing X!

| b && d == ' ' = "_"

| isIsaChar d = [d]

| otherwise = x : replaceChar d

in case str of

"" -> error "transString"

c : s -> let l = replaceChar1 c in

(if isDigit c || elem c "_'" then [x, c]

else l) ++ concatMap replaceChar1

(if b then replace "' '" "'Space'" s else s)

-- | injective replacement of special characters

replaceChar :: Char -> String

-- <http://www.htmlhelp.com/reference/charset/>

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

else fromMaybe (error "Isabelle.replaceChar") $ Map.lookup c charMap