446N/A{- |

4744N/AModule : $Header$

446N/ADescription : Export of the MPTP.Profile table to KRHyper format

446N/ACopyright : (c) Immanuel Normann, Uni Bremen 2007

446N/ALicense : GPLv2 or higher, see LICENSE.txt

446N/A

446N/AMaintainer : inormann@jacobs-university.de

446N/AStability : provisional

446N/APortability : portable

446N/A-}

446N/Amodule Search.DB.Export where

446N/A

446N/Aimport Config (home,dbDriver,dbServer,dbDatabase,dbPassword,dbUsername)

446N/Aimport qualified Utils.SetMap as SM

446N/Aimport Data.List

446N/Aimport qualified Data.Set as S

446N/Aimport qualified Data.Map as M

446N/Aimport Data.Char (toUpper)

446N/Aimport Database.HaskellDB

446N/Aimport Database.HaskellDB.GenericConnect

873N/Aimport Database.HaskellDB.HDBRec

446N/Aimport Search.DB.Connection

446N/Aimport Search.DB.MPTP.Profile hiding (Skeleton)

446N/Aimport System.IO

446N/A--import Control.Monad (filterM)

5061N/A

6184N/Adata Sequent =

446N/A Seq {assumptions :: [AbstractFormula],

446N/A conclusion :: AbstractFormula} deriving (Show)

4744N/Atype AbstractFormula = (String,[String])

4865N/A

4865N/AexportToKrhyper =

4865N/A do md5s <- getField skeleton_md5

4865N/A filenames <- getField file

4865N/A writeAxiomFiles md5s filenames

4865N/A mapM (writeRuleFile md5s filenames) (getGroups filenames)

4865N/A return 0

4865N/A

4865N/A

4865N/AwriteRuleFile md5s filenames group =

4865N/A do seqs <- getSequents md5s filenames group

4865N/A writeSequents group seqs

4865N/A{-

4865N/AwriteRuleFile "aff_2"

4865N/A-}

4865N/A

4865N/Adfg_krh = home ++ "/dfg/krh/"

4865N/A

4865N/AwriteSequents group seqs =

4865N/A do outhandle <- openFile (dfg_krh ++ "rules/" ++ group) AppendMode

4865N/A hPutStrLn outhandle ("% " ++ group ++ "\n\n")

4865N/A hPutStrLn outhandle $ formatSequents seqs

4865N/A hFlush outhandle

4865N/A

5073N/AwriteAxiomFiles md5s filenames =

5073N/A do filesAndSeqs <- mapM (getSequent md5s) filenames

4865N/A mapM writeAxioms filesAndSeqs

4865N/A return "habe fertig"

4865N/A

4865N/AwriteAxioms (file,seq) =

4865N/A do outhandle <- openFile (dfg_krh ++ "axioms/" ++ file ++ ".axioms") AppendMode

4865N/A putStrLn file

4865N/A hPutStrLn outhandle $ formatAxioms (file,seq)

4865N/A hFlush outhandle

4865N/A

4865N/A

4865N/AformatSequents seqs = concat $ intersperse "\n\n" (map formatSequent seqs)

4865N/AformatSequent (file,Seq assumptions conclusion) = "% " ++ file ++ "\n" ++ (formatAbstractFormula conclusion) ++ ":-\n\t" ++ (concat $ intersperse ",\n\t" $ map formatAbstractFormula assumptions) ++ "."

4865N/AformatAbstractFormula (h,args) = h ++ "(" ++ (concat $ intersperse "," (map upperFirst args)) ++ ")"

4865N/AformatAxioms (file,Seq assumptions _) = "% " ++ file ++ "\n" ++ (concat $ map formatAxiom assumptions)

4865N/AformatAxiom (h,args) = h ++ "(" ++ (concat $ intersperse "," args) ++ ").\n"

4865N/AupperFirst (c:str) = (toUpper c):str

