93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder{- |

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Module : $Header$

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Cop-D�yright : (c) Till Mossakowski and Uni Bremen 2003-A

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Licence : All rights reserved.

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Maintainer : hets@tzi.de

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Stability : provisional

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Portability : portable

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder

d697755cce49a436e1170e8e158c19f79b0389b8Christian Maeder Analysis of structured specifications

d697755cce49a436e1170e8e158c19f79b0389b8Christian Maeder

d697755cce49a436e1170e8e158c19f79b0389b8Christian Maeder Follows the extended static semantic rules in:

d697755cce49a436e1170e8e158c19f79b0389b8Christian Maeder

e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:

e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder CASL Proof calculus.

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder Available from <http://www.informatik.uni-bremen.de/~till/calculus.ps>

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder To appear in the CASL book.

d697755cce49a436e1170e8e158c19f79b0389b8Christian Maeder

9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder Todo:

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Option: only the structure is analysed => also for symbol maps!

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Check that translations and reductions do not effect local env

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Unions (already in the parser) need unions of logics

e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder = suprema in the lattice of default logic inclusions!

e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder (also needed by closed specs)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Should we use institution independent analysis over the Grothendieck logic?

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder abstract syntax + devgraph would have to be changed to homogeneous case

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder logic translations are symbol maps in the Grothendieck logic

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Problem with this approach: symbol functor goes into rel,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder and induced_from_morphism gets difficult to implement

e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder

9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder Unions need inclusion morphisms. Should these play a special role?

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder At least we need a function delivering the inclusion morphism

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder between two (sub)signatures.

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder In most logics, inclusions could be represented specially, such

9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder that composition for them becomes fast.

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Should we even identify an inclusion subcategory?

9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder Then inclusions are represented by pair of signatures

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (Non-inclusions could be specially displayed in the DG)

9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder

9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder Treatment of translations and reductions along logic translations

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder (see WADT 02 paper).

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Open question:

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder may local env be translated, and even reduced, along logic translations?

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder if yes: how is local env linked to signature of resulting spec?

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder (important e.g. for checking that local env is not being renamed?)

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder does signature+comorphism suffice, such that c(local env)\subseteq sig?

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder if no: this means that only closed specs may be translated

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Revealings wihout translations: just one arrow

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Pushouts: only admissible within one logic?

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Optimizations:

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Union nodes can be extended by a basic spec directly (no new node needed)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Also: free, cofree nodes

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-}

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maedermodule Static.AnalysisStructured (ana_SPEC, ana_GENERICITY, ana_VIEW_TYPE, ana_err)

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maederwhere

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederimport Data.Maybe

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederimport Logic.Logic

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederimport Logic.Comorphism

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Logic.Grothendieck

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Common.Lib.Graph hiding (empty)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Static.DevGraph

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Syntax.AS_Structured

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Common.AS_Annotation

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Common.Result

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Common.Id

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Common.Lib.Set hiding (filter)

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport qualified Common.Lib.Map as Map

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Data.List hiding (union)

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maederimport Common.PrettyPrint

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder-- should be moved to eslewhere!

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder

5d05fc7110bca98e897a726d60dd5f67c4100814Christian MaederlookupNode :: Node -> Graph a b -> a

5d05fc7110bca98e897a726d60dd5f67c4100814Christian MaederlookupNode n dg = lab' $ context n dg

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder

5d05fc7110bca98e897a726d60dd5f67c4100814Christian MaedersetFilter p s = fromList (filter p (toList s))

