AnalysisLibrary.hs revision c35969f341eb137848e9c0874503bed8c419cbd2
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbModule : $Header$
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbDescription : static analysis of CASL specification libraries
bc8fd1b0b1afdf89b8d28eefa8cd74e26ba97986fieldingCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbMaintainer : till@informatik.uni-bremen.de
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbStability : provisional
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbPortability : non-portable(Logic)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbStatic analysis of CASL specification libraries
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Follows the verification semantics sketched in Chap. IV:6
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb of the CASL Reference Manual.
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ( anaLibFileOrGetEnv
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , anaLibDefn
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , anaSourceFile
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , anaLibItem
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , anaViewDefn
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Static.ArchDiagram (emptyExtStUnitCtx)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Common.AS_Annotation hiding (isAxiom, isDef)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport qualified Data.Map as Map
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport qualified Data.Set as Set
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- a set of library names to check for cyclic imports
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbtype LNS = Set.Set LibName
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- | parsing and static analysis for files
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- Parameters: logic graph, default logic, file name
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbanaSourceFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -> FilePath -> ResultT IO (LibName, LibEnv)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbanaSourceFile = anaSource Nothing
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbanaSource :: Maybe LibName -- ^ suggested library name
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -> FilePath -> ResultT IO (LibName, LibEnv)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbanaSource mln lgraph opts topLns libenv initDG fname = ResultT $ do
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb fname' <- findFileOfLibName opts fname
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb case fname' of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Nothing ->
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return $ fail $ "no file for library '" ++ fname ++ "' found."
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Just file ->
f888346b48f5e5b5e3f0a47dedb8cefd2759a4e2gregames if any (`isSuffixOf` file) [envSuffix, prfSuffix] then
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb fail $ "no matching source file for '" ++ fname ++ "' found."
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb input <- readEncFile Latin1 file
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb putIfVerbose opts 2 $ "Reading file " ++ file
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb if takeExtension file /= ('.' : show TwelfIn)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb then runResultT $
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb anaString mln lgraph opts topLns libenv initDG input file
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz res <- anaTwelfFile opts file
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Nothing -> fail ""
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Just (lname,lenv) -> return $ Result [] $
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Just (lname, Map.union lenv libenv)
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz-- | parsing and static analysis for string (=contents of file)
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz-- Parameters: logic graph, default logic, contents of file, filename
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzanaString :: Maybe LibName -- ^ suggested library name
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> String
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -> FilePath -> ResultT IO (LibName, LibEnv)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbanaString mln lgraph opts topLns libenv initDG input file = do
4f9c22c4f27571d54197be9674e1fc0d528192aestriker curDir <- lift getCurrentDirectory -- get full path for parser positions
a2a0abd88b19e042a3eb2a9fa1702c25ad51303dwrowe mt <- lift $ getModificationTime file
4f9c22c4f27571d54197be9674e1fc0d528192aestriker let Result ds mast = readLibDefnM lgraph opts (curDir </> file) input
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb case mast of
4f9c22c4f27571d54197be9674e1fc0d528192aestriker Just (Lib_defn pln is ps ans) ->
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let noSuffixFile = dropExtensions file
4f9c22c4f27571d54197be9674e1fc0d528192aestriker spN = reverse $ takeWhile (/= '/') $ reverse
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb $ filter (\ c -> isAlphaNum c || elem c "'_/") noSuffixFile
4f9c22c4f27571d54197be9674e1fc0d528192aestriker noLibName = null $ show $ getLibId pln
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb nLn = setFilePath (curDir </> file) mt
4f9c22c4f27571d54197be9674e1fc0d528192aestriker $ if noLibName then fromMaybe (emptyLibName spN) mln else pln
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb nIs = case is of
4f9c22c4f27571d54197be9674e1fc0d528192aestriker [Annoted (Spec_defn spn gn as qs) rs [] []]
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb | noLibName && null (tokStr spn)
4f9c22c4f27571d54197be9674e1fc0d528192aestriker -> [Annoted (Spec_defn (mkSimpleId spN) gn as qs) rs [] []]
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ast@(Lib_defn ln _ _ _) = Lib_defn nLn nIs ps ans
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe in case analysis opts of
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe lift $ putIfVerbose opts 1 $
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe "Skipping static analysis of library " ++ show ln
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe ga <- liftR $ addGlobalAnnos emptyGlobalAnnos ans
c2cf53a40a9814eb91db2cdf820f97d943f21628coar lift $ writeLibDefn ga file opts ast
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe liftR $ Result ds Nothing
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar let libstring = show $ getLibId ln
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe unless (isSuffixOf libstring noSuffixFile) $ lift
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar $ putIfVerbose opts 1
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe $ "### file name '" ++ file ++ "' does not match library name '"
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe ++ libstring ++ "'"
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe lift $ putIfVerbose opts 1 $ "Analyzing "
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe ++ (if noLibName then "file " ++ file ++ " as " else "")
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe ++ "library " ++ show ln
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (_, ld, _, lenv) <- anaLibDefn lgraph opts topLns libenv initDG ast
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe case Map.lookup ln lenv of
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Nothing -> error $ "anaString: missing library: " ++ show ln
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Just dg -> lift $ do
3e392a5afd51526de3cb15d57ee46d8cb160ae65gregames writeLibDefn (globalAnnos dg) file opts ld
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe when (hasEnvOut opts)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (writeFileInfo opts ln file ld dg)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe return (ln, lenv)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Nothing -> liftR $ Result ds Nothing
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz-- lookup or read a library
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzanaLibFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LibName
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz -> ResultT IO (LibName, LibEnv)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweanaLibFile lgraph opts topLns libenv initDG ln =
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe let lnstr = show ln in case Map.lookup ln libenv of
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Just _ -> do
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe analyzing opts $ "from " ++ lnstr
4f9c22c4f27571d54197be9674e1fc0d528192aestriker return (ln, libenv)
4f9c22c4f27571d54197be9674e1fc0d528192aestriker Nothing -> do
3e392a5afd51526de3cb15d57ee46d8cb160ae65gregames putMessageIORes opts 1 $ "Downloading " ++ lnstr ++ " ..."
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe res <- anaLibFileOrGetEnv lgraph
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar (if recurse opts then opts else opts { outtypes = [] })
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe (Set.insert ln topLns) libenv initDG ln $ libNameToFile ln
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe putMessageIORes opts 1 $ "... loaded " ++ lnstr
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe-- | lookup or read a library
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweanaLibFileOrGetEnv :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe -> LibName -> FilePath -> ResultT IO (LibName, LibEnv)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweanaLibFileOrGetEnv lgraph opts topLns libenv initDG ln file = ResultT $ do
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe let envFile = rmSuffix file ++ envSuffix
4f9c22c4f27571d54197be9674e1fc0d528192aestriker recent_envFile <- checkRecentEnv opts envFile file
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe if recent_envFile
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe mgc <- readVerbose lgraph opts ln envFile
c2cf53a40a9814eb91db2cdf820f97d943f21628coar case mgc of
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Nothing -> runResultT $ do
4775dfc34c90fada8c7c4d6a57ed8a3114d55c2dtrawick lift $ putIfVerbose opts 1 $ "Deleting " ++ envFile
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe lift $ removeFile envFile
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe anaSource (Just ln) lgraph opts topLns libenv initDG file
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe Just (ld, gc) -> do
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe writeLibDefn (globalAnnos gc) file opts ld
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar -- get all DGRefs from DGraph
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe Result ds mEnv <- runResultT $ foldl
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe ( \ ioLibEnv labOfDG -> let node = snd labOfDG in
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe if isDGRef node then do
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe let ln2 = dgn_libname node
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe p_libEnv <- ioLibEnv
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe if Map.member ln2 p_libEnv then
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe return p_libEnv
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe else fmap snd $ anaLibFile lgraph
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe opts topLns p_libEnv initDG ln2
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe else ioLibEnv)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (return $ Map.insert ln gc libenv)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe $ labNodesDG gc
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe return $ Result ds $ fmap
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe ( \ rEnv -> (ln, rEnv)) mEnv
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe else runResultT
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe $ anaSource (Just ln) lgraph opts topLns libenv initDG file
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe{- | analyze a LIB_DEFN.
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe Parameters: logic graph, default logic, opts, library env, LIB_DEFN.
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe Call this function as follows:
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe> do Result diags res <- runResultT (anaLibDefn ...)
4f9c22c4f27571d54197be9674e1fc0d528192aestriker> mapM_ (putStrLn . show) diags
4f9c22c4f27571d54197be9674e1fc0d528192aestrikeranaLibDefn :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LIB_DEFN
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe -> ResultT IO (LibName, LIB_DEFN, DGraph, LibEnv)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweanaLibDefn lgraph opts topLns libenv dg (Lib_defn ln alibItems pos ans) = do
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar gannos <- showDiags1 opts $ liftR $ addGlobalAnnos emptyGlobalAnnos ans
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe (libItems', dg', libenv', _) <- foldM (anaLibItemAux opts topLns)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe ([], dg { globalAnnos = gannos }, libenv, lgraph) (map item alibItems)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe let dg1 = computeDGraphTheories libenv' $ markFree libenv' $
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe markHiding libenv' dg'
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe return (ln, Lib_defn ln
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (zipWith replaceAnnoted (reverse libItems') alibItems)
4f9c22c4f27571d54197be9674e1fc0d528192aestriker pos ans, dg1, Map.insert ln dg1 libenv')
c2cf53a40a9814eb91db2cdf820f97d943f21628coaranaLibItemAux :: HetcatsOpts -> LNS -> ([LIB_ITEM], DGraph, LibEnv, LogicGraph)
c2cf53a40a9814eb91db2cdf820f97d943f21628coar -> LIB_ITEM -> ResultT IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweanaLibItemAux opts topLns (libItems', dg1, libenv1, lG) libItem =
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz let newLG = case libItems' of
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz [] -> lG { currentLogic = defLogic opts }
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Logic_decl (Logic_name logTok _) _ : _ ->
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe lG { currentLogic = tokStr logTok }
c2cf53a40a9814eb91db2cdf820f97d943f21628coar currLog = currentLogic newLG
c2cf53a40a9814eb91db2cdf820f97d943f21628coar newOpts = if elem currLog ["DMU", "Framework"] then
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe opts { defLogic = currLog } else opts
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz in ResultT (do
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Result diags2 res <-
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz runResultT $ anaLibItem newLG newOpts topLns libenv1 dg1 libItem
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe runResultT $ showDiags1 newOpts (liftR (Result diags2 res))
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe let mRes = case res of
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe Just (libItem', dg1', libenv1') ->
4f9c22c4f27571d54197be9674e1fc0d528192aestriker Just (libItem' : libItems', dg1', libenv1', newLG)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe Nothing -> Nothing
4f9c22c4f27571d54197be9674e1fc0d528192aestriker if outputToStdout newOpts then
4f9c22c4f27571d54197be9674e1fc0d528192aestriker if hasErrors diags2 then
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe fail "Stopped due to errors"
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe else runResultT $ liftR $ Result [] mRes
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz else runResultT $ liftR $ Result diags2 mRes)
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzputMessageIORes :: HetcatsOpts -> Int -> String -> ResultT IO ()
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweputMessageIORes opts i msg =
4f9c22c4f27571d54197be9674e1fc0d528192aestriker if outputToStdout opts
c2cf53a40a9814eb91db2cdf820f97d943f21628coar then lift $ putIfVerbose opts i msg
c2cf53a40a9814eb91db2cdf820f97d943f21628coar else liftR $ message () msg
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzanalyzing :: HetcatsOpts -> String -> ResultT IO ()
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzanalyzing opts = putMessageIORes opts 1 . ("Analyzing " ++)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowealreadyDefined :: String -> String
4f9c22c4f27571d54197be9674e1fc0d528192aestrikeralreadyDefined str = "Name " ++ str ++ " already defined"
c2cf53a40a9814eb91db2cdf820f97d943f21628coar-- | analyze a GENERICITY
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweanaGenericity :: LogicGraph -> DGraph -> HetcatsOpts -> NodeName -> GENERICITY
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz -> Result (GENERICITY, GenSig, DGraph)
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzanaGenericity lg dg opts name
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz gen@(Genericity (Params psps) (Imported isps) pos) =
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe adjustPos pos $ case psps of
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe [] -> do -- no parameter ...
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe unless (null isps) $ plain_error ()
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe "Parameterless specifications must not have imports" pos
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe l <- lookupCurrentLogic "GENERICITY" lg
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe return (gen, GenSig (EmptyNode l) [] $ EmptyNode l, dg)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe l <- lookupCurrentLogic "IMPORTS" lg
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (imps', nsigI, dg') <- case isps of
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe [] -> return ([], EmptyNode l, dg)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (is', _, nsig', dgI) <- anaUnion False lg dg (EmptyNode l)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (extName "Imports" name) opts isps
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe return (is', JustNode nsig', dgI)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (ps', nsigPs, ns, dg'') <- anaUnion False lg dg' nsigI
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (extName "Parameters" name) opts psps
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe return (Genericity (Params ps') (Imported imps') pos,
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe GenSig nsigI nsigPs $ JustNode ns, dg'')
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe-- | analyse a LIB_ITEM
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweanaLibItem :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LIB_ITEM
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe -> ResultT IO (LIB_ITEM, DGraph, LibEnv)
cc9582e53aead2a044077c4a92f3dfc3605590b3wroweanaLibItem lgraph opts topLns libenv dg itm = case itm of
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe Spec_defn spn gen asp pos -> do
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe let spstr = tokStr spn
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe nName = makeName spn
4f9c22c4f27571d54197be9674e1fc0d528192aestriker analyzing opts $ "spec " ++ spstr
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe (gen', gsig@(GenSig _ args allparams), dg') <-
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe liftR $ anaGenericity lgraph dg opts nName gen
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe (sanno1, impliesA) <- liftR $ getSpecAnnos pos asp
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe when impliesA $ liftR $ plain_error ()
0540a0b469147b52e858587270dba31c2aaa9e09wrowe "unexpected initial %implies in spec-defn" pos
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe (sp', body, dg'') <-
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe liftR (anaSpecTop sanno1 True lgraph dg'
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe allparams nName opts (item asp))
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe genv = globalEnv dg
4f9c22c4f27571d54197be9674e1fc0d528192aestriker then liftR $ plain_error (libItem', dg'', libenv)
4f9c22c4f27571d54197be9674e1fc0d528192aestriker (alreadyDefined spstr) pos
4f9c22c4f27571d54197be9674e1fc0d528192aestriker let (_n, dg''') = addSpecNodeRT dg'' (UnitSig args body) $ show spn
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp , dg''' { globalEnv = Map.insert spn (SpecEntry
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe $ ExtGenSig gsig body) genv }
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp View_defn vn gen vt gsis pos -> do
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe analyzing opts $ "view " ++ tokStr vn
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe liftR $ anaViewDefn lgraph libenv dg opts vn gen vt gsis pos
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe Arch_spec_defn asn asp pos -> do
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe let asstr = tokStr asn
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe analyzing opts $ "arch spec " ++ asstr
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe (n, _, diag, archSig, dg', asp') <- liftR $ anaArchSpec lgraph dg opts
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe emptyExtStUnitCtx $ item asp
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp let asd' = Arch_spec_defn asn (replaceAnnoted asp' asp) pos
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp genv = globalEnv dg'
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp then liftR $ plain_error (asd', dg', libenv) (alreadyDefined asstr) pos
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp let dg'' = updateNodeNameSpecRT dg' n $ show asn
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp dg3 = dg'' { archSpecDiags =
4f9c22c4f27571d54197be9674e1fc0d528192aestriker Map.insert (show asn) diag $ archSpecDiags dg''}
4f9c22c4f27571d54197be9674e1fc0d528192aestriker return (asd', dg3
4f9c22c4f27571d54197be9674e1fc0d528192aestriker { globalEnv = Map.insert asn (ArchEntry archSig) genv },
4f9c22c4f27571d54197be9674e1fc0d528192aestriker Unit_spec_defn usn usp pos -> do
4f9c22c4f27571d54197be9674e1fc0d528192aestriker let usstr = tokStr usn
4f9c22c4f27571d54197be9674e1fc0d528192aestriker analyzing opts $ "unit spec " ++ usstr
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp l <- lookupCurrentLogic "Unit_spec_defn" lgraph
7a2edaa0193cbb0d79a65a8461a609a9402aea49brianp (rSig, dg', usp') <-
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe liftR $ anaUnitSpec lgraph dg opts (EmptyNode l) usp
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe unitSig <- liftR $ getUnitSigFromRef rSig
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe let usd' = Unit_spec_defn usn usp' pos
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe genv = globalEnv dg'
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe then liftR $ plain_error (itm, dg', libenv) (alreadyDefined usstr) pos
4f9c22c4f27571d54197be9674e1fc0d528192aestriker else return (usd', dg'
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp { globalEnv = Map.insert usn (UnitEntry unitSig) genv },
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe Ref_spec_defn rn rsp pos -> do
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe let rnstr = tokStr rn
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe l <- lookupCurrentLogic "Ref_spec_defn" lgraph
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (_, _, _, rsig, dg', rsp') <-
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb liftR (anaRefSpec lgraph dg opts (EmptyNode l) rn emptyExtStUnitCtx
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb analyzing opts $ "ref spec " ++ rnstr
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let rsd' = Ref_spec_defn rn rsp' pos
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb genv = globalEnv dg'
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb then liftR (plain_error (itm, dg', libenv)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (alreadyDefined rnstr)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb else return ( rsd', dg' { globalEnv = Map.insert rn (RefEntry rsig) genv }
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Logic_decl (Logic_name logTok _) _ -> do
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb logNm <- lookupLogic "LOGIC DECLARATION:" (tokStr logTok) lgraph
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb putMessageIORes opts 1 $ "logic " ++ show logNm
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return (itm, dg, libenv)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Download_items ln items pos -> if Set.member ln topLns then
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb liftR $ mkError "illegal cyclic library import"
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb $ Set.map getLibId topLns
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (ln', libenv') <- anaLibFile lgraph opts topLns libenv
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (cpIndexMaps dg emptyDG) ln
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb unless (ln == ln')
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb $ liftR $ warning ()
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (shows ln " does not match internal name " ++ shows ln' "")
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb case Map.lookup ln' libenv' of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Nothing -> error $ "Internal error: did not find library "
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ++ show ln' ++ " available: " ++ show (Map.keys libenv')
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Just dg' -> do
c2cf53a40a9814eb91db2cdf820f97d943f21628coar let dg0 = cpIndexMaps dg' dg
c2cf53a40a9814eb91db2cdf820f97d943f21628coar dg1 <- liftR $ anaItemNamesOrMaps libenv' ln' dg' dg0 items
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return (itm, dg1, libenv')
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Newlogic_defn ld _ -> ResultT $ do
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb dg' <- anaLogicDef ld dg
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe return $ Result [] $ Just (itm, dg', libenv)
4f9c22c4f27571d54197be9674e1fc0d528192aestriker-- the first DGraph dg' is that of the imported library
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweanaItemNamesOrMaps :: LibEnv -> LibName -> DGraph -> DGraph
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe -> [ITEM_NAME_OR_MAP] -> Result DGraph
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweanaItemNamesOrMaps libenv' ln dg' dg items = do
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe (genv1, dg1) <- foldM
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe (anaItemNameOrMap libenv' ln $ globalEnv dg') (globalEnv dg, dg) items
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe gannos'' <- globalAnnos dg `mergeGlobalAnnos` globalAnnos dg'
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe { globalAnnos = gannos''
4f9c22c4f27571d54197be9674e1fc0d528192aestriker , globalEnv = genv1 }
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe-- | analyse genericity and view type and construct gmorphism
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweanaViewDefn :: LogicGraph -> LibEnv -> DGraph -> HetcatsOpts -> SIMPLE_ID
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe -> Result (LIB_ITEM, DGraph, LibEnv)
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweanaViewDefn lgraph libenv dg opts vn gen vt gsis pos = do
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz let vName = makeName vn
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe (gen', gsig@(GenSig _ _ allparams), dg') <-
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar anaGenericity lgraph dg opts vName gen
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe (vt', (src@(NodeSig nodeS gsigmaS)
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar , tar@(NodeSig nodeT gsigmaT@(G_sign lidT _ _))), dg'') <-
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe anaViewType lgraph dg' allparams opts vName vt
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz let genv = globalEnv dg''
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz then plain_error (View_defn vn gen' vt' gsis pos, dg'', libenv)
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe (alreadyDefined $ tokStr vn) pos
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz (gsigmaS', imor) <- gSigCoerce lgraph gsigmaS (Logic lidT)
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe tmor <- gEmbedComorphism imor gsigmaS
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar emor <- fmap gEmbed $ anaGmaps lgraph opts pos gsigmaS' gsigmaT gsis
11fb2f3611e6ff9a541e10b13e3108934f828141gregames gmor <- comp tmor emor
11fb2f3611e6ff9a541e10b13e3108934f828141gregames let vsig = ExtViewSig src gmor $ ExtGenSig gsig tar
11fb2f3611e6ff9a541e10b13e3108934f828141gregames voidView = nodeS == nodeT && isHomInclusion gmor
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz when voidView $ warning ()
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz ("identity mapping of source to same target for view: " ++ tokStr vn)
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz return (View_defn vn gen' vt' gsis pos,
4f9c22c4f27571d54197be9674e1fc0d528192aestriker (if voidView then dg'' else insLink dg'' gmor globalThm
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe (DGLinkView vn $ Fitted gsis) nodeS nodeT)
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe -- 'LeftOpen' for conserv correct?
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe { globalEnv = Map.insert vn (ViewEntry vsig) genv }
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe-- | analyze a VIEW_TYPE
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe-- The first three arguments give the global context
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar-- The AnyLogic is the current logic
2f1949bb0e3c209db94c8d521cba7380b9d11421trawick-- The NodeSig is the signature of the parameter of the view
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar-- flag, whether just the structure shall be analysed
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweanaViewType :: LogicGraph -> DGraph -> MaybeNode -> HetcatsOpts -> NodeName
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar -> VIEW_TYPE -> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoaranaViewType lg dg parSig opts name (View_type aspSrc aspTar pos) = do
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe l <- lookupCurrentLogic "VIEW_TYPE" lg
4f9c22c4f27571d54197be9674e1fc0d528192aestriker (spSrc', srcNsig, dg') <- adjustPos pos $ anaSpec False lg dg (EmptyNode l)
4f9c22c4f27571d54197be9674e1fc0d528192aestriker (extName "Source" name) opts (item aspSrc)
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe (spTar', tarNsig, dg'') <- adjustPos pos $ anaSpec True lg dg' parSig
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar (extName "Target" name) opts (item aspTar)
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe return (View_type (replaceAnnoted spSrc' aspSrc)
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar (replaceAnnoted spTar' aspTar)
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar (srcNsig, tarNsig), dg'')
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweanaItemNameOrMap :: LibEnv -> LibName -> GlobalEnv -> (GlobalEnv, DGraph)
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe -> ITEM_NAME_OR_MAP -> Result (GlobalEnv, DGraph)
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantzanaItemNameOrMap libenv ln genv' res itm =
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz anaItemNameOrMap1 libenv ln genv' res $ case itm of
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz Item_name name -> (name, name)
7c301a1818939f85da8f3629cc3e9b5588610ef0jerenkrantz Item_name_map old new _ -> (old, new)
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe-- | Auxiliary function for not yet implemented features
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweanaErr :: String -> a
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbanaErr f = error $ "*** Analysis of " ++ f ++ " is not yet implemented!"
8aefbd756763807188d2e3ce336a8680e4893066wroweanaItemNameOrMap1 :: LibEnv -> LibName -> GlobalEnv -> (GlobalEnv, DGraph)
8aefbd756763807188d2e3ce336a8680e4893066wrowe -> (SIMPLE_ID, SIMPLE_ID) -> Result (GlobalEnv, DGraph)
8aefbd756763807188d2e3ce336a8680e4893066wroweanaItemNameOrMap1 libenv ln genv' (genv, dg) (old, new) = do
8aefbd756763807188d2e3ce336a8680e4893066wrowe let newName = makeName new
8aefbd756763807188d2e3ce336a8680e4893066wrowe entry <- maybeToResult (tokPos old)
8aefbd756763807188d2e3ce336a8680e4893066wrowe (tokStr old ++ " not found") (Map.lookup old genv')
8aefbd756763807188d2e3ce336a8680e4893066wrowe case Map.lookup new genv of
8aefbd756763807188d2e3ce336a8680e4893066wrowe Nothing -> return ()
8aefbd756763807188d2e3ce336a8680e4893066wrowe Just _ -> fail (tokStr new ++ " already used")
8aefbd756763807188d2e3ce336a8680e4893066wrowe case entry of
8aefbd756763807188d2e3ce336a8680e4893066wrowe SpecEntry extsig ->
8aefbd756763807188d2e3ce336a8680e4893066wrowe let (dg1, extsig1) = refExtsig libenv ln dg newName extsig
8aefbd756763807188d2e3ce336a8680e4893066wrowe genv1 = Map.insert new (SpecEntry extsig1) genv
8aefbd756763807188d2e3ce336a8680e4893066wrowe in return (genv1, dg1)
8aefbd756763807188d2e3ce336a8680e4893066wrowe StructEntry vsig ->
a2a0abd88b19e042a3eb2a9fa1702c25ad51303dwrowe let (dg1, vsig1) = refViewsig libenv ln dg newName vsig
8aefbd756763807188d2e3ce336a8680e4893066wrowe genv1 = Map.insert new (StructEntry vsig1) genv
e4a3f3c2f080cac75a15a6454cca429b8161c050wrowe in return (genv1, dg1)
8aefbd756763807188d2e3ce336a8680e4893066wrowe ViewEntry vsig ->
8aefbd756763807188d2e3ce336a8680e4893066wrowe let (dg1, vsig1) = refViewsig libenv ln dg newName vsig
2fa5b5878e7567e2875807c3e2a2b3b0d3ef74bewrowe genv1 = Map.insert new (ViewEntry vsig1) genv
2fa5b5878e7567e2875807c3e2a2b3b0d3ef74bewrowe in return (genv1, dg1)
e4a3f3c2f080cac75a15a6454cca429b8161c050wrowe ArchEntry _asig -> anaErr "arch spec download"
e4a3f3c2f080cac75a15a6454cca429b8161c050wrowe UnitEntry _usig -> anaErr "unit spec download"
8aefbd756763807188d2e3ce336a8680e4893066wrowe RefEntry _rsig -> anaErr "ref spec download"
dc8692c6c0ca616a09aa12dad005f2ef23baa1a0wrowerefNodesig :: LibEnv -> LibName -> DGraph -> (NodeName, NodeSig)
a8d11d78181478da6a672f7fbc58b8d523351f49wrowe -> (DGraph, NodeSig)
4f9c22c4f27571d54197be9674e1fc0d528192aestrikerrefNodesig libenv refln dg (name, NodeSig refn sigma@(G_sign lid sig ind)) =
23c6309e36a63b13b61c35999c978017521993d6wrowe let (ln, (n, lbl)) = getActualParent libenv refln refn
23c6309e36a63b13b61c35999c978017521993d6wrowe refInfo = newRefInfo ln n
4f9c22c4f27571d54197be9674e1fc0d528192aestriker new = newInfoNodeLab name refInfo
23c6309e36a63b13b61c35999c978017521993d6wrowe $ noSensGTheory lid sig ind
8aefbd756763807188d2e3ce336a8680e4893066wrowe nodeCont = new { globalTheory = globalTheory lbl }
23c6309e36a63b13b61c35999c978017521993d6wrowe node = getNewNodeDG dg
dc8692c6c0ca616a09aa12dad005f2ef23baa1a0wrowe in case lookupInAllRefNodesDG refInfo dg of
4f9c22c4f27571d54197be9674e1fc0d528192aestriker Just existNode -> (dg, NodeSig existNode sigma)
e4a3f3c2f080cac75a15a6454cca429b8161c050wrowe ( addToRefNodesDG node refInfo $ insNodeDG (node, nodeCont) dg
8aefbd756763807188d2e3ce336a8680e4893066wrowe , NodeSig node sigma)
cf6ef072483172309861d06e85b1aeff4573c060wrowe{- | get to the actual parent which is not a referenced node, so that
cf6ef072483172309861d06e85b1aeff4573c060wrowe the small chains between nodes in different library can be advoided.
cf6ef072483172309861d06e85b1aeff4573c060wrowe (details see ticket 5)
4f9c22c4f27571d54197be9674e1fc0d528192aestrikergetActualParent :: LibEnv -> LibName -> Node -> (LibName, LNode DGNodeLab)
4f9c22c4f27571d54197be9674e1fc0d528192aestrikergetActualParent libenv ln n =
e4a3f3c2f080cac75a15a6454cca429b8161c050wrowe let refLab = labDG (lookupDGraph ln libenv) n in
e4a3f3c2f080cac75a15a6454cca429b8161c050wrowe if isDGRef refLab then
e4a3f3c2f080cac75a15a6454cca429b8161c050wrowe -- recursively goes to parent of the current node, but
4f9c22c4f27571d54197be9674e1fc0d528192aestriker -- it actually would only be done once
a8d11d78181478da6a672f7fbc58b8d523351f49wrowe getActualParent libenv (dgn_libname refLab) (dgn_node refLab)
e4a3f3c2f080cac75a15a6454cca429b8161c050wrowe else (ln, (n, refLab))
8aefbd756763807188d2e3ce336a8680e4893066wrowerefNodesigs :: LibEnv -> LibName -> DGraph -> [(NodeName, NodeSig)]
cf6ef072483172309861d06e85b1aeff4573c060wrowe -> (DGraph, [NodeSig])
cf6ef072483172309861d06e85b1aeff4573c060wrowerefNodesigs libenv = mapAccumR . refNodesig libenv
8aefbd756763807188d2e3ce336a8680e4893066wrowerefExtsig :: LibEnv -> LibName -> DGraph -> NodeName -> ExtGenSig
cf6ef072483172309861d06e85b1aeff4573c060wrowe -> (DGraph, ExtGenSig)
cf6ef072483172309861d06e85b1aeff4573c060wrowerefExtsig libenv ln dg name (ExtGenSig (GenSig imps params gsigmaP) body) = let
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp pName = extName "Parameters" name
cf6ef072483172309861d06e85b1aeff4573c060wrowe (dg1, imps1) = case imps of
4f9c22c4f27571d54197be9674e1fc0d528192aestriker EmptyNode _ -> (dg, imps)
cf6ef072483172309861d06e85b1aeff4573c060wrowe JustNode ns -> let
cf6ef072483172309861d06e85b1aeff4573c060wrowe (dg0, nns) = refNodesig libenv ln dg (extName "Imports" name, ns)
cf6ef072483172309861d06e85b1aeff4573c060wrowe in (dg0, JustNode nns)
cf6ef072483172309861d06e85b1aeff4573c060wrowe (dg2, params1) = refNodesigs libenv ln dg1
cf6ef072483172309861d06e85b1aeff4573c060wrowe $ snd $ foldr (\ p (n, l) -> let nn = inc n in
cf6ef072483172309861d06e85b1aeff4573c060wrowe (nn, (nn, p) : l)) (pName, []) params
cf6ef072483172309861d06e85b1aeff4573c060wrowe (dg3, gsigmaP1) = case gsigmaP of
cf6ef072483172309861d06e85b1aeff4573c060wrowe EmptyNode _ -> (dg, gsigmaP)
cf6ef072483172309861d06e85b1aeff4573c060wrowe JustNode ns -> let
69adb3d949e3dd17c0492a01fc2cf298832c7eefwrowe (dg0, nns) = refNodesig libenv ln dg2 (pName, ns)
69adb3d949e3dd17c0492a01fc2cf298832c7eefwrowe in (dg0, JustNode nns)
d75626f0952c6152a99acd013a4f127d46f0f9edtrawick (dg4, body1) = refNodesig libenv ln dg3 (name, body)
d75626f0952c6152a99acd013a4f127d46f0f9edtrawick in (dg4, ExtGenSig (GenSig imps1 params1 gsigmaP1) body1)
d75626f0952c6152a99acd013a4f127d46f0f9edtrawickrefViewsig :: LibEnv -> LibName -> DGraph -> NodeName -> ExtViewSig
d75626f0952c6152a99acd013a4f127d46f0f9edtrawick -> (DGraph, ExtViewSig)
d75626f0952c6152a99acd013a4f127d46f0f9edtrawickrefViewsig libenv ln dg name (ExtViewSig src mor extsig) = let
d75626f0952c6152a99acd013a4f127d46f0f9edtrawick (dg1, src1) = refNodesig libenv ln dg (extName "Source" name, src)
d75626f0952c6152a99acd013a4f127d46f0f9edtrawick (dg2, extsig1) = refExtsig libenv ln dg1 (extName "Target" name) extsig
d75626f0952c6152a99acd013a4f127d46f0f9edtrawick in (dg2, ExtViewSig src1 mor extsig1)