GlobalEnv.hs revision 51ad29ec0d75f2212f801e8883ed9f6f4d6289fd
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- needs ghc -fglasgow-exts -package lang
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder Till Mossakowski
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder Data structure for global environment, representing heterogeneous CASL
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder structured and architectural specifications and libraries.
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder This is based on Logic.hs, providing a logic
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder independent interface for data structures for the local environment (signature).
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder The structure of the global environment follows the notion
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder of global environment in the CASL semantics (study note S-9).
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder However, there is a difference: we do not (only) flatten the specifications
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder into signatures, but rather keep the structure of the
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder specification (while transforming it into a more institution-like
d48085f765fca838c1d972d2123601997174583dChristian Maeder form, i.e. symbol maps are replaced by the induced signature morphisms).
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder The flattened local environment is kept at the outermost level
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder of the global environment, but not at the inner nodes (except
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder for nodes for basic specifications, of course), since
d48085f765fca838c1d972d2123601997174583dChristian Maeder this would consume too much space.
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder A library environment is a table of global environments,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder one for each library. This table is kept during static analysis,
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder in order to avoid re-reading of libraries.
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder CASL Semantics, version of July 24, 2001
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder T. Mossakowski, B. Klin:
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Institution Independent Static Analysis for CASL
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Use better tables
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Should architectural data structures be based on SpecLenvs as well?
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maedermodule GlobalEnv where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport AS_Annotation
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Grothendieck
eab576044505ba1fbc64610323053490fbd9e82cChristian Maederimport AS_Structured
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederimport AS_Architecture
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederimport AS_Library
eab576044505ba1fbc64610323053490fbd9e82cChristian Maedertype Table a b = [(a,b)] -- very inefficient, improve!
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- Keep structure of specifications,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- while replacing basic specs and symbol maps with their static semantics
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- (i.e. signatures, sentences and signature morphisms)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata SpecEnv = Basic_specEnv G_sign G_l_sentence_list
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder | TranslationEnv SpecEnv G_morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | ReductionEnv SpecEnv G_morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | UnionEnv [SpecEnv]
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder | ExtensionEnv [(SpecEnv,Annotation)]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | Free_spec SpecEnv
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder | Cofree SpecEnv -- covers CoCASL as well
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder | Local_spec SpecEnv SpecEnv G_morphism
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder | Closed_spec SpecEnv
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | Spec_instEnv {
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder name :: SPEC_NAME,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder body :: SpecEnv,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fittingMorphism :: G_morphism,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder actualParams :: [SpecEnv]
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian Maeder -- deriving (Show,Eq)
d92635f998347112e5d5803301c2abfe7832ab65Christian Maeder-- Add flattened Env at the outer level
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- for purposes of a quick static analysis
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederdata SpecLenv = SpecLenv {
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder flattenedEnv :: G_local_env,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder hiddenEnv :: G_local_env,
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder structuredEnv :: SpecEnv
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata GenericityEnv = GenericityEnv {
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder allImports :: SpecLenv,
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder formalParams :: [SpecLenv],
d48085f765fca838c1d972d2123601997174583dChristian Maeder flattenedParams :: G_local_env
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder-- Follows the semantic domains of the architectural semantics
d48085f765fca838c1d972d2123601997174583dChristian Maedertype CompSigs = G_sign_list
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maedertype UnitSig = (CompSigs, G_sign)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maedertype StBasedUnitCtx = Table UNIT_NAME Node
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maedertype BasedParUnitSig = (Node, UnitSig)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maedertype StParUnitCtx = Table UNIT_NAME BasedParUnitSig
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maedertype ExtStUnitCtx = (StParUnitCtx, StBasedUnitCtx, G_diagram)
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maedertype ArchSig = (ExtStUnitCtx, UnitSig)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder-- The global environment
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maederdata GlobalEntry =
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder SpecDefnEnv GenericityEnv SpecLenv
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder | ViewDefnEnv GenericityEnv SpecLenv G_morphism SpecLenv
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder | ArchSpecDefnEnv ArchSig
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder | UnitSpecDefnEnv UnitSig
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederdata GlobalEnv = GlobalEnv (Table SIMPLE_ID GlobalEntry) [Annotation]
d48085f765fca838c1d972d2123601997174583dChristian MaederemptyGlobalEnv = []
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder-- Flattened global environment
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maederdata FSign = FSign {
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder fFlattenedEnv, fHiddenEnv :: G_local_env,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder fAxioms :: G_l_sentence_list
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederdata FGenericityEnv = FGenericityEnv {
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder fAllImports :: FSign,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder fFormalParams :: FSign,
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder fFlattenedParams :: FSign
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederdata FGlobalEntry =
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder FSpecDefnEnv FGenericityEnv FSign
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder | FViewDefnEnv FGenericityEnv FSign G_morphism FSign
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder | FArchSpecDefnEnv ArchSig
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder | FUnitSpecDefnEnv UnitSig
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederdata FGlobalEnv = FGlobalEnv (Table SIMPLE_ID FGlobalEntry) [Annotation]
d48085f765fca838c1d972d2123601997174583dChristian MaederemptyFGlobalEnv = []
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maedertype LibEnv = Table String (GlobalEnv, LIB_DEFN)
d48085f765fca838c1d972d2123601997174583dChristian MaederemptyLibEnv = []