DevGraph.hs revision 2c839e02e7c8732f1e4af2b2d87a2055de4a98c6
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : till@tzi.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettPortability : non-portable(Logic)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCentral data structure for development graphs.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Follows Sect. IV:4.2 of the CASL Reference Manual.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach T. Mossakowski, S. Autexier and D. Hutter:
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Extending Development Graphs With Hiding.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett Lecture Notes in Computer Science 2029, p. 269-283,
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett Springer-Verlag 2001.
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett CASL Proof calculus. In: CASL reference manual, part IV.
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy GimblettIntegrate stuff from Saarbr�cken
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachShould AS be stored in GloblaContext as well?
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachsimplifyTh should be removed from instance Pretty G_theory
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyimport qualified Common.Lib.Graph as Tree
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyimport qualified Common.Lib.Map as Map
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyimport qualified Common.OrderedMap as OMap
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillygetNewNode :: Tree.Gr a b -> Node
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillygetNewNode g = case newNodes 1 g of
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder-- * Types for structured specification analysis
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- ??? Some info about the theorems already proved for a node
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett-- should be added
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett-- or should it be kept separately?
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett-- what about open theorems of a node???
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | name of a node in a DG; auxiliary nodes may have extension string
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- | and non-zero number (for these, names are usually hidden)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimbletttype NODE_NAME = (SIMPLE_ID, String, Int)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | node inscriptions in development graphs
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettdata DGNodeLab =
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett dgn_name :: NODE_NAME, -- name in the input language
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett dgn_theory :: G_theory, -- local theory
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett dgn_nf :: Maybe Node, -- normal form, for Theorem-Hide-Shift
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett dgn_sigma :: Maybe GMorphism, -- inclusion of signature into nf signature
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett dgn_origin :: DGOrigin, -- origin in input language
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett dgn_cons :: Conservativity,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett dgn_cons_status :: ThmLinkStatus
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett | DGRef { -- reference to node in a different DG
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett dgn_name :: NODE_NAME, -- new name of node (in current DG)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett dgn_libname :: LIB_NAME, -- pointer to DG where ref'd node resides
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett dgn_node :: Node, -- pointer to ref'd node
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett dgn_theory :: G_theory, -- local proof goals
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett dgn_nf :: Maybe Node, -- normal form, for Theorem-Hide-Shift
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett } deriving (Show, Eq)
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblettdgn_sign :: DGNodeLab -> G_sign
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettdgn_sign dn = case dgn_theory dn of
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett G_theory lid sig _ -> G_sign lid sig
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettisInternalNode :: DGNodeLab -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisInternalNode (DGNode n _ _ _ _ _ _) = isInternal n
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaederisInternalNode _ = False
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettisRefNode :: DGNodeLab -> Bool
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettisRefNode (DGNode _ _ _ _ _ _ _) = False
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettisRefNode _ = True
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- gets the name of a development graph node as a string
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettgetDGNodeName :: DGNodeLab -> String
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettgetDGNodeName dgn = showName $ dgn_name dgn
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettemptyNodeName :: NODE_NAME
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettemptyNodeName = (mkSimpleId "","",0)
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillyshowInt :: Int -> String
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillyshowInt i = if i==0 then "" else show i
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillyshowName :: NODE_NAME -> String
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'ReillyshowName (n,s,i) = show n ++ if ext=="" then "" else "_"++ext
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly where ext = s ++ showInt i
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettmakeName :: SIMPLE_ID -> NODE_NAME
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettmakeName n = (n,"",0)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettgetName :: NODE_NAME -> SIMPLE_ID
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettgetName (n,_,_) = n
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettmakeMaybeName :: Maybe SIMPLE_ID -> NODE_NAME
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettmakeMaybeName Nothing = emptyNodeName
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettmakeMaybeName (Just n) = makeName n
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinc :: NODE_NAME -> NODE_NAME
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettinc (n,s,i) = (n,s,i+1)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisInternal :: NODE_NAME -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisInternal (_,s,i) = (i/=0) || s/=""
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettextName :: String -> NODE_NAME -> NODE_NAME
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettextName s (n,s1,i) = (n,s1++showInt i++s,0)
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettisDGRef :: DGNodeLab -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisDGRef (DGNode _ _ _ _ _ _ _) = False
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettisDGRef (DGRef _ _ _ _ _ _) = True
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettlocallyEmpty :: DGNodeLab -> Bool
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettlocallyEmpty dgn =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett case dgn_theory dgn of
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett G_theory _lid _sigma sens ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (\s -> not (Logic.Prover.isAxiom s) && not (isProvenSenStatus s) ) sens
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- | link inscriptions in development graphs
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettdata DGLinkLab = DGLink {
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett dgl_morphism :: GMorphism, -- signature morphism of link
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett dgl_type :: DGLinkType, -- type: local, global, def, thm?
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -- dgl_depends :: [Int],
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgl_origin :: DGOrigin } -- origin in input language
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly deriving (Show, Eq)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Pretty DGLinkLab where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett pretty l = fsep [ pretty (dgl_morphism l)
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , pretty (dgl_type l)
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly , pretty (dgl_origin l)]
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly-- | coarser equality, ignoring the proof status
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimbletteqDGLinkLab :: DGLinkLab -> DGLinkLab -> Bool
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaedereqDGLinkLab l1 l2 =
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder dgl_morphism l1 == dgl_morphism l2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett && eqDGLinkType (dgl_type l1) (dgl_type l2)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett && dgl_origin l1 == dgl_origin l2
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimbletteqLEdgeDGLinkLab :: LEdge DGLinkLab -> LEdge DGLinkLab -> Bool
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimbletteqLEdgeDGLinkLab (m1,n1,l1) (m2,n2,l2) =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett m1==m2 && n1==n2 && eqDGLinkLab l1 l2
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettroughElem :: LEdge DGLinkLab -> [LEdge DGLinkLab] -> Bool
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyroughElem x = any (`eqLEdgeDGLinkLab` x)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettdata DGChange = InsertNode (LNode DGNodeLab)
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett | DeleteNode (LNode DGNodeLab)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly | InsertEdge (LEdge DGLinkLab)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly | DeleteEdge (LEdge DGLinkLab)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance Show DGChange where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly show (InsertNode (n, _)) = "InsertNode "++show n -- ++show l
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly show (DeleteNode (n, _)) = "DeleteNode "++show n -- ++show l
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly show (InsertEdge (n,m, _)) = "InsertEdge "++show n++"->"++show m -- ++show l
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly show (DeleteEdge (n,m, _)) = "DeleteEdge "++show n++"->"++show m -- ++show l
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Link types of development graphs
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | Sect. IV:4.2 of the CASL Reference Manual explains them in depth
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillydata DGLinkType = LocalDef
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly | FreeDef MaybeNode -- the "parameter" node
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly | CofreeDef MaybeNode -- the "parameter" node
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly | LocalThm ThmLinkStatus Conservativity ThmLinkStatus
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- ??? Some more proof information is needed here
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- (proof tree, ...)
c60c643bbac58809100f35f187493b6f170314f0Liam O'Reilly | GlobalThm ThmLinkStatus Conservativity ThmLinkStatus
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly | HidingThm GMorphism ThmLinkStatus
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | FreeThm GMorphism Bool
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- DGLink S1 S2 m2 (DGLinkType m1 p) n
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- corresponds to a span of morphisms
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- S1 <--m1-- S --m2--> S2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly deriving (Eq,Show)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillythmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillythmLinkStatus (LocalThm s _ _) = Just s
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillythmLinkStatus (GlobalThm s _ _) = Just s
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettthmLinkStatus (HidingThm _ s) = Just s
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettthmLinkStatus _ = Nothing
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | Coarser equality ignoring the proof status
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyeqDGLinkType :: DGLinkType -> DGLinkType -> Bool
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyLocalDef `eqDGLinkType` LocalDef = True
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyHidingDef `eqDGLinkType` HidingDef = True
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyFreeDef n1 `eqDGLinkType` FreeDef n2 = n1==n2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyLocalThm _ _ _ `eqDGLinkType` LocalThm _ _ _ = True
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyGlobalThm _ _ _ `eqDGLinkType` GlobalThm _ _ _ = True
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyHidingThm m1 _ `eqDGLinkType` HidingThm m2 _ = m1 == m2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyFreeThm m1 _ `eqDGLinkType` FreeThm m2 _ = m1 == m2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly_ `eqDGLinkType` _ = False
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance Pretty DGLinkType where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett pretty t = text $ case t of
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly LocalDef -> "LocalDef"
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett GlobalDef -> "GlobalDef"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly HidingDef -> "HidingDef"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly FreeDef _ -> "FreeDef"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly CofreeDef _ -> "CofreeDef"
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett LocalThm _ _ _ -> "LocalThm"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly GlobalThm _ _ _ -> "GlobalThm"
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett HidingThm _ _ -> "HidingThm"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett FreeThm _ _ -> "FreeThm"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | Conservativity annotations. For compactness, only the greatest
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | applicable value is used in a DG
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettdata Conservativity = None | Cons | Mono | Def
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly deriving (Eq,Ord)
5858e6262048894b0e933b547852f04aed009b58Andy Gimblettinstance Show Conservativity where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly show None = ""
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett show Cons = "Cons"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly show Mono = "Mono"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett show Def = "Def"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Rules in the development graph calculus
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly-- | Sect. IV:4.4 of the CASL Reference Manual explains them in depth
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett TheoremHideShift
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | HideTheoremShift (LEdge DGLinkLab)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly | GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | LocDecomp (LEdge DGLinkLab)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett | LocInference (LEdge DGLinkLab)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly | GlobSubsumption (LEdge DGLinkLab)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | Composition [LEdge DGLinkLab]
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly | LocalInference
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | BasicInference AnyComorphism BasicProof -- coding and proof tree. obsolete ?!?
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett | BasicConsInference Edge BasicConsProof
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly deriving (Show, Eq)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Pretty DGRule where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly pretty r = case r of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett TheoremHideShift -> text "Theorem-Hide-Shift"
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly HideTheoremShift l -> text "Hide-Theorem-Shift; resulting link:"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly <+> printLEdgeInProof l
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Borrowing -> text "Borrowing"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ConsShift -> text "Cons-Shift"
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly DefShift -> text "Def-Shift"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly MonoShift -> text "Mono-Shift"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett DefToMono -> text "DefToMono"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly MonoToCons -> text "MonoToCons"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly FreeIsMono -> text "FreeIsMono"
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly MonoIsFree -> text "MonoIsFree"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly GlobDecomp l -> text "Global Decomposition; resulting link:"
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly <+> printLEdgeInProof l
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly LocDecomp l -> text "Local Decomposition; resulting link:"
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett <+> printLEdgeInProof l
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly LocInference l -> text "Local Inference; resulting link:"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly <+> printLEdgeInProof l
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly GlobSubsumption l -> text "Global Subsumption; resulting link:"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <+> printLEdgeInProof l
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Composition ls ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly text "Composition" <+> vcat (map printLEdgeInProof ls)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett LocalInference -> text "Local Inference"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly BasicInference c bp -> text "Basic Inference using:"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly <+> text ("Comorphism: "++show c ++ "Proof tree: "++show bp)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly BasicConsInference _ bp -> text "Basic Cons-Inference using:"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <+> text (show bp)
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyprintLEdgeInProof :: LEdge DGLinkLab -> Doc
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettprintLEdgeInProof (s,t,l) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly pretty s <> text "-->" <> pretty t <> text ":"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly <+> printLabInProof l
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyprintLabInProof :: DGLinkLab -> Doc
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyprintLabInProof l =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly fsep [ pretty (dgl_type l)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett , text "with origin:"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly , pretty (dgl_origin l) <> comma
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly , text "and morphism:"
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly , pretty (dgl_morphism l)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillydata BasicProof =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly forall lid sublogics
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett basic_spec sentence symb_items symb_map_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign morphism symbol raw_symbol proof_tree .
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Logic lid sublogics
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly basic_spec sentence symb_items symb_map_items
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign morphism symbol raw_symbol proof_tree =>
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly BasicProof lid (Proof_status proof_tree)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly | Conjectured
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | Handwritten
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Eq BasicProof where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Guessed == Guessed = True
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Conjectured == Conjectured = True
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Handwritten == Handwritten = True
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly BasicProof lid1 p1 == BasicProof lid2 p2 =
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett coerceBasicProof lid1 lid2 "Eq BasicProof" p1 == Just p2
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett _ == _ = False
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Ord BasicProof where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Guessed <= _ = True
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Conjectured <= x = case x of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Guessed -> False
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Handwritten <= x = case x of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Guessed -> False
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Conjectured -> False
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly BasicProof lid1 pst1 <= x =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly BasicProof lid2 pst2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly | isProvedStat pst1 && not (isProvedStat pst2) -> False
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly | not (isProvedStat pst1) && isProvedStat pst2 -> True
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | otherwise -> case primCoerce lid1 lid2 "" pst1 of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Nothing -> False
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Just pst1' -> pst1' <= pst2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Show BasicProof where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly show (BasicProof _ p1) = show p1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly show Guessed = "Guessed"
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett show Conjectured = "Conjectured"
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly show Handwritten = "Handwritten"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillybasicProofTc :: TyCon
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillybasicProofTc = mkTyCon "Static.DevGraph.BasicProof"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance Typeable BasicProof where
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly typeOf _ = mkTyConApp basicProofTc []
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettdata BasicConsProof = BasicConsProof -- more detail to be added ...
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett deriving (Show, Eq)
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reillydata ThmLinkStatus = LeftOpen
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | Proven DGRule [LEdge DGLinkLab] -- Proven DGRule Int
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly deriving (Show, Eq)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Pretty ThmLinkStatus where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly pretty tls = case tls of
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett LeftOpen -> text "Open"
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly Proven r ls -> fsep [ text "Proven with rule"
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly , text "Proof based on links:"
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett ] $+$ vcat(map printLEdgeInProof ls)
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett-- | Data type indicating the origin of nodes and edges in the input language
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett-- | This is not used in the DG calculus, only may be used in the future
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett-- | for reconstruction of input and management of change.
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblettdata DGOrigin = DGBasic | DGExtension | DGTranslation | DGUnion | DGHiding
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett | DGRevealing | DGRevealTranslation | DGFree | DGCofree
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett | DGLocal | DGClosed | DGClosedLenv | DGLogicQual
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett | DGLogicQualLenv | DGData
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett | DGFormalParams | DGImports | DGSpecInst SIMPLE_ID | DGFitSpec
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | DGView SIMPLE_ID | DGFitView SIMPLE_ID | DGFitViewImp SIMPLE_ID
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | DGFitViewA SIMPLE_ID | DGFitViewAImp SIMPLE_ID | DGProof
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly | DGintegratedSCC
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly deriving (Show, Eq)
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimbletttype DGraph = Tree.Gr DGNodeLab DGLinkLab
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett{- type DGraph = DGraph { dgraph :: Tree.Gr DGNodeLab Int
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly , dgptr :: Int
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly , dglabels :: Map.Map Int (LEdge DGLinkLab) }
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett-- | Node with signature in a DG
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reillydata NodeSig = NodeSig Node G_sign deriving (Show, Eq)
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly-- | NodeSig or possibly the empty sig in a logic
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett-- | (but since we want to avoid lots of vacuous nodes with empty sig,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | we do not assign a real node in the DG here)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettdata MaybeNode = JustNode NodeSig | EmptyNode AnyLogic deriving (Show, Eq)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Pretty NodeSig where
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett pretty (NodeSig n sig) =
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett text "node" <+> pretty n <> colon <> pretty sig
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillyemptyG_sign :: AnyLogic -> G_sign
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillyemptyG_sign (Logic lid) = G_sign lid (empty_signature lid)
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillygetSig :: NodeSig -> G_sign
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillygetSig (NodeSig _ sigma) = sigma
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillygetNode :: NodeSig -> Node
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillygetNode (NodeSig n _) = n
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillygetMaybeSig :: MaybeNode -> G_sign
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillygetMaybeSig (JustNode ns) = getSig ns
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'ReillygetMaybeSig (EmptyNode l) = emptyG_sign l
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettgetLogic :: MaybeNode -> AnyLogic
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettgetLogic (JustNode ns) = getNodeLogic ns
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettgetLogic (EmptyNode l) = l
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillygetNodeLogic :: NodeSig -> AnyLogic
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillygetNodeLogic (NodeSig _ (G_sign lid _)) = Logic lid
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | Create a node that represents a union of signatures
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillynodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -> Result (NodeSig, DGraph)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillynodeSigUnion lgraph dg nodeSigs orig =
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly do sigUnion@(G_sign lid sigU) <- gsigManyUnion lgraph
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $ map getMaybeSig nodeSigs
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly let nodeContents = DGNode {dgn_name = emptyNodeName,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgn_theory = G_theory lid sigU noSens,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgn_nf = Nothing,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgn_sigma = Nothing,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgn_origin = orig,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgn_cons = None,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgn_cons_status = LeftOpen}
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly node = getNewNode dg
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dg' = insNode (node, nodeContents) dg
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly inslink dgres nsig = do
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly EmptyNode _ -> dgres
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett JustNode (NodeSig n sig) -> do
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly incl <- ginclusion lgraph sig sigUnion
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly return $ insEdge (n, node, DGLink
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly {dgl_morphism = incl,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgl_type = GlobalDef,
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly dgl_origin = orig }) dgv
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett dg'' <- foldl inslink (return dg') nodeSigs
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett return (NodeSig node sigUnion, dg'')
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | Extend the development graph with given morphism originating
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- from given NodeSig
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyextendDGraph :: DGraph -- ^ the development graph to be extended
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -> NodeSig -- ^ the NodeSig from which the morphism originates
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -> GMorphism -- ^ the morphism to be inserted
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett -> Result (NodeSig, DGraph)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- ^ returns the target signature of the morphism and the resulting DGraph
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyextendDGraph dg (NodeSig n _) morph orig = case cod Grothendieck morph of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly targetSig@(G_sign lid tar) -> let
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly nodeContents = DGNode {dgn_name = emptyNodeName,
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett dgn_theory = G_theory lid tar noSens,
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett dgn_nf = Nothing,
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett dgn_sigma = Nothing,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett dgn_origin = orig,
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett dgn_cons = None,
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly dgn_cons_status = LeftOpen}
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly linkContents = DGLink {dgl_morphism = morph,
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly dgl_type = GlobalDef, -- TODO: other type
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly dgl_origin = orig}
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly node = getNewNode dg
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly dg' = insNode (node, nodeContents) dg
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly dg'' = insEdge (n, node, linkContents) dg'
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly in return (NodeSig node targetSig, dg'')
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- | Extend the development graph with given morphism pointing to
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- given NodeSig
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillyextendDGraphRev :: DGraph -- ^ the development graph to be extended
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -> NodeSig -- ^ the NodeSig to which the morphism points
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -> GMorphism -- ^ the morphism to be inserted
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -> Result (NodeSig, DGraph)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- ^ returns the source signature of the morphism and the resulting DGraph
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillyextendDGraphRev dg (NodeSig n _) morph orig = case dom Grothendieck morph of
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly sourceSig@(G_sign lid src) -> let
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly nodeContents = DGNode {dgn_name = emptyNodeName,
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly dgn_theory = G_theory lid src OMap.empty,
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly dgn_nf = Nothing,
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly dgn_sigma = Nothing,
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly dgn_origin = orig,
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly dgn_cons = None,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly dgn_cons_status = LeftOpen}
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly linkContents = DGLink {dgl_morphism = morph,
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly dgl_type = GlobalDef, -- TODO: other type
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly dgl_origin = orig}
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly node = getNewNode dg
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly dg' = insNode (node, nodeContents) dg
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly dg'' = insEdge (node, n, linkContents) dg'
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly in return (NodeSig node sourceSig, dg'')
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- import, formal parameters and united signature of formal params
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillytype GenericitySig = (MaybeNode, [NodeSig], MaybeNode)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- import, formal parameters, united signature of formal params, body
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillytype ExtGenSig = (MaybeNode, [NodeSig], G_sign, NodeSig)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- source, morphism, parameterized target
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillytype ExtViewSig = (NodeSig,GMorphism,ExtGenSig)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- * Types for architectural and unit specification analysis
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly-- (as defined for basic static semantics in Chap. III:5.1)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillydata UnitSig = Unit_sig NodeSig
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly | Par_unit_sig [NodeSig] NodeSig
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly deriving Show
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reillydata ImpUnitSigOrSig = Imp_unit_sig MaybeNode UnitSig
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly | Sig NodeSig
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett deriving Show
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimbletttype StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettemptyStUnitCtx :: StUnitCtx
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'ReillyemptyStUnitCtx = Map.empty
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reillydata ArchSig = ArchSig StUnitCtx UnitSig deriving Show
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly-- * Types for global and library environments
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reillydata GlobalEntry = SpecEntry ExtGenSig
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly | ViewEntry ExtViewSig
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly | ArchEntry ArchSig
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly | UnitEntry UnitSig
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly deriving Show
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillytype GlobalEnv = Map.Map SIMPLE_ID GlobalEntry
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillyemptyHistory :: ([DGRule], [DGChange])
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'ReillyemptyHistory = ([], [])
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillytype ProofHistory = [([DGRule], [DGChange])]
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillydata GlobalContext = GlobalContext
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly { globalAnnos :: GlobalAnnos
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly , globalEnv :: GlobalEnv
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly , devGraph :: DGraph
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly , proofHistory :: ProofHistory
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly } deriving Show
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'ReillyemptyGlobalContext :: GlobalContext
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'ReillyemptyGlobalContext = GlobalContext
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett { globalAnnos = emptyGlobalAnnos
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett , proofHistory = [emptyHistory]
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reillytype LibEnv = Map.Map LIB_NAME GlobalContext
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly-- | an empty environment
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettemptyLibEnv :: LibEnv
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly-- | returns the global context that belongs to the given library name
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'ReillylookupGlobalContext :: LIB_NAME -> LibEnv -> GlobalContext
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'ReillylookupGlobalContext ln =
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Map.findWithDefault (error "lookupGlobalContext") ln
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett-- | returns the development graph that belongs to the given library name
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettlookupDGraph :: LIB_NAME -> LibEnv -> DGraph
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'ReillylookupDGraph ln = devGraph . lookupGlobalContext ln
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reillyinstance Pretty DGOrigin where
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly pretty origin = text $ case origin of
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett DGBasic -> "basic specification"
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett DGExtension -> "extension"
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett DGTranslation -> "translation"
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett DGUnion -> "union"
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett DGHiding -> "hiding"
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly DGRevealing -> "revealing"
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly DGRevealTranslation -> "translation part of a revealing"
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly DGFree -> "free specification"
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly DGCofree -> "cofree specification"
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly DGLocal -> "local specification"
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly DGClosed -> "closed specification"
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett DGClosedLenv -> "closed specification (inclusion of local environment)"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett DGFormalParams -> "formal parameters of a generic specification"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett DGImports -> "imports of a generic specification"
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly DGSpecInst n -> "instantiation of " ++ tokStr n
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly DGFitSpec -> "fittig specification"
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly DGView n -> "view " ++ tokStr n
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly DGFitView n -> "fitting view " ++ tokStr n
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett DGFitViewImp n -> "fitting view (imports) " ++ tokStr n
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly DGFitViewA n -> "fitting view (actual parameters) "++ tokStr n
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly DGFitViewAImp n -> "fitting view (imports and actual parameters) "
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly DGProof -> "constructed within a proof"
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett _ -> show origin
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett-- * Heterogenous sentences
a731366827a80af216ce6bfd4aa6388260577791Andy Gimbletttype HetSenStatus a = SenStatus a (AnyComorphism,BasicProof)
a731366827a80af216ce6bfd4aa6388260577791Andy GimblettisProvenSenStatus :: HetSenStatus a -> Bool
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'ReillyisProvenSenStatus = any isProvenSenStatusAux . thmStatus
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly where isProvenSenStatusAux (_,BasicProof _ pst) = isProvedStat pst
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly isProvenSenStatusAux _ = False
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly-- * Grothendieck theories
adce8375991a372444ab995895442dca6faf9677Andy Gimblett-- | Grothendieck theories
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblettdata G_theory = forall lid sublogics
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett basic_spec sentence symb_items symb_map_items
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett sign morphism symbol raw_symbol proof_tree .
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Logic lid sublogics
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly basic_spec sentence symb_items symb_map_items
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sign morphism symbol raw_symbol proof_tree =>
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly G_theory lid sign (ThSens sentence (AnyComorphism, BasicProof))
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'ReillycoerceThSens ::
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Typeable b) => lid1 -> lid2 -> String
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly -> ThSens sentence1 b -> m (ThSens sentence2 b)
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillycoerceThSens l1 l2 msg t1 = primCoerce l1 l2 msg t1
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reillyinstance Eq G_theory where
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett G_theory l1 sig1 sens1 == G_theory l2 sig2 sens2 =
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett coerceSign l1 l2 "" sig1 == Just sig2
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett && coerceThSens l1 l2 "" sens1 == Just sens2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance Show G_theory where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly show (G_theory _ sign sens) =
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly show sign ++ "\n" ++ show sens
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance Pretty G_theory where
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly pretty g = case simplifyTh g of
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly G_theory lid sign sens ->
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly pretty sign $++$ vsep (map (print_named lid)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $ toNamedList sens)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | compute sublogic of a theory
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'ReillysublogicOfTh :: G_theory -> G_sublogics
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'ReillysublogicOfTh (G_theory lid sigma sens) =
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (min_sublogic_sign lid sigma)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly OMap.map (min_sublogic_sentence lid . value)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly in G_sublogics lid sub
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | simplify a theory (throw away qualifications)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillysimplifyTh :: G_theory -> G_theory
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillysimplifyTh (G_theory lid sigma sens) = G_theory lid sigma $
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly OMap.map (mapValue $ simplify_sen lid sigma) sens
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | apply a comorphism to a theory
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillymapG_theory :: AnyComorphism -> G_theory -> Result G_theory
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillymapG_theory (Comorphism cid) (G_theory lid sign sens) = do
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly bTh <- coerceBasicTheory lid (sourceLogic cid)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly "mapG_theory" (sign, toNamedList sens)
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly (sign', sens') <- wrapMapTheory cid bTh
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly return $ G_theory (targetLogic cid) sign' $ toThSens sens'
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | Translation of a G_theory along a GMorphism
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimbletttranslateG_theory :: GMorphism -> G_theory -> Result G_theory
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimbletttranslateG_theory (GMorphism cid _ morphism2) (G_theory lid sign sens) = do
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett let tlid = targetLogic cid
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett bTh <- coerceBasicTheory lid (sourceLogic cid)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett "translateG_theory" (sign, toNamedList sens)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (_, sens'') <- map_theory cid bTh
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett sens''' <- mapM (mapNamedM $ map_sen tlid morphism2) sens''
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett return $ G_theory tlid (cod tlid morphism2) $ toThSens sens'''
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett-- | Join the sentences of two G_theories
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettjoinG_sentences :: Monad m => G_theory -> G_theory -> m G_theory
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettjoinG_sentences (G_theory lid1 sig1 sens1) (G_theory lid2 sig2 sens2) = do
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett sens2' <- coerceThSens lid2 lid1 "joinG_sentences" sens2
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett sig2' <- coerceSign lid2 lid1 "joinG_sentences" sig2
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett return $ assert (sig1 == sig2') $ G_theory lid1 sig1 $ joinSens sens1 sens2'
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | flattening the sentences form a list of G_theories
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettflatG_sentences :: Monad m => G_theory -> [G_theory] -> m G_theory
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettflatG_sentences th ths = foldM joinG_sentences th ths
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett-- | Get signature of a theory
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettsignOf :: G_theory -> G_sign
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettsignOf (G_theory lid sign _) = G_sign lid sign
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett------------------------------------------------------------------
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett-- Grothendieck diagrams and weakly amalgamable cocones
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett------------------------------------------------------------------
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimbletttype GDiagram = Tree.Gr G_theory GMorphism
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettgWeaklyAmalgamableCocone :: GDiagram
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -> Result (G_theory, Map.Map Graph.Node GMorphism)
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettgWeaklyAmalgamableCocone _ =
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett return (undefined, Map.empty) -- dummy implementation