{- |

Module : $Header$

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

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : till@tzi.de

Stability : provisional

Portability : non-portable(Logic)

Central data structure for development graphs.

Follows Sect. IV:4.2 of the CASL Reference Manual.

-}

{-

References:

T. Mossakowski, S. Autexier and D. Hutter:

Extending Development Graphs With Hiding.

H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,

Lecture Notes in Computer Science 2029, p. 269-283,

Springer-Verlag 2001.

T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:

CASL Proof calculus. In: CASL reference manual, part IV.

Available from http://www.cofi.info

todo:

Integrate stuff from Saarbr�cken

Should AS be stored in GloblaContext as well?

simplifyTh should be removed from instance PrettyPrint G_theory

-}

module Static.DevGraph where

import Logic.Logic

import Logic.Grothendieck

import Logic.Comorphism

import Logic.Prover

import Logic.Coerce

import Syntax.AS_Library

import Data.Graph.Inductive.Graph as Graph

import qualified Common.Lib.Graph as Tree

import qualified Common.Lib.Map as Map

import qualified Common.OrderedMap as OMap

import qualified Common.Lib.Set as Set

import Common.AS_Annotation

import Common.GlobalAnnotations

import Common.Id

import Common.Lib.Pretty

import Common.PrettyPrint

import Common.PPUtils

import Common.Result

import Common.DynamicUtils

import Control.Monad

import Control.Exception

getNewNode :: Tree.Gr a b -> Node

getNewNode g = case newNodes 1 g of

[n] -> n

_ -> error "Static.DevGraph.getNewNode"

-- * Types for structured specification analysis

-- ??? Some info about the theorems already proved for a node

-- should be added

-- or should it be kept separately?

-- what about open theorems of a node???

-- | name of a node in a DG; auxiliary nodes may have extension string

-- | and non-zero number (for these, names are usually hidden)

type NODE_NAME = (SIMPLE_ID, String, Int)

-- | node inscriptions in development graphs

data DGNodeLab =

DGNode {

dgn_name :: NODE_NAME, -- name in the input language

dgn_theory :: G_theory, -- local theory

dgn_nf :: Maybe Node, -- normal form, for Theorem-Hide-Shift

dgn_sigma :: Maybe GMorphism, -- inclusion of signature into nf signature

dgn_origin :: DGOrigin, -- origin in input language

dgn_cons :: Conservativity,

dgn_cons_status :: ThmLinkStatus

}

| DGRef { -- reference to node in a different DG

dgn_name :: NODE_NAME, -- new name of node (in current DG)

dgn_libname :: LIB_NAME, -- pointer to DG where ref'd node resides

dgn_node :: Node, -- pointer to ref'd node

dgn_theory :: G_theory, -- local proof goals

dgn_nf :: Maybe Node, -- normal form, for Theorem-Hide-Shift

dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature

} deriving (Show, Eq)

dgn_sign :: DGNodeLab -> G_sign

dgn_sign dn = case dgn_theory dn of

G_theory lid sig _ -> G_sign lid sig

isInternalNode :: DGNodeLab -> Bool

isInternalNode (DGNode n _ _ _ _ _ _) = isInternal n

isInternalNode _ = False

isRefNode :: DGNodeLab -> Bool

isRefNode (DGNode _ _ _ _ _ _ _) = False

isRefNode _ = True

-- gets the name of a development graph node as a string

getDGNodeName :: DGNodeLab -> String

getDGNodeName dgn = showName $ dgn_name dgn

emptyNodeName :: NODE_NAME

emptyNodeName = (mkSimpleId "","",0)

showInt :: Int -> String

showInt i = if i==0 then "" else show i

showName :: NODE_NAME -> String

showName (n,s,i) = show n ++ if ext=="" then "" else "_"++ext

where ext = s ++ showInt i

makeName :: SIMPLE_ID -> NODE_NAME

makeName n = (n,"",0)

getName :: NODE_NAME -> SIMPLE_ID

getName (n,_,_) = n

makeMaybeName :: Maybe SIMPLE_ID -> NODE_NAME

makeMaybeName Nothing = emptyNodeName

makeMaybeName (Just n) = makeName n

inc :: NODE_NAME -> NODE_NAME

inc (n,s,i) = (n,s,i+1)

isInternal :: NODE_NAME -> Bool

isInternal (_,s,i) = (i/=0) || s/=""

extName :: String -> NODE_NAME -> NODE_NAME