4865N/A{-

4865N/A*DB.Export> hr <- hide $ getField skeleton_md5

4865N/Ahabe fertig

4865N/A*DB.Export> let (Hide md5s) = hr

4865N/A*DB.Export> hr <- hide $ getField file

4865N/Ahabe fertig

4865N/A*DB.Export> let (Hide filenames) = hr

4865N/A

4865N/A*DB.Export> seqs <- getSequents md5s filenames "zfmisc_1"

4865N/A[("zfmisc_1__t100_zfmisc_1.dfg",Seq [("H1892",["r2_hidden","r2_hidden"]),("H8944",["k1_zfmisc_1","r2_hidden","r1_tarski","k1_zfmisc_1","r1_tarski","r2_hidden","r2_hidden","r1_tarski","k1_zfmisc_1","r2_hidden","k1_zfmisc_1","r2_hidden","r1_tarski","k1_zfmisc_1","r1_tarski","k1_zfmisc_1","r2_hidden","r1_tarski"]),("H6020",["r2_hidden","r1_tarski","r2_hidden","r1_tarski","r2_hidden","r2_hidden","r1_tarski"]),("H12556",[]),("H6737",["r2_hidden","r1_tarski","k3_tarski"]),("H6857",["v1_xboole_0"]),("H10165",["v1_xboole_0"]),("H10273",["r1_tarski"])] ("H16215",["r1_tarski","k1_zfmisc_1","k3_tarski"])),("zfmisc_1__t101_zfmisc_1.dfg",Seq [("H1892",["r2_hidden","r2_hidden"]),("H15818",["k2_xboole_0","k2_xboole_0"]),("H15818",["k3_xboole_0","k3_xboole_0"]),("H5272",["r1_tarski","r1_tarski","r1_tarski","r1_tarski"]),("H13679",["r2_hidden","r2_hidden","k2_xboole_0","r2_hidden","r2_hidden","k2_xboole_0","r2_hidden","r2_hidden","r2_hidden","k2_xboole_0","r2_hidden","r2_hidden","r2_hidden","k2_xboole_0","r2_hidden","r2_hidden","k2_xboole_0","r2_hidden","r2_hidden","r2_hidden","k2_xboole_0","r2_hidden","r2_hidden","k2_xboole_0","r2_hidden","r2_hidden","r2_hidden","k2_xboole_0","r2_hidden","r2_hidden","k2_xboole_0"]),("H6020",["r2_hidden","r1_tarski","r2_hidden","r1_tarski","r2_hidden","r2_hidden","r1_tarski"]),("H12879",["r2_hidden","r2_hidden","k3_xboole_0","r2_hidden","r2_hidden","k3_xboole_0","r2_hidden","r2_hidden","r2_hidden","k3_xboole_0","r2_hidden","r2_hidden","k3_xboole_0","r2_hidden","r2_hidden","k3_xboole_0","r2_hidden","r2_hidden","k3_xboole_0","r2_hidden","r2_hidden","r2_hidden","k3_xboole_0","r2_hidden","r2_hidden","r2_hidden","k3_xboole_0","r2_hidden","r2_hidden","r2_hidden","k3_xboole_0"]),("H14488",["k3_tarski","r2_hidden","r2_hidden","r2_hidden","r2_hidden","r2_hidden","r2_hidden","r2_hidden","r2_hidden","r2_hidden","r2_hidden","r2_hidden","r2_hidden","k3_tarski"]),("H12556",[]),("H16237",["v1_xboole_0","v1_xboole_0","k2_xboole_0"]),("H2906",["v1_xboole_0","v1_xboole_0","k2_xboole_0"]),("H11863",["k2_xboole_0"]),("H11863",["k3_xboole_0"]),("H6857",["v1_xboole_0"]),("H10165",["v1_xboole_0"]),("H10273",["r1_tarski"]),("H12766",["r1_xboole_0","r1_xboole_0"]),("H12745",["r1_xboole_0","r2_hidden","k3_xboole_0","r1_xboole_0","r2_hidden","k3_xboole_0"]),("H4663",["r1_tarski","k3_tarski","k3_xboole_0","k3_xboole_0","k3_tarski","k3_tarski"])] ("H9439",["k3_tarski","k3_xboole_0","k3_xboole_0","k3_tarski","k3_tarski","r1_xboole_0","k3_tarski","k3_xboole_0","k3_xboole_0","k3_tarski","k3_tarski","k3_tarski","k3_xboole_0","k3_xboole_0","k3_tarski","k3_tarski","r2_hidden","k2_xboole_0","k3_tarski","k3_xboole_0","k3_xboole_0","k3_tarski","k3_tarski","r2_hidden","k2_xboole_0"]))]

4865N/A

4865N/A-}

4865N/A

4865N/A

