a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett , GeneralizedNewtypeDeriving #-}

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski{- |

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederModule : $Header$

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : theory datastructure for development graphs

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiLicense : GPLv2 or higher, see LICENSE.txt

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@informatik.uni-bremen.de

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable(Logic)

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachtheory datastructure for development graphs

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule Static.GTheory where

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiimport Logic.Prover

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiimport Logic.Logic

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiimport Logic.ExtSign

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maederimport Logic.Grothendieck

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Logic.Comorphism

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Logic.Coerce

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Common.OrderedMap as OMap

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport ATerm.Lib

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Lib.Graph as Tree

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Amalgamate -- for now

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Keywords

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.AS_Annotation

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Doc

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.DocUtils

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.ExtSign

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Result

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Data.Graph.Inductive.Graph as Graph

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Data.Map as Map

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettimport Data.Typeable

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Control.Monad (foldM)

0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblettimport Control.Exception

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett

567db7182e691cce5816365d8c912d09ffe92f86Andy Gimblett-- a theory index describing a set of sentences

0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblettnewtype ThId = ThId Int

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)

0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy GimblettstartThId :: ThId

c4b2418421546a337f83332fe0db04742dcd735dAndy GimblettstartThId = ThId 0

9f6c50e7b48ca79fc104275f9b1ea091a1359f89Andy Gimblett

9f6c50e7b48ca79fc104275f9b1ea091a1359f89Andy Gimblett-- | Grothendieck theories with lookup indices

167414650dc57c11c13ba85253f0211b3de0ecc5Christian Maederdata G_theory = forall lid sublogics

167414650dc57c11c13ba85253f0211b3de0ecc5Christian Maeder basic_spec sentence symb_items symb_map_items

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett sign morphism symbol raw_symbol proof_tree .

167414650dc57c11c13ba85253f0211b3de0ecc5Christian Maeder Logic lid sublogics

167414650dc57c11c13ba85253f0211b3de0ecc5Christian Maeder basic_spec sentence symb_items symb_map_items

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski sign morphism symbol raw_symbol proof_tree => G_theory

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski { gTheoryLogic :: lid

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett , gTheorySign :: ExtSign sign symbol

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett , gTheorySignIdx :: SigId -- ^ index to lookup 'G_sign' (using 'signOf')

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett , gTheorySens :: ThSens sentence (AnyComorphism, BasicProof)

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski , gTheorySelfIdx :: ThId -- ^ index to lookup this 'G_theory' in theory map

567db7182e691cce5816365d8c912d09ffe92f86Andy Gimblett } deriving Typeable

567db7182e691cce5816365d8c912d09ffe92f86Andy Gimblett

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachcreateGThWith :: G_theory -> SigId -> ThId -> G_theory

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachcreateGThWith (G_theory gtl gts _ _ _) si = G_theory gtl gts si noSens

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaedercoerceThSens ::

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach sign2 morphism2 symbol2 raw_symbol2 proof_tree2

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , Monad m, Typeable b)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach => lid1 -> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachcoerceThSens = primCoerce

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachinstance Eq G_theory where

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach G_theory l1 sig1 ind1 sens1 ind1' == G_theory l2 sig2 ind2 sens2 ind2' =

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach G_sign l1 sig1 ind1 == G_sign l2 sig2 ind2

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach && (ind1' > startThId && ind2' > startThId && ind1' == ind2'

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach || coerceThSens l1 l2 "" sens1 == Just sens2)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maederinstance Show G_theory where

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach show (G_theory _ sign _ sens _) =

567db7182e691cce5816365d8c912d09ffe92f86Andy Gimblett shows sign $ '\n' : show sens

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder

af745a4a6cb26002e55b69f90d837fe9c6176d4bAndy Gimblettinstance Pretty G_theory where

af745a4a6cb26002e55b69f90d837fe9c6176d4bAndy Gimblett pretty g = prettyGTheorySL g $++$ prettyGTheory g

af745a4a6cb26002e55b69f90d837fe9c6176d4bAndy Gimblett

prettyGTheorySL :: G_theory -> Doc

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

prettyGTheory :: G_theory -> Doc

prettyGTheory g = case simplifyTh g of

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

if null l && ext_is_subsig lid sign (ext_empty_signature lid) then

specBraces Common.Doc.empty else printTheory lid (s, l)

-- | compute sublogic of a theory

sublogicOfTh :: G_theory -> G_sublogics

sublogicOfTh (G_theory lid (ExtSign sigma _) _ sens _) =

let sub = foldl join

(minSublogic sigma)

(map snd $ OMap.toList $

OMap.map (minSublogic . sentence)

sens)

in G_sublogics lid sub

-- | get theorem names with their best proof results

getThGoals :: G_theory -> [(String, Maybe BasicProof)]

getThGoals (G_theory _ _ _ sens _) = map toGoal . OMap.toList

$ OMap.filter (not . isAxiom) sens

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

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

-- | get axiom names plus True for former theorem

getThAxioms :: G_theory -> [(String, Bool)]

getThAxioms (G_theory _ _ _ sens _) = map

(\ (k, s) -> (k, wasTheorem s))

$ OMap.toList $ OMap.filter isAxiom sens

-- | simplify a theory (throw away qualifications)

simplifyTh :: G_theory -> G_theory

simplifyTh (G_theory lid sigma@(ExtSign s _) ind1 sens ind2) =

G_theory lid sigma ind1

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

-- | apply a comorphism to a theory

mapG_theory :: AnyComorphism -> G_theory -> Result G_theory

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

do

bTh <- coerceBasicTheory lid (sourceLogic cid)

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

(sign, toNamedList sens)

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

return $ G_theory (targetLogic cid) (mkExtSign sign')

ind1 (toThSens sens') ind2

-- | Translation of a G_theory along a GMorphism

translateG_theory :: GMorphism -> G_theory -> Result G_theory

translateG_theory (GMorphism cid _ _ morphism2 _)

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

let tlid = targetLogic cid

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 (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 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 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 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

-> G_theory -- ^ new local theory with deleted proofs

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

let vAxs = getValidAxioms oTh nTh

validProofs (_, bp) = case bp of

BasicProof _ pst -> all (`elem` vAxs) $ usedAxioms pst

_ -> True

newSens = OMap.map

(\ s -> if isAxiom s then s else

s { senAttr = ThmStatus $ filter validProofs

$ thmStatus s }) sens

in G_theory lid sig si 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 sig ind sens _) =

case coerceThSens glid lid "proveLocalSens" gsens of

Just lsens -> G_theory lid 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 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 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"