AS_Structured.der.hs revision 53ea24e19dbd4ca72fd75ab3a3105dc9f99e4f81
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- |
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : abstract syntax of CASL structured specifications
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Klaus Luettich, Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : till@informatik.uni-bremen.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable(Grothendieck)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederAbstract syntax of HetCASL (heterogeneous) structured specifications
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski Follows Sect. II:2.2.3 of the CASL Reference Manual.
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski-}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedermodule Syntax.AS_Structured where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder-- DrIFT command:
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-! global: GetRange !-}
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Id
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.AS_Annotation
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport Logic.Logic (AnyLogic)
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Logic.Grothendieck
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder ( G_basic_spec
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , G_symb_items_list
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder , G_symb_map_items_list
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang , LogicGraph
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , setCurLogic
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder , setCurSublogic )
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- for spec-defn and view-defn see AS_Library
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata SPEC = Basic_spec G_basic_spec Range
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder | EmptySpec Range
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder | Translation (Annoted SPEC) RENAMING
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Reduction (Annoted SPEC) RESTRICTION
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder | Union [Annoted SPEC] Range
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder -- pos: "and"s
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich | Extension [Annoted SPEC] Range
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -- pos: "then"s
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich | Free_spec (Annoted SPEC) Range
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- pos: "free"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder | Cofree_spec (Annoted SPEC) Range
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- pos: "cofree"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder | Local_spec (Annoted SPEC) (Annoted SPEC) Range
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu -- pos: "local", "within"
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder | Closed_spec (Annoted SPEC) Range
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder -- pos: "closed"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Group (Annoted SPEC) Range
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder -- pos: "{","}"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | Spec_inst SPEC_NAME [Annoted FIT_ARG] Range
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- pos: many of "[","]"; one balanced pair per FIT_ARG
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | Qualified_spec Logic_name (Annoted SPEC) Range
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- pos: "logic", Logic_name,":"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | Data AnyLogic AnyLogic (Annoted SPEC) (Annoted SPEC) Range
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- pos: "data"
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder deriving Show
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder{- Renaming and Hiding can be performend with intermediate Logic
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder mappings / Logic projections.
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder-}
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederdata RENAMING = Renaming [G_mapping] Range
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder -- pos: "with", list of comma pos
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder deriving (Show, Eq)
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederdata RESTRICTION = Hidden [G_hiding] Range
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder -- pos: "hide", list of comma pos
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder | Revealed G_symb_map_items_list Range
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder -- pos: "reveal", list of comma pos
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder deriving (Show, Eq)
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederdata G_mapping = G_symb_map G_symb_map_items_list
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder | G_logic_translation Logic_code
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder deriving (Show, Eq)
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maederdata G_hiding = G_symb_list G_symb_items_list
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder | G_logic_projection Logic_code
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder deriving (Show, Eq)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maederdata FIT_ARG = Fit_spec (Annoted SPEC) [G_mapping] Range
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder -- pos: opt "fit"
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder | Fit_view VIEW_NAME [Annoted FIT_ARG] Range
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder -- annotations before the view keyword are stored in Spec_inst
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder deriving Show
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maedertype SPEC_NAME = SIMPLE_ID
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maedertype VIEW_NAME = SIMPLE_ID
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata Logic_code = Logic_code (Maybe Token)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (Maybe Logic_name)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (Maybe Logic_name) Range
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder {- pos: "logic",<encoding>,":",<src-logic>,"->",<targ-logic>
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder one of <encoding>, <src-logic> or <targ-logic>
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder must be given (by Just)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "logic bla" => <encoding> only
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "logic bla ->" => <src-logic> only
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder "logic -> bla" => <targ-logic> only
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder "logic bla1 -> bla2" => <src-logic> and <targ-logic>
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- "logic bla1:bla2" => <encoding> and <src-logic>
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski this notation is not very useful and is not maintained
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder "logic bla1:bla2 ->" => <encoding> and <src-logic> (!)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "logic bla1: ->bla2" => <encoding> and <targ-logic> -}
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder deriving (Show, Eq)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederdata Logic_name = Logic_name Token (Maybe Token) (Maybe SPEC_NAME)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder deriving (Show, Eq)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian MaedersetLogicName :: Logic_name -> LogicGraph -> LogicGraph
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedersetLogicName (Logic_name lid _ ms) =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder setCurSublogic ms . setCurLogic (tokStr lid)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski