OMDocDefs.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : $Header$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : OMDoc-related functions for conversion (in\/out)
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Hendrik Iben, Uni Bremen 2005-2007
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederMaintainer : hiben@informatik.uni-bremen.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : non-portable
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederDefinitions for reading\/writing omdoc
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport qualified Common.Id as Id
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport qualified Data.Set as Set
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport qualified Common.Lib.Rel as Rel
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport qualified Data.Map as Map
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport qualified OMDoc.HetsDefs as Hets
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidebugEnv::forall a . DbgKey -> String -> a -> a
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- Global-Options (for debugging currently)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata GlobalOptions =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini dbgInf :: DbgInf
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , hetsOpts :: HetcatsOpts
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , processingConstraint :: Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini deriving Show
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidebugGO::forall a . GlobalOptions->DbgKey->String->a->a
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidebugGO go = debug (dbgInf go)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidebugGOIO::GlobalOptions->DbgKey->String->IO ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidebugGOIO go = debugIO (dbgInf go)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniemptyGlobalOptions::GlobalOptions
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniemptyGlobalOptions =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini dbgInf = (simpleDebug [])
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , processingConstraint = False
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- OMDoc definitions
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniomdocNameXMLNS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,omdocNameXMLAttr :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniomdocNameXMLNS = "xml"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniomdocNameXMLAttr = "id"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitheoryNameXMLNS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,theoryNameXMLAttr :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitheoryNameXMLNS = "xml"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitheoryNameXMLAttr = "id"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniaxiomNameXMLNS
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini ,axiomNameXMLAttr :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniaxiomNameXMLNS = "xml"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaxiomNameXMLAttr = "id"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,sortNameXMLAttr :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisortNameXMLNS = ""
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisortNameXMLAttr = "name"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisymbolTypeXMLNS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,symbolTypeXMLAttr :: String
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillysymbolTypeXMLNS = ""
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillysymbolTypeXMLAttr = "role"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder ,predNameXMLAttr :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpredNameXMLNS = ""
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpredNameXMLAttr = "name"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,opNameXMLAttr :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniopNameXMLNS = ""
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniopNameXMLAttr = "name"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini--caslQuantificationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslConjunctionS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslDisjunctionS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslImplicationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslImplication2S
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslEquivalenceS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslEquivalence2S
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslNegationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslPredicationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslDefinednessS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslExistl_equationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslStrong_equationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslMembershipS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslSort_gen_axS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslSymbolQuantUniversalS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslSymbolQuantExistentialS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslSymbolQuantUnique_existentialS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslSymbolAtomFalseS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,caslSymbolAtomTrueS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniunsupportedS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitypeS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniaxiomInclusionS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,theoryInclusionS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini--caslQuantificationS = "quantification"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslConjunctionS = "conjunction"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslDisjunctionS = "disjunction"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslImplicationS = "implication"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslImplication2S = "implies"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslEquivalenceS = "equivalence"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslEquivalence2S = "equal"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslNegationS = "neg"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslPredicationS = "predication"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedercaslDefinednessS = "definedness"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercaslExistl_equationS = "existial-equation"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercaslStrong_equationS = "strong-equation"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslMembershipS = "membership"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslSort_gen_axS = "sort-gen-ax"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata FormulaType =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini FTConjunction
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini | FTDisjunction
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini | FTImplication
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini | FTEquivalence
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | FTPredication
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder | FTDefinedness
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | FTExistl_equation
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder | FTStrong_equation
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | FTMembership
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | FTSort_gen_ax
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torriniinstance Show FormulaType where
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini show FTConjunction = caslConjunctionS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini show FTDisjunction = caslDisjunctionS
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder show FTImplication = caslImplicationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini show FTEquivalence = caslEquivalenceS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini show FTNegation = caslNegationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini show FTPredication = caslPredicationS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini show FTDefinedness = caslDefinednessS
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini show FTExistl_equation = caslExistl_equationS
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini show FTStrong_equation = caslStrong_equationS
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini show FTMembership = caslMembershipS
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini show FTSort_gen_ax = caslSort_gen_axS
c730c28919b53f940ed319ebb42780244c528e29Paolo Torriniinstance Read FormulaType where
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini readsPrec _ "conjunction" = [(FTConjunction, "")]
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini readsPrec _ "disjunction" = [(FTDisjunction, "")]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini readsPrec _ "implication" = [(FTImplication, "")]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini readsPrec _ "implies" = [(FTImplication, "")]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini readsPrec _ "equivalence" = [(FTEquivalence, "")]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini readsPrec _ "equal" = [(FTEquivalence, "")]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini readsPrec _ "neg" = [(FTNegation, "")]
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini readsPrec _ "predication" = [(FTPredication, "")]
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini readsPrec _ "definedness" = [(FTDefinedness, "")]
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini readsPrec _ "existial-equation" = [(FTExistl_equation, "")]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini readsPrec _ "strong-equation" = [(FTStrong_equation, "")]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini readsPrec _ "membership" = [(FTMembership, "")]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini readsPrec _ "sort-gen-ax" = [(FTSort_gen_ax, "")]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini readsPrec _ _ = []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslSymbolQuantUniversalS = "universal"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicaslSymbolQuantExistentialS = "existential"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicaslSymbolQuantUnique_existentialS = "unique-existential"
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinicaslSymbolAtomFalseS = "false"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaedercaslSymbolAtomTrueS = "true"
c730c28919b53f940ed319ebb42780244c528e29Paolo TorriniunsupportedS = "unsupported-formula"
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinitypeS = "type"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicaslS = "casl"
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederaxiomInclusionS = "axiom-inclusion"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitheoryInclusionS = "theory-inclusion"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | describes a value with an xml-name and an origin
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrinitype XmlNamedWO a b = XmlNamed (Hets.WithOrigin a b)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | describes a value with an xml-name and a Graph.Node for origin
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrinitype XmlNamedWON a = XmlNamedWO a Graph.Node
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | a SORT with an xml-name and a Graph.Node for origin
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrinitype XmlNamedWONSORT = XmlNamedWON SORT
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | strip origin
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinixnWOaToXNa::XmlNamedWO a b->XmlNamed a
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinixnWOaToXNa a = XmlNamed (Hets.woItem (xnItem a)) (xnName a)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | strip all
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinixnWOaToa::XmlNamedWO a b->a
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinixnWOaToa a = Hets.woItem (xnItem a)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | get origin (strip value and name)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinixnWOaToO::XmlNamedWO a b->b
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinixnWOaToO a = Hets.woOrigin (xnItem a)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- just an alias to complete this
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | strip xml-name
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinixnWOaToWOa::XmlNamedWO a b->Hets.WithOrigin a b
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederxnWOaToWOa a = xnItem a
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | a predicate with xml-name and origin
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederdata PredTypeXNWON = PredTypeXNWON {predArgsXNWON :: [XmlNamedWONSORT]}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder deriving (Show, Eq, Ord)
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- | an operator with xml-name and origin
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata OpTypeXNWON = OpTypeXNWON { opKindX :: OpKind, opArgsXNWON :: [XmlNamedWONSORT], opResXNWON :: XmlNamedWONSORT }
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini deriving (Show, Eq, Ord)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- | tries to find the 'pure' sort among named sorts
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedersortToXmlNamedWONSORT::[XmlNamedWONSORT]->SORT->(Maybe XmlNamedWONSORT)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisortToXmlNamedWONSORT list s = find (\i -> (Hets.idToString s) == (Hets.idToString (xnWOaToa i))) list
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisortToXmlNamedWONSORTSet::Set.Set XmlNamedWONSORT->SORT->(Maybe XmlNamedWONSORT)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisortToXmlNamedWONSORTSet sortset sort =
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maeder case Set.toList $ Set.filter (\i -> sort == (xnWOaToa i)) sortset of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder [] -> Nothing
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (i:_) -> (Just i)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederaToXmlNamedWONa::(Eq a)=>[XmlNamedWON a]->a->(Maybe (XmlNamedWON a))
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederaToXmlNamedWONa xnlist a = find (\i -> a == (xnWOaToa i)) xnlist
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederaToXmlNamedWONaSet::(Eq a, Ord a)=>Set.Set (XmlNamedWON a)->a->(Maybe (XmlNamedWON a))
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederaToXmlNamedWONaSet xnset a =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder case Set.toList $ Set.filter (\i -> a == (xnWOaToa i)) xnset of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini [] -> Nothing
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (i:_) -> (Just i)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederpredTypeToPredTypeXNWON::[XmlNamedWON SORT]->PredType->PredTypeXNWON
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipredTypeToPredTypeXNWON xnwonsorts (PredType {predArgs = pA}) =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder xnwonargs = map (\a -> case (sortToXmlNamedWONSORT xnwonsorts a) of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Nothing -> error "Unable to find xml-named sort for predicate argument!"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (Just xnsort) -> xnsort) pA
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder PredTypeXNWON xnwonargs
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederpredTypeXNWONToPredType::PredTypeXNWON->PredType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipredTypeXNWONToPredType (PredTypeXNWON xnargs) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini PredType $ map xnWOaToa xnargs
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederopTypeToOpTypeXNWON::[XmlNamedWON SORT]->OpType->OpTypeXNWON
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederopTypeToOpTypeXNWON xnwonsorts (OpType {CASL.Sign.opKind = oK, opArgs = oA, opRes = oR}) =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder xnwonargs = map (\a -> case (sortToXmlNamedWONSORT xnwonsorts a) of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Nothing -> error "Unable to find xml-named sort for operator argument!"
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder (Just xnsort) -> xnsort) oA
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder xnwonres = case sortToXmlNamedWONSORT xnwonsorts oR of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Nothing -> error "Unable to find xml-named sort for operator result!"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (Just xnsort) -> xnsort
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini OpTypeXNWON oK xnwonargs xnwonres
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederopTypeXNWONToOpType::OpTypeXNWON->OpType
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederopTypeXNWONToOpType (OpTypeXNWON fk xnargs xnres) =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder OpType fk (map xnWOaToa xnargs) (xnWOaToa xnres)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedertype XmlNamedWONId = XmlNamedWON Id.Id
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | A Theory (DevGraph-Node) with an xml-name
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedertype TheoryXN = XmlNamed (Graph.Node, NodeName)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder-- | Set of Theories
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maedertype TheoryXNSet = Set.Set TheoryXN
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | name by node
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedergetTheoryXmlName::TheoryXNSet->Graph.Node->Maybe XmlName
a2e8cca8a8217b158b0b7a760e8234c03186456dChristian MaedergetTheoryXmlName ts n =
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder case find (\i -> (fst (xnItem i)) == n) $ Set.toList ts of
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Nothing -> Nothing
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder (Just i) -> Just (xnName i)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder-- | node by name
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinigetNodeForTheoryName::TheoryXNSet->XmlName->Maybe Graph.Node
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinigetNodeForTheoryName xntheoryset xname =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini searchname = case xname of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini case find (\i -> (xnName i) == searchname) $ Set.toList xntheoryset of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Nothing -> Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (Just i) -> Just (fst (xnItem i))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinitype XmlTaggedDevGraph =
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Set.Set XmlNamedWONSORT
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder , Rel.Rel XmlNamedWONSORT
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , [(XmlNamedWONId, PredType)]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , [(XmlNamedWONId, OpType)]
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maedertype XmlTaggedLibEnv =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini XmlTaggedDevGraph