AnalysisLibrary.hs revision 3ea571db6dd6e0c42d02de4e56648c7cd86a3734
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweModule : $Header$
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweDescription : static analysis of CASL specification libraries
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweMaintainer : till@informatik.uni-bremen.de
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweStability : provisional
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowePortability : non-portable(Logic)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweStatic analysis of CASL specification libraries
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Follows the verification semantics sketched in Chap. IV:6
ead9bb4b1be81d7bbf8ed86ee41d6c1e58b069a3Yuri Pankov of the CASL Reference Manual.
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , ana_LIB_DEFN
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport Common.AS_Annotation hiding (isAxiom, isDef)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport qualified Data.Map as Map
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | lookup an env or read and analyze a file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLib :: HetcatsOpts -> FilePath -> IO (Maybe (LIB_NAME, LibEnv))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLib opts fname = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe fname' <- existsAnSource opts {intype = GuessIn} $ rmSuffix fname
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case fname' of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> anaLibExt opts fname emptyLibEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just file ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if isSuffixOf prfSuffix file then do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe putIfVerbose opts 0 $ "a matching source file for proof history '"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ++ file ++ "' not found."
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return Nothing
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else anaLibExt opts file emptyLibEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | read a file and extended the current library environment
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibExt :: HetcatsOpts -> FilePath -> LibEnv -> IO (Maybe (LIB_NAME, LibEnv))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibExt opts file libEnv = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe defl <- lookupLogic "logic from command line: "
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (defLogic opts) logicGraph
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Result ds res <- runResultT $ anaLibFileOrGetEnv logicGraph defl opts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe libEnv (fileToLibName opts file) file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe showDiags opts ds
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> return Nothing
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just (ln, lenv) -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let nEnv = if hasPrfOut opts then automatic ln lenv else lenv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dg = lookupDGraph ln nEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ga = globalAnnos dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe writeSpecFiles opts file nEnv ga (ln, globalEnv dg)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe putIfVerbose opts 3 $ showGlobalDoc ga ga ""
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return $ Just (ln, nEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | parsing and static analysis for files
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- Parameters: logic graph, default logic, file name
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaSourceFile :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> FilePath
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> ResultT IO (LIB_NAME, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaSourceFile lgraph defl opts libenv fname = ResultT $ do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe fname' <- existsAnSource opts {intype = GuessIn} fname
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case fname' of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return $ fail $ "a file for input '" ++ fname ++ "' not found."
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just file ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if any (flip isSuffixOf file) [envSuffix, prfSuffix] then
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe fail $ "a matching source file for '" ++ fname ++ "' not found."
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe curDir <- getCurrentDirectory
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe input <- readFile file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe mt <- getModificationTime file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- when switching to ghc 6.6.1 with System.FilePath use:
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- combine curDir file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let absolutePath = if "/" `isPrefixOf` file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else curDir ++ '/':file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe putIfVerbose opts 2 $ "Reading file " ++ absolutePath
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe runResultT $ anaString lgraph defl opts libenv input absolutePath mt
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | parsing and static analysis for string (=contents of file)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- Parameters: logic graph, default logic, contents of file, filename
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaString :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> FilePath -> ClockTime -> ResultT IO (LIB_NAME, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaString lgraph defl opts libenv input file mt =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let Result ds mast = read_LIB_DEFN_M lgraph defl opts file input mt
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in case mast of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just ast@(Lib_defn ln _ _ ans) -> case analysis opts of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe lift $ putIfVerbose opts 1 $
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe "Skipping static analysis of library " ++ show ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ga <- liftR $ addGlobalAnnos emptyGlobalAnnos ans
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case gui opts of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Only -> return ()
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe _ -> lift $ write_LIB_DEFN ga file opts ast
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe liftR $ Result ds Nothing
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let libstring = show $ getLIB_ID ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if libstring == libraryS then return ()
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if isSuffixOf libstring (rmSuffix file) then return () else
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe lift $ putIfVerbose opts 1 $
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe "### file name '" ++ file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ++ "' does not match library name '" ++
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe libstring ++ "'"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe lift $ putIfVerbose opts 1 $ "Analyzing library " ++ show ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (_,ld, _, lenv) <- ana_LIB_DEFN lgraph defl opts libenv ast
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case Map.lookup ln lenv of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> error $ "anaString: missing library: " ++ show ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just dg -> lift $ do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case gui opts of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Only -> return ()
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe _ -> write_LIB_DEFN (globalAnnos dg) file opts ld
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe when (hasEnvOut opts)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (writeFileInfo opts ln file ld dg)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (ln, lenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> liftR $ Result ds Nothing
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibFile :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> LIB_NAME
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> ResultT IO (LIB_NAME, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibFile lgraph defl opts libenv ln =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let lnstr = show ln in case Map.lookup ln libenv of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just _ -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe analyzing opts $ "from " ++ lnstr
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (ln, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe putMessageIORes opts 1 $ "Downloading " ++ lnstr ++ " ..."
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe res <- anaLibFileOrGetEnv lgraph defl
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (if recurse opts then opts else opts { outtypes = [] })
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe libenv ln $ libNameToFile opts ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe putMessageIORes opts 1 $ "... loaded " ++ lnstr
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibFileOrGetEnv :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> LIB_NAME -> FilePath -> ResultT IO (LIB_NAME, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibFileOrGetEnv lgraph defl opts libenv libname file = ResultT $ do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let env_file = rmSuffix file ++ envSuffix
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe recent_env_file <- checkRecentEnv opts env_file file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if recent_env_file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe mgc <- readVerbose opts libname env_file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> runResultT $ do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe lift $ putIfVerbose opts 1 $ "Deleting " ++ env_file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe anaSourceFile lgraph defl opts libenv file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just (ld, gc) -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe write_LIB_DEFN (globalAnnos gc) file opts ld
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- get all DGRefs from DGraph
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Result ds mEnv <- runResultT $ foldl
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ( \ ioLibEnv labOfDG -> let node = snd labOfDG in
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if isDGRef node then do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let ln = dgn_libname node
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe p_libEnv <- ioLibEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if Map.member ln p_libEnv then
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return p_libEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else fmap snd $ anaLibFile lgraph defl
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe opts p_libEnv ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else ioLibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (return $ Map.insert libname gc libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ labNodesDG gc
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return $ Result ds $ fmap
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ( \ rEnv -> (libname, rEnv)) mEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else runResultT $ anaSourceFile lgraph defl opts libenv file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | analyze a LIB_DEFN
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- Parameters: logic graph, default logic, opts, library env, LIB_DEFN
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- call this function as follows:
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- do Result diags res <- runResultT (ana_LIB_DEFN ...)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- mapM_ (putStrLn . show) diags
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_LIB_DEFN :: LogicGraph -> AnyLogic -> HetcatsOpts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> LibEnv -> LIB_DEFN
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> ResultT IO (LIB_NAME,LIB_DEFN,DGraph,LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_LIB_DEFN lgraph defl opts libenv (Lib_defn ln alibItems pos ans) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gannos <- showDiags1 opts $ liftR $ addGlobalAnnos emptyGlobalAnnos ans
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (libItems', dg, _, libenv') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe foldl ana (do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dg <- lift $ emptyDGwithMVar
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return ([], dg { globalAnnos = gannos }, defl, libenv))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (map item alibItems)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (map (uncurry replaceAnnoted)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (zip (reverse libItems') alibItems))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Map.insert ln dg libenv')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana res1 libItem = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (libItems',dg1,l1,libenv1) <- res1
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let newLG = case libItems' of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Logic_decl (Logic_name logTok _) _ : _ ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe lgraph { currentLogic = tokStr logTok }
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Result diags2 res <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe runResultT $ ana_LIB_ITEM newLG defl opts libenv1 dg1 l1 libItem
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe runResultT $ showDiags1 opts (liftR (Result diags2 res))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if outputToStdout opts then
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if hasErrors diags2 then
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe fail "Stopped due to errors"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else case res of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just (libItem',dg1',l1',libenv1') ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (return (libItem':libItems',dg1',l1',libenv1'))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> fail "Stopped. No result available"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe --result1 <- runResultT res1
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe --let diags1 = diags result1
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if hasErrors diags2 then
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe runResultT $ liftR (Result (diags2) Nothing)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else case res of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just (libItem',dg1',l1',libenv1') ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return ((return (libItem':libItems',dg1',l1',libenv1'))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe {diags = diags2})
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> return $ fail "Stopped. No result available"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweputMessageIORes :: HetcatsOpts -> Int -> String -> ResultT IO ()
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweputMessageIORes opts i msg =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if outputToStdout opts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe then lift $ putIfVerbose opts i msg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else liftR $ message () msg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweanalyzing :: HetcatsOpts -> String -> ResultT IO ()
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweanalyzing opts msg = putMessageIORes opts 1 $ "Analyzing " ++ msg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowealreadyDefined :: String -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowealreadyDefined str = "Name " ++ str ++ " already defined"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | analyze a GENERICITY
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_GENERICITY :: LogicGraph -> DGraph -> AnyLogic -> HetcatsOpts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> NODE_NAME -> GENERICITY
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (GENERICITY, GenericitySig, DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_GENERICITY lg dg l opts name
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gen@(Genericity params@(Params psps) imps@(Imported isps) pos) =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case psps of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [] -> do -- no parameter ...
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe when (not (null isps))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (plain_error () "Parameterless specifications must not have imports"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (gen, (EmptyNode l, [], EmptyNode l), dg)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (imps',nsigI,dg') <- ana_IMPORTS lg dg l opts (extName "I" name) imps
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case psps of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [asp] -> do -- one parameter ...
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sp', nsigP, dg'') <- ana_SPEC lg dg' nsigI name opts (item asp)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (Genericity (Params [replaceAnnoted sp' asp]) imps' pos,
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (nsigI, [nsigP], JustNode nsigP), dg'')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe _ -> do -- ... and more parameters
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (params',nsigPs,dg'') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_PARAMS lg dg' nsigI opts (inc name) params
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let adj = adjustPos pos
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gsigmaP <- adj $ gsigManyUnion lg (map getSig nsigPs)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe G_sign lidP gsigP indP <- return gsigmaP
5dbfd19ad5fcc2b779f40f80fa05c1bd28fd0b4eTheo Schlossnagle let node_contents = newNodeLab name DGFormalParams
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ noSensGTheory lidP gsigP indP
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe node = getNewNodeDG dg''
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dg''' = insNodeDG (node,node_contents) dg''
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe inslink dgres (NodeSig n sigma) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dgl <- dgres
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe incl <- adj $ ginclusion lg sigma gsigmaP
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (insLEdgeNubDG (n,node,DGLink
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe { dgl_morphism = incl
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , dgl_type = GlobalDef
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , dgl_origin = DGFormalParams
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , dgl_id = defaultEdgeID
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dg4 <- foldl inslink (return dg''') nsigPs
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (Genericity params' imps' pos,
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (nsigI, nsigPs, JustNode $ NodeSig node gsigmaP), dg4)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_PARAMS :: LogicGraph -> DGraph -> MaybeNode
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> HetcatsOpts -> NODE_NAME -> PARAMS
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (PARAMS, [NodeSig], DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_PARAMS lg dg nsigI opts name (Params asps) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sps',pars,dg',_) <- foldl ana (return ([], [], dg, name))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ map item asps
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (Params (map (uncurry replaceAnnoted)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (zip (reverse sps') asps)),
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe reverse pars, dg')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana res sp = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sps',pars,dg1,n) <- res
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sp',par,dg') <- ana_SPEC lg dg1 nsigI n opts sp
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (sp':sps',par:pars,dg',inc n)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_IMPORTS :: LogicGraph -> DGraph -> AnyLogic -> HetcatsOpts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> NODE_NAME -> IMPORTED -> Result (IMPORTED, MaybeNode, DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_IMPORTS lg dg l opts name imps@(Imported asps) = case asps of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [] -> return (imps, EmptyNode l, dg)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let sp = Union asps nullRange
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (Union asps' _, nsig', dg') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_SPEC lg dg (EmptyNode l) name opts sp
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (Imported asps', JustNode nsig', dg')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- ??? emptyExplicit stuff needs to be added here
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | analyse a LIB_ITEM
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_LIB_ITEM :: LogicGraph -> AnyLogic -> HetcatsOpts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> LibEnv -> DGraph -> AnyLogic
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> ResultT IO (LIB_ITEM, DGraph, AnyLogic, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_LIB_ITEM lgraph defl opts libenv dg l itm = case itm of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Spec_defn spn gen asp pos -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let spstr = tokStr spn
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe analyzing opts $ "spec " ++ spstr
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (gen', (imp, params, allparams), dg') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe liftR (ana_GENERICITY lgraph dg l opts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (extName "P" (makeName spn)) gen)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sp', body, dg'') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe liftR (ana_SPEC lgraph dg'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe allparams (makeName spn) opts (item asp))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe genv = globalEnv dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe then liftR (plain_error (libItem', dg'', l, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (alreadyDefined spstr) pos)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else return (libItem',
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dg'' { globalEnv = Map.insert spn (SpecEntry
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (imp, params, getMaybeSig allparams, body)) genv }
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , l, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe View_defn vn gen vt gsis pos -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe analyzing opts $ "view " ++ tokStr vn
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe liftR (ana_VIEW_DEFN lgraph libenv dg l opts vn gen vt gsis pos)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Arch_spec_defn asn asp pos -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let asstr = tokStr asn
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe analyzing opts $ "arch spec " ++ asstr
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (archSig, dg', asp') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe liftR (ana_ARCH_SPEC lgraph defl dg l opts (item asp))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let asd' = Arch_spec_defn asn (replaceAnnoted asp' asp) pos
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe genv = globalEnv dg'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe then liftR (plain_error (asd', dg', l, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (alreadyDefined asstr) pos)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else return (asd', dg'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe { globalEnv = Map.insert asn (ArchEntry archSig) genv },
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Unit_spec_defn usn usp pos -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let usstr = tokStr usn
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe analyzing opts $ "unit spec " ++ usstr
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (unitSig, dg', usp') <- liftR (ana_UNIT_SPEC lgraph defl dg l opts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (EmptyNode l) usp)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let usd' = Unit_spec_defn usn usp' pos
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe genv = globalEnv dg'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe then liftR (plain_error (itm, dg', l, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (alreadyDefined usstr) pos)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else return (usd', dg'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe { globalEnv = Map.insert usn (UnitEntry unitSig) genv },
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Ref_spec_defn rn _ pos -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let rnstr = tokStr rn
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe analyzing opts $ "refinement "
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ++ rnstr ++ "\n (refinement analysis not implemented yet)"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let genv = globalEnv dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe then liftR (plain_error (itm, dg, l, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (alreadyDefined rnstr)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else return ( itm, dg { globalEnv = Map.insert rn (RefEntry) genv }
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , l, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Logic_decl (Logic_name logTok _) _ -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe logNm <- lookupLogic "LOGIC DECLARATION:" (tokStr logTok) lgraph
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe putMessageIORes opts 1 $ "logic " ++ show logNm
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (itm, dg, logNm, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Download_items ln items _ -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- we take as the default logic for imported libs
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- the global default logic
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (ln', libenv') <- anaLibFile lgraph defl opts libenv ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if ln == ln' then case Map.lookup ln libenv' of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> error $ "Internal error: did not find library " ++
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe show ln ++ " available: " ++ show (Map.keys libenv')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just dg' -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (genv1,dg1) <- liftR (foldl (ana_ITEM_NAME_OR_MAP libenv' ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ globalEnv dg')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (return (globalEnv dg, dg))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gannos'' <- liftR $ globalAnnos dg `mergeGlobalAnnos` globalAnnos dg'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (itm, dg1
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe { globalAnnos = gannos''
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , globalEnv = genv1 }, l, libenv')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else liftR $ fail $ "downloaded library '" ++ show ln'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ++ "' does not match library name '" ++ shows ln "'"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- ??? Needs to be generalized to views between different logics
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_VIEW_DEFN :: LogicGraph -> LibEnv -> DGraph
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> AnyLogic -> HetcatsOpts -> SIMPLE_ID
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (LIB_ITEM, DGraph, AnyLogic, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_VIEW_DEFN lgraph libenv dg l opts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe vn gen vt gsis pos = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let adj = adjustPos pos
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (gen',(imp,params,allparams),dg') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_GENERICITY lgraph dg l opts (extName "VG" (makeName vn)) gen
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (vt', (src,tar), dg'') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_VIEW_TYPE lgraph dg' l allparams opts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (makeName vn) vt
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let gsigmaS = getSig src
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gsigmaT = getSig tar
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe G_sign lidS sigmaS _ <- return gsigmaS
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe G_sign lidT sigmaT _ <- return gsigmaT
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gsis1 <- adj $ homogenizeGM (Logic lidS) gsis
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe G_symb_map_items_list lid sis <- return gsis1
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe sigmaS' <- adj $ coerceSign lidS lid "" sigmaS
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe sigmaT' <- adj $ coerceSign lidT lid "" sigmaT
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe mor <- if isStructured opts then return (ide lid sigmaS')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe rmap <- adj $ stat_symb_map_items lid sis
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe adj $ induced_from_to_morphism lid rmap sigmaS' sigmaT'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let nodeS = getNode src
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe nodeT = getNode tar
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gmor = gEmbed (G_morphism lid 0 mor 0 0)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe link = (nodeS,nodeT,DGLink {
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dgl_morphism = gmor,
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dgl_type = GlobalThm LeftOpen None LeftOpen,
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- 'LeftOpen' for conserv correct?
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dgl_origin = DGView vn,
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dgl_id = [getNewEdgeID dg'']})
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe vsig = (src,gmor,(imp,params,getMaybeSig allparams,tar))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe genv = globalEnv dg''
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe then plain_error (View_defn vn gen' vt' gsis pos, dg'', l, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (alreadyDefined $ tokStr vn)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else return (View_defn vn gen' vt' gsis pos,
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (insEdgeDG link dg'')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe { globalEnv = Map.insert vn (ViewEntry vsig) genv }
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- | analyze a VIEW_TYPE
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- The first three arguments give the global context
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- The AnyLogic is the current logic
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- The NodeSig is the signature of the parameter of the view
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe-- flag, whether just the structure shall be analysed
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_VIEW_TYPE :: LogicGraph -> DGraph -> AnyLogic
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> MaybeNode -> HetcatsOpts -> NODE_NAME -> VIEW_TYPE
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_VIEW_TYPE lg dg l parSig opts name
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (View_type aspSrc aspTar pos) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (spSrc',srcNsig,dg') <- adjustPos pos $
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_SPEC lg dg (EmptyNode l) (extName "S" name) opts (item aspSrc)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (spTar',tarNsig,dg'') <- adjustPos pos $
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_SPEC lg dg' parSig
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (extName "T" name) opts (item aspTar)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (View_type (replaceAnnoted spSrc' aspSrc)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (replaceAnnoted spTar' aspTar)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (srcNsig, tarNsig), dg'')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_ITEM_NAME_OR_MAP :: LibEnv -> LIB_NAME -> GlobalEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (GlobalEnv, DGraph) -> ITEM_NAME_OR_MAP
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (GlobalEnv, DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_ITEM_NAME_OR_MAP libenv ln genv' res itm =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_ITEM_NAME_OR_MAP1 libenv ln genv' res $ case itm of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Item_name name -> (name, name)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Item_name_map old new _ -> (old, new)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_ITEM_NAME_OR_MAP1 :: LibEnv -> LIB_NAME -> GlobalEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (GlobalEnv, DGraph) -> (SIMPLE_ID, SIMPLE_ID)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (GlobalEnv, DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_ITEM_NAME_OR_MAP1 libenv ln genv' res (old, new) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (genv,dg) <- res
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe entry <- maybeToResult nullRange
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (tokStr old ++ " not found") (Map.lookup old genv')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case Map.lookup new genv of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> return ()
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just _ -> fail (tokStr new ++ " already used")
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case entry of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe SpecEntry extsig ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let (dg1,extsig1) = refExtsig libenv ln dg (Just new) extsig
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe genv1 = Map.insert new (SpecEntry extsig1) genv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in return (genv1,dg1)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ViewEntry vsig ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let (dg1,vsig1) = refViewsig libenv ln dg vsig
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe genv1 = Map.insert new (ViewEntry vsig1) genv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in return (genv1,dg1)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ArchEntry _asig -> ana_err "arch spec download"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe UnitEntry _usig -> ana_err "unit spec download"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe RefEntry -> ana_err "ref spec download"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefNodesig :: LibEnv -> LIB_NAME -> DGraph -> (Maybe SIMPLE_ID, NodeSig)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> (DGraph, NodeSig)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefNodesig libenv refln dg (name, NodeSig refn sigma@(G_sign lid sig ind)) =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let (ln, n) = getActualParent libenv refln refn
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe node_contents = newInfoNodeLab (makeMaybeName name)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (newRefInfo ln n) $ noSensGTheory lid sig ind
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe node = getNewNodeDG dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe --(insNode (node,node_contents) dg, NodeSig node sigma)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case (lookupInAllRefNodesDG (ln, n) dg) of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just existNode -> (dg, NodeSig existNode sigma)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> (addToRefNodesDG (node, ln, n)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ insNodeDG (node,node_contents) dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , NodeSig node sigma)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe{- | get to the actual parent which is not a referenced node, so that
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe the small chains between nodes in different library can be advoided.
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (details see ticket 5)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowegetActualParent :: LibEnv -> LIB_NAME -> Node -> (LIB_NAME, Node)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowegetActualParent libenv ln n =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dg = lookupDGraph ln libenv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe lab' $ safeContextDG "Static.AnalysisLibrary.getActualParent" dg n
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case isDGRef refLab of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- recursively goes to parent of the current node, but
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- it actually would only be done once
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe True -> getActualParent libenv (dgn_libname refLab) (dgn_node refLab)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe False -> (ln, n)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefNodesigs :: LibEnv -> LIB_NAME -> DGraph -> [(Maybe SIMPLE_ID, NodeSig)]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> (DGraph, [NodeSig])
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefNodesigs libenv ln = mapAccumR (refNodesig libenv ln)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefExtsig :: LibEnv -> LIB_NAME -> DGraph -> Maybe SIMPLE_ID -> ExtGenSig
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> (DGraph, ExtGenSig)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefExtsig libenv ln dg name (imps,params,gsigmaP,body) =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe params' = map (\x -> (Nothing,x)) params
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (dg0, body1) = refNodesig libenv ln dg (name, body)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (dg1, params1) = refNodesigs libenv ln dg0 params'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (dg2, imps1) = case imps of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe EmptyNode _ -> (dg1, imps)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe JustNode ns -> let
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (dg3, nns) = refNodesig libenv ln dg1 (Nothing, ns)
5dbfd19ad5fcc2b779f40f80fa05c1bd28fd0b4eTheo Schlossnagle in (dg3, JustNode nns)
5dbfd19ad5fcc2b779f40f80fa05c1bd28fd0b4eTheo Schlossnagle in (dg2,(imps1,params1,gsigmaP,body1))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefViewsig :: LibEnv -> LIB_NAME -> DGraph -> (NodeSig, t1, ExtGenSig)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> (DGraph, (NodeSig, t1, ExtGenSig))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefViewsig libenv ln dg (src,mor,extsig) =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (dg2,(src1,mor,extsig1))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (_,[src1]) = refNodesigs libenv ln dg [(Nothing,src)]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (dg2,extsig1) = refExtsig libenv ln dg Nothing extsig