DevGraph.hs revision ea22277038f87c1e12539f8917d61248015e80d8
936b7af69172dce89b577831f79c0e18d15e854bjwModule : $Header$
936b7af69172dce89b577831f79c0e18d15e854bjwCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
936b7af69172dce89b577831f79c0e18d15e854bjwLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
936b7af69172dce89b577831f79c0e18d15e854bjwMaintainer : till@tzi.de
936b7af69172dce89b577831f79c0e18d15e854bjwStability : provisional
936b7af69172dce89b577831f79c0e18d15e854bjwPortability : non-portable(Logic)
936b7af69172dce89b577831f79c0e18d15e854bjwCentral data structure for development graphs.
936b7af69172dce89b577831f79c0e18d15e854bjw Follows Sect. IV:4.2 of the CASL Reference Manual.
936b7af69172dce89b577831f79c0e18d15e854bjw References:
936b7af69172dce89b577831f79c0e18d15e854bjw T. Mossakowski, S. Autexier and D. Hutter:
936b7af69172dce89b577831f79c0e18d15e854bjw Extending Development Graphs With Hiding.
936b7af69172dce89b577831f79c0e18d15e854bjw H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
936b7af69172dce89b577831f79c0e18d15e854bjw Lecture Notes in Computer Science 2029, p. 269-283,
936b7af69172dce89b577831f79c0e18d15e854bjw Springer-Verlag 2001.
936b7af69172dce89b577831f79c0e18d15e854bjw T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
936b7af69172dce89b577831f79c0e18d15e854bjw CASL Proof calculus. In: CASL reference manual, part IV.
936b7af69172dce89b577831f79c0e18d15e854bjw Available from http://www.cofi.info
936b7af69172dce89b577831f79c0e18d15e854bjwIntegrate stuff from Saarbr�cken
936b7af69172dce89b577831f79c0e18d15e854bjwShould AS be stored in GloblaContext as well?
936b7af69172dce89b577831f79c0e18d15e854bjwsimplifyTh should be removed from instance PrettyPrint G_theory
936b7af69172dce89b577831f79c0e18d15e854bjwimport qualified Data.Graph.Inductive.Tree as Tree
936b7af69172dce89b577831f79c0e18d15e854bjwimport qualified Common.Lib.Map as Map
936b7af69172dce89b577831f79c0e18d15e854bjwimport qualified Common.OrderedMap as OMap
936b7af69172dce89b577831f79c0e18d15e854bjwimport qualified Common.Lib.Set as Set
936b7af69172dce89b577831f79c0e18d15e854bjwimport Data.List as List
936b7af69172dce89b577831f79c0e18d15e854bjwgetNewNode :: Tree.Gr a b -> Node
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhgetNewNode g = case newNodes 1 g of
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- * Types for structured specification analysis
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- ??? Some info about the theorems already proved for a node
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- should be added
936b7af69172dce89b577831f79c0e18d15e854bjw-- or should it be kept separately?
936b7af69172dce89b577831f79c0e18d15e854bjw-- what about open theorems of a node???
936b7af69172dce89b577831f79c0e18d15e854bjw-- | name of a node in a DG; auxiliary nodes may have extension string
936b7af69172dce89b577831f79c0e18d15e854bjw-- | and non-zero number (for these, names are usually hidden)
936b7af69172dce89b577831f79c0e18d15e854bjwtype NODE_NAME = (SIMPLE_ID, String, Int)
936b7af69172dce89b577831f79c0e18d15e854bjw-- | node inscriptions in development graphs
936b7af69172dce89b577831f79c0e18d15e854bjwdata DGNodeLab =
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_name :: NODE_NAME, -- name in the input language
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_theory :: G_theory, -- local theory
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_nf :: Maybe Node, -- normal form, for Theorem-Hide-Shift
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_sigma :: Maybe GMorphism, -- inclusion of signature into nf signature
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_origin :: DGOrigin, -- origin in input language
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_cons :: Conservativity,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_cons_status :: ThmLinkStatus
936b7af69172dce89b577831f79c0e18d15e854bjw | DGRef { -- reference to node in a different DG
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_name :: NODE_NAME, -- new name of node (in current DG)
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_libname :: LIB_NAME, -- pointer to DG where ref'd node resides
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_node :: Node, -- pointer to ref'd node
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne dgn_theory :: G_theory, -- local proof goals
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_nf :: Maybe Node, -- normal form, for Theorem-Hide-Shift
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature
936b7af69172dce89b577831f79c0e18d15e854bjw } deriving (Show, Eq)
936b7af69172dce89b577831f79c0e18d15e854bjwdgn_sign :: DGNodeLab -> G_sign
936b7af69172dce89b577831f79c0e18d15e854bjwdgn_sign dn = case dgn_theory dn of
936b7af69172dce89b577831f79c0e18d15e854bjw G_theory lid sig _ -> G_sign lid sig
193974072f41a843678abf5f61979c748687e66bSherry MooreisInternalNode :: DGNodeLab -> Bool
936b7af69172dce89b577831f79c0e18d15e854bjwisInternalNode (DGNode n _ _ _ _ _ _) = isInternal n
936b7af69172dce89b577831f79c0e18d15e854bjwisInternalNode _ = False
936b7af69172dce89b577831f79c0e18d15e854bjwisRefNode :: DGNodeLab -> Bool
936b7af69172dce89b577831f79c0e18d15e854bjwisRefNode (DGNode _ _ _ _ _ _ _) = False
193974072f41a843678abf5f61979c748687e66bSherry MooreisRefNode _ = True
936b7af69172dce89b577831f79c0e18d15e854bjw-- gets the name of a development graph node as a string
936b7af69172dce89b577831f79c0e18d15e854bjwgetDGNodeName :: DGNodeLab -> String
936b7af69172dce89b577831f79c0e18d15e854bjwgetDGNodeName dgn = showName $ dgn_name dgn
936b7af69172dce89b577831f79c0e18d15e854bjwemptyNodeName :: NODE_NAME
936b7af69172dce89b577831f79c0e18d15e854bjwemptyNodeName = (mkSimpleId "","",0)
936b7af69172dce89b577831f79c0e18d15e854bjwshowInt :: Int -> String
936b7af69172dce89b577831f79c0e18d15e854bjwshowInt i = if i==0 then "" else show i
936b7af69172dce89b577831f79c0e18d15e854bjwshowName :: NODE_NAME -> String
936b7af69172dce89b577831f79c0e18d15e854bjwshowName (n,s,i) = show n ++ if ext=="" then "" else "_"++ext
936b7af69172dce89b577831f79c0e18d15e854bjw where ext = s ++ showInt i
936b7af69172dce89b577831f79c0e18d15e854bjwmakeName :: SIMPLE_ID -> NODE_NAME
936b7af69172dce89b577831f79c0e18d15e854bjwmakeName n = (n,"",0)
936b7af69172dce89b577831f79c0e18d15e854bjwgetName :: NODE_NAME -> SIMPLE_ID
936b7af69172dce89b577831f79c0e18d15e854bjwgetName (n,_,_) = n
936b7af69172dce89b577831f79c0e18d15e854bjwmakeMaybeName :: Maybe SIMPLE_ID -> NODE_NAME
936b7af69172dce89b577831f79c0e18d15e854bjwmakeMaybeName Nothing = emptyNodeName
936b7af69172dce89b577831f79c0e18d15e854bjwmakeMaybeName (Just n) = makeName n
936b7af69172dce89b577831f79c0e18d15e854bjwinc :: NODE_NAME -> NODE_NAME
936b7af69172dce89b577831f79c0e18d15e854bjwinc (n,s,i) = (n,s,i+1)
936b7af69172dce89b577831f79c0e18d15e854bjwisInternal :: NODE_NAME -> Bool
936b7af69172dce89b577831f79c0e18d15e854bjwisInternal (_,s,i) = (i/=0) || s/=""
936b7af69172dce89b577831f79c0e18d15e854bjwextName :: String -> NODE_NAME -> NODE_NAME
936b7af69172dce89b577831f79c0e18d15e854bjwextName s (n,s1,i) = (n,s1++showInt i++s,0)
936b7af69172dce89b577831f79c0e18d15e854bjwisDGRef :: DGNodeLab -> Bool
936b7af69172dce89b577831f79c0e18d15e854bjwisDGRef (DGNode _ _ _ _ _ _ _) = False
936b7af69172dce89b577831f79c0e18d15e854bjwisDGRef (DGRef _ _ _ _ _ _) = True
936b7af69172dce89b577831f79c0e18d15e854bjwlocallyEmpty :: DGNodeLab -> Bool
936b7af69172dce89b577831f79c0e18d15e854bjwlocallyEmpty dgn =
936b7af69172dce89b577831f79c0e18d15e854bjw case dgn_theory dgn of
936b7af69172dce89b577831f79c0e18d15e854bjw G_theory _lid _sigma sens ->
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh (\s -> not (Logic.Prover.isAxiom s) && not (isProvenSenStatus s) ) sens
936b7af69172dce89b577831f79c0e18d15e854bjw-- | link inscriptions in development graphs
936b7af69172dce89b577831f79c0e18d15e854bjwdata DGLinkLab = DGLink {
936b7af69172dce89b577831f79c0e18d15e854bjw dgl_morphism :: GMorphism, -- signature morphism of link
936b7af69172dce89b577831f79c0e18d15e854bjw dgl_type :: DGLinkType, -- type: local, global, def, thm?
936b7af69172dce89b577831f79c0e18d15e854bjw dgl_origin :: DGOrigin } -- origin in input language
936b7af69172dce89b577831f79c0e18d15e854bjw deriving (Show, Eq)
936b7af69172dce89b577831f79c0e18d15e854bjwinstance PrettyPrint DGLinkLab where
936b7af69172dce89b577831f79c0e18d15e854bjw printText0 ga l = printText0 ga (dgl_morphism l)
936b7af69172dce89b577831f79c0e18d15e854bjw <+> printText0 ga (dgl_type l)
936b7af69172dce89b577831f79c0e18d15e854bjw <+> printText0 ga (dgl_origin l)
936b7af69172dce89b577831f79c0e18d15e854bjw proof status = (DG0,[(R1,DG1),...,(Rn,DGn)])
936b7af69172dce89b577831f79c0e18d15e854bjw DG0 is the development graph resulting from the static analysis
936b7af69172dce89b577831f79c0e18d15e854bjw Ri is a list of rules that transforms DGi-1 to DGi
936b7af69172dce89b577831f79c0e18d15e854bjw With the list of intermediate proof states, one can easily implement
936b7af69172dce89b577831f79c0e18d15e854bjw an undo operation
936b7af69172dce89b577831f79c0e18d15e854bjw{-type ProofStatus = (GlobalContext,LibEnv,[([DGRule],[DGChange])],DGraph)
936b7af69172dce89b577831f79c0e18d15e854bjwumstellen auf:-}
936b7af69172dce89b577831f79c0e18d15e854bjwtype ProofHistory = [([DGRule],[DGChange])]
936b7af69172dce89b577831f79c0e18d15e854bjwtype ProofStatus = (LIB_NAME,LibEnv,Map.Map LIB_NAME ProofHistory)
936b7af69172dce89b577831f79c0e18d15e854bjwdata DGChange = InsertNode (LNode DGNodeLab)
936b7af69172dce89b577831f79c0e18d15e854bjw | DeleteNode (LNode DGNodeLab)
936b7af69172dce89b577831f79c0e18d15e854bjw | InsertEdge (LEdge DGLinkLab)
936b7af69172dce89b577831f79c0e18d15e854bjw | DeleteEdge (LEdge DGLinkLab)
936b7af69172dce89b577831f79c0e18d15e854bjw deriving Eq
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horneinstance Show DGChange where
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne show (InsertNode (n,_)) = "InsertNode "++show n
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne show (DeleteNode (n,_)) = "DeleteNode "++show n
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne show (InsertEdge (n,m,_)) = "InsertEdge "++show n++"->"++show m
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne show (DeleteEdge (n,m,_)) = "DeleteEdge "++show n++"->"++show m
936b7af69172dce89b577831f79c0e18d15e854bjw-- | Link types of development graphs
936b7af69172dce89b577831f79c0e18d15e854bjw-- | Sect. IV:4.2 of the CASL Reference Manual explains them in depth
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Hornedata DGLinkType = LocalDef
936b7af69172dce89b577831f79c0e18d15e854bjw | HidingDef
936b7af69172dce89b577831f79c0e18d15e854bjw | FreeDef MaybeNode -- the "parameter" node
936b7af69172dce89b577831f79c0e18d15e854bjw | CofreeDef MaybeNode -- the "parameter" node
936b7af69172dce89b577831f79c0e18d15e854bjw | LocalThm ThmLinkStatus Conservativity ThmLinkStatus
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne -- ??? Some more proof information is needed here
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne -- (proof tree, ...)
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne | GlobalThm ThmLinkStatus Conservativity ThmLinkStatus
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne | HidingThm GMorphism ThmLinkStatus
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne | FreeThm GMorphism Bool
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne -- DGLink S1 S2 m2 (DGLinkType m1 p) n
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne -- corresponds to a span of morphisms
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne -- S1 <--m1-- S --m2--> S2
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne deriving (Show, Eq)
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horneinstance PrettyPrint DGLinkType where
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne printText0 _ t = text $ case t of
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne LocalDef -> "LocalDef"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne GlobalDef -> "GlobalDef"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne HidingDef -> "HidingDef"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne FreeDef _ -> "FreeDef"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne CofreeDef _ -> "CofreeDef"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne LocalThm _ _ _ -> "LocalThm"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne GlobalThm _ _ _ -> "GlobalThm"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne HidingThm _ _ -> "HidingThm"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne FreeThm _ _ -> "FreeThm"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne-- | Conservativity annotations. For compactness, only the greatest
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne-- | applicable value is used in a DG
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Hornedata Conservativity = None | Cons | Mono | Def
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne deriving (Eq,Ord)
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horneinstance Show Conservativity where
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne show None = ""
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne show Cons = "Cons"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne show Mono = "Mono"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne show Def = "Def"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne-- | Rules in the development graph calculus
936b7af69172dce89b577831f79c0e18d15e854bjw-- | Sect. IV:4.4 of the CASL Reference Manual explains them in depth
936b7af69172dce89b577831f79c0e18d15e854bjwdata DGRule =
936b7af69172dce89b577831f79c0e18d15e854bjw TheoremHideShift
936b7af69172dce89b577831f79c0e18d15e854bjw | HideTheoremShift (LEdge DGLinkLab)
936b7af69172dce89b577831f79c0e18d15e854bjw | Borrowing
936b7af69172dce89b577831f79c0e18d15e854bjw | ConsShift
936b7af69172dce89b577831f79c0e18d15e854bjw | DefShift
936b7af69172dce89b577831f79c0e18d15e854bjw | MonoShift
936b7af69172dce89b577831f79c0e18d15e854bjw | MonoToCons
936b7af69172dce89b577831f79c0e18d15e854bjw | FreeIsMono
936b7af69172dce89b577831f79c0e18d15e854bjw | MonoIsFree
936b7af69172dce89b577831f79c0e18d15e854bjw | GlobDecomp (LEdge DGLinkLab) -- edge in the conclusion
936b7af69172dce89b577831f79c0e18d15e854bjw | LocDecomp (LEdge DGLinkLab)
936b7af69172dce89b577831f79c0e18d15e854bjw | LocInference (LEdge DGLinkLab)
936b7af69172dce89b577831f79c0e18d15e854bjw | GlobSubsumption (LEdge DGLinkLab)
936b7af69172dce89b577831f79c0e18d15e854bjw | Composition [LEdge DGLinkLab]
936b7af69172dce89b577831f79c0e18d15e854bjw | LocalInference
936b7af69172dce89b577831f79c0e18d15e854bjw | BasicInference AnyComorphism BasicProof -- coding and proof tree
936b7af69172dce89b577831f79c0e18d15e854bjw | BasicConsInference Edge BasicConsProof
936b7af69172dce89b577831f79c0e18d15e854bjw deriving (Show, Eq)
936b7af69172dce89b577831f79c0e18d15e854bjwinstance PrettyPrint DGRule where
936b7af69172dce89b577831f79c0e18d15e854bjw printText0 ga r = case r of
936b7af69172dce89b577831f79c0e18d15e854bjw TheoremHideShift -> text "Theorem-Hide-Shift"
936b7af69172dce89b577831f79c0e18d15e854bjw HideTheoremShift l -> text "Hide-Theorem-Shift; resulting link:" <+> printLEdgeInProof ga l
936b7af69172dce89b577831f79c0e18d15e854bjw Borrowing -> text "Borrowing"
936b7af69172dce89b577831f79c0e18d15e854bjw ConsShift -> text "Cons-Shift"
936b7af69172dce89b577831f79c0e18d15e854bjw DefShift -> text "Def-Shift"
936b7af69172dce89b577831f79c0e18d15e854bjw MonoShift -> text "Mono-Shift"
936b7af69172dce89b577831f79c0e18d15e854bjw DefToMono -> text "DefToMono"
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh MonoToCons -> text "MonoToCons"
936b7af69172dce89b577831f79c0e18d15e854bjw FreeIsMono -> text "FreeIsMono"
936b7af69172dce89b577831f79c0e18d15e854bjw MonoIsFree -> text "MonoIsFree"
936b7af69172dce89b577831f79c0e18d15e854bjw GlobDecomp l -> text "Global Decomposition; resulting link:" <+> printLEdgeInProof ga l
936b7af69172dce89b577831f79c0e18d15e854bjw LocDecomp l -> text "Local Decomposition; resulting link:" <+> printLEdgeInProof ga l
936b7af69172dce89b577831f79c0e18d15e854bjw LocInference l -> text "Local Inference; resulting link:" <+> printLEdgeInProof ga l
936b7af69172dce89b577831f79c0e18d15e854bjw GlobSubsumption l -> text "Global Subsumption; resulting link:" <+> printLEdgeInProof ga l
936b7af69172dce89b577831f79c0e18d15e854bjw Composition ls ->
936b7af69172dce89b577831f79c0e18d15e854bjw text "Composition" <+> vcat (map (printLEdgeInProof ga) ls)
936b7af69172dce89b577831f79c0e18d15e854bjw LocalInference -> text "Local Inference"
936b7af69172dce89b577831f79c0e18d15e854bjw BasicInference c bp -> text "Basic Inference using:" <+> text ("Comorphism: "++show c ++ "Proof tree: "++show bp)
936b7af69172dce89b577831f79c0e18d15e854bjw BasicConsInference _ bp -> text "Basic Cons-Inference using:" <+> text (show bp)
936b7af69172dce89b577831f79c0e18d15e854bjwprintLEdgeInProof :: GlobalAnnos -> LEdge DGLinkLab -> Doc
936b7af69172dce89b577831f79c0e18d15e854bjwprintLEdgeInProof ga (s,t,l) =
936b7af69172dce89b577831f79c0e18d15e854bjw printText0 ga s <> text "-->" <> printText0 ga t <> text ":"
936b7af69172dce89b577831f79c0e18d15e854bjw <+> printLabInProof ga l
936b7af69172dce89b577831f79c0e18d15e854bjwprintLabInProof :: GlobalAnnos -> DGLinkLab -> Doc
936b7af69172dce89b577831f79c0e18d15e854bjwprintLabInProof ga l =
936b7af69172dce89b577831f79c0e18d15e854bjw printText0 ga (dgl_type l)
936b7af69172dce89b577831f79c0e18d15e854bjw <+> text "with origin: "
936b7af69172dce89b577831f79c0e18d15e854bjw <> printText0 ga (dgl_origin l)
936b7af69172dce89b577831f79c0e18d15e854bjw <> text ", and morphism: " )
936b7af69172dce89b577831f79c0e18d15e854bjw 2 (printText0 ga (dgl_morphism l))
936b7af69172dce89b577831f79c0e18d15e854bjwdata BasicProof =
936b7af69172dce89b577831f79c0e18d15e854bjw forall lid sublogics
936b7af69172dce89b577831f79c0e18d15e854bjw basic_spec sentence symb_items symb_map_items
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh sign morphism symbol raw_symbol proof_tree .
936b7af69172dce89b577831f79c0e18d15e854bjw Logic lid sublogics
936b7af69172dce89b577831f79c0e18d15e854bjw basic_spec sentence symb_items symb_map_items
936b7af69172dce89b577831f79c0e18d15e854bjw sign morphism symbol raw_symbol proof_tree =>
936b7af69172dce89b577831f79c0e18d15e854bjw BasicProof lid (Proof_status proof_tree)
936b7af69172dce89b577831f79c0e18d15e854bjw | Conjectured
936b7af69172dce89b577831f79c0e18d15e854bjw | Handwritten
936b7af69172dce89b577831f79c0e18d15e854bjwinstance Eq BasicProof where
936b7af69172dce89b577831f79c0e18d15e854bjw Guessed == Guessed = True
936b7af69172dce89b577831f79c0e18d15e854bjw Conjectured == Conjectured = True
936b7af69172dce89b577831f79c0e18d15e854bjw Handwritten == Handwritten = True
936b7af69172dce89b577831f79c0e18d15e854bjw BasicProof lid1 p1 == BasicProof lid2 p2 =
936b7af69172dce89b577831f79c0e18d15e854bjw coerceBasicProof lid1 lid2 "Eq BasicProof" p1 == Just p2
936b7af69172dce89b577831f79c0e18d15e854bjw _ == _ = False
936b7af69172dce89b577831f79c0e18d15e854bjwinstance Show BasicProof where
936b7af69172dce89b577831f79c0e18d15e854bjw show (BasicProof _ p1) = show p1
936b7af69172dce89b577831f79c0e18d15e854bjw show Guessed = "Guessed"
936b7af69172dce89b577831f79c0e18d15e854bjw show Conjectured = "Conjectured"
936b7af69172dce89b577831f79c0e18d15e854bjw show Handwritten = "Handwritten"
936b7af69172dce89b577831f79c0e18d15e854bjwbasicProofTc :: TyCon
936b7af69172dce89b577831f79c0e18d15e854bjwbasicProofTc = mkTyCon "Static.DevGraph.BasicProof"
936b7af69172dce89b577831f79c0e18d15e854bjwinstance Typeable BasicProof where
936b7af69172dce89b577831f79c0e18d15e854bjw typeOf _ = mkTyConApp basicProofTc []
936b7af69172dce89b577831f79c0e18d15e854bjwdata BasicConsProof = BasicConsProof -- more detail to be added ...
936b7af69172dce89b577831f79c0e18d15e854bjw deriving (Show, Eq)
936b7af69172dce89b577831f79c0e18d15e854bjwdata ThmLinkStatus = LeftOpen
936b7af69172dce89b577831f79c0e18d15e854bjw | Proven DGRule [LEdge DGLinkLab]
936b7af69172dce89b577831f79c0e18d15e854bjw deriving (Show, Eq)
936b7af69172dce89b577831f79c0e18d15e854bjwinstance PrettyPrint ThmLinkStatus where
936b7af69172dce89b577831f79c0e18d15e854bjw printText0 ga tls = case tls of
936b7af69172dce89b577831f79c0e18d15e854bjw LeftOpen -> text "Open"
936b7af69172dce89b577831f79c0e18d15e854bjw Proven r ls -> hang (text "Proven with rule" <+> printText0 ga r
936b7af69172dce89b577831f79c0e18d15e854bjw $$ text "Proof based on links:")
936b7af69172dce89b577831f79c0e18d15e854bjw 2 (vcat (map (printLEdgeInProof ga) ls))
936b7af69172dce89b577831f79c0e18d15e854bjw-- | Data type indicating the origin of nodes and edges in the input language
936b7af69172dce89b577831f79c0e18d15e854bjw-- | This is not used in the DG calculus, only may be used in the future
936b7af69172dce89b577831f79c0e18d15e854bjw-- | for reconstruction of input and management of change.
936b7af69172dce89b577831f79c0e18d15e854bjwdata DGOrigin = DGBasic | DGExtension | DGTranslation | DGUnion | DGHiding
936b7af69172dce89b577831f79c0e18d15e854bjw | DGRevealing | DGRevealTranslation | DGFree | DGCofree
936b7af69172dce89b577831f79c0e18d15e854bjw | DGLocal | DGClosed | DGClosedLenv | DGLogicQual | DGLogicQualLenv
936b7af69172dce89b577831f79c0e18d15e854bjw | DGFormalParams | DGImports | DGSpecInst SIMPLE_ID | DGFitSpec
936b7af69172dce89b577831f79c0e18d15e854bjw | DGView SIMPLE_ID | DGFitView SIMPLE_ID | DGFitViewImp SIMPLE_ID
936b7af69172dce89b577831f79c0e18d15e854bjw | DGFitViewA SIMPLE_ID | DGFitViewAImp SIMPLE_ID | DGProof
936b7af69172dce89b577831f79c0e18d15e854bjw | DGintegratedSCC
936b7af69172dce89b577831f79c0e18d15e854bjw deriving (Show, Eq)
936b7af69172dce89b577831f79c0e18d15e854bjwtype DGraph = Tree.Gr DGNodeLab DGLinkLab
936b7af69172dce89b577831f79c0e18d15e854bjw-- | Node with signature in a DG
936b7af69172dce89b577831f79c0e18d15e854bjwdata NodeSig = NodeSig Node G_sign deriving (Show, Eq)
936b7af69172dce89b577831f79c0e18d15e854bjw-- | NodeSig or possibly the empty sig in a logic
936b7af69172dce89b577831f79c0e18d15e854bjw-- | (but since we want to avoid lots of vacuous nodes with empty sig,
936b7af69172dce89b577831f79c0e18d15e854bjw-- | we do not assign a real node in the DG here)
936b7af69172dce89b577831f79c0e18d15e854bjwdata MaybeNode = JustNode NodeSig | EmptyNode AnyLogic deriving (Show, Eq)
8eadeb3489ef8b23c9940c162fade966feeaa2d0mlinstance PrettyPrint NodeSig where
8eadeb3489ef8b23c9940c162fade966feeaa2d0ml printText0 ga (NodeSig n sig) =
8eadeb3489ef8b23c9940c162fade966feeaa2d0ml ptext "node" <+> printText0 ga n <> ptext ":" <> printText0 ga sig
936b7af69172dce89b577831f79c0e18d15e854bjwemptyG_sign :: AnyLogic -> G_sign
936b7af69172dce89b577831f79c0e18d15e854bjwemptyG_sign (Logic lid) = G_sign lid (empty_signature lid)
936b7af69172dce89b577831f79c0e18d15e854bjwgetSig :: NodeSig -> G_sign
936b7af69172dce89b577831f79c0e18d15e854bjwgetSig (NodeSig _ sigma) = sigma
936b7af69172dce89b577831f79c0e18d15e854bjwgetNode :: NodeSig -> Node
936b7af69172dce89b577831f79c0e18d15e854bjwgetNode (NodeSig n _) = n
936b7af69172dce89b577831f79c0e18d15e854bjwgetMaybeSig :: MaybeNode -> G_sign
936b7af69172dce89b577831f79c0e18d15e854bjwgetMaybeSig (JustNode ns) = getSig ns
936b7af69172dce89b577831f79c0e18d15e854bjwgetMaybeSig (EmptyNode l) = emptyG_sign l
936b7af69172dce89b577831f79c0e18d15e854bjwgetLogic :: MaybeNode -> AnyLogic
936b7af69172dce89b577831f79c0e18d15e854bjwgetLogic (JustNode ns) = getNodeLogic ns
936b7af69172dce89b577831f79c0e18d15e854bjwgetLogic (EmptyNode l) = l
936b7af69172dce89b577831f79c0e18d15e854bjwgetNodeLogic :: NodeSig -> AnyLogic
936b7af69172dce89b577831f79c0e18d15e854bjwgetNodeLogic (NodeSig _ (G_sign lid _)) = Logic lid
936b7af69172dce89b577831f79c0e18d15e854bjw-- | Create a node that represents a union of signatures
936b7af69172dce89b577831f79c0e18d15e854bjwnodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin
936b7af69172dce89b577831f79c0e18d15e854bjw -> Result (NodeSig, DGraph)
936b7af69172dce89b577831f79c0e18d15e854bjwnodeSigUnion lgraph dg nodeSigs orig =
936b7af69172dce89b577831f79c0e18d15e854bjw do sigUnion@(G_sign lid sigU) <- gsigManyUnion lgraph
936b7af69172dce89b577831f79c0e18d15e854bjw $ map getMaybeSig nodeSigs
936b7af69172dce89b577831f79c0e18d15e854bjw let nodeContents = DGNode {dgn_name = emptyNodeName,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_theory = G_theory lid sigU noSens,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_nf = Nothing,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_sigma = Nothing,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_origin = orig,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_cons = None,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_cons_status = LeftOpen}
936b7af69172dce89b577831f79c0e18d15e854bjw node = getNewNode dg
936b7af69172dce89b577831f79c0e18d15e854bjw dg' = insNode (node, nodeContents) dg
936b7af69172dce89b577831f79c0e18d15e854bjw inslink dgres nsig = do
936b7af69172dce89b577831f79c0e18d15e854bjw dgv <- dgres
936b7af69172dce89b577831f79c0e18d15e854bjw case nsig of
936b7af69172dce89b577831f79c0e18d15e854bjw EmptyNode _ -> dgres
936b7af69172dce89b577831f79c0e18d15e854bjw JustNode (NodeSig n sig) -> do
936b7af69172dce89b577831f79c0e18d15e854bjw incl <- ginclusion lgraph sig sigUnion
936b7af69172dce89b577831f79c0e18d15e854bjw return $ insEdge (n, node, DGLink
936b7af69172dce89b577831f79c0e18d15e854bjw {dgl_morphism = incl,
936b7af69172dce89b577831f79c0e18d15e854bjw dgl_type = GlobalDef,
936b7af69172dce89b577831f79c0e18d15e854bjw dgl_origin = orig }) dgv
936b7af69172dce89b577831f79c0e18d15e854bjw dg'' <- foldl inslink (return dg') nodeSigs
936b7af69172dce89b577831f79c0e18d15e854bjw return (NodeSig node sigUnion, dg'')
936b7af69172dce89b577831f79c0e18d15e854bjw-- | Extend the development graph with given morphism originating
936b7af69172dce89b577831f79c0e18d15e854bjw-- from given NodeSig
936b7af69172dce89b577831f79c0e18d15e854bjwextendDGraph :: DGraph -- ^ the development graph to be extended
936b7af69172dce89b577831f79c0e18d15e854bjw -> NodeSig -- ^ the NodeSig from which the morphism originates
936b7af69172dce89b577831f79c0e18d15e854bjw -> GMorphism -- ^ the morphism to be inserted
936b7af69172dce89b577831f79c0e18d15e854bjw -> DGOrigin
936b7af69172dce89b577831f79c0e18d15e854bjw -> Result (NodeSig, DGraph)
936b7af69172dce89b577831f79c0e18d15e854bjw-- ^ returns the target signature of the morphism and the resulting DGraph
936b7af69172dce89b577831f79c0e18d15e854bjwextendDGraph dg (NodeSig n _) morph orig = case cod Grothendieck morph of
936b7af69172dce89b577831f79c0e18d15e854bjw targetSig@(G_sign lid tar) -> let
936b7af69172dce89b577831f79c0e18d15e854bjw nodeContents = DGNode {dgn_name = emptyNodeName,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_theory = G_theory lid tar noSens,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_nf = Nothing,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_sigma = Nothing,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_origin = orig,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_cons = None,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_cons_status = LeftOpen}
936b7af69172dce89b577831f79c0e18d15e854bjw linkContents = DGLink {dgl_morphism = morph,
936b7af69172dce89b577831f79c0e18d15e854bjw dgl_type = GlobalDef, -- TODO: other type
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne dgl_origin = orig}
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne node = getNewNode dg
936b7af69172dce89b577831f79c0e18d15e854bjw dg' = insNode (node, nodeContents) dg
936b7af69172dce89b577831f79c0e18d15e854bjw dg'' = insEdge (n, node, linkContents) dg'
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne in return (NodeSig node targetSig, dg'')
936b7af69172dce89b577831f79c0e18d15e854bjw-- | Extend the development graph with given morphism pointing to
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne-- given NodeSig
936b7af69172dce89b577831f79c0e18d15e854bjwextendDGraphRev :: DGraph -- ^ the development graph to be extended
936b7af69172dce89b577831f79c0e18d15e854bjw -> NodeSig -- ^ the NodeSig to which the morphism points
936b7af69172dce89b577831f79c0e18d15e854bjw -> GMorphism -- ^ the morphism to be inserted
936b7af69172dce89b577831f79c0e18d15e854bjw -> DGOrigin
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne -> Result (NodeSig, DGraph)
936b7af69172dce89b577831f79c0e18d15e854bjw-- ^ returns 1. the source signature of the morphism and 2. the resulting DGraph
936b7af69172dce89b577831f79c0e18d15e854bjwextendDGraphRev dg (NodeSig n _) morph orig = case dom Grothendieck morph of
936b7af69172dce89b577831f79c0e18d15e854bjw sourceSig@(G_sign lid src) -> let
936b7af69172dce89b577831f79c0e18d15e854bjw nodeContents = DGNode {dgn_name = emptyNodeName,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_theory = G_theory lid src OMap.empty,
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne dgn_nf = Nothing,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_sigma = Nothing,
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne dgn_origin = orig,
936b7af69172dce89b577831f79c0e18d15e854bjw dgn_cons = None,
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne dgn_cons_status = LeftOpen}
936b7af69172dce89b577831f79c0e18d15e854bjw linkContents = DGLink {dgl_morphism = morph,
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne dgl_type = GlobalDef, -- TODO: other type
936b7af69172dce89b577831f79c0e18d15e854bjw dgl_origin = orig}
936b7af69172dce89b577831f79c0e18d15e854bjw node = getNewNode dg
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne dg' = insNode (node, nodeContents) dg
936b7af69172dce89b577831f79c0e18d15e854bjw dg'' = insEdge (node, n, linkContents) dg'
936b7af69172dce89b577831f79c0e18d15e854bjw in return (NodeSig node sourceSig, dg'')
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- import, formal parameters andd united signature of formal params
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhtype GenericitySig = (MaybeNode, [NodeSig], MaybeNode)
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- import, formal parameters, united signature of formal params, body
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhtype ExtGenSig = (MaybeNode, [NodeSig], G_sign, NodeSig)
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- source, morphism, parameterized target
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhtype ExtViewSig = (NodeSig,GMorphism,ExtGenSig)
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- * Types for architectural and unit specification analysis
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- (as defined for basic static semantics in Chap. III:5.1)
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhdata UnitSig = Unit_sig NodeSig
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh | Par_unit_sig [NodeSig] NodeSig
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh deriving Show
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhdata ImpUnitSigOrSig = Imp_unit_sig MaybeNode UnitSig
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh | Sig NodeSig
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne deriving Show
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhtype StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhemptyStUnitCtx :: StUnitCtx
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhemptyStUnitCtx = Map.empty
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhdata ArchSig = ArchSig StUnitCtx UnitSig deriving Show
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- * Types for global and library environments
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhdata GlobalEntry = SpecEntry ExtGenSig
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh | ViewEntry ExtViewSig
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh | ArchEntry ArchSig
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh | UnitEntry UnitSig
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh | RefEntry
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh deriving Show
936b7af69172dce89b577831f79c0e18d15e854bjwtype GlobalEnv = Map.Map SIMPLE_ID GlobalEntry
936b7af69172dce89b577831f79c0e18d15e854bjwtype GlobalContext = (GlobalAnnos,GlobalEnv,DGraph)
936b7af69172dce89b577831f79c0e18d15e854bjwtype LibEnv = Map.Map LIB_NAME GlobalContext
936b7af69172dce89b577831f79c0e18d15e854bjwemptyLibEnv :: LibEnv
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dhemptyLibEnv = Map.empty
936b7af69172dce89b577831f79c0e18d15e854bjwinstance PrettyPrint DGOrigin where
936b7af69172dce89b577831f79c0e18d15e854bjw printText0 _ origin = text $ case origin of
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh DGBasic -> "basic specification"
936b7af69172dce89b577831f79c0e18d15e854bjw DGExtension -> "extension"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne DGTranslation -> "translation"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne DGUnion -> "union"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne DGHiding -> "hiding"
936b7af69172dce89b577831f79c0e18d15e854bjw DGRevealing -> "revealing"
936b7af69172dce89b577831f79c0e18d15e854bjw DGRevealTranslation -> "translation part of a revealing"
936b7af69172dce89b577831f79c0e18d15e854bjw DGFree -> "free specification"
936b7af69172dce89b577831f79c0e18d15e854bjw DGCofree -> "cofree specification"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne DGLocal -> "local specification"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne DGClosed -> "closed specification"
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne DGClosedLenv -> "closed specification (inclusion of local environment)"
936b7af69172dce89b577831f79c0e18d15e854bjw DGFormalParams -> "formal parameters of a generic specification"
936b7af69172dce89b577831f79c0e18d15e854bjw DGImports -> "imports of a generic specification"
936b7af69172dce89b577831f79c0e18d15e854bjw DGSpecInst n -> ("instantiation of "++showPretty n "")
936b7af69172dce89b577831f79c0e18d15e854bjw DGFitSpec -> "fittig specification"
936b7af69172dce89b577831f79c0e18d15e854bjw DGView n -> ("view "++showPretty n "")
936b7af69172dce89b577831f79c0e18d15e854bjw DGFitView n -> ("fitting view "++showPretty n "")
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne DGFitViewImp n -> ("fitting view (imports) "++showPretty n "")
936b7af69172dce89b577831f79c0e18d15e854bjw DGFitViewA n -> ("fitting view (actual parameters) "++showPretty n "")
936b7af69172dce89b577831f79c0e18d15e854bjw DGFitViewAImp n -> ("fitting view (imports and actual parameters) "
936b7af69172dce89b577831f79c0e18d15e854bjw ++showPretty n "")
936b7af69172dce89b577831f79c0e18d15e854bjw DGProof -> "constructed within a proof"
936b7af69172dce89b577831f79c0e18d15e854bjw _ -> show origin
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne-- * Heterogenous sentences
936b7af69172dce89b577831f79c0e18d15e854bjwtype HetSenStatus a = SenStatus a (AnyComorphism,BasicProof)
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris HorneisProvenSenStatus :: HetSenStatus a -> Bool
936b7af69172dce89b577831f79c0e18d15e854bjwisProvenSenStatus = any isProvenSenStatusAux . thmStatus
936b7af69172dce89b577831f79c0e18d15e854bjw where isProvenSenStatusAux (_,BasicProof _ (Proved _ _ _ _ _)) = True
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris Horne isProvenSenStatusAux _ = False
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- * Grothendieck theories
4c06356b0f0fffb4fc1b6eccc8e5d8e2254a84d6dh-- | Grothendieck theories
936b7af69172dce89b577831f79c0e18d15e854bjwdata G_theory = forall lid sublogics
936b7af69172dce89b577831f79c0e18d15e854bjw basic_spec sentence symb_items symb_map_items
936b7af69172dce89b577831f79c0e18d15e854bjw sign morphism symbol raw_symbol proof_tree .
936b7af69172dce89b577831f79c0e18d15e854bjw Logic lid sublogics
936b7af69172dce89b577831f79c0e18d15e854bjw basic_spec sentence symb_items symb_map_items
936b7af69172dce89b577831f79c0e18d15e854bjw sign morphism symbol raw_symbol proof_tree =>
936b7af69172dce89b577831f79c0e18d15e854bjw G_theory lid sign (ThSens sentence (AnyComorphism,BasicProof))
936b7af69172dce89b577831f79c0e18d15e854bjwcoerceThSens ::
936b7af69172dce89b577831f79c0e18d15e854bjw (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
936b7af69172dce89b577831f79c0e18d15e854bjw sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
936b7af69172dce89b577831f79c0e18d15e854bjw Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
936b7af69172dce89b577831f79c0e18d15e854bjw sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
936b7af69172dce89b577831f79c0e18d15e854bjw Typeable b) => lid1 -> lid2 -> String
936b7af69172dce89b577831f79c0e18d15e854bjw -> ThSens sentence1 b -> m (ThSens sentence2 b)
936b7af69172dce89b577831f79c0e18d15e854bjwcoerceThSens l1 l2 msg t1 = primCoerce l1 l2 msg t1
936b7af69172dce89b577831f79c0e18d15e854bjwinstance Eq G_theory where
936b7af69172dce89b577831f79c0e18d15e854bjw G_theory l1 sig1 sens1 == G_theory l2 sig2 sens2 =
936b7af69172dce89b577831f79c0e18d15e854bjw coerceSign l1 l2 "" sig1 == Just sig2
936b7af69172dce89b577831f79c0e18d15e854bjw && coerceThSens l1 l2 "" sens1 == Just sens2
936b7af69172dce89b577831f79c0e18d15e854bjwinstance Show G_theory where
936b7af69172dce89b577831f79c0e18d15e854bjw show (G_theory _ sign sens) =
936b7af69172dce89b577831f79c0e18d15e854bjw show sign ++ "\n" ++ show sens
936b7af69172dce89b577831f79c0e18d15e854bjwinstance PrettyPrint G_theory where
936b7af69172dce89b577831f79c0e18d15e854bjw printText0 ga g = case simplifyTh g of
936b7af69172dce89b577831f79c0e18d15e854bjw G_theory lid sign sens ->
936b7af69172dce89b577831f79c0e18d15e854bjw printText0 ga sign $++$ vsep (map (print_named lid ga)
936b7af69172dce89b577831f79c0e18d15e854bjw $ toNamedList sens)
936b7af69172dce89b577831f79c0e18d15e854bjw-- | compute sublogic of a theory
96c4a178a18cd52ee5001195f1552d9cef0c38f0Chris HornesublogicOfTh :: G_theory -> G_sublogics
936b7af69172dce89b577831f79c0e18d15e854bjwsublogicOfTh (G_theory lid sigma sens) =
936b7af69172dce89b577831f79c0e18d15e854bjw (min_sublogic_sign lid sigma)
936b7af69172dce89b577831f79c0e18d15e854bjw OMap.map (min_sublogic_sentence lid . value)
936b7af69172dce89b577831f79c0e18d15e854bjw in G_sublogics lid sub
OMap.map (mapValue $ simplify_sen lid sigma) sens
type GDiagram = Tree.Gr G_theory GMorphism
return (undefined,Map.empty) -- dummy implementation