extName s (n,s1,i) = (n,s1++showInt i++s,0)

isDGRef :: DGNodeLab -> Bool

isDGRef (DGNode _ _ _ _ _ _ _) = False

isDGRef (DGRef _ _ _ _ _ _) = True

locallyEmpty :: DGNodeLab -> Bool

locallyEmpty dgn =

case dgn_theory dgn of

G_theory _lid _sigma sens ->

OMap.null $ OMap.filter

(\s -> not (Logic.Prover.isAxiom s) && not (isProvenSenStatus s) ) sens

-- | link inscriptions in development graphs

data DGLinkLab = DGLink {

dgl_morphism :: GMorphism, -- signature morphism of link

dgl_type :: DGLinkType, -- type: local, global, def, thm?

-- dgl_depends :: [Int],

dgl_origin :: DGOrigin } -- origin in input language

deriving (Show, Eq)

instance PrettyPrint DGLinkLab where

printText0 ga l = printText0 ga (dgl_morphism l)

<+> printText0 ga (dgl_type l)

<+> printText0 ga (dgl_origin l)

-- | coarser equality, ignoring the proof status

eqDGLinkLab :: DGLinkLab -> DGLinkLab -> Bool

eqDGLinkLab l1 l2 =

dgl_morphism l1 == dgl_morphism l2

&& eqDGLinkType (dgl_type l1) (dgl_type l2)

&& dgl_origin l1 == dgl_origin l2

eqLEdgeDGLinkLab :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool

eqLEdgeDGLinkLab (m1,n1,l1) (m2,n2,l2) =

m1==m2 && n1==n2 && eqDGLinkLab l1 l2

roughElem :: LEdge DGLinkLab -> [LEdge DGLinkLab] -> Bool

roughElem x = any (`eqLEdgeDGLinkLab` x)

data DGChange = InsertNode (LNode DGNodeLab)

| DeleteNode (LNode DGNodeLab)

| InsertEdge (LEdge DGLinkLab)

| DeleteEdge (LEdge DGLinkLab)

deriving Eq

instance Show DGChange where

show (InsertNode (n, _)) = "InsertNode "++show n -- ++show l

show (DeleteNode (n, _)) = "DeleteNode "++show n -- ++show l

show (InsertEdge (n,m, _)) = "InsertEdge "++show n++"->"++show m -- ++show l

show (DeleteEdge (n,m, _)) = "DeleteEdge "++show n++"->"++show m -- ++show l

-- | Link types of development graphs

-- | Sect. IV:4.2 of the CASL Reference Manual explains them in depth

data DGLinkType = LocalDef

| GlobalDef

| HidingDef

| FreeDef MaybeNode -- the "parameter" node

| CofreeDef MaybeNode -- the "parameter" node

| LocalThm ThmLinkStatus Conservativity ThmLinkStatus

-- ??? Some more proof information is needed here

-- (proof tree, ...)

| GlobalThm ThmLinkStatus Conservativity ThmLinkStatus

| HidingThm GMorphism ThmLinkStatus

| FreeThm GMorphism Bool

-- DGLink S1 S2 m2 (DGLinkType m1 p) n

-- corresponds to a span of morphisms

-- S1 <--m1-- S --m2--> S2

deriving (Eq,Show)

thmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus

thmLinkStatus (LocalThm s _ _) = Just s

thmLinkStatus (GlobalThm s _ _) = Just s

thmLinkStatus (HidingThm _ s) = Just s

thmLinkStatus _ = Nothing

-- | Coarser equality ignoring the proof status

eqDGLinkType :: DGLinkType -> DGLinkType -> Bool

LocalDef `eqDGLinkType` LocalDef = True

HidingDef `eqDGLinkType` HidingDef = True

FreeDef n1 `eqDGLinkType` FreeDef n2 = n1==n2

LocalThm _ _ _ `eqDGLinkType` LocalThm _ _ _ = True

GlobalThm _ _ _ `eqDGLinkType` GlobalThm _ _ _ = True

HidingThm m1 _ `eqDGLinkType` HidingThm m2 _ = m1 == m2

FreeThm m1 _ `eqDGLinkType` FreeThm m2 _ = m1 == m2

_ `eqDGLinkType` _ = False

instance PrettyPrint DGLinkType where

printText0 _ t = text $ case t of

LocalDef -> "LocalDef"

GlobalDef -> "GlobalDef"

