AnalysisStructured.hs revision c529224e0ec191fbaa87261f05c34f89c17b3f3a
c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maeder Module : $Header$
75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski Copyright : (c) Till Mossakowski and Uni Bremen 2003
75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Maintainer : hets@tzi.de
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Stability : provisional
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Portability : portable
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Analysis of structured specifications
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski Follows the verfication semantic rules in Chap. IV:4.7
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski of the CASL Reference Manual.
82d681fe6950e2a35f28fdefb874d060632faccaTill Mossakowski Improve efficiency by storing local signature fragments only
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Name views in devgraphs?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Check that translations and reductions do not effect local env
82d681fe6950e2a35f28fdefb874d060632faccaTill Mossakowski (Implement new semantics for revealing here)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Unions (already in the parser) need unions of logics
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder = suprema in the lattice of default logic inclusions!
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (also needed by closed specs)
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.
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian 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!
c529224e0ec191fbaa87261f05c34f89c17b3f3aTill Mossakowski (or use heterogeneous compInclusion in Proofs/Proof.hs)
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
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski 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]
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski reveal Set[Object], #__, __eps__,
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski Nat,0,1,2,3,4,5,6,7,8,9,__@@__,__>=__,__<=__
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski op toSet : Subject -> Set [Object]
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski forall x : Subject; y : Object
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski . predicate (x,y) <=> y eps toSet(x)
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski pred minCardinality(s: Subject;n: Nat) <=>
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski # toSet(s) >= n;
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski maxCardinality(s: Subject;n: Nat) <=>
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski # toSet(s) <= n;
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski cardinality(s: Subject;n: Nat) <=>
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski # toSet(s) = n
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski%%} hide Pos,toSet,Set[Object],#__,__eps__,__<=__,__>=__
16f81021a104661b1872eb5af876e7c4d22fdab5Maciek Makowskimodule Static.AnalysisStructured (ana_SPEC, ana_GENERICITY, ana_VIEW_TYPE, ana_err,
16f81021a104661b1872eb5af876e7c4d22fdab5Maciek Makowski ana_RENAMING, ana_RESTRICTION)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Common.Lib.Graph hiding (empty)
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowskiimport qualified Common.Lib.Set as Set
c616e681da8c052b62e14247fea522da099ac0e4Christian Maederimport qualified Common.Lib.Map as Map
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Data.List hiding (union)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiimport Common.Lib.Parsec.Pos -- for testing purposes
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,
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- flag: shall only the structure be analysed?
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_SPEC :: LogicGraph -> GlobalContext -> NodeSig -> Maybe SIMPLE_ID ->
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Bool -> SPEC -> Result (SPEC,NodeSig,DGraph)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_SPEC lg gctx@(gannos,genv,dg) nsig name just_struct sp =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Basic_spec (G_basic_spec lid bspec) ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do G_sign lid' sigma' <- return (getSig nsig)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski sigma <- rcoerce lid' lid (newPos "a" 0 0) sigma'
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (bspec',sigma_local, sigma_complete, ax) <-
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski if just_struct
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski then return (bspec,empty_signature lid, empty_signature lid,[])
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski else do b <- maybeToResult (newPos "b" 0 0)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski ("no basic analysis for logic "
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski ++language_name lid)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski (basic_analysis lid)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski b (bspec,sigma,gannos)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl <- ginclusion lg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (G_sign lid sigma) (G_sign lid sigma_complete)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = G_sign lid sigma_complete, -- no, not only the delta
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid ax,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGBasic }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 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'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder NodeSig (n,_) -> insEdge (n,node,link) dg'
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Basic_spec (G_basic_spec lid bspec'),
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig (node,G_sign lid sigma_complete),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Translation asp ren ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp1',nsig',dg') <- ana_SPEC lg gctx nsig Nothing just_struct sp1
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski n' <- maybeToResult (newPos "c" 0 0)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Translation of empty spec" (getNode nsig')
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski let gsigma = getSig nsig'
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski mor <- ana_RENAMING dg gsigma just_struct ren
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? check that mor is identity on local env
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski let gsigma' = cod Grothendieck mor
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? too simplistic for non-comorphism inter-logic translations
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid' _ <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
a938729e277da5c7742bb88946ab2c150416fd5dTill Mossakowski dgn_sign = gsigma',
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGTranslation }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 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,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Reduction asp restr ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp1',nsig',dg') <- ana_SPEC lg gctx nsig Nothing just_struct sp1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigma = getSig nsig
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma' = getSig nsig'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski n' <- maybeToResult (newPos "d" 0 0)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Reduction of empty spec" (getNode nsig')
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski (hmor,tmor) <- ana_RESTRICTION dg gsigma gsigma' just_struct 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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid' _ <- return gsigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma'', -- G_sign lid' (empty_signature lid'),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGHiding }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 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,
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski NodeSig(node,gsigma''),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just tmor' ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the case with identity translation leads to a simpler dg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if tmor' == ide Grothendieck (dom Grothendieck tmor')
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let gsigma1 = dom Grothendieck tmor'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- ??? too simplistic for non-comorphism inter-logic reductions
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski G_sign lid1 _ <- return gsigma1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let [node1] = newNodes 0 dg'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski node_contents1 = DGNode {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma1, --G_sign lid1 (empty_signature lid1),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid1 [],
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_origin = DGRevealing }
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,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski NodeSig(node1,gsigma1),
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insEdge link1 $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insNode (node1,node_contents1) dg')
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let gsigma1 = dom Grothendieck tmor'
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski gsigma'' = cod Grothendieck tmor'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid1 _ <- return gsigma1
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid'' _ <- return gsigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [node1,node''] = newNodes 1 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents1 = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = Nothing,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma1, --G_sign lid1 (empty_signature lid1),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid1 [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGRevealing }
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,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma'', -- G_sign lid'' (empty_signature lid''),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid'' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGRevealTranslation }
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,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node'',gsigma''),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link'' $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node'',node_contents'') $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link1 $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node1,node_contents1) dg')
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski Union [] _ -> return (sp,nsig,dg)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Union asps pos ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sps = map item asps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sps',nsigs,dg') <-
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski let ana r sp' = do
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sps1,nsigs,dg') <- r
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp1,nsig',dg1) <- ana_SPEC lg (gannos,genv,dg')
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski nsig Nothing just_struct sp'
a205324331077b7d5a2c08fb3f0f57e5c029f9aaTill Mossakowski return (sp1:sps1,nsig':nsigs,dg1)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in foldl ana (return ([],[],dg)) sps
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let nsigs' = reverse nsigs
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski gbigSigma <- homogeneousGsigManyUnion (headPos pos) (map getSig nsigs')
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid' _ <- return gbigSigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gbigSigma, -- G_sign lid' (empty_signature lid'),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGUnion }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 dg'
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski insE dgres (n,gsigma) = do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl <- ginclusion lg gsigma gbigSigma
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let link = DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_origin = DGUnion }
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (insEdge (n,node,link) dg1)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dg'' <- foldl insE (return (insNode (node,node_contents) dg'))
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (catMaybes (map getNodeAndSig nsigs'))
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski return (Union (map (uncurry replaceAnnoted)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (zip (reverse sps') asps))
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski NodeSig(node,gbigSigma),
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski --Extension [] pos -> return (sp,nsig,dg)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Extension asps pos -> do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sps',nsig1,dg1) <- foldl ana (return ([],nsig,dg)) namedSps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Extension (map (uncurry replaceAnnoted)
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski (zip (reverse sps') asps))
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski namedSps = zip3 (map (\_ -> Nothing) (tail asps) ++ [name])
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski (nullPos:pos)
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski ana res (name',asp',pos') = do
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sps',nsig',dg') <- res
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski (sp1',nsig1,dg1) <-
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski ana_SPEC lg (gannos,genv,dg') nsig' name' just_struct (item asp')
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski dg2 <- case (any isImplies $ l_annos asp',getNode nsig',getNode nsig1) of
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski (True,Just n',Just n1) -> do
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski let sig1 = getSig nsig1
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski sig' = getSig nsig'
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski when (not (sig1==sig')) (pplain_error ()
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski (ptext "Signature must not be extended in presence of %implies")
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski return $ insEdge (n1,n',DGLink {
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski dgl_morphism = ide Grothendieck sig1,
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski dgl_type = LocalThm Open None Open,
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski dgl_origin = DGExtension }) dg1
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski _ -> return dg1
1a7b7802544aa94828d7f4e7be5788501c572934Till Mossakowski return (sp1':sps',nsig1,dg2)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Free_spec asp pos ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp',nsig',dg') <- ana_SPEC lg gctx nsig Nothing just_struct sp1
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski n' <- maybeToResult (newPos "e" 0 0)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Free spec over empty spec" (getNode nsig')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigma' = getSig nsig'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid' _ <- return gsigma'
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl <- ginclusion lg (getSig nsig) gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma', -- G_sign lid' (empty_signature lid'), -- delta is empty
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGFree }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = FreeDef nsig,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGFree })
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Free_spec (replaceAnnoted sp' asp) pos,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Cofree_spec asp pos ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp',nsig',dg') <- ana_SPEC lg gctx nsig Nothing just_struct sp1
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski n' <- maybeToResult (newPos "f" 0 0)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski "Internal error: Cofree spec over empty spec" (getNode nsig')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigma' = getSig nsig'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid' _ <- return gsigma'
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl <- ginclusion lg (getSig nsig) gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma', -- G_sign lid' (empty_signature lid'), -- delta is empty
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGCofree }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = CofreeDef nsig,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGCofree })
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Cofree_spec (replaceAnnoted sp' asp) pos,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Local_spec asp asp' pos ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski sp1' = item asp'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp2,nsig',dg') <- ana_SPEC lg gctx nsig Nothing just_struct sp1
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp2',nsig'',dg'') <- ana_SPEC lg (gannos,genv,dg') nsig' Nothing just_struct sp1'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski n'' <- maybeToResult (newPos "g" 0 0)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Local spec over empty spec" (getNode nsig'')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigma = getSig nsig
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma' = getSig nsig'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma'' = getSig nsig''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid sigma <- return gsigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid' sigma' <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid'' sigma'' <- return gsigma''
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski sigma1 <- rcoerce lid' lid (newPos "h" 0 0) sigma'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski sigma2 <- rcoerce lid'' lid (newPos "i" 0 0) sigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let sys = sym_of lid sigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys1 = sym_of lid sigma1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys2 = sym_of lid sigma2
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski mor3 <- if just_struct then return (ide lid sigma2)
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski else 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
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski when (not( just_struct || sys2 `Set.difference` sys1 `Set.subset` sys3))
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski (pplain_error ()
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski (ptext "attempt to hide the following symbols from the local environment"
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski $$ printText ((sys2 `Set.difference` sys1) `Set.difference` sys3))
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski (headPos pos))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma3, -- G_sign lid (empty_signature lid), -- delta is empty
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGLocal }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 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')
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma3),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg'')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Closed_spec asp pos ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder l = getLogic nsig
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp',nsig',dg') <- ana_SPEC lg gctx (EmptyNode l) Nothing just_struct sp1
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski n' <- maybeToResult (newPos "j" 0 0)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Closed spec over empty spec" (getNode nsig')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigma = getSig nsig
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma' = getSig nsig'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma'' <- homogeneousGsigUnion (headPos pos) gsigma gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- also allow different logics???
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid'' _ <- return gsigma''
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl1 <- ginclusion lg gsigma' gsigma''
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl2 <- ginclusion lg gsigma' gsigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma'', -- G_sign lid'' (empty_signature lid''),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid'' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGClosed }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link1 = (n',node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl1,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGClosed })
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link2 = DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl2,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGClosedLenv }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insLink2 = case (getNode nsig) of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Nothing -> id
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just n -> insEdge (n,node,link2)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Closed_spec (replaceAnnoted sp' asp) pos,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma''),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link1 $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Group asp pos -> do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (sp',nsig',dg') <- ana_SPEC lg gctx nsig name just_struct (item asp)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Group (replaceAnnoted sp' asp) pos,nsig',dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Spec_inst spname afitargs pos ->
c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder case Map.lookup spname genv of
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Nothing -> plain_error (sp,nsig,dg)
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder ("Specification "++ showPretty spname " not found") (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just (ViewEntry _) ->
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski plain_error (sp,nsig,dg)
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder (showPretty spname " is a view, not a specification") (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just (ArchEntry _) ->
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski plain_error (sp,nsig,dg)
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder (showPretty spname
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder " is an architectural, not a structured specification") (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just (UnitEntry _) ->
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski plain_error (sp,nsig,dg)
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder (showPretty spname
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder " is a unit specification, not a structured specification") (headPos pos)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski Just (SpecEntry gs@(imps,params,_,body)) ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case (\x y -> (x,x-y)) (length afitargs) (length params) of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- the case without parameters leads to a simpler dg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigmaB = getSig body
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski gsigma <- gsigLeftUnion lg (headPos pos) (getSig nsig) gsigmaB
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lid _ <- return gsigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nB <- maybeToResult (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: empty body spec" (getNode body)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case (getNode nsig) of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the subcase with empty local env leads to an even simpler dg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- if the node shall not be named and the logic does not change,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if isNothing name && langNameSig gsigma==langNameSig gsigmaB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- then just return the body
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski then return (sp,body,dg)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski -- otherwise, we need to create a new one
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl <- ginclusion lg gsigmaB gsigma
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let [node] = newNodes 0 dg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski node_contents = DGNode {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma, -- G_sign lid (empty_signature lid),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid [],
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgn_origin = DGSpecInst spname}
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski link = (nB,node,DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_type = GlobalDef,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_origin = DGSpecInst spname})
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski NodeSig(node,gsigma),
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski insEdge link $
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski insNode (node,node_contents) dg)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the subcase with nonempty local env
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl1 <- ginclusion lg (getSig nsig) gsigma
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl2 <- ginclusion lg gsigmaB gsigma
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski let [node] = newNodes 0 dg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski node_contents = DGNode {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma, -- G_sign lid (empty_signature lid),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid [],
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgn_origin = DGSpecInst spname}
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})
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski NodeSig(node,gsigma),
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski insEdge link1 $
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski insEdge link2 $
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski insNode (node,node_contents) dg)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- now the case with parameters
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let fitargs = map item afitargs
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (fitargs',dg',args) <-
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski foldl anaFitArg (return ([],dg,[])) (zip params fitargs)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let actualargs = reverse args
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (gsigma',morDelta) <- apply_GS (headPos pos) gs actualargs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski gsigmaRes <- homogeneousGsigUnion (headPos pos) (getSig nsig) gsigma'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski G_sign lidRes _ <- return gsigmaRes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nB <- maybeToResult (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: empty body spec" (getNode body)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski incl1 <- ginclusion lg (getSig nsig) gsigmaRes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigmaRes, -- G_sign lid' (empty_signature lid'),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lidRes [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGSpecInst spname}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link1 = DGLink {
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski dgl_morphism = incl1,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insLink1 = case (getNode nsig) of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Nothing -> id
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just n -> insEdge (n,node,link1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link2 = (nB,node,DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = gEmbed morDelta,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski parLinks = catMaybes (map (parLink gsigmaRes node) actualargs)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Spec_inst spname
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (map (uncurry replaceAnnoted)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (zip (reverse fitargs') afitargs))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski NodeSig(node,gsigmaRes),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldr insEdge
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link2 $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski anaFitArg res (nsig',fa) = do
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (fas',dg1,args) <- res
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (fa',dg',arg) <- ana_FIT_ARG lg (gannos,genv,dg1)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski spname imps nsig' just_struct fa
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (fa':fas',dg',arg:args)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski parLink gsigma' node (mor_i,nsigA_i) = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nA_i <- getNode nsigA_i
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski incl <- maybeResult $ ginclusion lg (getSig nsigA_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)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- finally the case with conflicting numbers of formal and actual parameters
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski plain_error (sp,nsig,dg)
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder (showPretty spname " expects "++show (length params)++" arguments"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ++" but was given "++show (length afitargs)) (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Qualified_spec logname asp pos ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ana_err "logic qualified specs"
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski Data (Logic lid1) asp1 asp2 pos ->
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski do let sp1 = item asp1
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski sp2 = item asp2
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski l = getLogic nsig
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski (sp1',nsig1,dg1) <-
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ana_SPEC lg gctx (EmptyNode lid1) Nothing just_struct sp1
49b9a9cbf17489cbaf97431247161f42e9fc5ae0Till Mossakowski (sp2',nsig2,dg2) <-
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ana_SPEC lg (gannos,genv,dg1) nsig1 Nothing just_struct sp2
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski n' <- maybeToResult (newPos "k" 0 0)
49b9a9cbf17489cbaf97431247161f42e9fc5ae0Till Mossakowski "Internal error: Data spec over empty spec" (getNode nsig1)
49b9a9cbf17489cbaf97431247161f42e9fc5ae0Till Mossakowski let gsigma' = getSig nsig1
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski G_sign lid' sigma' <- return gsigma'
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski let node_contents = DGNode {
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgn_name = name,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigma', -- G_sign lid' (empty_signature lid'), -- delta is empty
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lid' [],
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgn_origin = DGFree }
49b9a9cbf17489cbaf97431247161f42e9fc5ae0Till Mossakowski [node] = newNodes 0 dg2
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski link = (n',node,DGLink {
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski dgl_morphism = error "AnalysisStructured.hs:5", -- ??? inclusion
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgl_type = FreeDef nsig,
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgl_origin = DGFree })
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski return (Data (Logic lid1)
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski (replaceAnnoted sp1' asp1)
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski (replaceAnnoted sp2' asp2)
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski NodeSig(node,gsigma'),
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski insEdge link $
49b9a9cbf17489cbaf97431247161f42e9fc5ae0Till Mossakowski insNode (node,node_contents) dg2)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of renamings
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_ren1 :: DGraph -> GMorphism -> (G_mapping,Pos) -> Result GMorphism
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_ren1 _ (GMorphism r sigma mor)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (G_symb_map (G_symb_map_items_list lid sis),pos) = do
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski let lid2 = targetLogic r
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sis1 <- rcoerce lid2 lid pos sis
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder rmap <- stat_symb_map_items lid2 sis1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor1 <- induced_from_morphism lid2 rmap (cod lid2 mor)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor2 <- maybeToResult pos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "renaming: signature morphism composition failed"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (comp lid2 mor mor1)
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski return (GMorphism r sigma mor2)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_ren1 _ mor (G_logic_translation (Logic_code tok src tar pos1),pos2) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder fatal_error "no analysis of logic translations yet" pos2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_ren :: DGraph -> Result GMorphism -> (G_mapping,Pos) -> Result GMorphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_ren dg mor_res ren =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do mor <- mor_res
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ana_ren1 dg mor ren
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowskiana_RENAMING :: DGraph -> G_sign -> Bool -> RENAMING -> Result GMorphism
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowskiana_RENAMING dg gSigma just_struct (Renaming ren pos) =
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski if just_struct
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski then return (ide Grothendieck gSigma)
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski else foldl (ana_ren dg) (return (ide Grothendieck gSigma)) ren'
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski ren' = zip ren (tail (pos ++ repeat (newPos "l" 0 0)))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of restrictions
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_restr1 :: DGraph -> G_sign -> GMorphism -> (G_hiding,Pos) -> Result GMorphism
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_restr1 _ (G_sign lid sigma) (GMorphism cid sigma1 mor)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (G_symb_list (G_symb_items_list lid' sis'),pos) = do
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski let lid1 = sourceLogic cid
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski lid2 = targetLogic cid
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sis1 <- rcoerce lid1 lid' pos sis'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian 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 ()
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- else plain_error () "attempt to hide symbols from the local environment" pos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor1 <- cogenerated_sign lid1 sys' sigma1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor1' <- maybeToResult pos
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ("restriction: could not map morphism along" ++ language_name cid)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (map_morphism cid mor1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor2 <- maybeToResult pos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "restriction: signature morphism composition failed"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (comp lid2 mor1' mor)
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski return (GMorphism cid (dom lid1 mor1) mor2)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_restr1 dg gSigma mor
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (G_logic_projection (Logic_code tok src tar pos1),pos2) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder fatal_error "no analysis of logic projections yet" pos2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_restr :: DGraph -> G_sign -> Result GMorphism -> (G_hiding,Pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian 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
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowskiana_RESTRICTION :: DGraph -> G_sign -> G_sign -> Bool -> RESTRICTION
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> Result (GMorphism, Maybe GMorphism)
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowskiana_RESTRICTION _ _ gSigma True _ =
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski return (ide Grothendieck gSigma,Nothing)
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowskiana_RESTRICTION dg gSigma gSigma' False (Hidden restr pos) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do mor <- foldl (ana_restr dg gSigma)
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski (return (ide Grothendieck gSigma'))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (mor,Nothing)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski restr' = zip restr (tail (pos ++ repeat (newPos "m" 0 0)))
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski -- ??? Need to check that local env is not affected !
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_RESTRICTION _ (G_sign lid sigma) (G_sign lid' sigma')
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski 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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sis' <- rcoerce lid1 lid' (headPos pos) sis
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder rmap <- stat_symb_map_items lid' sis'
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowski [sy | sy <- Set.toList sys', rsy <- 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' ???
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys1 <- rcoerce lid lid' (headPos pos) sys
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? this is too simple in case that local env is translated
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- to a different logic
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mor1 <- generated_sign lid' (sys1 `Set.union` sys'') sigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor2 <- induced_from_morphism lid' rmap (dom lid' mor1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (gEmbed (G_morphism lid' mor1),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just (gEmbed (G_morphism lid' mor2)))
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_FIT_ARG :: LogicGraph -> GlobalContext -> SPEC_NAME -> NodeSig -> NodeSig
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski -> Result (FIT_ARG, DGraph, (G_morphism,NodeSig))
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_FIT_ARG lg gctx spname nsigI nsigP just_struct
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Fit_spec asp gsis pos) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let adj = adjustPos (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski nP <- maybeToResult (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: empty parameter spec" (getNode nsigP)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (sp',nsigA,dg') <- ana_SPEC lg gctx nsigI Nothing just_struct (item asp)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski nA <- maybeToResult (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: empty argument spec" (getNode nsigA)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigmaP = getSig nsigP
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaA = getSig nsigA
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaI = getSig nsigI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lidP sigmaP <- return gsigmaP
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lidA sigmaA <- return gsigmaA
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lidI sigmaI <- return gsigmaI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_symb_map_items_list lid sis <- return gsis
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sigmaA' <- rcoerce lidA lidP (headPos pos) sigmaA
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sigmaI' <- rcoerce lidI lidP (headPos pos) sigmaI
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski mor <- if just_struct then return (ide lidP sigmaP)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski rmap <- adj $ stat_symb_map_items lid sis
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski rmap' <- rcoerce lid lidP (headPos pos) rmap
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski adj $ 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?
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski {- if Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder then return ()
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else plain_error () "Fitting morphism must not affect import" (headPos 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),
022f4e4f5488defedc48581e87f0222f82d5afe4Jorina Freya Gerken dgl_type = GlobalThm Open None Open,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname})
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Fit_spec (replaceAnnoted sp' asp) gsis pos,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski insEdge link dg',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (G_morphism lidP mor,nsigA)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_FIT_ARG lg gctx@(gannos,genv,dg) spname nsigI nsigP just_struct
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski fv@(Fit_view vn afitargs pos ans) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case Map.lookup vn genv of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> plain_error (fv,dg,error "no morphism")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ("View "++ showPretty vn " not found") (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just (SpecEntry _) ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski plain_error (fv,dg,error "no fit view")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (showPretty spname " is a specification, not a view") (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just (ArchEntry _) ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski plain_error (fv,dg,error "no fit view")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (showPretty spname
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski " is an architectural specification, not a view ") (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just (UnitEntry _) ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski plain_error (fv,dg,error "no fit view")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (showPretty spname
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski " is a unit specification, not a view") (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just (ViewEntry (src,mor,gs@(imps,params,_,target))) -> do
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski let adj = adjustPos (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski nSrc <- maybeToResult (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "Internal error: empty source spec of view" (getNode src)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski nTar <- maybeToResult (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "Internal error: empty target spec of view" (getNode target)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski nP <- maybeToResult (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "Internal error: empty parameter specification" (getNode nsigP)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let gsigmaS = getSig src
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski gsigmaT = getSig target
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski gsigmaP = getSig nsigP
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski gsigmaI = getSig nsigI
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski gsigmaIS <- gsigLeftUnion lg (headPos pos) gsigmaI gsigmaS
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski when (not (gsigmaIS == gsigmaP))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (pplain_error ()
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (ptext "Parameter does not match source of fittig view."
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $$ ptext "Parameter signature:"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $$ printText gsigmaP
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $$ ptext "Source signature of fitting view (united with import):"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $$ printText gsigmaIS) (headPos pos))
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 (headPos pos))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case (\x y -> (x,x-y)) (length afitargs) (length params) of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the case without parameters leads to a simpler dg
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (0,0) -> case getNode nsigI of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the subcase with empty import leads to a simpler dg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let link = (nP,nSrc,DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = ide Grothendieck gsigmaP,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalThm Open None Open,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_origin = DGFitView spname})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (fv,insEdge link dg,(G_morphism lid morHom,target))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- the subcase with nonempty import
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just nI -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski G_sign lidI sigI1 <- return gsigmaI
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sigI <- rcoerce lidI lid (headPos pos) sigI1
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski mor_I <- adj $ morphism_union lid morHom $ ide lid sigI
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski gsigmaA <- gsigLeftUnion lg (headPos pos) gsigmaI gsigmaT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski G_sign lidA _ <- return gsigmaA
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski G_sign lidP _ <- 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
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let [nA,n'] = newNodes 1 dg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski node_contentsA = DGNode {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_name = Nothing,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigmaA,
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lidA [],
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_origin = DGFitViewA spname}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski node_contents' = DGNode {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_name = Nothing,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigmaP,
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lidP [],
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_origin = DGFitView spname}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski link = (nP,n',DGLink {
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_morphism = ide Grothendieck gsigmaP,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgl_type = GlobalThm Open None Open,
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})
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insEdge link $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insEdge link1 $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insEdge link2 $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insEdge link3 $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insEdge link4 $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insNode (nA,node_contentsA) $
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insNode (n',node_contents') dg,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (G_morphism lid mor_I,NodeSig (nA,gsigmaA)))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- now the case with parameters
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let fitargs = map item afitargs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (fitargs',dg',args) <-
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski foldl anaFitArg (return ([],dg,[])) (zip params fitargs)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let actualargs = reverse args
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (gsigmaA,mor_f) <- apply_GS (headPos pos) gs actualargs
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski let gmor_f = gEmbed mor_f
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski gsigmaRes <- homogeneousGsigUnion (headPos pos) gsigmaI gsigmaA
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski G_sign lidRes _ <- return gsigmaRes
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski mor1 <- maybeToResult (headPos pos)
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (show (ptext "Morphism composition failed when instantiating generic fitting view"
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski $$ ptext "Morphism 1" $$ printText mor
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski $$ ptext "Morphism 2" $$ printText gmor_f))
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski $ comp Grothendieck mor gmor_f
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski incl1 <- adj $ ginclusion lg gsigmaA gsigmaRes
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski mor' <- maybeToResult (headPos pos)
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (show (ptext "Morphism composition with inclusion failed in fitting view"
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski $$ ptext "Morphism 1" $$ printText gmor_f
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski $$ ptext "Morphism 2" $$ printText incl1))
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski $ 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 (headPos pos))
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski G_sign lidI sigI1 <- return gsigmaI
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski sigI <- rcoerce lidI lid1 (headPos pos) 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
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski G_sign lidP _ <- return gsigmaP
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski let [nA,n'] = newNodes 1 dg'
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski node_contentsA = DGNode {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgn_name = Nothing,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgn_sign = gsigmaRes,
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lidRes [],
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgn_origin = DGFitViewA spname}
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski node_contents' = DGNode {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgn_name = Nothing,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgn_sign = gsigmaP,
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lidP [],
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgn_origin = DGFitView spname}
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski link = (nP,n',DGLink {
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_morphism = ide Grothendieck gsigmaP,
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski dgl_type = GlobalThm Open None Open,
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})
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski fitLinks = [link,link1,link2] ++ case getNode nsigI of
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski Nothing -> []
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski Just 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)
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski return (Fit_view vn
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (map (uncurry replaceAnnoted)
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (zip (reverse fitargs') afitargs))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski foldr insEdge
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (insNode (nA,node_contentsA) $
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski insNode (n',node_contents') dg')
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (fitLinks++parLinks),
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski (G_morphism lid1 theta,NodeSig (nA,gsigmaRes)))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski anaFitArg res (nsig',fa) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (fas',dg1,args) <- res
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (fa',dg',arg) <- ana_FIT_ARG lg (gannos,genv,dg1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski spname imps nsig' just_struct fa
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (fa':fas',dg',arg:args)
a946fa1fe525f04a8b4e2734fa2082bbe5e6ed3fTill Mossakowski parLink gsigmaRes node (mor_i,nsigA_i) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 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)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- finally the case with conflicting numbers of formal and actual parameters
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski plain_error (fv,dg,error "no fit view")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (showPretty spname " expects "++show (length params)++" arguments"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ++" but was given "++show (length afitargs)) (headPos pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- Extension of signature morphisms (for instantitations)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- first some auxiliary functions
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski{- not really needed:
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- for an Id, compute the list of components that are relevant for extension
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidComponents :: Id -> Set.Set Id -> [Id]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidComponents (Id toks comps pos) ids =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski foldl (\x y -> y++x) []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ map (\id1 -> if id1 `Set.member` ids
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else idComponents id1 ids)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicomponentRelation :: Set.Set Id -> Set.Set (Id,[Id])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicomponentRelation ids =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Set.image (\id -> (id,idComponents id ids)) ids
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapID :: Pos -> Map.Map Id (Set.Set Id) -> Id -> Result Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapID pos idmap id@(Id toks comps pos1) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case Map.lookup id idmap of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compsnew <- sequence $ map (mapID pos idmap) comps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (Id toks compsnew pos1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just ids -> case Set.size ids of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 0 -> return id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 1 -> return $ Set.findMin ids
82d681fe6950e2a35f28fdefb874d060632faccaTill Mossakowski _ -> pplain_error id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (ptext "Identifier component " <+> printText id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski <+> ptext "can be mapped in various ways:"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski <+> printText ids) pos
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiextID1 :: Pos -> Map.Map Id (Set.Set Id) -> Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Result (Map.EndoMap Id) -> Result (Map.EndoMap Id)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiextID1 pos idmap id@(Id toks comps pos1) m = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compsnew <- sequence $ map (mapID pos idmap) comps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if comps==compsnew
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski then return m1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else return (Map.insert id (Id toks compsnew pos1) m1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiextID :: Pos -> Set.Set Id -> Map.Map Id (Set.Set Id) -> Result (Map.EndoMap Id)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiextID pos ids idmap =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Set.fold (extID1 pos idmap) (return Map.empty) ids
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederextendMorphism :: Pos -> G_sign -> G_sign -> G_sign -> G_morphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Result(G_sign,G_morphism)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiextendMorphism pos (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....
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sigmaB <- rcoerce lidB lid pos sigmaB1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sigmaA <- rcoerce lidA lid pos sigmaA1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski fittingMor <- rcoerce lidM lid pos fittingMor1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let symsP = sym_of lid sigmaP
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski symsB = sym_of lid sigmaB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski idsB = Set.image (sym_name lid) symsB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski h = symmap_of lid fittingMor
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski symbMapToRawSymbMap =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Map.foldWithKey (\sy1 sy2 -> Map.insert (symbol_to_raw lid sy1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (symbol_to_raw lid sy2))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski rh = symbMapToRawSymbMap h
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (\sy1 sy2 -> Map.setInsert (sym_name lid sy1) (sym_name lid sy2))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski idhExt <- extID pos idsB idh
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (\id1 id2 -> Map.insert (id_to_raw lid id1) (id_to_raw lid id2))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (foldr (\id -> Map.delete id) 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 )
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski when (not (Set.isEmpty illShared))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (pplain_error () (ptext
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "Symbols shared between actual parameter and body must be in formal parameter"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $$ printText illShared) pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let newIdentifications = Map.kernel hmor Set.\\ Map.kernel h
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Set.\\ Set.fromList (map (\x -> (x,x)) (Map.keys hmor))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski when (not (Set.isEmpty newIdentifications))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (pplain_error () (ptext
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski "Fitting morphism leads to forbidden identifications"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $$ printText newIdentifications) pos)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski incl <- inclusion lid sigmaAD sigma
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mor1 <- maybeToResult pos
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ("extendMorphism: composition of two morphisms failed:"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ++showPretty mor "\n" ++ showPretty incl "")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ comp lid mor incl
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (G_sign lid sigma, G_morphism lid mor1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederapply_GS :: Pos -> ExtGenSig -> [(G_morphism,NodeSig)] -> Result(G_sign,G_morphism)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederapply_GS pos (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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaI = getSig nsigI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lidI sigmaI <- return gsigmaI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let idI = ide lidI sigmaI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaA <- homogeneousGsigManyUnion pos gsigmaA_i
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor_f <- homogeneousMorManyUnion pos (G_morphism lidI idI:mor_i)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder extendMorphism pos gsigmaP gsigmaB gsigmaA mor_f
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- | analyze a GENERICITY
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- Parameters: global context, current logic, just-structure-flag, GENERICITY
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_GENERICITY :: LogicGraph -> GlobalContext -> AnyLogic -> Bool
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski -> GENERICITY
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (GENERICITY,ExtGenSig,DGraph)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- zero parameters,
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_GENERICITY _ (_,_,dg) l@(Logic lid) _
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski gen@(Genericity (Params []) (Imported imps) pos) = do
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski when (not (null imps))
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (plain_error () "Parameterless specifications must not have imports"
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (headPos pos))
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (gen,(EmptyNode l,[],G_sign lid (empty_signature lid),EmptyNode l),dg)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- one parameter ...
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_GENERICITY lg gctx@(gannos,genv,_) l just_struct
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Genericity (Params [asp]) imps pos) = do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (imps',nsigI,dg') <- ana_IMPORTS lg gctx l just_struct imps
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (sp',nsigP,dg'') <- ana_SPEC lg (gannos,genv,dg') nsigI Nothing just_struct (item asp)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Genericity (Params [replaceAnnoted sp' asp]) imps' pos,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (nsigI,[nsigP],getSig nsigP,nsigP),
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- ... and more parameters
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_GENERICITY lg gctx@(gannos,genv,_) l just_struct
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Genericity params imps pos) = do
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (imps',nsigI,dg') <- ana_IMPORTS lg gctx l just_struct imps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (params',nsigPs,dg'') <-
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ana_PARAMS lg (gannos,genv,dg') l nsigI just_struct params
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaP <- homogeneousGsigManyUnion (headPos pos) (map getSig nsigPs)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski G_sign lidP _ <- return gsigmaP
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = Nothing,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski dgn_sign = gsigmaP, -- G_sign lidP (empty_signature lidP),
242691238a8d1a89581751d782af87ec5d7470c0Till Mossakowski dgn_sens = G_l_sentence_list lidP [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGFormalParams }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 dg''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dg''' = insNode (node,node_contents) dg''
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski inslink dgres nsig = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case getNode nsig of
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Nothing -> return dg
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski incl <- ginclusion lg (getSig nsig) gsigmaP
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski return (insEdge (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,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (nsigI,nsigPs,gsigmaP,NodeSig(node,gsigmaP)),
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_PARAMS :: LogicGraph -> GlobalContext -> AnyLogic -> NodeSig -> Bool
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (PARAMS,[NodeSig],DGraph)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowskiana_PARAMS lg (gannos,genv,dg) _ nsigI just_struct (Params asps) = do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sps',pars,dg') <- foldl ana (return ([],[],dg)) (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
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sps',pars,dg1) <- res
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (sp',par,dg') <- ana_SPEC lg (gannos,genv,dg1) nsigI Nothing just_struct sp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (sp':sps',par:pars,dg')
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_IMPORTS :: LogicGraph -> GlobalContext -> AnyLogic -> Bool -> IMPORTED
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (IMPORTED,NodeSig,DGraph)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_IMPORTS lg gctx l just_struct (Imported asps) = do
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski let sp = Union asps (map (\_ -> (newPos "p" 0 0)) asps)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Union asps' _,nsig',dg') <-
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ana_SPEC lg gctx (EmptyNode l) Nothing just_struct sp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Imported asps',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
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_VIEW_TYPE:: LogicGraph -> GlobalContext -> AnyLogic -> NodeSig -> Bool
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (VIEW_TYPE,(NodeSig,NodeSig),DGraph)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiana_VIEW_TYPE lg gctx@(gannos,genv,_) l parSig just_struct
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (View_type aspSrc aspTar pos) = do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (spSrc',srcNsig,dg') <-
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ana_SPEC lg gctx (EmptyNode l) Nothing just_struct (item aspSrc)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (spTar',tarNsig,dg'') <-
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ana_SPEC lg (gannos,genv,dg') parSig Nothing just_struct (item aspTar)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (View_type (replaceAnnoted spSrc' aspSrc)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (replaceAnnoted spTar' aspTar)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (srcNsig,tarNsig),
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- | Auxiliary function for not yet implemented features
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_err :: String -> a
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_err fname =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder error ("*** Analysis of " ++ fname ++ " is not yet implemented!")