Prover.hs revision 8b5f9f72ba210940b26034bcadd34b2fe7f93bbd
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederMaintainer : hets@tzi.de
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederStability : provisional
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederPortability : portable
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder Provide prover stuff for class Logic.Sentences
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder-- theories and theory morphisms
f353be6210f67ffd4a46967bba749afc968cee52Christian Maederdata Theory sign sen = Theory sign [Named sen]
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederdata TheoryMorphism sign sen mor =
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder TheoryMorphism {t_source, t_target :: Theory sign sen,
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder t_morphism :: mor
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-- proofs and provers
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder-- e.g. the file name, or the script itself, or a configuration string
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedertype Tactic_script = String
2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maederdata Proof_status proof_tree = Open String
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder | Disproved String
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder | Proved(String,
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder [String], -- used axioms
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder String, -- name of prover
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder Tactic_script)
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder | Consistent Tactic_script
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder deriving (Eq, Show, Read)
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederdata ProverTemplate goal proof_tree = Prover
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder { prover_name :: String,
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder prover_sublogic :: String,
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder prove :: String -> goal -> IO([Proof_status proof_tree])
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder -- input: theory name, theory, goals
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -- output: proof status for goals and lemmas
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder{- possibly needed in the future
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder add_sym :: symbol -> IO(Bool), -- returns True if succeeded
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder remove_sym :: symbol -> IO(Bool), -- returns True if succeeded
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder add_sen :: sen -> IO(Bool), -- returns True if succeeded
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder remove_sen :: sen -> IO(Bool), -- returns True if succeeded
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder add_termination_info :: [symbol] -> [(symbol,[symbol])] -> IO(Bool), -- returns True if succeeded
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder remove_termination_info :: [symbol] -> [(symbol,[symbol])] -> IO(Bool), -- returns True if succeeded
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder replay :: proof_tree -> Maybe sen -- what about the theory???
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maedertype Prover sign sentence proof_tree =
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder ProverTemplate (Theory sign sentence) proof_tree
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maedertype ConsChecker sign sentence morphism proof_tree =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ProverTemplate (TheoryMorphism sign sentence morphism) proof_tree
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedertheoryTc :: TyCon
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedertheoryTc = mkTyCon "Logic.Prover.Theory"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance (Typeable a, Typeable b) => Typeable (Theory a b) where
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder typeOf t = mkTyConApp theoryTc
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder [typeOf ((undefined :: Theory a b -> a) t),
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder typeOf ((undefined :: Theory a b -> b) t)]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertheoryMorTc :: TyCon
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertheoryMorTc = mkTyCon "Logic.Prover.TheoryMorphism"
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiinstance (Typeable a, Typeable b, Typeable c)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder => Typeable (TheoryMorphism a b c) where
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder typeOf t = mkTyConApp theoryMorTc
2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder [typeOf ((undefined :: TheoryMorphism a b c -> a) t),
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder typeOf ((undefined :: TheoryMorphism a b c -> b) t),
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder typeOf ((undefined :: TheoryMorphism a b c -> c) t)]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederproverTc :: TyCon
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederproverTc = mkTyCon "Logic.Prover.ProverTemplate"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance (Typeable a, Typeable b) => Typeable (ProverTemplate a b) where
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder typeOf p = mkTyConApp proverTc
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder [typeOf ((undefined :: ProverTemplate a b -> a) p),
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder typeOf ((undefined :: ProverTemplate a b -> b) p)]
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedertcProof_status :: TyCon
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedertcProof_status = mkTyCon "Logic.Prover.Proof_status"
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederinstance Typeable proof_tree => Typeable (Proof_status proof_tree) where
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder typeOf b = mkTyConApp tcProof_status
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder [typeOf $ (undefined :: Proof_status proof_tree -> proof_tree) b]