Translate.hs revision 0a4b45d334a2ce05c65500fffe5a23adc96a9a76
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederModule : $Header$
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederCopyright : (c) University of Cambridge, Cambridge, England
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder adaption (c) Till Mossakowski, Uni Bremen 2002-2005
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederLicense : 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
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ( showIsaConstT, showIsaConstIT, showIsaTypeT, transConstStringT
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder , mkIsaConstT, mkIsaConstIT, transString, isaPrelude
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maederimport qualified Common.Lib.Map as Map
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maederimport qualified Common.Lib.Set as Set
0789323dfca89bae8f710da5bba20220b9af2feaChristian Maederimport qualified Common.Lib.Rel as Rel
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder------------------- Id translation functions -------------------
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maederdata IsaPreludes = IsaPreludes
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder { preTypes :: Map.Map BaseSig (Set.Set String)
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder , preConsts :: Map.Map BaseSig (Set.Set String) }
0789323dfca89bae8f710da5bba20220b9af2feaChristian MaederisaKeyset :: Set.Set String
0789323dfca89bae8f710da5bba20220b9af2feaChristian MaederisaKeyset = Set.fromList isaKeywords
0789323dfca89bae8f710da5bba20220b9af2feaChristian MaedermkPreludeMap :: [(BaseSig, Set.Set String)] -> Map.Map BaseSig (Set.Set String)
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian MaedermkPreludeMap = Map.fromList . map (\ (b, s) -> (b, Set.union s isaKeyset))
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederisaPrelude :: IsaPreludes
6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst SchulzisaPrelude = IsaPreludes {
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder preTypes = mkPreludeMap
6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz [(HsHOL_thy, types mainS),
6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz (HsHOLCF_thy, types holcfS), (MainHC_thy, types mainS),
6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz (Main_thy, types mainS), (HOLCF_thy, types holcfS)],
6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz preConsts = mkPreludeMap
6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz [(HsHOL_thy, consts mainS),
6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz (HsHOLCF_thy, Set.insert fliftbinS (consts holcfS)),
6df66a8a7be47ca0d9a4d15b89d3380c8e1f4aedEwaryst Schulz (MainHC_thy, foldr Set.insert (consts mainS)
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder [pAppS, aptS, appS, defOpS, pairC]),
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder (Main_thy, consts mainS), (HOLCF_thy, consts holcfS)]}
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedertoAltSyntax :: Bool -> Int -> GlobalAnnos -> Int -> Id -> BaseSig
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder -> Maybe AltSyntax
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedertoAltSyntax prd over ga n i@(Id ms cs qs) thy = let
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder (precMap, mx) = Rel.toPrecMap $ prec_annos ga
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder minPrec = if prd then 42 else 52
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder adjustPrec p = 2 * p + minPrec
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder newPlace = "/ _ "
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder minL = replicate n lowPrio
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder minL1 = tail minL
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder minL2 = tail minL1
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder (fs, ps) = splitMixToken ms
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder nonPlaces = filter (not . isPlace) fs
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder constSet = Map.findWithDefault Set.empty thy $ preConsts isaPrelude
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder over2 = if isSingle nonPlaces && Set.member (tokStr $ head nonPlaces)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder constSet || Set.member (show i) constSet
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder then over + 1 else over
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder newFs = if null fs || over2 < 2 then fs else
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder fs ++ [mkSimpleId $ let o1 = over2 - 1 in
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder if over2 < 4 then replicate o1 '\'' else '_' : show o1]
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder (hd : tl) = getTokenList newPlace $ Id (newFs ++ ps) cs qs
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder tts = (if endPlace i then init else id) $ concatMap convert tl
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ht = convert hd
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ts = ht ++ tts
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder convert = \ Token { tokStr = s } -> if s == newPlace then s
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder (precList, erg) = if isInfix i then case Map.lookup i precMap of
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder Just p -> let
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder q = adjustPrec p
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder (l, r) = case Map.lookup i $ assoc_annos ga of
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder Nothing -> (q + 1, q + 1)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Just ALeft -> (q, q + 1)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder Just ARight -> (q + 1, q)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder in (l : minL2 ++ [r], q)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Nothing -> let q = adjustPrec $ mx + 1 in (q : minL2 ++ [q], minPrec)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder else if begPlace i then let q = adjustPrec $ mx + 3 in (q : minL1 , q)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder else if endPlace i then let q = adjustPrec $ mx + 2 in (minL1 ++ [q], q)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder else (minL, maxPrio - 1)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder in if n == 0 then Just $ AltSyntax ts [] maxPrio
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder else if isMixfix i then Just $ AltSyntax
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ('(' : (if begPlace i then "_ " else ht)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder ++ tts ++ ")") precList erg
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder else Just $ AltSyntax
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder (ts ++ "'(" ++
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder concat (replicate (n - 1) "_,/ ")
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maeder ++ "_')") minL $ maxPrio - 1
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maederquote :: String -> String
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maederquote l = case l of
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder c : r -> (if c `elem` "_/'()" then '\'' : [c]
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder else if c `elem` "\\\"" then '\\' : [c] else [c]) ++ quote r
14d7908303969441ba30c2748de45f20345c6b31Christian MaedershowIsaT1 :: (String -> String) -> Id -> String
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedershowIsaT1 tr ide = let
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder rdru = reverse . dropWhile (== '_')
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder str = show ide
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder in if isInfix2 ide then "XX" ++ tr (rdru $ rdru str) else tr str
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedershowIsaConstT :: Id -> BaseSig -> String
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedershowIsaConstT ide thy = showIsaT1 (transConstStringT thy) ide
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder-- also pass number of arguments
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedermkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> VName
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedermkIsaConstT = mkIsaConstVName 1 showIsaConstT
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedermkIsaConstVName :: Int -> (Id -> BaseSig -> String)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder -> Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> VName
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedermkIsaConstVName over f prd ga n ide thy = VName
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder { new = f ide thy
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder , altSyn = toAltSyntax prd over ga n ide thy }
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedershowIsaTypeT :: Id -> BaseSig -> String
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedershowIsaTypeT ide thy = showIsaT1 (transTypeStringT thy) ide
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder-- | add a number for overloading
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedershowIsaConstIT :: Id -> Int -> BaseSig -> String
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedershowIsaConstIT ide i thy = showIsaConstT ide thy ++ "_" ++ show i
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedermkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig -> VName
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedermkIsaConstIT prd ga n ide i thy =
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder {- if n == 0 || isPrefixOf "g__" (show ide)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder then mkVName $ showIsaConstIT ide i thy
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder mkIsaConstVName i ( \ ide' -> showIsaConstIT ide' i) prd ga n ide thy
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedertransIsaStringT :: Map.Map BaseSig (Set.Set String) -> BaseSig
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder -> String -> String
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaedertransIsaStringT m i s = let t = transString s in
$ Map.lookup i m