01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- |

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : static analysis of heterogeneous structured specifications

1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Till Mossakowski and Uni Bremen 2003-2006

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : till@informatik.uni-bremen.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable (imports Logic.Grothendieck)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederStatic analysis of CASL (heterogeneous) structured specifications

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski Follows the verfication semantic rules in Chap. IV:4.7

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski of the CASL Reference Manual.

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-}

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedermodule Static.AnalysisStructured

f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder ( anaSpec

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , anaSpecTop

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , anaUnion

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , getSpecAnnos

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , isStructured

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , anaRenaming

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang , anaRestriction

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder , partitionGmaps

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , homogenizeGM

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , anaGmaps

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang , insGSig

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , insLink

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder , extendMorphism

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , insGTheory

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ) where

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Driver.Options

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederimport Logic.Logic

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Logic.ExtSign

90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maederimport Logic.Coerce

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maederimport Logic.Comorphism

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichimport Logic.Grothendieck

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederimport Logic.Prover

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Static.DevGraph

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Static.DgUtils

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Static.GTheory

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport Syntax.AS_Structured

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederimport Syntax.Print_AS_Structured ()

986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.AS_Annotation hiding (isAxiom, isDef)

8e80792f474d154ff11762fac081a422e34f1accChristian Maederimport Common.Consistency

03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.DocUtils

03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.ExtSign

03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.Id

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederimport Common.LibName

03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.Result

03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.Utils (number)

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maederimport Common.Lib.MapSet (imageSet, setInsert)

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederimport Data.Graph.Inductive.Graph as Graph (Node)

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederimport qualified Data.Set as Set

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederimport qualified Data.Map as Map

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederimport Data.List (find)

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederimport Control.Monad

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedercoerceMaybeNode :: LogicGraph -> DGraph -> MaybeNode -> NodeName -> AnyLogic

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder -> Result (MaybeNode, DGraph)

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedercoerceMaybeNode lg dg mn nn l2 = case mn of

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder EmptyNode _ -> return (EmptyNode l2, dg)

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder JustNode ns -> do

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (ms, dg2) <- coerceNode lg dg ns nn l2

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return (JustNode ms, dg2)

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedercoerceNode :: LogicGraph -> DGraph -> NodeSig -> NodeName -> AnyLogic

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -> Result (NodeSig, DGraph)

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedercoerceNode lg dg ns@(NodeSig _ (G_sign lid1 _ _)) nn l2@(Logic lid2) =

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder if language_name lid1 == language_name lid2 then return (ns, dg)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else do

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder c <- logicInclusion lg (Logic lid1) l2

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder coerceNodeByComorph c dg ns nn

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedercoerceNodeByComorph :: AnyComorphism -> DGraph -> NodeSig -> NodeName

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> Result (NodeSig, DGraph)

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedercoerceNodeByComorph c dg (NodeSig n s) nn = do

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder gmor <- gEmbedComorphism c s

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder case find (\ (_, _, l) -> dgl_origin l == SeeTarget

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder && dgl_type l == globalDef

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder && dgl_morphism l == gmor) $ outDG dg n of

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Nothing -> do

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let (ms@(NodeSig m _), dg2) =

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder insGSig dg (extName "XCoerced" nn) DGLogicCoercion $ cod gmor

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder dg3 = insLink dg2 gmor globalDef SeeTarget n m

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return (ms, dg3)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just (_, t, _) ->

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return (NodeSig t $ signOf $ dgn_theory $ labDG dg t, dg)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiinsGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiinsGTheory dg name orig (G_theory lid sig ind sens tind) =

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder let (sgMap, s) = sigMapI dg

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (tMap, t) = thMapI dg

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder nind = if ind == startSigId then succ s else ind

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder tb = tind == startThId && not (Map.null sens)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ntind = if tb then succ t else tind

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder nsig = G_sign lid sig nind

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder nth = G_theory lid sig nind sens ntind

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder node_contents = newNodeLab name orig nth

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder node = getNewNodeDG dg

26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder in (NodeSig node nsig,

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (if tb then setThMapDG $ Map.insert (succ t) nth tMap else id) $

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (if ind == startSigId

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder then setSigMapDG $ Map.insert (succ s) nsig sgMap else id)

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder $ insNodeDG (node, node_contents) dg)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaederinsGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederinsGSig dg name orig (G_sign lid sig ind) =

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder insGTheory dg name orig $ noSensGTheory lid sig ind

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederinsLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -> DGraph

aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederinsLink dg (GMorphism cid sign si mor mi) ty orig n t =

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder let (sgMap, s) = sigMapI dg

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (mrMap, m) = morMapI dg

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder nsi = if si == startSigId then succ s else si

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder nmi = if mi == startMorId then succ m else mi

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder nmor = GMorphism cid sign nsi mor nmi

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder link = defDGLink nmor ty orig

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in (if mi == startMorId then setMorMapDG $ Map.insert (succ m)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (toG_morphism nmor) mrMap else id) $

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (if si == startSigId then setSigMapDG $ Map.insert (succ s)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (G_sign (sourceLogic cid) sign nsi) sgMap else id)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ insLEdgeNubDG (n, t, link) dg

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder

5e46b572ed576c0494768998b043d9d340594122Till MossakowskicreateConsLink :: LinkKind -> Conservativity -> LogicGraph -> DGraph

74d9a385499bf903b24848dff450a153f525bda7Christian Maeder -> MaybeNode -> NodeSig -> DGLinkOrigin -> Result DGraph

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedercreateConsLink lk conser lg dg nsig (NodeSig node gsig) orig = case nsig of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder EmptyNode _ | conser == None -> return dg

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> case nsig of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder JustNode (NodeSig n sig) -> do

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder incl <- ginclusion lg sig gsig

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ insLink dg incl

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (ScopedLink Global lk $ mkConsStatus conser) orig n node

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder EmptyNode _ -> -- add conservativity to the target node

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ let lbl = labDG dg node

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in if isDGRef lbl then dg else

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder fst $ labelNodeDG

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (node, lbl

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder { nodeInfo =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (nodeInfo lbl)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder { node_cons_status = case getNodeConsStatus lbl of

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ConsStatus c d th -> ConsStatus (max c conser) d th }}) dg

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederanaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> MaybeNode -> NodeName -> HetcatsOpts -> SPEC

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Result (SPEC, NodeSig, DGraph)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederanaSpecTop conser addSyms lg ln dg nsig name opts sp =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder if conser == None || case sp of

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- for these cases def-links are re-used

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Basic_spec _ _ -> True

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Closed_spec _ _ -> True

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Spec_inst _ _ _ -> True

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Group _ _ -> True -- in this case we recurse

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder _ -> False

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder then anaSpecAux conser addSyms lg ln dg nsig name opts sp else do

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder let provenThmLink =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ThmLink $ Proven (DGRule "static analysis") emptyProofBasis

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (rsp, ns, rdg) <- anaSpec addSyms lg ln dg nsig name opts sp

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ndg <- createConsLink provenThmLink conser lg rdg nsig ns SeeTarget

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder return (rsp, ns, ndg)

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder

