4752N/A{- |

4752N/AModule : $Header$

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

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

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

4752N/A

4752N/AMaintainer : maeder@tzi.de

4752N/AStability : provisional

4752N/APortability : portable

4752N/A

4752N/AInterface for Isabelle theorem prover.

4752N/A-}

4752N/A{-

4752N/A todo: thy files in subdir, check of legal changes in thy file

4752N/A consistency check

4752N/A

4752N/A Interface between Isabelle and Hets:

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

4752N/A User extends .thy file with proofs

4752N/A User finishes Isabelle

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

4752N/A-}

4752N/A

4752N/Amodule Isabelle.IsaProve where

4752N/A

4752N/Aimport Logic.Prover

4752N/Aimport Isabelle.IsaSign

4752N/Aimport Isabelle.IsaConsts

4752N/Aimport Isabelle.IsaPrint

4752N/Aimport Isabelle.Translate

4752N/A

4752N/Aimport Common.AS_Annotation

4752N/Aimport Common.DefaultMorphism

4752N/Aimport Common.ProofUtils

4752N/Aimport qualified Common.Lib.Map as Map

4752N/A

4752N/Aimport Driver.Options

4752N/A

4752N/Aimport Data.Char

4752N/Aimport Control.Monad

4752N/A

4752N/Aimport System.Directory

4752N/Aimport System.Environment

4752N/Aimport System.Exit

4752N/Aimport System.Cmd

4752N/A

4752N/AisabelleS :: String

4752N/AisabelleS = "Isabelle"

4752N/A

4752N/AisabelleProver :: Prover Sign Sentence ()

4752N/AisabelleProver =

4752N/A Prover { prover_name = isabelleS,

4752N/A prover_sublogic = isabelleS,

4752N/A prove = isaProve

4752N/A }

4752N/A

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

4752N/AisabelleConsChecker =

4752N/A Prover { prover_name = "Isabelle-refute",

4752N/A prover_sublogic = isabelleS,

4752N/A prove = consCheck }

4752N/A

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

4752N/AinconsistentS :: String

4752N/AinconsistentS = "inconsistent"

4752N/A

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

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

4752N/AconsCheck thName tm = case t_target tm of

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

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

4752N/A Theory emptySign { baseSig = baseSig sig }

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

4752N/A [ (emptyName $ mkRefuteSen $ termAppl notOp

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

4752N/A { senName = inconsistentS } ]

4752N/A

4752N/AprepareTheory :: Theory Sign Sentence ()

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

4752N/AprepareTheory (Theory sig nSens) = let

4752N/A oSens = toNamedList nSens

4752N/A nSens' = prepareSenNames transString oSens

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

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

4752N/A Map.fromList $ zip (map senName nSens') $ map senName oSens)

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

4752N/A

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

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

4752N/A let depFile = getDepsFileName thName thm

4752N/A ex <- doesFileExist depFile

4752N/A when ex $ removeFile depFile

4752N/A

4752N/AgetDepsFileName :: String -> String -> String

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

4752N/A

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

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

4752N/AgetProofDeps m thName thm = do

4752N/A let file = getDepsFileName thName thm

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

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

4752N/A b <- checkInFile file

4752N/A if b then do

4752N/A s <- readFile file

4752N/A if null s then return $ Open $ mapN thm

4752N/A else let l = filter (not . null) $ map strip $ lines s

4752N/A in return $ mkProved (mapN thm) $ map mapN l

4752N/A else return $ Open $ mapN thm

4752N/A

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

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

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

4752N/A

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

4752N/AmkProved thm used = Proved

4752N/A { goalName = thm

4752N/A , usedAxioms = used

4752N/A , proverName = isabelleS

4752N/A , proofTree = ()

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

4752N/A }

4752N/A

4752N/AprepareThyFiles :: String -> String -> IO ()

4752N/AprepareThyFiles thyFile thy = do

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

4752N/A exOrig <- checkInFile origFile

4752N/A exThyFile <- checkInFile thyFile

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

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

4752N/A thy_time <- getModificationTime thyFile

4752N/A orig_time <- getModificationTime origFile

4752N/A s <- readFile origFile

unless (thy_time >= orig_time && s == thy)

$ patchThyFile origFile thyFile thy

patchThyFile :: FilePath -> FilePath -> String -> IO ()

patchThyFile origFile thyFile thy = do

let patchFile = thyFile ++ ".patch"

oldFile = thyFile ++ ".old"

diffCall = "diff -u " ++ origFile ++ " " ++ thyFile

++ " > " ++ patchFile

patchCall = "patch -fu " ++ thyFile ++ " " ++ patchFile

callSystem diffCall

renameFile thyFile oldFile

removeFile origFile

writeFile origFile thy

writeFile thyFile thy

callSystem patchCall

return()

callSystem :: String -> IO ExitCode

callSystem s = putStrLn s >> system s

isaProve :: String -> Theory Sign Sentence () -> IO([Proof_status ()])

isaProve thName th = do

let (sig, axs, ths, m) = prepareTheory th

thms = map senName ths

hlibdir <- getEnv "HETS_LIB"

let thBaseName = reverse . takeWhile (/= '/') $ reverse thName

thy = show $ printIsaTheory thBaseName hlibdir sig $ axs ++ ths

thyFile = thName ++ ".thy"

prepareThyFiles thyFile thy

removeDepFiles thName thms

isabelle <- getEnv "HETS_ISABELLE"

callSystem $ isabelle ++ " " ++ thyFile

getAllProofDeps m thName thms

markSimp :: Named Sentence -> Named Sentence

markSimp = mapNamed markSimpSen

markSimpSen :: Sentence -> Sentence

markSimpSen s = case s of

Sentence {} -> s {isSimp = isSimpRuleSen s}

_ -> s

isSimpRuleSen :: Sentence -> Bool

isSimpRuleSen sen = case sen of

RecDef {} -> False

_ -> isSimpRule $ senTerm sen

-- | test whether a formula should be put into the simpset

isSimpRule :: Term -> Bool

-- only universal quantifications

isSimpRule App { funId = Const {termName = VName { new = q }}

, argId = arg@Abs{}}

| q == exS || q == ex1S = False

| q == allS = isSimpRule (termId arg)

-- accept everything expect from abstractions

isSimpRule App {funId = arg1, argId = arg2} =

isSimpRule arg1 && isSimpRule arg2

isSimpRule MixfixApp {funId = arg1, argIds = args } =

isSimpRule arg1 && all isSimpRule args

isSimpRule Const{} = True

isSimpRule Free{} = True

isSimpRule Var{} = True

isSimpRule Bound{} = True

isSimpRule Abs{} = False

isSimpRule If{} = True

isSimpRule Case{} = True

isSimpRule Let{} = True

isSimpRule (Paren t) = isSimpRule t

isSimpRule _ = False