e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription: functions useful for all prover connections in Hets
d5fe06af711a6912ae028ebf873eada4ee8733f8Christian MaederCopyright : (c) Klaus Luettich, C. Maeder, Uni Bremen 2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichMaintainer : luecke@informatik.uni-bremen.de
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus LuettichStability : provisional
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiFunctions useful for all prover connections in Hets
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian MaederSome were moved from Isabelle.Translate and some others from
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich * generic names are added
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich * disambiguation of duplicate assigned names
87ab788adadc73fd49e3c762caee6a88f844a5bcChristian Maederis done by toThSens
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich * translation of special characters with the aid of the provided function
87ab788adadc73fd49e3c762caee6a88f844a5bcChristian Maederis done by prepareSenNames
0a943b3aa43eff8a8d5f42da56fa895e13c7040cKlaus LuettichWarning: all sentence names are disambiguated by adding a natural number.
0a943b3aa43eff8a8d5f42da56fa895e13c7040cKlaus LuettichIf that does not work for a certain reasoner you can hand in a function
0a943b3aa43eff8a8d5f42da56fa895e13c7040cKlaus Luettichwhich uses a different alghorithm.
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich-- | translate special characters in sentence names
87ab788adadc73fd49e3c762caee6a88f844a5bcChristian MaederprepareSenNames :: (String -> String) -> [Named a] -> [Named a]
e51568cd733ccb83a799f48f0802095e3f3a8d62Christian MaederprepareSenNames = map . reName
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich-- | disambiguate sentence names
0a943b3aa43eff8a8d5f42da56fa895e13c7040cKlaus LuettichdisambiguateSens :: Set.Set String -> [Named a] -> [Named a]
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian MaederdisambiguateSens =
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder genericDisambigSens 0 senAttr $ reName . const
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian Maeder-- | generically disambiguate lists with names
427aeade34f2771c0295250e9a94b89489bb9204Christian MaedergenericDisambigSens :: Int -> (a -> String) -> (String -> a -> a)
427aeade34f2771c0295250e9a94b89489bb9204Christian Maeder -> Set.Set String -> [a] -> [a]
427aeade34f2771c0295250e9a94b89489bb9204Christian MaedergenericDisambigSens _ _ _ _ [] = []
427aeade34f2771c0295250e9a94b89489bb9204Christian MaedergenericDisambigSens c sel upd nameSet (ax : rest) =
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian Maeder let name = sel ax in case Set.splitMember name nameSet of
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian Maeder (_, False, _) ->
427aeade34f2771c0295250e9a94b89489bb9204Christian Maeder ax : genericDisambigSens c sel upd (Set.insert name nameSet) rest
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian Maeder (_, _, greater) -> let
427aeade34f2771c0295250e9a94b89489bb9204Christian Maeder n = until (not . flip Set.member greater . (name ++) . ('_' :) . show)
427aeade34f2771c0295250e9a94b89489bb9204Christian Maeder (+ 1) (c + 1)
427aeade34f2771c0295250e9a94b89489bb9204Christian Maeder name' = name ++ '_' : show n
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian Maeder in upd name' ax :
427aeade34f2771c0295250e9a94b89489bb9204Christian Maeder genericDisambigSens n sel upd (Set.insert name' nameSet) rest
a129422b14eea673dc481d2553cec108e35e72efChristian MaedernameAndDisambiguate :: [Named a] -> [Named a]
a129422b14eea673dc481d2553cec108e35e72efChristian MaedernameAndDisambiguate = disambiguateSens Set.empty . nameSens
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich-- | name unlabeled axioms with "Axnnn"
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus LuettichnameSens :: [Named a] -> [Named a]
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder map (\ (sen, no) ->
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder if senAttr sen == "" then reName (const $ "Ax" ++ show no) sen else sen)
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian Maeder-- | collect the mapping of new to old names
433bc07a43dd58f7ca4c93b6ea5a026a2dcb114dChristian MaedercollectNameMapping :: [Named a] -> [Named a] -> Map.Map String String
433bc07a43dd58f7ca4c93b6ea5a026a2dcb114dChristian MaedercollectNameMapping ns os = if any (null . senAttr) os
433bc07a43dd58f7ca4c93b6ea5a026a2dcb114dChristian Maeder then error "Common.ProofUtils.collectNameMapping"
433bc07a43dd58f7ca4c93b6ea5a026a2dcb114dChristian Maeder else Map.fromList $ zipWith (\ n o -> (senAttr n, senAttr o)) ns os
72204f862232e7e51b0207bba020c1d781fa7798Christian MaederlookupCharMap :: Char -> String
72204f862232e7e51b0207bba020c1d781fa7798Christian MaederlookupCharMap c = Map.findWithDefault ("Slash_" ++ show (ord c)) c charMap
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich-- | a separate Map speeds up lookup
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus LuettichcharMap :: Map.Map Char String
10a655fc665d418549eefbc09baccbaaff913670Till Mossakowski [(' ' , "Space"),
10a655fc665d418549eefbc09baccbaaff913670Till Mossakowski ('\n', "Newline"),
10a655fc665d418549eefbc09baccbaaff913670Till Mossakowski ('\t', "Tab"),
10a655fc665d418549eefbc09baccbaaff913670Till Mossakowski ('!' , "Exclam"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('"' , "Quot"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('#' , "Hash"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('$' , "Dollar"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('%' , "Percent"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('&' , "Amp"),
c1a0a4f5712942d8ef09bfdb5b8d1e3b576ab438Christian Maeder ('\'', "Prime"), -- Apostrophe?
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('(' , "OBr"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich (')' , "CBr"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('+' , "Plus"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich (',' , "Comma"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('-' , "Minus"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('.' , "Period"), -- Dot?
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('/' , "Slash"), -- Div?
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich (':' , "Colon"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich (';' , "Semi"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('<' , "Lt"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('=' , "Eq"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('>' , "Gt"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('?' , "Quest"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('@' , "At"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('[' , "OSqBr"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('\\' , "Bslash"),
9753523d7bfe7c9413207e8f0c7548bd3dc15322Christian Maeder (']' , "CSqBr"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('^' , "Caret"), -- Hat?
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('`' , "Grave"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('{' , "LBrace"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('|' , "VBar"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('}' , "RBrace"),
d9abda6d63cc31c8a81d9c84275c9bd4c8ae8f57Klaus Luettich ('~' , "Tilde"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\160', "nbsp"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\161', "iexcl"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\162', "cent"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\163', "pound"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\164', "curren"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\165', "yen"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\166', "brvbar"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\167', "sect"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\168', "uml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\169', "copy"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\170', "ordf"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\171', "laquo"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\172', "not"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\173', "shy"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\174', "reg"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\175', "macr"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\176', "deg"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\177', "plusmn"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\178', "sup2"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\179', "sup3"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\180', "acute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\181', "micro"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\182', "para"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\183', "middot"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\184', "cedil"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\185', "sup1"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\186', "ordm"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\187', "raquo"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\188', "quarter"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\189', "half"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\190', "frac34"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\191', "iquest"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\192', "Agrave"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\193', "Aacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\194', "Acirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\195', "Atilde"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\196', "Auml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\197', "Aring"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\198', "AElig"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\199', "Ccedil"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\200', "Egrave"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\201', "Eacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\202', "Ecirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\203', "Euml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\204', "Igrave"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\205', "Iacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\206', "Icirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\207', "Iuml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\208', "ETH"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\209', "Ntilde"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\210', "Ograve"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\211', "Oacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\212', "Ocirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\213', "Otilde"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\214', "Ouml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\215', "Times"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\216', "OSlash"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\217', "Ugrave"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\218', "Uacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\219', "Ucirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\220', "Uuml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\221', "Yacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\222', "THORN"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\223', "szlig"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\224', "agrave"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\225', "aacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\226', "acirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\227', "atilde"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\228', "auml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\229', "aring"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\230', "aelig"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\231', "ccedil"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\232', "egrave"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\233', "eacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\234', "ecirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\235', "euml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\236', "igrave"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\237', "iacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\238', "icirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\239', "iuml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\240', "eth"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\241', "ntilde"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\242', "ograve"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\243', "oacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\244', "ocirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\245', "otilde"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\246', "ouml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\247', "Divide"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\248', "oslash"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\249', "ugrave"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\250', "uacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\251', "ucirc"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\252', "uuml"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\253', "yacute"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\254', "thorn"),
9029484754c7b2037321e7cbd077580866845265Christian Maeder ('\255', "yuml")]