99476ac2689c74251219db4782e57fe713a24a52Christian MaederanaFreeOrCofreeSpec :: Bool -> LogicGraph -> HetcatsOpts -> LibName -> DGraph

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> MaybeNode -> NodeName -> FreeOrCofree -> Annoted SPEC -> Range

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -> Result (Annoted SPEC, NodeSig, DGraph)

99476ac2689c74251219db4782e57fe713a24a52Christian MaederanaFreeOrCofreeSpec addSyms lg opts ln dg nsig name dglType asp pos =

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder adjustPos pos $ do

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (sp', NodeSig n' gsigma, dg') <-

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder anaSpec addSyms lg ln dg nsig (extName (show dglType) name) opts

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder $ item asp

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder let (ns@(NodeSig node _), dg2) =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder insGSig dg' name (DGFreeOrCofree dglType) gsigma

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder nsigma = case nsig of

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder EmptyNode cl -> emptyG_sign cl

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder JustNode nds -> getSig nds

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder incl <- ginclusion lg nsigma gsigma

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return (replaceAnnoted sp' asp, ns,

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder insLink dg2 incl (FreeOrCofreeDefLink dglType nsig)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder SeeTarget n' node)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder{- | analyze a SPEC. The Bool Parameter determines if incoming symbols shall

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maederbe ignored. The options are needed to check: shall only the structure be

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maederanalysed? -}

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederanaSpec :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder -> HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, DGraph)

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaederanaSpec = anaSpecAux None

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaederanaSpecAux :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> MaybeNode -> NodeName -> HetcatsOpts -> SPEC

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> Result (SPEC, NodeSig, DGraph)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederanaSpecAux conser addSyms lg ln dg nsig name opts sp = case sp of

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Basic_spec (G_basic_spec lid bspec) pos -> adjustPos pos $ do

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let curLogic = Logic lid

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (nsig', dg0) <- coerceMaybeNode lg dg nsig name curLogic

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder G_sign lid' sigma' _ <- return $ case nsig' of

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder EmptyNode cl -> emptyG_sign cl

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder JustNode ns -> getSig ns

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder ExtSign sig sys <-

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder coerceSign lid' lid "Analysis of basic spec" sigma'

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (bspec', ExtSign sigma_complete sysd, ax) <-

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder if isStructured opts

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder then return (bspec, mkExtSign $ empty_signature lid, [])

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let res@(Result ds mb) = extBasicAnalysis lid (getName name)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (getLibId ln) bspec sig $ globalAnnos dg0

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in case mb of

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Nothing | null ds ->

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder fail "basic analysis failed without giving a reason"

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder _ -> res

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder diffSig <- case signatureDiff lid sigma_complete sig of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Result _ (Just ds) -> return ds

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> warning sigma_complete

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder "signature difference could not be computed using full one" pos

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let gsysd = Set.map (G_symbol lid) sysd

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (ns, dg') = insGTheory dg0 name

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (DGBasicSpec (Just $ G_basic_spec lid bspec')

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (G_sign lid (mkExtSign diffSig) startSigId) gsysd)

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $ G_theory lid (ExtSign sigma_complete

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder $ Set.intersection

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (if addSyms then Set.union sys sysd else sysd)

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder $ symset_of lid sigma_complete)

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder startSigId (toThSens ax) startThId

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (Basic_spec (G_basic_spec lid bspec') pos, ns, dg'')

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder EmptySpec pos -> case nsig of

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder EmptyNode _ -> do

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder warning () "empty spec" pos

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return (sp, ns, dg')

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder {- anaSpec should be changed to return a MaybeNode!

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Then this duplicate dummy node could be avoided.

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Also empty unions could be treated then -}

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder JustNode ns -> return (sp, ns , dg)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Translation asp ren ->

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do let sp1 = item asp

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (sp1', ns'@(NodeSig n' gsigma), dg') <-

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder anaSpec addSyms lg ln dg nsig (extName "Translation" name) opts sp1

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder mor <- anaRenaming lg nsig gsigma opts ren

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- ??? check that mor is identity on local env

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder when (isIdentity mor) $ warning ()

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder ("nothing renamed by:\n" ++ showDoc ren "") $ getRange ren

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (fs, dgf) <- if isIdentity mor && isInternal name then return (ns', dg')

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder else do

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let (ns@(NodeSig node _), dg'') =

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder insGSig dg' name (DGTranslation $ Renamed ren) $ cod mor

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- ??? too simplistic for non-comorphism inter-logic translations

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder return (ns, insLink dg'' mor globalDef SeeTarget n' node)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return (Translation (replaceAnnoted sp1' asp) ren, fs, dgf)

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Reduction asp restr ->

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder do let sp1 = item asp

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder rname = extName "Restriction" name

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder (sp1', ns0, dg0) <- anaSpec addSyms lg ln dg nsig rname opts sp1

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder rLid <- getRestrLogic restr

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder p1@(NodeSig n' gsigma', dg') <- coerceNode lg dg0 ns0 rname rLid

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (hmor, tmor) <- anaRestriction lg (getMaybeSig nsig) gsigma' opts restr

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let noRename = maybe True isIdentity tmor

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder noHide = isIdentity hmor

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder when noHide $ (if noRename then warning else hint) ()

0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder ("nothing hidden by:\n" ++ showDoc restr "") $ getRange restr

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder p2@(NodeSig node1 _, dg2) <- if noHide && isInternal name then return p1

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder else do

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let trgSg = dom hmor

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder hidSyms = Set.difference (symsOfGsign gsigma')

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder $ symsOfGsign trgSg

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder orig = DGRestriction (Restricted restr) hidSyms

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (ns@(NodeSig node _), dg'') = insGSig dg'

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (if noRename then name else extName "Hiding" name)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder orig trgSg

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder return (ns, insLink dg'' hmor HidingDefLink SeeTarget n' node)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder {- we treat hiding and revealing differently

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder in order to keep the dg as simple as possible -}

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (fs, dgf) <- case tmor of

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Just tmor' | not noRename -> do

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let (ns@(NodeSig node2 _), dg3) =

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder insGSig dg2 name DGRevealTranslation $ cod tmor'

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder return (ns, insLink dg3 tmor' globalDef SeeTarget node1 node2)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Nothing -> return p2

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder _ -> hint p2 ("nothing renamed by:\n" ++ showDoc restr "")

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder $ getRange restr

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return (Reduction (replaceAnnoted sp1' asp) restr, fs, dgf)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Union asps pos -> do

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (newAsps, _, ns, dg') <- adjustPos pos $ anaUnion addSyms lg ln dg nsig

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder name opts asps

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder return (Union newAsps pos, ns, dg')

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Extension asps pos -> do

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let namedSps = map (\ (asp, n) ->

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let nn = incBy n (extName "Extension" name) in

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder if n < length asps then (nn, asp)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder else (name { xpath = xpath nn }, asp)) $ number asps

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (sps', nsig1', dg1, _, _) <- foldM (anaExtension lg opts ln pos)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder ([], nsig, dg, conser, addSyms) namedSps

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder case nsig1' of

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder EmptyNode _ -> fail "empty extension"

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder JustNode nsig1 -> return (Extension (zipWith replaceAnnoted

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder (reverse sps') asps)

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder pos, nsig1, dg1)

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Free_spec asp poss -> do

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder name Free asp poss

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder return (Free_spec nasp poss, nsig', dg')

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Cofree_spec asp poss -> do

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder name Cofree asp poss

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (Cofree_spec nasp poss, nsig', dg')

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Local_spec asp asp' poss -> adjustPos poss $ do

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let sp1 = item asp

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder sp1' = item asp'

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder lname = extName "Local" name

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder (sp2, nsig'@(NodeSig _ gsig1), dg') <-

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder anaSpec False lg ln dg nsig (extName "Spec" lname) opts sp1

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder (sp2', NodeSig n'' gsig2@(G_sign lid2 sigma2 _), dg'') <- anaSpec False lg

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ln dg' (JustNode nsig') (extName "Within" lname) opts sp1'

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let gSigN = getMaybeSig nsig

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (G_sign lid sigmaN _, _) <- gSigCoerce lg gSigN (Logic lid2)

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder sigma <- coerceSign lid lid2 "Analysis of local spec1" sigmaN

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder (G_sign lid' sigma' _, _) <- gSigCoerce lg gsig1 (Logic lid2)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sigma1 <- coerceSign lid' lid2 "Analysis of local spec2" sigma'

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let sys = ext_sym_of lid2 sigma

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder sys1 = ext_sym_of lid2 sigma1

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder sys2 = ext_sym_of lid2 sigma2

44d2a211a352759ee988ed8353026f5fa9511209Christian Maeder mor3 <- if isStructured opts then return (ext_ide sigma2)

44d2a211a352759ee988ed8353026f5fa9511209Christian Maeder else ext_cogenerated_sign lid2

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder (sys1 `Set.difference` sys) sigma2

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let sigma3 = dom mor3

4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder gsigma3 = G_sign lid2 (makeExtSign lid2 sigma3) startSigId

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sys3 = symset_of lid2 sigma3

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder unless (isStructured opts

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder || sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3)

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder $ plain_error () (

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder "illegal use of locally declared symbols: "

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ++ showDoc ((sys2 `Set.intersection` sys1) `Set.difference` sys3) "")

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder poss

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let hidSyms = Set.difference (symsOfGsign gsig2) $ symsOfGsign gsigma3

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder orig = DGRestriction NoRestriction hidSyms

4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder (ns@(NodeSig node _), dg2) = insGSig dg'' name orig gsigma3

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return (Local_spec (replaceAnnoted sp2 asp)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (replaceAnnoted sp2' asp')

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder poss, ns,

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid2 mor3)

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder HidingDefLink SeeTarget n'' node)

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder Closed_spec asp pos -> adjustPos pos $ do

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder let sp1 = item asp

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder l = getLogic nsig

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder -- analyse spec with empty local env

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder (sp', NodeSig n' gsigma', dg') <- anaSpec False lg ln dg

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder (EmptyNode l) (extName "Closed" name) opts sp1

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder gsigma2 <- gsigUnionMaybe lg nsig gsigma'

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder let (ns@(NodeSig node _), dg2) = insGSig dg' name DGClosed gsigma2

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski incl2 <- ginclusion lg gsigma' gsigma2

74d9a385499bf903b24848dff450a153f525bda7Christian Maeder let dg3 = insLink dg2 incl2 globalDef SeeTarget n' node

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski dg4 <- createConsLink DefLink conser lg dg3 nsig ns DGLinkClosedLenv

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return (Closed_spec (replaceAnnoted sp' asp) pos, ns, dg4)

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder Qualified_spec lognm asp pos -> adjustPos pos $ do

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let newLG = setLogicName lognm lg

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder l <- lookupCurrentLogic "Qualified_spec" newLG

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let newNSig = case nsig of

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder EmptyNode _ -> EmptyNode l

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski _ -> nsig

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski qname = extName "Qualified" name

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (sp', ns', dg') <- anaSpec addSyms newLG ln dg newNSig qname opts

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder $ item asp

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (ns, dg2) <- coerceNode lg dg' ns' qname l

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return (Qualified_spec lognm asp { item = sp' } pos, ns, dg2)

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Group asp pos -> do

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder (sp', nsig', dg') <-

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder anaSpecTop conser addSyms lg ln dg nsig name opts (item asp)

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder return (Group (replaceAnnoted sp' asp) pos, nsig', dg')

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Spec_inst spname afitargs pos0 -> let

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder pos = if null afitargs then tokPos spname else pos0

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder in adjustPos pos $ case lookupGlobalEnvDG spname dg of

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Just (SpecEntry gs@(ExtGenSig (GenSig _ params _)

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder body@(NodeSig nB gsigmaB))) ->

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder case (length afitargs, length params) of

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder -- the case without parameters leads to a simpler dg

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder (0, 0) -> case nsig of

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder -- if the node shall not be named and the logic does not change,

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder EmptyNode _ | isInternal name -> do

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder dg2 <- createConsLink DefLink conser lg dg nsig body SeeTarget

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder -- then just return the body

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder return (sp, body, dg2)

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- otherwise, we need to create a new one

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> do

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder gsigma <- gsigUnionMaybe lg nsig gsigmaB

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder let (fsig@(NodeSig node _), dg2) =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder insGSig dg name (DGInst spname) gsigma

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder incl <- ginclusion lg gsigmaB gsigma

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder let dg3 = case nsig of

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder JustNode (NodeSig nI _) | nI == nB -> dg2

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> insLink dg2 incl globalDef (DGLinkMorph spname) nB node

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder dg4 <- createConsLink DefLink conser lg dg3 nsig fsig SeeTarget

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder return (sp, fsig, dg4)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- now the case with parameters

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder (la, lp) | la == lp -> do

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder (ffitargs, dg', (morDelta, gsigmaA, ns@(NodeSig nA gsigmaRes))) <-

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski anaAllFitArgs lg opts ln dg nsig name spname gs afitargs

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder GMorphism cid _ _ _ _ <- return morDelta

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder morDelta' <- case nsig of

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder EmptyNode _

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder | logicOfGsign gsigmaA == logicOfGsign gsigmaRes

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> return morDelta

5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder _ -> ginclusion lg gsigmaA gsigmaRes >>= comp morDelta

5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder (_, imor) <- gSigCoerce lg gsigmaB $ Logic $ sourceLogic cid

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder tmor <- gEmbedComorphism imor gsigmaB

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder morDelta'' <- comp tmor morDelta'

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder let dg4 = case nsig of

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski JustNode (NodeSig nI _) | nI == nB -> dg'

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder _ -> insLink dg' morDelta'' globalDef (DGLinkMorph spname) nB nA

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder dg5 <- createConsLink DefLink conser lg dg4 nsig ns SeeTarget

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder return (Spec_inst spname ffitargs pos, ns, dg5)

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder | otherwise -> instMismatchError spname lp la pos

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder _ -> notFoundError "Structured specification" spname pos

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder -- analyse "data SPEC1 SPEC2"

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder Data lD@(Logic lidD) lP asp1 asp2 pos -> adjustPos pos $ do

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder let sp1 = item asp1

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder sp2 = item asp2

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder {- look for the inclusion comorphism from the current logic's data logic

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder into the current logic itself -}

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder c <- logicInclusion lg lD lP

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder let dname = extName "Data" name

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder -- analyse SPEC1

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (sp1', ns', dg') <- anaSpec False (setCurLogic (language_name lidD) lg)

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder ln dg (EmptyNode lD) dname opts sp1

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- force the result to be in the data logic

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder (ns'', dg'') <- coerceNode lg dg' ns' (extName "Qualified" dname) lD

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder -- translate SPEC1's signature along the comorphism

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder (nsig2@(NodeSig node gsigmaD), dg2) <-

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder coerceNodeByComorph c dg'' ns'' dname

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder (usig, udg) <- case nsig of

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder EmptyNode _ -> return (nsig2, dg2)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski JustNode ns2 -> do

32562a567baac248a00782d2727716c13117dc4aChristian Maeder gsigma2 <- gsigUnion lg (getSig ns2) gsigmaD

32562a567baac248a00782d2727716c13117dc4aChristian Maeder let (ns@(NodeSig node2a _), dg2a) =

32562a567baac248a00782d2727716c13117dc4aChristian Maeder insGSig dg2 (extName "Union" name) DGUnion gsigma2

32562a567baac248a00782d2727716c13117dc4aChristian Maeder incl2 <- ginclusion lg gsigmaD gsigma2

32562a567baac248a00782d2727716c13117dc4aChristian Maeder let dg3 = insLink dg2a incl2 globalDef SeeTarget node node2a

32562a567baac248a00782d2727716c13117dc4aChristian Maeder dg4 <- createConsLink DefLink conser lg dg3 nsig ns SeeTarget

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return (ns, dg4)

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -- analyse SPEC2

32562a567baac248a00782d2727716c13117dc4aChristian Maeder (sp2', nsig3, udg3) <-

32562a567baac248a00782d2727716c13117dc4aChristian Maeder anaSpec addSyms lg ln udg (JustNode usig) name opts sp2

32562a567baac248a00782d2727716c13117dc4aChristian Maeder return (Data lD lP

32562a567baac248a00782d2727716c13117dc4aChristian Maeder (replaceAnnoted sp1' asp1)

32562a567baac248a00782d2727716c13117dc4aChristian Maeder (replaceAnnoted sp2' asp2)

32562a567baac248a00782d2727716c13117dc4aChristian Maeder pos, nsig3, udg3)

746440cc1b984a852f5864235b8fa3930963a081Christian Maeder

32562a567baac248a00782d2727716c13117dc4aChristian MaederinstMismatchError :: SIMPLE_ID -> Int -> Int -> Range -> Result a

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederinstMismatchError spname lp la = fatal_error $ tokStr spname ++ " expects "

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ++ show lp ++ " arguments" ++ " but was given " ++ show la

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaedernotFoundError :: String -> SIMPLE_ID -> Range -> Result a

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian MaedernotFoundError str sid = fatal_error $ str ++ " " ++ tokStr sid ++ " not found"

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedergsigUnionMaybe :: LogicGraph -> MaybeNode -> G_sign -> Result G_sign

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedergsigUnionMaybe lg mn gsig = case mn of

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder EmptyNode _ -> return gsig

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder JustNode ns -> gsigUnion lg (getSig ns) gsig

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

fa167e362877db231378e17ba49c66fbb84862fcChristian MaederanaUnion :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName

4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder -> HetcatsOpts -> [Annoted SPEC]

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederanaUnion addSyms lg ln dg nsig name opts asps = case asps of

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder [] -> fail "empty union"

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder _ -> do

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let sps = map item asps

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (sps', nsigs, dg', _) <-

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let ana (sps1, nsigs, dg', n) sp' = do

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let n1 = inc n

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (sp1, nsig', dg1) <- anaSpec addSyms lg ln dg' nsig n1 opts sp'

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder return (sp1 : sps1, nsig' : nsigs, dg1, n1)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder in foldM ana ([], [], dg, extName "Union" name) sps

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let newAsps = zipWith replaceAnnoted (reverse sps') asps

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder case nsigs of

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder [ns] -> return (newAsps, nsigs, ns, dg')

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder _ -> do

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let nsigs' = reverse nsigs

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder gbigSigma <- gsigManyUnion lg (map getSig nsigs')

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let (ns@(NodeSig node _), dg2) = insGSig dg' name DGUnion gbigSigma

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder insE dgl (NodeSig n gsigma) = do

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder incl <- ginclusion lg gsigma gbigSigma

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder return $ insLink dgl incl globalDef SeeTarget n node

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder dg3 <- foldM insE dg2 nsigs'

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder return (newAsps, nsigs', ns, dg3)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- analysis of renamings

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian MaederanaRen :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder -> G_mapping -> Result GMorphism

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederanaRen lg opts lenv pos gmor@(GMorphism r sigma ind1 mor _) gmap =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder adjustPos pos $ case gmap of

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder G_symb_map (G_symb_map_items_list lid sis) ->

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let lid2 = targetLogic r in

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder if language_name lid2 == language_name lid then

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder if isStructured opts then return gmor else do

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder src@(ExtSign sig _) <- return $ makeExtSign lid2 $ cod mor

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder rmap <- stat_symb_map_items lid2 sig Nothing sis1

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder mor1 <- ext_induced_from_morphism lid2 rmap src

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder case lenv of

32562a567baac248a00782d2727716c13117dc4aChristian Maeder EmptyNode _ -> return ()

32562a567baac248a00782d2727716c13117dc4aChristian Maeder JustNode (NodeSig _ sigLenv) -> do

32562a567baac248a00782d2727716c13117dc4aChristian Maeder -- needs to be changed for logic translations

32562a567baac248a00782d2727716c13117dc4aChristian Maeder (G_sign lid1 sigmaLenv1 _, _) <-

32562a567baac248a00782d2727716c13117dc4aChristian Maeder gSigCoerce lg sigLenv (Logic lid2)

32562a567baac248a00782d2727716c13117dc4aChristian Maeder sigmaLenv' <- coerceSign lid1 lid2 "" sigmaLenv1

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder let sysLenv = ext_sym_of lid2 sigmaLenv'

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder m = symmap_of lid2 mor1

32562a567baac248a00782d2727716c13117dc4aChristian Maeder isChanged sy = case Map.lookup sy m of

32562a567baac248a00782d2727716c13117dc4aChristian Maeder Just sy' -> sy /= sy'

32562a567baac248a00782d2727716c13117dc4aChristian Maeder Nothing -> False

32562a567baac248a00782d2727716c13117dc4aChristian Maeder forbiddenSys = Set.filter isChanged sysLenv

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski unless (Set.null forbiddenSys) $ plain_error () (

3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski "attempt to rename the following symbols from " ++

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder "the local environment:\n" ++ showDoc forbiddenSys "") pos

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder mor2 <- comp mor mor1

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder return $ GMorphism r sigma ind1 mor2 startMorId

3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski else do

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder comor <- logicInclusion lg (Logic lid2) (Logic lid)

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder gmorTrans <- gEmbedComorphism comor $ cod gmor

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder newMor <- comp gmor gmorTrans

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder anaRen lg opts lenv pos newMor gmap

ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski G_logic_translation (Logic_code tok src tar pos1) ->

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder let adj1 = adjustPos $ if pos1 == nullRange then pos else pos1

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder in adj1 $ do

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder G_sign srcLid srcSig ind <- return (cod gmor)

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder c <- case tok of

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder Just ctok -> lookupComorphism (tokStr ctok) lg

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Nothing -> case tar of

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder Just (Logic_name l _ _) ->

ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski lookupLogic "with logic: " (tokStr l) lg

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang >>= logicInclusion lg (Logic srcLid)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Nothing -> fail "with logic: cannot determine comorphism"

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang checkSrcOrTarLogic True c src

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder checkSrcOrTarLogic False c tar

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mor1 <- gEmbedComorphism c (G_sign srcLid srcSig ind)

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder comp gmor mor1

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangcheckSrcOrTarLogic :: Bool -> AnyComorphism -> Maybe Logic_name -> Result ()

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian MaedercheckSrcOrTarLogic b (Comorphism cid) ml = case ml of

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder Nothing -> return ()

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Just (Logic_name l _ _) -> let s = tokStr l in

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder when (s /= if b then language_name $ sourceLogic cid

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder else language_name $ targetLogic cid)

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder $ plain_error () (s ++ " is is not the "

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder ++ (if b then "source" else "target") ++ " logic of "

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder ++ language_name cid) (tokPos l)

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian MaederanaRenaming :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder -> Result GMorphism

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaederanaRenaming lg lenv gSigma opts (Renaming ren pos) =

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder foldM (anaRen lg opts lenv pos) (ide gSigma) ren

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaedergetRestrLogic :: RESTRICTION -> Result AnyLogic

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaedergetRestrLogic restr = case restr of

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder Revealed (G_symb_map_items_list lid _) _ -> return $ Logic lid

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Hidden l _ -> case l of

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder [] -> error "getRestrLogic"

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder h : _ -> case h of

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang G_symb_list (G_symb_items_list lid _) -> return $ Logic lid

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang G_logic_projection (Logic_code _ _ _ pos1) ->

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang fatal_error "no analysis of logic projections yet" pos1

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

-- analysis of restrictions

anaRestr :: LogicGraph -> G_sign -> Range -> GMorphism -> G_hiding

-> Result GMorphism

anaRestr lg sigEnv pos (GMorphism cid (ExtSign sigma1 sys1) _ mor _) gh =

case gh of

G_symb_list (G_symb_items_list lid' sis') -> do

let lid1 = sourceLogic cid

sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction1" sis'

rsys <- stat_symb_items lid1 sigma1 sis1

let sys = symset_of lid1 sigma1

sys' = Set.filter (\ sy -> any (matches lid1 sy) rsys) sys

unmatched = filter ( \ rsy -> Set.null $ Set.filter

( \ sy -> matches lid1 sy rsy) sys') rsys

unless (null unmatched)

$ plain_error () ("attempt to hide unknown symbols:\n"

++ showDoc unmatched "") pos

-- needs to be changed when logic projections are implemented

(G_sign lidE sigmaLenv0 _, _) <- gSigCoerce lg sigEnv (Logic lid1)

sigmaLenv' <- coerceSign lidE lid1 "" sigmaLenv0

let sysLenv = ext_sym_of lid1 sigmaLenv'

forbiddenSys = sys' `Set.intersection` sysLenv

unless (Set.null forbiddenSys)

$ plain_error () (

"attempt to hide the following symbols from the local environment:\n"

++ showDoc forbiddenSys "") pos

mor1 <- cogenerated_sign lid1 sys' sigma1

mor1' <- map_morphism cid mor1

mor2 <- comp mor1' mor

return $ GMorphism cid (ExtSign (dom mor1) $ Set.fold (\ sy ->

case Map.lookup sy $ symmap_of lid1 mor1 of

Nothing -> id

Just sy1 -> Set.insert sy1) Set.empty sys1)

startSigId mor2 startMorId

G_logic_projection (Logic_code _ _ _ pos1) ->

fatal_error "no analysis of logic projections yet" pos1

anaRestriction :: LogicGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION

-> Result (GMorphism, Maybe GMorphism)

anaRestriction lg gSigma gSigma'@(G_sign lid0 sig0 _) opts restr =

if isStructured opts then return (ide gSigma, Nothing) else

case restr of

Hidden rstr pos -> do

mor <- foldM (anaRestr lg gSigma pos) (ide gSigma') rstr

return (mor, Nothing)

Revealed (G_symb_map_items_list lid1 sis) pos -> adjustPos pos $ do

(G_sign lid sigma _, _) <- gSigCoerce lg gSigma (Logic lid1)

sigma0 <- coerceSign lid lid1 "reveal1" sigma

sigma1 <- coerceSign lid0 lid1 "reveal2" sig0

let sys = ext_sym_of lid1 sigma0 -- local env

sys' = ext_sym_of lid1 sigma1 -- "big" signature

rmap <- stat_symb_map_items lid1 (plainSign sigma1) Nothing sis

let sys'' = Set.fromList

[sy | sy <- Set.toList sys', rsy <-

Map.keys rmap, matches lid1 sy rsy]

{- domain of rmap intersected with sys'

rmap is checked by ext_induced_from_morphism below -}

mor1 <- ext_generated_sign lid1 (sys `Set.union` sys'') sigma1

let extsig1 = makeExtSign lid1 $ dom mor1

mor2 <- ext_induced_from_morphism lid1 rmap extsig1

return (gEmbed2 (G_sign lid1 extsig1 startSigId)

$ G_morphism lid1 mor1 startMorId

, Just $ gEmbed $ mkG_morphism lid1 mor2)

partitionGmaps :: [G_mapping] -> ([G_mapping], [G_mapping])

partitionGmaps l = let

(hs, rs) = span (\ sm -> case sm of

G_symb_map _ -> True

G_logic_translation _ -> False) $ reverse l

in (reverse rs, reverse hs)

anaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign

-> [G_mapping] -> Result G_morphism

anaGmaps lg opts pos psig@(G_sign lidP sigmaP _) asig@(G_sign lidA sigmaA _)

gsis = adjustPos pos $ if isStructured opts

then return $ mkG_morphism lidP $ ext_ide sigmaP

else if null gsis then do

(G_sign lidP' sigmaP' _, _) <- gSigCoerce lg psig (Logic lidA)

sigmaA' <- coerceSign lidA lidP' "anaGmaps" sigmaA

fmap (mkG_morphism lidP') $

ext_induced_from_to_morphism lidP' Map.empty sigmaP' sigmaA'

else do

cl <- lookupCurrentLogic "anaGmaps" lg

G_symb_map_items_list lid sis <- homogenizeGM cl gsis

(G_sign lidP' sigmaP'' _, _) <- gSigCoerce lg psig (Logic lid)

sigmaP' <- coerceSign lidP' lid "anaGmaps1" sigmaP''

(G_sign lidA' sigmaA'' _, _) <- gSigCoerce lg asig (Logic lid)

sigmaA' <- coerceSign lidA' lid "anaGmaps2" sigmaA''

rmap <- stat_symb_map_items lid (plainSign sigmaP')

(Just $ plainSign sigmaA') sis

fmap (mkG_morphism lid)

$ ext_induced_from_to_morphism lid rmap sigmaP' sigmaA'

{-

let symI = sym_of lidP sigmaI'

symmap_mor = symmap_of lidP mor

-- are symbols of the imports left untouched?

if Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI

then return ()

else plain_error () "Fitting morphism must not affect import" pos

-- does not work

-- also output symbols that are affected

-}

anaFitArg :: LogicGraph -> LibName -> DGraph -> SIMPLE_ID -> MaybeNode

-> NodeSig -> HetcatsOpts -> NodeName -> FIT_ARG

-> Result (FIT_ARG, DGraph, (G_morphism, NodeSig))

anaFitArg lg ln dg spname nsigI nsigP@(NodeSig nP gsigmaP) opts name fv =

case fv of

Fit_spec asp gsis pos -> do

(sp', nsigA, dg') <- anaSpec False lg ln dg nsigI name opts (item asp)

(_, Comorphism aid) <-

logicUnion lg (getNodeLogic nsigP) (getNodeLogic nsigA)

let tl = Logic $ targetLogic aid

(nsigA'@(NodeSig nA' gsigA'), dg'') <- coerceNode lg dg' nsigA name tl

(gsigmaP', pmor) <- gSigCoerce lg gsigmaP tl

tmor <- gEmbedComorphism pmor gsigmaP

gmor <- anaGmaps lg opts pos gsigmaP' gsigA' gsis

eGmor <- comp tmor $ gEmbed gmor

return ( Fit_spec (replaceAnnoted sp' asp) gsis pos

, if nP == nA' && isInclusion eGmor then dg'' else

insLink dg'' eGmor globalThm

(DGLinkInst spname $ Fitted gsis) nP nA'

, (gmor, nsigA'))

Fit_view vn afitargs pos -> case lookupGlobalEnvDG vn dg of

Just (ViewEntry (ExtViewSig (NodeSig nSrc gsigmaS) mor

gs@(ExtGenSig (GenSig _ params _) target@(NodeSig nTar _))))

-> adjustPos pos $ do

GMorphism cid _ _ morHom ind <- return mor

let lid = targetLogic cid

pname = dgn_name $ labDG dg nP

gsigmaI = getMaybeSig nsigI

dg5 <- do

gsigmaIS <- gsigUnionMaybe lg nsigI gsigmaS

unless (isSubGsign lg gsigmaP gsigmaIS

&& isSubGsign lg gsigmaIS gsigmaP)

(plain_error ()

("Parameter does not match source of fittig view. "

++ "Parameter signature:\n"

++ showDoc gsigmaP

"\nSource signature of fitting view (united with import):\n"

++ showDoc gsigmaIS "") pos)

(dg4, iSrc) <- case nsigI of

EmptyNode _ -> return (dg, nSrc)

JustNode (NodeSig nI _) -> do

inclI <- ginclusion lg gsigmaI gsigmaIS

inclS <- ginclusion lg gsigmaS gsigmaIS

let (NodeSig n' _, dg1) = insGSig dg (extName "View" name)

{xpath = xpath pname} (DGFitView vn) gsigmaIS

dg2 = insLink dg1 inclI globalDef

(DGLinkFitViewImp vn) nI n'

return (insLink dg2 inclS globalDef

(DGLinkFitViewImp vn) nSrc n', n')

if nP == iSrc then return dg4 else do

gmor <- ginclusion lg gsigmaP gsigmaIS

return $ insLink dg4 gmor globalThm (DGLinkFitView vn) nP iSrc

case (length afitargs, length params) of

-- the case without parameters leads to a simpler dg

(0, 0) -> return (fv, dg5, (G_morphism lid morHom ind, target))

-- now the case with parameters

(la, lp) | la == lp -> do

(ffitargs, dg', (gmor_f, _, ns@(NodeSig nA _))) <-

anaAllFitArgs lg opts ln dg5 (EmptyNode $ Logic lid)

name vn gs afitargs

mor1 <- comp mor gmor_f

GMorphism cid1 _ _ theta _ <- return mor1

let lid1 = targetLogic cid1

when (language_name (sourceLogic cid1) /= language_name lid1)

$ fatal_error "heterogeneous fitting views not yet implemented"

pos

let dg9 = insLink dg' gmor_f globalDef (DGLinkMorph vn) nTar nA

return (Fit_view vn ffitargs pos, dg9, (mkG_morphism lid1 theta, ns))

| otherwise -> instMismatchError spname lp la pos

_ -> notFoundError "View" vn pos

anaFitArgs :: LogicGraph -> HetcatsOpts -> LibName -> SIMPLE_ID -> MaybeNode

-> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)

-> (NodeSig, FIT_ARG)

-> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)

anaFitArgs lg opts ln spname imps (fas', dg1, args, name') (nsig', fa) = do

let n1 = inc name'

(fa', dg', arg) <- anaFitArg lg ln dg1 spname imps nsig' opts n1 fa

return (fa' : fas', dg', arg : args, n1)

anaAllFitArgs :: LogicGraph -> HetcatsOpts -> LibName -> DGraph -> MaybeNode

-> NodeName -> SIMPLE_ID -> ExtGenSig -> [Annoted FIT_ARG]

-> Result ([Annoted FIT_ARG], DGraph, (GMorphism, G_sign, NodeSig))

anaAllFitArgs lg opts ln dg nsig name spname

gs@(ExtGenSig (GenSig imps params _) _)

afitargs = do

let fitargs = map item afitargs

(fitargs', dg', args, _) <- foldM (anaFitArgs lg opts ln spname imps)

([], dg, [], extName "Actuals" name) (zip params fitargs)

let actualargs = reverse args

(gsigma', morDelta) <- applyGS lg gs actualargs

gsigmaRes <- gsigUnionMaybe lg nsig gsigma'

let (ns, dg2) = insGSig dg' name (DGInst spname) gsigmaRes

dg3 <- foldM (parLink lg nsig (DGLinkInstArg spname) ns) dg2

$ map snd actualargs

return ( zipWith replaceAnnoted (reverse fitargs') afitargs, dg3

, (morDelta, gsigma', ns))

parLink :: LogicGraph -> MaybeNode -> DGLinkOrigin -> NodeSig -> DGraph

-> NodeSig -> Result DGraph

parLink lg nsig orig (NodeSig node gsigma') dg (NodeSig nA_i sigA_i) =

case nsig of

JustNode (NodeSig nI _) | nI == nA_i -> return dg

-- actual parameter will be included via import

_ -> do

incl <- ginclusion lg sigA_i gsigma'

return $ insLink dg incl globalDef orig nA_i node

{- Extension of signature morphisms (for instantitations)

first some auxiliary functions -}

mapID :: Map.Map Id (Set.Set Id) -> Id -> Result Id

mapID idmap i@(Id toks comps pos1) =

case Map.lookup i idmap of

Nothing -> do

compsnew <- mapM (mapID idmap) comps

return (Id toks compsnew pos1)

Just ids -> case Set.toList ids of

[] -> return i

[h] -> return h

_ -> plain_error i

("Identifier component " ++ showId i

" can be mapped in various ways:\n"

++ showDoc ids "") $ getRange i

extID1 :: Map.Map Id (Set.Set Id) -> Id

-> Result (EndoMap Id) -> Result (EndoMap Id)

extID1 idmap i@(Id toks comps pos1) m = do

m1 <- m

compsnew <- mapM (mapID idmap) comps

return $ if comps == compsnew then m1 else

Map.insert i (Id toks compsnew pos1) m1

extID :: Set.Set Id -> Map.Map Id (Set.Set Id) -> Result (EndoMap Id)

extID ids idmap = Set.fold (extID1 idmap) (return Map.empty) ids

extendMorphism :: G_sign -- ^ formal parameter

-> G_sign -- ^ body

-> G_sign -- ^ actual parameter

-> G_morphism -- ^ fitting morphism

-> Result (G_sign, G_morphism)

extendMorphism (G_sign lid sigmaP _) (G_sign lidB sigmaB1 _)

(G_sign lidA sigmaA1 _) (G_morphism lidM fittingMor1 _) = do

-- for now, only homogeneous instantiations....

sigmaB@(ExtSign _ sysB) <-

coerceSign lidB lid "Extension of symbol map1" sigmaB1

sigmaA <- coerceSign lidA lid "Extension of symbol map2" sigmaA1

fittingMor <- coerceMorphism lidM lid "Extension of symbol map3" fittingMor1

let symsP = ext_sym_of lid sigmaP

symsB = ext_sym_of lid sigmaB

idsB = Set.map (sym_name lid) symsB

h = symmap_of lid fittingMor

symbMapToRawSymbMap =

Map.foldWithKey (\ sy1 sy2 -> Map.insert (symbol_to_raw lid sy1)

(symbol_to_raw lid sy2))

Map.empty

rh = symbMapToRawSymbMap h

idh = Map.foldWithKey

(\ sy1 sy2 -> setInsert (sym_name lid sy1) (sym_name lid sy2))

Map.empty h

idhExt <- extID idsB idh

let rIdExt = Map.foldWithKey (\ id1 id2 -> Map.insert

(id_to_raw lid id1) (id_to_raw lid id2))

Map.empty

(foldr Map.delete idhExt $ Map.keys idh)

r = rh `Map.union` rIdExt

-- do we need combining function catching the clashes???

mor <- ext_induced_from_morphism lid r sigmaB

let hmor = symmap_of lid mor

sigmaAD = ExtSign (cod mor) $ Set.map (\ sy ->

Map.findWithDefault sy sy hmor) sysB

sigma <- ext_signature_union lid sigmaA sigmaAD

let illShared = (ext_sym_of lid sigmaA `Set.intersection`

ext_sym_of lid sigmaAD )

Set.\\ imageSet h symsP

unless (Set.null illShared)

$ plain_error () ("Symbols shared between actual parameter and body"

++ "\nmust be in formal parameter:\n"

++ showDoc illShared "") nullRange

let myKernel = Set.fromDistinctAscList . comb1 . Map.toList

comb1 [] = []

comb1 (p : qs) =

comb2 p qs [] ++ comb1 qs

comb2 _ [] rs = rs

comb2 p@(a, b) ((c, d) : qs) rs =

comb2 p qs $ if b == d then (a, c) : rs else rs

newIdentifications = myKernel hmor Set.\\ myKernel h

unless (Set.null newIdentifications)

$ warning () (

"Fitting morphism may lead to forbidden identifications:\n"

++ showDoc newIdentifications "") nullRange

incl <- ext_inclusion lid sigmaAD sigma

mor1 <- comp mor incl

return (G_sign lid sigma startSigId, mkG_morphism lid mor1)

applyGS :: LogicGraph -> ExtGenSig -> [(G_morphism, NodeSig)]

-> Result (G_sign, GMorphism)

applyGS lg (ExtGenSig (GenSig nsigI _ gsigmaP) nsigB) args = do

let mor_i = map fst args

gsigmaA_i = map (getSig . snd) args

gsigmaB = getSig nsigB

gsigmaA@(G_sign lidA _ _) <- gsigManyUnion lg gsigmaA_i

(Comorphism bid, Comorphism uid) <-

logicUnion lg (getNodeLogic nsigB) (Logic lidA)

let cl = Logic $ targetLogic uid

G_morphism lidG mor0 _ <- case nsigI of

EmptyNode _ -> homogeneousMorManyUnion mor_i

JustNode (NodeSig _ gsigmaI) -> do

(G_sign lidI sigmaI _, _) <- gSigCoerce lg gsigmaI (Logic lidA)

let idI = ext_ide sigmaI

homogeneousMorManyUnion $ mkG_morphism lidI idI : mor_i

(gsigmaP', _) <- gSigCoerce lg (getMaybeSig gsigmaP) cl

(gsigmaB', _) <- gSigCoerce lg gsigmaB cl

(gsigmaA', Comorphism aid) <- gSigCoerce lg gsigmaA cl

mor1 <- coerceMorphism lidG (sourceLogic aid) "applyGS" mor0

mor2 <- map_morphism aid mor1

(gsig, G_morphism gid mor3 mId) <- extendMorphism gsigmaP' gsigmaB' gsigmaA' $

G_morphism (targetLogic aid) mor2 startMorId

case gsigmaB of

G_sign lidB sigB indB -> do

sigB' <- coerceSign lidB (sourceLogic bid) "applyGS2" sigB

mor4 <- coerceMorphism gid (targetLogic bid) "applyGS3" mor3

return (gsig, GMorphism bid sigB' indB mor4 mId)

homogenizeGM :: AnyLogic -> [G_mapping] -> Result G_symb_map_items_list

homogenizeGM (Logic lid) gsis =

foldM homogenize1 (G_symb_map_items_list lid []) gsis

where

homogenize1 (G_symb_map_items_list lid2 sis) sm = case sm of

G_symb_map (G_symb_map_items_list lid1 sis1) -> do

sis1' <- coerceSymbMapItemsList lid1 lid2 "" sis1

return $ G_symb_map_items_list lid2 $ sis ++ sis1'

G_logic_translation lc ->

fail $ "translation not supported by " ++ showDoc lc ""

-- | check if structured analysis should be performed

isStructured :: HetcatsOpts -> Bool

isStructured a = case analysis a of

Structured -> True

_ -> False

getSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)

getSpecAnnos pos a = do

let sannos = filter isSemanticAnno $ l_annos a

(sanno1, conflict, impliedA, impliesA) = case sannos of

f@(Semantic_anno anno1 _) : r -> (case anno1 of

SA_cons -> Cons

SA_def -> Def

SA_mono -> Mono

_ -> None, any (/= f) r,

anno1 == SA_implied, anno1 == SA_implies)

_ -> (None, False, False, False)

when conflict $ plain_error () "Conflicting semantic annotations" pos

when impliedA $ plain_error ()

"Annotation %implied should come after a BASIC-ITEM" pos

return (sanno1, impliesA)

-- only consider addSyms for the first spec

anaExtension :: LogicGraph -> HetcatsOpts -> LibName -> Range

-> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)

-> (NodeName, Annoted SPEC)

-> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)

anaExtension lg opts ln pos (sps', nsig', dg', conser, addSyms) (name', asp')

= do

(sanno1, impliesA) <- getSpecAnnos pos asp'

-- attach conservativity to definition link

(sp1', nsig1@(NodeSig n1 sig1), dg1) <- anaSpecTop (max conser sanno1)

addSyms lg ln dg' nsig' name' opts (item asp')

dg2 <- if impliesA then case nsig' of

JustNode (NodeSig n' sig') -> do

-- is the extension going between real nodes?

unless (isHomSubGsign sig1 sig') $ plain_error ()

"Signature must not be extended in presence of %implies" pos

-- insert a theorem link according to p. 319 of the CASL Reference Manual

return $ insLink dg1 (ide sig1) globalThm DGImpliesLink n1 n'

_ -> return dg1

else return dg1

return (sp1' : sps', JustNode nsig1, dg2, None, True)