66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder , GeneralizedNewtypeDeriving #-}

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederModule : $Header$

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederDescription : theory datastructure for development graphs

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : till@informatik.uni-bremen.de

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : provisional

fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederPortability : non-portable(Logic)

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maedertheory datastructure for development graphs

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule Static.GTheory where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maederimport Logic.Prover

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Logic.Logic

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Logic.ExtSign

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Logic.Grothendieck

30203b61afb4393c8e459470b3a16d1fe26acc7fChristian Maederimport Logic.Comorphism

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maederimport Logic.Coerce

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maederimport qualified Common.OrderedMap as OMap

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder

f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maederimport ATerm.Lib

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Lib.Graph as Tree

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederimport Common.Amalgamate -- for now

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Common.Keywords

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport Common.AS_Annotation

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.Doc

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport Common.DocUtils

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport Common.ExtSign

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport Common.IRI

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport Common.Result

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport Data.Graph.Inductive.Graph as Graph

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Data.List

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport qualified Data.Map as Map

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Data.Typeable

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

51281dddda866c0cda9fca22bf6bc4eea7128112Christian Maederimport Control.Monad (foldM)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Control.Exception

ac07a6558423dae7adc488ed9092cd8e9450a29dChristian Maeder

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder-- a theory index describing a set of sentences

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maedernewtype ThId = ThId Int

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederstartThId :: ThId

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederstartThId = ThId 0

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- | Grothendieck theories with lookup indices

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederdata G_theory = forall lid sublogics

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder basic_spec sentence symb_items symb_map_items

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder sign morphism symbol raw_symbol proof_tree .

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Logic lid sublogics

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder basic_spec sentence symb_items symb_map_items

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maeder sign morphism symbol raw_symbol proof_tree => G_theory

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maeder { gTheoryLogic :: lid

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , gTheorySyntax :: Maybe IRI

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , gTheorySign :: ExtSign sign symbol

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , gTheorySignIdx :: SigId -- ^ index to lookup 'G_sign' (using 'signOf')

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , gTheorySens :: ThSens sentence (AnyComorphism, BasicProof)

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , gTheorySelfIdx :: ThId -- ^ index to lookup this 'G_theory' in theory map

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder } deriving Typeable

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian MaedercreateGThWith :: G_theory -> SigId -> ThId -> G_theory

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedercreateGThWith (G_theory gtl gsub gts _ _ _) si =

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder G_theory gtl gsub gts si noSens

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercoerceThSens ::

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder , Monad m, Typeable b)

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder => lid1 -> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)

628310b42327ad76ce471caf0dde6563d6fa6307Christian MaedercoerceThSens = primCoerce

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederinstance Eq G_theory where

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder G_theory l1 ser1 sig1 ind1 sens1 ind1'

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder == G_theory l2 ser2 sig2 ind2 sens2 ind2' = ser1 == ser2

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder && G_sign l1 sig1 ind1 == G_sign l2 sig2 ind2

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder && (ind1' > startThId && ind2' > startThId && ind1' == ind2'

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder || coerceThSens l1 l2 "" sens1 == Just sens2)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederinstance Show G_theory where

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder show (G_theory _ _ sign _ sens _) =

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder shows sign $ '\n' : show sens

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maederinstance Pretty G_theory where

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder pretty g = prettyFullGTheory (gTheorySyntax g) g

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederprettyFullGTheory :: Maybe IRI -> G_theory -> Doc

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederprettyFullGTheory sm g = prettyGTheorySL g $++$ prettyGTheory sm g

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederprettyGTheorySL :: G_theory -> Doc

f0742398d4587242b1a115de113cd17f63dcb6d0Christian MaederprettyGTheorySL g = keyword logicS <+> structId (show $ sublogicOfTh g)

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederprettyGTheory :: Maybe IRI -> G_theory -> Doc

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederprettyGTheory sm g = case simplifyTh g of

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder G_theory lid _ sign@(ExtSign s _) _ sens _ -> let l = toNamedList sens in

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder if null l && ext_is_subsig lid sign (ext_empty_signature lid) then

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder specBraces Common.Doc.empty else printTheory sm lid (s, l)

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- | compute sublogic of a theory

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian MaedersublogicOfTh :: G_theory -> G_sublogics

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian MaedersublogicOfTh (G_theory lid _ (ExtSign sigma _) _ sens _) =

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder let sub = foldl join

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder (minSublogic sigma)

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder (map snd $ OMap.toList $

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder OMap.map (minSublogic . sentence)

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder sens)

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder in G_sublogics lid sub

