Prover.hs revision 48fd7a27ee103bd46c8993836280985bddebb6b3
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikiModule : $Header$
353bea4bd4f2d567232d91686f797810bc176f2etakashiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
031b91a62d25106ae69d4693475c79618dd5e884fieldingMaintainer : till@tzi.de
031b91a62d25106ae69d4693475c79618dd5e884fieldingStability : provisional
031b91a62d25106ae69d4693475c79618dd5e884fieldingPortability : portable
031b91a62d25106ae69d4693475c79618dd5e884fieldingProvide prover stuff for class Logic.Sentences
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport qualified Common.AS_Annotation as AS_Anno
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport qualified Common.OrderedMap as OMap
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport qualified Common.Lib.Map as Map (toList,fromList)
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki-- * sentence packing
208651a016b098f4fa1f6279559f104d70f1632dtakashidata SenStatus a tStatus = SenStatus
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki { value :: a
208651a016b098f4fa1f6279559f104d70f1632dtakashi , isAxiom :: Bool
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki , isDef :: Bool
208651a016b098f4fa1f6279559f104d70f1632dtakashi , thmStatus :: [tStatus]
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki } deriving Show
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikiinstance PrettyPrint a => PrettyPrint (SenStatus a b) where
208651a016b098f4fa1f6279559f104d70f1632dtakashi printText0 ga x = printText0 ga (value x)
208651a016b098f4fa1f6279559f104d70f1632dtakashiemptySenStatus :: SenStatus a b
208651a016b098f4fa1f6279559f104d70f1632dtakashiemptySenStatus = SenStatus { value = error "emptySenStatus"
208651a016b098f4fa1f6279559f104d70f1632dtakashi , isDef = False
208651a016b098f4fa1f6279559f104d70f1632dtakashi , isAxiom = True
208651a016b098f4fa1f6279559f104d70f1632dtakashi , thmStatus = [] }
208651a016b098f4fa1f6279559f104d70f1632dtakashiinstance Eq a => Eq (SenStatus a b) where
208651a016b098f4fa1f6279559f104d70f1632dtakashi d1 == d2 = (value d1) == (value d2)
208651a016b098f4fa1f6279559f104d70f1632dtakashiinstance Ord a => Ord (SenStatus a b) where
208651a016b098f4fa1f6279559f104d70f1632dtakashi d1 <= d2 = (value d1) <= (value d2)
208651a016b098f4fa1f6279559f104d70f1632dtakashidecoTc :: TyCon
208651a016b098f4fa1f6279559f104d70f1632dtakashidecoTc = mkTyCon "Static.DevGraph.SenStatus"
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikiinstance (Typeable s,Typeable b) => Typeable (SenStatus s b) where
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf s = mkTyConApp decoTc [typeOf ((undefined :: SenStatus a b -> a) s),
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf ((undefined :: SenStatus a b -> b) s)]
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikielemWOrdTc :: TyCon
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikielemWOrdTc = mkTyCon "Common.OrderedMap.ElemWOrd"
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikiinstance (Typeable a) => Typeable (OMap.ElemWOrd a) where
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf s = mkTyConApp elemWOrdTc [typeOf ((undefined :: OMap.ElemWOrd a -> a) s)]
208651a016b098f4fa1f6279559f104d70f1632dtakashiinstance PrettyPrint a => PrettyPrint (OMap.ElemWOrd a) where
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki printText0 ga e = printText0 ga (OMap.ele e)
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikitype ThSens a b = OMap.OMap String (SenStatus a b)
208651a016b098f4fa1f6279559f104d70f1632dtakashinoSens :: ThSens a b
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- | join and disambiguate
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki-- * separate Axioms from Theorems
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki-- * don't merge sentences with same key but different contents?
208651a016b098f4fa1f6279559f104d70f1632dtakashijoinSens :: (Ord a,Eq b) => ThSens a b -> ThSens a b -> ThSens a b
208651a016b098f4fa1f6279559f104d70f1632dtakashijoinSens s1 s2 = let l1 = sortBy (comparing snd) $ Map.toList s1
208651a016b098f4fa1f6279559f104d70f1632dtakashi updN n (_,e) = (n,e)
208651a016b098f4fa1f6279559f104d70f1632dtakashi l2 = map (\ (x,e) ->
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki sortBy (comparing snd) $ Map.toList s2
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki in Map.fromList $ mergeSens l1 $
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki genericDisambigSens fst updN (OMap.keysSet s1) l2
208651a016b098f4fa1f6279559f104d70f1632dtakashi where mergeSens [] l2 = l2
208651a016b098f4fa1f6279559f104d70f1632dtakashi mergeSens l1 [] = l1
208651a016b098f4fa1f6279559f104d70f1632dtakashi mergeSens l1@((k1,e1) : r1) l2@((k2,e2) : r2) =
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki case compare e1 e2 of
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki LT -> (k1,e1) : mergeSens r1 l2
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki { thmStatus =
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki union (thmStatus $ OMap.ele e1)
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki (thmStatus $ OMap.ele e2)}})
a4b591abd5d8601b85aeed3ec7e129420a2c91a5kawai : mergeSens r1 r2
208651a016b098f4fa1f6279559f104d70f1632dtakashi | otherwise -> (k1,e1):mergeSens r1 l2
208651a016b098f4fa1f6279559f104d70f1632dtakashi GT -> (k2,e2) : mergeSens l1 r2
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikimapValue :: (a -> b) -> SenStatus a c -> SenStatus b c
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikimapValue f d = d { value = f $ value d }
208651a016b098f4fa1f6279559f104d70f1632dtakashimarkAsGoal :: Ord a => ThSens a b -> ThSens a b
208651a016b098f4fa1f6279559f104d70f1632dtakashimarkAsGoal = OMap.map (\d -> d { isAxiom = False})
208651a016b098f4fa1f6279559f104d70f1632dtakashitoNamedList :: ThSens a b -> [AS_Anno.Named a]
208651a016b098f4fa1f6279559f104d70f1632dtakashitoNamedList = map (uncurry toNamed) . OMap.toList
208651a016b098f4fa1f6279559f104d70f1632dtakashitoNamed :: String -> SenStatus a b -> AS_Anno.Named a
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki , AS_Anno.isAxiom = isAxiom s}
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki-- | putting Sentences from a list into a map
208651a016b098f4fa1f6279559f104d70f1632dtakashitoThSens :: Ord a => [AS_Anno.Named a] -> ThSens a b
208651a016b098f4fa1f6279559f104d70f1632dtakashitoThSens = OMap.fromList . map
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki emptySenStatus { value = AS_Anno.sentence v
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki , isDef = AS_Anno.isDef v }))
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- theories and theory morphisms
208651a016b098f4fa1f6279559f104d70f1632dtakashidata Theory sign sen proof_tree =
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki Theory sign (ThSens sen (Proof_status proof_tree))
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikidata TheoryMorphism sign sen mor proof_tree =
208651a016b098f4fa1f6279559f104d70f1632dtakashi TheoryMorphism {t_source :: Theory sign sen proof_tree,
208651a016b098f4fa1f6279559f104d70f1632dtakashi t_target :: Theory sign sen proof_tree,
208651a016b098f4fa1f6279559f104d70f1632dtakashi t_morphism :: mor
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- proofs and provers
208651a016b098f4fa1f6279559f104d70f1632dtakashi-- e.g. the file name, or the script itself, or a configuration string
208651a016b098f4fa1f6279559f104d70f1632dtakashidata Tactic_script = Tactic_script String deriving (Eq, Ord, Show)
208651a016b098f4fa1f6279559f104d70f1632dtakashidata Proof_status proof_tree =
208651a016b098f4fa1f6279559f104d70f1632dtakashi Open { goalName :: String }
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki | Disproved { goalName :: String }
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki | Proved { goalName :: String,
208651a016b098f4fa1f6279559f104d70f1632dtakashi usedAxioms :: [String], -- used axioms or theorems or goals
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki proverName :: String, -- name of prover
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki proofTree :: proof_tree,
208651a016b098f4fa1f6279559f104d70f1632dtakashi tacticScript :: Tactic_script }
208651a016b098f4fa1f6279559f104d70f1632dtakashi | Consistent Tactic_script
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki deriving (Eq, Show)
208651a016b098f4fa1f6279559f104d70f1632dtakashiinstance Eq a => Ord (Proof_status a) where
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki Open _ <= _ = True
208651a016b098f4fa1f6279559f104d70f1632dtakashi Disproved _ <= x = case x of
208651a016b098f4fa1f6279559f104d70f1632dtakashi Open _ -> False
208651a016b098f4fa1f6279559f104d70f1632dtakashi Proved _ _ _ _ _ <= x = case x of
208651a016b098f4fa1f6279559f104d70f1632dtakashi Proved _ _ _ _ _ -> True
208651a016b098f4fa1f6279559f104d70f1632dtakashi _ <= _ = False
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikiisProvedStat :: Proof_status proof_tree -> Bool
208651a016b098f4fa1f6279559f104d70f1632dtakashiisProvedStat (Proved _ _ _ _ _) = True
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikiisProvedStat _ = False
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikidata ProverTemplate goal proof_tree = Prover
208651a016b098f4fa1f6279559f104d70f1632dtakashi { prover_name :: String,
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki prover_sublogic :: String,
208651a016b098f4fa1f6279559f104d70f1632dtakashi prove :: String -> goal -> IO([Proof_status proof_tree])
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki -- input: theory name, theory, goals
208651a016b098f4fa1f6279559f104d70f1632dtakashi -- output: proof status for goals and lemmas
a1f584caa24d05addeef8d264232afe0c60e0482yoshiki{- possibly needed in the future
353bea4bd4f2d567232d91686f797810bc176f2etakashi add_sym :: symbol -> IO(Bool), -- returns True if succeeded
a1f584caa24d05addeef8d264232afe0c60e0482yoshiki remove_sym :: symbol -> IO(Bool), -- returns True if succeeded
208651a016b098f4fa1f6279559f104d70f1632dtakashi add_sen :: sen -> IO(Bool), -- returns True if succeeded
208651a016b098f4fa1f6279559f104d70f1632dtakashi remove_sen :: sen -> IO(Bool), -- returns True if succeeded
208651a016b098f4fa1f6279559f104d70f1632dtakashi add_termination_info :: [symbol] -> [(symbol,[symbol])] -> IO(Bool), -- returns True if succeeded
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki remove_termination_info :: [symbol] -> [(symbol,[symbol])] -> IO(Bool), -- returns True if succeeded
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki replay :: proof_tree -> Maybe sen -- what about the theory???
208651a016b098f4fa1f6279559f104d70f1632dtakashitype Prover sign sentence proof_tree =
208651a016b098f4fa1f6279559f104d70f1632dtakashi ProverTemplate (Theory sign sentence proof_tree) proof_tree
208651a016b098f4fa1f6279559f104d70f1632dtakashitype ConsChecker sign sentence morphism proof_tree =
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki ProverTemplate (TheoryMorphism sign sentence morphism proof_tree) proof_tree
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshikitheoryTc :: TyCon
208651a016b098f4fa1f6279559f104d70f1632dtakashitheoryTc = mkTyCon "Logic.Prover.Theory"
208651a016b098f4fa1f6279559f104d70f1632dtakashiinstance (Typeable a, Typeable b,Typeable c)
208651a016b098f4fa1f6279559f104d70f1632dtakashi => Typeable (Theory a b c) where
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki typeOf t = mkTyConApp theoryTc
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki [typeOf ((undefined :: Theory a b c -> a) t),
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf ((undefined :: Theory a b c -> b) t),
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf ((undefined :: Theory a b c -> c) t)]
208651a016b098f4fa1f6279559f104d70f1632dtakashitheoryMorTc :: TyCon
208651a016b098f4fa1f6279559f104d70f1632dtakashitheoryMorTc = mkTyCon "Logic.Prover.TheoryMorphism"
208651a016b098f4fa1f6279559f104d70f1632dtakashiinstance (Typeable a, Typeable b, Typeable c, Typeable d)
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki => Typeable (TheoryMorphism a b c d) where
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf t = mkTyConApp theoryMorTc
208651a016b098f4fa1f6279559f104d70f1632dtakashi [typeOf ((undefined :: TheoryMorphism a b c d -> a) t),
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki typeOf ((undefined :: TheoryMorphism a b c d -> b) t),
f6e426d8627afcd70d2cd78c21f0f8afe7964f93yoshiki typeOf ((undefined :: TheoryMorphism a b c d -> c) t),
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf ((undefined :: TheoryMorphism a b c d -> d) t)]
208651a016b098f4fa1f6279559f104d70f1632dtakashiproverTc :: TyCon
208651a016b098f4fa1f6279559f104d70f1632dtakashiproverTc = mkTyCon "Logic.Prover.ProverTemplate"
208651a016b098f4fa1f6279559f104d70f1632dtakashiinstance (Typeable a, Typeable b) => Typeable (ProverTemplate a b) where
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf p = mkTyConApp proverTc
208651a016b098f4fa1f6279559f104d70f1632dtakashi [typeOf ((undefined :: ProverTemplate a b -> a) p),
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf ((undefined :: ProverTemplate a b -> b) p)]
208651a016b098f4fa1f6279559f104d70f1632dtakashitcProof_status :: TyCon
208651a016b098f4fa1f6279559f104d70f1632dtakashitcProof_status = mkTyCon "Logic.Prover.Proof_status"
208651a016b098f4fa1f6279559f104d70f1632dtakashiinstance Typeable proof_tree => Typeable (Proof_status proof_tree) where
208651a016b098f4fa1f6279559f104d70f1632dtakashi typeOf b = mkTyConApp tcProof_status
208651a016b098f4fa1f6279559f104d70f1632dtakashi [typeOf $ (undefined :: Proof_status proof_tree -> proof_tree) b]