fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder{-# LANGUAGE DeriveDataTypeable #-}
c208973c890b8f993297720fd0247bc7481d4304Christian MaederDescription : auxiliary datastructures for development graphs
c208973c890b8f993297720fd0247bc7481d4304Christian MaederCopyright : (c) DFKI GmbH 2011
c208973c890b8f993297720fd0247bc7481d4304Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
c208973c890b8f993297720fd0247bc7481d4304Christian MaederMaintainer : Christian.Maeder@dfki.de
c208973c890b8f993297720fd0247bc7481d4304Christian MaederStability : provisional
dc21a74c78d138d5eba4a2b7c7965936f0892d77Christian MaederPortability : portable
c208973c890b8f993297720fd0247bc7481d4304Christian Maederimport qualified Common.Lib.Rel as Rel
c208973c890b8f993297720fd0247bc7481d4304Christian Maederimport qualified Data.Map as Map
c208973c890b8f993297720fd0247bc7481d4304Christian Maederimport qualified Data.Set as Set
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- ** node label types
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaederdata XPathPart = ElemName String | ChildIndex Int deriving (Show, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder{- | name of a node in a DG; auxiliary nodes may have extension string
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder and non-zero number (for these, names are usually hidden). -}
c208973c890b8f993297720fd0247bc7481d4304Christian Maederdata NodeName = NodeName
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa { getName :: IRI
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , extString :: String
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , extIndex :: Int
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , xpath :: [XPathPart]
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder , srcRange :: Range
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder } deriving (Show, Typeable, Data)
21bac9aa8d0fae4d14308065235814f653241357Christian Maederinstance Ord NodeName where
21bac9aa8d0fae4d14308065235814f653241357Christian Maeder compare n1 n2 = compare (showName n1) (showName n2)
21bac9aa8d0fae4d14308065235814f653241357Christian Maederinstance Eq NodeName where
21bac9aa8d0fae4d14308065235814f653241357Christian Maeder n1 == n2 = compare n1 n2 == EQ
c208973c890b8f993297720fd0247bc7481d4304Christian MaederreadXPath :: Monad m => String -> m [XPathPart]
c208973c890b8f993297720fd0247bc7481d4304Christian MaederreadXPath = mapM readXPathComp . splitOn '/'
c208973c890b8f993297720fd0247bc7481d4304Christian MaederreadXPathComp :: Monad m => String -> m XPathPart
c208973c890b8f993297720fd0247bc7481d4304Christian MaederreadXPathComp s = case splitAt 5 s of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder ("Spec[", s') -> case readMaybe $ takeWhile (/= ']') s' of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder Just i -> return $ ChildIndex i
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder Nothing -> fail "cannot read nodes ChildIndex"
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder _ -> return $ ElemName s
c208973c890b8f993297720fd0247bc7481d4304Christian MaederisInternal :: NodeName -> Bool
c208973c890b8f993297720fd0247bc7481d4304Christian MaederisInternal n = extIndex n /= 0 || not (null $ extString n)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | test if a conservativity is open, return input for None
c208973c890b8f993297720fd0247bc7481d4304Christian MaederhasOpenConsStatus :: Bool -> ConsStatus -> Bool
c208973c890b8f993297720fd0247bc7481d4304Christian MaederhasOpenConsStatus b (ConsStatus cons _ thm) = case cons of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder _ -> not $ isProvenThmLinkStatus thm
c208973c890b8f993297720fd0247bc7481d4304Christian Maederdata DGNodeType = DGNodeType
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder { isRefType :: Bool
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isProvenNode :: Bool
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isProvenCons :: Bool
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isInternalSpec :: Bool }
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian MaederlistDGNodeTypes :: [DGNodeType]
c208973c890b8f993297720fd0247bc7481d4304Christian MaederlistDGNodeTypes = let bs = [False, True] in
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder { isRefType = ref
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isProvenNode = isEmpty'
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isProvenCons = proven
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isInternalSpec = spec }
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isEmpty' <- bs
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , proven <- bs
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , spec <- bs ]
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder-- | node modifications
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maederdata NodeMod = NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder { delAx :: Bool
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder , delTh :: Bool
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder , addSen :: Bool
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder , delSym :: Bool
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder , addSym :: Bool }
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder-- | an unmodified node
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederunMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederunMod = NodeMod False False False False False
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederdelAxMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederdelAxMod = unMod { delAx = True }
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederdelThMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederdelThMod = unMod { delTh = True }
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederdelSenMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederdelSenMod = delAxMod { delTh = True }
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederaddSenMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederaddSenMod = unMod { addSen = True }
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaedersenMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaedersenMod = delSenMod { addSen = True }
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederdelSymMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederdelSymMod = unMod { delSym = True }
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederaddSymMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaederaddSymMod = unMod { addSym = True }
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaedersymMod :: NodeMod
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaedersymMod = delSymMod { addSym = True }
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian MaedermergeNodeMod :: NodeMod -> NodeMod -> NodeMod
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian MaedermergeNodeMod NodeMod
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder { delAx = delAx1
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , delTh = delTh1
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , addSen = addSen1
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , delSym = delSym1
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , addSym = addSym1 }
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder { delAx = delAx2
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , delTh = delTh2
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , addSen = addSen2
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , delSym = delSym2
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , addSym = addSym2 }
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder = let delSym3 = delSym1 || delSym2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder setSenMod a b = not delSym3 && (a || b)
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder { delAx = setSenMod delAx1 delAx2
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , delTh = setSenMod delTh1 delTh2
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , addSen = setSenMod addSen1 addSen2
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , delSym = delSym3
5fcf9c4aaca73698c4c220308c9fd5fc174ae334Christian Maeder , addSym = addSym1 || addSym2 }
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- ** edge types
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | unique number for edges
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaedernewtype EdgeId = EdgeId { getEdgeNum :: Int }
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Eq, Ord, Typeable, Data)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederinstance Show EdgeId where
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder show = show . getEdgeNum
dc21a74c78d138d5eba4a2b7c7965936f0892d77Christian Maeder-- | next edge id
dc21a74c78d138d5eba4a2b7c7965936f0892d77Christian MaederincEdgeId :: EdgeId -> EdgeId
dc21a74c78d138d5eba4a2b7c7965936f0892d77Christian MaederincEdgeId (EdgeId i) = EdgeId $ i + 1
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | the first edge in a graph
c208973c890b8f993297720fd0247bc7481d4304Christian MaederstartEdgeId :: EdgeId
c208973c890b8f993297720fd0247bc7481d4304Christian MaederstartEdgeId = EdgeId 0
c208973c890b8f993297720fd0247bc7481d4304Christian MaedershowEdgeId :: EdgeId -> String
c208973c890b8f993297720fd0247bc7481d4304Christian MaedershowEdgeId (EdgeId i) = show i
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | a set of used edges
c208973c890b8f993297720fd0247bc7481d4304Christian Maedernewtype ProofBasis = ProofBasis { proofBasis :: Set.Set EdgeId }
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Eq, Ord, Typeable, Data)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederinstance Show ProofBasis where
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder show = show . Set.toList . proofBasis
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder{- | Rules in the development graph calculus,
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder Sect. IV:4.4 of the CASL Reference Manual explains them in depth
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder DGRule String
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder | DGRuleWithEdge String EdgeId
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder | DGRuleLocalInference [(String, String)] -- renamed theorems
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder | Composition [EdgeId]
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | proof status of a link
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaederdata ThmLinkStatus = LeftOpen | Proven DGRule ProofBasis
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian MaederisProvenThmLinkStatus :: ThmLinkStatus -> Bool
c208973c890b8f993297720fd0247bc7481d4304Christian MaederisProvenThmLinkStatus tls = case tls of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder LeftOpen -> False
17be7914f897d0b0c6488eb1391f5695ec74f7e1Christian MaederproofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis
17be7914f897d0b0c6488eb1391f5695ec74f7e1Christian MaederproofBasisOfThmLinkStatus tls = case tls of
17be7914f897d0b0c6488eb1391f5695ec74f7e1Christian Maeder LeftOpen -> emptyProofBasis
17be7914f897d0b0c6488eb1391f5695ec74f7e1Christian Maeder Proven _ pB -> pB
26210e52bda19c75ac6a4287d16ce9d8789b68deChristian MaederupdProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus
26210e52bda19c75ac6a4287d16ce9d8789b68deChristian MaederupdProofBasisOfThmLinkStatus tls pB = case tls of
26210e52bda19c75ac6a4287d16ce9d8789b68deChristian Maeder LeftOpen -> tls
26210e52bda19c75ac6a4287d16ce9d8789b68deChristian Maeder Proven r _ -> Proven r pB
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaederdata Scope = Local | Global deriving (Show, Eq, Ord, Typeable, Data)
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaederdata LinkKind = DefLink | ThmLink ThmLinkStatus
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
8b130bc25851c830d22a51ba03c8f2b778a6904fMarcel Zirbeldata FreeOrCofree = Free | Cofree | NPFree | Minimize
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Enum, Bounded, Read, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian MaederfcList :: [FreeOrCofree]
c208973c890b8f993297720fd0247bc7481d4304Christian MaederfcList = [minBound .. maxBound]
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | required and proven conservativity (with a proof)
c208973c890b8f993297720fd0247bc7481d4304Christian Maederdata ConsStatus = ConsStatus Conservativity Conservativity ThmLinkStatus
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian MaederisProvenConsStatusLink :: ConsStatus -> Bool
c208973c890b8f993297720fd0247bc7481d4304Christian MaederisProvenConsStatusLink = not . hasOpenConsStatus False
c208973c890b8f993297720fd0247bc7481d4304Christian MaedermkConsStatus :: Conservativity -> ConsStatus
c208973c890b8f993297720fd0247bc7481d4304Christian MaedermkConsStatus c = ConsStatus c None LeftOpen
c208973c890b8f993297720fd0247bc7481d4304Christian MaedergetConsOfStatus :: ConsStatus -> Conservativity
c208973c890b8f993297720fd0247bc7481d4304Christian MaedergetConsOfStatus (ConsStatus c _ _) = c
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | to be displayed as edge label
c208973c890b8f993297720fd0247bc7481d4304Christian MaedershowConsStatus :: ConsStatus -> String
c208973c890b8f993297720fd0247bc7481d4304Christian MaedershowConsStatus cs = case cs of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder ConsStatus None None _ -> ""
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder ConsStatus None _ LeftOpen -> ""
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder ConsStatus c _ LeftOpen -> show c ++ "?"
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder ConsStatus _ cp _ -> show cp
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | converts a DGEdgeType to a String
c208973c890b8f993297720fd0247bc7481d4304Christian MaedergetDGEdgeTypeName :: DGEdgeType -> String
c208973c890b8f993297720fd0247bc7481d4304Christian MaedergetDGEdgeTypeName e =
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder (if isInc e then (++ "Inc") else id)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder $ getDGEdgeTypeModIncName $ edgeTypeModInc e
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrevertDGEdgeTypeName :: String -> DGEdgeType
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrevertDGEdgeTypeName tp = fromMaybe (error "DevGraph.revertDGEdgeTypeName")
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder $ find ((== tp) . getDGEdgeTypeName) listDGEdgeTypes
c208973c890b8f993297720fd0247bc7481d4304Christian MaedergetDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String
c208973c890b8f993297720fd0247bc7481d4304Christian MaedergetDGEdgeTypeModIncName et = case et of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder ThmType thm isPrvn _ _ ->
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder let prvn = (if isPrvn then "P" else "Unp") ++ "roven" in
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder HidingThm -> prvn ++ "HidingThm"
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder FreeOrCofreeThm fc -> prvn ++ shows fc "Thm"
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder GlobalOrLocalThm scope isHom ->
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder let het = if isHom then id else ("Het" ++) in
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder het (case scope of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder Local -> "Local"
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder Global -> if isHom then "Global" else "") ++ prvn ++ "Thm"
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder FreeOrCofreeDef fc -> shows fc "Def"
c208973c890b8f993297720fd0247bc7481d4304Christian Maederdata DGEdgeType = DGEdgeType
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder { edgeTypeModInc :: DGEdgeTypeModInc
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isInc :: Bool }
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian Maederdata DGEdgeTypeModInc =
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder | FreeOrCofreeDef FreeOrCofree
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder | ThmType { thmEdgeType :: ThmTypes
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isProvenEdge :: Bool
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isConservativ :: Bool
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isPending :: Bool }
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian Maederdata ThmTypes =
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder | FreeOrCofreeThm FreeOrCofree
fb5b958b07a002f7f6daa0ac032976979c63b7c3Christian Maeder | GlobalOrLocalThm { thmScope :: Scope
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isHomThm :: Bool }
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | Creates a list with all DGEdgeType types
c208973c890b8f993297720fd0247bc7481d4304Christian MaederlistDGEdgeTypes :: [DGEdgeType]
c208973c890b8f993297720fd0247bc7481d4304Christian MaederlistDGEdgeTypes =
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder [ DGEdgeType { edgeTypeModInc = modinc
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isInc = isInclusion' }
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder ] ++ [ FreeOrCofreeDef fc | fc <- fcList ] ++
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder [ ThmType { thmEdgeType = thmType
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isProvenEdge = proven
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isConservativ = cons
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isPending = pending }
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder | thmType <- HidingThm
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder : [ FreeOrCofreeThm fc | fc <- fcList ] ++
fb5b958b07a002f7f6daa0ac032976979c63b7c3Christian Maeder [ GlobalOrLocalThm { thmScope = scope
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isHomThm = hom }
fb5b958b07a002f7f6daa0ac032976979c63b7c3Christian Maeder | scope <- [Local, Global]
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , hom <- [True, False]
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , proven <- [True, False]
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , cons <- [True, False]
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , pending <- [True, False]
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , isInclusion' <- [True, False]
0013ad45ed76357d2ca114ce128d9c75d42fc2ffSimon Ulbricht-- | check an EdgeType and see if its a definition link
0013ad45ed76357d2ca114ce128d9c75d42fc2ffSimon UlbrichtisDefEdgeType :: DGEdgeType -> Bool
0013ad45ed76357d2ca114ce128d9c75d42fc2ffSimon UlbrichtisDefEdgeType edgeTp = case edgeTypeModInc edgeTp of
2ed246fd6018aaa96b81825598ee74e2f1408cc4Christian Maeder ThmType {} -> False
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- * datatypes for storing the nodes of the ref tree in the global env
c208973c890b8f993297720fd0247bc7481d4304Christian Maederdata RTPointer =
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maeder | NPBranch Int (Map.Map IRI RTPointer)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder -- here the leaves can be either NPUnit or NPComp
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maeder | NPRef Int Int
55b14de0878c596dc00920ecac65bab478e930e8Christian Maeder | NPComp (Map.Map IRI RTPointer)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder {- here the leaves can be NPUnit or NPComp
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder and roots are needed for inserting edges -}
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Eq, Ord, Typeable, Data)
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian MaedermapRTNodes :: Map.Map Int Int -> RTPointer -> RTPointer
c208973c890b8f993297720fd0247bc7481d4304Christian MaedermapRTNodes f rtp = let app = flip $ Map.findWithDefault (error "mapRTNodes")
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder in case rtp of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder RTNone -> RTNone
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder NPUnit x -> NPUnit (app f x)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder NPRef x y -> NPRef (app f x) (app f y)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder NPBranch x g -> NPBranch (app f x) (Map.map (mapRTNodes f) g)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder NPComp g -> NPComp (Map.map (mapRTNodes f) g)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- compositions
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer :: RTPointer -> RTPointer -> RTPointer
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer (NPUnit n1) (NPUnit n2) = NPRef n1 n2
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer (NPUnit n1) (NPBranch _ f) = NPBranch n1 f
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer (NPUnit n1) (NPRef _ n2) = NPRef n1 n2
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer (NPRef n1 _) (NPRef _ n2) = NPRef n1 n2
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer (NPRef n1 _) (NPBranch _ f) = NPBranch n1 f
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer (NPBranch n1 f1) (NPComp f2) =
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder NPBranch n1 (Map.unionWith (\ _ y -> y) f1 f2 )
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer (NPComp f1) (NPComp f2) =
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder NPComp (Map.unionWith (\ _ y -> y) f1 f2)
c208973c890b8f993297720fd0247bc7481d4304Christian MaedercompPointer x y = error $ "compPointer:" ++ show x ++ " " ++ show y
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian MaederrefSource :: RTPointer -> Int
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefSource (NPUnit n) = n
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefSource (NPBranch n _) = n
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefSource (NPRef n _) = n
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefSource x = error ("refSource:" ++ show x)
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maederdata RTLeaves = RTLeaf Int | RTLeaves (Map.Map IRI RTLeaves)
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder deriving (Show, Typeable, Data)
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefTarget :: RTPointer -> RTLeaves
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefTarget (NPUnit n) = RTLeaf n
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefTarget (NPRef _ n) = RTLeaf n
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefTarget (NPComp f) = RTLeaves $ Map.map refTarget f
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefTarget (NPBranch _ f) = RTLeaves $ Map.map refTarget f
c208973c890b8f993297720fd0247bc7481d4304Christian MaederrefTarget x = error ("refTarget:" ++ show x)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- ** for node names
c208973c890b8f993297720fd0247bc7481d4304Christian MaederemptyNodeName :: NodeName
764c796b88ef1d3921d7807683ee7bba3e764a29Christian MaederemptyNodeName = NodeName nullIRI "" 0 [] nullRange
c208973c890b8f993297720fd0247bc7481d4304Christian MaedershowExt :: NodeName -> String
c208973c890b8f993297720fd0247bc7481d4304Christian MaedershowExt n = let i = extIndex n in extString n ++ if i == 0 then "" else show i
c208973c890b8f993297720fd0247bc7481d4304Christian MaedershowName :: NodeName -> String
c208973c890b8f993297720fd0247bc7481d4304Christian MaedershowName n = let ext = showExt n in
01ddc4cad68fa84b4e9dd41089ad876329bae5b0Christian Maeder iriToStringShortUnsecure (setAngles False $ getName n)
2ed246fd6018aaa96b81825598ee74e2f1408cc4Christian Maeder ++ if null ext then ext else "__" ++ ext
764c796b88ef1d3921d7807683ee7bba3e764a29Christian MaedermakeRgName :: IRI -> Range -> NodeName
764c796b88ef1d3921d7807683ee7bba3e764a29Christian MaedermakeRgName n = NodeName n "" 0 [ElemName $ iriToStringShortUnsecure n]
ea8e98e298f33f9362293f392c8fb192722b8904Eugen KuksamakeName :: IRI -> NodeName
764c796b88ef1d3921d7807683ee7bba3e764a29Christian MaedermakeName n = makeRgName n $ iriPos n
764c796b88ef1d3921d7807683ee7bba3e764a29Christian MaedersetSrcRange :: Range -> NodeName -> NodeName
764c796b88ef1d3921d7807683ee7bba3e764a29Christian MaedersetSrcRange r n = n { srcRange = r }
c208973c890b8f993297720fd0247bc7481d4304Christian MaederparseNodeName :: String -> NodeName
3b29702156f4c15d97b08578785725b9778c8221Christian MaederparseNodeName s =
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder let err msg = error $ "parseNodeName: malformed NodeName" ++ msg ++ s
6b08bf3d86add8676df4400a1803dba9d1041c08Christian Maeder mkName = makeName . fromMaybe (err ": ") . parseCurie
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder in case splitByList "__" s of
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder [i] -> mkName i
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder let n = mkName i
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder mSf = numberSuffix e
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder (es, sf) = fromMaybe (e, 0) mSf
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder in n { extString = es
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder , extIndex = sf }
3b29702156f4c15d97b08578785725b9778c8221Christian Maeder _ -> err ", too many __: "
c208973c890b8f993297720fd0247bc7481d4304Christian MaederincBy :: Int -> NodeName -> NodeName
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder { extIndex = extIndex n + i
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , xpath = case xpath n of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder ChildIndex j : r -> ChildIndex (j + i) : r
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder l -> ChildIndex i : l }
c208973c890b8f993297720fd0247bc7481d4304Christian Maederinc :: NodeName -> NodeName
c208973c890b8f993297720fd0247bc7481d4304Christian MaederextName :: String -> NodeName -> NodeName
c208973c890b8f993297720fd0247bc7481d4304Christian MaederextName s n = n
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder { extString = showExt n ++ take 1 s
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , extIndex = 0
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , xpath = ElemName s : xpath n }
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- ** handle edge numbers and proof bases
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | create a default ID which has to be changed when inserting a certain edge.
c208973c890b8f993297720fd0247bc7481d4304Christian MaederdefaultEdgeId :: EdgeId
c208973c890b8f993297720fd0247bc7481d4304Christian MaederdefaultEdgeId = EdgeId $ -1
c208973c890b8f993297720fd0247bc7481d4304Christian MaederemptyProofBasis :: ProofBasis
c208973c890b8f993297720fd0247bc7481d4304Christian MaederemptyProofBasis = ProofBasis Set.empty
c208973c890b8f993297720fd0247bc7481d4304Christian MaedernullProofBasis :: ProofBasis -> Bool
c208973c890b8f993297720fd0247bc7481d4304Christian MaedernullProofBasis = Set.null . proofBasis
c208973c890b8f993297720fd0247bc7481d4304Christian MaederaddEdgeId :: ProofBasis -> EdgeId -> ProofBasis
c208973c890b8f993297720fd0247bc7481d4304Christian MaederaddEdgeId (ProofBasis s) e = ProofBasis $ Set.insert e s
26210e52bda19c75ac6a4287d16ce9d8789b68deChristian MaederdelEdgeId :: ProofBasis -> EdgeId -> ProofBasis
26210e52bda19c75ac6a4287d16ce9d8789b68deChristian MaederdelEdgeId (ProofBasis s) e = ProofBasis $ Set.delete e s
26210e52bda19c75ac6a4287d16ce9d8789b68deChristian MaederupdEdgeId :: ProofBasis -> EdgeId -> EdgeId -> ProofBasis
26210e52bda19c75ac6a4287d16ce9d8789b68deChristian MaederupdEdgeId pb = addEdgeId . delEdgeId pb
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | checks if the given edge is contained in the given proof basis..
be5ff99194b2ba0a1a35093e0ea21d4da332b526Christian MaederedgeInProofBasis :: EdgeId -> ProofBasis -> Bool
be5ff99194b2ba0a1a35093e0ea21d4da332b526Christian MaederedgeInProofBasis e = Set.member e . proofBasis
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- * utilities
c208973c890b8f993297720fd0247bc7481d4304Christian MaedertopsortedLibsWithImports :: Rel.Rel LibName -> [LibName]
c208973c890b8f993297720fd0247bc7481d4304Christian MaedertopsortedLibsWithImports = concatMap Set.toList . Rel.topSort
c208973c890b8f993297720fd0247bc7481d4304Christian MaedergetMapAndMaxIndex :: Ord k => k -> (b -> Map.Map k a) -> b -> (Map.Map k a, k)
c208973c890b8f993297720fd0247bc7481d4304Christian MaedergetMapAndMaxIndex c f gctx =
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder let m = f gctx in (m, if Map.null m then c else fst $ Map.findMax m)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | or two predicates
c208973c890b8f993297720fd0247bc7481d4304Christian MaederliftOr :: (a -> Bool) -> (a -> Bool) -> a -> Bool
c208973c890b8f993297720fd0247bc7481d4304Christian MaederliftOr f g x = f x || g x