AnalysisLibrary.hs revision 84a30e66aef85cc54d3dd6f8e408729007fe8809
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederModule : $Header$
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederDescription : static analysis of CASL specification libraries
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMaintainer : till@informatik.uni-bremen.de
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStability : provisional
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederPortability : non-portable(Logic)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStatic analysis of CASL specification libraries
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Follows the verification semantics sketched in Chap. IV:6
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder of the CASL Reference Manual.
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder , ana_LIB_DEFN
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , anaSourceFile
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maederimport Common.AS_Annotation hiding (isAxiom, isDef)
d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maederimport qualified Data.Map as Map
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder-- | lookup an env or read and analyze a file
473f5af6e4803fbeecc814065952396f2501039bChristian MaederanaLib :: HetcatsOpts -> FilePath -> IO (Maybe (LIB_NAME, LibEnv))
473f5af6e4803fbeecc814065952396f2501039bChristian MaederanaLib opts fname = do
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder fname' <- existsAnSource opts {intype = GuessIn} $ rmSuffix fname
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder case fname' of
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder Nothing -> anaLibExt opts fname emptyLibEnv
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder if isSuffixOf prfSuffix file then do
844c7d2ec3917393e139e53503757098d568713eSimon Ulbricht putIfVerbose opts 0 $ "a matching source file for proof history '"
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder ++ file ++ "' not found."
04c445e50a1d8b95e667595594e6b551c8b2ff59Simon Ulbricht return Nothing
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder else anaLibExt opts file emptyLibEnv
c99b0eb6632087d502dd4269599c5aa68a148eebSimon Ulbricht-- | read a file and extended the current library environment
b99c9606f2faafeabb3fa8c596992143a561c787Simon UlbrichtanaLibExt :: HetcatsOpts -> FilePath -> LibEnv -> IO (Maybe (LIB_NAME, LibEnv))
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon UlbrichtanaLibExt opts file libEnv = do
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder Result ds res <- runResultT $ anaLibFileOrGetEnv logicGraph opts
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder libEnv (fileToLibName opts file) file
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder showDiags opts ds
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder Nothing -> return Nothing
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder Just (ln, lenv) -> do
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder let nEnv = if hasPrfOut opts then automatic ln lenv else lenv
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder dg = lookupDGraph ln nEnv
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder ga = globalAnnos dg
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder writeSpecFiles opts file nEnv ga ln dg
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder putIfVerbose opts 3 $ showGlobalDoc ga ga ""
dae8246f1f55b6a85e946fc1bfb6d32d556395f1Simon Ulbricht return $ Just (ln, nEnv)
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder-- | parsing and static analysis for files
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- Parameters: logic graph, default logic, file name
7710f7c3425e45af11af124ff37bec27229d24f7Christian MaederanaSourceFile :: LogicGraph -> HetcatsOpts -> LibEnv -> FilePath
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht -> ResultT IO (LIB_NAME, LibEnv)
df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaederanaSourceFile lgraph opts libenv fname = ResultT $ do
be1ce1c2b2819ef32743136c13101f1927375311Christian Maeder fname' <- existsAnSource opts {intype = GuessIn} fname
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder case fname' of
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder Nothing -> do
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder return $ fail $ "a file for input '" ++ fname ++ "' not found."
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder if any (flip isSuffixOf file) [envSuffix, prfSuffix] then
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder fail $ "a matching source file for '" ++ fname ++ "' not found."
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder curDir <- getCurrentDirectory
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder input <- readFile file
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder mt <- getModificationTime file
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder -- when switching to ghc 6.6.1 with System.FilePath use:
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -- combine curDir file
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder let absolutePath = if "/" `isPrefixOf` file
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder else curDir ++ '/':file
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder putIfVerbose opts 2 $ "Reading file " ++ absolutePath
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder runResultT $ anaString lgraph opts libenv input absolutePath mt
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder-- | parsing and static analysis for string (=contents of file)
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder-- Parameters: logic graph, default logic, contents of file, filename
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian MaederanaString :: LogicGraph -> HetcatsOpts -> LibEnv -> String
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder -> FilePath -> ClockTime -> ResultT IO (LIB_NAME, LibEnv)
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian MaederanaString lgraph opts libenv input file mt = do
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder let Result ds mast = read_LIB_DEFN_M lgraph opts file input mt
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder Just ast@(Lib_defn ln _ _ ans) -> case analysis opts of
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder lift $ putIfVerbose opts 1 $
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder "Skipping static analysis of library " ++ show ln
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder ga <- liftR $ addGlobalAnnos emptyGlobalAnnos ans
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder case gui opts of
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder Only -> return ()
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder _ -> lift $ write_LIB_DEFN ga file opts ast
5dd895cd3d794ecd2f0035ee3a7b6d6bf2eac5efChristian Maeder liftR $ Result ds Nothing
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder let libstring = show $ getLIB_ID ln
262a0a50e5f72336445bee69630a964660cc8622Christian Maeder if libstring == libraryS then return ()
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder if isSuffixOf libstring (rmSuffix file) then return () else
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder lift $ putIfVerbose opts 1 $
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder "### file name '" ++ file
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder ++ "' does not match library name '" ++
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder libstring ++ "'"
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder lift $ putIfVerbose opts 1 $ "Analyzing library " ++ show ln
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder (_,ld, _, lenv) <- ana_LIB_DEFN lgraph opts libenv ast
232c13ff6847a6f2bac7163392f80ab692cd7774Christian Maeder case Map.lookup ln lenv of
232c13ff6847a6f2bac7163392f80ab692cd7774Christian Maeder Nothing -> error $ "anaString: missing library: " ++ show ln
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder Just dg -> lift $ do
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder case gui opts of
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder Only -> return ()
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder _ -> write_LIB_DEFN (globalAnnos dg) file opts ld
2f0ca8050a33fbc1a23c0bd2dec0d09c17e3c548Christian Maeder when (hasEnvOut opts)
f50c9f317ed743022255535248028675a5716d2aSimon Ulbricht (writeFileInfo opts ln file ld dg)
232c13ff6847a6f2bac7163392f80ab692cd7774Christian Maeder return (ln, lenv)
232c13ff6847a6f2bac7163392f80ab692cd7774Christian Maeder Nothing -> liftR $ Result ds Nothing
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian MaederanaLibFile :: LogicGraph -> HetcatsOpts -> LibEnv -> LIB_NAME
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder -> ResultT IO (LIB_NAME, LibEnv)
63ec46a77d00127c46ec526df43da8d701c30c65Christian MaederanaLibFile lgraph opts libenv ln =
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder let lnstr = show ln in case Map.lookup ln libenv of
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder analyzing opts $ "from " ++ lnstr
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder return (ln, libenv)
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder Nothing -> do
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder putMessageIORes opts 1 $ "Downloading " ++ lnstr ++ " ..."
cc9f19b1fe81424205736fe0ae73620395b1bb74Simon Ulbricht res <- anaLibFileOrGetEnv lgraph
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht (if recurse opts then opts else opts { outtypes = [] })
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht libenv ln $ libNameToFile opts ln
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht putMessageIORes opts 1 $ "... loaded " ++ lnstr
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon UlbrichtanaLibFileOrGetEnv :: LogicGraph -> HetcatsOpts -> LibEnv
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht -> LIB_NAME -> FilePath -> ResultT IO (LIB_NAME, LibEnv)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon UlbrichtanaLibFileOrGetEnv lgraph opts libenv libname file = ResultT $ do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht let envFile = rmSuffix file ++ envSuffix
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht recent_envFile <- checkRecentEnv opts envFile file
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht if recent_envFile
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht mgc <- readVerbose opts libname envFile
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Nothing -> runResultT $ do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht lift $ putIfVerbose opts 1 $ "Deleting " ++ envFile
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht anaSourceFile lgraph opts libenv file
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Just (ld, gc) -> do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht write_LIB_DEFN (globalAnnos gc) file opts ld
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht -- get all DGRefs from DGraph
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Result ds mEnv <- runResultT $ foldl
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht ( \ ioLibEnv labOfDG -> let node = snd labOfDG in
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht if isDGRef node then do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht let ln = dgn_libname node
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht p_libEnv <- ioLibEnv
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht if Map.member ln p_libEnv then
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht return p_libEnv
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht else fmap snd $ anaLibFile lgraph
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht opts p_libEnv ln
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht else ioLibEnv)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht (return $ Map.insert libname gc libenv)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht $ labNodesDG gc
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht return $ Result ds $ fmap
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht ( \ rEnv -> (libname, rEnv)) mEnv
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht else runResultT $ anaSourceFile lgraph opts libenv file
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht-- | analyze a LIB_DEFN
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht-- Parameters: logic graph, default logic, opts, library env, LIB_DEFN
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht-- call this function as follows:
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht-- do Result diags res <- runResultT (ana_LIB_DEFN ...)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht-- mapM_ (putStrLn . show) diags
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbrichtana_LIB_DEFN :: LogicGraph -> HetcatsOpts -> LibEnv -> LIB_DEFN
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht -> ResultT IO (LIB_NAME,LIB_DEFN, DGraph, LibEnv)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbrichtana_LIB_DEFN lgraph opts libenv (Lib_defn ln alibItems pos ans) = do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht gannos <- showDiags1 opts $ liftR $ addGlobalAnnos emptyGlobalAnnos ans
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht dg <- lift $ emptyDGwithMVar
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht (libItems', dg1, libenv', _) <- foldM ana
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht ([], dg { globalAnnos = gannos }, libenv, lgraph) (map item alibItems)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht return (ln, Lib_defn ln
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht (map (uncurry replaceAnnoted) (zip (reverse libItems') alibItems))
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht pos ans, dg1, Map.insert ln dg1 libenv')
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht ana (libItems', dg1, libenv1, lG) libItem =
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht let newLG = case libItems' of
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht [] -> lG { currentLogic = defLogic opts }
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Logic_decl (Logic_name logTok _) _ : _ ->
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht lG { currentLogic = tokStr logTok }
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht in ResultT (do
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht Result diags2 res <-
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht runResultT $ ana_LIB_ITEM newLG opts libenv1 dg1 libItem
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht runResultT $ showDiags1 opts (liftR (Result diags2 res))
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht let mRes = case res of
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Just (libItem', dg1', libenv1') ->
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Just (libItem' : libItems', dg1', libenv1', newLG)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Nothing -> Nothing
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht if outputToStdout opts then
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht if hasErrors diags2 then
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht fail "Stopped due to errors"
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht else runResultT $ liftR $ Result [] mRes
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht else runResultT $ liftR $ Result diags2 mRes)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon UlbrichtputMessageIORes :: HetcatsOpts -> Int -> String -> ResultT IO ()
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon UlbrichtputMessageIORes opts i msg =
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht if outputToStdout opts
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht then lift $ putIfVerbose opts i msg
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht else liftR $ message () msg
562e30787355109feb0133ffea2ad86b6c143c26Simon Ulbrichtanalyzing :: HetcatsOpts -> String -> ResultT IO ()
562e30787355109feb0133ffea2ad86b6c143c26Simon Ulbrichtanalyzing opts msg = putMessageIORes opts 1 $ "Analyzing " ++ msg
562e30787355109feb0133ffea2ad86b6c143c26Simon UlbrichtalreadyDefined :: String -> String
562e30787355109feb0133ffea2ad86b6c143c26Simon UlbrichtalreadyDefined str = "Name " ++ str ++ " already defined"
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht-- | analyze a GENERICITY
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbrichtana_GENERICITY :: LogicGraph -> DGraph -> HetcatsOpts -> NodeName
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht -> GENERICITY -> Result (GENERICITY, GenericitySig, DGraph)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbrichtana_GENERICITY lg dg opts name
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht gen@(Genericity params@(Params psps) imps@(Imported isps) pos) =
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht [] -> do -- no parameter ...
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht when (not (null isps))
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht (plain_error () "Parameterless specifications must not have imports"
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht l <- lookupCurrentLogic "GENERICITY" lg
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht return (gen, GenericitySig (EmptyNode l) [] $ EmptyNode l, dg)
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht (imps', nsigI, dg') <- ana_IMPORTS lg dg opts (extName "I" name) imps
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht [asp] -> do -- one parameter ...
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht (sp', nsigP, dg'') <- ana_SPEC False lg dg' nsigI name opts (item asp)
7463a1bf64cfa90917e2afb6a5017ec411d2b3dbSimon Ulbricht return (Genericity (Params [replaceAnnoted sp' asp]) imps' pos,
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht GenericitySig nsigI [nsigP] $ JustNode nsigP, dg'')
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht _ -> do -- ... and more parameters
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht (params',nsigPs,dg'') <-
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht ana_PARAMS lg dg' nsigI opts (inc name) params
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht let adj = adjustPos pos
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht gsigmaP <- adj $ gsigManyUnion lg (map getSig nsigPs)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht let (NodeSig node _, dg3) = insGSig dg'' name DGFormalParams gsigmaP
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht inslink dgl (NodeSig n sigma) = do
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht incl <- adj $ ginclusion lg sigma gsigmaP
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht return $ insLink dgl incl GlobalDef DGFormalParams n node
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht dg4 <- foldM inslink dg3 nsigPs
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht return (Genericity params' imps' pos,
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht GenericitySig nsigI nsigPs $ JustNode $ NodeSig node gsigmaP, dg4)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbrichtana_PARAMS :: LogicGraph -> DGraph -> MaybeNode
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht -> HetcatsOpts -> NodeName -> PARAMS
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht -> Result (PARAMS, [NodeSig], DGraph)
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbrichtana_PARAMS lg dg nsigI opts name (Params asps) = do
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht (sps', pars, dg', _) <- foldM ana ([], [], dg, name) $ map item asps
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht return (Params (map (uncurry replaceAnnoted)
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht (zip (reverse sps') asps)),
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht reverse pars, dg')
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht ana (sps', pars, dg1, n) sp = do
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht (sp', par, dg') <- ana_SPEC False lg dg1 nsigI n opts sp
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht return (sp' : sps', par : pars, dg', inc n)
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbrichtana_IMPORTS :: LogicGraph -> DGraph -> HetcatsOpts -> NodeName -> IMPORTED
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht -> Result (IMPORTED, MaybeNode, DGraph)
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbrichtana_IMPORTS lg dg opts name imps@(Imported asps) = do
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht l <- lookupCurrentLogic "IMPORTS" lg
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht [] -> return (imps, EmptyNode l, dg)
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht let sp = Union asps nullRange
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht (Union asps' _, nsig', dg') <-
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht ana_SPEC False lg dg (EmptyNode l) name opts sp
2e76bbbed1c936bb0aee1753837e1c50416847a2Simon Ulbricht return (Imported asps', JustNode nsig', dg')
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht -- ??? emptyExplicit stuff needs to be added here
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht-- | analyse a LIB_ITEM
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbrichtana_LIB_ITEM :: LogicGraph -> HetcatsOpts -> LibEnv -> DGraph -> LIB_ITEM
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht -> ResultT IO (LIB_ITEM, DGraph, LibEnv)
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbrichtana_LIB_ITEM lgraph opts libenv dg itm = case itm of
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht Spec_defn spn gen asp pos -> do
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht let spstr = tokStr spn
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht analyzing opts $ "spec " ++ spstr
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht (gen', GenericitySig imp params allparams, dg') <-
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht liftR (ana_GENERICITY lgraph dg opts
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht (extName "P" (makeName spn)) gen)
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht (sp', body, dg'') <-
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht liftR (ana_SPEC True lgraph dg'
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht allparams (makeName spn) opts (item asp))
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht genv = globalEnv dg
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht then liftR (plain_error (libItem', dg'', libenv)
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht (alreadyDefined spstr) pos)
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht , dg'' { globalEnv = Map.insert spn (SpecEntry
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht $ ExtGenSig imp params (getMaybeSig allparams) body) genv }
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht View_defn vn gen vt gsis pos -> do
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht analyzing opts $ "view " ++ tokStr vn
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht liftR (ana_VIEW_DEFN lgraph libenv dg opts vn gen vt gsis pos)
562e30787355109feb0133ffea2ad86b6c143c26Simon Ulbricht Arch_spec_defn asn asp pos -> do
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht let asstr = tokStr asn
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht analyzing opts $ "arch spec " ++ asstr
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht (archSig, dg', asp') <-
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht liftR (ana_ARCH_SPEC lgraph dg opts (item asp))
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht let asd' = Arch_spec_defn asn (replaceAnnoted asp' asp) pos
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht genv = globalEnv dg'
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht then liftR (plain_error (asd', dg', libenv)
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht (alreadyDefined asstr) pos)
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder else return (asd', dg'
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht { globalEnv = Map.insert asn (ArchEntry archSig) genv },
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht Unit_spec_defn usn usp pos -> do
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht let usstr = tokStr usn
f6a562e28240e4f9107c199ba7a8e500ccfbfa55Simon Ulbricht analyzing opts $ "unit spec " ++ usstr
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht l <- lookupCurrentLogic "Unit_spec_defn" lgraph
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht (unitSig, dg', usp') <- liftR (ana_UNIT_SPEC lgraph dg opts
9a5e6e537c43a631facd9d87ce1a6c76f4b0af6dSimon Ulbricht (EmptyNode l) usp)
05c714be15ce094d83f1b989cdf5236be78419bfSimon Ulbricht let usd' = Unit_spec_defn usn usp' pos
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht genv = globalEnv dg'
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht then liftR (plain_error (itm, dg', libenv)
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (alreadyDefined usstr) pos)
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder else return (usd', dg'
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht { globalEnv = Map.insert usn (UnitEntry unitSig) genv },
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder Ref_spec_defn rn _ pos -> do
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder let rnstr = tokStr rn
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder analyzing opts $ "refinement "
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder ++ rnstr ++ "\n (refinement analysis not implemented yet)"
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder let genv = globalEnv dg
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder then liftR (plain_error (itm, dg, libenv)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder (alreadyDefined rnstr)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder else return ( itm, dg { globalEnv = Map.insert rn (RefEntry) genv }
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder Logic_decl (Logic_name logTok _) _ -> do
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder logNm <- lookupLogic "LOGIC DECLARATION:" (tokStr logTok) lgraph
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder putMessageIORes opts 1 $ "logic " ++ show logNm
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder return (itm, dg, libenv)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder Download_items ln items _ -> do
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder -- we take as the default logic for imported libs
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder -- the global default logic
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder (ln', libenv') <- anaLibFile lgraph opts libenv ln
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder if ln == ln' then case Map.lookup ln libenv' of
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Nothing -> error $ "Internal error: did not find library " ++
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder show ln ++ " available: " ++ show (Map.keys libenv')
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Just dg' -> do
993e01fc242fa58d3dcf1b3272cd411726817eeeSimon Ulbricht (genv1, dg1) <-
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder liftR $ foldM (ana_ITEM_NAME_OR_MAP libenv' ln $ globalEnv dg')
f3fb0e085030be5bc309d946a6a9c20736dd3e0fSimon Ulbricht (globalEnv dg, dg) items
f3fb0e085030be5bc309d946a6a9c20736dd3e0fSimon Ulbricht gannos'' <- liftR $ globalAnnos dg `mergeGlobalAnnos` globalAnnos dg'
f3fb0e085030be5bc309d946a6a9c20736dd3e0fSimon Ulbricht return (itm, dg1
f3fb0e085030be5bc309d946a6a9c20736dd3e0fSimon Ulbricht { globalAnnos = gannos''
f3fb0e085030be5bc309d946a6a9c20736dd3e0fSimon Ulbricht , globalEnv = genv1 }, libenv')
f3fb0e085030be5bc309d946a6a9c20736dd3e0fSimon Ulbricht else liftR $ fail $ "downloaded library '" ++ show ln'
116efc752fbf094a464c4f4940d9a450ab41c6c9Simon Ulbricht ++ "' does not match library name '" ++ shows ln "'"
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder-- ??? Needs to be generalized to views between different logics
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maederana_VIEW_DEFN :: LogicGraph -> LibEnv -> DGraph -> HetcatsOpts -> SIMPLE_ID
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder -> Result (LIB_ITEM, DGraph, LibEnv)
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maederana_VIEW_DEFN lgraph libenv dg opts vn gen vt gsis pos = do
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder let adj = adjustPos pos
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder (gen', GenericitySig imp params allparams, dg') <-
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder ana_GENERICITY lgraph dg opts (extName "VG" (makeName vn)) gen
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder (vt', (src, tar), dg'') <-
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maeder ana_VIEW_TYPE lgraph dg' allparams opts (makeName vn) vt
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder let gsigmaS = getSig src
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder gsigmaT = getSig tar
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder G_sign lidS sigmaS _ <- return gsigmaS
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder G_sign lidT sigmaT _ <- return gsigmaT
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder gsis1 <- adj $ homogenizeGM (Logic lidS) gsis
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder G_symb_map_items_list lid sis <- return gsis1
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder sigmaS' <- adj $ coerceSign lidS lid "" sigmaS
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder sigmaT' <- adj $ coerceSign lidT lid "" sigmaT
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder mor <- if isStructured opts then return (ext_ide lid sigmaS') else do
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder rmap <- adj $ stat_symb_map_items lid sis
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder adj $ ext_induced_from_to_morphism lid rmap sigmaS' sigmaT'
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder let nodeS = getNode src
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder nodeT = getNode tar
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder gmor = gEmbed (mkG_morphism lid mor)
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder vsig = ExtViewSig src gmor
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder $ ExtGenSig imp params (getMaybeSig allparams) tar
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder genv = globalEnv dg''
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder then plain_error (View_defn vn gen' vt' gsis pos, dg'', libenv)
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder (alreadyDefined $ tokStr vn)
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder else return (View_defn vn gen' vt' gsis pos,
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder (insLink dg'' gmor (GlobalThm LeftOpen None LeftOpen)
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder (DGView vn) nodeS nodeT) -- 'LeftOpen' for conserv correct?
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder { globalEnv = Map.insert vn (ViewEntry vsig) genv }
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder-- | analyze a VIEW_TYPE
de8eee2014437ec4020be15cd363257f87e79943Christian Maeder-- The first three arguments give the global context
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder-- The AnyLogic is the current logic
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder-- The NodeSig is the signature of the parameter of the view
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder-- flag, whether just the structure shall be analysed
5a448e9be8c4482a978b174b744237757335140fChristian Maederana_VIEW_TYPE :: LogicGraph -> DGraph -> MaybeNode -> HetcatsOpts
5a448e9be8c4482a978b174b744237757335140fChristian Maeder -> NodeName -> VIEW_TYPE
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder -> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maederana_VIEW_TYPE lg dg parSig opts name
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder (View_type aspSrc aspTar pos) = do
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder l <- lookupCurrentLogic "VIEW_TYPE" lg
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder (spSrc', srcNsig, dg') <- adjustPos pos $
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder ana_SPEC False lg dg (EmptyNode l) (extName "S" name) opts (item aspSrc)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder (spTar', tarNsig, dg'') <- adjustPos pos $
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder ana_SPEC True lg dg' parSig (extName "T" name) opts (item aspTar)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder return (View_type (replaceAnnoted spSrc' aspSrc)
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian Maeder (replaceAnnoted spTar' aspTar)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder (srcNsig, tarNsig), dg'')
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maederana_ITEM_NAME_OR_MAP :: LibEnv -> LIB_NAME -> GlobalEnv
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder -> (GlobalEnv, DGraph) -> ITEM_NAME_OR_MAP
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder -> Result (GlobalEnv, DGraph)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maederana_ITEM_NAME_OR_MAP libenv ln genv' res itm =
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder ana_ITEM_NAME_OR_MAP1 libenv ln genv' res $ case itm of
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder Item_name name -> (name, name)
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maeder Item_name_map old new _ -> (old, new)
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder-- | Auxiliary function for not yet implemented features
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maederana_err :: String -> a
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maederana_err f = error $ "*** Analysis of " ++ f ++ " is not yet implemented!"
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maederana_ITEM_NAME_OR_MAP1 :: LibEnv -> LIB_NAME -> GlobalEnv
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder -> (GlobalEnv, DGraph) -> (SIMPLE_ID, SIMPLE_ID)
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder -> Result (GlobalEnv, DGraph)
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maederana_ITEM_NAME_OR_MAP1 libenv ln genv' (genv, dg) (old, new) = do
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder entry <- maybeToResult nullRange
59fa2ed5a4936e7e56f7164d8a274df68dd4160cSimon Ulbricht (tokStr old ++ " not found") (Map.lookup old genv')
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder case Map.lookup new genv of
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder Nothing -> return ()
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder Just _ -> fail (tokStr new ++ " already used")
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder case entry of
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder SpecEntry extsig ->
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder let (dg1,extsig1) = refExtsig libenv ln dg (Just new) extsig
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder genv1 = Map.insert new (SpecEntry extsig1) genv
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder in return (genv1,dg1)
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder ViewEntry vsig ->
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder let (dg1,vsig1) = refViewsig libenv ln dg vsig
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder genv1 = Map.insert new (ViewEntry vsig1) genv
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder in return (genv1,dg1)
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder ArchEntry _asig -> ana_err "arch spec download"
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder UnitEntry _usig -> ana_err "unit spec download"
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder RefEntry -> ana_err "ref spec download"
142fd5dd7fcfa170f08b2a0ab232859428f6e3c2Christian MaederrefNodesig :: LibEnv -> LIB_NAME -> DGraph -> (Maybe SIMPLE_ID, NodeSig)
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder -> (DGraph, NodeSig)
7be1485dfcaa5decb3586d194ff4b2443668e349Simon UlbrichtrefNodesig libenv refln dg (name, NodeSig refn sigma@(G_sign lid sig ind)) =
7be1485dfcaa5decb3586d194ff4b2443668e349Simon Ulbricht let (ln, n) = getActualParent libenv refln refn
7be1485dfcaa5decb3586d194ff4b2443668e349Simon Ulbricht refInfo = newRefInfo ln n
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder node_contents = newInfoNodeLab (makeMaybeName name) refInfo
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder $ noSensGTheory lid sig ind
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder node = getNewNodeDG dg
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder in case lookupInAllRefNodesDG refInfo dg of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Just existNode -> (dg, NodeSig existNode sigma)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ( addToRefNodesDG node refInfo $ insNodeDG (node, node_contents) dg
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder , NodeSig node sigma)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder{- | get to the actual parent which is not a referenced node, so that
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder the small chains between nodes in different library can be advoided.
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (details see ticket 5)
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedergetActualParent :: LibEnv -> LIB_NAME -> Node -> (LIB_NAME, Node)
f675b8f0a612e37472640da57b48d795bef4427eChristian MaedergetActualParent libenv ln n =
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder let refLab = labDG (lookupDGraph ln libenv) n in
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder if isDGRef refLab then
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder -- recursively goes to parent of the current node, but
7a3e20d1b7fe1b0e47c0b9138716b0bbc8ecf1f6Christian Maeder -- it actually would only be done once
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder getActualParent libenv (dgn_libname refLab) (dgn_node refLab)
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederrefNodesigs :: LibEnv -> LIB_NAME -> DGraph -> [(Maybe SIMPLE_ID, NodeSig)]
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder -> (DGraph, [NodeSig])
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederrefNodesigs libenv ln = mapAccumR (refNodesig libenv ln)
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederrefExtsig :: LibEnv -> LIB_NAME -> DGraph -> Maybe SIMPLE_ID -> ExtGenSig
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder -> (DGraph, ExtGenSig)
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederrefExtsig libenv ln dg name (ExtGenSig imps params gsigmaP body) = let
be9d4ffdd00c0665f9c25a4a905b0a0bf0c90bbfChristian Maeder params' = map (\x -> (Nothing,x)) params
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (dg0, body1) = refNodesig libenv ln dg (name, body)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (dg1, params1) = refNodesigs libenv ln dg0 params'
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (dg2, imps1) = case imps of
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder EmptyNode _ -> (dg1, imps)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder JustNode ns -> let
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (dg3, nns) = refNodesig libenv ln dg1 (Nothing, ns)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder in (dg3, JustNode nns)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder in (dg2, ExtGenSig imps1 params1 gsigmaP body1)
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederrefViewsig :: LibEnv -> LIB_NAME -> DGraph -> ExtViewSig
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder -> (DGraph, ExtViewSig)
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederrefViewsig libenv ln dg (ExtViewSig src mor extsig) = let
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (_,[src1]) = refNodesigs libenv ln dg [(Nothing, src)]
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (dg2, extsig1) = refExtsig libenv ln dg Nothing extsig
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder in (dg2, ExtViewSig src1 mor extsig1)