AnalysisStructured.hs revision c1f654e5454af20eca35aa69f13c5144f405aed9
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederModule : $Header$
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)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederAnalysis of structured specifications
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski Follows the verfication semantic rules in Chap. IV:4.7
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski of the CASL Reference Manual.
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski analysis of basic specs: use union of sigs
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder analysis of instantiations:
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder if necessary, translate body along inclusion comorphism
82d681fe6950e2a35f28fdefb874d060632faccaTill Mossakowski Improve efficiency by storing local signature fragments only
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Name views in devgraphs?
70e2af8d4bf21bcdfb53e9a0414e27173b577a1eTill Mossakowski spec <name> not found: line number!
2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowski Issue warning for unions of non-disjoint signatures
2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowski (and offer tool for renaming?)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Check that translations and reductions do not effect local env
82d681fe6950e2a35f28fdefb874d060632faccaTill Mossakowski (Implement new semantics for revealing here)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Should we use institution independent analysis over the Grothendieck logic?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder abstract syntax + devgraph would have to be changed to homogeneous case
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder logic translations are symbol maps in the Grothendieck logic
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Problem with this approach: symbol functor goes into rel,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder and induced_from_morphism gets difficult to implement
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Unions need inclusion morphisms. Should these play a special role?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder At least we need a function delivering the inclusion morphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder between two (sub)signatures.
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder In most logics, inclusions could be represented specially, such
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder that composition for them becomes fast.
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Should we even identify an inclusion subcategory?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Then inclusions are represented by pair of signatures
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (Non-inclusions could be specially displayed in the DG)
c529224e0ec191fbaa87261f05c34f89c17b3f3aTill Mossakowski No optimization of heterogeneous unions!
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (or use heterogeneous compInclusion in Proofs/Proof.hs)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (or perhaps abandon optimized unions at all and
02b3d9f81150bedd0916c2ffc637a14668e34097Till Mossakowski replace compHomInclusion with comp Grothendieck? is this more efficient?)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Treatment of translations and reductions along logic translations
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (see WADT 02 paper).
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Open question:
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder may local env be translated, and even reduced, along logic translations?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if yes: how is local env linked to signature of resulting spec?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (important e.g. for checking that local env is not being renamed?)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder does signature+comorphism suffice, such that c(local env)\subseteq sig?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if no: this means that only closed specs may be translated
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Revealings without translations: just one arrow
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Pushouts: only admissible within one logic?
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski Instantiations with formal parameter: add no new internal nodes
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski call extend_morphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Optimizations:
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski Union nodes can be extended by a basic spec directly (no new node needed)
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski no new nodes for trivial translations
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Also: free, cofree nodes
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Basic specs: if local env node is otherwise unused, overwrite it with
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski local sig+axioms
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Ensure that just_struct option leads to disabling of various dg operations
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (show sig, show mor, proving)
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski local: better error message for the following
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowskispec GenCardinality [sort Subject,Object;
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski pred predicate : Subject * Object] =
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski Set [sort Object fit sort Elem |-> Object]
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder reveal Set[Object], #__, __eps__,
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder Nat,0,1,2,3,4,5,6,7,8,9,__@@__,__>=__,__<=__
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski op toSet : Subject -> Set [Object]
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder forall x : Subject; y : Object
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder . predicate (x,y) <=> y eps toSet(x)
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski pred minCardinality(s: Subject;n: Nat) <=>
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder # toSet(s) >= n;
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder maxCardinality(s: Subject;n: Nat) <=>
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder # toSet(s) <= n;
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder cardinality(s: Subject;n: Nat) <=>
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder # toSet(s) = n
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski%%} hide Pos,toSet,Set[Object],#__,__eps__,__<=__,__>=__
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)
9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettichimport Common.AS_Annotation hiding (isAxiom,isDef)
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowskiimport qualified Common.Lib.Set as Set
c616e681da8c052b62e14247fea522da099ac0e4Christian Maederimport qualified Common.Lib.Map as Map
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederimport qualified Common.Lib.Rel as Rel(image, setInsert)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian 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
de6c4edf5694b8bad67ecec910c492eaf1129dc8Christian Maeder else (p, v, l', (l, w) : s) & g'
de6c4edf5694b8bad67ecec910c492eaf1129dc8Christian Maeder where (Just (p, _, l', s), g') = match 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 =
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder let dg = devGraph gctx in
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Basic_spec (G_basic_spec lid bspec) ->
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder do G_sign lid' sigma' <- return (getMaybeSig nsig)
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder sigma <- coerceSign lid' lid "Analysis of basic spec" sigma'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (bspec', _sigma_local, sigma_complete, ax) <-
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder if isStructured opts
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski then return (bspec,empty_signature lid, empty_signature lid,[])
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder else do b <- maybeToMonad
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski ("no basic analysis for logic "
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder ++language_name lid)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski (basic_analysis lid)
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder b (bspec,sigma, globalAnnos gctx)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder incl <- ginclusion lg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (G_sign lid sigma) (G_sign lid sigma_complete)
5d812ccb300d5ca8b6e9474d2a644b964faf2d28Jorina Freya Gerken let node_contents =
30f64088b9425c9b928bd4074e8f37ea35cb0278Till Mossakowski dgn_name = name,
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder dgn_theory = G_theory lid sigma_complete $ toThSens ax,
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 }
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dg' = insNode (node,node_contents) dg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGExtension }
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'),
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node $ G_sign lid sigma_complete,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx { devGraph = dg'' })
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
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski mor <- ana_RENAMING lg 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
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lid' gsig <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid' gsig noSens,
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'
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = mor,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGTranslation })
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Translation (replaceAnnoted sp1' asp) ren,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg' })
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'
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
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let gsigma'' = dom Grothendieck hmor
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lid' gsig <- return gsigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder dgn_theory = G_theory lid' gsig noSens,
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 }
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = hmor,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = HidingDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGHiding })
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Reduction (replaceAnnoted sp1' asp) restr,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma'',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg' })
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
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lid1 gsig <- return gsigma1
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lid'' gsig'' <- return gsigma''
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the case with identity translation leads to a simpler dg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if tmor' == ide Grothendieck (dom Grothendieck tmor')
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder let node1 = getNewNode dg'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski node_contents1 = DGNode {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid1 gsig noSens,
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 {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = hmor,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = HidingDef,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_origin = DGRevealing })
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (Reduction (replaceAnnoted sp1' asp) restr,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node1 gsigma1,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link1 $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node1,node_contents1) dg' } )
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder let [node1,node''] = newNodes 2 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents1 = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = extName "T" name,
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder dgn_theory = G_theory lid1 gsig noSens,
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 }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link1 = (n',node1,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = hmor,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = HidingDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGRevealing })
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents'' = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder dgn_theory = G_theory lid'' gsig'' noSens,
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,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGRevealTranslation })
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Reduction (replaceAnnoted sp1' asp) restr,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node'' gsigma'',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link'' $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node'',node_contents'') $
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski insEdgeNub link1 $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node1,node_contents1) dg' })
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
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski gbigSigma <- adj $ gsigManyUnion lg (map getSig nsigs')
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lid' gsig <- return gbigSigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder dgn_theory = G_theory lid' gsig noSens,
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 }
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg'
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder insE dgres (NodeSig n gsigma) = do
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder incl <- adj $ ginclusion lg gsigma gbigSigma
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let link = DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_origin = DGUnion }
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski return (insEdgeNub (n,node,link) dg1)
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder dg'' <- foldl insE (return (insNode (node,node_contents) dg')) nsigs'
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski return (Union (map (uncurry replaceAnnoted)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (zip (reverse sps') asps))
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gbigSigma,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = dg'' })
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Extension asps pos -> do
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sps',nsig1',dg1) <- foldl ana (return ([], nsig, gctx)) 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)))))
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder ana res (name',asp') = do
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (sps', nsig', dg') <- res
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp1', nsig1@(NodeSig n1 sig1), gctx1) <-
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder ana_SPEC lg dg' nsig' name' opts (item asp')
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski -- insert theorem link for semantic annotations
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski -- take the first semantic annotation
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski let anno = find isSemanticAnno $ l_annos asp'
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg1 = devGraph gctx1
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski -- is the extension going between real nodes?
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder dg2 <- case (anno, nsig') of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (Just anno0@(Semantic_anno anno1 _), JustNode (NodeSig n' sig')) -> do
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski -- any other semantic annotation? that's an error
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski when (any (\an -> isSemanticAnno an && an/=anno0) $ l_annos asp')
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (pplain_error () (text "Conflicting semantic annotations")
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski -- %implied should not occur here
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder when (anno1==SA_implied)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (pplain_error () (text
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder "Annotation %implied should come after a BASIC-ITEM")
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski if anno1==SA_implies then do
4cb77926a2d85ce3bb32ac0938f0100c8c528dc2Till Mossakowski when (not (isHomSubGsign sig1 sig')) (pplain_error ()
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (text "Signature must not be extended in presence of %implies")
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- insert a theorem link according to p. 319 of the CASL Reference Manual
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski return $ insEdgeNub (n1,n',DGLink {
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski dgl_morphism = ide Grothendieck sig1,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski dgl_origin = DGExtension }) dg1
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski let anno2 = case anno1 of
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski SA_cons -> Cons
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski SA_def -> Def
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski SA_mono -> Mono
f3782b0e45c58a2410166c52a0854f46e0cbac65Till Mossakowski _ -> error "Static.AnalysisStructured: this cannot happen"
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- insert a theorem link according to p. 319 of the CASL Reference Manual
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- the theorem link is trivally proved by the parallel definition link,
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski -- but for clarity, we leave it open here
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski -- the interesting open proof obligation is anno2, of course
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski incl <- ginclusion lg sig' sig1
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski return $ insEdgeNub (n',n1,DGLink {
c1168130136b44bcfa8946dbda76be553aa7344bTill Mossakowski dgl_morphism = incl,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgl_type = GlobalThm LeftOpen anno2 LeftOpen,
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder dgl_origin = DGExtension }) dg1
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski _ -> return dg1
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder return (sp1':sps', JustNode nsig1, gctx1 { devGraph = dg2 })
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder Free_spec asp poss ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp', NodeSig n' gsigma'@(G_sign lid' gsig), gctx') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let pos = poss
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid' gsig noSens, -- 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 }
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = FreeDef nsig,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGFree })
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder return (Free_spec (replaceAnnoted sp' asp) poss,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg' })
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder Cofree_spec asp poss ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (sp', NodeSig n' gsigma'@(G_sign lid' gsig), gctx') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder let pos = poss
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg' = devGraph gctx'
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid' gsig noSens, -- 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 }
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = CofreeDef nsig,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGCofree })
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder return (Cofree_spec (replaceAnnoted sp' asp) poss,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insEdgeNub link $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg' })
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder Local_spec asp asp' poss ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski sp1' = item asp'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (sp2, nsig'@(NodeSig _ (G_sign lid' sigma')), dg') <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder ana_SPEC lg gctx nsig (extName "L" name) opts sp1
c3a264bbb3692f9b44024c6024382e3ed6590688Christian 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''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian 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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma3 = G_sign lid sigma3
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys3 = sym_of lid sigma3
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder when (not( isStructured opts ||
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3))
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder $ pplain_error () (text
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder "attempt to hide the following symbols from the local environment"
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski $$ printText ((sys2 `Set.difference` sys1) `Set.difference` sys3))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid sigma3 noSens,
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 }
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n'',node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = gEmbed (G_morphism lid mor3),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = HidingDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGLocal })
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Local_spec (replaceAnnoted sp2 asp)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (replaceAnnoted sp2' asp')
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma3,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx'' { devGraph = insEdgeNub link $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg'' })
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'
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lid'' gsig'' <- return gsigma''
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski incl1 <- adj $ ginclusion lg gsigma gsigma''
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder incl2 <- adj $ ginclusion lg gsigma' gsigma''
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder let node = getNewNode dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid'' gsig'' noSens,
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 {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl1,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_origin = DGClosedLenv }
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski link2 = (n',node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl2,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_origin = DGClosed })
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder insLink1 = case nsig of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> id
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Closed_spec (replaceAnnoted sp' asp) pos,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma'',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insLink1 $
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski insEdgeNub link2 $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg' })
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
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lid'' gsig'' <- return gsigma''
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski incl1 <- adj $ ginclusion lg gsigma gsigma''
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski incl2 <- adj $ ginclusion lg gsigma' gsigma''
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder let node = getNewNode dg'
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski node_contents = DGNode {
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid'' gsig'' noSens,
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 {
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_morphism = incl1,
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_type = GlobalDef,
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_origin = DGLogicQualLenv }
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski link2 = (n',node,DGLink {
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_morphism = incl2,
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_type = GlobalDef,
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski dgl_origin = DGLogicQual })
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder insLink1 = case nsig of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> id
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder return (Qualified_spec (Logic_name ln sublog)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted sp' asp) pos,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma'',
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = insLink1 $
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski insEdgeNub link2 $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg' })
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')
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Spec_inst spname afitargs pos -> do
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder let adj = adjustPos pos
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder case Map.lookup spname $ globalEnv gctx of
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Nothing -> fatal_error
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder ("Specification "++ showPretty spname " not found") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (ViewEntry _) ->
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder (showPretty spname " is a view, not a specification") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (ArchEntry _) ->
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder (showPretty spname
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder " is an architectural, not a structured specification") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (UnitEntry _) ->
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder (showPretty spname
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder " is a unit specification, not a structured specification") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (RefEntry) ->
95656e84acc96386173c1d6fc068aa2fb8820020Till Mossakowski (showPretty spname
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
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder gsigma@(G_sign lid gsig) <-
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder adj $ gsigUnion lg (getMaybeSig nsig) gsigmaB
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,
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski 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
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder incl <- adj $ ginclusion lg gsigmaB gsigma
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder let node = getNewNode dg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski node_contents = DGNode {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid gsig noSens,
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 {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_origin = DGSpecInst spname})
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx { devGraph = insEdgeNub link $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg })
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- the subcase with nonempty local env
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder JustNode (NodeSig n sigma) -> do
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder incl1 <- adj $ ginclusion lg sigma gsigma
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder incl2 <- adj $ ginclusion lg gsigmaB gsigma
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder let node = getNewNode dg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski node_contents = DGNode {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lid gsig noSens,
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 {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl1,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_origin = DGSpecInst spname})
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski link2 = (nB,node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl2,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_origin = DGSpecInst spname})
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigma,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx { devGraph = insEdgeNub link1 $
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski insEdgeNub link2 $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (node,node_contents) dg })
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- now the case with parameters
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let fitargs = map item afitargs
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (fitargs', gctx', args, _) <-
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder 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'
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lidRes gsigRes <- return gsigmaRes
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder incl1 <- adj $ ginclusion lg (getMaybeSig nsig) gsigmaRes
f3782b0e45c58a2410166c52a0854f46e0cbac65Till Mossakowski incl2 <- adj $ ginclusion lg gsigma' gsigmaRes
f3782b0e45c58a2410166c52a0854f46e0cbac65Till Mossakowski morDelta' <- comp Grothendieck (gEmbed morDelta) incl2
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder let node = getNewNode dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lidRes gsigRes noSens,
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 {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl1,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname}
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,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski parLinks = catMaybes (map (parLink gsigmaRes node) actualargs)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder return (Spec_inst spname
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (map (uncurry replaceAnnoted)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (zip (reverse fitargs') afitargs))
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder NodeSig node gsigmaRes ,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx' { devGraph = foldr insEdgeNub
f534c0116096e25659ceaa57de030c497ce9345aTill Mossakowski insEdgeNub link2 $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski anaFitArg res (nsig',fa) = do
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian Maeder (fas',dg1,args,name') <- res
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (fa',dg',arg) <- ana_FIT_ARG lg dg1 spname imps nsig' opts name' fa
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian 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,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitSpec }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (nA_i,node,link)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- finally the case with conflicting numbers of formal and actual parameters
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder (showPretty spname " expects "++show (length params)++" arguments"
3476beb5baf84bef7cc7d627b130de9d48700399Christian 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
c3a264bbb3692f9b44024c6024382e3ed6590688Christian 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
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski let gsigmaD' = G_sign lidP' sigmaD'
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder dg1 = devGraph gctx1
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski node_contents = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lidP' sigmaD' $ toThSens sensD',
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 }
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg1
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski link = (n',node,DGLink {
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski dgl_morphism = GMorphism cid sigmaD (ide lidP' sigmaD'),
5b1394673f35f4d23cfe08175841ab414a39678eMarkus Roggenbach dgl_type = GlobalDef,
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski dgl_origin = DGData })
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski dg2 = insEdgeNub link $
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski insNode (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
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederana_ren1 :: LogicGraph -> GMorphism -> G_mapping -> Result GMorphism
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_ren1 _ (GMorphism r sigma 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)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor2 <- comp lid2 mor mor1
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder return $ GMorphism r sigma mor2
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederana_ren1 lg mor (G_logic_translation (Logic_code tok src tar pos1)) = do
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder let adj = adjustPos pos1
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski G_sign srcLid srcSig <- 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"
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder mor1 <- adj $ gEmbedComorphism c (G_sign srcLid srcSig)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder adj $ comp Grothendieck mor mor1
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder where getLogicStr (Logic_name l _) = tokStr l
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederana_ren :: LogicGraph -> Result GMorphism -> G_mapping -> Result GMorphism
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowskiana_ren lg mor_res ren =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do mor <- mor_res
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski ana_ren1 lg mor ren
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_RENAMING :: LogicGraph -> G_sign -> HetcatsOpts -> RENAMING
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> Result GMorphism
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_RENAMING lg gSigma opts (Renaming ren _) =
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder if isStructured opts
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski then return (ide Grothendieck gSigma)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder else foldl (ana_ren lg) (return (ide Grothendieck gSigma)) ren
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of restrictions
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederana_restr1 :: DGraph -> G_sign -> GMorphism -> G_hiding -> Result GMorphism
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_restr1 _ (G_sign _lid _sigma) (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
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let sys' = Set.filter (\sy -> any (\rsy -> matches lid1 sy rsy) rsys)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- if sys' `disjoint` () then return ()
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder-- else error "attempt to hide symbols from the local environment"
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor1 <- cogenerated_sign lid1 sys' sigma1
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor1' <- map_morphism cid mor1
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder mor2 <- comp lid2 mor1' mor
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder return $ GMorphism cid (dom lid1 mor1) mor2
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_restr1 _dg _gSigma _mor
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (G_logic_projection (Logic_code _tok _src _tar pos1)) =
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder fatal_error "no analysis of logic projections yet" pos1
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_restr :: DGraph -> G_sign -> Result GMorphism -> G_hiding
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder -> Result GMorphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_restr dg gSigma mor_res restr =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do mor <- mor_res
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ana_restr1 dg gSigma 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)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_RESTRICTION' dg gSigma gSigma' False (Hidden restr _) =
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder do mor <- foldl (ana_restr dg gSigma)
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski (return (ide Grothendieck gSigma'))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (mor,Nothing)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski -- ??? Need to check that local env is not affected !
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederana_RESTRICTION' _ (G_sign lid sigma) (G_sign lid' sigma')
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)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (gEmbed (G_morphism lid' mor1),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just (gEmbed (G_morphism lid' mor2)))
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
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (NodeSig nP (G_sign lidP sigmaP)) opts name
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder (Fit_spec asp gsis pos) = do
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder let adj = adjustPos pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian 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 ()
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian 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 {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = gEmbed (G_morphism lidP mor),
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname})
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder return (Fit_spec (replaceAnnoted sp' asp) gsis pos,
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder gctx { devGraph = insEdgeNub link $ devGraph dg' },
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (G_morphism lidP mor,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
b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder case Map.lookup vn $ globalEnv gctx of
2b346670d3e146788fa056a4b0fafa357d8bf31bTill Mossakowski Nothing -> fatal_error
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder ("View "++ showPretty vn " not found") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (SpecEntry _) ->
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder (showPretty spname " is a specification, not a view") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (ArchEntry _) ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (showPretty spname
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder " is an architectural specification, not a view ") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (UnitEntry _) ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (showPretty spname
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder " is a unit specification, not a view") pos
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder Just (RefEntry) ->
95656e84acc96386173c1d6fc068aa2fb8820020Till Mossakowski (showPretty spname
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
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski GMorphism cid _ morHom <- 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,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_origin = DGFitView spname})
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder return (fv, gctx { devGraph = insEdgeNub link dg },
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (G_morphism lid morHom, 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))
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (pplain_error ()
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (text "Parameter does not match source of fittig view."
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder $$ text "Parameter signature:"
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder $$ printText gsigmaP
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder $$ text "Source signature of fitting view (united with import):"
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder $$ printText gsigmaIS) pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 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
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lidA gsigA <- return gsigmaA
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lidP gsigP <- 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
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder let [nA,n'] = newNodes 2 dg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski node_contentsA = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lidA gsigA noSens,
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,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lidP gsigP noSens,
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,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_origin = DGFitView spname})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link1 = (nSrc,n',DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl4,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitView spname})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski link2 = (nTar,nA,DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = incl2,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_origin = DGFitViewA spname})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski link3 = (nI,n',DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = incl3,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_origin = DGFitViewImp spname})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link4 = (nI,nA,DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl1,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitViewAImp spname})
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 $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insNode (nA,node_contentsA) $
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder insNode (n',node_contents') dg },
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (G_morphism lid mor_I, 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
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lidRes gsigRes <- 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
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski 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")
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski 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
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lidP gsigP <- return gsigmaP
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder let dg' = devGraph gctx'
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder [nA,n'] = newNodes 2 dg'
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski node_contentsA = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lidRes gsigRes noSens,
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,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lidP gsigP noSens,
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,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitView spname})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link1 = (nSrc,n',DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl4,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitView spname})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link2 = (nTar,nA,DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = mor',
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalDef,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitViewA spname})
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,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitViewImp spname})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link4 = (nI,nA,DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = incl2,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_type = GlobalDef,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitViewAImp spname})
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
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (insNode (nA,node_contentsA) $
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski insNode (n',node_contents') dg')
c3a264bbb3692f9b44024c6024382e3ed6590688Christian Maeder (fitLinks++parLinks) },
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (G_morphism lid1 theta, 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,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_origin = DGFitView spname }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (nA_i,node,link)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder-- finally the case with conflicting numbers of formal and actual parameters
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (showPretty spname " expects "++show (length params)++" arguments"
3476beb5baf84bef7cc7d627b130de9d48700399Christian 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)
eb8a05567e94cb9f477cd9dee6b337aa8dee02d6Christian Maeder Just ids -> if Set.null ids then return i else
eb8a05567e94cb9f477cd9dee6b337aa8dee02d6Christian Maeder Just j -> return j
eb8a05567e94cb9f477cd9dee6b337aa8dee02d6Christian Maeder Nothing -> pplain_error i
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (text "Identifier component " <+> printText i
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder <+> text "can be mapped in various ways:"
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski <+> printText ids) nullRange
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)
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaederextendMorphism (G_sign lid sigmaP) (G_sign lidB sigmaB1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (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))
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (pplain_error () (text "Symbols shared between actual parameter and body"
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder $$ text "must be in formal parameter:"
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder $$ printText 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))
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (pplain_error () (text
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "Fitting morphism leads to forbidden identifications"
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski $$ printText newIdentifications) nullRange)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski incl <- inclusion lid sigmaAD sigma
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder mor1 <- comp lid mor incl
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (G_sign lid sigma, G_morphism lid mor1)
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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lidI sigmaI <- return gsigmaI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let idI = ide lidI sigmaI
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski gsigmaA <- gsigManyUnion lg gsigmaA_i
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder mor_f <- homogeneousMorManyUnion (G_morphism lidI idI: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,
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (nsigI, [nsigP], JustNode nsigP),
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)
8a8880f1b6a0681e636480991d45dfea11d62ff8Christian Maeder G_sign lidP gsigP <- return gsigmaP
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski dgn_name = name,
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder dgn_theory = G_theory lidP gsigP noSens,
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''
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder node = getNewNode dg''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dg''' = insNode (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,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_origin = DGFormalParams }) 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)),
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski reverse pars,
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)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (srcNsig,tarNsig),
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
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian 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!"