AnalysisLibrary.hs revision e6d40133bc9f858308654afb1262b8b483ec5922
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : static analysis of CASL specification libraries
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiMaintainer : till@tzi.de
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable(Logic)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStatic analysis of CASL specification libraries
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder Follows the verification semantics sketched in Chap. IV:6
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder of the CASL Reference Manual.
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Generalization to heterogeneous views
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder check that libname coincides with filename (otherwise internal error occurs)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , ana_LIB_DEFN
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Common.AS_Annotation hiding (isAxiom, isDef)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Common.Lib.Map as Map
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- | lookup an env or read and analyze a file
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaLib :: HetcatsOpts -> FilePath -> IO (Maybe (LIB_NAME, LibEnv))
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaLib opts file = anaLibExt opts file emptyLibEnv
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- | read a file and extended the current library environment
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaLibExt :: HetcatsOpts -> FilePath -> LibEnv -> IO (Maybe (LIB_NAME, LibEnv))
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederanaLibExt opts file libEnv = do
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder defl <- lookupLogic "logic from command line: "
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder (defLogic opts) logicGraph
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder Result ds res <- runResultT $ anaLibFileOrGetEnv logicGraph defl opts
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder libEnv (fileToLibName opts file) file
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder showDiags opts ds
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder Nothing -> return Nothing
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just (ln, lenv) -> do
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder let nEnv = if hasPrfOut opts then automatic ln lenv else lenv
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder gctx = lookupGlobalContext ln nEnv
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder ga = globalAnnos gctx
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder writeSpecFiles opts file nEnv ga (ln, globalEnv gctx)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski putIfVerbose opts 3 $ showGlobalDoc ga ga ""
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang return $ Just (ln, nEnv)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- | parsing and static analysis for files
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- Parameters: logic graph, default logic, file name
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian MaederanaSourceFile :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> FilePath
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang -> ResultT IO (LIB_NAME, LibEnv)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaederanaSourceFile lgraph defl opts libenv fname = ResultT $ do
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder fname' <- existsAnSource opts fname
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case fname' of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Nothing -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ fail $ "a file for input '" ++ fname ++ "' not found."
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder if any (flip isSuffixOf file) [envSuffix, prfSuffix] then
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let file' = rmSuffix file in
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder runResultT $ anaLibFileOrGetEnv lgraph defl opts libenv
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder (fileToLibName opts file') file'
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder input <- readFile file
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich putIfVerbose opts 2 $ "Reading file " ++ file
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder runResultT $ anaString lgraph defl opts libenv input file
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | parsing and static analysis for string (=contents of file)
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu-- Parameters: logic graph, default logic, contents of file, filename
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederanaString :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder -> FilePath -> ResultT IO (LIB_NAME, LibEnv)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederanaString lgraph defl opts libenv input file =
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder let Result ds mast = read_LIB_DEFN_M lgraph defl opts file input
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in case mast of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just ast@(Lib_defn ln _ _ ans) -> case analysis opts of
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder lift $ putIfVerbose opts 1 $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "Skipping static analysis of library " ++ show ln
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ga <- liftR $ addGlobalAnnos emptyGlobalAnnos ans
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder case gui opts of
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder Only -> return ()
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder _ -> lift $ write_LIB_DEFN ga file opts ast
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder liftR $ Result ds Nothing
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder if ln == fileToLibName opts file
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder then return ()
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder else showDiags1 opts $ liftR $ Result [mkDiag Warning
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder ("file name '" ++ file
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder ++ "' does not match library name") $ getLIB_ID ln]
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder lift $ putIfVerbose opts 1 $ "Analyzing library " ++ show ln
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (_,ld,_,lenv) <-
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder ana_LIB_DEFN lgraph defl opts libenv ast
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder case Map.lookup ln lenv of
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Nothing -> error $ "anaString: missing library: " ++ show ln
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Just gctx -> lift $ do
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder case gui opts of
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Only -> return ()
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder _ -> write_LIB_DEFN (globalAnnos gctx) file opts ld
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder when (hasEnvOut opts)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (writeFileInfo opts ln file ld gctx)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder return (ln, lenv)
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder Nothing -> liftR $ Result ds Nothing
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederanaLibFile :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> LIB_NAME
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder -> ResultT IO (LIB_NAME, LibEnv)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederanaLibFile lgraph defl opts libenv ln =
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder let lnstr = show ln in case Map.lookup ln libenv of
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder analyzing opts $ "from " ++ lnstr
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder return (ln, libenv)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Nothing -> do
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder putMessageIORes opts 1 $ "Downloading " ++ lnstr ++ " ..."
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder res <- anaLibFileOrGetEnv lgraph defl
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder (if recurse opts then opts else opts { outtypes = [] })
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder libenv ln $ libNameToFile opts ln
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder putMessageIORes opts 1 $ "... loaded " ++ lnstr
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederanaLibFileOrGetEnv :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> LIB_NAME -> FilePath -> ResultT IO (LIB_NAME, LibEnv)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederanaLibFileOrGetEnv lgraph defl opts libenv libname file = ResultT $ do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder let env_file = rmSuffix file ++ envSuffix
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder recent_env_file <- checkRecentEnv opts env_file file
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder if recent_env_file
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mgc <- readVerbose opts libname env_file
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Nothing -> runResultT $ do
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder lift $ putIfVerbose opts 1 $ "Deleting " ++ env_file
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder anaSourceFile lgraph defl opts libenv file
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Just (ld, gc) -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder write_LIB_DEFN (globalAnnos gc) file opts ld
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -- get all DGRefs from DGraph
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Result ds mEnv <- runResultT $ foldl
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ( \ ioLibEnv labDG -> case snd labDG of
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder DGRef { dgn_libname = ln } -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder p_libEnv <- ioLibEnv
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder if Map.member ln p_libEnv then
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return p_libEnv
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder else fmap snd $ anaLibFile lgraph defl
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski opts p_libEnv ln
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> ioLibEnv)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (return $ Map.insert libname gc libenv)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder $ labNodes $ devGraph gc
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return $ Result ds $ fmap
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ( \ rEnv -> (libname, rEnv)) mEnv
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder else runResultT $ anaSourceFile lgraph defl opts libenv file
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- | analyze a LIB_DEFN
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- Parameters: logic graph, default logic, opts, library env, LIB_DEFN
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder-- call this function as follows:
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- do Result diags res <- runResultT (ana_LIB_DEFN ...)
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder-- mapM_ (putStrLn . show) diags
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederana_LIB_DEFN :: LogicGraph -> AnyLogic -> HetcatsOpts
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> LibEnv -> LIB_DEFN
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> ResultT IO (LIB_NAME,LIB_DEFN,DGraph,LibEnv)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederana_LIB_DEFN lgraph defl opts libenv (Lib_defn ln alibItems pos ans) = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder gannos <- showDiags1 opts $ liftR $ addGlobalAnnos emptyGlobalAnnos ans
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (libItems', gctx, _, libenv') <-
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder foldl ana (return ([], emptyGlobalContext { globalAnnos = gannos }
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder , defl, libenv))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (map item alibItems)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (map (uncurry replaceAnnoted)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (zip (reverse libItems') alibItems))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski devGraph gctx,
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Map.insert ln gctx libenv')
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder ana res1 libItem = do
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder (libItems',gctx1,l1,libenv1) <- res1
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Result diags2 res <-
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz runResultT $ ana_LIB_ITEM lgraph defl opts libenv1 gctx1 l1 libItem
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder runResultT $ showDiags1 opts (liftR (Result diags2 res))
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder if outputToStdout opts then
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz if hasErrors diags2 then
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder fail "Stopped due to errors"
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder else case res of
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Just (libItem',gctx1',l1',libenv1') ->
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder return (return (libItem':libItems',gctx1',l1',libenv1'))
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Nothing -> fail "Stopped. No result available"
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maeder --result1 <- runResultT res1
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maeder --let diags1 = diags result1
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder if hasErrors diags2 then
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder runResultT $ liftR (Result (diags2) Nothing)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz else case res of
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz Just (libItem',gctx1',l1',libenv1') ->
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return ((return (libItem':libItems',gctx1',l1',libenv1'))
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz {diags = diags2})
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz Nothing -> return $ fail "Stopped. No result available"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederputMessageIORes :: HetcatsOpts -> Int -> String -> ResultT IO ()
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederputMessageIORes opts i msg =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder if outputToStdout opts
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder then lift $ putIfVerbose opts i msg
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder else liftR $ message () msg
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederanalyzing :: HetcatsOpts -> String -> ResultT IO ()
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederanalyzing opts msg = putMessageIORes opts 1 $ "Analyzing " ++ msg
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederalreadyDefined :: String -> String
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederalreadyDefined str = "Name " ++ str ++ " already defined"
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder-- analyse a LIB_ITEM
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- Parameters: logic graph, default logic, opts, library env
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- global context, current logic, LIB_ITEM
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederana_LIB_ITEM :: LogicGraph -> AnyLogic -> HetcatsOpts
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> LibEnv -> GlobalContext -> AnyLogic
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder -> ResultT IO (LIB_ITEM,GlobalContext,AnyLogic,LibEnv)
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maederana_LIB_ITEM lgraph _defl opts libenv gctx l
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (Spec_defn spn gen asp pos) = do
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let spstr = tokStr spn
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder analyzing opts $ "spec " ++ spstr
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (gen',(imp,params,allparams),dg') <-
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder liftR (ana_GENERICITY lgraph gctx l opts
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (extName "P" (makeName spn)) gen)
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder (sp',body,dg'') <-
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder liftR (ana_SPEC lgraph dg'
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder allparams (makeName spn) opts (item asp))
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder genv = globalEnv gctx
4e144aa4be1f50519f8fa377a7883edfbc76d406Christian Maeder then liftR (plain_error (libItem', dg'', l, libenv)
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder (alreadyDefined spstr)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder else return (libItem',
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder dg'' { globalEnv = Map.insert spn (SpecEntry
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (imp, params, getMaybeSig allparams, body)) genv }
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederana_LIB_ITEM lgraph defl opts libenv gctx l
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (View_defn vn gen vt gsis pos) = do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder analyzing opts $ "view " ++ tokStr vn
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder liftR (ana_VIEW_DEFN lgraph defl libenv gctx l opts
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder vn gen vt gsis pos)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- architectural specification
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederana_LIB_ITEM lgraph defl opts libenv gctx l
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder (Arch_spec_defn asn asp pos) = do
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let asstr = tokStr asn
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder analyzing opts $ "arch spec " ++ asstr
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder (archSig, gctx', asp') <- liftR (ana_ARCH_SPEC lgraph defl gctx l opts
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let asd' = Arch_spec_defn asn (replaceAnnoted asp' asp) pos
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski genv = globalEnv gctx'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder liftR (plain_error (asd', gctx', l, libenv)
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (alreadyDefined asstr)
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder return (asd', gctx'
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder { globalEnv = Map.insert asn (ArchEntry archSig) genv },
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder-- unit specification
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederana_LIB_ITEM lgraph defl opts libenv gctx l
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder usd@(Unit_spec_defn usn usp pos) = do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let usstr = tokStr usn
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder analyzing opts $ "unit spec " ++ usstr
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder (unitSig, gctx', usp') <- liftR (ana_UNIT_SPEC lgraph defl gctx l opts
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (EmptyNode defl) usp)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let usd' = Unit_spec_defn usn usp' pos
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder genv = globalEnv gctx'
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder liftR (plain_error (usd, gctx', l, libenv)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (alreadyDefined usstr)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return (usd', gctx'
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder { globalEnv = Map.insert usn (UnitEntry unitSig) genv },
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder-- refinement specification
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maederana_LIB_ITEM _lgraph _defl opts libenv gctx l
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder rd@(Ref_spec_defn rn _ pos) = do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let rnstr = tokStr rn
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder analyzing opts $ "refinement "
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ++ rnstr ++ "\n (refinement analysis not implemented yet)"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder genv = globalEnv gctx
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder liftR (plain_error (rd, gctx, l, libenv)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (alreadyDefined rnstr)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return (rd', gctx { globalEnv = Map.insert rn (RefEntry) genv }
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder-- logic declaration
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maederana_LIB_ITEM lgraph _defl opts libenv gctx _l
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder (Logic_decl ln@(Logic_name logTok _) pos) = do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder logNm <- lookupLogic "LOGIC DECLARATION:" (tokStr logTok) lgraph
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski putMessageIORes opts 1 $ "logic " ++ show logNm
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return (Logic_decl ln pos,gctx,logNm,libenv)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederana_LIB_ITEM lgraph defl opts libenv gctx l
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder libItem@(Download_items ln items _) = do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- we take as the default logic for imported libs
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -- the global default logic
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder (ln', libenv') <- anaLibFile lgraph defl opts libenv ln
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder if ln == ln' then case Map.lookup ln libenv' of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> error $ "Internal error: did not find library " ++
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder show ln ++ " available: " ++ show (Map.keys libenv')
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just gctx' -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (genv1,dg1) <- liftR (foldl (ana_ITEM_NAME_OR_MAP ln
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder $ globalEnv gctx')
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (return (globalEnv gctx, devGraph gctx))
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder gannos'' <- liftR $
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder globalAnnos gctx `mergeGlobalAnnos` globalAnnos gctx'
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder return (libItem, gctx
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder { globalAnnos = gannos''
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder , globalEnv = genv1
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder , devGraph = dg1 }, l, libenv')
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else liftR $ fail $ "downloaded library '" ++ show ln'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ++ "' does not match library name '" ++ shows ln "'"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- ??? Needs to be generalized to views between different logics
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederana_VIEW_DEFN :: LogicGraph -> AnyLogic -> LibEnv -> GlobalContext
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> AnyLogic -> HetcatsOpts -> SIMPLE_ID
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> Result (LIB_ITEM, GlobalContext, AnyLogic, LibEnv)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederana_VIEW_DEFN lgraph _defl libenv gctx l opts
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder vn gen vt gsis pos = do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let adj = adjustPos pos
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (gen',(imp,params,allparams),dg') <-
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ana_GENERICITY lgraph gctx l opts (extName "VG" (makeName vn)) gen
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (vt', (src,tar), gctx'') <-
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ana_VIEW_TYPE lgraph dg' l allparams opts
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (makeName vn) vt
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let gsigmaS = getSig src
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder gsigmaT = getSig tar
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder dg'' = devGraph gctx''
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder G_sign lidS sigmaS _ <- return gsigmaS
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder G_sign lidT sigmaT _ <- return gsigmaT
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder gsis1 <- adj $ homogenizeGM (Logic lidS) gsis
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder G_symb_map_items_list lid sis <- return gsis1
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder sigmaS' <- adj $ coerceSign lidS lid "" sigmaS
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder sigmaT' <- adj $ coerceSign lidT lid "" sigmaT
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder mor <- if isStructured opts then return (ide lid sigmaS')
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rmap <- adj $ stat_symb_map_items lid sis
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder adj $ induced_from_to_morphism lid rmap sigmaS' sigmaT'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let nodeS = getNode src
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder nodeT = getNode tar
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder gmor = gEmbed (G_morphism lid mor 0)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder link = (nodeS,nodeT,DGLink {
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder dgl_morphism = gmor,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- 'LeftOpen' for conserv correct?
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder dgl_origin = DGView vn})
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder vsig = (src,gmor,(imp,params,getMaybeSig allparams,tar))
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder genv = globalEnv gctx''
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder then plain_error (View_defn vn gen' vt' gsis pos, gctx'', l, libenv)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (alreadyDefined $ tokStr vn)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else return (View_defn vn gen' vt' gsis pos,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder gctx'' { globalEnv = Map.insert vn (ViewEntry vsig) genv
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder , devGraph = insEdge link dg''}, l, libenv)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederana_ITEM_NAME_OR_MAP :: LIB_NAME -> GlobalEnv -> Result (GlobalEnv, DGraph)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> ITEM_NAME_OR_MAP -> Result (GlobalEnv, DGraph)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederana_ITEM_NAME_OR_MAP ln genv' res (Item_name name) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ana_ITEM_NAME_OR_MAP1 ln genv' res name name
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederana_ITEM_NAME_OR_MAP ln genv' res (Item_name_map old new _) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ana_ITEM_NAME_OR_MAP1 ln genv' res old new
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederana_ITEM_NAME_OR_MAP1 :: LIB_NAME -> GlobalEnv -> Result (GlobalEnv, DGraph)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> SIMPLE_ID -> SIMPLE_ID
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> Result (GlobalEnv, DGraph)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maederana_ITEM_NAME_OR_MAP1 ln genv' res old new = do
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (genv,dg) <- res
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder entry <- maybeToResult nullRange
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (tokStr old ++ " not found") (Map.lookup old genv')
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder case Map.lookup new genv of
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Nothing -> return ()
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Just _ -> fail (tokStr new ++ " already used")
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder case entry of
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder SpecEntry extsig ->
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let (dg1,extsig1) = refExtsig ln dg (Just new) extsig
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder genv1 = Map.insert new (SpecEntry extsig1) genv
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder in return (genv1,dg1)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ViewEntry vsig ->
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let (dg1,vsig1) = refViewsig ln dg vsig
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder genv1 = Map.insert new (ViewEntry vsig1) genv
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder in return (genv1,dg1)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ArchEntry _asig -> ana_err "arch spec download"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder UnitEntry _usig -> ana_err "unit spec download"
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder RefEntry -> ana_err "ref spec download"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrefNodesig :: LIB_NAME -> DGraph -> (Maybe SIMPLE_ID, NodeSig)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder -> (DGraph, NodeSig)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederrefNodesig ln dg (name, NodeSig n sigma@(G_sign lid sig ind)) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let node_contents = DGRef {
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder dgn_name = makeMaybeName name,
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder dgn_libname = ln,
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder dgn_node = n,
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder dgn_theory = G_theory lid sig ind noSens 0,
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder dgn_nf = Nothing,
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder dgn_sigma = Nothing
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder node = getNewNode dg
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder in (insNode (node,node_contents) dg, NodeSig node sigma)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskirefNodesigs :: LIB_NAME -> DGraph -> [(Maybe SIMPLE_ID, NodeSig)]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> (DGraph, [NodeSig])
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederrefNodesigs ln = mapAccumR (refNodesig ln)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaederrefExtsig :: LIB_NAME -> DGraph -> Maybe SIMPLE_ID -> ExtGenSig
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder -> (DGraph, ExtGenSig)
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian MaederrefExtsig ln dg name (imps,params,gsigmaP,body) =
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder params' = map (\x -> (Nothing,x)) params
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (dg0, body1) = refNodesig ln dg (name, body)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (dg1, params1) = refNodesigs ln dg0 params'
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder (dg2, imps1) = case imps of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder EmptyNode _ -> (dg1, imps)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder JustNode ns -> let
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (dg3, nns) = refNodesig ln dg1 (Nothing, ns)
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder in (dg3, JustNode nns)
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder in (dg2,(imps1,params1,gsigmaP,body1))
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaederrefViewsig :: LIB_NAME -> DGraph -> (NodeSig, t1, ExtGenSig)
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder -> (DGraph, (NodeSig, t1, ExtGenSig))
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaederrefViewsig ln dg (src,mor,extsig) =
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder (dg2,(src1,mor,extsig1))
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder (_,[src1]) = refNodesigs ln dg [(Nothing,src)]
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder (dg2,extsig1) = refExtsig ln dg Nothing extsig