9784417c60301832780850e1ff9d7e46706268f1Till MossakowskiDescription : static analysis of DOL documents and CASL specification libraries
9784417c60301832780850e1ff9d7e46706268f1Till MossakowskiCopyright : (c) Till Mossakowski, Uni Magdeburg 2002-2016
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable(Logic)
9784417c60301832780850e1ff9d7e46706268f1Till MossakowskiStatic analysis of DOL documents and CASL specification libraries
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski Follows the verification semantics sketched in Chap. IV:6
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski of the CASL Reference Manual.
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu Follows the semantics of DOL documents, DOL OMG standard, clause 10.2.1
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder ( anaLibFileOrGetEnv
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , anaSourceFile
fa1efeb55163f27f261d22a9062fbc25ab4d8d52Michael Chan , anaLibItem
fa1efeb55163f27f261d22a9062fbc25ab4d8d52Michael Chan , anaViewDefn
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maederimport Static.ArchDiagram (emptyExtStUnitCtx)
9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettichimport Common.AS_Annotation hiding (isAxiom, isDef)
1b9ecb3b9c41106d0c90dcdb731b360eb5240c33Christian Maederimport qualified Common.Unlit as Unlit
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport qualified Data.Map as Map
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maederimport qualified Data.Set as Set
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulzeimport Data.Either (lefts, rights)
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder-- a set of library names to check for cyclic imports
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maedertype LNS = Set.Set LibName
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder{- | parsing and static analysis for files
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian MaederParameters: logic graph, default logic, file name -}
a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian MaederanaSourceFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder -> FilePath -> ResultT IO (LibName, LibEnv)
2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaederanaSourceFile = anaSource Nothing
2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaederanaSource :: Maybe LibName -- ^ suggested library name
2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder -> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder -> FilePath -> ResultT IO (LibName, LibEnv)
ffd2214759f0055aa5dfa95583a6060516ad766fChristian MaederanaSource mln lg opts topLns libenv initDG origName = ResultT $ do
c557355ae6efec37e229b26cb11ee12ad4c2de31Christian Maeder let mName = useCatalogURL opts origName
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa fname = tryToStripPrefix "file://" mName
70e5d1e7199cc22d75e5f3498a7cc851cade9a5dChristian Maeder syn = case defSyntax opts of
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder "" -> Nothing
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder s -> Just $ simpleIdToIRI $ mkSimpleId s
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder lgraph = setSyntax syn $ setCurLogic (defLogic opts) lg
fb9ec1e4dd1877781ec2b491fb0a6bcd38a7b04dcmaeder fname' <- getContentAndFileType opts fname
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa dir <- getCurrentDirectory
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski case fname' of
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder Left err -> return $ fail err
2ccdb81b4018e0a76f6dad3a940ba1241e98f6d9cmaeder Right (mr, _, file, inputLit) ->
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder if any (`isSuffixOf` file) [envSuffix, prfSuffix] then
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder return . fail $ "no matching source file for '" ++ fname ++ "' found."
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder input = (if unlit opts then Unlit.unlit else id) inputLit
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder libStr = if isAbsolute fname
94c729aeac99df6d844da014f46d584c035a91a6Christian Maeder then convertFileToLibStr fname
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder else dropExtensions fname
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder nLn = case mln of
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder Nothing | useLibPos opts && not (checkUri fname) ->
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder Just $ emptyLibName libStr
f448ac6b7846addfe6041275edf1fb90962e76eacmaeder fn2 = keepOrigClifName opts origName file
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa fnAbs = if isAbsolute fn2 then fn2 else dir </> fn2
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa url = if checkUri fn2 then fn2 else "file://" ++ fnAbs
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder if runMMT opts then mmtRes fname else
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder if takeExtension file /= ('.' : show TwelfIn)
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder then runResultT $
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa anaString nLn lgraph opts topLns libenv initDG input url mr
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder res <- anaTwelfFile opts file
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder return $ case res of
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder Nothing -> fail $ "failed to analyse file: " ++ file
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder Just (lname, lenv) -> return (lname, Map.union lenv libenv)
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaeder-- | parsing of input string (content of file)
2a0562f417902e59161fe6a2173fdc8aa3877616Christian MaederanaString :: Maybe LibName -- ^ suggested library name
2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder -> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> String
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaeder -> FilePath -> Maybe String -- ^ mime-type of file
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaeder -> ResultT IO (LibName, LibEnv)
6f70475dddc12732bdbef3e3dd116373e34cd6b9Christian MaederanaString mln lgraph opts topLns libenv initDG input file mr = do
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder curDir <- lift getCurrentDirectory -- get full path for parser positions
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder let realFileName = curDir </> file
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder posFileName = case mln of
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder Just gLn | useLibPos opts -> libToFileName gLn
acc358348c23ba8b7a0c58aff12c49c947b01825Christian Maeder _ -> if checkUri file then file else realFileName
ffd2214759f0055aa5dfa95583a6060516ad766fChristian Maeder lift $ putIfVerbose opts 2 $ "Reading file " ++ file
6f70475dddc12732bdbef3e3dd116373e34cd6b9Christian Maeder libdefns <- readLibDefn lgraph opts mr file posFileName input
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder when (null libdefns) . fail $ "failed to read contents of file: " ++ file
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaeder foldM (anaStringAux mln lgraph opts topLns initDG mr file posFileName)
74be884c1e3c3a9b0bace45a482a9030065b7ab4cmaeder $ case analysis opts of
74be884c1e3c3a9b0bace45a482a9030065b7ab4cmaeder Skip -> [last libdefns]
74be884c1e3c3a9b0bace45a482a9030065b7ab4cmaeder _ -> libdefns
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaeder-- | calling static analysis for parsed library-defn
966ad5a92ae6faa736f7abd8aff54aa239037f0aTill MossakowskianaStringAux :: Maybe LibName -- ^ suggested library name
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaeder -> LogicGraph -> HetcatsOpts -> LNS -> DGraph -> Maybe String -> FilePath
966ad5a92ae6faa736f7abd8aff54aa239037f0aTill Mossakowski -> FilePath -> (LibName, LibEnv) -> LIB_DEFN -> ResultT IO (LibName, LibEnv)
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaederanaStringAux mln lgraph opts topLns initDG mt file posFileName (_, libenv)
80083e5c815823405eed7c5a7f4db30d0512223fChristian Maeder (Lib_defn pln is' ps ans) = do
a6ebae9cdcee5b4f6388f3493295fe6b740a728dChristian Maeder let pm = fst $ partPrefixes ans
a6ebae9cdcee5b4f6388f3493295fe6b740a728dChristian Maeder expnd i = fromMaybe i $ expandCurie pm i
a6ebae9cdcee5b4f6388f3493295fe6b740a728dChristian Maeder spNs = Set.unions . map (Set.map expnd . getSpecNames)
8c777006135f9191933250b9ebd78c514781b1d6Christian Maeder $ concatMap (getSpecDef . item) is'
a6ebae9cdcee5b4f6388f3493295fe6b740a728dChristian Maeder declNs = Set.fromList . map expnd
a6ebae9cdcee5b4f6388f3493295fe6b740a728dChristian Maeder $ concatMap (getDeclSpecNames . item) is'
5d3a79579335f02a578cec84a622e1b6fabdab44Christian Maeder missNames = Set.toList $ spNs Set.\\ declNs
5d3a79579335f02a578cec84a622e1b6fabdab44Christian Maeder unDecls = map (addDownload True) $ filter
5d3a79579335f02a578cec84a622e1b6fabdab44Christian Maeder (isNothing . (`lookupGlobalEnvDG` initDG)) missNames
80083e5c815823405eed7c5a7f4db30d0512223fChristian Maeder is = unDecls ++ is'
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz spN = convertFileToLibStr file
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder noLibName = getLibId pln == nullIRI
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz nIs = case is of
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz [Annoted (Spec_defn spn gn as qs) rs [] []]
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa | noLibName && null (iriToStringUnsecure spn)
b47b9b7b9d177e7b48e74998082de5f0d3943255Christian Maeder -> [Annoted (Spec_defn (simpleIdToIRI $ mkSimpleId spN)
b47b9b7b9d177e7b48e74998082de5f0d3943255Christian Maeder gn as qs) rs [] []]
32c38acfa0f8c8032f829cd8fa83fdb1d8e5e581Christian Maeder emptyFilePath = null $ getFilePath pln
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaeder ln = setMimeType mt $ if emptyFilePath then setFilePath posFileName
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa $ if noLibName then fromMaybe (emptyLibName spN) mln else pln
b47b9b7b9d177e7b48e74998082de5f0d3943255Christian Maeder ast = Lib_defn ln nIs ps ans
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz case analysis opts of
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder lift $ putIfVerbose opts 1 $
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder "Skipping static analysis of library " ++ show ln
b47b9b7b9d177e7b48e74998082de5f0d3943255Christian Maeder ga <- liftR $ addGlobalAnnos emptyGlobalAnnos ans
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder lift $ writeLibDefn lgraph ga file opts ast
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder let libstring = libToFileName ln
6ffe605966ec108478dbb5278fbfa96d92f5abdfChristian Maeder unless (isSuffixOf libstring (dropExtension file)
18e43e29918ad49367b18340d6d0731636a54242Christian Maeder || not emptyFilePath) . lift . putIfVerbose opts 1
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa $ "### file name '" ++ file ++ "' does not match library name '"
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa ++ libstring ++ "'"
55e1458efb5b53c71df7d3263f5d7fae04503619Christian Maeder lift $ putIfVerbose opts 1 $ "Analyzing "
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa ++ (if noLibName then "file " ++ file ++ " as " else "")
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa ++ "library " ++ show ln
d6845258c75f903bb4dcc228077a68bb648e1597Christian Maeder (lnFinal, ld, ga, lenv) <-
e167a3665dac3fca4313bb76ee5b1a04f8e5b266Christian Maeder anaLibDefn lgraph opts topLns libenv initDG ast file
d6845258c75f903bb4dcc228077a68bb648e1597Christian Maeder case Map.lookup lnFinal lenv of
d6845258c75f903bb4dcc228077a68bb648e1597Christian Maeder Nothing -> error $ "anaString: missing library: " ++ show lnFinal
2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder Just dg -> lift $ do
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder writeLibDefn lgraph ga file opts ld
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder when (hasEnvOut opts)
d6845258c75f903bb4dcc228077a68bb648e1597Christian Maeder (writeFileInfo opts lnFinal file ld dg)
d6845258c75f903bb4dcc228077a68bb648e1597Christian Maeder return (lnFinal, lenv)
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder-- lookup or read a library
a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian MaederanaLibFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LibName
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder -> ResultT IO (LibName, LibEnv)
a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian MaederanaLibFile lgraph opts topLns libenv initDG ln =
966b9e5b583d3a4986e7fe05c0e5e49c8566c39eChristian Maeder let lnstr = show ln in case find (== ln) $ Map.keys libenv of
966b9e5b583d3a4986e7fe05c0e5e49c8566c39eChristian Maeder Just ln' -> do
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder analyzing opts $ "from " ++ lnstr
966b9e5b583d3a4986e7fe05c0e5e49c8566c39eChristian Maeder return (ln', libenv)
bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder putMessageIORes opts 1 $ "Downloading " ++ lnstr ++ " ..."
bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder res <- anaLibFileOrGetEnv lgraph
44afe69b6b3cc7314ef270e125196127777c6c87Christian Maeder (if recurse opts then opts else opts
44afe69b6b3cc7314ef270e125196127777c6c87Christian Maeder { outtypes = []
44afe69b6b3cc7314ef270e125196127777c6c87Christian Maeder , unlit = False })
d0cc19953154042415f3a85ada1c905397884936Christian Maeder (Set.insert ln topLns) libenv initDG (Just ln) $ libNameToFile ln
bcd35fcdda4233c42766519772b2e9fbab57f975Christian Maeder putMessageIORes opts 1 $ "... loaded " ++ lnstr
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder-- | lookup or read a library
a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian MaederanaLibFileOrGetEnv :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
d0cc19953154042415f3a85ada1c905397884936Christian Maeder -> Maybe LibName -> FilePath -> ResultT IO (LibName, LibEnv)
2a9702a373738717c83824512bd9389b5870fc92Christian MaederanaLibFileOrGetEnv lgraph opts topLns libenv initDG mln file = do
be8b8876edf3d7138ddd39a4ec07d857dde5bbb5Christian Maeder let envFile = rmSuffix file ++ envSuffix
d0cc19953154042415f3a85ada1c905397884936Christian Maeder recent_envFile <- lift $ checkRecentEnv opts envFile file
be8b8876edf3d7138ddd39a4ec07d857dde5bbb5Christian Maeder if recent_envFile
2a9702a373738717c83824512bd9389b5870fc92Christian Maeder mgc <- lift $ readVerbose lgraph opts mln envFile
d0cc19953154042415f3a85ada1c905397884936Christian Maeder Nothing -> do
be8b8876edf3d7138ddd39a4ec07d857dde5bbb5Christian Maeder lift $ putIfVerbose opts 1 $ "Deleting " ++ envFile
a55b09f4ef6e58ad617b59899d93c63bb4d6f287Christian Maeder lift $ removeFile envFile
d0cc19953154042415f3a85ada1c905397884936Christian Maeder anaSource mln lgraph opts topLns libenv initDG file
2a9702a373738717c83824512bd9389b5870fc92Christian Maeder Just (ld@(Lib_defn ln _ _ _), gc) -> do
d0cc19953154042415f3a85ada1c905397884936Christian Maeder lift $ writeLibDefn lgraph (globalAnnos gc) file opts ld
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -- get all DGRefs from DGraph
d0cc19953154042415f3a85ada1c905397884936Christian Maeder mEnv <- foldl
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder ( \ ioLibEnv labOfDG -> let node = snd labOfDG in
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder if isDGRef node then do
2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder let ln2 = dgn_libname node
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder p_libEnv <- ioLibEnv
2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder if Map.member ln2 p_libEnv then
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder return p_libEnv
4b0e0613129ebfc53e3e87985c20a537da91d18dChristian Maeder else fmap snd $ anaLibFile lgraph
2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder opts topLns p_libEnv initDG ln2
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder else ioLibEnv)
2a0562f417902e59161fe6a2173fdc8aa3877616Christian Maeder (return $ Map.insert ln gc libenv)
2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder $ labNodesDG gc
d0cc19953154042415f3a85ada1c905397884936Christian Maeder return (ln, mEnv)
d0cc19953154042415f3a85ada1c905397884936Christian Maeder else anaSource mln lgraph opts topLns libenv initDG file
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder{- | analyze a LIB_DEFN.
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder Parameters: logic graph, default logic, opts, library env, LIB_DEFN.
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder Call this function as follows:
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder> do Result diags res <- runResultT (anaLibDefn ...)
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder> mapM_ (putStrLn . show) diags
a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian MaederanaLibDefn :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LIB_DEFN
ff0845ce4591e851711953d8d613022764ef6cc7Eugen Kuksa -> FilePath -> ResultT IO (LibName, LIB_DEFN, GlobalAnnos, LibEnv)
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. SchulzeanaLibDefn lgraph opts topLns libenv dg (Lib_defn ln alibItems pos ans) file
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder let libStr = libToFileName ln
3498df662e47578110a1c0c08834fff054bc8878Christian Maeder isDOLlib = elem ':' libStr
3498df662e47578110a1c0c08834fff054bc8878Christian Maeder gannos <- showDiags1 opts $ liftR $ addGlobalAnnos
3498df662e47578110a1c0c08834fff054bc8878Christian Maeder (defPrefixGlobalAnnos $ if isDOLlib then file else libStr) ans
e3e5a829ebb586d49f580ae14b15d55ec3d766d9Christian Maeder allAnnos <- liftR $ mergeGlobalAnnos (globalAnnos dg) gannos
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder (libItems', dg', libenv', _, _) <- foldM (anaLibItemAux opts topLns ln)
9c72712d9d512b0f48146a299ccf80c1de325e5aChristian Maeder ([], dg { globalAnnos = allAnnos }, libenv
7242e6bea0919135c6ef667c118ad3f47c023b46Christian Maeder , lgraph, Map.empty) (map item alibItems)
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu let dg1 = computeDGraphTheories libenv' ln $ markFree libenv'
117a0f03fb483fc6d8ad4fb39cf2d142187c8e2fmscodescu $ markHiding libenv' $ fromMaybe dg' $ maybeResult
117a0f03fb483fc6d8ad4fb39cf2d142187c8e2fmscodescu $ shortcutUnions dg'
df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder newLD = Lib_defn ln
df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder (zipWith replaceAnnoted (reverse libItems') alibItems) pos ans
df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder dg2 = dg1 { optLibDefn = Just newLD }
8d60e45ae6ee598d910c5c85eba70c5500d7f519mscodescu return (ln, newLD, globalAnnos dg2, Map.insert ln dg2 libenv')
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian MaedershortcutUnions :: DGraph -> Result DGraph
c246854fd9abd0cdb3d11a52a350ebad2fbaa09bChristian MaedershortcutUnions dgraph = let spNs = getGlobNodes $ globalEnv dgraph in
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder foldM (\ dg (n, nl) -> let
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder locTh = dgn_theory nl
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder innNs = innDG dg n
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder in case outDG dg n of
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder [(_, t, et@DGLink {dgl_type = lt})]
64d8c3cace7c7a6bc3d862c4afc2628bcd54a3bfChristian Maeder | Set.notMember n spNs && null (getThSens locTh) && isGlobalDef lt
85e47ae3b5dc43834dd9b10af3bd42ca2e10fc88mscodescu && not (hasOutgoingFreeEdge dg t)
64d8c3cace7c7a6bc3d862c4afc2628bcd54a3bfChristian Maeder && length innNs > 1
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder && all (\ (_, _, el) -> case dgl_type el of
64d8c3cace7c7a6bc3d862c4afc2628bcd54a3bfChristian Maeder ScopedLink Global DefLink (ConsStatus cs None LeftOpen)
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder | cs == getCons lt -> True
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder _ -> False) innNs
ff42a5cc0c7e80d095b6c0488ef97df36f148a06Christian Maeder && case nodeInfo nl of
ff42a5cc0c7e80d095b6c0488ef97df36f148a06Christian Maeder DGNode DGUnion _ -> True
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder -> foldM (\ dg' (s, _, el) -> do
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder newMor <- composeMorphisms (dgl_morphism el) $ dgl_morphism et
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder return $ insLink dg' newMor
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder (dgl_type el) (dgl_origin el) s t) (delNodeDG n dg) innNs
e0c1a78a8e0075253d2df7f3a7da7d0e1fc258e7Christian Maeder _ -> return dg) dgraph $ topsortedNodes dgraph
ff0845ce4591e851711953d8d613022764ef6cc7Eugen KuksadefPrefixGlobalAnnos :: FilePath -> GlobalAnnos
63ba2f828c63eb66506bc014b24a87adf97ae950Christian MaederdefPrefixGlobalAnnos file = emptyGlobalAnnos
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder { prefix_map = Map.singleton ""
be7add16c3f4e230929bcb948a67a710c6a4d222Christian Maeder $ fromMaybe nullIRI $ parseIRIReference $ file ++ "?" }
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian MaederanaLibItemAux :: HetcatsOpts -> LNS -> LibName
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder -> ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides) -> LIB_ITEM
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder -> ResultT IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian MaederanaLibItemAux opts topLns ln q@(libItems', dg1, libenv1, lg, eo) libItem = let
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder currLog = currentLogic lg
78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder newOpts = if elem currLog ["DMU", "Framework"] then
78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder opts { defLogic = currLog } else opts
78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder in ResultT $ do
78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder res2@(Result diags2 res) <- runResultT
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder $ anaLibItem lg newOpts topLns ln libenv1 dg1 eo libItem
78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder runResultT $ showDiags1 opts (liftR res2)
4b0e0613129ebfc53e3e87985c20a537da91d18dChristian Maeder let mRes = case res of
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa Just (libItem', dg1', libenv1', newLG, eo') ->
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa Just (libItem' : libItems', dg1', libenv1', newLG, eo')
aeb4e74b8b3328d8ea15512ec4e1e1b8d0919f01Christian Maeder Nothing -> Just q
78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder if outputToStdout opts then
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder if hasErrors diags2 then
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder fail "Stopped due to errors"
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder else runResultT $ liftR $ Result [] mRes
78efc385d85998e49a363929b2d1016e37835b6dChristian Maeder else runResultT $ liftR $ Result diags2 mRes
7f7460e7095628f3437b116ee78d3043d11f8febChristian MaederputMessageIORes :: HetcatsOpts -> Int -> String -> ResultT IO ()
948f37fdb71c544ff4c907bc5863702648cf36e4Christian MaederputMessageIORes opts i msg =
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder if outputToStdout opts
1e3950d5c1f0e041dd7677856e43f07796567d5bChristian Maeder then lift $ putIfVerbose opts i msg
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder else liftR $ message () msg
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maederanalyzing :: HetcatsOpts -> String -> ResultT IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maederanalyzing opts = putMessageIORes opts 1 . ("Analyzing " ++)
1e3950d5c1f0e041dd7677856e43f07796567d5bChristian MaederalreadyDefined :: String -> String
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian MaederalreadyDefined str = "Name " ++ str ++ " already defined"
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder-- | analyze a GENERICITY
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaGenericity :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder -> ExpOverrides -> NodeName -> GENERICITY
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder -> Result (GENERICITY, GenSig, DGraph)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaGenericity lg libEnv ln dg opts eo name
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder gen@(Genericity (Params psps) (Imported isps) pos) =
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder let ms = currentBaseTheory dg in
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder adjustPos pos $ case psps of
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder [] -> do -- no parameter ...
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder unless (null isps) $ plain_error ()
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder "Parameterless specifications must not have imports" pos
1f315f2e146d15c0aec01f7ae076708bbac29796Christian Maeder l <- lookupCurrentLogic "GENERICITY" lg
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder return (gen, GenSig (EmptyNode l) []
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder $ maybe (EmptyNode l) JustNode ms, dg)
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder l <- lookupCurrentLogic "IMPORTS" lg
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder let baseNode = maybe (EmptyNode l) JustNode ms
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder (imps', nsigI, dg') <- case isps of
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder [] -> return ([], baseNode, dg)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (is', _, nsig', dgI) <- anaUnion False lg libEnv ln dg baseNode
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder (extName "Imports" name) opts eo isps $ getRange isps
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder return (is', JustNode nsig', dgI)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (ps', nsigPs, ns, dg'') <- anaUnion False lg libEnv ln dg' nsigI
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder (extName "Parameters" name) opts eo psps $ getRange psps
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder return (Genericity (Params ps') (Imported imps') pos,
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder GenSig nsigI nsigPs $ JustNode ns, dg'')
818fb3d880eaabc835456d7344945c80f97cee9cChristian MaederexpCurieT :: GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
818fb3d880eaabc835456d7344945c80f97cee9cChristian MaederexpCurieT ga eo = liftR . expCurieR ga eo
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder-- | analyse a LIB_ITEM
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaLibItem :: LogicGraph -> HetcatsOpts -> LNS -> LibName -> LibEnv -> DGraph
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder -> ExpOverrides -> LIB_ITEM
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian MaederanaLibItem lg opts topLns currLn libenv dg eo itm =
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder Spec_defn spn2 gen asp pos -> do
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder let spn' = if null (iriToStringUnsecure spn2) then
eac68e99c56a3e8f240d455cff5380eeca9ef165Christian Maeder simpleIdToIRI $ mkSimpleId "Spec" else spn2
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder spn <- expCurieT (globalAnnos dg) eo spn'
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa let spstr = iriToStringUnsecure spn
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder nName = makeName spn
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder analyzing opts $ "spec " ++ spstr
54d25074b7ddc5534322f0627e54a51e66568c14Christian Maeder (gen', gsig@(GenSig _ _args allparams), dg') <-
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu liftR $ anaGenericity lg libenv currLn dg opts eo nName gen
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder (sanno1, impliesA) <- liftR $ getSpecAnnos pos asp
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder when impliesA $ liftR $ plain_error ()
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa "unexpected initial %implies in spec-defn" pos
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder (sp', body, dg'') <-
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu liftR (anaSpecTop sanno1 True lg libenv currLn dg'
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder allparams nName opts eo (item asp) pos)
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder genv = globalEnv dg
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa then liftR $ plain_error (libItem', dg'', libenv, lg, eo)
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa (alreadyDefined spstr) pos
54d25074b7ddc5534322f0627e54a51e66568c14Christian Maeder -- let (_n, dg''') = addSpecNodeRT dg'' (UnitSig args body) $ show spn
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa , dg'' { globalEnv = Map.insert spn (SpecEntry
28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu $ ExtGenSig gsig body) genv }
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa , libenv, lg, eo)
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu Entail_defn en' etype pos -> do
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu en <- expCurieT (globalAnnos dg) eo en'
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu analyzing opts $ "entailment " ++ iriToStringUnsecure en
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu liftR $ anaEntailmentDefn lg currLn libenv dg opts eo en etype pos
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder View_defn vn' gen vt gsis pos -> do
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder vn <- expCurieT (globalAnnos dg) eo vn'
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa analyzing opts $ "view " ++ iriToStringUnsecure vn
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder liftR $ anaViewDefn lg currLn libenv dg opts eo vn gen vt gsis pos
5fee2261e6cd08951dadfa48df5cdd1641b671a8cmaeder Align_defn an' arities atype acorresps _ pos -> do
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder an <- expCurieT (globalAnnos dg) eo an'
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder analyzing opts $ "alignment " ++ iriToStringUnsecure an
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder anaAlignDefn lg currLn libenv dg opts eo an arities atype acorresps pos
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder Arch_spec_defn asn' asp pos -> do
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder asn <- expCurieT (globalAnnos dg) eo asn'
55b14de0878c596dc00920ecac65bab478e930e8Christian Maeder let asstr = iriToStringUnsecure asn
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder analyzing opts $ "arch spec " ++ asstr
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (_, _, diag, archSig, dg', asp') <- liftR $ anaArchSpec lg libenv currLn dg
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder opts eo emptyExtStUnitCtx Nothing $ item asp
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder let asd' = Arch_spec_defn asn (replaceAnnoted asp' asp) pos
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder genv = globalEnv dg'
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa then liftR $ plain_error (asd', dg', libenv, lg, eo)
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (alreadyDefined asstr) pos
87ad371ce86a15cd4424f59fa2fb8393f496cca4Mihai Codescu let aName = show asn
87ad371ce86a15cd4424f59fa2fb8393f496cca4Mihai Codescu dg'' = updateNodeNameRT dg'
1fac2740f74f98ed96b78abce2370edbd03065a5Christian Maeder (refSource $ getPointerFromRef archSig)
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder dg3 = dg'' { archSpecDiags =
23a0c19ea8d6075fc765c64a20c70b119434823aMihai Codescu $ archSpecDiags dg''}
54d25074b7ddc5534322f0627e54a51e66568c14Christian Maeder return (asd', dg3
55b14de0878c596dc00920ecac65bab478e930e8Christian Maeder { globalEnv = Map.insert asn
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder (ArchOrRefEntry True archSig) genv }
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa , libenv, lg, eo)
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder Unit_spec_defn usn' usp pos -> do
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder usn <- expCurieT (globalAnnos dg) eo usn'
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa let usstr = iriToStringUnsecure usn
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder analyzing opts $ "unit spec " ++ usstr
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder l <- lookupCurrentLogic "Unit_spec_defn" lg
28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu (rSig, dg', usp') <-
641a7885e8424e92967525dd3886ef307cfcbcd6mcodescu liftR $ anaUnitSpec lg libenv currLn dg opts eo
641a7885e8424e92967525dd3886ef307cfcbcd6mcodescu usn' (EmptyNode l) Nothing usp
28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu unitSig <- liftR $ getUnitSigFromRef rSig
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder let usd' = Unit_spec_defn usn usp' pos
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder genv = globalEnv dg'
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa then liftR $ plain_error (itm, dg', libenv, lg, eo)
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (alreadyDefined usstr) pos
ddd8734e5b3802a1a6c908af6b1e870af76c932dChristian Maeder else return (usd', dg'
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder { globalEnv = Map.insert usn (UnitEntry unitSig) genv },
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa libenv, lg, eo)
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder Ref_spec_defn rn' rsp pos -> do
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder rn <- expCurieT (globalAnnos dg) eo rn'
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa let rnstr = iriToStringUnsecure rn
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder l <- lookupCurrentLogic "Ref_spec_defn" lg
7ce79f9759f3d4b9c0483e42b7420b94cbdd7086mcodescu (_, _, _, rsig, dg', rsp') <- liftR $
7ce79f9759f3d4b9c0483e42b7420b94cbdd7086mcodescu anaRefSpec True lg libenv currLn dg opts eo
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (EmptyNode l) rn emptyExtStUnitCtx Nothing rsp
28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu analyzing opts $ "ref spec " ++ rnstr
28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu let rsd' = Ref_spec_defn rn rsp' pos
28cbeb7eb61216d3b5a27dca176333d1ff8d3357Mihai Codescu genv = globalEnv dg'
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa then liftR $ plain_error (itm, dg', libenv, lg, eo)
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (alreadyDefined rnstr) pos
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder else return ( rsd', dg'
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder { globalEnv = Map.insert rn (ArchOrRefEntry False rsig) genv }
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa , libenv, lg, eo)
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze Logic_decl logN pos -> do
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder putMessageIORes opts 1 . show $ prettyLG lg itm
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder (mth, newLg) <- liftR
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder $ adjustPos pos $ anaSublogic opts logN currLn dg libenv lg
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder return (itm, dg { currentBaseTheory = Nothing }, libenv, newLg, eo)
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder Just (s, (libName, refDG, (_, lbl))) -> do
c36a0ff8c61927b9654efa7b6319ba1d72a8abbdChristian Maeder -- store th-lbl in newDG
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder let dg2 = if libName /= currLn then
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder let (s2, (genv, newDG)) = refExtsigAndInsert libenv libName refDG
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder (globalEnv dg, dg) (getName $ dgn_name lbl) s
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder in newDG { globalEnv = genv
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder , currentBaseTheory = Just $ extGenBody s2 }
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder else dg { currentBaseTheory = Just $ extGenBody s }
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa return (itm, dg2, libenv, newLg, eo)
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu Network_defn anIri (Network cItems eItems _) pos -> do
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu nn <- expCurieT (globalAnnos dg) eo anIri
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu let nnstr = iriToStringUnsecure nn
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu analyzing opts $ "network " ++ nnstr
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu let (cNodes, cEdges) = networkDiagram dg cItems eItems
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu diag = makeDiagram dg cNodes cEdges
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu genv = globalEnv dg
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu liftR $ plain_error (itm, dg, libenv, lg, eo)
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu (alreadyDefined nnstr) pos
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu return (itm, dg{globalEnv = Map.insert nn (NetworkEntry diag) genv},
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu libenv, lg, eo)
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze Download_items ln items pos ->
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa if Set.member ln topLns then
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa liftR $ mkError "illegal cyclic library import"
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa $ Set.map getLibId topLns
2a7671a774095bfc1e5a6f34a298dbe8b5947394cmaeder let newOpts = opts { intype = GuessIn }
2a7671a774095bfc1e5a6f34a298dbe8b5947394cmaeder (ln', libenv') <- anaLibFile lg newOpts topLns libenv
1f5065a59c38b9f9794c45b6174027fe8e007943Christian Maeder (cpIndexMaps dg emptyDG { globalAnnos =
1f5065a59c38b9f9794c45b6174027fe8e007943Christian Maeder emptyGlobalAnnos { prefix_map = prefix_map $ globalAnnos dg }}) ln
1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder unless (ln == ln')
1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder $ liftR $ warning ()
1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder (shows ln " does not match internal name " ++ shows ln' "")
1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder case Map.lookup ln' libenv' of
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder Nothing -> error $ "Internal error: did not find library "
1f2332c370e11e77b36718b96d05e2b180bb3bebChristian Maeder ++ show ln' ++ " available: " ++ show (Map.keys libenv')
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder Just dg' -> do
a2e1df1a654e9f683373245b6fbfc5f415842eb5Christian Maeder let dg0 = cpIndexMaps dg' dg
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder fn = libToFileName ln'
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder currFn = libToFileName currLn
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa (realItems, errs, origItems) = case items of
213d4ca73d95296397abc0d34dc91f5da648af60Christian Maeder ItemMaps rawIms ->
213d4ca73d95296397abc0d34dc91f5da648af60Christian Maeder let (ims, warns) = foldr (\ im@(ItemNameMap i mi)
213d4ca73d95296397abc0d34dc91f5da648af60Christian Maeder (is, ws) -> if Just i == mi then
213d4ca73d95296397abc0d34dc91f5da648af60Christian Maeder (ItemNameMap i Nothing : is
213d4ca73d95296397abc0d34dc91f5da648af60Christian Maeder , warning () (show i ++ " item no renamed")
213d4ca73d95296397abc0d34dc91f5da648af60Christian Maeder (getRange mi) : ws)
213d4ca73d95296397abc0d34dc91f5da648af60Christian Maeder else (im : is, ws)) ([], []) rawIms
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze expIms = map (expandCurieItemNameMap fn currFn) ims
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze leftExpIms = lefts expIms
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze in if not $ null leftExpIms
b5444dac524839f6e7c9b18fe497fe12dbd3d8edChristian Maeder then ([], leftExpIms, itemNameMapsToIRIs ims)
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze else (rights expIms, warns, itemNameMapsToIRIs ims)
ef39467deccce0e8a9d257a57030426d14d9b4d8cmaeder UniqueItem i ->
ef39467deccce0e8a9d257a57030426d14d9b4d8cmaeder let is = Map.keys $ globalEnv dg'
ef39467deccce0e8a9d257a57030426d14d9b4d8cmaeder ks = case is of
ef39467deccce0e8a9d257a57030426d14d9b4d8cmaeder _ -> filter (== getLibId ln') is
ef39467deccce0e8a9d257a57030426d14d9b4d8cmaeder in case ks of
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder [j] -> case expCurie (globalAnnos dg) eo i of
d9435c21e9292561d38b689c1a0e5ab52982277aChristian Maeder Nothing -> ([], [prefixErrorIRI i], [i])
3498df662e47578110a1c0c08834fff054bc8878Christian Maeder Just expI -> case expCurie (globalAnnos dg) eo j of
d9435c21e9292561d38b689c1a0e5ab52982277aChristian Maeder Nothing -> ([], [prefixErrorIRI j], [i, j])
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder ([ItemNameMap expJ (Just expI)], [], [i, j])
ef39467deccce0e8a9d257a57030426d14d9b4d8cmaeder , [ mkError ("non-unique name within imported library: "
a2108db5b55fb4ab98a45a2b5a296771bda0ed83cmaeder ++ intercalate ", " (map show is))
329f09824e0b9202d1327e52358912eddac8ad38Christian Maeder additionalEo = Map.fromList $ map (\ o -> (o, fn)) origItems
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder eo' = Map.unionWith (\ _ p2 -> p2) eo additionalEo
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder mapM_ liftR errs
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder dg1 <- liftR $ anaItemNamesOrMaps libenv' ln' dg' dg0 realItems
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa return (itm, dg1, libenv', lg, eo')
c35969f341eb137848e9c0874503bed8c419cbd2Kristina Sojakova Newlogic_defn ld _ -> ResultT $ do
c35969f341eb137848e9c0874503bed8c419cbd2Kristina Sojakova dg' <- anaLogicDef ld dg
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa return $ Result [] $ Just (itm, dg', libenv, lg, eo)
429b8f515a133b86a5771f8d8f6a71a15a70a315Iulia Ignatov Newcomorphism_defn com _ -> ResultT $ do
429b8f515a133b86a5771f8d8f6a71a15a70a315Iulia Ignatov dg' <- anaComorphismDef com dg
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa return $ Result [] $ Just (itm, dg', libenv, lg, eo)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder _ -> return (itm, dg, libenv, lg, eo)
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian MaedersymbolsOf :: LogicGraph -> G_sign -> G_sign -> [CORRESPONDENCE]
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder -> Result (Set.Set (G_symbol, G_symbol))
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian MaedersymbolsOf lg gs1@(G_sign l1 (ExtSign sig1 sys1) _)
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder gs2@(G_sign l2 (ExtSign sig2 sys2) _) corresps =
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder case corresps of
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder c : corresps' -> case c of
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder Default_correspondence -> symbolsOf lg gs1 gs2 corresps' -- TO DO
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder Correspondence_block _ _ cs -> do
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder sPs1 <- symbolsOf lg gs1 gs2 cs
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder sPs2 <- symbolsOf lg gs1 gs2 corresps'
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder return $ Set.union sPs1 sPs2
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder Single_correspondence _ (G_symb_items_list lid1 sis1)
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder (G_symb_items_list lid2 sis2) _ _ -> do
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder ss1 <- coerceSymbItemsList lid1 l1 "symbolsOf1" sis1
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder rs1 <- stat_symb_items l1 sig1 ss1
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu ss2 <- coerceSymbItemsList lid2 l2 "symbolsOf2" sis2
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder rs2 <- stat_symb_items l2 sig2 ss2
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder p <- case (rs1, rs2) of
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu ([r1], [r2]) ->
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder ( filter (\ sy -> matches l1 sy r1) $ Set.toList sys1
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder , filter (\ sy -> matches l2 sy r2) $ Set.toList sys2) of
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder ([s1], [s2]) ->
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder return (G_symbol l1 s1, G_symbol l2 s2)
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu (ll1, ll2) ->
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu plain_error (G_symbol l1 $ head ll1, G_symbol l2 $ head ll2) -- this is a hack!
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu ("Missing or non-unique symbol match " ++
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu "for correspondence\nMatches for first symbol: " ++
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu showDoc rs1 "\n" ++
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu showDoc ll1 "\nMatches for second symbol: " ++
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu showDoc rs2 "\n" ++
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu showDoc ll2 "\n")
9044adfd85e4d57a29ea3eefd73a973d36c862ddmcodescu _ -> fail $ "non-unique raw symbols"
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder ps <- symbolsOf lg gs1 gs2 corresps'
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu-- | analyse an entailment type
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu-- | analyse genericity and view type and construct gmorphism
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescuanaEntailmentDefn :: LogicGraph -> LibName -> LibEnv -> DGraph -> HetcatsOpts
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu -> ExpOverrides -> IRI -> ENTAIL_TYPE -> Range
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu -> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescuanaEntailmentDefn lg ln libEnv dg opts eo en et pos = do
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu Entail_type on1 on2 _ -> do
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu case (on1, on2) of
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu (MkOms asp1, MkOms asp2) -> do
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu let spS = item asp1
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu spT = item asp2
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu name = makeName en
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu l <- lookupCurrentLogic "ENTAIL_DEFN" lg
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (_spSrc', srcNsig, dg') <- anaSpec False True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg (EmptyNode l) (extName "Source" name)
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu opts eo spS $ getRange spS
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (_spTgt', tgtNsig, dg'') <- anaSpec True True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg' (EmptyNode l)
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu (extName "Target" name) opts eo spT $ getRange spT
d8fad841d8b6d97d423f2f2e24c3ceaf4c177b1bmcodescu incl <- ginclusion lg (getSig tgtNsig) (getSig srcNsig)
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu let dg3 = insLink dg'' incl globalThm SeeSource
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu (getNode tgtNsig) (getNode srcNsig)
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu gsig = GenSig (EmptyNode l) [] (EmptyNode l)
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu let vsig = ExtViewSig srcNsig incl $ ExtGenSig gsig tgtNsig
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu return (Entail_defn en et pos, dg3{
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu globalEnv = Map.insert en (ViewOrStructEntry True vsig)
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu $ globalEnv dg3},
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu libEnv, lg, eo)
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu _ -> fail "entailment between networks not supported yet"
81e837fb2b28d5fd25519b672e94fd4c705573b8mcodescu _ -> fail "omsinnetwork entailment not supported yet"
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder-- | analyse genericity and view type and construct gmorphism
acd4f79e6bf85f7596b30089e8c884560fad724bChristian MaederanaViewDefn :: LogicGraph -> LibName -> LibEnv -> DGraph -> HetcatsOpts
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -> ExpOverrides -> IRI -> GENERICITY -> VIEW_TYPE
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -> [G_mapping] -> Range
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian MaederanaViewDefn lg ln libenv dg opts eo vn gen vt gsis pos = do
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder let vName = makeName vn
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (gen', gsig@(GenSig _ _ allparams), dg') <-
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu anaGenericity lg libenv ln dg opts eo vName gen
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (vt', (src@(NodeSig nodeS gsigmaS)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder , tar@(NodeSig nodeT gsigmaT@(G_sign lidT _ _))), dg'') <-
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu anaViewType lg libenv ln dg' allparams opts eo vName vt
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder let genv = globalEnv dg''
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder then plain_error (View_defn vn gen' vt' gsis pos, dg'', libenv, lg, eo)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (alreadyDefined $ iriToStringUnsecure vn) pos
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder let (tsis, hsis) = partitionGmaps gsis
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (gsigmaS', tmor) <- if null tsis then do
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (gsigmaS', imor) <- gSigCoerce lg gsigmaS (Logic lidT)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder tmor <- gEmbedComorphism imor gsigmaS
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder return (gsigmaS', tmor)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder mor <- anaRenaming lg allparams gsigmaS opts (Renaming tsis pos)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder let gsigmaS'' = cod mor
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (gsigmaS', imor) <- gSigCoerce lg gsigmaS'' (Logic lidT)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder tmor <- gEmbedComorphism imor gsigmaS''
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder fmor <- comp mor tmor
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder return (gsigmaS', fmor)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder emor <- fmap gEmbed $ anaGmaps lg opts pos gsigmaS' gsigmaT hsis
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder gmor <- comp tmor emor
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder let vsig = ExtViewSig src gmor $ ExtGenSig gsig tar
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder voidView = nodeS == nodeT && isInclusion gmor
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder when voidView $ warning ()
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder ("identity mapping of source to same target for view: " ++
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder iriToStringUnsecure vn) pos
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder return (View_defn vn gen' vt' gsis pos,
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (if voidView then dg'' else insLink dg'' gmor globalThm
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (DGLinkView vn $ Fitted gsis) nodeS nodeT)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -- 'LeftOpen' for conserv correct?
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder { globalEnv = Map.insert vn (ViewOrStructEntry True vsig) genv }
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder , libenv, lg, eo)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder{- | analyze a VIEW_TYPE
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuThe first four arguments give the global context
acd4f79e6bf85f7596b30089e8c884560fad724bChristian MaederThe AnyLogic is the current logic
acd4f79e6bf85f7596b30089e8c884560fad724bChristian MaederThe NodeSig is the signature of the parameter of the view
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maederflag, whether just the structure shall be analysed -}
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaViewType :: LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> HetcatsOpts
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -> ExpOverrides
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -> NodeName -> VIEW_TYPE -> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaViewType lg libEnv ln dg parSig opts eo name (View_type aspSrc aspTar pos) = do
75927e7789d48f149b3ee62742253c508a80f4ccChristian Maeder -- trace "called anaViewType" $ do
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder l <- lookupCurrentLogic "VIEW_TYPE" lg
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder let spS = item aspSrc
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder spT = item aspTar
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (spSrc', srcNsig, dg') <- anaSpec False True lg libEnv ln dg (EmptyNode l)
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder (extName "Source" name) opts eo spS $ getRange spS
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (spTar', tarNsig, dg'') <- anaSpec True True lg libEnv ln dg' parSig
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder (extName "Target" name) opts eo spT $ getRange spT
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder return (View_type (replaceAnnoted spSrc' aspSrc)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (replaceAnnoted spTar' aspTar)
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (srcNsig, tarNsig), dg'')
acd4f79e6bf85f7596b30089e8c884560fad724bChristian MaederanaAlignDefn :: LogicGraph -> LibName -> LibEnv -> DGraph -> HetcatsOpts
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -> ExpOverrides -> IRI -> Maybe ALIGN_ARITIES -> VIEW_TYPE
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -> [CORRESPONDENCE] -> Range
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
34b91d5f66992fd04bfaad5076a21369c41448b3Christian MaederanaAlignDefn lg ln libenv dg opts eo an arities atype acorresps pos = do
9fe7f3d3fba58c1892ba8fea90b144eced88ca4fChristian Maeder l <- lookupCurrentLogic "Align_defn" lg
acd4f79e6bf85f7596b30089e8c884560fad724bChristian Maeder (atype', (src, tar), dg') <- liftR
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu $ anaViewType lg libenv ln dg (EmptyNode l) opts eo (makeName an) atype
a55ce02e3132df0dc1d865b6bd0dc09f5d9b9e82Christian Maeder let gsig1 = getSig src
a55ce02e3132df0dc1d865b6bd0dc09f5d9b9e82Christian Maeder gsig2 = getSig tar
a55ce02e3132df0dc1d865b6bd0dc09f5d9b9e82Christian Maeder case (gsig1, gsig2) of
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu (G_sign lid1 _ _, G_sign lid2 _ _) ->
818fb3d880eaabc835456d7344945c80f97cee9cChristian Maeder if Logic lid1 == Logic lid2 then do
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu -- arities TO DO
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder pairsSet <- liftR $ symbolsOf lg gsig1 gsig2 acorresps
0c5ae2bb1841d0efb4fa1fb55c510fd1ac0884fdChristian Maeder let leftList = map fst $ Set.toList pairsSet
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu rightList = map snd $ Set.toList pairsSet
a55ce02e3132df0dc1d865b6bd0dc09f5d9b9e82Christian Maeder isTotal gsig sList = Set.fromList sList == symsOfGsign gsig
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu isInjective sList = length sList == length (nub sList)
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu checkArity sList1 sList2 gsig arity = case arity of
731b0689c37481ff271c1cedddd76b941c32de05Christian Maeder AA_InjectiveAndTotal -> isTotal gsig sList1 &&
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu isInjective sList2
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu AA_Injective -> isInjective sList2
731b0689c37481ff271c1cedddd76b941c32de05Christian Maeder AA_Total -> isTotal gsig sList1
731b0689c37481ff271c1cedddd76b941c32de05Christian Maeder aCheck = case arities of
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu Nothing -> True
731b0689c37481ff271c1cedddd76b941c32de05Christian Maeder Just (Align_arities aleft aright) ->
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu checkArity leftList rightList gsig1 aleft &&
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu checkArity rightList leftList gsig2 aright
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu if not aCheck then
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder liftR $ mkError "Arities do not check" arities
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu newDg <- do
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu -- (A_source, A_target, A_bridge,
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- A_source -> O1, A_target -> O2)
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder (gt1, gt2, gt, gmor1, gmor2) <- liftR $
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu generateWAlign an gsig1 gsig2 acorresps
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- A_source
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu let n1 = getNewNodeDG dg'
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder labN1 = newInfoNodeLab
4037819986b425d49a61142750c5620ff1087d12mscodescu (makeName $ addSuffixToIRI "_source" an)
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder (newNodeInfo DGAlignment)
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu dg1 = insLNodeDG (n1, labN1) dg'
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- A_target
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu n2 = getNewNodeDG dg1
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder labN2 = newInfoNodeLab
4037819986b425d49a61142750c5620ff1087d12mscodescu (makeName $ addSuffixToIRI "_target" an)
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder (newNodeInfo DGAlignment)
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu dg2 = insLNodeDG (n2, labN2) dg1
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- A_bridge
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu n = getNewNodeDG dg2
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder labN = newInfoNodeLab
4037819986b425d49a61142750c5620ff1087d12mscodescu (makeName $ addSuffixToIRI "_bridge" an)
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder (newNodeInfo DGAlignment)
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu dg3 = insLNodeDG (n, labN) dg2
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- A_target-> O2
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder (_, dg4) = insLEdgeDG
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu (n2, getNode tar, globDefLink gmor2 $ DGLinkAlign an)
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu -- A_source -> O1
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder (_, dg5) = insLEdgeDG
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu (n1, getNode src, globDefLink gmor1 $ DGLinkAlign an)
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu -- inclusion of A_source in A_bridge
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu incl1 <- liftR $ ginclusion lg (signOf gt1) $ signOf gt
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- inclusion of A_target in A_bridge
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu incl2 <- liftR $ ginclusion lg (signOf gt2) $ signOf gt
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- add the inclusions to the dg
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu let (_, dg6) = insLEdgeDG
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu globDefLink incl1 $ DGLinkAlign an) dg5
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu (_, dg7) = insLEdgeDG
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder globDefLink incl2 $ DGLinkAlign an) dg6
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu -- store the alignment in the global env
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder asign = WAlign (NodeSig n1 $ signOf gt1) incl1 gmor1
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu (NodeSig n2 $ signOf gt2) incl2 gmor2
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu src tar (NodeSig n $ signOf gt)
75927e7789d48f149b3ee62742253c508a80f4ccChristian Maeder return dg7 {globalEnv = Map.insert an (AlignEntry asign)
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu $ globalEnv dg7}
5fee2261e6cd08951dadfa48df5cdd1641b671a8cmaeder let itm = Align_defn an arities atype' acorresps SingleDomain pos
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder anstr = iriToStringUnsecure an
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu if Map.member an $ globalEnv dg
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu then liftR $ plain_error (itm, dg, libenv, lg, eo)
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu (alreadyDefined anstr) pos
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu else return (itm, newDg, libenv, lg, eo)
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder else liftR $ fatal_error
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder ("Alignments only work between ontologies in the same logic\n"
34b91d5f66992fd04bfaad5076a21369c41448b3Christian Maeder ++ show (prettyLG lg atype)) pos
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescugenerateWAlign :: IRI -> G_sign -> G_sign -> [CORRESPONDENCE]
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu -> Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescugenerateWAlign an
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu (G_sign lid1 (ExtSign ssig _) _)
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu (G_sign lid2 (ExtSign tsig _) _)
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu tsig' <- coercePlainSign lid2 lid1 "coercePlainSign" tsig
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder -- 1. initialize
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu sig1 = empty_signature lid1
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu sig2 = empty_signature lid1
75927e7789d48f149b3ee62742253c508a80f4ccChristian Maeder sig = empty_signature lid1
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu -- 2. for each correspondence (e1,e2,r),
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- build the bridge ontology (s', sens')
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- the signatures s1'' and s2'' of the involved symbols
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- together with the maps (aname:e1 -> e1) and (aname:e2 -> e2)
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- This is done by corresp2th, in a logic dependent way.
36780327ef7de799210a7fdcfdb666a4cf3ce648mcodescu -- first we check if we must disambiguate names in the bridge ontology
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu let flag = let insNames aSet aLid aSItems = foldl (\s n -> Set.insert n s) aSet $
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu map (symb_items_name aLid) aSItems
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu (syms1, syms2) =
36780327ef7de799210a7fdcfdb666a4cf3ce648mcodescu foldl (\ (set1, set2) c -> case c of
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu Single_correspondence _ (G_symb_items_list lidS1 sitems1)
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu (G_symb_items_list lidS2 sitems2) _ _ ->
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu (insNames set1 lidS1 sitems1,
36780327ef7de799210a7fdcfdb666a4cf3ce648mcodescu insNames set2 lidS2 sitems2)
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu _ -> error "only single corrs")
36780327ef7de799210a7fdcfdb666a4cf3ce648mcodescu -- then we set a flag in addCorresp to True if disambiguation is needed
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder let addCorresp (s1, s2, s, sens, p1, p2) (G_symb_items_list lids1 l1,
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu G_symb_items_list lids2 l2, rrel) = do
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu l1' <- coerceSymbItemsList lids1 lid1 "coerceSymbItemsList" l1
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu l2' <- coerceSymbItemsList lids2 lid1 "coerceSymbItemsList" l2
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu (sigb, senb, s1', s2', eMap1, eMap2) <-
36780327ef7de799210a7fdcfdb666a4cf3ce648mcodescu corresp2th lid1 (iriToStringUnsecure an) flag
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu l1' l2' p1 p2 rrel
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu s1'' <- signature_union lid1 s1 s1'
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu s2'' <- signature_union lid1 s2 s2'
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu s' <- signature_union lid1 s sigb
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu let p1' = Map.union eMap1 p1
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu p2' = Map.union eMap2 p2
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu sens' = sens ++ senb
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu return (s1'', s2'', s', sens', p1', p2')
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu (sig1'', sig2'', sig'', sens'', sMap1, sMap2) <- foldM addCorresp
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu (sig1, sig2, sig, [], phi1, phi2) $
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu map (\c -> case c of
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu Single_correspondence _ s1 s2 (Just rref) _ ->
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu (s1, s2, refToRel rref)
2efe65dbd4bd6f3f2d22515523be169b9781fc86mcodescu _ -> error "only single correspondences for now")
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- 3. make G_ results
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- gth1 is A_source
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu let gth1 = noSensGTheory lid1 (mkExtSign sig1'') startSigId
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- gth2 is A_target
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu gth2 = noSensGTheory lid1 (mkExtSign sig2'') startSigId
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- gth is A_bridge
75927e7789d48f149b3ee62742253c508a80f4ccChristian Maeder gth = G_theory lid1 Nothing (mkExtSign sig'') startSigId
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu (toThSens sens'') startThId
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- prepare the maps for morphism generation
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder rsMap1 = Map.mapKeys (symbol_to_raw lid1) $
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu Map.map (symbol_to_raw lid1) sMap1
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder rsMap2 = Map.mapKeys (symbol_to_raw lid1) $
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu Map.map (symbol_to_raw lid1) sMap2
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- mor1 should go from A_source to O1: sig1'' to ssig
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder mor1 <- induced_from_to_morphism
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu lid1 rsMap1 (mkExtSign sig1'') (mkExtSign ssig)
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu let gmor1 = gEmbed2 (signOf gth1) $ mkG_morphism lid1 mor1
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu -- mor2 should go from A_target to O2: sig2'' to tsig'
75927e7789d48f149b3ee62742253c508a80f4ccChristian Maeder mor2 <- {- trace "mor2:" $
75927e7789d48f149b3ee62742253c508a80f4ccChristian Maeder trace ("source: " ++ (show sig2'')) $
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu trace ("target: " ++ (show tsig')) $ -}
f4fac4c564ea2067cdee2a76815ea72135b5f6caChristian Maeder induced_from_to_morphism
96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu lid1 rsMap2 (mkExtSign sig2'') (mkExtSign tsig')
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu let gmor2 = gEmbed2 (signOf gth2) $ mkG_morphism lid1 mor2
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu return (gth1, gth2, gth, gmor1, gmor2)
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder-- the first DGraph dg' is that of the imported library
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederanaItemNamesOrMaps :: LibEnv -> LibName -> DGraph -> DGraph
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder -> [ItemNameMap] -> Result DGraph
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederanaItemNamesOrMaps libenv' ln refDG dg items = do
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder (genv1, dg1) <- foldM
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (anaItemNameOrMap libenv' ln refDG) (globalEnv dg, dg) items
e204143b65ca66736dba0ad9561bba72b0497525Christian Maeder gannos'' <- mergeGlobalAnnos (globalAnnos refDG) $ globalAnnos dg
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder { globalAnnos = gannos''
54fb645be0a806e7fd3c0eed5691c2153eb8d518Christian Maeder , globalEnv = genv1 }
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederanaItemNameOrMap :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder -> ItemNameMap -> Result (GlobalEnv, DGraph)
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian MaederanaItemNameOrMap libenv ln refDG res (ItemNameMap old m) =
3fea26a73b8fa69b22dfd2653d8f7bdacb45b9c9Christian Maeder anaItemNameOrMap1 libenv ln refDG res (old, fromMaybe old m)
e5fae0f42a23c12fce5389f405659d4e5dce73a4Christian Maeder-- | Auxiliary function for not yet implemented features
16023c23c9d17743033afd994ad11c386d17b376Christian MaederanaErr :: String -> a
16023c23c9d17743033afd994ad11c386d17b376Christian MaederanaErr f = error $ "*** Analysis of " ++ f ++ " is not yet implemented!"
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederanaItemNameOrMap1 :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -> (IRI, IRI) -> Result (GlobalEnv, DGraph)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederanaItemNameOrMap1 libenv ln refDG (genv, dg) (old, new) = do
076d5429ce08d87ebced34c308d41225e0d12cdeChristian Maeder entry <- maybe (notFoundError "item" old) return
076d5429ce08d87ebced34c308d41225e0d12cdeChristian Maeder $ lookupGlobalEnvDG old refDG
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa maybeToResult (iriPos new) (iriToStringUnsecure new ++ " already used")
eb462c821104069a719090787f0f44793ba9a081Christian Maeder $ case Map.lookup new genv of
eb462c821104069a719090787f0f44793ba9a081Christian Maeder Nothing -> Just ()
eb462c821104069a719090787f0f44793ba9a081Christian Maeder Just _ -> Nothing
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case entry of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder SpecEntry extsig ->
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder return $ snd $ refExtsigAndInsert libenv ln refDG (genv, dg) new extsig
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder ViewOrStructEntry b vsig ->
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder let (dg1, vsig1) = refViewsig libenv ln refDG dg (makeName new) vsig
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder genv1 = Map.insert new (ViewOrStructEntry b vsig1) genv
e1a13f91fd3074f2e4b9c6fd1933787d2ad9e753Christian Maeder in return (genv1, dg1)
16023c23c9d17743033afd994ad11c386d17b376Christian Maeder UnitEntry _usig -> anaErr "unit spec download"
e4e39c9a78ab34bafd75b292839c20506e7f539bMihai Codescu AlignEntry _asig -> anaErr "alignment download"
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder ArchOrRefEntry b _rsig -> anaErr $ (if b then "arch" else "ref")
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder ++ " spec download"
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu NetworkEntry _gdiag -> anaErr "network download"
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederrefNodesig :: LibEnv -> LibName -> DGraph -> DGraph -> (NodeName, NodeSig)
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder -> (DGraph, NodeSig)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederrefNodesig libenv refln refDG dg
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (name, NodeSig refn sigma@(G_sign lid sig ind)) =
25ee45aee4dcd86c02a1e90d4c8d0438eed0ccf1Christian Maeder let (ln, _, (n, lbl)) =
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder lookupRefNode libenv refln refDG refn
84a30e66aef85cc54d3dd6f8e408729007fe8809Christian Maeder refInfo = newRefInfo ln n
cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maeder new = newInfoNodeLab name refInfo
cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maeder $ noSensGTheory lid sig ind
cc5f3c5391fbe9d1274e3a3afb1dc458bb424ba5Christian Maeder nodeCont = new { globalTheory = globalTheory lbl }
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg
84a30e66aef85cc54d3dd6f8e408729007fe8809Christian Maeder in case lookupInAllRefNodesDG refInfo dg of
2c08058468dab64c89a8eae51b56f9afb8b6cb71Cui Jian Just existNode -> (dg, NodeSig existNode sigma)
66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder ( insNodeDG (node, nodeCont) dg
84a30e66aef85cc54d3dd6f8e408729007fe8809Christian Maeder , NodeSig node sigma)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederrefNodesigs :: LibEnv -> LibName -> DGraph -> DGraph -> [(NodeName, NodeSig)]
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder -> (DGraph, [NodeSig])
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederrefNodesigs libenv ln = mapAccumR . refNodesig libenv ln
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian MaederrefExtsigAndInsert :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -> IRI -> ExtGenSig -> (ExtGenSig, (GlobalEnv, DGraph))
a07b1088ec14605a305cd48245f804b79cdce7b7Christian MaederrefExtsigAndInsert libenv ln refDG (genv, dg) new extsig =
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder let (dg1, extsig1) = refExtsig libenv ln refDG dg (makeName new) extsig
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder genv1 = Map.insert new (SpecEntry extsig1) genv
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder in (extsig1, (genv1, dg1))
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederrefExtsig :: LibEnv -> LibName -> DGraph -> DGraph -> NodeName -> ExtGenSig
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder -> (DGraph, ExtGenSig)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederrefExtsig libenv ln refDG dg name
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (ExtGenSig (GenSig imps params gsigmaP) body) = let
22250d2b3c9f86fe19cba665d71c301de03db142Christian Maeder pName = extName "Parameters" name
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder (dg1, imps1) = case imps of
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder EmptyNode _ -> (dg, imps)
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder JustNode ns -> let
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (dg0, nns) = refNodesig libenv ln refDG dg (extName "Imports" name, ns)
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder in (dg0, JustNode nns)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (dg2, params1) = refNodesigs libenv ln refDG dg1
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder $ snd $ foldr (\ p (n, l) -> let nn = inc n in
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder (nn, (nn, p) : l)) (pName, []) params
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder (dg3, gsigmaP1) = case gsigmaP of
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder EmptyNode _ -> (dg, gsigmaP)
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder JustNode ns -> let
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (dg0, nns) = refNodesig libenv ln refDG dg2 (pName, ns)
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder in (dg0, JustNode nns)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (dg4, body1) = refNodesig libenv ln refDG dg3 (name, body)
3d4e57e86d8aee818b589cd1029838e0accade55Christian Maeder in (dg4, ExtGenSig (GenSig imps1 params1 gsigmaP1) body1)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederrefViewsig :: LibEnv -> LibName -> DGraph -> DGraph -> NodeName -> ExtViewSig
7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder -> (DGraph, ExtViewSig)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian MaederrefViewsig libenv ln refDG dg name (ExtViewSig src mor extsig) = let
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (dg1, src1) = refNodesig libenv ln refDG dg (extName "Source" name, src)
18ff0b3378b1ad4f9d95be89e1d943634f9b1c7bChristian Maeder (dg2, extsig1) = refExtsig libenv ln refDG dg1 (extName "Target" name) extsig
7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder in (dg2, ExtViewSig src1 mor extsig1)
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder-- BEGIN CURIE expansion
48cf28f5245ec6879710165606262238784a1f15Soeren D. SchulzeexpandCurieItemNameMap :: FilePath -> FilePath -> ItemNameMap
b5444dac524839f6e7c9b18fe497fe12dbd3d8edChristian Maeder -> Either (Result ()) ItemNameMap
48cf28f5245ec6879710165606262238784a1f15Soeren D. SchulzeexpandCurieItemNameMap fn newFn (ItemNameMap i1 mi2) =
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze case expandCurieByPath fn i1 of
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze Just i -> case mi2 of
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze Nothing -> Right $ ItemNameMap i mi2
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze Just j -> case expandCurieByPath newFn j of
b5444dac524839f6e7c9b18fe497fe12dbd3d8edChristian Maeder Nothing -> Left $ prefixErrorIRI j
48cf28f5245ec6879710165606262238784a1f15Soeren D. Schulze mj -> Right $ ItemNameMap i mj
b5444dac524839f6e7c9b18fe497fe12dbd3d8edChristian Maeder Nothing -> Left $ prefixErrorIRI i1
f8065e835104ae5eaa148e9b37a81e768990724bEugen KuksaitemNameMapsToIRIs :: [ItemNameMap] -> [IRI]
a670ae262852ddcf674185307f9c343d42719ea2Christian MaederitemNameMapsToIRIs = concatMap (\ (ItemNameMap i mi) -> [i | isNothing mi])
63ba2f828c63eb66506bc014b24a87adf97ae950Christian Maeder-- END CURIE expansion