0N/A{- |

2105N/AModule : $Header$

0N/ADescription : interface to the Isabelle theorem prover

0N/ACopyright : (c) University of Cambridge, Cambridge, England

0N/A adaption (c) Till Mossakowski, Uni Bremen 2002-2005

0N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

0N/A

0N/AMaintainer : Christian.Maeder@dfki.de

0N/AStability : provisional

0N/APortability : portable

0N/A

0N/AInterface for Isabelle theorem prover.

0N/A-}

0N/A{-

0N/A Interface between Isabelle and Hets:

0N/A Hets writes Isabelle .thy file and starts Isabelle

0N/A User extends .thy file with proofs

0N/A User finishes Isabelle

1472N/A Hets reads in created *.deps files

1472N/A-}

1472N/A

0N/Amodule Isabelle.IsaProve where

0N/A

0N/Aimport Logic.Prover

91N/Aimport Isabelle.IsaSign

0N/Aimport Isabelle.IsaConsts

0N/Aimport Isabelle.IsaPrint

0N/Aimport Isabelle.IsaParse

0N/Aimport Isabelle.Translate

0N/Aimport Isabelle.MarkSimp

1879N/A

1879N/Aimport Common.AS_Annotation

1879N/Aimport Common.DocUtils

1879N/Aimport Common.DefaultMorphism

1879N/Aimport Common.ProofUtils

1879N/Aimport qualified Data.Map as Map

1879N/Aimport qualified Data.Set as Set

1879N/A

1879N/Aimport Text.ParserCombinators.Parsec

1879N/Aimport Data.Char

2240N/Aimport Data.List (intersperse)

1879N/Aimport Control.Monad

1879N/A

1879N/Aimport System.Directory

0N/Aimport System.Environment

0N/Aimport System.Exit

1879N/Aimport System.Cmd

2105N/A

2105N/AisabelleS :: String

2105N/AisabelleS = "Isabelle"

2105N/A

1879N/AisabelleProver :: Prover Sign Sentence () ()

0N/AisabelleProver = mkProverTemplate isabelleS () isaProve

0N/A

0N/AisabelleConsChecker :: ConsChecker Sign Sentence () (DefaultMorphism Sign) ()

1879N/AisabelleConsChecker = mkProverTemplate "Isabelle-refute" () consCheck

1879N/A

1879N/AopenIsaProof_status :: String -> Proof_status ()

1879N/AopenIsaProof_status n = openProof_status n (prover_name isabelleProver) ()

1879N/A

0N/A-- | the name of the inconsistent lemma for consistency checks

0N/AinconsistentS :: String

1879N/AinconsistentS = "inconsistent"

0N/A

0N/AconsCheck :: String -> TheoryMorphism Sign Sentence (DefaultMorphism Sign) ()

0N/A -> IO([Proof_status ()])

0N/AconsCheck thName tm = case t_target tm of

0N/A Theory sig nSens -> let (axs, _) = getAxioms $ toNamedList nSens in

1879N/A isaProve (thName ++ "_c") $

0N/A Theory sig

0N/A $ markAsGoal $ toThSens $ if null axs then [] else

0N/A [ makeNamed inconsistentS $ mkRefuteSen $ termAppl notOp

0N/A $ foldr1 binConj $ map (senTerm . sentence) axs ]

0N/A

0N/AprepareTheory :: Theory Sign Sentence ()

1879N/A -> (Sign, [Named Sentence], [Named Sentence], Map.Map String String)

0N/AprepareTheory (Theory sig nSens) = let

0N/A oSens = toNamedList nSens

0N/A nSens' = prepareSenNames transString oSens

1879N/A (disAxs, disGoals) = getAxioms nSens'