HidingDef -> "HidingDef"

FreeDef _ -> "FreeDef"

CofreeDef _ -> "CofreeDef"

LocalThm _ _ _ -> "LocalThm"

GlobalThm _ _ _ -> "GlobalThm"

HidingThm _ _ -> "HidingThm"

FreeThm _ _ -> "FreeThm"

-- | Conservativity annotations. For compactness, only the greatest

-- | applicable value is used in a DG

data Conservativity = None | Cons | Mono | Def

deriving (Eq,Ord)

instance Show Conservativity where

show None = ""

show Cons = "Cons"

show Mono = "Mono"

show Def = "Def"

-- | Rules in the development graph calculus

-- | Sect. IV:4.4 of the CASL Reference Manual explains them in depth

data DGRule =

TheoremHideShift

| HideTheoremShift (LEdge DGLinkLab)

| Borrowing

| ConsShift

| DefShift

| MonoShift

| DefToMono

| MonoToCons

| FreeIsMono

| MonoIsFree

| GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion

| LocDecomp (LEdge DGLinkLab)

| LocInference (LEdge DGLinkLab)

| GlobSubsumption (LEdge DGLinkLab)

| Composition [LEdge DGLinkLab]

| LocalInference

| BasicInference AnyComorphism BasicProof -- coding and proof tree

| BasicConsInference Edge BasicConsProof

deriving (Show, Eq)

instance PrettyPrint DGRule where

printText0 ga r = case r of

TheoremHideShift -> text "Theorem-Hide-Shift"

HideTheoremShift l -> text "Hide-Theorem-Shift; resulting link:"

<+> printLEdgeInProof ga l

Borrowing -> text "Borrowing"

ConsShift -> text "Cons-Shift"

DefShift -> text "Def-Shift"

MonoShift -> text "Mono-Shift"

DefToMono -> text "DefToMono"

MonoToCons -> text "MonoToCons"

FreeIsMono -> text "FreeIsMono"

MonoIsFree -> text "MonoIsFree"

GlobDecomp l -> text "Global Decomposition; resulting link:"

<+> printLEdgeInProof ga l

LocDecomp l -> text "Local Decomposition; resulting link:"

<+> printLEdgeInProof ga l

LocInference l -> text "Local Inference; resulting link:"

<+> printLEdgeInProof ga l

GlobSubsumption l -> text "Global Subsumption; resulting link:"

<+> printLEdgeInProof ga l

Composition ls ->

text "Composition" <+> vcat (map (printLEdgeInProof ga) ls)

LocalInference -> text "Local Inference"

BasicInference c bp -> text "Basic Inference using:"

<+> text ("Comorphism: "++show c ++ "Proof tree: "++show bp)

BasicConsInference _ bp -> text "Basic Cons-Inference using:"

<+> text (show bp)

printLEdgeInProof :: GlobalAnnos -> LEdge DGLinkLab -> Doc

printLEdgeInProof ga (s,t,l) =

printText0 ga s <> text "-->" <> printText0 ga t <> text ":"

<+> printLabInProof ga l

printLabInProof :: GlobalAnnos -> DGLinkLab -> Doc

printLabInProof ga l =

hang(

printText0 ga (dgl_type l)

<+> text "with origin: "

<> printText0 ga (dgl_origin l)

<> text ", and morphism: " )

2 (printText0 ga (dgl_morphism l))

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 (Proof_status proof_tree)

| Guessed

| Conjectured

| Handwritten

instance Eq BasicProof where

Guessed == Guessed = True

Conjectured == Conjectured = True

Handwritten == Handwritten = True

BasicProof lid1 p1 == BasicProof lid2 p2 =

coerceBasicProof 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"

basicProofTc :: TyCon

basicProofTc = mkTyCon "Static.DevGraph.BasicProof"

instance Typeable BasicProof where

typeOf _ = mkTyConApp basicProofTc []

data BasicConsProof = BasicConsProof -- more detail to be added ...

deriving (Show, Eq)

data ThmLinkStatus = LeftOpen

| Proven DGRule [LEdge DGLinkLab] -- Proven DGRule Int

deriving (Show, Eq)

instance PrettyPrint ThmLinkStatus where

printText0 ga tls = case tls of

LeftOpen -> text "Open"

Proven r ls -> hang (text "Proven with rule" <+> printText0 ga r

$$ text "Proof based on links:")