4865N/AgetSequents md5s filenames group =

4865N/A let theories = groupFileNames filenames

4865N/A (Just fileNameSet) = M.lookup group theories

4865N/A fileNameList = S.toList fileNameSet

4865N/A in do mapM (getSequent md5s) fileNameList --(take 2 fileNameList)

4865N/A

4865N/A{-

4865N/A removeEmptyAssumptions seq = filter (not . null . snd) (assumptions $ snd seq)

4865N/A in do seqs <- mapM (getSequent md5s) (take 2 fileNameList)

4865N/A --return $ filter (not . null . assumptions . snd) seqs

4865N/A return $ map removeEmptyAssumptions seqs

4865N/A-}

4865N/A

4865N/AgetSequent md5s file =

4865N/A do abstractFormulas <- getAbstractFormulas file

4865N/A return (file,(tuplesToSequent md5s abstractFormulas))

4865N/A

4865N/AtuplesToSequent md5s tuples = Seq assumptions conclusion

4865N/A where (axs,cs) = partition isAxiom tuples

4865N/A isAxiom tuple = fst tuple == "axiom"

4865N/A assumptions = map ((md5ToId md5s) . snd) axs

5061N/A conclusion = case cs of [(_,c)] -> md5ToId md5s c

5061N/A _ -> error "there is not exactly one conclusion"

5061N/A

5061N/Amd5ToId md5s (md5,ps) = case elemIndex md5 md5s

5061N/A of (Just id) -> (('h':(show id)),ps)

5061N/A Nothing -> error (md5 ++ " does not exist")

5061N/A

4865N/AgetAbstractFormulas file =

4865N/A do recs <- selectMd5Params file

4865N/A return (map recToTuple recs)

4865N/A

4865N/ArecToTuple rec = (role,(skeleton_md5,params))

4865N/A where (RecCons role (RecCons skeleton_md5 (RecCons paramStr _))) = rec RecNil

4865N/A params = (read paramStr)::[String]

4865N/A

4865N/AselectMd5Params f =

4865N/A do withDB $ do t <- table profile

4865N/A restrict (t!file .==. (constant f) .&&.

4865N/A t!skeleton .<>. (constant "true"))

4865N/A project (role << t!role #

4865N/A skeleton_md5 << t!skeleton_md5 #

4865N/A parameter << t!parameter)

4865N/A

4865N/Adata Hide a = Hide a

4865N/Ainstance Show (Hide a) where

4865N/A show a = "habe fertig"

4865N/A

4865N/Ahide a = a >>= return . Hide

5073N/A

5073N/AgroupFileNames names = SM.fromListSetValues $ map mkPair names

4865N/A where mkPair name = (getPrefix name,name)

4865N/A

4865N/AgetGroups names = S.toList $ fill names S.empty

4865N/A where fill (n:names)acc = fill names (S.insert (getPrefix n) acc)

4865N/A fill [] acc = acc

4865N/A

4865N/AgetPrefix str = concat $ takeWhile ("__"/=) $ group str

4865N/A

4865N/AgetFilesOf filenames pre = filter (\file -> (getPrefix file) == pre) filenames

4865N/A

4865N/A{-

5061N/A*DB.Export> groupFileNames names

5061N/AfromList [("aff_1",fromList ["aff_1__t48_aff_1.dfg","aff_1__t49_aff_1.dfg","aff_1__t50_aff_1.dfg","aff_1__t51_aff_1.dfg"]),("alg_1",fromList ["alg_1__t7_alg_1.dfg","alg_1__t8_alg_1.dfg","alg_1__t9_alg_1.dfg"]),("algspec1",fromList ["algspec1__t10_algspec1.dfg","algspec1__t11_algspec1.dfg"])]

5061N/A-}

5061N/A

5061N/Anames = ["aff_1__t48_aff_1.dfg",

5061N/A "aff_1__t49_aff_1.dfg",

5061N/A "aff_1__t50_aff_1.dfg",

4865N/A "aff_1__t51_aff_1.dfg",

4865N/A "alg_1__t7_alg_1.dfg",

4865N/A "alg_1__t8_alg_1.dfg",

4865N/A "alg_1__t9_alg_1.dfg",

4865N/A "algspec1__t10_algspec1.dfg",

4865N/A "algspec1__t11_algspec1.dfg"]

4865N/A