b897c52f865b2fc4e220e2110b874e59c716456bBob Halley{-|

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyModule : $Header$

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyMaintainer : till@tzi.de

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyStability : provisional

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyPortability : non-portable(Logic)

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley Analysis of libraries

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley Follows the verification semantics sketched in Chap. IV:6

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley of the CASL Reference Manual.

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley-}

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley{-

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley Todo:

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Generalization to heterogeneous views

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley check that libname coincides with filename (otherwise internal error occurs)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-}

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleymodule Static.AnalysisLibrary (anaFile, ana_LIB_DEFN, anaString) where

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Logic.Logic

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Logic.Grothendieck

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Data.Graph.Inductive.Graph

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Static.DevGraph

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halleyimport Syntax.AS_Structured hiding (View_defn, Spec_defn)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Syntax.AS_Library

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Static.AnalysisStructured

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Static.AnalysisArchitecture

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Common.AS_Annotation

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halleyimport Common.GlobalAnnotations

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Common.ConvertGlobalAnnos

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halleyimport Common.AnalyseAnnos

e6d6ce00e2bf0f6a755f8229212e35706e4035aeMichael Graffimport Common.Result

e6d6ce00e2bf0f6a755f8229212e35706e4035aeMichael Graffimport Common.Id

