1008N/ACopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
1008N/APortability : non-portable(Logic)
1008N/ACentral data structure for development graphs.
1008N/A Follows Sect. IV:4.2 of the CASL Reference Manual.
1008N/A T. Mossakowski, S. Autexier and D. Hutter:
1008N/A Extending Development Graphs With Hiding.
1008N/A H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
1008N/A Lecture Notes in Computer Science 2029, p. 269-283,
1008N/A T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
1008N/A CASL Proof calculus. In: CASL reference manual, part IV.
1821N/AIntegrate stuff from Saarbr�cken
1821N/AShould AS be stored in GloblaContext as well?
1008N/AgetNewNode g = case newNodes 1 g of
1821N/A-- * Types for structured specification analysis
1821N/A-- ??? Some info about the theorems already proved for a node
1821N/A-- or should it be kept separately?
1821N/A-- what about open theorems of a node???
0N/Atype NODE_NAME = (SIMPLE_ID, String, Int)
1821N/A dgn_sigma :: Maybe GMorphism,
1821N/A dgn_sigma :: Maybe GMorphism
0N/Adgn_sign :: DGNodeLab -> G_sign
1008N/Adgn_sign dn = case dgn_theory dn of
1821N/A G_theory lid sig _ -> G_sign lid sig
1821N/AisInternalNode :: DGNodeLab -> Bool
1821N/AisInternalNode (DGNode n _ _ _ _) = isInternal n
1821N/A-- gets the name of a development graph node as a string
1821N/AgetDGNodeName :: DGNodeLab -> String
1821N/AgetDGNodeName (DGNode n _ _ _ _) = showName n
1821N/AgetDGNodeName (DGRef n _ _ _ _) = showName n
1821N/AemptyNodeName = (mkSimpleId "","",0)
1821N/AshowInt i = if i==0 then "" else show i
1821N/AshowName :: NODE_NAME -> String
1821N/AshowName (n,s,i) = show n ++ if ext=="" then "" else "_"++ext
1821N/AmakeName :: SIMPLE_ID -> NODE_NAME
1821N/AgetName :: NODE_NAME -> SIMPLE_ID
1821N/AmakeMaybeName :: Maybe SIMPLE_ID -> NODE_NAME
1821N/AmakeMaybeName Nothing = emptyNodeName
1821N/AmakeMaybeName (Just n) = makeName n
1821N/Ainc :: NODE_NAME -> NODE_NAME
1821N/AisInternal :: NODE_NAME -> Bool
1821N/AisInternal (_,s,i) = (i/=0) || s/=""
1821N/AextName :: String -> NODE_NAME -> NODE_NAME
1821N/AextName s (n,s1,i) = (n,s1++showInt i++s,0)
1821N/AisDGRef :: DGNodeLab -> Bool
1821N/AisDGRef (DGNode _ _ _ _ _) = False
1821N/AisDGRef (DGRef _ _ _ _ _) = True
1821N/AlocallyEmpty :: DGNodeLab -> Bool
1821N/AlocallyEmpty (DGNode _ (G_theory lid sigma sens) _ _ _) =
1821N/AlocallyEmpty (DGRef _ _ _ _ _) = True
0N/A -- dgl_name :: String,
1821N/A -- dgl_src, dgl_tar :: DGNodeLab, -- already in graph structure
0N/A dgl_type :: DGLinkType,
0N/A dgl_origin :: DGOrigin }
0N/Ainstance PrettyPrint DGLinkLab where
1008N/A printText0 ga l = printText0 ga (dgl_morphism l)
1008N/A <+> printText0 ga (dgl_type l)
1008N/A <+> printText0 ga (dgl_origin l)
1008N/A | HideTheoremShift (LEdge DGLinkLab)
1821N/A | GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion
1008N/A | LocDecomp (LEdge DGLinkLab)
1008N/A | LocSubsumption (LEdge DGLinkLab)
1008N/A | GlobSubsumption (LEdge DGLinkLab)
1008N/A | Composition [LEdge DGLinkLab]
1008N/A | BasicInference BasicProof
1821N/A | BasicConsInference Edge BasicConsProof
0N/A forall lid sublogics
1008N/A basic_spec sentence symb_items symb_map_items
1008N/A sign morphism symbol raw_symbol proof_tree .
1008N/A basic_spec sentence symb_items symb_map_items
1008N/A sign morphism symbol raw_symbol proof_tree =>
0N/A BasicProof lid (Proof_status proof_tree)
1821N/A -- should be list of Proof_Status!
1821N/Ainstance Eq BasicProof where
1821N/A Conjectured == Conjectured = True
1821N/A Handwritten == Handwritten = True
1821N/A BasicProof lid1 p1 == BasicProof lid2 p2 =
1821N/A coerceBasicProof lid1 lid2 "Eq BasicProof" p1 == Just p2
1821N/Ainstance Show BasicProof where
1821N/A show (BasicProof _ p1) = show p1
1008N/A show Conjectured = "Conjectured"
1008N/A show Handwritten = "Handwritten"
1008N/Adata BasicConsProof = BasicConsProof -- more detail to be added ...
1008N/Adata ThmLinkStatus = LeftOpen
1008N/A | Proven DGRule [DGLinkLab]
1821N/Ainstance PrettyPrint ThmLinkStatus where
1821N/A printText0 ga tls = case tls of
1821N/A Proven _ ls -> vcat $ map (printText0 ga) ls
1947N/A | FreeDef MaybeNode -- the "parameter" node
1947N/A | CofreeDef MaybeNode -- the "parameter" node
1947N/A | LocalThm ThmLinkStatus Conservativity ThmLinkStatus
1947N/A -- ??? Some more proof information is needed here
1947N/A | GlobalThm ThmLinkStatus Conservativity ThmLinkStatus
1947N/A | HidingThm GMorphism ThmLinkStatus
1947N/A -- DGLink S1 S2 m2 (DGLinkType m1 p) n
1821N/A -- corresponds to a span of morphisms
1947N/Ainstance PrettyPrint DGLinkType where
1947N/A printText0 _ t = text $ case t of
1821N/A LocalThm _ _ _ -> "LocalThm"
1821N/A GlobalThm _ _ _ -> "GlobalThm"
1821N/A HidingThm _ _ -> "HidingThm"
1947N/Adata Conservativity = None | Cons | Mono | Def
1821N/Ainstance Show Conservativity where
1821N/Adata DGOrigin = DGBasic | DGExtension | DGTranslation | DGUnion | DGHiding
1821N/A | DGRevealing | DGRevealTranslation | DGFree | DGCofree
1821N/A | DGLocal | DGClosed | DGClosedLenv | DGLogicQual | DGLogicQualLenv
1821N/A | DGFormalParams | DGImports | DGSpecInst SIMPLE_ID | DGFitSpec
1821N/A | DGView SIMPLE_ID | DGFitView SIMPLE_ID | DGFitViewImp SIMPLE_ID
1821N/A | DGFitViewA SIMPLE_ID | DGFitViewAImp SIMPLE_ID | DGProof
1947N/Adata NodeSig = NodeSig Node G_sign deriving Eq
1008N/Adata MaybeNode = JustNode NodeSig | EmptyNode AnyLogic deriving (Show, Eq)
0N/Ainstance PrettyPrint NodeSig where
1008N/A printText0 ga (NodeSig n sig) =
1008N/A ptext "node" <+> printText0 ga n <> ptext ":" <> printText0 ga sig
0N/Ainstance Show NodeSig where
1008N/AemptyG_sign :: AnyLogic -> G_sign
1008N/AemptyG_sign (Logic lid) = G_sign lid (empty_signature lid)
0N/AgetSig :: NodeSig -> G_sign
0N/AgetSig (NodeSig _ sigma) = sigma
1008N/AgetMaybeSig :: MaybeNode -> G_sign
1008N/AgetMaybeSig (JustNode ns) = getSig ns
1008N/AgetMaybeSig (EmptyNode l) = emptyG_sign l
1934N/AgetLogic :: MaybeNode -> AnyLogic
1934N/AgetLogic (JustNode ns) = getNodeLogic ns
1934N/AgetNodeLogic :: NodeSig -> AnyLogic
1008N/AgetNodeLogic (NodeSig _ (G_sign lid _)) = Logic lid
1008N/A-- | Create a node that represents a union of signatures
1008N/AnodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin
1821N/A -> Result (NodeSig, DGraph)
1821N/AnodeSigUnion lgraph dg nodeSigs orig =
1821N/A do sigUnion@(G_sign lid sigU) <- gsigManyUnion lgraph
1821N/A let nodeContents = DGNode {dgn_name = emptyNodeName,
1821N/A dgn_theory = G_theory lid sigU noSens,
2020N/A dg' = insNode (node, nodeContents) dg
1821N/A JustNode (NodeSig n sig) -> do
1821N/A incl <- ginclusion lgraph sig sigUnion
1821N/A return $ insEdge (n, node, DGLink
1821N/A dg'' <- foldl inslink (return dg') nodeSigs
1821N/A return (NodeSig node sigUnion, dg'')
1821N/A-- | Extend the development graph with given morphism originating
1934N/AextendDGraph :: DGraph -- ^ the development graph to be extended
1821N/A -> NodeSig -- ^ the NodeSig from which the morphism originates
1934N/A -> GMorphism -- ^ the morphism to be inserted
1934N/A -> Result (NodeSig, DGraph)
1934N/A-- ^ returns the target signature of the morphism and the resulting DGraph
1934N/AextendDGraph dg (NodeSig n _) morph orig = case cod Grothendieck morph of
1934N/A targetSig@(G_sign lid tar) -> let
1821N/A nodeContents = DGNode {dgn_name = emptyNodeName,
1821N/A dgn_theory = G_theory lid tar noSens,
1821N/A linkContents = DGLink {dgl_morphism = morph,
1821N/A dgl_type = GlobalDef, -- TODO: other type
1008N/A dg' = insNode (node, nodeContents) dg
1934N/A dg'' = insEdge (n, node, linkContents) dg'
1934N/A in return (NodeSig node targetSig, dg'')
1821N/A-- | Extend the development graph with given morphism pointing to
1934N/AextendDGraphRev :: DGraph -- ^ the development graph to be extended
1934N/A -> NodeSig -- ^ the NodeSig to which the morphism points
1821N/A -> GMorphism -- ^ the morphism to be inserted
1934N/A -> Result (NodeSig, DGraph)
1934N/A-- ^ returns 1. the source signature of the morphism and 2. the resulting DGraph
1821N/AextendDGraphRev dg (NodeSig n _) morph orig = case dom Grothendieck morph of
1821N/A sourceSig@(G_sign lid src) -> let
2017N/A nodeContents = DGNode {dgn_name = emptyNodeName,
1821N/A linkContents = DGLink {dgl_morphism = morph,
1821N/A dgl_type = GlobalDef, -- TODO: other type
1821N/A dg' = insNode (node, nodeContents) dg
1821N/A dg'' = insEdge (node, n, linkContents) dg'
1821N/A in return (NodeSig node sourceSig, dg'')
1821N/A-- import, formal parameters andd united signature of formal params
1821N/Atype GenericitySig = (MaybeNode, [NodeSig], MaybeNode)
1821N/A-- import, formal parameters, united signature of formal params, body
1821N/Atype ExtGenSig = (MaybeNode, [NodeSig], G_sign, NodeSig)
1821N/A-- source, morphism, parameterized target
1821N/Atype ExtViewSig = (NodeSig,GMorphism,ExtGenSig)
1821N/A-- * Types for architectural and unit specification analysis
1821N/A-- (as defined for basic static semantics in Chap. III:5.1)
1821N/Adata UnitSig = Unit_sig NodeSig
1821N/A | Par_unit_sig [NodeSig] NodeSig
2017N/Adata ImpUnitSigOrSig = Imp_unit_sig MaybeNode UnitSig
2017N/Adata ArchSig = ArchSig StUnitCtx UnitSig
1934N/A-- * Types for global and library environments
1821N/Adata GlobalEntry = SpecEntry ExtGenSig
1821N/Atype GlobalContext = (GlobalAnnos,GlobalEnv,DGraph)
1821N/Ainstance PrettyPrint DGOrigin where
1821N/A printText0 _ origin = text $ case origin of
1821N/A DGBasic -> "basic specification"
1821N/A DGTranslation -> "translation"
1934N/A DGRevealTranslation -> "translation part of a revealing"
1934N/A DGFree -> "free specification"
1821N/A DGCofree -> "cofree specification"
1821N/A DGLocal -> "local specification"
1821N/A DGClosed -> "closed specification"
1821N/A DGClosedLenv -> "closed specification (inclusion of local environment)"
1821N/A DGFormalParams -> "formal parameters of a generic specification"
1821N/A DGImports -> "imports of a generic specification"
1821N/A DGSpecInst n -> ("instantiation of "++showPretty n "")
1821N/A DGFitSpec -> "fittig specification"
1821N/A DGView n -> ("view "++showPretty n "")
1821N/A DGFitView n -> ("fitting view "++showPretty n "")
1821N/A DGFitViewImp n -> ("fitting view (imports) "++showPretty n "")
1821N/A DGFitViewA n -> ("fitting view (actual parameters) "++showPretty n "")
1821N/A DGFitViewAImp n -> ("fitting view (imports and actual parameters) "
1821N/A DGProof -> "constructed within a proof"
1821N/Adata Decorated a = Decorated
1821N/A , thmStatus :: [ThmLinkStatus]
1821N/AemptyDecorated :: Decorated a
1821N/AemptyDecorated = Decorated { value = error "emptyDecorated"
1821N/Ainstance Eq a => Eq (Decorated a) where
1821N/A d1 == d2 = (value d1, isDef d1) ==
1934N/Ainstance Ord a => Ord (Decorated a) where
1934N/A d1 <= d2 = (value d1, isDef d1) <=
1821N/Ainstance Typeable s => Typeable (Decorated s) where
1821N/A typeOf s = mkTyConApp decoTc [typeOf ((undefined :: Decorated a -> a) s)]
1821N/AjoinSens :: Ord a => ThSens a -> ThSens a -> ThSens a
2017N/A mergeSens l1@(e1 : r1) l2@(e2 : r2) = case compare e1 e2 of
2017N/AmapValue :: (a -> b) -> Decorated a -> Decorated b
1934N/AmapValue f d = d { value = mapNamed f $ value d }
1934N/AtoNamedList :: ThSens a -> [Named a]
1821N/AtoNamedList s = let compO d1 d2 = compare (order d1) (order d2)
1821N/AtoThSens :: Ord a => [Named a] -> ThSens a
1821N/A ( \ v i -> emptyDecorated { value = v, order = i })
2017N/Adata G_theory = forall lid sublogics
1821N/A basic_spec sentence symb_items symb_map_items
1821N/A sign morphism symbol raw_symbol proof_tree .
2017N/A basic_spec sentence symb_items symb_map_items
2017N/A sign morphism symbol raw_symbol proof_tree =>
2017N/A G_theory lid sign (ThSens sentence)
1821N/A (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1821N/A sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
2017N/A Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1934N/A sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
1934N/A Monad m) => lid1 -> lid2 -> String
1934N/A -> ThSens sentence1 -> m (ThSens sentence2)
1821N/AcoerceThSens l1 l2 msg t1 = primCoerce l1 l2 msg t1
1821N/A G_theory l1 sig1 sens1 == G_theory l2 sig2 sens2 =
1821N/A coerceSign l1 l2 "" sig1 == Just sig2
1821N/A && coerceThSens l1 l2 "" sens1 == Just sens2
1821N/Ainstance PrettyPrint G_theory where
2017N/A printText0 ga g = case simplifyTh g of
2017N/A printText0 ga sign $++$ vsep (map (print_named lid ga)
1821N/Ainstance Show G_theory where
1821N/A-- | compute sublogic of a theory
1821N/AsublogicOfTh :: G_theory -> G_sublogics
1008N/AsublogicOfTh (G_theory lid sigma sens) =
1821N/A (min_sublogic_sign lid sigma)
2020N/A-- | simplify a theory (throw away qualifications)
2020N/AsimplifyTh :: G_theory -> G_theory
1821N/AsimplifyTh (G_theory lid sigma sens) = G_theory lid sigma $
1821N/A-- | Translation of a G_theory along a GMorphism
1821N/AtranslateG_theory :: GMorphism -> G_theory -> Result G_theory
2020N/AtranslateG_theory (GMorphism cid _ morphism2)
2020N/A (G_theory lid sign sens) = do
2020N/A --(sigma2,_) <- map_sign cid sign1
2020N/A bTh <- coerceBasicTheory lid (sourceLogic cid)
1821N/A "translateG_theory" (sign, toNamedList sens)
2020N/A (_, sens'') <- map_theory cid bTh
2020N/A sens''' <- mapM (mapNamedM $ map_sen tlid morphism2) sens''
1008N/A return $ G_theory tlid (cod tlid morphism2) $ toThSens sens'''
1821N/A-- | Join the sentences of two G_theories
1821N/AjoinG_sentences :: Monad m => G_theory -> G_theory -> m G_theory
1821N/AjoinG_sentences (G_theory lid1 sig1 sens1) (G_theory lid2 _ sens2) = do
1821N/A sens2' <- coerceThSens lid2 lid1 "joinG_sentences" sens2
1821N/A -- assert (sig1 == sig2') ?
1821N/A return $ G_theory lid1 sig1 $ joinSens sens1 sens2'
1821N/A-- | flattening the sentences form a list of G_theories
1821N/AflatG_sentences :: Monad m => G_theory -> [G_theory] -> m G_theory
1821N/AflatG_sentences th ths = foldM joinG_sentences th ths
1821N/A-- | Get signature of a theory
1821N/AsignOf :: G_theory -> G_sign
1821N/AsignOf (G_theory lid sign _) = G_sign lid sign
1821N/A------------------------------------------------------------------
1821N/A-- Grothendieck diagrams and weakly amalgamable cocones
1821N/A------------------------------------------------------------------
1008N/AgWeaklyAmalgamableCocone :: GDiagram
1008N/AgWeaklyAmalgamableCocone _ =