1879N/A in (sig, map markSimp disAxs, map markSimp disGoals,

0N/A Map.fromList $ zip (map senAttr nSens') $ map senAttr oSens)

1879N/A-- return a reverse mapping for renamed sentences

0N/A

1879N/AremoveDepFiles :: String -> [String] -> IO ()

2105N/AremoveDepFiles thName = mapM_ $ \ thm -> do

0N/A let depFile = getDepsFileName thName thm

0N/A ex <- doesFileExist depFile

0N/A when ex $ removeFile depFile

659N/A

1934N/AgetDepsFileName :: String -> String -> String

1879N/AgetDepsFileName thName thm = thName ++ "_" ++ thm ++ ".deps"

1879N/A

1879N/AgetProofDeps :: Map.Map String String -> String -> String

1879N/A -> IO (Proof_status ())

1879N/AgetProofDeps m thName thm = do

1879N/A let file = getDepsFileName thName thm

1879N/A mapN n = Map.findWithDefault n n m

1879N/A strip = takeWhile (not . isSpace) . dropWhile isSpace

1879N/A b <- doesFileExist file

1879N/A if b then do

1879N/A s <- readFile file

1879N/A return $ mkProved (mapN thm) $ map mapN $

0N/A Set.toList $ Set.filter (not . null) $

0N/A Set.fromList $ map strip $ lines s

0N/A else return $ openIsaProof_status $ mapN thm

1879N/A

2105N/AgetAllProofDeps :: Map.Map String String -> String -> [String]

1879N/A -> IO([Proof_status ()])

1879N/AgetAllProofDeps m thName = mapM $ getProofDeps m thName

1879N/A

1879N/AcheckFinalThyFile :: (TheoryHead, Body) -> String -> IO Bool

2105N/AcheckFinalThyFile (ho, bo) thyFile = do

1879N/A s <- readFile thyFile

2105N/A case parse parseTheory thyFile s of

2105N/A Right (hb, b) -> do

2105N/A let ds = compatibleBodies bo b

1879N/A mapM_ (\ d -> putStrLn $ showDoc d "") $ ds ++ warnSimpAttr b

2105N/A if hb /= ho then do

2105N/A putStrLn "illegal change of theory header"

2105N/A return False

0N/A else return $ null ds

0N/A Left err -> putStrLn (show err) >> return False

1879N/A

1879N/AmkProved :: String -> [String] -> Proof_status ()

1879N/AmkProved thm used = (openIsaProof_status thm)

1879N/A { goalStatus = Proved Nothing

1879N/A , usedAxioms = used

1879N/A , tacticScript = Tactic_script "unknown isabelle user input"

1879N/A }

1879N/A

1879N/AprepareThyFiles :: (TheoryHead, Body) -> String -> String -> IO ()

1879N/AprepareThyFiles ast thyFile thy = do

1879N/A let origFile = thyFile ++ ".orig"

1879N/A exOrig <- doesFileExist origFile

1879N/A exThyFile <- doesFileExist thyFile

1879N/A if exOrig then return () else writeFile origFile thy

1879N/A if exThyFile then return () else writeFile thyFile thy

1879N/A thy_time <- getModificationTime thyFile

1879N/A orig_time <- getModificationTime origFile

1879N/A s <- readFile origFile

1879N/A unless (thy_time >= orig_time && s == thy)

1879N/A $ patchThyFile ast origFile thyFile thy

1879N/A

1879N/ApatchThyFile :: (TheoryHead, Body) -> FilePath -> FilePath -> String -> IO ()

1879N/ApatchThyFile (ho, bo) origFile thyFile thy = do

0N/A let patchFile = thyFile ++ ".patch"

0N/A oldFile = thyFile ++ ".old"

0N/A diffCall = "diff -u " ++ origFile ++ " " ++ thyFile

1879N/A ++ " > " ++ patchFile

0N/A patchCall = "patch -bfu " ++ thyFile ++ " " ++ patchFile

1879N/A callSystem diffCall

1879N/A renameFile thyFile oldFile

1879N/A removeFile origFile

1879N/A writeFile origFile thy

1879N/A writeFile thyFile thy

1879N/A callSystem patchCall

1879N/A s <- readFile thyFile

1879N/A case parse parseTheory thyFile s of

1879N/A Right (hb, b) -> do

1879N/A let ds = compatibleBodies bo b

1879N/A h = hb == ho

1879N/A mapM_ (\ d -> putStrLn $ showDoc d "") ds

1879N/A unless h $ putStrLn "theory header is corrupt"

1879N/A unless (h && null ds) $ revertThyFile thyFile thy

1879N/A Left err -> do

1879N/A putStrLn $ show err

1879N/A revertThyFile thyFile thy

1879N/A

1879N/ArevertThyFile :: String -> String -> IO ()

1879N/ArevertThyFile thyFile thy = do

1879N/A putStrLn $ "replacing corrupt file " ++ show thyFile

1879N/A removeFile thyFile

1879N/A writeFile thyFile thy

1879N/A

1879N/AcallSystem :: String -> IO ExitCode

1879N/AcallSystem s = putStrLn s >> system s

1879N/A

1879N/AisaProve :: String -> Theory Sign Sentence () -> IO([Proof_status ()])

1879N/AisaProve thName th = do

1879N/A let (sig, axs, ths, m) = prepareTheory th

1879N/A thms = map senAttr ths

1879N/A thBaseName = reverse . takeWhile (/= '/') $ reverse thName

1879N/A defaultProof = "using " ++ concat (intersperse " " $

1879N/A map senAttr $ filter ((/= mkSen true) . sentence) axs)

1879N/A ++ " by auto"

1879N/A thy = shows (printIsaTheoryWithProofs defaultProof thBaseName sig

1879N/A $ axs ++ ths) "\n"

1879N/A thyFile = thBaseName ++ ".thy"

1879N/A case parse parseTheory thyFile thy of

1879N/A Right (ho, bo) -> do

1879N/A prepareThyFiles (ho, bo) thyFile thy

1879N/A removeDepFiles thBaseName thms

1879N/A isabelleEnv <- getEnv "HETS_ISABELLE"

1879N/A let isabelle = if null isabelleEnv then "Isabelle" else isabelleEnv

1879N/A callSystem $ isabelle ++ " " ++ thyFile

1879N/A ok <- checkFinalThyFile (ho, bo) thyFile

1879N/A if ok then getAllProofDeps m thBaseName thms

1879N/A else return []

1879N/A Left err -> do

1879N/A putStrLn $ show err

1879N/A putStrLn $ "Sorry, generated theory cannot be parsed, see: " ++ thyFile

0N/A writeFile thyFile thy

0N/A putStrLn "aborting Isabelle proof attempt"

0N/A return []

0N/A