AnalysisLibrary.hs revision 14ccb7ad7ef9ccd32a92696192fe46bc19e9dd68
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 , anaLibReadPrfs
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , ana_LIB_DEFN
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , anaSourceFile
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport Common.AS_Annotation hiding (isAxiom, isDef)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweimport qualified Data.Map as Map
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibReadPrfs :: HetcatsOpts -> FilePath -> IO (Maybe (LIB_NAME, LibEnv))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibReadPrfs opts file = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe m <- anaLib opts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe { outtypes = []
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , specNames = []
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , modelSparQ = ""
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , dumpOpts = [] } file
89b9271284be1a4e3e3053d7bc12f9bbf8145b06Robert Mustacchi Nothing -> return Nothing
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just (ln, libEnv) -> do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe nEnv <- readPrfFiles opts libEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe writeSpecFiles (removePrfOut opts) file nEnv ln $ lookupDGraph ln nEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return $ Just (ln, nEnv)
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 Result ds res <- runResultT $ anaLibFileOrGetEnv logicGraph 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 writeSpecFiles opts file nEnv ln $ lookupDGraph ln nEnv
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 -> HetcatsOpts -> LibEnv -> FilePath
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> ResultT IO (LIB_NAME, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaSourceFile lgraph 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
ce83b99835cc4643ab0fefd88dea62427d9ced5eRobert Mustacchi putIfVerbose opts 2 $ "Reading file " ++ absolutePath
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe runResultT $ anaString lgraph 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 -> HetcatsOpts -> LibEnv -> String
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> FilePath -> ClockTime -> ResultT IO (LIB_NAME, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaString lgraph opts libenv input file mt = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let Result ds mast = read_LIB_DEFN_M lgraph opts file input mt
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe 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 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 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 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 -> HetcatsOpts -> LibEnv -> LIB_NAME
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> ResultT IO (LIB_NAME, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibFile lgraph opts libenv ln =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let lnstr = show ln in case Map.lookup ln libenv of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just _ -> do
296749875bd503e7a14e25b4c57d3142cb496df1Joshua M. Clulow 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
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 -> HetcatsOpts -> LibEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> LIB_NAME -> FilePath -> ResultT IO (LIB_NAME, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LoweanaLibFileOrGetEnv lgraph opts libenv libname file = ResultT $ do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let envFile = rmSuffix file ++ envSuffix
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe recent_envFile <- checkRecentEnv opts envFile file
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if recent_envFile
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe mgc <- readVerbose opts libname envFile
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> runResultT $ do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe lift $ putIfVerbose opts 1 $ "Deleting " ++ envFile
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe anaSourceFile lgraph 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
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 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 -> HetcatsOpts -> LibEnv -> LIB_DEFN
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> ResultT IO (LIB_NAME,LIB_DEFN, DGraph, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_LIB_DEFN lgraph opts libenv (Lib_defn ln alibItems pos ans) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gannos <- showDiags1 opts $ liftR $ addGlobalAnnos emptyGlobalAnnos ans
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dg <- lift $ emptyDGwithMVar
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (libItems', dg1, libenv', _) <- foldM ana
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ([], dg { globalAnnos = gannos }, libenv, lgraph) (map item alibItems)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (ln, Lib_defn ln
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (map (uncurry replaceAnnoted) (zip (reverse libItems') alibItems))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe pos ans, dg1, Map.insert ln dg1 libenv')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana (libItems', dg1, libenv1, lG) libItem =
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let newLG = case libItems' of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [] -> lG { currentLogic = defLogic opts }
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Logic_decl (Logic_name logTok _) _ : _ ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe lG { currentLogic = tokStr logTok }
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in ResultT (do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Result diags2 res <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe runResultT $ ana_LIB_ITEM newLG opts libenv1 dg1 libItem
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe runResultT $ showDiags1 opts (liftR (Result diags2 res))
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let mRes = case res of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just (libItem', dg1', libenv1') ->
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just (libItem' : libItems', dg1', libenv1', newLG)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Nothing -> Nothing
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if outputToStdout opts then
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe if hasErrors diags2 then
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe fail "Stopped due to errors"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else runResultT $ liftR $ Result [] mRes
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else runResultT $ liftR $ Result diags2 mRes)
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 -> HetcatsOpts -> NodeName
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> GENERICITY -> Result (GENERICITY, GenericitySig, DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_GENERICITY lg dg 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 l <- lookupCurrentLogic "GENERICITY" lg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (gen, GenericitySig (EmptyNode l) [] $ EmptyNode l, dg)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (imps', nsigI, dg') <- ana_IMPORTS lg dg opts (extName "I" name) imps
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe case psps of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe [asp] -> do -- one parameter ...
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sp', nsigP, dg'') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_SPEC True False lg dg' nsigI name opts (item asp)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (Genericity (Params [replaceAnnoted sp' asp]) imps' pos,
462453d2d0c563559a4caf186db76954e563bd1aMatthew Ahrens GenericitySig 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 let (NodeSig node _, dg3) = insGSig dg'' name DGFormalParams gsigmaP
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe inslink dgl (NodeSig n sigma) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe incl <- adj $ ginclusion lg sigma gsigmaP
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return $ insLink dgl incl GlobalDef SeeTarget n node
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe dg4 <- foldM inslink dg3 nsigPs
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (Genericity params' imps' pos,
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe GenericitySig nsigI nsigPs $ if null nsigPs then nsigI else
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe JustNode $ NodeSig node gsigmaP, dg4)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_PARAMS :: LogicGraph -> DGraph -> MaybeNode
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> HetcatsOpts -> NodeName -> PARAMS
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (PARAMS, [NodeSig], DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_PARAMS lg dg nsigI opts name (Params asps) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sps', pars, dg', _) <- foldM ana ([], [], dg, name) $ map item asps
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (Params (map (uncurry replaceAnnoted)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (zip (reverse sps') asps)),
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe reverse pars, dg')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana (sps', pars, dg1, n) sp = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sp', par, dg') <- ana_SPEC True False lg dg1 nsigI n opts sp
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (sp' : sps', par : pars, dg', inc n)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_IMPORTS :: LogicGraph -> DGraph -> HetcatsOpts -> NodeName -> IMPORTED
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (IMPORTED, MaybeNode, DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_IMPORTS lg dg opts name imps@(Imported asps) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe l <- lookupCurrentLogic "IMPORTS" lg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe 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 False False 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 -> HetcatsOpts -> LibEnv -> DGraph -> LIB_ITEM
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> ResultT IO (LIB_ITEM, DGraph, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_LIB_ITEM lgraph opts libenv dg 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', GenericitySig imp params allparams, dg') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe liftR (ana_GENERICITY lgraph dg opts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (extName "P" (makeName spn)) gen)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (sp', body, dg'') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe liftR (ana_SPEC False True 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'', libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (alreadyDefined spstr) pos)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , dg'' { globalEnv = Map.insert spn (SpecEntry
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ ExtGenSig imp params (getMaybeSig allparams) body) genv }
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 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 dg 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', 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 l <- lookupCurrentLogic "Unit_spec_defn" lgraph
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (unitSig, dg', usp') <- liftR (ana_UNIT_SPEC lgraph dg 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', 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, libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (alreadyDefined rnstr)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else return ( itm, dg { globalEnv = Map.insert rn (RefEntry) genv }
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, 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 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) <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe liftR $ foldM (ana_ITEM_NAME_OR_MAP libenv' ln $ globalEnv dg')
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (globalEnv dg, dg) items
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe gannos'' <- liftR $ globalAnnos dg `mergeGlobalAnnos` globalAnnos dg'
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe return (itm, dg1
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe { globalAnnos = gannos''
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe , globalEnv = genv1 }, 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 -> HetcatsOpts -> SIMPLE_ID
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (LIB_ITEM, DGraph, LibEnv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_VIEW_DEFN lg libenv dg opts vn gen vt gsis pos = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (gen', GenericitySig imp params allparams, dg') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_GENERICITY lg dg opts (extName "VG" (makeName vn)) gen
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (vt', (src@(NodeSig nodeS gsigmaS), tar@(NodeSig nodeT gsigmaT)), dg'') <-
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_VIEW_TYPE lg dg' allparams opts (makeName vn) vt
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe l <- lookupCurrentLogic "VIEW_DEFN" lg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe mor <- ana_Gmaps lg opts (EmptyNode l) pos gsigmaS gsigmaT gsis
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe let gmor = gEmbed mor
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe vsig = ExtViewSig src gmor
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ ExtGenSig imp params (getMaybeSig allparams) tar
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe genv = globalEnv dg''
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe then plain_error (View_defn vn gen' vt' gsis pos, dg'', libenv)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (alreadyDefined $ tokStr vn)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe else return (View_defn vn gen' vt' gsis pos,
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (insLink dg'' gmor (GlobalThm LeftOpen None LeftOpen)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (DGLinkView vn) nodeS nodeT)
2d08521bd15501c8370ba2153b9cca4f094979d0Garrett D'Amore -- 'LeftOpen' for conserv correct?
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 -> MaybeNode -> HetcatsOpts
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> NodeName -> VIEW_TYPE
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_VIEW_TYPE lg dg parSig opts name
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (View_type aspSrc aspTar pos) = do
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe l <- lookupCurrentLogic "VIEW_TYPE" lg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (spSrc', srcNsig, dg') <- adjustPos pos $ ana_SPEC False False lg dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (EmptyNode l) (extName "S" name) opts (item aspSrc)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (spTar', tarNsig, dg'') <- adjustPos pos $
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ana_SPEC False True lg dg' parSig (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 -> (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 Lowe-- | Auxiliary function for not yet implemented features
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_err :: String -> a
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_err f = error $ "*** Analysis of " ++ f ++ " is not yet implemented!"
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_ITEM_NAME_OR_MAP1 :: LibEnv -> LIB_NAME -> GlobalEnv
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> (GlobalEnv, DGraph) -> (SIMPLE_ID, SIMPLE_ID)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> Result (GlobalEnv, DGraph)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Loweana_ITEM_NAME_OR_MAP1 libenv ln genv' (genv, dg) (old, new) = do
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
2d08521bd15501c8370ba2153b9cca4f094979d0Garrett D'Amore genv1 = Map.insert new (ViewEntry vsig1) genv
2d08521bd15501c8370ba2153b9cca4f094979d0Garrett D'Amore 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 refInfo = newRefInfo ln n
cb66c7814563eb32e20c1be88ae738ad8d63079dRobert Mustacchi node_contents = newInfoNodeLab (makeMaybeName name) refInfo
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe $ noSensGTheory lid sig ind
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe node = getNewNodeDG dg
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in case lookupInAllRefNodesDG refInfo dg of
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe Just existNode -> (dg, NodeSig existNode sigma)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe ( addToRefNodesDG node refInfo $ 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 let refLab = labDG (lookupDGraph ln libenv) n in
f07f0fb66492a2792d4da5e0a6f9a92b4c581ab3Garrett D'Amore if isDGRef refLab then
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -- recursively goes to parent of the current node, but
f07f0fb66492a2792d4da5e0a6f9a92b4c581ab3Garrett D'Amore -- it actually would only be done once
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe getActualParent libenv (dgn_libname refLab) (dgn_node refLab)
f07f0fb66492a2792d4da5e0a6f9a92b4c581ab3Garrett D'AmorerefNodesigs :: 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 (ExtGenSig imps params gsigmaP body) = let
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)
2d08521bd15501c8370ba2153b9cca4f094979d0Garrett D'Amore JustNode ns -> let
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (dg3, nns) = refNodesig libenv ln dg1 (Nothing, ns)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in (dg3, JustNode nns)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in (dg2, ExtGenSig imps1 params1 gsigmaP body1)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefViewsig :: LibEnv -> LIB_NAME -> DGraph -> ExtViewSig
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe -> (DGraph, ExtViewSig)
c10c16dec587a0662068f6e2991c29ed3a9db943Richard LowerefViewsig libenv ln dg (ExtViewSig src mor extsig) = let
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (_,[src1]) = refNodesigs libenv ln dg [(Nothing, src)]
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe (dg2, extsig1) = refExtsig libenv ln dg Nothing extsig
c10c16dec587a0662068f6e2991c29ed3a9db943Richard Lowe in (dg2, ExtViewSig src1 mor extsig1)