AnalysisStructured.hs revision a205324331077b7d5a2c08fb3f0f57e5c029f9aa
c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maeder Module : $Header$
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski Cop-D�yright : (c) Till Mossakowski and Uni Bremen 2003-A
c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maeder Licence : All rights reserved.
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Maintainer : hets@tzi.de
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Stability : provisional
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Portability : portable
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Analysis of structured specifications
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Follows the extended static semantic rules in:
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder CASL Proof calculus.
c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maeder Available from <http://www.informatik.uni-bremen.de/~till/calculus.ps>
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder To appear in the CASL book.
c0ba7121c93e4f9292f2d95a0ac7460a7b9e5aeaTill Mossakowski Option: only the structure is analysed => also for symbol maps!
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Check that translations and reductions do not effect local env
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)
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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Revealings wihout translations: just one arrow
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Pushouts: only admissible within one logic?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Optimizations:
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski Union nodes can be extended by a basic spec directly (no new node needed)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Also: free, cofree nodes
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskimodule Static.AnalysisStructured (ana_SPEC, ana_GENERICITY, ana_VIEW_TYPE, ana_err)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Common.Lib.Graph hiding (empty)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Common.Lib.Set hiding (filter)
c616e681da8c052b62e14247fea522da099ac0e4Christian Maederimport qualified Common.Lib.Map as Map
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Data.List hiding (union)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- should be moved to eslewhere!
e18f5e61d29064a427ca7bef421e250a9a4c9701Till MossakowskilookupNode :: Node -> Graph a b -> a
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederlookupNode n dg = lab' $ context n dg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedersetFilter p s = fromList (filter p (toList s))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedersetAny p s = any p (toList s)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedersetAll p s = all p (toList s)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeders1 `disjoint` s2 = s1 `intersection` s2 == empty
c616e681da8c052b62e14247fea522da099ac0e4Christian MaederdomFM m = fromList (Map.keys m)
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?
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_SPEC :: GlobalContext -> NodeSig -> Maybe SIMPLE_ID -> Bool -> SPEC
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (SPEC,NodeSig,DGraph)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_SPEC 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)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sigma <- rcoerce lid' lid nullPos 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,[])
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski else do b <- maybeToResult nullPos
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski ("no basic analysis for logic "
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski ++language_name lid)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski (basic_analysis lid)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski b (bspec,sigma,gannos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid sigma_local, -- only the delta
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence 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 {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = undefined, -- where to get it from ???
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 ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sp = item asp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder n' <- maybeToResult nullPos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Translation of empty spec" (getNode nsig')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor <- ana_RENAMING dg (getSig nsig') ren
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? check that mor is identity on local env
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let gsigma' = codGrothendieck mor
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? too simplistic for non-comorphism inter-logic translations
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid' sigma' <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence 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 })
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Translation (replaceAnnoted sp' asp) ren,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Reduction asp restr ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sp = item asp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigma = getSig nsig
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma' = getSig nsig'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder n' <- maybeToResult nullPos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Reduction of empty spec" (getNode nsig')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (hmor,tmor) <- ana_RESTRICTION dg gsigma gsigma' restr
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- we treat hiding and revealing differently
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- in order to keep the dg as simple as possible
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do let gsigma' = domGrothendieck hmor
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid' sigma' <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence 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 })
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Reduction (replaceAnnoted sp' asp) restr,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just tmor' ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do let gsigma1 = domGrothendieck tmor'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski gsigma'' = codGrothendieck tmor'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid1 sigma1 <- return gsigma1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid'' sigma'' <- return gsigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [node1,node''] = newNodes 1 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents1 = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = Nothing,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid1 (empty_signature lid1),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence 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,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid'' (empty_signature lid''),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence 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 })
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Reduction (replaceAnnoted sp' 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')
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Union [] pos -> return (sp,nsig,dg)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Union asps pos ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sps = map item asps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sps',nsigs,dg') <-
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski let ana r sp = do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sps1,nsigs,dg) <- r
a205324331077b7d5a2c08fb3f0f57e5c029f9aaTill Mossakowski (sp1,nsig',dg1) <- ana_SPEC (gannos,genv,dg) 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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nodes = catMaybes (map getNode nsigs')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid' bigSigma <-
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder homogeneousGsigManyUnion (headPos pos) (map getSig nsigs')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGUnion }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = undefined, -- ??? how to get it?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGUnion }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (let insE dg n = insEdge (n,node,link) dg -- link should vary
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in (Union (map (uncurry replaceAnnoted)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (zip (reverse sps') asps))
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,G_sign lid' bigSigma),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldl insE (insNode (node,node_contents) dg') nodes))
e379124f467e5d0ef7d3c0ca238bff0521f70831Till 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))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder namedSps = zip (map (\_ -> Nothing) (tail asps) ++ [name]) (map item asps)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ana res (name,sp) = do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sps',nsig,dg) <- res
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp1',nsig1,dg1) <- ana_SPEC (gannos,genv,dg) nsig name just_struct sp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (sp1':sps',nsig1,dg1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Free_spec asp pos ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sp = item asp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder n' <- maybeToResult nullPos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Free spec over empty spec" (getNode nsig')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigma' = getSig nsig'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid' sigma' <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGFree }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = undefined, -- ??? inclusion
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 ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sp = item asp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder n' <- maybeToResult nullPos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: Free spec over empty spec" (getNode nsig')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let gsigma' = getSig nsig'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid' sigma' <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGCofree }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (n',node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = undefined, -- ??? inclusion
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 ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sp = item asp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sp' = item asp'
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp1,nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp1',nsig'',dg'') <- ana_SPEC (gannos,genv,dg') nsig' Nothing just_struct sp'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder n'' <- maybeToResult nullPos
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''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sigma1 <- rcoerce lid' lid nullPos sigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sigma2 <- rcoerce lid'' lid nullPos sigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let sys = sym_of lid sigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys1 = sym_of lid sigma1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys2 = sym_of lid sigma2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor3 <- cogenerated_sign lid (toList (sys1 `difference` sys)) sigma2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let sigma3 = dom lid mor3
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma2 = G_sign lid sigma2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma3 = G_sign lid sigma3
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys3 = sym_of lid sigma3
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if sys2 `difference` sys1 `subset` sys3 then return ()
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else plain_error ()
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "attempt to hide symbols from the local environment" (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid (empty_signature lid), -- delta is empty
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence 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 })
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Local_spec (replaceAnnoted sp1 asp)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (replaceAnnoted sp1' asp')
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma3),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg'')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Closed_spec asp pos ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sp = item asp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder l = getLogic nsig
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',nsig',dg') <- ana_SPEC gctx (EmptyNode l) Nothing just_struct sp
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder n' <- maybeToResult nullPos
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???
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid'' sigma'' <- return gsigma''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid'' (empty_signature lid''),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence lid'' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGClosed }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link1 = (n',node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = inclusion gsigma' gsigma'',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGClosed })
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link2 = DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = inclusion gsigma' gsigma'',
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
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',nsig',dg') <- ana_SPEC 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)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just (SpecEntry gs@(imps,params,gSigmaP,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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigma <- homogeneousGsigUnion (headPos pos) (getSig nsig) gsigmaB
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid sigma <- return gsigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nB <- maybeToResult (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: empty body spec" (getNode body)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case (getNode nsig) of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- the case with empty local env leads to an even simpler dg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Nothing -> case name of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- if the node shall not be named, just return the body
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Nothing -> return (sp,body,dg)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- if the node shall be named, we need to create a new one
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [node] = newNodes 0 dg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid (empty_signature lid),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence lid [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGSpecInst spname}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link = (nB,node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = inclusion gsigmaB gsigma,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname})
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in return (sp,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- the case with nonempty local env
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [node] = newNodes 0 dg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid (empty_signature lid),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence lid [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGSpecInst spname}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link1 = (n,node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = inclusion (getSig nsig) gsigma,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname})
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link2 = (nB,node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = inclusion gsigmaB gsigma,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname})
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in return (sp,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link1 $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link2 $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- now the general case: with parameters
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let fitargs = map item afitargs
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (fitargs',dg',args) <-
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski foldl ana (return ([],dg,[])) (zip params fitargs)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let actualargs = reverse args
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (gsigma',mor_f) <- apply_GS (headPos pos) gs actualargs
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid' sigma' <- return gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaRes <- homogeneousGsigUnion (headPos pos) (getSig nsig) gsigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nB <- maybeToResult (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: empty body spec" (getNode body)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [node] = newNodes 0 dg'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = name,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence lid' [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGSpecInst spname}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder link1 = DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = inclusion (getSig nsig) gsigma',
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 {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = inclusion (getSig body) gsigma',
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGSpecInst spname})
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder parLinks = catMaybes (map (parLink node) actualargs)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Spec_inst spname
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (map (uncurry replaceAnnoted)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (zip (reverse fitargs') afitargs))
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski NodeSig(node,gsigma'),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldr insEdge
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insEdge link2 $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder insNode (node,node_contents) dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ana res (nsig,fa) = do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (fas',dg,args) <- res
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (fa',dg',arg) <- ana_FIT_ARG (gannos,genv,dg)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski spname imps nsig just_struct fa
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (fa':fas',dg',arg:args)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder parLink node (mor_i,nsigA_i) = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nA_i <- getNode nsigA_i
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let link = DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = gEmbed mor_i,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGClosed }
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) <-
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski ana_SPEC gctx (EmptyNode lid1) Nothing just_struct sp1
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski (sp2'nsig2,dg2) <-
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski ana_SPEC (gannos,genv,dg1) nsig1 Nothing just_struct sp2
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski n' <- maybeToResult nullPos
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski "Internal error: Free spec over empty spec" (getNode nsig')
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski let gsigma' = getSig nsig'
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski G_sign lid' sigma' <- return gsigma'
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski let node_contents = DGNode {
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgn_name = name,
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgn_sens = G_l_sentence lid' [],
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgn_origin = DGFree }
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski [node] = newNodes 0 dg'
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski link = (n',node,DGLink {
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski dgl_morphism = undefined, -- ??? 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 $
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski insNode (node,node_contents) dg')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of renamings
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiana_ren1 dg (GMorphism r sigma mor)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (G_symb_map (G_symb_map_items_list lid sis),pos) = do
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski let lid1 = sourceLogic r
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski 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)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_ren1 dg 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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_RENAMING :: DGraph -> G_sign -> RENAMING -> Result GMorphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_RENAMING dg gSigma (Renaming ren pos) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski foldl (ana_ren dg) (return (ideGrothendieck gSigma)) ren'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ren' = zip ren (tail (pos ++ repeat nullPos))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of restrictions
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskiana_restr1 dg (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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let sys' = 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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_RESTRICTION :: DGraph -> G_sign -> G_sign -> RESTRICTION
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> Result (GMorphism, Maybe GMorphism)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_RESTRICTION dg gSigma gSigma' (Hidden restr pos) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do mor <- foldl (ana_restr dg gSigma)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (return (ideGrothendieck gSigma'))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (mor,Nothing)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder restr' = zip restr (tail (pos ++ repeat nullPos))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederana_RESTRICTION dg gSigma@(G_sign lid sigma) gSigma'@(G_sign lid' sigma')
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (Revealed (G_symb_map_items_list lid1 sis) pos) =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do let sys = sym_of lid sigma
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sys' = sym_of lid' sigma'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sis' <- rcoerce lid1 lid' (headPos pos) sis
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder rmap <- stat_symb_map_items lid' sis'
c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder [sy | sy <- toList sys', rsy <- Map.keys rmap, matches lid' sy rsy]
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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if sys1 `disjoint` sys'' then return ()
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else plain_error () "attempt to hide symbols from the local environment" (headPos pos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor1 <- generated_sign lid' (toList (sys1 `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)))
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskiana_FIT_ARG gctx@(gannos,genv,dg) spname nsigI nsigP just_struct
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Fit_spec asp gsis pos) = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nP <- maybeToResult nullPos
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "Internal error: empty parameter spec" (getNode nsigP)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',nsigA,dg') <- ana_SPEC gctx nsigI Nothing just_struct (item asp)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder nA <- maybeToResult nullPos
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 rmap <- stat_symb_map_items lid sis
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sigmaA' <- rcoerce lidA lidP (headPos pos) sigmaA
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sigmaI' <- rcoerce lidI lidP (headPos pos) sigmaI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder rmap' <- rcoerce lid lidP (headPos pos) rmap
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mor <- 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?
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder {- if setAll (\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),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalThm False,
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)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskiana_FIT_ARG gctx@(gannos,genv,dg) spname nsigI nsigP just_struct
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Fit_view vn fas pos ans) = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lid sigma <- return (getSig nsigP)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Fit_view vn fas pos ans,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (G_morphism lid (ide lid sigma),nsigP))
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? Needs to be implemented
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederextendMorphism :: Pos -> G_sign -> G_sign -> G_sign -> G_morphism
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> Result(G_sign,G_morphism)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederextendMorphism pos gsigma gsigma' gsigmaA mor =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return (gsigmaA,mor) -- ??? needs to be implemented
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
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_GENERICITY :: GlobalContext -> AnyLogic -> Bool -> GENERICITY
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (GENERICITY,ExtGenSig,DGraph)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- zero parameters,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskiana_GENERICITY (_,_,dg) l@(Logic lid) _
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski gen@(Genericity (Params []) (Imported []) pos) =
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (gen,(EmptyNode l,[],G_sign lid (empty_signature lid),EmptyNode l),dg)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- one parameter ...
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskiana_GENERICITY gctx@(gannos,genv,_) l just_struct
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Genericity (Params [asp]) imps pos) = do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (imps',nsigI,dg') <- ana_IMPORTS gctx l just_struct imps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',nsigP,dg'') <- ana_SPEC (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
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskiana_GENERICITY gctx@(gannos,genv,_) l just_struct
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Genericity params imps pos) = do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (imps',nsigI,dg') <- ana_IMPORTS gctx l just_struct imps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (params',nsigPs,dg'') <-
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski ana_PARAMS (gannos,genv,dg') l nsigI just_struct params
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaP <- homogeneousGsigManyUnion (headPos pos) (map getSig nsigPs)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder G_sign lidP sigmaP <- return gsigmaP
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let node_contents = DGNode {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_name = Nothing,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sign = G_sign lidP (empty_signature lidP),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_sens = G_l_sentence lidP [],
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgn_origin = DGFormalParams }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [node] = newNodes 0 dg''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dg''' = insNode (node,node_contents) dg''
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder inslink dg nsig =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case getNode nsig of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Nothing -> dg
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just n -> insEdge (n,node,DGLink {
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_morphism = inclusion (getSig nsig) gsigmaP,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_type = GlobalDef,
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder dgl_origin = DGFormalParams }) dg
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (Genericity params' imps' pos,
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (nsigI,nsigPs,gsigmaP,NodeSig(node,gsigmaP)),
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldl inslink dg''' nsigPs)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_PARAMS :: GlobalContext -> AnyLogic -> NodeSig -> Bool -> PARAMS
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (PARAMS,[NodeSig],DGraph)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_PARAMS gctx@(gannos,genv,dg) l 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
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sps',pars,dg) <- res
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (sp',par,dg') <- ana_SPEC (gannos,genv,dg) nsigI Nothing just_struct sp
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return (sp':sps',par:pars,dg')
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_IMPORTS :: GlobalContext -> AnyLogic -> Bool -> IMPORTED
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (IMPORTED,NodeSig,DGraph)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_IMPORTS gctx l just_struct (Imported asps) = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let sp = Union asps (map (\_ -> nullPos) asps)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (Union asps' _,nsig',dg') <-
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski ana_SPEC 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
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_VIEW_TYPE:: GlobalContext -> AnyLogic -> NodeSig -> Bool -> VIEW_TYPE
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -> Result (VIEW_TYPE,(NodeSig,NodeSig),DGraph)
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiana_VIEW_TYPE gctx@(gannos,genv,_) l parSig just_struct
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (View_type aspSrc aspTar pos) = do
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (spSrc',srcNsig,dg') <-
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski ana_SPEC gctx (EmptyNode l) Nothing just_struct (item aspSrc)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (spTar',tarNsig,dg'') <-
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski ana_SPEC (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!")