2 (vcat (map (printLEdgeInProof ga) ls))

-- | Data type indicating the origin of nodes and edges in the input language

-- | This is not used in the DG calculus, only may be used in the future

-- | for reconstruction of input and management of change.

data DGOrigin = DGBasic | DGExtension | DGTranslation | DGUnion | DGHiding

| DGRevealing | DGRevealTranslation | DGFree | DGCofree

| DGLocal | DGClosed | DGClosedLenv | DGLogicQual

| DGLogicQualLenv | DGData

| DGFormalParams | DGImports | DGSpecInst SIMPLE_ID | DGFitSpec

| DGView SIMPLE_ID | DGFitView SIMPLE_ID | DGFitViewImp SIMPLE_ID

| DGFitViewA SIMPLE_ID | DGFitViewAImp SIMPLE_ID | DGProof

| DGintegratedSCC

deriving (Show, Eq)

type DGraph = Tree.Gr DGNodeLab DGLinkLab

{- type DGraph = DGraph { dgraph :: Tree.Gr DGNodeLab Int

, dgptr :: Int

, dglabels :: Map.Map Int (LEdge DGLinkLab) }

-}

-- | Node with signature in a DG

data NodeSig = NodeSig Node G_sign deriving (Show, Eq)

-- | NodeSig or possibly the empty sig in a logic

-- | (but since we want to avoid lots of vacuous nodes with empty sig,

-- | we do not assign a real node in the DG here)

data MaybeNode = JustNode NodeSig | EmptyNode AnyLogic deriving (Show, Eq)

instance PrettyPrint NodeSig where

printText0 ga (NodeSig n sig) =

text "node" <+> printText0 ga n <> colon <> printText0 ga sig

emptyG_sign :: AnyLogic -> G_sign

emptyG_sign (Logic lid) = G_sign lid (empty_signature lid)

getSig :: NodeSig -> G_sign

getSig (NodeSig _ sigma) = sigma

getNode :: NodeSig -> Node

getNode (NodeSig n _) = n

getMaybeSig :: MaybeNode -> G_sign

getMaybeSig (JustNode ns) = getSig ns

getMaybeSig (EmptyNode l) = emptyG_sign l

getLogic :: MaybeNode -> AnyLogic

getLogic (JustNode ns) = getNodeLogic ns

getLogic (EmptyNode l) = l

getNodeLogic :: NodeSig -> AnyLogic

getNodeLogic (NodeSig _ (G_sign lid _)) = Logic lid

-- | Create a node that represents a union of signatures

nodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin

-> Result (NodeSig, DGraph)

nodeSigUnion lgraph dg nodeSigs orig =

do sigUnion@(G_sign lid sigU) <- gsigManyUnion lgraph

$ map getMaybeSig nodeSigs

let nodeContents = DGNode {dgn_name = emptyNodeName,

dgn_theory = G_theory lid sigU noSens,

dgn_nf = Nothing,

dgn_sigma = Nothing,

dgn_origin = orig,

dgn_cons = None,

dgn_cons_status = LeftOpen}

node = getNewNode dg

dg' = insNode (node, nodeContents) dg

inslink dgres nsig = do

dgv <- dgres

case nsig of

EmptyNode _ -> dgres

JustNode (NodeSig n sig) -> do

incl <- ginclusion lgraph sig sigUnion

return $ insEdge (n, node, DGLink

{dgl_morphism = incl,

dgl_type = GlobalDef,

dgl_origin = orig }) dgv