5d05fc7110bca98e897a726d60dd5f67c4100814Christian MaedersetAny p s = any p (toList s)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedersetAll p s = all p (toList s)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeders1 `disjoint` s2 = s1 `intersection` s2 == empty

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederdomFM m = fromList (Map.keys m)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-- | analyze a SPEC

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder-- Parameters: global context, local environment,

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- the SIMPLE_ID may be a name if the specification shall be named,

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder-- flag: shall only the structure be analysed?

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederana_SPEC :: GlobalContext -> NodeSig -> Maybe SIMPLE_ID -> Bool -> SPEC

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder -> Result (SPEC,NodeSig,DGraph)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederana_SPEC gctx@(gannos,genv,dg) nsig name just_struct sp =

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder case sp of

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Basic_spec (G_basic_spec lid bspec) ->

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder do G_sign lid' sigma' <- return (getSig nsig)

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder sigma <- rcoerce lid' lid nullPos sigma'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (bspec',sigma_local, sigma_complete, ax) <-

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if just_struct

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder then return (bspec,empty_signature lid, empty_signature lid,[])

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder else do b <- maybeToResult nullPos

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder ("no basic analysis for logic "

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder ++language_name lid)

6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder (basic_analysis lid)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder b (bspec,sigma,gannos)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let node_contents = DGNode {

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_name = name,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sign = G_sign lid sigma_local, -- only the delta

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sens = G_l_sentence lid ax,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_origin = DGBasic }

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder [node] = newNodes 0 dg

6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder dg' = insNode (node,node_contents) dg

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder link = DGLink {

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_morphism = undefined, -- where to get it from ???

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_type = GlobalDef,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_origin = DGExtension }

6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder dg'' = case nsig of

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder EmptyNode _ -> dg'

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder NodeSig (n,_) -> insEdge (n,node,link) dg'

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder return (Basic_spec (G_basic_spec lid bspec'),

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder NodeSig (node,G_sign lid sigma_complete),

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dg'')

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Translation asp ren ->

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder do let sp = item asp

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (sp',nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder n' <- maybeToResult nullPos

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder "Internal error: Translation of empty spec" (getNode nsig')

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder mor <- ana_RENAMING dg (getSig nsig') ren

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder -- ??? check that mor is identity on local env

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let gsigma' = codGrothendieck mor

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder -- ??? too simplistic for non-comorphism inter-logic translations

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder G_sign lid' sigma' <- return gsigma'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let node_contents = DGNode {

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_name = name,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_sens = G_l_sentence lid' [],

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_origin = DGTranslation }

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder [node] = newNodes 0 dg'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder link = (n',node,DGLink {

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_morphism = mor,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_type = GlobalDef,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_origin = DGTranslation })

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder return (Translation (replaceAnnoted sp' asp) ren,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder NodeSig(node,gsigma'),

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder insEdge link $

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder insNode (node,node_contents) dg')

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Reduction asp restr ->

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder do let sp = item asp

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder (sp',nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder let gsigma = getSig nsig

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder gsigma' = getSig nsig'

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder n' <- maybeToResult nullPos

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder "Internal error: Reduction of empty spec" (getNode nsig')

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder (hmor,tmor) <- ana_RESTRICTION dg gsigma gsigma' restr

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder -- we treat hiding and revealing differently

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder -- in order to keep the dg as simple as possible

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case tmor of

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder Nothing ->

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder do let gsigma' = domGrothendieck hmor

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

70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder G_sign lid' sigma' <- return gsigma'

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder let node_contents = DGNode {

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_name = name,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_sign = G_sign lid' (empty_signature lid'),

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_sens = G_l_sentence lid' [],

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_origin = DGHiding }

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder [node] = newNodes 0 dg'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder link = (n',node,DGLink {

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder dgl_morphism = hmor,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_type = HidingDef,

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder dgl_origin = DGHiding })

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder return (Reduction (replaceAnnoted sp' asp) restr,

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder NodeSig(node,gsigma'),

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder insEdge link $

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder insNode (node,node_contents) dg')

70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder Just tmor' ->

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder do let gsigma1 = domGrothendieck tmor'

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder gsigma'' = codGrothendieck tmor'

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

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder G_sign lid1 sigma1 <- return gsigma1

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder G_sign lid'' sigma'' <- return gsigma''

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let [node1,node''] = newNodes 1 dg'

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder node_contents1 = DGNode {

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_name = Nothing,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sign = G_sign lid1 (empty_signature lid1),

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sens = G_l_sentence lid1 [],

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_origin = DGRevealing }

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder link1 = (n',node1,DGLink {

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_morphism = hmor,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_type = HidingDef,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_origin = DGRevealing })

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder node_contents'' = DGNode {

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_name = name,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sign = G_sign lid'' (empty_signature lid''),

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sens = G_l_sentence lid'' [],

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_origin = DGRevealTranslation }

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder link'' = (node1,node'',DGLink {

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_morphism = tmor',

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_type = GlobalDef,

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder dgl_origin = DGRevealTranslation })

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder return (Reduction (replaceAnnoted sp' asp) restr,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder NodeSig(node'',gsigma''),

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder insEdge link'' $

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder insNode (node'',node_contents'') $

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder insEdge link1 $

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder insNode (node1,node_contents1) dg')

b26211de8c1e50efbabbb95497e7508c4d852634Christian Maeder

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Union [] pos -> return (sp,nsig,dg)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Union asps pos ->

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder do let sps = map item asps

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (sps',nsigs,dg') <-

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder let ana r sp = do

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder (sps1,nsigs,dg) <- r

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder (sp1,nsig,dg1) <- ana_SPEC gctx nsig Nothing just_struct sp

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder return (sp1:sps1,nsig:nsigs,dg1)

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder in foldl ana (return ([],[],dg)) sps

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder let nsigs' = reverse nsigs

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder nodes = catMaybes (map getNode nsigs')

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder G_sign lid' bigSigma <-

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder homogeneousGsigManyUnion (headPos pos) (map getSig nsigs')

6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder let node_contents = DGNode {

c8bf82bdb27dfa58f7f05045c639c14276be3333Christian Maeder dgn_name = name,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sign = G_sign lid' (empty_signature lid'),

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_sens = G_l_sentence lid' [],

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_origin = DGUnion }

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder [node] = newNodes 0 dg'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder link = DGLink {

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_morphism = undefined, -- ??? how to get it?

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_type = GlobalDef,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_origin = DGUnion }

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder return (let insE dg n = insEdge (n,node,link) dg -- link should vary

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in (Union (map (uncurry replaceAnnoted)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (zip (reverse sps') asps))

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder pos,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder NodeSig(node,G_sign lid' bigSigma),

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder foldl insE (insNode (node,node_contents) dg') nodes))

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Extension [] pos -> return (sp,nsig,dg)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Extension asps pos -> do

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (sps',nsig1,dg1) <- foldl ana (return ([],nsig,dg)) namedSps

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder return (Extension (map (uncurry replaceAnnoted)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (zip (reverse sps') asps))

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder pos,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder nsig1,dg1)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder where

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder namedSps = zip (map (\_ -> Nothing) (tail asps) ++ [name]) (map item asps)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ana res (name,sp) = do

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (sps',nsig,dg) <- res

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (sp1',nsig1,dg1) <- ana_SPEC (gannos,genv,dg) nsig name just_struct sp

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder return (sp1':sps',nsig1,dg1)

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Free_spec asp pos ->

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder do let sp = item asp

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (sp',nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder n' <- maybeToResult nullPos

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder "Internal error: Free spec over empty spec" (getNode nsig')

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let gsigma' = getSig nsig'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder G_sign lid' sigma' <- return gsigma'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let node_contents = DGNode {

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_name = name,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_sens = G_l_sentence lid' [],

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_origin = DGFree }

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder [node] = newNodes 0 dg'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder link = (n',node,DGLink {

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_morphism = undefined, -- ??? inclusion

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_type = FreeDef nsig,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_origin = DGFree })

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder return (Free_spec (replaceAnnoted sp' asp) pos,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder NodeSig(node,gsigma'),

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder insEdge link $

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder insNode (node,node_contents) dg')

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Cofree_spec asp pos ->

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder do let sp = item asp

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder (sp',nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder n' <- maybeToResult nullPos

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder "Internal error: Free spec over empty spec" (getNode nsig')

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let gsigma' = getSig nsig'

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder G_sign lid' sigma' <- return gsigma'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let node_contents = DGNode {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_name = name,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_sens = G_l_sentence lid' [],

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgn_origin = DGCofree }

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder [node] = newNodes 0 dg'

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder link = (n',node,DGLink {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_morphism = undefined, -- ??? inclusion

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_type = CofreeDef nsig,

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder dgl_origin = DGCofree })

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder return (Cofree_spec (replaceAnnoted sp' asp) pos,

215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder NodeSig(node,gsigma'),

215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder insEdge link $

215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder insNode (node,node_contents) dg')

215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder

215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder Local_spec asp asp' pos ->

9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder do let sp = item asp

9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder sp' = item asp'

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder (sp1,nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder (sp1',nsig'',dg'') <- ana_SPEC (gannos,genv,dg') nsig' Nothing just_struct sp'

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder n'' <- maybeToResult nullPos

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder "Internal error: Local spec over empty spec" (getNode nsig'')

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let gsigma = getSig nsig

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder gsigma' = getSig nsig'

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder gsigma'' = getSig nsig''

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder G_sign lid sigma <- return gsigma

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder G_sign lid' sigma' <- return gsigma'

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder G_sign lid'' sigma'' <- return gsigma''

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder sigma1 <- rcoerce lid' lid nullPos sigma'

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder sigma2 <- rcoerce lid'' lid nullPos sigma''

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let sys = sym_of lid sigma

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder sys1 = sym_of lid sigma1

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder sys2 = sym_of lid sigma2

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder mor3 <- cogenerated_sign lid (toList (sys1 `difference` sys)) sigma2

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let sigma3 = dom lid mor3

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder gsigma2 = G_sign lid sigma2

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder gsigma3 = G_sign lid sigma3

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder sys3 = sym_of lid sigma3

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder if sys2 `difference` sys1 `subset` sys3 then return ()

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder else plain_error ()

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder "attempt to hide symbols from the local environment" (headPos pos)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let node_contents = DGNode {

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_name = name,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sign = G_sign lid (empty_signature lid), -- delta is empty

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sens = G_l_sentence lid [],

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_origin = DGLocal }

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder [node] = newNodes 0 dg''

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder link = (n'',node,DGLink {

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_morphism = gEmbed (G_morphism lid mor3),

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_type = HidingDef,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_origin = DGLocal })

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder return (Local_spec (replaceAnnoted sp1 asp)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder (replaceAnnoted sp1' asp')

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder pos,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder NodeSig(node,gsigma3),

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder insEdge link $

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder insNode (node,node_contents) dg'')

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Closed_spec asp pos ->

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder do let sp = item asp

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder l = getLogic nsig

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder (sp',nsig',dg') <- ana_SPEC gctx (EmptyNode l) Nothing just_struct sp

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder n' <- maybeToResult nullPos

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder "Internal error: Closed spec over empty spec" (getNode nsig')

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let gsigma = getSig nsig

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder gsigma' = getSig nsig'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder gsigma'' <- homogeneousGsigUnion (headPos pos) gsigma gsigma'

3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder -- also allow different logics???

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder G_sign lid'' sigma'' <- return gsigma''

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder let [node] = newNodes 0 dg'

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder node_contents = DGNode {

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder dgn_name = name,

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder dgn_sign = G_sign lid'' (empty_signature lid''),

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder dgn_sens = G_l_sentence lid'' [],

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_origin = DGClosed }

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder link1 = (n',node,DGLink {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_morphism = inclusion gsigma' gsigma'',

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_type = GlobalDef,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_origin = DGClosed })

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder link2 = DGLink {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_morphism = inclusion gsigma' gsigma'',

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_type = GlobalDef,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_origin = DGClosedLenv }

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder insLink2 = case (getNode nsig) of

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> id

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Just n -> insEdge (n,node,link2)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return (Closed_spec (replaceAnnoted sp' asp) pos,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder NodeSig(node,gsigma''),

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder insLink2 $

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder insEdge link1 $

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder insNode (node,node_contents) dg')

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Group asp pos -> do

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (sp',nsig',dg') <- ana_SPEC gctx nsig name just_struct (item asp)

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

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Spec_inst spname afitargs pos ->

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder case Map.lookup spname genv of

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> plain_error (sp,nsig,dg)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ("Specification "++ showPretty spname " not found") (headPos pos)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Just (ViewEntry _) ->

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder plain_error (sp,nsig,dg)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (showPretty spname " is a view, not a specification") (headPos pos)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Just (ArchEntry _) ->

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder plain_error (sp,nsig,dg)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (showPretty spname

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder " is an architectural, not a structured specification") (headPos pos)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Just (UnitEntry _) ->

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder plain_error (sp,nsig,dg)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (showPretty spname

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder " is a unit specification, not a structured specification") (headPos pos)

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Just (SpecEntry gs@(imps,params,gSigmaP,body)) ->

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder case (\x y -> (x,x-y)) (length afitargs) (length params) of

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder -- the case without parameters leads to a simpler dg

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (0,0) -> do

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder let gsigmaB = getSig body

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder gsigma <- homogeneousGsigUnion (headPos pos) (getSig nsig) gsigmaB

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder G_sign lid sigma <- return gsigma

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder nB <- maybeToResult (headPos pos)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder "Internal error: empty body spec" (getNode body)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder case (getNode nsig) of

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder -- the case with empty local env leads to an even simpler dg

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Nothing -> case name of

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder -- if the node shall not be named, just return the body

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Nothing -> return (sp,body,dg)

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder -- if the node shall be named, we need to create a new one

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder Just _ ->

5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder let [node] = newNodes 0 dg

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder node_contents = DGNode {

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder dgn_name = name,

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder dgn_sign = G_sign lid (empty_signature lid),

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_sens = G_l_sentence lid [],

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgn_origin = DGSpecInst spname}

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder link = (nB,node,DGLink {

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_morphism = inclusion gsigmaB gsigma,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_type = GlobalDef,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder dgl_origin = DGSpecInst spname})

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder in return (sp,

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder NodeSig(node,gsigma),

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder insEdge link $

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder insNode (node,node_contents) dg)

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder -- the case with nonempty local env

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Just n ->

ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder let [node] = newNodes 0 dg

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder node_contents = DGNode {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_name = name,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_sign = G_sign lid (empty_signature lid),

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_sens = G_l_sentence lid [],

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_origin = DGSpecInst spname}

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder link1 = (n,node,DGLink {

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder dgl_morphism = inclusion (getSig nsig) gsigma,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_type = GlobalDef,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_origin = DGSpecInst spname})

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder link2 = (nB,node,DGLink {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_morphism = inclusion gsigmaB gsigma,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_type = GlobalDef,

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder dgl_origin = DGSpecInst spname})

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder in return (sp,

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder NodeSig(node,gsigma),

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder insEdge link1 $

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder insEdge link2 $

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder insNode (node,node_contents) dg)

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder -- now the general case: with parameters

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (_,0) -> do

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let fitargs = map item afitargs

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (fitargs',dg',args) <-

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder foldl ana (return ([],dg,[])) (zip params fitargs)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let actualargs = reverse args

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (gsigma',mor_f) <- apply_GS (headPos pos) gs actualargs

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder G_sign lid' sigma' <- return gsigma'

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder gsigmaRes <- homogeneousGsigUnion (headPos pos) (getSig nsig) gsigma'

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder nB <- maybeToResult (headPos pos)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder "Internal error: empty body spec" (getNode body)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let [node] = newNodes 0 dg'

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder node_contents = DGNode {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_name = name,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'),

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_sens = G_l_sentence lid' [],

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgn_origin = DGSpecInst spname}

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder link1 = DGLink {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_morphism = inclusion (getSig nsig) gsigma',

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_type = GlobalDef,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_origin = DGSpecInst spname}

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder insLink1 = case (getNode nsig) of

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Nothing -> id

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Just n -> insEdge (n,node,link1)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder link2 = (nB,node,DGLink {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_morphism = inclusion (getSig body) gsigma',

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_type = GlobalDef,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_origin = DGSpecInst spname})

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder parLinks = catMaybes (map (parLink node) actualargs)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return (Spec_inst spname

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (map (uncurry replaceAnnoted)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (zip (reverse fitargs') afitargs))

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder pos,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder NodeSig(node,gsigma'),

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder foldr insEdge

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (insLink1 $

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder insEdge link2 $

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder insNode (node,node_contents) dg')

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder parLinks)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder where

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ana res (nsig,fa) = do

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (fas',dg,args) <- res

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (fa',dg',arg) <- ana_FIT_ARG (gannos,genv,dg)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder spname imps nsig just_struct fa

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return (fa':fas',dg',arg:args)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder parLink node (mor_i,nsigA_i) = do

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder nA_i <- getNode nsigA_i

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let link = DGLink {

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_morphism = gEmbed mor_i,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_type = GlobalDef,

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder dgl_origin = DGClosed }

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return (nA_i,node,link)

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder -- finally the case with conflicting numbers of formal and actual parameters

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder otherwise ->

14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder plain_error (sp,nsig,dg)

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (showPretty spname " expects "++show (length params)++" arguments"

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++" but was given "++show (length afitargs)) (headPos pos)

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Qualified_spec logname asp pos ->

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder ana_err "logic qualified specs"

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder{-

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Data (Logic lid1) asp1 asp2 pos ->

190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do let sp1 = item asp1

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder sp2 = item asp2

70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder l = getLogic nsig

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder (sp1',nsig1,dg1) <-

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder ana_SPEC gctx (EmptyNode lid1) Nothing just_struct sp1

93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder (sp2'nsig2,dg2) <-

d697755cce49a436e1170e8e158c19f79b0389b8Christian Maeder ana_SPEC (gannos,genv,dg1) nsig1 Nothing just_struct sp2

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder n' <- maybeToResult nullPos

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder "Internal error: Free spec over empty spec" (getNode nsig')

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder let gsigma' = getSig nsig'

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder G_sign lid' sigma' <- return gsigma'

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder let node_contents = DGNode {

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder dgn_name = name,

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder dgn_sens = G_l_sentence lid' [],

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder dgn_origin = DGFree }

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [node] = newNodes 0 dg'

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder link = (n',node,DGLink {

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder dgl_morphism = undefined, -- ??? inclusion

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder dgl_type = FreeDef nsig,

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder dgl_origin = DGFree })

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder return (Data (Logic lid1)

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder (replaceAnnoted sp1' asp1)

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder (replaceAnnoted sp2' asp2)

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder pos,

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder NodeSig(node,gsigma'),

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder insEdge link $

3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder insNode (node,node_contents) dg')

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-}

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- analysis of renamings

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_ren1 dg (GMorphism r sigma mor)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (G_symb_map (G_symb_map_items_list lid sis),pos) = do

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let lid1 = sourceLogic r

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder lid2 = targetLogic r

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder sis1 <- rcoerce lid2 lid pos sis

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder rmap <- stat_symb_map_items lid2 sis1

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder mor1 <- induced_from_morphism lid2 rmap (cod lid2 mor)

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder mor2 <- maybeToResult pos

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder "renaming: signature morphism composition failed"

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (comp lid2 mor mor1)

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder return (GMorphism r sigma mor2)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_ren1 dg mor (G_logic_translation (Logic_code tok src tar pos1),pos2) =

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder fatal_error "no analysis of logic translations yet" pos2

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_ren :: DGraph -> Result GMorphism -> (G_mapping,Pos) -> Result GMorphism

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_ren dg mor_res ren =

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder do mor <- mor_res

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder ana_ren1 dg mor ren

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_RENAMING :: DGraph -> G_sign -> RENAMING -> Result GMorphism

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_RENAMING dg gSigma (Renaming ren pos) =

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder foldl (ana_ren dg) (return (ideGrothendieck gSigma)) ren'

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder where

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder ren' = zip ren (tail (pos ++ repeat nullPos))

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- analysis of restrictions

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_restr1 dg (G_sign lid sigma) (GMorphism cid sigma1 mor)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (G_symb_list (G_symb_items_list lid' sis'),pos) = do

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let lid1 = sourceLogic cid

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder lid2 = targetLogic cid

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder sis1 <- rcoerce lid1 lid' pos sis'

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder rsys <- stat_symb_items lid1 sis1

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let sys = sym_of lid1 sigma1

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let sys' = filter (\sy -> any (\rsy -> matches lid1 sy rsy) rsys)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (toList sys)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- if sys' `disjoint` () then return ()

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- else plain_error () "attempt to hide symbols from the local environment" pos

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder mor1 <- cogenerated_sign lid1 sys' sigma1

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder mor1' <- maybeToResult pos

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder ("restriction: could not map morphism along" ++ language_name cid)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (map_morphism cid mor1)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder mor2 <- maybeToResult pos

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder "restriction: signature morphism composition failed"

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (comp lid2 mor1' mor)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder return (GMorphism cid (dom lid1 mor1) mor2)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_restr1 dg gSigma mor

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (G_logic_projection (Logic_code tok src tar pos1),pos2) =

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder fatal_error "no analysis of logic projections yet" pos2

fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maederana_restr :: DGraph -> G_sign -> Result GMorphism -> (G_hiding,Pos)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder -> Result GMorphism

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_restr dg gSigma mor_res restr =

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder do mor <- mor_res

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder ana_restr1 dg gSigma mor restr

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maederana_RESTRICTION :: DGraph -> G_sign -> G_sign -> RESTRICTION

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder -> Result (GMorphism, Maybe GMorphism)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maederana_RESTRICTION dg gSigma gSigma' (Hidden restr pos) =

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder do mor <- foldl (ana_restr dg gSigma)

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (return (ideGrothendieck gSigma'))

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder restr'

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder return (mor,Nothing)

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder where

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder restr' = zip restr (tail (pos ++ repeat nullPos))

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maederana_RESTRICTION dg gSigma@(G_sign lid sigma) gSigma'@(G_sign lid' sigma')

1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (Revealed (G_symb_map_items_list lid1 sis) pos) =

9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder do let sys = sym_of lid sigma

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder sys' = sym_of lid' sigma'

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder sis' <- rcoerce lid1 lid' (headPos pos) sis

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder rmap <- stat_symb_map_items lid' sis'

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let sys'' =

e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder fromList

[sy | sy <- toList sys', rsy <- Map.keys rmap, matches lid' sy rsy]

sys1 <- rcoerce lid lid' (headPos pos) sys

-- ??? this is too simple in case that local env is translated

-- to a different logic

if sys1 `disjoint` sys'' then return ()

else plain_error () "attempt to hide symbols from the local environment" (headPos pos)

mor1 <- generated_sign lid' (toList (sys1 `union` sys'')) sigma'

mor2 <- induced_from_morphism lid' rmap (dom lid' mor1)

return (gEmbed (G_morphism lid' mor1),

Just (gEmbed (G_morphism lid' mor2)))

ana_FIT_ARG gctx@(gannos,genv,dg) spname nsigI nsigP just_struct

(Fit_spec asp gsis pos) = do

nP <- maybeToResult nullPos

"Internal error: empty parameter spec" (getNode nsigP)

(sp',nsigA,dg') <- ana_SPEC gctx nsigI Nothing just_struct (item asp)

nA <- maybeToResult nullPos

"Internal error: empty argument spec" (getNode nsigA)

let gsigmaP = getSig nsigP

gsigmaA = getSig nsigA

gsigmaI = getSig nsigI

G_sign lidP sigmaP <- return gsigmaP

G_sign lidA sigmaA <- return gsigmaA

G_sign lidI sigmaI <- return gsigmaI

G_symb_map_items_list lid sis <- return gsis

rmap <- stat_symb_map_items lid sis

sigmaA' <- rcoerce lidA lidP (headPos pos) sigmaA

sigmaI' <- rcoerce lidI lidP (headPos pos) sigmaI

rmap' <- rcoerce lid lidP (headPos pos) rmap

mor <- induced_from_to_morphism lidP rmap' sigmaP sigmaA'

let symI = sym_of lidP sigmaI'

symmap_mor = symmap_of lidP mor

-- are symbols of the imports left untouched?

{- if setAll (\sy -> lookupFM symmap_mor sy == Just sy) symI

then return ()

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

-} -- ??? does not work

-- ??? also output some symbol that is affected

let link = (nP,nA,DGLink {

dgl_morphism = gEmbed (G_morphism lidP mor),

dgl_type = GlobalThm False,

dgl_origin = DGSpecInst spname})

return (Fit_spec (replaceAnnoted sp' asp) gsis pos,

insEdge link dg',

(G_morphism lidP mor,nsigA)

)

ana_FIT_ARG gctx@(gannos,genv,dg) spname nsigI nsigP just_struct

(Fit_view vn fas pos ans) = do

G_sign lid sigma <- return (getSig nsigP)

return (Fit_view vn fas pos ans,

dg,

(G_morphism lid (ide lid sigma),nsigP))

-- ??? Needs to be implemented

extendMorphism :: Pos -> G_sign -> G_sign -> G_sign -> G_morphism

-> Result(G_sign,G_morphism)

extendMorphism pos gsigma gsigma' gsigmaA mor =

return (gsigmaA,mor) -- ??? needs to be implemented

apply_GS :: Pos -> ExtGenSig -> [(G_morphism,NodeSig)] -> Result(G_sign,G_morphism)

apply_GS pos (nsigI,params,gsigmaP,nsigB) args = do

let mor_i = map fst args

gsigmaA_i = map (getSig . snd) args

gsigmaB = getSig nsigB

gsigmaI = getSig nsigI

G_sign lidI sigmaI <- return gsigmaI

let idI = ide lidI sigmaI

gsigmaA <- homogeneousGsigManyUnion pos gsigmaA_i

mor_f <- homogeneousMorManyUnion pos (G_morphism lidI idI:mor_i)

extendMorphism pos gsigmaP gsigmaB gsigmaA mor_f

-- | analyze a GENERICITY

-- Parameters: global context, current logic, just-structure-flag, GENERICITY

ana_GENERICITY :: GlobalContext -> AnyLogic -> Bool -> GENERICITY

-> Result (GENERICITY,ExtGenSig,DGraph)

-- zero parameters,

ana_GENERICITY (_,_,dg) l@(Logic lid) _

gen@(Genericity (Params []) (Imported []) pos) =

return (gen,(EmptyNode l,[],G_sign lid (empty_signature lid),EmptyNode l),dg)

-- one parameter ...

ana_GENERICITY gctx@(gannos,genv,_) l just_struct

(Genericity (Params [asp]) imps pos) = do

(imps',nsigI,dg') <- ana_IMPORTS gctx l just_struct imps

(sp',nsigP,dg'') <- ana_SPEC (gannos,genv,dg') nsigI Nothing just_struct (item asp)

return (Genericity (Params [replaceAnnoted sp' asp]) imps' pos,

(nsigI,[nsigP],getSig nsigP,nsigP),

dg'')

-- ... and more parameters

ana_GENERICITY gctx@(gannos,genv,_) l just_struct

(Genericity params imps pos) = do

(imps',nsigI,dg') <- ana_IMPORTS gctx l just_struct imps

(params',nsigPs,dg'') <-

ana_PARAMS (gannos,genv,dg') l nsigI just_struct params

gsigmaP <- homogeneousGsigManyUnion (headPos pos) (map getSig nsigPs)

G_sign lidP sigmaP <- return gsigmaP

let node_contents = DGNode {

dgn_name = Nothing,

dgn_sign = G_sign lidP (empty_signature lidP),

dgn_sens = G_l_sentence lidP [],

dgn_origin = DGFormalParams }

[node] = newNodes 0 dg''

dg''' = insNode (node,node_contents) dg''

inslink dg nsig =

case getNode nsig of

Nothing -> dg

Just n -> insEdge (n,node,DGLink {

dgl_morphism = inclusion (getSig nsig) gsigmaP,

dgl_type = GlobalDef,

dgl_origin = DGFormalParams }) dg

return (Genericity params' imps' pos,

(nsigI,nsigPs,gsigmaP,NodeSig(node,gsigmaP)),

foldl inslink dg''' nsigPs)

ana_PARAMS :: GlobalContext -> AnyLogic -> NodeSig -> Bool -> PARAMS

-> Result (PARAMS,[NodeSig],DGraph)

ana_PARAMS gctx@(gannos,genv,dg) l nsigI just_struct (Params asps) = do

(sps',pars,dg') <- foldl ana (return ([],[],dg)) (map item asps)

return (Params (map (uncurry replaceAnnoted)

(zip (reverse sps') asps)),

reverse pars,

dg')

where

ana res sp = do

(sps',pars,dg) <- res

(sp',par,dg') <- ana_SPEC (gannos,genv,dg) nsigI Nothing just_struct sp

return (sp':sps',par:pars,dg')

ana_IMPORTS :: GlobalContext -> AnyLogic -> Bool -> IMPORTED

-> Result (IMPORTED,NodeSig,DGraph)

ana_IMPORTS gctx l just_struct (Imported asps) = do

let sp = Union asps (map (\_ -> nullPos) asps)

(Union asps' _,nsig',dg') <-

ana_SPEC gctx (EmptyNode l) Nothing just_struct sp

return (Imported asps',nsig',dg')

-- ??? emptyExplicit stuff needs to be added here

-- | analyze a VIEW_TYPE

-- The first three arguments give the global context

-- The AnyLogic is the current logic

-- The NodeSig is the signature of the parameter of the view

-- flag, whether just the structure shall be analysed

ana_VIEW_TYPE:: GlobalContext -> AnyLogic -> NodeSig -> Bool -> VIEW_TYPE

-> Result (VIEW_TYPE,(NodeSig,NodeSig),DGraph)

ana_VIEW_TYPE gctx@(gannos,genv,_) l parSig just_struct

(View_type aspSrc aspTar pos) = do

(spSrc',srcNsig,dg') <-

ana_SPEC gctx (EmptyNode l) Nothing just_struct (item aspSrc)

(spTar',tarNsig,dg'') <-

ana_SPEC (gannos,genv,dg') parSig Nothing just_struct (item aspTar)

return (View_type (replaceAnnoted spSrc' aspSrc)

(replaceAnnoted spTar' aspTar)

pos,

(srcNsig,tarNsig),

dg'')

-- | Auxiliary function for not yet implemented features

ana_err :: String -> a

ana_err fname =

error ("*** Analysis of " ++ fname ++ " is not yet implemented!")