b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu{-|

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner

127a36cba0c92b465681ec55ad366aca423735ebChristian MaederModule : $Header$

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder

127a36cba0c92b465681ec55ad366aca423735ebChristian MaederMaintainer : hets@tzi.de

127a36cba0c92b465681ec55ad366aca423735ebChristian MaederStability : provisional

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuPortability : portable

b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder Provide prover stuff for class Logic.Sentences

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder-}

cd76927a77fc0f09d1087ed4a5ad45e3602feb75Christian Maeder

ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maedermodule Logic.Prover where

ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport Common.DynamicUtils

09ca01bcf4700ec3ea86d06ec08b9485e4a908d5Klaus Luettichimport Common.AS_Annotation (Named)

09ca01bcf4700ec3ea86d06ec08b9485e4a908d5Klaus Luettichimport Data.Dynamic

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder-- theories and theory morphisms

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder

09ca01bcf4700ec3ea86d06ec08b9485e4a908d5Klaus Luettichtype Theory sign sen = (sign,[Named sen])

09ca01bcf4700ec3ea86d06ec08b9485e4a908d5Klaus Luettich

127a36cba0c92b465681ec55ad366aca423735ebChristian Maederdata TheoryMorphism sign sen mor =

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder TheoryMorphism {t_source, t_target :: Theory sign sen,

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder t_morphism :: mor

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder }

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder-- proofs and provers

127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder

type Rule = String

type Tactic_script = String -- the file name

data Proof_status proof_tree = Open String

| Disproved String

| Proved(String,

[String], -- used axioms

String, -- name of prover

proof_tree,

Tactic_script)

deriving (Eq, Show, Read)

data Prover sign sen proof_tree symbol =

Prover { prover_name :: String,

prover_sublogic :: String,

prove :: String -> (sign, [Named sen]) -> [Named sen]

-> IO([Proof_status proof_tree])

-- input: theory name, theory, goals

-- output: proof status for goals and lemmas

}

{- possibly needed in the future

add_sym :: symbol -> IO(Bool), -- returns True if succeeded

remove_sym :: symbol -> IO(Bool), -- returns True if succeeded

add_sen :: sen -> IO(Bool), -- returns True if succeeded

remove_sen :: sen -> IO(Bool), -- returns True if succeeded

add_termination_info :: [symbol] -> [(symbol,[symbol])] -> IO(Bool), -- returns True if succeeded

remove_termination_info :: [symbol] -> [(symbol,[symbol])] -> IO(Bool), -- returns True if succeeded

replay :: proof_tree -> Maybe sen -- what about the theory???

-}

data ConsChecker morphism =

ConsChecker {cons_checker_name :: String,

cons_checker_sublogic :: String,

cons_check :: morphism -> IO(Maybe Bool, Tactic_script)

}

proverTc :: TyCon

proverTc = mkTyCon "Logic.Prover.Prover"

instance Typeable (Prover sign sen proof_tree symbol) where

typeOf _ = mkTyConApp proverTc []

consCheckerTc :: TyCon

consCheckerTc = mkTyCon "Logic.Prover.ConsChecker"

instance Typeable (ConsChecker mor) where

typeOf _ = mkTyConApp consCheckerTc []

tcProof_status :: TyCon

tcProof_status = mkTyCon "Logic.Prover.Proof_status"

instance Typeable proof_tree

=> Typeable (Proof_status proof_tree) where

typeOf b = mkTyConApp tcProof_status

[typeOf $ (undefined :: Proof_status proof_tree -> proof_tree) b]