4954b30d3c209d7dee4e43016cee8189daf646e8Christian Maeder

4954b30d3c209d7dee4e43016cee8189daf646e8Christian Maeder-- | get theorem names with their best proof results

4954b30d3c209d7dee4e43016cee8189daf646e8Christian MaedergetThGoals :: G_theory -> [(String, Maybe BasicProof)]

08b724e8dcbba5820d80f0974b9a5385140815baChristian MaedergetThGoals (G_theory _ _ _ _ sens _) = map toGoal . OMap.toList

4954b30d3c209d7dee4e43016cee8189daf646e8Christian Maeder $ OMap.filter (not . isAxiom) sens

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder where toGoal (n, st) = let ts = thmStatus st in

4954b30d3c209d7dee4e43016cee8189daf646e8Christian Maeder (n, if null ts then Nothing else Just $ maximum $ map snd ts)

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder

4954b30d3c209d7dee4e43016cee8189daf646e8Christian Maeder-- | get axiom names plus True for former theorem

5ea4161a514362065110614dd0d92adb13bf7cc3Christian MaedergetThAxioms :: G_theory -> [(String, Bool)]

4954b30d3c209d7dee4e43016cee8189daf646e8Christian MaedergetThAxioms (G_theory _ _ _ _ sens _) = map

5ea4161a514362065110614dd0d92adb13bf7cc3Christian Maeder (\ (k, s) -> (k, wasTheorem s))

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder $ OMap.toList $ OMap.filter isAxiom sens

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder-- | get sentence names

08b724e8dcbba5820d80f0974b9a5385140815baChristian MaedergetThSens :: G_theory -> [String]

08b724e8dcbba5820d80f0974b9a5385140815baChristian MaedergetThSens (G_theory _ _ _ _ sens _) = map fst $ OMap.toList sens

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | simplify a theory (throw away qualifications)

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedersimplifyTh :: G_theory -> G_theory

