Prover.hs revision ef4b978a005bdccb8bd5e611887661db703114f2
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiModule : $Header$
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : till@tzi.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiProvide prover stuff for class Logic.Sentences
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.AS_Annotation as AS_Anno
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport qualified Common.OrderedMap as OMap
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport qualified Common.Lib.Map as Map (toList,fromList)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- * sentence packing
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederdata SenStatus a tStatus = SenStatus
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , isAxiom :: Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , isDef :: Bool
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder , thmStatus :: [tStatus]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder } deriving Show
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maederinstance PrettyPrint a => PrettyPrint (SenStatus a b) where
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich printText0 ga x = printText0 ga (value x)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichemptySenStatus :: SenStatus a b
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederemptySenStatus = SenStatus { value = error "emptySenStatus"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , isDef = False
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , isAxiom = True
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , thmStatus = [] }
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maederinstance Eq a => Eq (SenStatus a b) where
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder d1 == d2 = (value d1) == (value d2)
8e80792f474d154ff11762fac081a422e34f1accChristian Maederinstance Ord a => Ord (SenStatus a b) where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder d1 <= d2 = (value d1) <= (value d2)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederdecoTc :: TyCon
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederdecoTc = mkTyCon "Static.DevGraph.SenStatus"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance (Typeable s,Typeable b) => Typeable (SenStatus s b) where
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder typeOf s = mkTyConApp decoTc [typeOf ((undefined :: SenStatus a b -> a) s),
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder typeOf ((undefined :: SenStatus a b -> b) s)]
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederelemWOrdTc :: TyCon
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederelemWOrdTc = mkTyCon "Common.OrderedMap.ElemWOrd"
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederinstance (Typeable a) => Typeable (OMap.ElemWOrd a) where
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder typeOf s = mkTyConApp elemWOrdTc [typeOf ((undefined :: OMap.ElemWOrd a -> a) s)]
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederinstance PrettyPrint a => PrettyPrint (OMap.ElemWOrd a) where
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder printText0 ga e = printText0 ga (OMap.ele e)
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maedertype ThSens a b = OMap.OMap String (SenStatus a b)
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaedernoSens :: ThSens a b
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | join and disambiguate
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederjoinSens :: (Ord a,Eq b) => ThSens a b -> ThSens a b -> ThSens a b
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederjoinSens s1 s2 = let l1 = sortBy (comparing snd) $ Map.toList s1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder updN n (_,e) = (n,e)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder l2 = map (\ (x,e) ->
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski sortBy (comparing snd) $ Map.toList s2
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski in Map.fromList $ mergeSens l1 $
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski genericDisambigSens fst updN (OMap.keysSet s1) l2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder where mergeSens [] l2 = l2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mergeSens l1 [] = l1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mergeSens l1@((k1,e1) : r1) l2@((k2,e2) : r2) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case compare e1 e2 of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder LT -> (k1,e1) : mergeSens r1 l2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { thmStatus =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder union (thmStatus $ OMap.ele e1)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (thmStatus $ OMap.ele e2)}})
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder : mergeSens r1 r2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski GT -> (k2,e2) : mergeSens l1 r2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapValue :: (a -> b) -> SenStatus a c -> SenStatus b c
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapValue f d = d { value = f $ value d }
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermarkAsGoal :: Ord a => ThSens a b -> ThSens a b
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermarkAsGoal = OMap.map (\d -> d { isAxiom = False})
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedertoNamedList :: ThSens a b -> [AS_Anno.Named a]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedertoNamedList = map (uncurry toNamed) . OMap.toList
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedertoNamed :: String -> SenStatus a b -> AS_Anno.Named a
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoThSens :: Ord a => [AS_Anno.Named a] -> ThSens a b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder emptySenStatus { value = AS_Anno.sentence v
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- theories and theory morphisms
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata Theory sign sen proof_tree =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Theory sign (ThSens sen (Proof_status proof_tree))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata TheoryMorphism sign sen mor proof_tree =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder TheoryMorphism {t_source :: Theory sign sen proof_tree,
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder t_target :: Theory sign sen proof_tree,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder t_morphism :: mor
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- proofs and provers
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- e.g. the file name, or the script itself, or a configuration string
74d9a385499bf903b24848dff450a153f525bda7Christian Maederdata Tactic_script = Tactic_script String deriving (Eq, Ord, Show)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederdata Proof_status proof_tree =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | Disproved String
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | Proved { goalName :: String,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder usedAxioms :: [String], -- used axioms or theorems or goals
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder proverName :: String, -- name of prover
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder proofTree :: proof_tree,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder tacticScript :: Tactic_script }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Consistent Tactic_script
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Eq, Show)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maederinstance Eq a => Ord (Proof_status a) where
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Open _ <= _ = True
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Disproved _ <= x = case x of
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Open _ -> False
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Proved _ _ _ _ _ <= x = case x of
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Proved _ _ _ _ _ -> True
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder _ <= _ = False
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaederisProvedStat :: Proof_status proof_tree -> Bool
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaederisProvedStat (Proved _ _ _ _ _) = True
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederisProvedStat _ = False
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maederdata ProverTemplate goal proof_tree = Prover
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { prover_name :: String,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder prover_sublogic :: String,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder prove :: String -> goal -> IO([Proof_status proof_tree])
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -- input: theory name, theory, goals
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -- output: proof status for goals and lemmas
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder{- possibly needed in the future
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder add_sym :: symbol -> IO(Bool), -- returns True if succeeded
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder remove_sym :: symbol -> IO(Bool), -- returns True if succeeded
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder add_sen :: sen -> IO(Bool), -- returns True if succeeded
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder remove_sen :: sen -> IO(Bool), -- returns True if succeeded
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder add_termination_info :: [symbol] -> [(symbol,[symbol])] -> IO(Bool), -- returns True if succeeded
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder remove_termination_info :: [symbol] -> [(symbol,[symbol])] -> IO(Bool), -- returns True if succeeded
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder replay :: proof_tree -> Maybe sen -- what about the theory???
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedertype Prover sign sentence proof_tree =
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder ProverTemplate (Theory sign sentence proof_tree) proof_tree
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maedertype ConsChecker sign sentence morphism proof_tree =
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder ProverTemplate (TheoryMorphism sign sentence morphism proof_tree) proof_tree
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedertheoryTc :: TyCon
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedertheoryTc = mkTyCon "Logic.Prover.Theory"
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maederinstance (Typeable a, Typeable b,Typeable c)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder => Typeable (Theory a b c) where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski typeOf t = mkTyConApp theoryTc
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [typeOf ((undefined :: Theory a b c -> a) t),
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder typeOf ((undefined :: Theory a b c -> b) t),
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder typeOf ((undefined :: Theory a b c -> c) t)]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitheoryMorTc :: TyCon
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertheoryMorTc = mkTyCon "Logic.Prover.TheoryMorphism"
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederinstance (Typeable a, Typeable b, Typeable c, Typeable d)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder => Typeable (TheoryMorphism a b c d) where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder typeOf t = mkTyConApp theoryMorTc
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder [typeOf ((undefined :: TheoryMorphism a b c d -> a) t),
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder typeOf ((undefined :: TheoryMorphism a b c d -> b) t),
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder typeOf ((undefined :: TheoryMorphism a b c d -> c) t),
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder typeOf ((undefined :: TheoryMorphism a b c d -> d) t)]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederproverTc :: TyCon
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederproverTc = mkTyCon "Logic.Prover.ProverTemplate"
99476ac2689c74251219db4782e57fe713a24a52Christian Maederinstance (Typeable a, Typeable b) => Typeable (ProverTemplate a b) where
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder typeOf p = mkTyConApp proverTc
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder [typeOf ((undefined :: ProverTemplate a b -> a) p),
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder typeOf ((undefined :: ProverTemplate a b -> b) p)]
3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian MaedertcProof_status :: TyCon
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertcProof_status = mkTyCon "Logic.Prover.Proof_status"
99476ac2689c74251219db4782e57fe713a24a52Christian Maederinstance Typeable proof_tree => Typeable (Proof_status proof_tree) where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder typeOf b = mkTyConApp tcProof_status
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder [typeOf $ (undefined :: Proof_status proof_tree -> proof_tree) b]