{- |
Module : ./Isabelle/Translate.hs
Description : create legal Isabelle mixfix identifier
Copyright : (c) University of Cambridge, Cambridge, England
adaption (c) Till Mossakowski, Uni Bremen 2002-2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
translate 'Id' to Isabelle strings
-}
module Isabelle.Translate
( showIsaConstT, showIsaConstIT, showIsaTypeT, transConstStringT
, transTypeStringT
, mkIsaConstT, mkIsaConstIT, transString, isaPrelude
, IsaPreludes (..)
, getConstIsaToks ) where
import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Id
import Common.ProofUtils
import Common.Utils
import qualified Common.Lib.Rel as Rel
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Char
import Data.Maybe
import Data.List
import Isabelle.IsaSign
import Isabelle.IsaConsts
import Isabelle.IsaStrings
-- ----------------- Id translation functions -------------------
data IsaPreludes = IsaPreludes
isaKeyset :: Set.Set String
isaKeyset = Set.fromList isaKeywords
mkPreludeMap = Map.fromList . map (\ (b, s) -> (b, Set.union s isaKeyset))
hc2isaNames :: [String]
hc2isaNames =
[ defOpS, "mapSnd", "mapFst", "lift2partial", "lift2bool"
, "lift2unit", "liftUnit", "liftUnit2partial", "liftUnit2bool"
, "liftUnit2unit", "bool2partial", "curryOp", "uncurryOp", "unpack2bool"
, "partial2bool", "unpack2partial", "unpackBool", "unpackPartial"
, "resOp", "whenElseOp", "exEqualOp", "existEqualOp", "ifImplOp", "flip"
, "makePartial", "makeTotal", "noneOp", "strongEqualOp", "restrictOp"]
isaPrelude :: IsaPreludes
isaPrelude = IsaPreludes
{ preTypes = mkPreludeMap
[ (HsHOL_thy, types mainS)
, (HsHOLCF_thy, types holcfS)
, (MainHC_thy, types mainS)
, (MainHCPairs_thy, types mainS)
, (Main_thy, types mainS)
, (HOLCF_thy, types holcfS)]
, preConsts = mkPreludeMap
[ (HsHOL_thy, consts mainS)
, (HsHOLCF_thy, Set.insert fliftbinS (consts holcfS))
, (MainHC_thy, foldr Set.insert (consts mainS)
$ [ pAppS, aptS, appS, pairC ] ++ hc2isaNames)
, (MainHCPairs_thy, foldr Set.insert (consts mainS) hc2isaNames)
, (Main_thy, consts mainS), (HOLCF_thy, consts holcfS)]}
getAltTokenList :: String -> Int -> Id -> BaseSig -> [Token]
getAltTokenList newPlace over i@(Id ms cs qs) thy = let
(fs, ps) = splitMixToken ms
nonPlaces = filter (not . isPlace) fs
constSet = Map.findWithDefault Set.empty thy $ preConsts isaPrelude
over2 = isSingle nonPlaces && Set.member (tokStr $ head nonPlaces)
constSet || Set.member (show i) constSet
o1 = if over2 && over == 0 then over + 1 else over
newFs =
let (fps, rts) = span isPlace fs in case rts of
hd : tl | o1 > 0 -> fps ++ mkSimpleId (tokStr hd ++
if o1 < 3 then replicate o1 '\'' else '_' : show o1)
: tl
_ -> fs
in getTokenList newPlace $ Id (newFs ++ ps) cs qs
toAltSyntax :: Bool -> Int -> GlobalAnnos -> Int -> Id -> BaseSig
-> Set.Set String -> Maybe AltSyntax
toAltSyntax prd over ga n i thy toks = let
(precMap, mx) = Rel.toPrecMap $ prec_annos ga
minPrec = if prd then 42 else 52
adjustPrec p = 2 * p + minPrec
br = "/ "
newPlace = br ++ "_"
minL = replicate n lowPrio
minL1 = tail minL
minL2 = tail minL1
ni = placeCount i
atoks@(hd : tl) = getAltTokenList newPlace over i thy
compoundToks = map (: []) ",[]{}"
convert Token { tokStr = s } =
if elem s $ newPlace : compoundToks then s else br ++ quote s
tts = concatMap convert tl
ht = let chd = convert hd in
if isPrefixOf br chd then drop (length br) chd else chd
ts = ht ++ tts
(precList, erg)
| isInfix i = case Map.lookup i precMap of
Just p -> let
q = adjustPrec p
(l, r) = case Map.lookup i $ assoc_annos ga of
Nothing -> (q + 1, q + 1)
Just ALeft -> (q, q + 1)
Just ARight -> (q + 1, q)
in (l : minL2 ++ [r], q)
Nothing -> let q = adjustPrec $ mx + 1 in (q : minL2 ++ [q], minPrec)
| begPlace i = let q = adjustPrec $ mx + 3 in (q : minL1 , q)
| endPlace i = let q = adjustPrec $ mx + 2 in (minL1 ++ [q], q)
| otherwise = (minL, maxPrio - 1)
in if n < 0 || ni > 1 && ni /= n
|| any (flip Set.member toks . tokStr) atoks then Nothing
else Just $ if n == 0 then AltSyntax ts [] maxPrio
else if isMixfix i then AltSyntax
('(' : ts ++ ")") precList erg
else AltSyntax
(ts ++ "/'(" ++
concat (replicate (n - 1) "_,/ ")
++ "_')") (replicate n 3) $ maxPrio - 1
quote :: String -> String
quote l = case l of
[] -> l
c : r -> (if elem c "_/'()" then '\'' : [c]
else if elem c "\\\"" then '\\' : [c] else [c]) ++ quote r
showIsaT1 :: (String -> String) -> Id -> String
showIsaT1 tr ide = let
str = tr $ show ide
in if null str then error "showIsaT1" else if
elem (last str) "_" then str ++ "X" else str
showIsaConstT :: Id -> BaseSig -> String
showIsaConstT ide thy = showIsaT1 (transConstStringT thy) ide
-- also pass number of arguments
mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set.Set String
-> VName
mkIsaConstT = mkIsaConstVName 0 showIsaConstT
mkIsaConstVName :: Int -> (Id -> BaseSig -> String) -> Bool -> GlobalAnnos
-> Int -> Id -> BaseSig -> Set.Set String -> VName
mkIsaConstVName over f prd ga n ide thy toks =
let s = f ide thy
a = toAltSyntax prd over ga n ide thy toks
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
-> Set.Set String -> VName
mkIsaConstIT prd ga n ide i =
mkIsaConstVName i (`showIsaConstIT` 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 =
foldr (Set.insert . tokStr)
Set.empty . getAltTokenList "" i ide
transIsaInternalName :: String -> String
transIsaInternalName s = if last s == '_' then s ++ "X" else s
-> 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
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 lookupCharMap c