IsaProve.hs revision 31c49f2fa23d4ac089f35145d80a224deb6ea7e4
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederCopyright : (c) University of Cambridge, Cambridge, England
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian Maeder adaption (c) Till Mossakowski, Uni Bremen 2002-2004
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : hets@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Interface for Isabelle theorem prover.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder todo: thy files in subdir
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport Configuration
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport ChildProcess
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederimport Directory
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian MaederisabelleProver :: Prover Sign Sentence () ()
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederisabelleProver =
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder Prover { prover_name = "Isabelle",
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder prover_sublogic = "Isabelle",
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder prove = isaProve
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder -- input: theory name, theory, goals
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich -- output: proof status for goals and lemmas
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus LuettichisaProve :: String -> (Sign,[Named Sentence]) -> [Named Sentence]
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder -> IO([Proof_status Sentence ()])
4cb215739e9ab13447fa21162482ebe485b47455Christian MaederisaProve thName (sig,axs) goals = do
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder let fileName = thName++".thy"
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich origName = thName++".orig.thy"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder patchName = thName++".patch"
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder ex <- doesFileExist fileName
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder exorig <- doesFileExist origName
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder case (ex,exorig) of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (True,True) -> do
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder putStrLn ("diff -u "++origName++" "++fileName++" > "++patchName)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder system ("diff -u "++origName++" "++fileName++" > "++patchName)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeFile fileName showTheory
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder putStrLn ("cp "++fileName++" "++origName)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder system ("cp "++fileName++" "++origName)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder putStrLn ("patch -u "++fileName++" "++patchName)
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder system ("patch -u "++fileName++" "++patchName)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (True,False) -> do
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder system ("cp "++fileName++" "++fileName++".old")
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder writeFile fileName showTheory
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder system ("cp "++fileName++" "++origName)
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder (False,_) -> do
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder writeFile fileName showTheory
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder system ("cp "++fileName++" "++origName)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder isabelle <- getEnv "ISABELLE"
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder isa <- newChildProcess isabelle [arguments [fileName]]
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder msgs <- readProofs isa
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder closeChildProcessFds isa
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder return [] -- ??? to be implemented
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder disAxs = disambiguateSens [] $ nameSens $ transSens axs
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder showLemma = concat $ map ((++"\n") . formLemmas) disAxs
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder showAxs = concat $ map ((++"\n") . showSen) disAxs
f13d1e86e58da53680e78043e8df182eed867efbChristian Maeder disGoals = disambiguateSens disAxs $ nameSens $ transSens goals
c2a4d8ae266aa37cc922eba97077520229a19902Christian Maeder showGoals = concat
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun Wang $ map showGoal disGoals
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder getFileName = reverse . fst . break (=='/') . reverse
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun Wang showGoal goal = (("theorem "++) . -- (++(ipc (show fd) (senName goal))) .
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (++"\noops\n") . showSen) goal
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maeder showTheory = "ML \"val hetsLib = (OS.Process.getEnv \\\"HETS_LIB\\\"); \n"
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski ++ "case hetsLib of NONE => add_path \\\".\\\" \n"
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich ++ "| SOME s => add_path (s ^ \\\"/Isabelle\\\")\"\n\n"
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich ++ "theory " ++ getFileName thName ++ " = "
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich ++ showPretty sig "\n\naxioms\n"
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder ++ showAxs ++ "\n" ++ showLemma ++ "\n\n" ++ showGoals --fd
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder -- ipc fd thmName = "\nML \" writeArr("++ fd ++ ", {Pretty.string_of(pretty_proof_of \""++ thmName ++"\") , 0, None})\"\n\n"
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian MaederreadProofs :: ChildProcess -> IO [String]
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederreadProofs = rP []
df35538fec1d9135602308d577255c0d466b6365Christian MaederrP :: [String] -> ChildProcess -> IO [String]
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder msg <- readMsg cp
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder "EOF" -> return s
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder _ -> rP (s++[msg]) cp
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- translate special characters in sentence names
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedertransSens :: [Named a] -> [Named a]
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedertransSens = map (\ax -> ax{senName = transString $ senName ax})
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- disambiguate sentence names
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederdisambiguateSens :: [Named a] -> [Named a] -> [Named a]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederdisambiguateSens others axs = reverse $ disambiguateSensAux others axs []
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederdisambiguateSensAux others [] soFar = soFar
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian MaederdisambiguateSensAux others (ax:rest) soFar =
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder disambiguateSensAux (ax':others) rest (ax':soFar)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder name' = fromJust $ find (not . flip elem namesSoFar)
776a1a086df734581431e6edb4343ed4c8d34d55Christian Maeder (name:[name++show i | i<-[1..]])
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder name = senName ax
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder namesSoFar = map senName others
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder ax' = ax{senName = name'}
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- output a sentences
c0c2380bced8159ff0297ece14eba948bd236471Christian MaedershowSen :: PrettyPrint a => Named a -> String
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedershowSen x = (if null (senName x) then ""
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else senName x++": ")
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ++ "\""++showPretty (sentence x) "\""
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- name unlabeled axioms with "Axnnn"
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedernameSens :: [Named a] -> [Named a]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedernameSens sens =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder map nameSen (zip sens [1..length sens])
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder where nameSen (sen,no) = if senName sen == ""
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder then sen{senName = "Ax"++show no}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- form a lemmas from given axiom and add them both to Isabelles simplifier
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederformLemmas :: Named a -> String
4017ebc0f692820736d796af3110c3b3018c108aChristian MaederformLemmas sen =
ad4889ebb40efae8595b0969dd6ba1162d52bac3Christian Maeder let (sn, ln) = lemmaName (senName sen)
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder "lemmas " ++ ln ++ " = " ++ sn ++ " [simplified]\n" ++
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder dec ln ++ "\n" ++ dec sn
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder lemmaName s = (s, s++"a")
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder dec s = "declare " ++ s ++ "[simp]"