dg'' <- foldl inslink (return dg') nodeSigs

return (NodeSig node sigUnion, dg'')

-- | Extend the development graph with given morphism originating

-- from given NodeSig

extendDGraph :: DGraph -- ^ the development graph to be extended

-> NodeSig -- ^ the NodeSig from which the morphism originates

-> GMorphism -- ^ the morphism to be inserted

-> DGOrigin

-> Result (NodeSig, DGraph)

-- ^ returns the target signature of the morphism and the resulting DGraph

extendDGraph dg (NodeSig n _) morph orig = case cod Grothendieck morph of

targetSig@(G_sign lid tar) -> let

nodeContents = DGNode {dgn_name = emptyNodeName,

dgn_theory = G_theory lid tar noSens,

dgn_nf = Nothing,

dgn_sigma = Nothing,

dgn_origin = orig,

dgn_cons = None,

dgn_cons_status = LeftOpen}

linkContents = DGLink {dgl_morphism = morph,

dgl_type = GlobalDef, -- TODO: other type

dgl_origin = orig}

node = getNewNode dg

dg' = insNode (node, nodeContents) dg

dg'' = insEdge (n, node, linkContents) dg'

in return (NodeSig node targetSig, dg'')

-- | Extend the development graph with given morphism pointing to

-- given NodeSig

extendDGraphRev :: DGraph -- ^ the development graph to be extended

-> NodeSig -- ^ the NodeSig to which the morphism points

-> GMorphism -- ^ the morphism to be inserted

-> DGOrigin

-> Result (NodeSig, DGraph)

-- ^ returns the source signature of the morphism and the resulting DGraph

extendDGraphRev dg (NodeSig n _) morph orig = case dom Grothendieck morph of

sourceSig@(G_sign lid src) -> let

nodeContents = DGNode {dgn_name = emptyNodeName,

dgn_theory = G_theory lid src OMap.empty,

dgn_nf = Nothing,

dgn_sigma = Nothing,

dgn_origin = orig,

dgn_cons = None,

dgn_cons_status = LeftOpen}

linkContents = DGLink {dgl_morphism = morph,

dgl_type = GlobalDef, -- TODO: other type

dgl_origin = orig}

node = getNewNode dg

dg' = insNode (node, nodeContents) dg

dg'' = insEdge (node, n, linkContents) dg'

in return (NodeSig node sourceSig, dg'')

-- import, formal parameters and united signature of formal params

type GenericitySig = (MaybeNode, [NodeSig], MaybeNode)

-- import, formal parameters, united signature of formal params, body

type ExtGenSig = (MaybeNode, [NodeSig], G_sign, NodeSig)

-- source, morphism, parameterized target

type ExtViewSig = (NodeSig,GMorphism,ExtGenSig)

-- * Types for architectural and unit specification analysis

-- (as defined for basic static semantics in Chap. III:5.1)

data UnitSig = Unit_sig NodeSig

| Par_unit_sig [NodeSig] NodeSig

deriving Show

data ImpUnitSigOrSig = Imp_unit_sig MaybeNode UnitSig

| Sig NodeSig

deriving Show

type StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig

emptyStUnitCtx :: StUnitCtx

emptyStUnitCtx = Map.empty

data ArchSig = ArchSig StUnitCtx UnitSig deriving Show

-- * Types for global and library environments

data GlobalEntry = SpecEntry ExtGenSig

| ViewEntry ExtViewSig

| ArchEntry ArchSig

| UnitEntry UnitSig

| RefEntry

deriving Show

type GlobalEnv = Map.Map SIMPLE_ID GlobalEntry

emptyHistory :: ([DGRule], [DGChange])

emptyHistory = ([], [])

type ProofHistory = [([DGRule], [DGChange])]

data GlobalContext = GlobalContext

{ globalAnnos :: GlobalAnnos

, globalEnv :: GlobalEnv

, devGraph :: DGraph

, sigMap :: Map.Map Int G_sign

, thMap :: Map.Map Int G_theory

, morMap :: Map.Map Int G_morphism

, proofHistory :: ProofHistory

}

{- the fields sigMap, thMap, and morMap are currently unused but will

be hopefully set by the static analysis in the future. Corresponding

entries in NodeSig, DGNodeLab, DGLinkLab, and DGLinkType could then be

replaced by indices. -}

emptyGlobalContext :: GlobalContext

emptyGlobalContext = GlobalContext

{ globalAnnos = emptyGlobalAnnos

, globalEnv = Map.empty

, devGraph = Graph.empty

, sigMap = Map.empty

, thMap = Map.empty

, morMap = Map.empty

, proofHistory = [emptyHistory]

}

type LibEnv = Map.Map LIB_NAME GlobalContext

-- | an empty environment

emptyLibEnv :: LibEnv

emptyLibEnv = Map.empty

-- | returns the global context that belongs to the given library name

lookupGlobalContext :: LIB_NAME -> LibEnv -> GlobalContext

lookupGlobalContext ln =

Map.findWithDefault (error "lookupGlobalContext") ln

-- | returns the development graph that belongs to the given library name

lookupDGraph :: LIB_NAME -> LibEnv -> DGraph

lookupDGraph ln = devGraph . lookupGlobalContext ln

instance PrettyPrint DGOrigin where

printText0 _ origin = text $ case origin of

DGBasic -> "basic specification"

DGExtension -> "extension"

DGTranslation -> "translation"

DGUnion -> "union"

DGHiding -> "hiding"

DGRevealing -> "revealing"

DGRevealTranslation -> "translation part of a revealing"

DGFree -> "free specification"

DGCofree -> "cofree specification"

DGLocal -> "local specification"

DGClosed -> "closed specification"

DGClosedLenv -> "closed specification (inclusion of local environment)"

DGFormalParams -> "formal parameters of a generic specification"

DGImports -> "imports of a generic specification"

DGSpecInst n -> "instantiation of " ++ showPretty n ""

DGFitSpec -> "fittig specification"

DGView n -> "view " ++ showPretty n ""

DGFitView n -> "fitting view " ++ showPretty n ""

DGFitViewImp n -> "fitting view (imports) " ++ showPretty n ""

DGFitViewA n -> "fitting view (actual parameters) "++ showPretty n ""

DGFitViewAImp n -> "fitting view (imports and actual parameters) "

++showPretty n ""

DGProof -> "constructed within a proof"

_ -> show origin

-- * Heterogenous sentences

type HetSenStatus a = SenStatus a (AnyComorphism,BasicProof)

isProvenSenStatus :: HetSenStatus a -> Bool

isProvenSenStatus = any isProvenSenStatusAux . thmStatus

where isProvenSenStatusAux (_,BasicProof _ pst) = isProvedStat pst

isProvenSenStatusAux _ = False

-- * Grothendieck theories

-- | Grothendieck theories

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 lid sign (ThSens sentence (AnyComorphism,BasicProof))

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 l1 l2 msg t1 = primCoerce l1 l2 msg t1

instance Eq G_theory where

G_theory l1 sig1 sens1 == G_theory l2 sig2 sens2 =

coerceSign l1 l2 "" sig1 == Just sig2

&& coerceThSens l1 l2 "" sens1 == Just sens2

instance Show G_theory where

show (G_theory _ sign sens) =

show sign ++ "\n" ++ show sens

instance PrettyPrint G_theory where

printText0 ga g = case simplifyTh g of

G_theory lid sign sens ->

printText0 ga sign $++$ vsep (map (print_named lid ga)

$ toNamedList sens)

-- | compute sublogic of a theory

sublogicOfTh :: G_theory -> G_sublogics

sublogicOfTh (G_theory lid sigma sens) =

let sub = Set.fold Logic.Logic.join

(min_sublogic_sign lid sigma)

(Set.fromList $ map snd $ OMap.toList $

OMap.map (min_sublogic_sentence lid . value)

sens)

in G_sublogics lid sub

-- | simplify a theory (throw away qualifications)

simplifyTh :: G_theory -> G_theory

simplifyTh (G_theory lid sigma sens) = G_theory lid sigma $

OMap.map (mapValue $ simplify_sen lid sigma) sens

-- | Translation of a G_theory along a GMorphism

translateG_theory :: GMorphism -> G_theory -> Result G_theory

translateG_theory (GMorphism cid _ morphism2) (G_theory lid sign sens) = do

let tlid = targetLogic cid

bTh <- coerceBasicTheory lid (sourceLogic cid)

"translateG_theory" (sign, toNamedList sens)

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

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

return $ G_theory tlid (cod tlid morphism2) $ toThSens sens'''

-- | Join the sentences of two G_theories

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

joinG_sentences (G_theory lid1 sig1 sens1) (G_theory lid2 sig2 sens2) = do

sens2' <- coerceThSens lid2 lid1 "joinG_sentences" sens2

sig2' <- coerceSign lid2 lid1 "joinG_sentences" sig2

return $ assert (sig1 == sig2') $ G_theory lid1 sig1 $ joinSens sens1 sens2'

-- | flattening the sentences form a list of G_theories

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

flatG_sentences th ths = foldM joinG_sentences th ths

-- | Get signature of a theory

signOf :: G_theory -> G_sign

signOf (G_theory lid sign _) = G_sign lid sign

------------------------------------------------------------------

-- Grothendieck diagrams and weakly amalgamable cocones

------------------------------------------------------------------

type GDiagram = Tree.Gr G_theory GMorphism

gWeaklyAmalgamableCocone :: GDiagram

-> Result (G_theory, Map.Map Graph.Node GMorphism)

gWeaklyAmalgamableCocone _ =

return (undefined, Map.empty) -- dummy implementation