Translate.hs revision 2654a161816b814311b1ad23f12ab304cdffb132
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederModule : $Header$
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederCopyright : (c) University of Cambridge, Cambridge, England
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder adaption (c) Till Mossakowski, Uni Bremen 2002-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederMaintainer : maeder@tzi.de
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederStability : provisional
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederPortability : portable
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maedertranslate 'Id' to Isabelle strings
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder ( showIsaConstT, showIsaConstIT, showIsaTypeT, transConstStringT
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maeder , mkIsaConstT, mkIsaConstIT, transString, isaPrelude, toAltSyntax
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maederimport qualified Common.Lib.Map as Map
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maederimport qualified Common.Lib.Set as Set
33f5512f0538c5ec4141205a8440ff6ba9e96139Christian Maederimport qualified Common.Lib.Rel as Rel
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder------------------- Id translation functions -------------------
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederdata IsaPreludes = IsaPreludes
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder { preTypes :: Map.Map BaseSig (Set.Set String)
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder , preConsts :: Map.Map BaseSig (Set.Set String) }
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian MaederisaPrelude :: IsaPreludes
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian MaederisaPrelude = IsaPreludes {
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder [(HsHOLCF_thy, types holcfS), (MainHC_thy, types mainS),
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder (Main_thy, types mainS), (HOLCF_thy, types holcfS)],
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder [(HsHOLCF_thy, Set.insert "fliftbin" (consts holcfS)),
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder (MainHC_thy, foldr Set.insert (consts mainS)
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder ["pApp","apt","app","defOp","pair"]),
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder (Main_thy, consts mainS), (HOLCF_thy, consts holcfS)]}
0789323dfca89bae8f710da5bba20220b9af2feaChristian MaedertoAltSyntax :: GlobalAnnos -> Id -> Maybe AltSyntax
720eeee7c9d8442093c8d05bed743193eee906e0Christian MaedertoAltSyntax ga i = let
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder (precMap, mx) = Rel.toPrecMap $ prec_annos ga
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder adjustPrec p = 2 * p + minPrec
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder newPlace = "/ _"
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder minL = replicate (placeCount i) minPrec
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder minL1 = tail minL
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder minL2 = tail minL1
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder hd : tl = getTokenList newPlace i
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder convert = \ Token { tokStr = s } -> if s == newPlace then s
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder (precList, erg) = if isInfix i then case Map.lookup i precMap of
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder Just p -> let
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maeder q = adjustPrec p
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder (l, r) = case Map.lookup i $ assoc_annos ga of
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder Nothing -> (q, q)
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder Just ALeft -> (q, q + 1)
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder Just ARight -> (q + 1, q)
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder in (l : minL2 ++ [r], q)
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder Nothing -> let q = adjustPrec $ mx + 1 in (q : minL2 ++ [q], minPrec)
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder else if begPlace i then let q = adjustPrec $ mx + 3 in (q : minL1 , q)
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder else if endPlace i then let q = adjustPrec $ mx + 2 in (minL1 ++ [q], q)
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder else (minL, adjustPrec $ mx + 4)
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder in if isMixfix i then Just $ AltSyntax
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder ('(' : (if begPlace i then "_ " else convert hd)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ++ concatMap convert tl ++ ")") precList erg
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maederquote :: String -> String
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maederquote l = case l of
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder c : r -> (if c `elem` "_/'" then '\'' : [c] else [c]) ++ quote r
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedershowIsaT1 :: (String -> String) -> Id -> String
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedershowIsaT1 tr ide = let
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder rdru = reverse . dropWhile (== '_')
1596a4d2cc01bff500afdd3789a43ec93210e81fChristian Maeder str = show ide
1596a4d2cc01bff500afdd3789a43ec93210e81fChristian Maeder in if isInfix2 ide then "XX" ++ tr (rdru $ rdru str) else tr str
429df04296fa571432f62cbfad6855e1420e0fd6Christian MaedershowIsaConstT :: Id -> BaseSig -> String
fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst SchulzshowIsaConstT ide thy = showIsaT1 (transConstStringT thy) ide
fbc1e851413f39999a00a0d3be0edf75bbf42007Ewaryst SchulzmkIsaConstT :: GlobalAnnos -> Id -> BaseSig -> VName
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian MaedermkIsaConstT = mkIsaConstVName showIsaConstT
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedermkIsaConstVName :: (Id -> BaseSig -> String) -> GlobalAnnos -> Id -> BaseSig
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedermkIsaConstVName f ga ide thy = VName { new = f ide thy
14d7908303969441ba30c2748de45f20345c6b31Christian Maeder , altSyn = toAltSyntax ga ide }
54a535fb81b928ac8f99a11bdcfa8998533204a5Christian MaedershowIsaTypeT :: Id -> BaseSig -> String
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian MaedershowIsaTypeT ide thy = showIsaT1 (transTypeStringT thy) ide
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian Maeder-- | add a number for overloading
b410420153cc9ac37fb4ebb86699cba7fa19bc35Christian MaedershowIsaConstIT :: Id -> Int -> BaseSig -> String
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedershowIsaConstIT ide i thy = showIsaConstT ide thy ++ "_" ++ show i
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedermkIsaConstIT :: GlobalAnnos -> Id -> Int -> BaseSig -> VName
db6729e623b4053149084ccf4b35e5308ac7e359Christian MaedermkIsaConstIT ga ide i = mkIsaConstVName
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ( \ ide' -> showIsaConstIT ide' i) ga ide
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian MaedertransIsaStringT :: Map.Map BaseSig (Set.Set String) -> BaseSig
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder -> String -> String
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedertransIsaStringT m i s = let t = transString s in
a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian Maeder if Set.member t $ maybe (error "Isabelle.transIsaStringT") id
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder then t ++ "X" else t
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedertransConstStringT :: BaseSig -> String -> String
720eeee7c9d8442093c8d05bed743193eee906e0Christian MaedertransConstStringT = transIsaStringT $ preConsts isaPrelude
831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst SchulztransTypeStringT :: BaseSig -> String -> String
831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst SchulztransTypeStringT = transIsaStringT $ preTypes isaPrelude
8acac20a235839e60ea2d43709fce47de1c68bc1Christian Maeder-- | check for legal alphanumeric isabelle characters
8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaederisIsaChar :: Char -> Bool
8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaederisIsaChar c = isAlphaNum c && isAscii c || c `elem` "_'"
8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaedertransString :: String -> String
8acac20a235839e60ea2d43709fce47de1c68bc1Christian MaedertransString str = let