e6d6ce00e2bf0f6a755f8229212e35706e4035aeMichael Graffimport qualified Common.Lib.Map as Map

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Common.PrettyPrint

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Driver.Options

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Driver.ReadFn

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halleyimport Driver.WriteFn (writeFileInfo)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halleyimport Data.List(nub)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halleyimport System.Environment(getEnv)

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- | parsing and static analysis for files

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halley-- Parameters: logic graph, default logic, file name

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyanaFile :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -> IO (Maybe (LIB_NAME,LIB_DEFN,DGraph,LibEnv))

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleyanaFile logicGraph defaultLogic opts libenv fname = do

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley putIfVerbose opts 1 ("Reading " ++ fname)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley fname' <- existsAnSource fname

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley case fname' of

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley Nothing -> do

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley if outputToStdout opts then

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley putStrLn (fname++" not found.")

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halley else return ()

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halley return Nothing

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Just fname'' -> do

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley input <- readFile fname''

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley anaString logicGraph defaultLogic opts libenv input (Just fname'')

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | parsing and static analysis for string (=contents of file)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- Parameters: logic graph, default logic, contents of file, filename (if any)

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyanaString :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -> Maybe String -> IO (Maybe (LIB_NAME,LIB_DEFN,DGraph,LibEnv))

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyanaString logicGraph defaultLogic opts libenv input fname = do

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley let fname' = case fname of

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Nothing -> "<stdin>"

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Just n -> n

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley ast <- read_LIB_DEFN_M defaultLogic fname' input

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Result ds res <-

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley ioresToIO (ana_LIB_DEFN logicGraph defaultLogic opts

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley libenv ast)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -- no diags expected here, since these are handled in ana_LIB_DEFN

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- sequence (map (putStrLn . show) diags)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley case (res,fname) of

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley (Just (ln,_,_,lenv), Just n) ->

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley writeFileInfo opts ds n ln lenv

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley _ -> return ()

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley return res

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- lookup/read a library

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleyanaLibFile :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> LIB_NAME

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -> IO ([Diagnosis], LibEnv)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleyanaLibFile logicGraph defaultLogic opts libenv libname = do

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- is the library already in memory?

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley case Map.lookup libname libenv of

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley Just _ -> return ([],libenv)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley Nothing -> do

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- if not compute the filename,

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley fname <- case getLIB_ID libname of

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley Indirect_link file _ -> do

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley path <- case libdir opts of

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley "" -> catch (getEnv "HETS_LIB")

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley (\ _ -> return "")

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley p -> return p

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- add trailing "/" if necessary

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley let path1 = case path of

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley "" -> ""

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley p -> case last p of

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley '/' -> p

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley _ -> p++"/"

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley return (path1++file)

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley Direct_link _ _ ->

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley if outputToStdout opts then

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley error "No direct links implemented yet"

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley else return (error "No direct links implemented yet")

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley -- check if and env file is there and read it if it is recent

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley let env_fname = fname++".env"

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -- fname is sufficient here, because anaFile

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -- trys all possible suffices with this basename

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley recent_env_file <- checkRecentEnv env_fname fname

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley if recent_env_file

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley then do

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley putIfVerbose opts 1 ("Reading "++env_fname)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley (Result dias mgc) <- globalContextfromShATerm env_fname

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -- the conversion/reading might yield an error that

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -- should be caught here

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley (dias2, mLibEnv) <-

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley maybe (do ioresToIO $ showDiags1 opts

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley (resToIORes (Result dias mgc))

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley anaLibFile' fname dias)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley (\ gc@(_,_,dgraph) -> do

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley putIfVerbose opts 1 ""

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -- get all DGRefs from DGraph

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley let libEnv' = (Map.insert libname gc libenv)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley nodesDGRef =

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley filter (\ labDG -> case labDG of

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley DGRef _ _ _ _ _ -> True

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley _ -> False)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley (map snd (labNodes dgraph))

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -- and call anaLibFile with each of the dgn_libname

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley -- of the DGRefs

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley refLibs = nub $ map dgn_libname nodesDGRef

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley newRefLibs =

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley filter (\ ln ->

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley not (ln `elem` Map.keys libEnv'))

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley refLibs

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley foldl (\ioLibEnv tlibname ->

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley do (dias3 ,p_libEnv) <- ioLibEnv

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley putIfVerbose opts 1

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley ("Analyzing from " ++

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley showPretty tlibname "\n")

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley (dias4, libEnvF) <-

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley anaLibFile logicGraph defaultLogic

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley opts p_libEnv tlibname

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley return ((dias3 ++ dias4),libEnvF)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley ) (return ([], libEnv')) newRefLibs

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley )

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley mgc

59a6d9cbcdbec6960d47e5871fb7e7c0253e1fb2Mark Andrews if outputToStdout opts then

59a6d9cbcdbec6960d47e5871fb7e7c0253e1fb2Mark Andrews return ([], mLibEnv)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley else return( dias ++ dias2 , mLibEnv)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley else anaLibFile' fname []

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

where anaLibFile' :: FilePath -> [Diagnosis] -> IO ([Diagnosis], LibEnv)

anaLibFile' fname diags'=

do

-- read and analyze the library,

if outputToStdout opts then

do

res <- anaFile logicGraph defaultLogic opts libenv fname

putIfVerbose opts 1 ""

-- and just return the libenv

return (case res of

Just (_,_,_,libenv') -> (diags', libenv')

Nothing -> (diags', libenv)

)

else do

(dias, res) <- anaFileW logicGraph defaultLogic opts

libenv fname

return (case res of

Just (_,_,_,libenv') -> (diags'++dias, libenv')

Nothing -> ((diags $ message ()

(fname ++" not found."))

++ diags',libenv))

anaFileW :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String

-> IO ([Diagnosis], Maybe (LIB_NAME,LIB_DEFN,DGraph,LibEnv))

anaFileW logicGraph' defLogic' opts' libenv' fname = do

fname' <- existsAnSource fname

case fname' of

Nothing -> return ([], Nothing)

Just fname'' -> do

input <- readFile fname''

anaStringW logicGraph' defLogic' opts' libenv' input

(Just fname'')

anaStringW :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String

-> Maybe String

-> IO ([Diagnosis], Maybe (LIB_NAME,LIB_DEFN,DGraph,LibEnv))

anaStringW logicGraph' defLogic' opts' libenv' input fname = do

let fname' = case fname of

Nothing -> "<stdin>"

Just n -> n

(_, ast) <- read_LIB_DEFN_M_WI defLogic' fname' input

Result ds res <-

ioresToIO (ana_LIB_DEFN logicGraph' defLogic' opts'

libenv' ast)

case (res,fname) of

(Just (ln,_,_,lenv), Just n) ->

writeFileInfo opts' ds n ln lenv

_ -> return ()

return (ds, res)

-- | analyze a LIB_DEFN

-- Parameters: logic graph, default logic, opts, library env, LIB_DEFN

-- call this function as follows:

-- do Result diags res <- ioresToIO (ana_LIB_DEFN ...)

-- sequence (map (putStrLn . show) diags)

ana_LIB_DEFN :: LogicGraph -> AnyLogic -> HetcatsOpts

-> LibEnv -> LIB_DEFN

-> IOResult (LIB_NAME,LIB_DEFN,DGraph,LibEnv)

ana_LIB_DEFN lgraph defl opts libenv (Lib_defn ln alibItems pos ans) = do

gannos <- resToIORes $ addGlobalAnnos emptyGlobalAnnos ans

(libItems',gctx@(_,_,dg),_,libenv') <-

foldl ana (return ([],(gannos,Map.empty,empty),defl,libenv))

(map item alibItems)

return (ln,

Lib_defn ln

(map (uncurry replaceAnnoted)

(zip (reverse libItems') alibItems))

pos

ans,

dg,

Map.insert ln gctx libenv')

where

ana res1 libItem = do

(libItems',gctx1,l1,libenv1) <- res1

IOResult (do

Result diags2 res <-

ioresToIO $ ana_LIB_ITEM lgraph defl opts libenv1 gctx1 l1 libItem

ioresToIO $ showDiags1 opts (resToIORes (Result diags2 res))

if outputToStdout opts then

if hasErrors diags2 then

fail "Stopped due to errors"

else case res of

Just (libItem',gctx1',l1',libenv1') ->

return (return (libItem':libItems',gctx1',l1',libenv1'))

Nothing -> fail "Stopped. No result available"

else do

--result1 <- ioresToIO res1

--let diags1 = diags result1

if hasErrors diags2 then

ioresToIO $ resToIORes (Result (diags2) Nothing)

else case res of

Just (libItem',gctx1',l1',libenv1') ->

return ((return (libItem':libItems',gctx1',l1',libenv1'))

{diags = diags2})

Nothing -> return $ fail "Stopped. No result available"

)

-- analyse a LIB_ITEM

-- Parameters: logic graph, default logic, opts, library env

-- global context, current logic, LIB_ITEM

ana_LIB_ITEM :: LogicGraph -> AnyLogic -> HetcatsOpts

-> LibEnv -> GlobalContext -> AnyLogic

-> LIB_ITEM

-> IOResult (LIB_ITEM,GlobalContext,AnyLogic,LibEnv)

ana_LIB_ITEM lgraph _defl opts libenv gctx@(gannos, genv, _) l

(Spec_defn spn gen asp pos) = do

let analyseMessage = "Analyzing spec " ++ showPretty spn ""

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

(gen',(imp,params,parsig,allparams),dg') <-

resToIORes (ana_GENERICITY lgraph gctx l opts (extName "P" (makeName spn)) gen)

(sp',body,dg'') <-

resToIORes (ana_SPEC lgraph (gannos,genv,dg')

allparams (makeName spn) opts (item asp))

let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos

if Map.member spn genv

then resToIORes (plain_error (libItem',gctx,l,libenv)

("Name "++ showPretty spn " already defined")

pos)

else return (libItem',

(gannos,

Map.insert spn (SpecEntry (imp,params,parsig,body)) genv,

dg''),

l,

libenv)

ana_LIB_ITEM lgraph defl opts libenv gctx l

(View_defn vn gen vt gsis pos) = do

let analyseMessage = "Analyzing view " ++ showPretty vn ""

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

resToIORes (ana_VIEW_DEFN lgraph defl libenv gctx l opts

vn gen vt gsis pos)

-- architectural specification

ana_LIB_ITEM lgraph defl opts libenv gctx@(gannos, genv, _) l

(Arch_spec_defn asn asp pos) = do

let analyseMessage = "Analyzing arch spec " ++ showPretty asn ""

ioToIORes (putIfVerbose opts 1 analyseMessage )

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

(archSig, dg', asp') <- resToIORes (ana_ARCH_SPEC lgraph defl gctx l opts

(item asp))

let asd' = Arch_spec_defn asn (replaceAnnoted asp' asp) pos

gctx' = (gannos, genv, dg')

if Map.member asn genv

then

resToIORes (plain_error (asd', gctx', l, libenv)

("Name " ++ showPretty asn " already defined")

pos)

else

return (asd',

(gannos,

Map.insert asn (ArchEntry archSig) genv,

dg'),

l,

libenv)

-- unit specification

ana_LIB_ITEM lgraph defl opts libenv gctx@(gannos, genv, _) l

usd@(Unit_spec_defn usn usp pos) = do

let analyseMessage = "Analyzing unit spec " ++ showPretty usn ""

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

(unitSig, dg', usp') <- resToIORes (ana_UNIT_SPEC lgraph defl gctx l opts

(EmptyNode defl) usp)

let usd' = Unit_spec_defn usn usp' pos

if Map.member usn genv

then

resToIORes (plain_error (usd, (gannos, genv, dg'), l, libenv)

("Name " ++ showPretty usn " already defined")

pos)

else

return (usd',

(gannos,

Map.insert usn (UnitEntry unitSig) genv,

dg'),

l,

libenv)

-- refinement specification

ana_LIB_ITEM lgraph defl opts libenv gctx@(gannos, genv, dg) l

rd@(Ref_spec_defn rn ref pos) = do

let analyseMessage = "Analyzing refinement " ++ showPretty rn "\n (refinement analysis not implemented yet)"

ioToIORes (putIfVerbose opts 1 analyseMessage )

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

let rd' = rd

dg' = dg

if Map.member rn genv

then

resToIORes (plain_error (rd, (gannos, genv, dg), l, libenv)

("Name " ++ showPretty rn " already defined")

pos)

else

return (rd',

(gannos,

Map.insert rn (RefEntry) genv,

dg'),

l,

libenv)

-- logic declaration

ana_LIB_ITEM lgraph _defl opts libenv gctx _l

(Logic_decl ln@(Logic_name logTok _) pos) = do

logNm <- lookupLogic "LOGIC DECLARATION:" (tokStr logTok) lgraph

let analyseMessage = "logic " ++ show logNm

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

return (Logic_decl ln pos,gctx,logNm,libenv)

ana_LIB_ITEM lgraph defl opts libenv gctx@(gannos,genv,dg) l

libItem@(Download_items ln items pos) = do

-- we take as the default logic for imported libs

-- the global default logic

let analyseMessage = "Analyzing from " ++ showPretty ln "\n"

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

(diags', libenv') <- ioToIORes (anaLibFile lgraph defl opts libenv ln)

resToIORes $ Result diags' $ Just ()

-- let libMsg = unlines $ map show diags'

-- resToIORes $ message () libMsg

case Map.lookup ln libenv' of

Nothing -> do

if outputToStdout opts then

do

ioToIORes (putStrLn ("Internal error: did not find library "++

show ln++" available: "++show (Map.keys libenv')))

return (libItem,gctx,l,libenv')

else

resToIORes $ (fatal_error ("Internal error: did not find library "

++show ln++" available: "++show (Map.keys libenv')) nullPos)

Just (gannos', genv', _dg') -> do

(genv1,dg1) <- resToIORes (foldl (ana_ITEM_NAME_OR_MAP ln genv')

(return (genv,dg)) items

)

gannos'' <- resToIORes $ gannos `mergeGlobalAnnos` gannos'

return (libItem,(gannos'',genv1,dg1),l,libenv')

-- ??? Needs to be generalized to views between different logics

ana_VIEW_DEFN :: LogicGraph -> AnyLogic -> LibEnv -> GlobalContext

-> AnyLogic -> HetcatsOpts -> SIMPLE_ID

-> GENERICITY -> VIEW_TYPE -> [G_mapping] -> [Pos]

-> Result (LIB_ITEM, GlobalContext, AnyLogic, LibEnv)

ana_VIEW_DEFN lgraph _defl libenv gctx@(gannos, genv, _) l opts

vn gen vt gsis pos = do

let adj = adjustPos pos

(gen',(imp,params,parsig,allparams),dg') <-

ana_GENERICITY lgraph gctx l opts (extName "VG" (makeName vn)) gen

(vt',(src,tar),dg'') <-

ana_VIEW_TYPE lgraph (gannos,genv,dg') l allparams opts (makeName vn) vt

let gsigmaS = getSig src

gsigmaT = getSig tar

G_sign lidS sigmaS <- return gsigmaS

G_sign lidT sigmaT <- return gsigmaT

gsis1 <- adj $ homogenizeGM (Logic lidS) gsis

G_symb_map_items_list lid sis <- return gsis1

sigmaS' <- rcoerce lid lidS pos sigmaS

sigmaT' <- rcoerce lid lidT pos sigmaT

mor <- if isStructured opts then return (ide lid sigmaS')

else do

rmap <- adj $ stat_symb_map_items lid sis

adj $ induced_from_to_morphism lid rmap sigmaS' sigmaT'

nodeS <- maybeToResult pos

"Internal error: empty source spec of view" (getNode src)

nodeT <- maybeToResult pos

"Internal error: empty source spec of view" (getNode tar)

let gmor = gEmbed (G_morphism lid mor)

link = (nodeS,nodeT,DGLink {

dgl_morphism = gmor,

dgl_type = GlobalThm Open None Open,

-- 'Open' for conserv correct?

dgl_origin = DGView vn})

vsig = (src,gmor,(imp,params,parsig,tar))

if Map.member vn genv

then plain_error (View_defn vn gen' vt' gsis pos,gctx,l,libenv)

("Name "++showPretty vn " already defined")

pos

else return (View_defn vn gen' vt' gsis pos,

(gannos,

Map.insert vn (ViewEntry vsig) genv,

insEdge link dg''),

l,

libenv)

ana_ITEM_NAME_OR_MAP :: LIB_NAME -> GlobalEnv -> Result (GlobalEnv, DGraph)

-> ITEM_NAME_OR_MAP -> Result (GlobalEnv, DGraph)

ana_ITEM_NAME_OR_MAP ln genv' res (Item_name name) =

ana_ITEM_NAME_OR_MAP1 ln genv' res name name

ana_ITEM_NAME_OR_MAP ln genv' res (Item_name_map old new _) =

ana_ITEM_NAME_OR_MAP1 ln genv' res old new

ana_ITEM_NAME_OR_MAP1 :: LIB_NAME -> GlobalEnv -> Result (GlobalEnv, DGraph)

-> SIMPLE_ID -> SIMPLE_ID

-> Result (GlobalEnv, DGraph)

ana_ITEM_NAME_OR_MAP1 ln genv' res old new = do

(genv,dg) <- res

entry <- maybeToResult []

(showPretty old " not found") (Map.lookup old genv')

case Map.lookup new genv of

Nothing -> return ()

Just _ -> fail (showPretty new " already used")

case entry of

SpecEntry extsig ->

let (dg1,extsig1) = refExtsig ln dg (Just new) extsig

genv1 = Map.insert new (SpecEntry extsig1) genv

in return (genv1,dg1)

ViewEntry vsig ->

let (dg1,vsig1) = refViewsig ln dg vsig

genv1 = Map.insert new (ViewEntry vsig1) genv

in return (genv1,dg1)

ArchEntry _asig -> ana_err "arch spec download"

UnitEntry _usig -> ana_err "unit spec download"

refNodesig :: LIB_NAME -> (DGraph, [NodeSig]) -> (Maybe SIMPLE_ID, NodeSig)

-> (DGraph, [NodeSig])

refNodesig ln (dg,refdNodes) (name,NodeSig(n,sigma)) =

let node_contents = DGRef {

dgn_renamed = makeMaybeName name,

dgn_libname = ln,

dgn_node = n,

dgn_nf = Nothing,

dgn_sigma = Nothing

}

node = getNewNode dg

in (insNode (node,node_contents) dg, NodeSig(node,sigma) : refdNodes)

refNodesig _ln (dg,refdNodes) (_,EmptyNode l) =

(dg,EmptyNode l : refdNodes)

refNodesigs :: LIB_NAME -> DGraph -> [(Maybe SIMPLE_ID, NodeSig)]

-> (DGraph, [NodeSig])

refNodesigs ln dg nds =

(dg',reverse nodes')

where (dg', nodes') = foldl (refNodesig ln) (dg,[]) nds

refExtsig :: LIB_NAME -> DGraph -> Maybe SIMPLE_ID -> ExtGenSig

-> (DGraph, ExtGenSig)

refExtsig ln dg name (imps,params,gsigmaP,body) =

(dg1,(imps1,params1,gsigmaP,body1))

where

params' = map (\x -> (Nothing,x)) params

(dg1,imps1:body1:params1) =

refNodesigs ln dg

((Nothing,imps):(name,body):params')

refViewsig :: LIB_NAME -> DGraph -> (NodeSig, t1, ExtGenSig)

-> (DGraph, (NodeSig, t1, ExtGenSig))

refViewsig ln dg (src,mor,extsig) =

(dg2,(src1,mor,extsig1))

where

(_,[src1]) = refNodesigs ln dg [(Nothing,src)]

(dg2,extsig1) = refExtsig ln dg Nothing extsig