4752N/A{- |

4752N/AModule : $Header$

4752N/ADescription : create legal Isabelle mixfix identifier

4752N/ACopyright : (c) University of Cambridge, Cambridge, England

4752N/A adaption (c) Till Mossakowski, Uni Bremen 2002-2005

4752N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4752N/A

4752N/AMaintainer : Christian.Maeder@dfki.de

4752N/AStability : provisional

4752N/APortability : portable

6982N/A

6982N/Atranslate 'Id' to Isabelle strings

4752N/A-}

4752N/A

4752N/Amodule Isabelle.Translate

4752N/A ( showIsaConstT, showIsaConstIT, showIsaTypeT, transConstStringT

6982N/A , mkIsaConstT, mkIsaConstIT, transString, isaPrelude, IsaPreludes

6982N/A , getConstIsaToks ) where

6982N/A

6982N/Aimport Common.Id

4752N/Aimport Common.ProofUtils

4752N/Aimport Common.GlobalAnnotations

4752N/Aimport Common.AS_Annotation

4752N/A

4752N/Aimport qualified Data.Map as Map

5821N/Aimport qualified Data.Set as Set

4752N/Aimport qualified Common.Lib.Rel as Rel

4752N/Aimport Data.Char

4752N/A

4752N/Aimport Isabelle.IsaSign

4752N/Aimport Isabelle.IsaConsts

4752N/Aimport Isabelle.IsaStrings

4752N/A

4752N/A------------------- Id translation functions -------------------

4752N/Adata IsaPreludes = IsaPreludes

4752N/A { preTypes :: Map.Map BaseSig (Set.Set String)

4752N/A , preConsts :: Map.Map BaseSig (Set.Set String) }

4752N/A

4752N/AisaKeyset :: Set.Set String

4752N/AisaKeyset = Set.fromList isaKeywords

4752N/A

4752N/AmkPreludeMap :: [(BaseSig, Set.Set String)] -> Map.Map BaseSig (Set.Set String)

4752N/AmkPreludeMap = Map.fromList . map (\ (b, s) -> (b, Set.union s isaKeyset))

4752N/A

4752N/AisaPrelude :: IsaPreludes

4752N/AisaPrelude = IsaPreludes {

4752N/A preTypes = mkPreludeMap

4752N/A [(HsHOL_thy, types mainS),

4752N/A (HsHOLCF_thy, types holcfS), (MainHC_thy, types mainS),

4752N/A (Main_thy, types mainS), (HOLCF_thy, types holcfS)],

4752N/A preConsts = mkPreludeMap

4752N/A [(HsHOL_thy, consts mainS),

4752N/A (HsHOLCF_thy, Set.insert fliftbinS (consts holcfS)),

4752N/A (MainHC_thy, foldr Set.insert (consts mainS)

4752N/A [pAppS, aptS, appS, defOpS, pairC]),

4752N/A (Main_thy, consts mainS), (HOLCF_thy, consts holcfS)]}

4752N/A

4752N/AgetAltTokenList :: String -> Int -> Id -> BaseSig -> [Token]

4752N/AgetAltTokenList newPlace over i@(Id ms cs qs) thy = let

4752N/A (fs, ps) = splitMixToken ms

4752N/A nonPlaces = filter (not . isPlace) fs

4752N/A constSet = Map.findWithDefault Set.empty thy $ preConsts isaPrelude

4752N/A over2 = isSingle nonPlaces && Set.member (tokStr $ head nonPlaces)

4752N/A constSet || Set.member (show i) constSet

4752N/A o1 = if over2 && over == 0 then over + 1 else over

4752N/A newFs = if null fs || not over2 && over == 0 then fs else

4752N/A init fs ++ [mkSimpleId $

4752N/A tokStr (last fs) ++

4752N/A if o1 < 3 then replicate o1 '\'' else '_' : show o1]

4752N/A in getTokenList newPlace $ Id (newFs ++ ps) cs qs

4752N/A

4752N/AtoAltSyntax :: Bool -> Int -> GlobalAnnos -> Int -> Id -> BaseSig

4752N/A -> Maybe AltSyntax

4752N/AtoAltSyntax prd over ga n i thy = let

4752N/A (precMap, mx) = Rel.toPrecMap $ prec_annos ga

4752N/A minPrec = if prd then 42 else 52

