0N/A{- |

2105N/AModule : $Header$

0N/ADescription : Main module to read dfg files into the database

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

0N/ALicense : GPLv2 or higher

0N/A

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

0N/AStability : provisional

0N/APortability : portable

0N/A-}

0N/A--module Main where

0N/Amodule Search.SPASS.DB where

0N/A

0N/Aimport Data.List as L hiding (intersect)

0N/Aimport Data.Map (toList)

0N/Aimport Search.Common.Intersection

0N/Aimport Search.Common.Data

0N/Aimport Search.Common.Normalization

1472N/Aimport Search.Common.Select --(search,LongInclusionTuple)

1472N/Aimport SoftFOL.Sign

1472N/Aimport Search.SPASS.FormulaWrapper

0N/Aimport Search.SPASS.UnWrap --hiding (formula)

0N/Aimport System.Directory

0N/Aimport System.IO

91N/Aimport Text.ParserCombinators.Parsec

0N/Aimport MD5

0N/Aimport Search.DB.Connection

0N/Aimport System.Environment (getArgs)

0N/A

0N/A

1879N/Amain = do args <- getArgs

1879N/A case args of

1879N/A ("search":dir:file:_) -> searchDFG dir file >> return ()

1879N/A ("insert":lib:dir:file:_) -> indexFile lib dir file >> return ()

1879N/A ("intersect":file1:file2:_) -> intersectDFG file1 file2

1879N/A >>= ppIntersection

1879N/A >> return ()

1879N/A _ -> error ("invalid arguments! It should be one of:\n"

1879N/A ++ "1) search <dir> <file>\n"

1879N/A ++ "2) insert <lib> <dir> <file>\n"

2240N/A ++ "3) intersect <file1> <file2>\n")

1879N/A

1879N/A-- -----------------------------------------------------------

1879N/A-- * Search

0N/A-- -----------------------------------------------------------

0N/A

1879N/A{- |

2105N/A searchDFG reads in a source theory from file and returns all possible profile morphisms

2105N/A from all matching target theories in the database.

2105N/A-}

2105N/AsearchDFG :: FilePath -> TheoryName

1879N/A -> IO [[LongInclusionTuple SPIdentifier]]

0N/AsearchDFG = search readAxiomsAndTheorems

0N/A

0N/A{- |

1879N/A readProblem reads in from file a dfg problem and returns

1879N/A all axioms but removes duplicates and trivially true axioms.

1879N/A-}

1879N/A--readAxiomsAndTheorems :: FilePath -> FilePath -> IO ([Profile],[DFGProfile])

1879N/AreadAxiomsAndTheorems dir file =

0N/A do fs <- readDFGFormulae (dir ++ "/" ++ file)

0N/A return $ cleanUp fs

1879N/A

0N/AcleanUp :: [DFGFormula] -> ([ShortProfile SPIdentifier],[ShortProfile SPIdentifier])

0N/AcleanUp fs = (axioms,theorems)

0N/A where fs1 = nubBy eqSen $ filter isNotTrueAtom $ map (dfgNormalize ("","")) fs

0N/A isAxiom p = role p == Axiom

0N/A (ax,th) = partition isAxiom fs1

1879N/A toSProfile p = (md5s $ Str $ show $ skeleton p, parameter p, lineNr p, show $ role p)

0N/A (axioms,theorems) = (map toSProfile ax, map toSProfile th)

0N/A

0N/A-- -----------------------------------------------------------

0N/A-- * Indexing

0N/A-- -----------------------------------------------------------

0N/A

1879N/A

0N/A{-|

0N/A indexFile reads the file TheoryName in directory FilePath and feeds it

0N/A to the database. The first argument specifies the library the theory

1879N/A should be associated with.

1879N/A-}

0N/AindexFile :: URI -> FilePath -> FilePath -> IO () -- ([Char], Int, Int, Int)

1879N/AindexFile lib dir file =

0N/A do fs <- readDFGFormulae (dir ++ "/" ++ file)

1879N/A (nrOfTautologies,nrOfDuplicates,fs3,len) <- return $ normalizeAndAnalyze fs

2105N/A multiInsertProfiles (map toPTuple fs3)

0N/A insertStatistics (lib,file,nrOfTautologies,nrOfDuplicates,len)

0N/A return () -- (file,nrOfTautologies,nrOfDuplicates,len)

0N/A

659N/A

1934N/A-- -----------------------------------------------------------

1879N/A-- * Intersection

1879N/A-- -----------------------------------------------------------

1879N/A

1879N/Atype DFGIntersection = Intersection SPTerm (Formula (Constant SpassConst) Int) SPIdentifier

1879N/A

1879N/AintersectDFG :: FilePath

1879N/A -> FilePath

1879N/A -> IO DFGIntersection

1879N/AintersectDFG = intersect readDFGProfiles

1879N/A

1879N/AppIntersection :: DFGIntersection -> IO ()

1879N/AppIntersection (ps,r) = mapM_ (putStrLn . show . lineNr) ps >> ppRen r

0N/A where ppRen renaming = mapM_ ppPair (toList renaming)

0N/A ppPair (p,q) = putStrLn (show p ++ "\t|->\t" ++ show q)

0N/A

1879N/A-- -----------------------------------------------------------

2105N/A-- * Helper Functions

1879N/A-- -----------------------------------------------------------

1879N/A

1879N/AreadDFGProfiles file =

1879N/A do fs <- readDFGFormulae file

2105N/A return $ nubBy eqSen $ filter isNotTrueAtom $ map (dfgNormalize ("","")) fs

1879N/A

2105N/A

2105N/AeqSen :: (Eq s, Eq p) => Profile f s p -> Profile f1 s p -> Bool

2105N/AeqSen f1 f2 = (skeleton f1) == (skeleton f2) &&

1879N/A (parameter f1) == (parameter f2) &&

2105N/A (role f1) == (role f2)

2105N/A

2105N/AisNotTrueAtom f = case skeleton f

0N/A of (Const TrueAtom []) -> False

0N/A _ -> True

1879N/A

1879N/AnormalizeAndAnalyze fs = (nrOfTautologies,nrOfDuplicates,fs3,length fs3)

1879N/A where fs1 = map (dfgNormalize ("","")) fs

1879N/A fs2 = filter isNotTrueAtom fs1

1879N/A nrOfTautologies = (length fs1) - (length fs2)

1879N/A fs3 = nubBy eqSen fs2

1879N/A nrOfDuplicates = (length fs2) - (length fs3)

1879N/A

1879N/AtoPTuple p = (library',file',line',role',formula',skeleton',parameter',strength')

1879N/A where library' = libName p

1879N/A file' = theoryName p

1879N/A line' = lineNr p

1879N/A formula' = show $ formula p

1879N/A skeleton' = show $ skeleton p

1879N/A parameter' = show $ parameter p

1879N/A role' = show $ role p

1879N/A strength' = strength p

1879N/A