AnalysisStructured.hs revision edd35c6c970fa1707dc6ad7a3ba26119e0046223
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : static analysis of CASL (heterogeneous) structured specifications
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003-2006
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederMaintainer : till@tzi.de
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederStability : provisional
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederPortability : non-portable (imports Logic.Grothendieck)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiStatic analysis of CASL (heterogeneous) structured specifications
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski Follows the verfication semantic rules in Chap. IV:4.7
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski of the CASL Reference Manual.
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maedermodule Static.AnalysisStructured (ana_SPEC, ana_GENERICITY,
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder ana_VIEW_TYPE, ana_err, isStructured,
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder ana_RENAMING, ana_RESTRICTION,
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder homogenizeGM, extendMorphism)
410ff490af511ffa09b52e4de631d36a154b9730Christian Maederimport Common.AS_Annotation hiding (isAxiom,isDef)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederimport qualified Common.Lib.Rel as Rel(image, setInsert)
410ff490af511ffa09b52e4de631d36a154b9730Christian Maederimport Data.List hiding (union)
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian MaederinsEdgeNub :: LEdge DGLinkLab -> DGraph -> DGraph
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederinsEdgeNub (v, w, l) g =
c1f654e5454af20eca35aa69f13c5144f405aed9Christian Maeder if (l, w) `elem` s then g
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian else g'{edgeCounter = edgeCounter g'+1,
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian (p, v, l', (l{dgl_id=[getNewEdgeID g]}, w) : s) & (dgBody g')}
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian where (Just (p, _, l', s), g') = matchDG v g
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- | analyze a SPEC
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- Parameters: global context, local environment,
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- the SIMPLE_ID may be a name if the specification shall be named,
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski-- options: here we need the info: shall only the structure be analysed?
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_SPEC :: LogicGraph -> GlobalContext -> MaybeNode -> NODE_NAME ->
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, GlobalContext)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederana_SPEC lg gctx nsig name opts sp =
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder let dg = devGraph gctx
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder in case sp of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Basic_spec (G_basic_spec lid bspec) ->
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder do G_sign lid' sigma' i1 <- return (getMaybeSig nsig)
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sigma <- coerceSign lid' lid "Analysis of basic spec" sigma'
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder (bspec', sigma_complete, ax) <-
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder if isStructured opts
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder then return (bspec, empty_signature lid, [])
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder else do b <- maybeToMonad
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski ("no basic analysis for logic "
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ language_name lid)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski (basic_analysis lid)
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder b (bspec, sigma, globalAnnos gctx)
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder let (sgMap, s) = sigMapI gctx
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (mrMap, m) = morMapI gctx
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (tMap, t) = thMapI gctx
e6aa023e6cf2d2c6978114a70d8c3ba7b8b027e1Christian Maeder gsig = G_sign lid sigma_complete (s+1)
2bb9a3bf532ca82f097e01da9ab9e06015c246afChristian Maeder incl <- ginclusion lg (G_sign lid sigma i1) gsig
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let gTh = G_theory lid sigma_complete (s+1) (toThSens ax) (t+1)
2bb9a3bf532ca82f097e01da9ab9e06015c246afChristian Maeder node_contents =
30f64088b9425c9b928bd4074e8f37ea35cb0278Till Mossakowski dgn_name = name,
2bb9a3bf532ca82f097e01da9ab9e06015c246afChristian Maeder dgn_theory = gTh,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -- no, not only the delta
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_origin = DGBasic,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian dg' = insNodeDG (node,node_contents) dg
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl' = updateMorIndex (m+1) incl
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = DGLink {
33902665eab01da3a367b5d67ed6513a5e669003Christian Maeder dgl_morphism = incl',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGExtension,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dg'' = case nsig of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder EmptyNode _ -> dg'
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n,node,link) dg'
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Basic_spec (G_basic_spec lid bspec'),
2bb9a3bf532ca82f097e01da9ab9e06015c246afChristian Maeder NodeSig node gsig,
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder gctx { devGraph = dg''
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang , sigMap = Map.insert (s+1) gsig sgMap
2bb9a3bf532ca82f097e01da9ab9e06015c246afChristian Maeder , thMap = Map.insert (t+1) gTh tMap
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang , morMap = Map.insert (m+1) (toG_morphism incl') mrMap})
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Translation asp ren ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp1', NodeSig n' gsigma, gctx') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder let (mrMap, m) = morMapI gctx'
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski mor <- ana_RENAMING lg nsig gsigma opts ren
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? check that mor is identity on local env
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder let gsigma' = cod Grothendieck mor
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- ??? too simplistic for non-comorphism inter-logic translations
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lid' gsig ind <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lid' gsig ind noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGTranslation,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang mor' = updateMorIndex (m+1) mor
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = mor',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGTranslation,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian dg'' = insNodeDG (node,node_contents) dg'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Translation (replaceAnnoted sp1' asp) ren,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma',
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gctx' { devGraph = insEdgeNub link dg''
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang , morMap = Map.insert (m+1) (toG_morphism mor') mrMap})
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Reduction asp restr ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp1', NodeSig n' gsigma', gctx') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let gsigma = getMaybeSig nsig
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (mrMap, m) = morMapI gctx'
6a57a555c8ef0a79aa5d20e1d721400dbffa564aMaciek Makowski (hmor,tmor) <- ana_RESTRICTION dg gsigma gsigma' opts restr
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- we treat hiding and revealing differently
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- in order to keep the dg as simple as possible
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let hmor' = updateMorIndex (m+1) hmor
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let gsigma'' = dom Grothendieck hmor
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lid' gsig ind <- return gsigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lid' gsig ind noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGHiding,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = hmor',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = HidingDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGHiding,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian dg'' = insNodeDG (node,node_contents) dg'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Reduction (replaceAnnoted sp1' asp) restr,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma'',
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder gctx' { devGraph = insEdgeNub link dg''
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = Map.insert (m+1) (toG_morphism hmor')
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just tmor' -> do
d08907a7832988612fbc0682b216e150d1e738d2Christian Maeder let gsigma1 = dom Grothendieck tmor'
d08907a7832988612fbc0682b216e150d1e738d2Christian Maeder gsigma'' = cod Grothendieck tmor'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lid1 gsig ind <- return gsigma1
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lid'' gsig'' ind'' <- return gsigma''
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the case with identity translation leads to a simpler dg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if tmor' == ide Grothendieck (dom Grothendieck tmor')
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian let node1 = getNewNodeDG dg'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski node_contents1 = DGNode {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lid1 gsig ind noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGRevealing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski link1 = (n',node1,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = hmor',
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = HidingDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGRevealing,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian dg'' = insNodeDG (node1,node_contents1) dg'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (Reduction (replaceAnnoted sp1' asp) restr,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node1 gsigma1,
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder gctx' { devGraph = insEdgeNub link1 dg''
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = Map.insert (m+1) (toG_morphism hmor')
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian let [node1,node''] = newNodesDG 2 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents1 = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = extName "T" name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lid1 gsig ind noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGRevealing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian link1 = (n',node1,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = hmor',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = HidingDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGRevealing,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents'' = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lid'' gsig'' ind'' noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGRevealTranslation,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link'' = (node1,node'',DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = tmor',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGRevealTranslation,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Reduction (replaceAnnoted sp1' asp) restr,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node'' gsigma'',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link'' $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node'',node_contents'') $
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder insEdgeNub link1 $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node1,node_contents1) dg'
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = Map.insert (m+1) (toG_morphism hmor')
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder Union [] pos -> adjustPos pos $ fail $ "empty union"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Union asps pos ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sps = map item asps
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sps', nsigs, gctx', _) <-
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski let ana r sp' = do
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski (sps1,nsigs,dg',n) <- r
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp1,nsig',dg1) <- ana_SPEC lg dg' nsig n opts sp'
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski return (sp1:sps1,nsig':nsigs,dg1,inc n)
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder in foldl ana (return ([], [], gctx, extName "U" name)) sps
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let nsigs' = reverse nsigs
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder adj = adjustPos pos
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (sgMap, s) = sigMapI gctx'
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski gbigSigma <- adj $ gsigManyUnion lg (map getSig nsigs')
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang G_sign lid' gsig _ <- return gbigSigma
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gbigSigma' <- return $ G_sign lid' gsig (s+1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgn_theory = G_theory lid' gsig (s+1) noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGUnion,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg'
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian dg1 = insNodeDG (node, node_contents) dg'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gctx1 = gctx' { devGraph = dg1
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang , sigMap = Map.insert (s+1) gbigSigma' sgMap }
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang insE gctxres (NodeSig n gsigma) = do
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gctxl <- gctxres
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang let (mrMapl, ml) = morMapI gctxl
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder dgl = devGraph gctxl
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder incl <- adj $ ginclusion lg gsigma gbigSigma
ebed90d00e82aebf729405fc3aa14504cd4176f7Christian Maeder let incl' = updateMorIndex (ml+1) incl
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang link = DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl',
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGUnion,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID}
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang return (gctxl { devGraph = insEdgeNub (n,node,link) dgl
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = Map.insert (ml+1)
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang (toG_morphism incl') mrMapl})
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gctx2 <- foldl insE (return gctx1) nsigs'
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski return (Union (map (uncurry replaceAnnoted)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (zip (reverse sps') asps))
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang NodeSig node gbigSigma', gctx2)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Extension asps pos -> do
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (sps',nsig1',dg1, _, _, _) <-
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder foldl ana_Extension (return ([], nsig, gctx, lg, opts, pos)) namedSps
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder case nsig1' of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> fail "empty extension"
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode nsig1 -> return (Extension (map (uncurry replaceAnnoted)
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski (zip (reverse sps') asps))
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder pos, nsig1,dg1)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder namedSps = zip (reverse (name: tail (take (length asps)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (iterate inc (extName "E" name)))))
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder Free_spec asp poss ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder (sp', NodeSig n' gsigma'@(G_sign lid' gsig ind), gctx') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let pos = poss
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (mrMap, m) = morMapI gctx'
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let incl' = updateMorIndex (m+1) incl
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lid' gsig ind noSens 0, -- delta is empty
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGFree,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = FreeDef nsig,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFree,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder return (Free_spec (replaceAnnoted sp' asp) poss,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg'
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = Map.insert (m+1) (toG_morphism incl') mrMap})
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder Cofree_spec asp poss ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder (sp', NodeSig n' gsigma'@(G_sign lid' gsig ind), gctx') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let pos = poss
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (mrMap, m) = morMapI gctx'
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let incl' = updateMorIndex (m+1) incl
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lid' gsig ind noSens 0, -- delta is empty
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGCofree,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = CofreeDef nsig,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGCofree,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder return (Cofree_spec (replaceAnnoted sp' asp) poss,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg'
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = Map.insert (m+1) (toG_morphism incl') mrMap})
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder Local_spec asp asp' poss ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski sp1' = item asp'
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder (sp2, nsig'@(NodeSig _ (G_sign lid' sigma' _)), dg') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsig (extName "L" name) opts sp1
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder (sp2', NodeSig n'' (G_sign lid'' sigma'' _), gctx'') <-
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder ana_SPEC lg dg' (JustNode nsig') (inc name) opts sp1'
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let gsigma = getMaybeSig nsig
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg'' = devGraph gctx''
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (sgMap, s) = sigMapI gctx''
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (mrMap, m) = morMapI gctx''
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder G_sign lid sigma _ <- return gsigma
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sigma1 <- coerceSign lid' lid "Analysis of local spec" sigma'
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sigma2 <- coerceSign lid'' lid "Analysis of local spec" sigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let sys = sym_of lid sigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys1 = sym_of lid sigma1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys2 = sym_of lid sigma2
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder mor3 <- if isStructured opts then return (ide lid sigma2)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder else adjustPos pos $ cogenerated_sign lid
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (sys1 `Set.difference` sys) sigma2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let sigma3 = dom lid mor3
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski -- gsigma2 = G_sign lid sigma2
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gsigma3 = G_sign lid sigma3 (s+1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys3 = sym_of lid sigma3
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder when (not( isStructured opts ||
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3))
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder $ plain_error () (
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder "illegal use of locally declared symbols: "
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder ++ showDoc ((sys2 `Set.intersection` sys1) `Set.difference` sys3) "")
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgn_theory = G_theory lid sigma3 (s+1) noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGLocal,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg''
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder link = (n'', node, DGLink {
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang dgl_morphism = gEmbed2 gsigma3 (G_morphism lid 0 mor3 (m+1) 0),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = HidingDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGLocal,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Local_spec (replaceAnnoted sp2 asp)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (replaceAnnoted sp2' asp')
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma3,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx'' { devGraph = insEdgeNub link $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg''
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , sigMap = Map.insert (s+1) gsigma3 sgMap
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang , morMap = Map.insert (m+1) (G_morphism lid 0 mor3 (m+1) 0)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Closed_spec asp pos ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder l = getLogic nsig
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski -- analyse spec with empty local env
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp', NodeSig n' gsigma', gctx') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx (EmptyNode l) (inc name) opts sp1
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let gsigma = getMaybeSig nsig
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder adj = adjustPos pos
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (sgMap, s) = sigMapI gctx'
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (mrMap, m) = morMapI gctx'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang G_sign lid'' gsig'' _ <- return gsigma''
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gsigma2 <- return $ G_sign lid'' gsig'' (s+1)
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl1 <- adj $ ginclusion lg gsigma gsigma2
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl2 <- adj $ ginclusion lg gsigma' gsigma2
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let incl1' = updateMorIndex (m+1) incl1
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl2' = updateMorIndex (m+2) incl2
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgn_theory = G_theory lid'' gsig'' (s+1) noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGClosed,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski link1 = DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl1',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGClosedLenv,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID}
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski link2 = (n',node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl2',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGClosed,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder insLink1 = case nsig of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> id
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang morMap1 = Map.insert (m+1) (toG_morphism incl1') mrMap
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang morMap2 = Map.insert (m+2) (toG_morphism incl2') morMap1
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Closed_spec (replaceAnnoted sp' asp) pos,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang NodeSig node gsigma2,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insLink1 $
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder insEdgeNub link2 $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg'
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , sigMap = Map.insert (s+1) gsigma2 sgMap
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = morMap2})
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski Qualified_spec (Logic_name ln sublog) asp pos -> do
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder l <- lookupLogic "Static analysis: " (tokStr ln) lg
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski -- analyse spec with empty local env
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp', NodeSig n' gsigma', gctx') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx (EmptyNode l) (inc name) opts (item asp)
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski -- construct union with local env
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let gsigma = getMaybeSig nsig
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder adj = adjustPos pos
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (sgMap, s) = sigMapI gctx'
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (mrMap, m) = morMapI gctx'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang G_sign lid'' gsig'' _ <- return gsigma''
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gsigma2 <- return $ G_sign lid'' gsig'' (s+1)
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl1 <- adj $ ginclusion lg gsigma gsigma2
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl2 <- adj $ ginclusion lg gsigma' gsigma2
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let incl1' = updateMorIndex (m+1) incl1
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl2' = updateMorIndex (m+2) incl2
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg'
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski node_contents = DGNode {
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgn_name = name,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgn_theory = G_theory lid'' gsig'' (s+1) noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGLogicQual,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski link1 = DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl1',
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGLogicQualLenv,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID}
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski link2 = (n',node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl2',
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGLogicQual,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder insLink1 = case nsig of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> id
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang morMap1 = Map.insert (m+1) (toG_morphism incl1') mrMap
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang morMap2 = Map.insert (m+2) (toG_morphism incl2') morMap1
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder return (Qualified_spec (Logic_name ln sublog)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted sp' asp) pos,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang NodeSig node gsigma2,
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder gctx' { devGraph = insLink1 $ insEdgeNub link2 $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg'
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , sigMap = Map.insert (s+1) gsigma2 sgMap
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = morMap2})
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Group asp pos -> do
6a57a555c8ef0a79aa5d20e1d721400dbffa564aMaciek Makowski (sp',nsig',dg') <- ana_SPEC lg gctx nsig name opts (item asp)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Group (replaceAnnoted sp' asp) pos,nsig',dg')
2cafc2361fcaccf6b82d81f6a94f59e42af725c7Christian Maeder Spec_inst spname afitargs pos0 -> do
2cafc2361fcaccf6b82d81f6a94f59e42af725c7Christian Maeder let pos = if null afitargs then tokPos spname else pos0
2cafc2361fcaccf6b82d81f6a94f59e42af725c7Christian Maeder adj = adjustPos pos
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder spstr = tokStr spname
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (sgMap, s) = sigMapI gctx
6f7271963dfd7c46ffdf946d659a1cf791899270Jian Chun Wang (mrMap, m) = morMapI gctx
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder case Map.lookup spname $ globalEnv gctx of
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Nothing -> fatal_error
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ("Specification " ++ spstr ++ " not found") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (ViewEntry _) ->
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (spstr ++ " is a view, not a specification") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (ArchEntry _) ->
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder " is an architectural, not a structured specification") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (UnitEntry _) ->
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder " is a unit specification, not a structured specification") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (RefEntry) ->
95656e84acc96386173c1d6fc068aa2fb8820020Till Mossakowski " is a refinement specification, not a structured specification") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (SpecEntry gs@(imps,params,_,body@(NodeSig nB gsigmaB))) ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case (\x y -> (x,x-y)) (length afitargs) (length params) of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- the case without parameters leads to a simpler dg
ebed90d00e82aebf729405fc3aa14504cd4176f7Christian Maeder G_sign lid gsig _ <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder adj $ gsigUnion lg (getMaybeSig nsig) gsigmaB
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder let gsigma' = G_sign lid gsig (s+1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the subcase with empty local env leads to an even simpler dg
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder EmptyNode _ ->
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- if the node shall not be named and the logic does not change,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang if isInternal name && langNameSig gsigma'==langNameSig gsigmaB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- then just return the body
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder then return (sp, body, gctx)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski -- otherwise, we need to create a new one
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl <- adj $ ginclusion lg gsigmaB gsigma'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let incl' = updateMorIndex (m+1) incl
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski node_contents = DGNode {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgn_name = name,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgn_theory = G_theory lid gsig (s+1) noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGSpecInst spname,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen}
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski link = (nB,node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl',
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGSpecInst spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang NodeSig node gsigma',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx { devGraph = insEdgeNub link $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , sigMap = Map.insert (s+1) gsigma' sgMap
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder , morMap = Map.insert (m+1) (toG_morphism incl')
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- the subcase with nonempty local env
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig n sigma) -> do
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl1 <- adj $ ginclusion lg sigma gsigma'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl2 <- adj $ ginclusion lg gsigmaB gsigma'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let incl1' = updateMorIndex (m+1) incl1
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl2' = updateMorIndex (m+2) incl2
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski node_contents = DGNode {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgn_name = name,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgn_theory = G_theory lid gsig (s+1) noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGSpecInst spname,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen}
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski link1 = (n,node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl1',
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGSpecInst spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski link2 = (nB,node,DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl2',
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGSpecInst spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang morMap1 = Map.insert (m+1) (toG_morphism incl1') mrMap
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang morMap2 = Map.insert (m+2) (toG_morphism incl2') morMap1
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang NodeSig node gsigma',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx { devGraph = insEdgeNub link1 $
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder insEdgeNub link2 $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , sigMap = Map.insert (s+1) gsigma' sgMap
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = morMap2})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- now the case with parameters
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let fitargs = map item afitargs
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (fitargs', gctx', args, _) <-
640bbf0d230043651258cb317510aa77621e8c36Christian Maeder adj $ foldl anaFitArg (return ([], gctx, [], extName "A" name))
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski (zip params fitargs)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let actualargs = reverse args
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski (gsigma',morDelta) <- adj $ apply_GS lg gs actualargs
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder gsigmaRes <- adj $ gsigUnion lg (getMaybeSig nsig) gsigma'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang G_sign lidRes gsigRes _ <- return gsigmaRes
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang gsigmaRes' <- return $ G_sign lidRes gsigRes (s+1)
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl1 <- adj $ ginclusion lg (getMaybeSig nsig) gsigmaRes'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl2 <- adj $ ginclusion lg gsigma' gsigmaRes'
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang let incl1' = updateMorIndex (m+1) incl1
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang incl2' = updateMorIndex (m+2) incl2
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang morDelta' <- comp Grothendieck (gEmbed morDelta) incl2'
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian let node = getNewNodeDG dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgn_theory = G_theory lidRes gsigRes (s+1) noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGSpecInst spname,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link1 = DGLink {
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang dgl_morphism = incl1',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGSpecInst spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID}
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder insLink1 = case nsig of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> id
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link2 = (nB,node,DGLink {
f3782b0e45c58a2410166c52a0854f46e0cbac65Till Mossakowski dgl_morphism = morDelta',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGSpecInst spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang parLinks = catMaybes (map (parLink gsigmaRes' node) actualargs)
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian morMap1 = Map.insert (m+1) (toG_morphism incl1') mrMap
a980a2f16eda9aad70f1f53f9df713595f57cb78Jian Chun Wang morMap2 = Map.insert (m+2) (toG_morphism incl2') morMap1
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder return (Spec_inst spname
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (map (uncurry replaceAnnoted)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (zip (reverse fitargs') afitargs))
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder NodeSig node gsigmaRes',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = foldr insEdgeNub
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (insLink1 $ insEdgeNub link2 $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg')
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , sigMap = Map.insert (s+1) gsigmaRes' sgMap
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = morMap2})
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder anaFitArg res (nsig', fa) = do
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (fas', dg1, args, name') <- res
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (fa', dg', arg) <- ana_FIT_ARG lg dg1 spname imps nsig' opts name' fa
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder return (fa' : fas', dg', arg : args , inc name')
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder parLink gsigma' node (_mor_i, NodeSig nA_i sigA_i) = do
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder incl <- maybeResult $ ginclusion lg sigA_i gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let link = DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = incl,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitSpec,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (nA_i,node,link)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- finally the case with conflicting numbers of formal and actual parameters
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (spstr ++ " expects " ++ show (length params) ++ " arguments"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ " but was given " ++ show (length afitargs)) pos
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski Data (Logic lidD) (Logic lidP) asp1 asp2 pos ->
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski do let sp1 = item asp1
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski sp2 = item asp2
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder adj = adjustPos pos
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder Comorphism cid <- adj $ logicInclusion lg (Logic lidD) (Logic lidP)
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski let lidD' = sourceLogic cid
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski lidP' = targetLogic cid
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder (sp1', NodeSig n' (G_sign lid' sigma' _), gctx1) <-
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski ana_SPEC lg gctx (EmptyNode (Logic lidD)) (inc name) opts sp1
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder sigmaD <- adj $ coerceSign lid' lidD' "Analysis of data spec" sigma'
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder (sigmaD',sensD') <- adj $ map_sign cid sigmaD
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder let gsigmaD' = G_sign lidP' sigmaD' 0
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg1 = devGraph gctx1
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski node_contents = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lidP' sigmaD' 0 (toThSens sensD') 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGData,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg1
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski link = (n',node,DGLink {
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgl_morphism = GMorphism cid sigmaD 0 (ide lidP' sigmaD') 0,
5b1394673f35f4d23cfe08175841ab414a39678eMarkus Roggenbach dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGData,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski dg2 = insEdgeNub link $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (node,node_contents) dg1
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder nsig2 = NodeSig node gsigmaD'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (sp2',nsig3,dg3) <-
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder ana_SPEC lg gctx1 { devGraph = dg2 } (JustNode nsig2) name opts sp2
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski return (Data (Logic lidD) (Logic lidP)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted sp1' asp1)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted sp2' asp2)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of renamings
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maederana_ren1 :: LogicGraph -> MaybeNode -> Range -> GMorphism -> G_mapping
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski -> Result GMorphism
410ff490af511ffa09b52e4de631d36a154b9730Christian Maederana_ren1 _ lenv _pos (GMorphism r sigma ind1 mor _)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (G_symb_map (G_symb_map_items_list lid sis)) = do
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski let lid2 = targetLogic r
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder rmap <- stat_symb_map_items lid2 sis1
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor1 <- induced_from_morphism lid2 rmap (cod lid2 mor)
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski EmptyNode _ -> return ()
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder JustNode (NodeSig _ (G_sign lidLenv sigmaLenv _)) -> do
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski -- needs to be changed for logic translations
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder sigmaLenv' <- coerceSign lidLenv lid2
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder "Analysis of renaming: logic translations not yet properly handeled"
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski let sysLenv = sym_of lid2 sigmaLenv'
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski m = symmap_of lid2 mor1
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski isChanged sy = case Map.lookup sy m of
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski Just sy' -> sy /= sy'
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski Nothing -> False
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder _forbiddenSys = Set.filter isChanged sysLenv
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder{- when (not (forbiddenSys == Set.empty)) $ plain_error () (
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder "attempt to rename the following symbols from the local environment:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc forbiddenSys "") pos
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor2 <- comp lid2 mor mor1
8db9f3913d0449639e5ba99c0600852fbe6afe2bChristian Maeder return $ GMorphism r sigma ind1 mor2 0
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maederana_ren1 lg _ _ mor (G_logic_translation (Logic_code tok src tar pos1)) = do
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder let adj = adjustPos pos1
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign srcLid srcSig ind<- return (cod Grothendieck mor)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder c <- adj $ case tok of
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just ctok -> do
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski Comorphism cid <- lookupComorphism (tokStr ctok) lg
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski when (isJust src && getLogicStr (fromJust src) /=
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski language_name (sourceLogic cid))
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (fail (getLogicStr (fromJust src) ++
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder "is not the source logic of "
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski ++ language_name cid))
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski when (isJust tar && getLogicStr (fromJust tar) /=
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski language_name (targetLogic cid))
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (fail (getLogicStr (fromJust tar) ++
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder "is not the target logic of "
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski ++ language_name cid))
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski return (Comorphism cid)
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski Nothing -> case tar of
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski Just (Logic_name l _) -> do
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski tarL <- lookupLogic "with logic: " (tokStr l) lg
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski logicInclusion lg (Logic srcLid) tarL
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski Nothing -> fail "with logic: cannot determine comorphism"
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder mor1 <- adj $ gEmbedComorphism c (G_sign srcLid srcSig ind)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder adj $ comp Grothendieck mor mor1
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder where getLogicStr (Logic_name l _) = tokStr l
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maederana_ren :: LogicGraph -> MaybeNode -> Range -> Result GMorphism -> G_mapping
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski -> Result GMorphism
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowskiana_ren lg lenv pos mor_res ren =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do mor <- mor_res
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski ana_ren1 lg lenv pos mor ren
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowskiana_RENAMING :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> Result GMorphism
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowskiana_RENAMING lg lenv gSigma opts (Renaming ren pos) =
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder if isStructured opts
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski then return (ide Grothendieck gSigma)
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski else foldl (ana_ren lg lenv pos) (return (ide Grothendieck gSigma)) ren
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of restrictions
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maederana_restr1 :: DGraph -> G_sign -> Range -> GMorphism -> G_hiding
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski -> Result GMorphism
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maederana_restr1 _ (G_sign lidLenv sigmaLenv _) pos
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder (GMorphism cid sigma1 _ mor _)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (G_symb_list (G_symb_items_list lid' sis')) = do
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski let lid1 = sourceLogic cid
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski lid2 = targetLogic cid
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction" sis'
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder rsys <- stat_symb_items lid1 sis1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let sys = sym_of lid1 sigma1
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski sys' = Set.filter (\sy -> any (\rsy -> matches lid1 sy rsy) rsys)
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski -- needs to be changed when logic projections are implemented
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder sigmaLenv' <- coerceSign lidLenv lid1
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder "Analysis of restriction: logic projections not yet properly handeled"
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski let sysLenv = sym_of lid1 sigmaLenv'
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski forbiddenSys = sys' `Set.intersection` sysLenv
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski when (not (forbiddenSys == Set.empty))
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder $ plain_error () (
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder "attempt to hide the following symbols from the local environment:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc forbiddenSys "") pos
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor1 <- cogenerated_sign lid1 sys' sigma1
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor1' <- map_morphism cid mor1
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor2 <- comp lid2 mor1' mor
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder return $ GMorphism cid (dom lid1 mor1) 0 mor2 0
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowskiana_restr1 _dg _gSigma _mor _pos
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (G_logic_projection (Logic_code _tok _src _tar pos1)) =
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder fatal_error "no analysis of logic projections yet" pos1
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowskiana_restr :: DGraph -> G_sign -> Range -> Result GMorphism -> G_hiding
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> Result GMorphism
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowskiana_restr dg gSigma pos mor_res restr =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do mor <- mor_res
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski ana_restr1 dg gSigma pos mor restr
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_RESTRICTION :: DGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> Result (GMorphism, Maybe GMorphism)
6a57a555c8ef0a79aa5d20e1d721400dbffa564aMaciek Makowskiana_RESTRICTION dg gSigma gSigma' opts restr =
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder ana_RESTRICTION' dg gSigma gSigma' (isStructured opts) restr
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_RESTRICTION' :: DGraph -> G_sign -> G_sign -> Bool -> RESTRICTION
6a57a555c8ef0a79aa5d20e1d721400dbffa564aMaciek Makowski -> Result (GMorphism, Maybe GMorphism)
6a57a555c8ef0a79aa5d20e1d721400dbffa564aMaciek Makowskiana_RESTRICTION' _ _ gSigma True _ =
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski return (ide Grothendieck gSigma,Nothing)
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowskiana_RESTRICTION' dg gSigma gSigma' False (Hidden restr pos) =
ff3bc28a09cff76d4d6cbe8914ab53d1e032d009Till Mossakowski do mor <- foldl (ana_restr dg gSigma pos)
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski (return (ide Grothendieck gSigma'))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (mor,Nothing)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski -- ??? Need to check that local env is not affected !
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wangana_RESTRICTION' _ (G_sign lid sigma _) (G_sign lid' sigma' si')
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder False (Revealed (G_symb_map_items_list lid1 sis) pos) =
79ee6b8eb396ed31807784a4bb1c9cc2ce094835Till Mossakowski do let sys = sym_of lid sigma -- local env
79ee6b8eb396ed31807784a4bb1c9cc2ce094835Till Mossakowski sys' = sym_of lid' sigma' -- "big" signature
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder adj = adjustPos pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder sis' <- adj $ coerceSymbMapItemsList lid1 lid'
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder "Analysis of restriction" sis
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder rmap <- adj $ stat_symb_map_items lid' sis'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder [sy | sy <- Set.toList sys', rsy <-
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Map.keys rmap, matches lid' sy rsy]
79ee6b8eb396ed31807784a4bb1c9cc2ce094835Till Mossakowski -- domain of rmap intersected with sys'
79ee6b8eb396ed31807784a4bb1c9cc2ce094835Till Mossakowski -- domain of rmap should be checked to match symbols from sys' ???
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sys1 <- adj $ coerceSymbolSet lid lid' "Analysis of restriction" sys
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? this is too simple in case that local env is translated
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- to a different logic
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder mor1 <- adj $ generated_sign lid' (sys1 `Set.union` sys'') sigma'
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder mor2 <- adj $ induced_from_morphism lid' rmap (dom lid' mor1)
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang return (gEmbed (G_morphism lid' si' mor1 0 0),
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang Just (gEmbed (G_morphism lid' 0 mor2 0 0)))
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maederana_FIT_ARG :: LogicGraph -> GlobalContext -> SPEC_NAME -> MaybeNode
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder -> NodeSig -> HetcatsOpts -> NODE_NAME -> FIT_ARG
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder -> Result (FIT_ARG, GlobalContext, (G_morphism,NodeSig))
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_FIT_ARG lg gctx spname nsigI
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder (NodeSig nP (G_sign lidP sigmaP _)) opts name
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder (Fit_spec asp gsis pos) = do
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder let adj = adjustPos pos
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder (sp', nsigA@(NodeSig nA (G_sign lidA sigmaA _)), dg') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsigI name opts (item asp)
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder G_symb_map_items_list lid sis <- homogenizeGM (Logic lidP) gsis
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sigmaA' <- adj $ coerceSign lidA lidP "Analysis of fitting argument" sigmaA
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder mor <- adj $ if isStructured opts then return (ide lidP sigmaP)
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder rmap <- stat_symb_map_items lid sis
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder rmap' <- if null sis then return Map.empty
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder else coerceRawSymbolMap lid lidP
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder "Analysis of fitting argument" rmap
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder induced_from_to_morphism lidP rmap' sigmaP sigmaA'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let symI = sym_of lidP sigmaI'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder symmap_mor = symmap_of lidP mor
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- are symbols of the imports left untouched?
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder if Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder then return ()
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder else plain_error () "Fitting morphism must not affect import" pos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -} -- ??? does not work
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? also output some symbol that is affected
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let link = (nP,nA,DGLink {
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang dgl_morphism = gEmbed (G_morphism lidP 0 mor 0 0),
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGSpecInst spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder return (Fit_spec (replaceAnnoted sp' asp) gsis pos,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx { devGraph = insEdgeNub link $ devGraph dg' },
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang (G_morphism lidP 0 mor 0 0,nsigA)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederana_FIT_ARG lg gctx spname nsigI (NodeSig nP gsigmaP)
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder opts name fv@(Fit_view vn afitargs pos) = do
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder let adj = adjustPos pos
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder dg = devGraph gctx
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder spstr = tokStr spname
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder case Map.lookup vn $ globalEnv gctx of
2b346670d3e146788fa056a4b0fafa357d8bf31bTill Mossakowski Nothing -> fatal_error
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ("View " ++ tokStr vn ++ " not found") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (SpecEntry _) ->
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (spstr ++ " is a specification, not a view") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (ArchEntry _) ->
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder " is an architectural specification, not a view ") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (UnitEntry _) ->
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder " is a unit specification, not a view") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (RefEntry) ->
95656e84acc96386173c1d6fc068aa2fb8820020Till Mossakowski " is a refinement specification, not a view") pos
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just (ViewEntry (src,mor,gs@(imps,params,_,target))) -> do
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let nSrc = getNode src
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder nTar = getNode target
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder gsigmaS = getSig src
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski gsigmaT = getSig target
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder gsigmaI = getMaybeSig nsigI
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder GMorphism cid _ _ morHom ind<- return mor
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let lid = targetLogic cid
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski when (not (language_name (sourceLogic cid) == language_name lid))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "heterogeneous fitting views not yet implemented"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case (\x y -> (x,x-y)) (length afitargs) (length params) of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the case without parameters leads to a simpler dg
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (0,0) -> case nsigI of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the subcase with empty import leads to a simpler dg
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let link = (nP,nSrc,DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = ide Grothendieck gsigmaP,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder dgl_origin = DGFitView spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder return (fv, gctx { devGraph = insEdgeNub link dg },
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang (G_morphism lid 0 morHom ind 0, target))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the subcase with nonempty import
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig nI _) -> do
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder gsigmaIS <- adj $ gsigUnion lg gsigmaI gsigmaS
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski when (not (isSubGsign lg gsigmaP gsigmaIS))
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (plain_error ()
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ("Parameter does not match source of fittig view. "
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ "Parameter signature:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc gsigmaP
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder "\nSource signature of fitting view (united with import):\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc gsigmaIS "") pos)
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lidI sigI1 _<- return gsigmaI
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder sigI <- adj $ coerceSign lidI lid
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder "Analysis of instantiation with import" sigI1
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder mor_I <- adj $ morphism_union lid morHom $ ide lid sigI
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski gsigmaA <- adj $ gsigUnion lg gsigmaI gsigmaT
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lidA gsigA indA <- return gsigmaA
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lidP gsigP indP <- return gsigmaP
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl1 <- adj $ ginclusion lg gsigmaI gsigmaA
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl2 <- adj $ ginclusion lg gsigmaT gsigmaA
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl3 <- adj $ ginclusion lg gsigmaI gsigmaP
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl4 <- adj $ ginclusion lg gsigmaS gsigmaP
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian let [nA,n'] = newNodesDG 2 dg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski node_contentsA = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lidA gsigA indA noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGFitViewA spname,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski node_contents' = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = inc name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lidP gsigP indP noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGFitView spname,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski link = (nP,n',DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = ide Grothendieck gsigmaP,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitView spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link1 = (nSrc,n',DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl4,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitView spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski link2 = (nTar,nA,DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = incl2,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitViewA spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski link3 = (nI,n',DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = incl3,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitViewImp spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link4 = (nI,nA,DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl1,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitViewAImp spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder return (fv, gctx { devGraph =
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski insEdgeNub link $
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski insEdgeNub link1 $
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski insEdgeNub link2 $
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski insEdgeNub link3 $
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski insEdgeNub link4 $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (nA,node_contentsA) $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (n',node_contents') dg },
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang (G_morphism lid 0 mor_I 0 0, NodeSig nA gsigmaA))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- now the case with parameters
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let fitargs = map item afitargs
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (fitargs', gctx', args,_) <-
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder foldl anaFitArg (return ([], gctx, [], extName "A" name))
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski (zip params fitargs)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let actualargs = reverse args
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski (gsigmaA,mor_f) <- adj $ apply_GS lg gs actualargs
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski let gmor_f = gEmbed mor_f
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski gsigmaRes <- adj $ gsigUnion lg gsigmaI gsigmaA
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lidRes gsigRes indRes<- return gsigmaRes
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder mor1 <- adj $ comp Grothendieck mor gmor_f
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl1 <- adj $ ginclusion lg gsigmaA gsigmaRes
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder mor' <- adj $ comp Grothendieck gmor_f incl1
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder GMorphism cid1 _ _ mor1Hom _<- return mor1
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski let lid1 = targetLogic cid1
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski when (not (language_name (sourceLogic cid1) == language_name lid1))
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski ("heterogeneous fitting views not yet implemented")
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lidI sigI1 _<- return gsigmaI
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder sigI <- adj $ coerceSign lidI lid1
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder "Analysis of instantiation with parameters" sigI1
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski theta <- adj $ morphism_union lid1 mor1Hom (ide lid1 sigI)
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl2 <- adj $ ginclusion lg gsigmaI gsigmaRes
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl3 <- adj $ ginclusion lg gsigmaI gsigmaP
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl4 <- adj $ ginclusion lg gsigmaS gsigmaP
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lidP gsigP indP <- return gsigmaP
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder let dg' = devGraph gctx'
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian [nA,n'] = newNodesDG 2 dg'
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski node_contentsA = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lidRes gsigRes indRes noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGFitViewA spname,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen}
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski node_contents' = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = extName "V" name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lidP gsigP indP noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGFitView spname,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen}
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link = (nP,n',DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = ide Grothendieck gsigmaP,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitView spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link1 = (nSrc,n',DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl4,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitView spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link2 = (nTar,nA,DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = mor',
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitViewA spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder fitLinks = [link,link1,link2] ++ case nsigI of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> []
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig nI _) -> let
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link3 = (nI,n',DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl3,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitViewImp spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link4 = (nI,nA,DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl2,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitViewAImp spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski in [link3,link4]
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski parLinks = catMaybes (map (parLink gsigmaRes nA) actualargs)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder return (Fit_view vn
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (map (uncurry replaceAnnoted)
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (zip (reverse fitargs') afitargs))
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = foldr insEdgeNub
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian (insNodeDG (nA,node_contentsA) $
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian insNodeDG (n',node_contents') dg')
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (fitLinks ++ parLinks) },
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang (G_morphism lid1 0 theta 0 0, NodeSig nA gsigmaRes))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski anaFitArg res (nsig',fa) = do
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian Maeder (fas',dg1,args,name') <- res
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (fa',dg',arg) <- ana_FIT_ARG lg dg1
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian Maeder spname imps nsig' opts name' fa
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian Maeder return (fa':fas',dg',arg:args,inc name')
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder parLink gsigmaRes node (_mor_i,nsigA_i) = do
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let nA_i = getNode nsigA_i
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl <- maybeResult $ ginclusion lg (getSig nsigA_i) gsigmaRes
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let link = DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = incl,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFitView spname,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (nA_i,node,link)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder-- finally the case with conflicting numbers of formal and actual parameters
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (spstr ++ " expects " ++ show (length params) ++ " arguments"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ " but was given " ++ show (length afitargs)) pos
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- Extension of signature morphisms (for instantitations)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- first some auxiliary functions
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaedermapID :: Map.Map Id (Set.Set Id) -> Id -> Result Id
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaedermapID idmap i@(Id toks comps pos1) =
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder case Map.lookup i idmap of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> do
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder compsnew <- sequence $ map (mapID idmap) comps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (Id toks compsnew pos1)
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder Just ids -> if Set.null ids then return i else
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder if Set.null $ Set.deleteMin ids then return $ Set.findMin ids else
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder plain_error i
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ("Identifier component " ++ showId i
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder " can be mapped in various ways:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc ids "") $ getRange i
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder -> Result (EndoMap Id) -> Result (EndoMap Id)
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaederextID1 idmap i@(Id toks comps pos1) m = do
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder compsnew <- sequence $ map (mapID idmap) comps
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder if comps==compsnew
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski then return m1
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder else return (Map.insert i (Id toks compsnew pos1) m1)
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederextID :: Set.Set Id -> Map.Map Id (Set.Set Id) -> Result (EndoMap Id)
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaederextID ids idmap = Set.fold (extID1 idmap) (return Map.empty) ids
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaederextendMorphism :: G_sign -- ^ formal parameter
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -> G_sign -- ^ body
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -> G_sign -- ^ actual parameter
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -> G_morphism -- ^ fitting morphism
cf29cb0194d75de2182bfc73fa7da68e90a4a19eMaciek Makowski -> Result(G_sign,G_morphism)
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian MaederextendMorphism (G_sign lid sigmaP _) (G_sign lidB sigmaB1 _)
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang (G_sign lidA sigmaA1 _) (G_morphism lidM _ fittingMor1 _ _) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- for now, only homogeneous instantiations....
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sigmaB <- coerceSign lidB lid "Extension of symbol map" sigmaB1
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sigmaA <- coerceSign lidA lid "Extension of symbol map" sigmaA1
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder fittingMor <- coerceMorphism lidM lid "Extension of symbol map" fittingMor1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let symsP = sym_of lid sigmaP
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski symsB = sym_of lid sigmaB
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder idsB = Set.map (sym_name lid) symsB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski h = symmap_of lid fittingMor
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski symbMapToRawSymbMap =
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Map.foldWithKey (\sy1 sy2 -> Map.insert (symbol_to_raw lid sy1)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (symbol_to_raw lid sy2))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski rh = symbMapToRawSymbMap h
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (\sy1 sy2 -> Rel.setInsert (sym_name lid sy1) (sym_name lid sy2))
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder idhExt <- extID idsB idh
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder let rIdExt = Map.foldWithKey (\id1 id2 -> Map.insert
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (id_to_raw lid id1) (id_to_raw lid id2))
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder (foldr (\i -> Map.delete i) idhExt $ Map.keys idh)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski r = rh `Map.union` rIdExt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- do we need combining function catching the clashes???
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mor <- induced_from_morphism lid r sigmaB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let hmor = symmap_of lid mor
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sigmaAD = cod lid mor
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sigma <- final_union lid sigmaA sigmaAD
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let illShared = (sym_of lid sigmaA `Set.intersection` sym_of lid sigmaAD )
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder when (not (Set.null illShared))
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (plain_error () ("Symbols shared between actual parameter and body"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ "\nmust be in formal parameter:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc illShared "") nullRange)
ed373f8356ebc42bd83aaa5ff9b908e07721f2beChristian Maeder let myKernel m = Set.fromDistinctAscList $ comb1 $ Map.toList m
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian Maeder comb1 [] = []
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder comb1 (p : qs) =
f9690de9acb57e279b8ad5792d71b48ffbb807e7Christian Maeder comb2 p qs [] ++ comb1 qs
f9690de9acb57e279b8ad5792d71b48ffbb807e7Christian Maeder comb2 _ [] rs = rs
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder comb2 p@(a, b) ((c, d) : qs) rs =
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder comb2 p qs $ if b == d then (a, c) : rs else rs
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian Maeder newIdentifications = myKernel hmor Set.\\ myKernel h
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder when (not (Set.null newIdentifications))
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (plain_error () (
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder "Fitting morphism leads to forbidden identifications:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc newIdentifications "") nullRange)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski incl <- inclusion lid sigmaAD sigma
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder mor1 <- comp lid mor incl
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang return (G_sign lid sigma 0, G_morphism lid 0 mor1 0 0)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederapply_GS :: LogicGraph -> ExtGenSig -> [(G_morphism,NodeSig)]
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski -> Result(G_sign,G_morphism)
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowskiapply_GS lg (nsigI,_params,gsigmaP,nsigB) args = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let mor_i = map fst args
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaA_i = map (getSig . snd) args
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaB = getSig nsigB
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder gsigmaI = getMaybeSig nsigI
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lidI sigmaI _<- return gsigmaI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let idI = ide lidI sigmaI
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski gsigmaA <- gsigManyUnion lg gsigmaA_i
d4755076e0e91104c0a08fc71d8846db8c81be3eJian Chun Wang mor_f <- homogeneousMorManyUnion (G_morphism lidI 0 idI 0 0:mor_i)
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder extendMorphism gsigmaP gsigmaB gsigmaA mor_f
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- | analyze a GENERICITY
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- Parameters: global context, current logic, just-structure-flag, GENERICITY
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_GENERICITY :: LogicGraph -> GlobalContext -> AnyLogic -> HetcatsOpts
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski -> NODE_NAME -> GENERICITY
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder -> Result (GENERICITY, GenericitySig, GlobalContext)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- zero parameters,
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederana_GENERICITY _ gctx l _ _
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski gen@(Genericity (Params []) (Imported imps) pos) = do
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder when (not (null imps))
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (plain_error () "Parameterless specifications must not have imports"
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder return (gen,(EmptyNode l, [], EmptyNode l), gctx)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- one parameter ...
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederana_GENERICITY lg gctx l opts name
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Genericity (Params [asp]) imps pos) = do
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski (imps',nsigI,dg') <- ana_IMPORTS lg gctx l opts (extName "I" name) imps
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp',nsigP,dg'') <- ana_SPEC lg dg' nsigI
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder name opts (item asp)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Genericity (Params [replaceAnnoted sp' asp]) imps' pos,
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (nsigI, [nsigP], JustNode nsigP), dg'')
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- ... and more parameters
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederana_GENERICITY lg gctx l opts name
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Genericity params imps pos) = do
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder let adj = adjustPos pos
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski (imps',nsigI,dg') <- ana_IMPORTS lg gctx l opts (extName "I" name) imps
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (params',nsigPs,gctx'') <-
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder ana_PARAMS lg dg' l nsigI opts (inc name) params
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski gsigmaP <- adj $ gsigManyUnion lg (map getSig nsigPs)
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder G_sign lidP gsigP indP <- return gsigmaP
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = name,
e24d81c69aecd41abb2f4969519c9e7126b1d687Christian Maeder dgn_theory = G_theory lidP gsigP indP noSens 0,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_nf = Nothing,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_sigma = Nothing,
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken dgn_origin = DGFormalParams,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons = None,
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder dgn_cons_status = LeftOpen }
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg'' = devGraph gctx''
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian node = getNewNodeDG dg''
edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian dg''' = insNodeDG (node,node_contents) dg''
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder inslink dgres (NodeSig n sigma) = do
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder incl <- adj $ ginclusion lg sigma gsigmaP
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski return (insEdgeNub (n,node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_origin = DGFormalParams,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID}) dg)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dg4 <- foldl inslink (return dg''') nsigPs
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Genericity params' imps' pos,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (nsigI, nsigPs, JustNode $ NodeSig node gsigmaP),
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx { devGraph = dg4 })
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_PARAMS :: LogicGraph -> GlobalContext -> AnyLogic -> MaybeNode
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder -> HetcatsOpts -> NODE_NAME -> PARAMS
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder -> Result (PARAMS, [NodeSig], GlobalContext)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederana_PARAMS lg gctx _ nsigI opts name (Params asps) = do
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sps',pars,dg',_) <- foldl ana (return ([], [], gctx, name))
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder $ map item asps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Params (map (uncurry replaceAnnoted)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (zip (reverse sps') asps)),
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder reverse pars, dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ana res sp = do
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski (sps',pars,dg1,n) <- res
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp',par,dg') <- ana_SPEC lg dg1 nsigI n opts sp
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski return (sp':sps',par:pars,dg',inc n)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_IMPORTS :: LogicGraph -> GlobalContext -> AnyLogic -> HetcatsOpts
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski -> NODE_NAME -> IMPORTED
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder -> Result (IMPORTED, MaybeNode, GlobalContext)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederana_IMPORTS lg gctx l opts name imps@(Imported asps) =
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder [] -> return (imps, EmptyNode l, gctx)
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let sp = Union asps nullRange
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (Union asps' _, nsig', dg') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx (EmptyNode l) name opts sp
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder return (Imported asps', JustNode nsig', dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? emptyExplicit stuff needs to be added here
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- | analyze a VIEW_TYPE
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- The first three arguments give the global context
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- The AnyLogic is the current logic
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- The NodeSig is the signature of the parameter of the view
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- flag, whether just the structure shall be analysed
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_VIEW_TYPE :: LogicGraph -> GlobalContext -> AnyLogic
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder -> MaybeNode -> HetcatsOpts -> NODE_NAME -> VIEW_TYPE
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder -> Result (VIEW_TYPE, (NodeSig, NodeSig), GlobalContext)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maederana_VIEW_TYPE lg gctx l parSig opts name
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (View_type aspSrc aspTar pos) = do
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (spSrc',srcNsig,dg') <-
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski ana_SPEC lg gctx (EmptyNode l) (extName "S" name) opts (item aspSrc)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (spTar',tarNsig,dg'') <-
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder ana_SPEC lg dg' parSig
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (extName "T" name) opts (item aspTar)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder return (View_type (replaceAnnoted spSrc' aspSrc)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted spTar' aspTar)
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (srcNsig, tarNsig), dg'')
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederhomogenizeGM :: AnyLogic -> [Syntax.AS_Structured.G_mapping]
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -> Result G_symb_map_items_list
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederhomogenizeGM (Logic lid) gsis =
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder foldl homogenize1 (return (G_symb_map_items_list lid [])) gsis
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder homogenize1 res
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder (Syntax.AS_Structured.G_symb_map (G_symb_map_items_list lid1 sis1)) = do
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder (G_symb_map_items_list lid2 sis) <- res
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sis1' <- coerceSymbMapItemsList lid1 lid2 "" sis1
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder return $ G_symb_map_items_list lid2 $ sis ++ sis1'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder homogenize1 res _ = res
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder-- | check if structured analysis should be performed
7297175957c5ad3c0498032190b1dee9ec5fb873Christian MaederisStructured :: HetcatsOpts -> Bool
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederisStructured a = case analysis a of
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Structured -> True
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- | Auxiliary function for not yet implemented features
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_err :: String -> a
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_err f = error $ "*** Analysis of " ++ f ++ " is not yet implemented!"
410ff490af511ffa09b52e4de631d36a154b9730Christian Maederana_Extension :: Result ([SPEC],MaybeNode, GlobalContext,
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder LogicGraph, HetcatsOpts, Range)
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -> (NODE_NAME, Annoted SPEC) ->
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder Result ([SPEC], MaybeNode, GlobalContext,
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder LogicGraph, HetcatsOpts, Range)
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maederana_Extension res (name',asp') = do
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (sps', nsig', dg',lg,opts, pos) <- res
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (sp1', nsig1@(NodeSig n1 sig1), gctx1) <-
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder ana_SPEC lg dg' nsig' name' opts (item asp')
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder let anno = find isSemanticAnno $ l_annos asp'
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder dg1 = devGraph gctx1
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder mrMapl = morMap gctx1
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder ml = if Map.null mrMapl then 0 else fst $ Map.findMax mrMapl
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -- is the extension going between real nodes?
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder gctx2 <- case (anno, nsig') of
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (Just anno0@(Semantic_anno anno1 _), JustNode (NodeSig n' sig')) -> do
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -- any other semantic annotation? that's an error
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder when (any (\an -> isSemanticAnno an && an/=anno0) $ l_annos asp')
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (plain_error () "Conflicting semantic annotations"
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -- %implied should not occur here
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder when (anno1==SA_implied)
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder (plain_error ()
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder "Annotation %implied should come after a BASIC-ITEM"
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder if anno1==SA_implies then do
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder when (not (isHomSubGsign sig1 sig')) (plain_error ()
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder "Signature must not be extended in presence of %implies"
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -- insert a theorem link according to p. 319 of the CASL Reference Manual
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder return gctx1 { devGraph = insEdgeNub (n1, n', DGLink
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder { dgl_morphism = ide Grothendieck sig1,
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder dgl_origin = DGExtension,
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian dgl_id = defaultEdgeID}) dg1 }
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder let anno2 = case anno1 of
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder SA_cons -> Cons
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder SA_def -> Def
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder SA_mono -> Mono
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder _ -> error "Static.AnalysisStructured: this cannot happen"
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -- insert a theorem link according to p. 319 of the CASL Reference Manual
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -- the theorem link is trivally proved by the parallel definition link,
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -- but for clarity, we leave it open here
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder -- the interesting open proof obligation is anno2, of course
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder incl <- ginclusion lg sig' sig1
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder let incl' = updateMorIndex (ml+1) incl
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder return gctx1 { devGraph = insEdgeNub (n', n1, DGLink
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder { dgl_morphism = incl'
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , dgl_type = GlobalThm LeftOpen anno2 LeftOpen
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian , dgl_origin = DGExtension
0066f18f8ce6221eb08845adf63cc034f90d62e0Cui Jian , dgl_id = defaultEdgeID }) dg1
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder , morMap = Map.insert (ml+1) (toG_morphism incl')
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder _ -> return gctx1
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder return (sp1' : sps', JustNode nsig1, gctx2, lg, opts, pos)