08b724e8dcbba5820d80f0974b9a5385140815baChristian MaedersimplifyTh (G_theory lid gsyn sigma@(ExtSign s _) ind1 sens ind2) =

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder G_theory lid gsyn sigma ind1

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (OMap.map (mapValue $ simplify_sen lid s) sens) ind2

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- | apply a comorphism to a theory

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermapG_theory :: AnyComorphism -> G_theory -> Result G_theory

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermapG_theory (Comorphism cid) (G_theory lid _ (ExtSign sign _) ind1 sens ind2) =

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder do

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder bTh <- coerceBasicTheory lid (sourceLogic cid)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder ("unapplicable comorphism '" ++ language_name cid ++ "'\n")

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (sign, toNamedList sens)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (sign', sens') <- wrapMapTheory cid bTh

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder return $ G_theory (targetLogic cid) Nothing (mkExtSign sign')

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder ind1 (toThSens sens') ind2

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- | Translation of a G_theory along a GMorphism

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertranslateG_theory :: GMorphism -> G_theory -> Result G_theory

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertranslateG_theory (GMorphism cid _ _ morphism2 _)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (G_theory lid _ (ExtSign sign _) _ sens _) = do

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder let tlid = targetLogic cid

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder bTh <- coerceBasicTheory lid (sourceLogic cid)

"translateG_theory" (sign, toNamedList sens)

(_, sens'') <- wrapMapTheory cid bTh

sens''' <- mapM (mapNamedM $ map_sen tlid morphism2) sens''

return $ G_theory tlid Nothing (mkExtSign $ cod morphism2)

startSigId (toThSens sens''') startThId

-- | Join the sentences of two G_theories

joinG_sentences :: Monad m => G_theory -> G_theory -> m G_theory

joinG_sentences (G_theory lid1 syn sig1 ind sens1 _)

(G_theory lid2 _ sig2 _ sens2 _) = do

sens2' <- coerceThSens lid2 lid1 "joinG_sentences" sens2

sig2' <- coerceSign lid2 lid1 "joinG_sentences" sig2

return $ assert (plainSign sig1 == plainSign sig2')

$ G_theory lid1 syn sig1 ind (joinSens sens1 sens2') startThId

-- | flattening the sentences form a list of G_theories

flatG_sentences :: Monad m => G_theory -> [G_theory] -> m G_theory

flatG_sentences = foldM joinG_sentences

-- | Get signature of a theory

signOf :: G_theory -> G_sign

signOf (G_theory lid _ sign ind _ _) = G_sign lid sign ind

-- | create theory without sentences

noSensGTheory :: Logic lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol proof_tree

=> lid -> ExtSign sign symbol -> SigId -> G_theory

noSensGTheory lid sig si = G_theory lid Nothing sig si noSens startThId

data BasicProof =

forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

BasicProof lid (ProofStatus proof_tree)

| Guessed

| Conjectured

| Handwritten

deriving Typeable

instance Eq BasicProof where

Guessed == Guessed = True

Conjectured == Conjectured = True

Handwritten == Handwritten = True

BasicProof lid1 p1 == BasicProof lid2 p2 =

coerceProofStatus lid1 lid2 "Eq BasicProof" p1 == Just p2

_ == _ = False

instance Ord BasicProof where

Guessed <= _ = True

Conjectured <= x = case x of

Guessed -> False

_ -> True

Handwritten <= x = case x of

Guessed -> False

Conjectured -> False

_ -> True

BasicProof lid1 pst1 <= x =

case x of

BasicProof lid2 pst2

| isProvedStat pst1 && not (isProvedStat pst2) -> False

| not (isProvedStat pst1) && isProvedStat pst2 -> True

| otherwise -> case primCoerce lid1 lid2 "" pst1 of

Nothing -> False

Just pst1' -> pst1' <= pst2

_ -> False

instance Show BasicProof where

show (BasicProof _ p1) = show p1

show Guessed = "Guessed"

show Conjectured = "Conjectured"

show Handwritten = "Handwritten"

-- | test a theory sentence

isProvenSenStatus :: SenStatus a (AnyComorphism, BasicProof) -> Bool

isProvenSenStatus = any (isProvedBasically . snd) . thmStatus

isProvedBasically :: BasicProof -> Bool

isProvedBasically b = case b of

BasicProof _ pst -> isProvedStat pst

_ -> False

getValidAxioms

:: G_theory -- ^ old global theory

-> G_theory -- ^ new global theory

-> [String] -- ^ unchanged axioms

getValidAxioms

(G_theory lid1 _ _ _ sens1 _)

(G_theory lid2 _ _ _ sens2 _) =

case coerceThSens lid1 lid2 "" sens1 of

Nothing -> []

Just sens -> OMap.keys $ OMap.filterWithKey (\ k s ->

case OMap.lookup k sens of

Just s2 -> isAxiom s && isAxiom s2 && sentence s == sentence s2

_ -> False) sens2

invalidateProofs

:: G_theory -- ^ old global theory

-> G_theory -- ^ new global theory

-> G_theory -- ^ local theory with proven goals

-> (Bool, G_theory) -- ^ no changes and new local theory with deleted proofs

invalidateProofs oTh nTh (G_theory lid syn sig si sens _) =

let vAxs = getValidAxioms oTh nTh

oAxs = map fst $ getThAxioms oTh

iValAxs = vAxs \\ oAxs

validProofs (_, bp) = case bp of

BasicProof _ pst -> not . any (`elem` iValAxs) $ usedAxioms pst

_ -> True

newSens = OMap.map

(\ s -> if isAxiom s then (True, s) else

let (ps, ups) = partition validProofs $ thmStatus s

in (null ups, s { senAttr = ThmStatus ps })) sens

in ( all fst $ OMap.elems newSens

, G_theory lid syn sig si (OMap.map snd newSens) startThId)

{- | mark sentences as proven if an identical axiom or other proven sentence

is part of the same theory. -}

proveSens :: Logic lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol proof_tree

=> lid -> ThSens sentence (AnyComorphism, BasicProof)

-> ThSens sentence (AnyComorphism, BasicProof)

proveSens lid sens = let

(axs, ths) = OMap.partition (\ s -> isAxiom s || isProvenSenStatus s) sens

in Map.union axs $ proveSensAux lid axs ths

proveLocalSens :: G_theory -> G_theory -> G_theory

proveLocalSens (G_theory glid _ _ _ gsens _)

lth@(G_theory lid syn sig ind sens _) =

case coerceThSens glid lid "proveLocalSens" gsens of

Just lsens -> G_theory lid syn sig ind

(proveSensAux lid (OMap.filter (\ s -> isAxiom s || isProvenSenStatus s)

lsens) sens) startThId

Nothing -> lth

{- | mark sentences as proven if an identical axiom or other proven sentence

is part of a given global theory. -}

proveSensAux :: Logic lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol proof_tree

=> lid -> ThSens sentence (AnyComorphism, BasicProof)

-> ThSens sentence (AnyComorphism, BasicProof)

-> ThSens sentence (AnyComorphism, BasicProof)

proveSensAux lid axs ths = let

axSet = Map.fromList $ map (\ (n, s) -> (sentence s, n)) $ OMap.toList axs

in Map.mapWithKey (\ i e -> let sen = OMap.ele e in

case Map.lookup (sentence sen) axSet of

Just ax ->

e { OMap.ele = sen { senAttr = ThmStatus $

( Comorphism $ mkIdComorphism lid $ top_sublogic lid

, BasicProof lid

(openProofStatus i "hets" $ empty_proof_tree lid)

{ usedAxioms = [ax]

, goalStatus = Proved True }) : thmStatus sen } }

_ -> e) ths

{- | mark all sentences of a local theory that have been proven via a prover

over a global theory (with the same signature) as proven. Also mark

duplicates of proven sentences as proven. Assume that the sentence names of

the local theory are identical to the global theory. -}

propagateProofs :: G_theory -> G_theory -> G_theory

propagateProofs locTh@(G_theory lid1 syn sig ind lsens _)

(G_theory lid2 _ _ _ gsens _) =

case coerceThSens lid2 lid1 "" gsens of

Just ps ->

if Map.null ps then locTh else

G_theory lid1 syn sig ind

(proveSens lid1 $ Map.union (Map.intersection ps lsens) lsens)

startThId

Nothing -> error "propagateProofs"

-- | Grothendieck diagrams

type GDiagram = Gr G_theory (Int, GMorphism)

-- | checks whether a connected GDiagram is homogeneous

isHomogeneousGDiagram :: GDiagram -> Bool

isHomogeneousGDiagram = all (\ (_, _, (_, phi)) -> isHomogeneous phi) . labEdges

-- | homogenise a GDiagram to a targeted logic

homogeniseGDiagram :: Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

=> lid -- ^ the target logic to be coerced to

-> GDiagram -- ^ the GDiagram to be homogenised

-> Result (Gr sign (Int, morphism))

homogeniseGDiagram targetLid diag = do

let convertNode (n, gth) = do

G_sign srcLid extSig _ <- return $ signOf gth

extSig' <- coerceSign srcLid targetLid "" extSig

return (n, plainSign extSig')

convertEdge (n1, n2, (nr, GMorphism cid _ _ mor _ ))

= if isIdComorphism (Comorphism cid) then

do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor

return (n1, n2, (nr, mor'))

else fail $

"Trying to coerce a morphism between different logics.\n" ++

"Heterogeneous specifications are not fully supported yet."

convertNodes cDiag [] = return cDiag

convertNodes cDiag (lNode : lNodes) = do

convNode <- convertNode lNode

let cDiag' = insNode convNode cDiag

convertNodes cDiag' lNodes

convertEdges cDiag [] = return cDiag

convertEdges cDiag (lEdge : lEdges) = do

convEdge <- convertEdge lEdge

let cDiag' = insEdge convEdge cDiag

convertEdges cDiag' lEdges

dNodes = labNodes diag

dEdges = labEdges diag

-- insert converted nodes to an empty diagram

cDiag <- convertNodes Graph.empty dNodes

-- insert converted edges to the diagram containing only nodes

convertEdges cDiag dEdges

{- | Coerce GMorphisms in the list of (diagram node, GMorphism) pairs

to morphisms in given logic -}

homogeniseSink :: Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

=> lid -- ^ the target logic to which morphisms will be coerced

-> [(Node, GMorphism)] -- ^ the list of edges to be homogenised

-> Result [(Node, morphism)]

homogeniseSink targetLid dEdges =

-- See homogeniseDiagram for comments on implementation.

let convertMorphism (n, GMorphism cid _ _ mor _) =

if isIdComorphism (Comorphism cid) then

do mor' <- coerceMorphism (targetLogic cid) targetLid "" mor

return (n, mor')

else fail $

"Trying to coerce a morphism between different logics.\n" ++

"Heterogeneous specifications are not fully supported yet."

convEdges [] = return []

convEdges (e : es) = do

ce <- convertMorphism e

ces <- convEdges es

return (ce : ces)

in convEdges dEdges

{- amalgamabilty check for heterogeneous diagrams

currently only checks whether the diagram is

homogeneous and if so, calls amalgamability check

for the specific logic -}

gEnsuresAmalgamability :: [CASLAmalgOpt] -- the options

-> GDiagram -- the diagram

-> [(Int, GMorphism)] -- the sink

-> Result Amalgamates

gEnsuresAmalgamability options gd sink =

if isHomogeneousGDiagram gd && all (isHomogeneous . snd) sink then

case labNodes gd of

(_, G_theory lid _ _ _ _ _) : _ -> do

diag <- homogeniseGDiagram lid gd

sink' <- homogeniseSink lid sink

ensures_amalgamability lid (options, diag, sink', Graph.empty)

_ -> error "heterogeneous amalgability check: no nodes"

else error "heterogeneous amalgability check not yet implemented"