{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable

, GeneralizedNewtypeDeriving #-}

{- |

Module : ./Static/GTheory.hs

Description : theory datastructure for development graphs

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

License : GPLv2 or higher, see LICENSE.txt

Maintainer : till@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable(Logic)

theory datastructure for development graphs

-}

module Static.GTheory where

import Logic.Prover

import Logic.Logic

import Logic.ExtSign

import Logic.Grothendieck

import Logic.Comorphism

import Logic.Coerce

import qualified Common.OrderedMap as OMap

import ATerm.Lib

import Common.Lib.Graph as Tree

import Common.Amalgamate -- for now

import Common.Keywords

import Common.AS_Annotation

import Common.Doc

import Common.DocUtils

import Common.ExtSign

import Common.IRI

import Common.Result

import Data.Graph.Inductive.Graph as Graph

import Data.List

import qualified Data.Map as Map

import Data.Typeable

import Control.Monad (foldM)

import Control.Exception

-- a theory index describing a set of sentences

newtype ThId = ThId Int

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

startThId :: ThId

startThId = ThId 0

-- | Grothendieck theories with lookup indices

data G_theory = 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 => G_theory

{ gTheoryLogic :: lid

, gTheorySyntax :: Maybe IRI

, gTheorySign :: ExtSign sign symbol

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

, gTheorySens :: ThSens sentence (AnyComorphism, BasicProof)

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

} deriving Typeable

createGThWith :: G_theory -> SigId -> ThId -> G_theory

createGThWith (G_theory gtl gsub gts _ _ _) si =

G_theory gtl gsub gts si noSens

coerceThSens ::

( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2

, Monad m, Typeable b)

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

coerceThSens = primCoerce

instance Eq G_theory where

G_theory l1 ser1 sig1 ind1 sens1 ind1'

== G_theory l2 ser2 sig2 ind2 sens2 ind2' = ser1 == ser2

&& G_sign l1 sig1 ind1 == G_sign l2 sig2 ind2

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

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

instance Show G_theory where

show (G_theory _ _ sign _ sens _) =

shows sign $ '\n' : show sens

instance Pretty G_theory where

pretty g = prettyFullGTheory (gTheorySyntax g) g

prettyFullGTheory :: Maybe IRI -> G_theory -> Doc

prettyFullGTheory sm g = prettyGTheorySL g $++$ prettyGTheory sm g

prettyGTheorySL :: G_theory -> Doc

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

prettyGTheory :: Maybe IRI -> G_theory -> Doc

prettyGTheory sm 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 sm lid (s, l)

-- | compute sublogic of a theory

sublogicOfTh :: G_theory -> G_sublogics

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

let sub = foldl lub

(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

-- | get sentence names

getThSens :: G_theory -> [String]

getThSens (G_theory _ _ _ _ sens _) = map fst $ OMap.toList sens

-- | simplify a theory (throw away qualifications)

simplifyTh :: G_theory -> G_theory

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

G_theory lid gsyn 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) Nothing (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 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

-- | Intersect the sentences of two G_theories, G_sign is the intersection of their signatures

intersectG_sentences :: Monad m => G_sign -> G_theory -> G_theory -> m G_theory

intersectG_sentences gsig@(G_sign lidS signS indS)

(G_theory lid1 syn sig1 ind sens1 _)

(G_theory lid2 _ sig2 _ sens2 _) = do

sens1' <- coerceThSens lid1 lidS "intersectG_sentences1" sens1

sens2' <- coerceThSens lid2 lidS "intersectG_sentences2" sens2

return $ G_theory lidS Nothing signS indS (intersectSens 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"