4752N/A adjustPrec p = 2 * p + minPrec

4752N/A newPlace = "/ _"

4752N/A minL = replicate n lowPrio

4752N/A minL1 = tail minL

4752N/A minL2 = tail minL1

4752N/A ni = placeCount i

4752N/A hd : tl = getAltTokenList newPlace over i thy

4752N/A convert = \ Token { tokStr = s } -> if s == newPlace then s

4752N/A else "/ " ++ quote s

4752N/A tts = concatMap convert tl

4752N/A ht = drop 2 $ convert hd

4752N/A ts = ht ++ tts

4752N/A (precList, erg) = if isInfix i then case Map.lookup i precMap of

4752N/A Just p -> let

4752N/A q = adjustPrec p

4752N/A (l, r) = case Map.lookup i $ assoc_annos ga of

4752N/A Nothing -> (q + 1, q + 1)

4752N/A Just ALeft -> (q, q + 1)

4752N/A Just ARight -> (q + 1, q)

4752N/A in (l : minL2 ++ [r], q)

4752N/A Nothing -> let q = adjustPrec $ mx + 1 in (q : minL2 ++ [q], minPrec)

4752N/A else if begPlace i then let q = adjustPrec $ mx + 3 in (q : minL1 , q)

4752N/A else if endPlace i then let q = adjustPrec $ mx + 2 in (minL1 ++ [q], q)

4752N/A else (minL, maxPrio - 1)

4752N/A in if n < 0 || ni > 1 && ni /= n then Nothing

4752N/A else if n == 0 then Just $ AltSyntax ts [] maxPrio

4752N/A else if isMixfix i then Just $ AltSyntax

4752N/A ('(' : ts ++ ")") precList erg

4752N/A else Just $ AltSyntax

4752N/A (ts ++ "/'(" ++

4752N/A concat (replicate (n - 1) "_,/ ")

4752N/A ++ "_')") (replicate n 3) $ maxPrio - 1

4752N/A

4752N/Aquote :: String -> String

4752N/Aquote l = case l of

4752N/A [] -> l

4752N/A c : r -> (if elem c "_/'()" then '\'' : [c]

4752N/A else if elem c "\\\"" then '\\' : [c] else [c]) ++ quote r

5821N/A

4752N/AshowIsaT1 :: (String -> String) -> Id -> String

4752N/AshowIsaT1 tr ide = let

4752N/A str = tr $ show ide

4752N/A in if null str then error "showIsaT1" else if

4752N/A elem (last str) "_" then str ++ "X" else str

4752N/A

4752N/AshowIsaConstT :: Id -> BaseSig -> String

4752N/AshowIsaConstT ide thy = showIsaT1 (transConstStringT thy) ide

4752N/A

4752N/A-- also pass number of arguments

4752N/AmkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> VName

4752N/AmkIsaConstT prd ga n ide = mkIsaConstVName 0 showIsaConstT prd ga n ide

4752N/A

4752N/AmkIsaConstVName :: Int -> (Id -> BaseSig -> String) -> Bool -> GlobalAnnos

4752N/A -> Int -> Id -> BaseSig -> VName

4752N/AmkIsaConstVName over f prd ga n ide thy =

4752N/A let s = f ide thy

4752N/A a = toAltSyntax prd over ga n ide thy

4752N/A in if n == 0 && case a of

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

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

else VName

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

, altSyn = a }

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 ++ "X" ++ show i

mkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig -> VName

mkIsaConstIT prd ga n ide i =

mkIsaConstVName i ( \ ide' -> showIsaConstIT ide' i) prd ga n ide

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

as variables -}

getConstIsaToks :: Id -> Int -> BaseSig -> Set.Set String

getConstIsaToks ide i thy = if i < 2 then

Set.union (getConstIsaToksAux ide 0 thy) (getConstIsaToksAux ide 1 thy)

else getConstIsaToksAux ide i thy

getConstIsaToksAux :: Id -> Int -> BaseSig -> Set.Set String

getConstIsaToksAux ide i thy =

foldr (Set.insert . tokStr)

Set.empty $ getAltTokenList "" i ide thy

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

-> String -> String

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

if Set.member t $ maybe (error "Isabelle.transIsaStringT") id

$ 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 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 maybe (error "Isabelle.replaceChar") id $ Map.lookup c charMap