AnalysisStructured.hs revision 7bf4436b6f9987b070033a323757b206c898c1be
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder{- |
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski Module : $Header$
2725abe920f91de62ae5c0b7230c1627cccf5fabChristian Maeder Copyright : (c) Till Mossakowski and Uni Bremen 2003-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder Maintainer : till@tzi.de
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Stability : provisional
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Portability : non-portable
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederAnalysis of structured specifications
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Follows the verfication semantic rules in Chap. IV:4.7
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder of the CASL Reference Manual.
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder-}
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder{-
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder Todo:
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder analysis of basic specs: use union of sigs
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder analysis of instantiations: if necessary, translate body along inclusion comorphism
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder Improve efficiency by storing local signature fragments only
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder Name views in devgraphs?
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder spec <name> not found: line number!
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder Issue warning for unions of non-disjoint signatures
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder (and offer tool for renaming?)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder Check that translations and reductions do not effect local env
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder (Implement new semantics for revealing here)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder Should we use institution independent analysis over the Grothendieck logic?
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder abstract syntax + devgraph would have to be changed to homogeneous case
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder logic translations are symbol maps in the Grothendieck logic
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder Problem with this approach: symbol functor goes into rel,
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder and induced_from_morphism gets difficult to implement
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder Unions need inclusion morphisms. Should these play a special role?
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder At least we need a function delivering the inclusion morphism
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder between two (sub)signatures.
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder In most logics, inclusions could be represented specially, such
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder that composition for them becomes fast.
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Should we even identify an inclusion subcategory?
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Then inclusions are represented by pair of signatures
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (Non-inclusions could be specially displayed in the DG)
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder No optimization of heterogeneous unions!
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder (or use heterogeneous compInclusion in Proofs/Proof.hs)
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder (or perhaps abandon optimized unions at all and
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder replace compHomInclusion with comp Grothendieck? is this more efficient?)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder Treatment of translations and reductions along logic translations
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (see WADT 02 paper).
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Open question:
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder may local env be translated, and even reduced, along logic translations?
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder if yes: how is local env linked to signature of resulting spec?
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (important e.g. for checking that local env is not being renamed?)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder does signature+comorphism suffice, such that c(local env)\subseteq sig?
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder if no: this means that only closed specs may be translated
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder Revealings without translations: just one arrow
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Pushouts: only admissible within one logic?
2353f65833a3da763392f771223250cd50b8d873Christian Maeder Instantiations with formal parameter: add no new internal nodes
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder call extend_morphism
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
ea38cad7e4f09060750da5d0b8ebc426628c4d88Christian Maeder Optimizations:
cb2044812811d66efe038d914966e04290be93faChristian Maeder Union nodes can be extended by a basic spec directly (no new node needed)
966519955f5f7111abac20118563132b9dd41165Christian Maeder no new nodes for trivial translations
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder use foldM
d81905a5b924415c524d702df26204683c82c12eChristian Maeder Also: free, cofree nodes
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Basic specs: if local env node is otherwise unused, overwrite it with
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder local sig+axioms
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Ensure that just_struct option leads to disabling of various dg operations
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (show sig, show mor, proving)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
cb2044812811d66efe038d914966e04290be93faChristian Maeder local: better error message for the following
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederspec GenCardinality [sort Subject,Object;
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder pred predicate : Subject * Object] =
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder%%Nat then
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maederlocal {
6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu Set [sort Object fit sort Elem |-> Object]
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu reveal Set[Object], #__, __eps__,
b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanu Nat,0,1,2,3,4,5,6,7,8,9,__@@__,__>=__,__<=__
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu then
966519955f5f7111abac20118563132b9dd41165Christian Maeder op toSet : Subject -> Set [Object]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder forall x : Subject; y : Object
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder . predicate (x,y) <=> y eps toSet(x)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder } within
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder pred minCardinality(s: Subject;n: Nat) <=>
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder # toSet(s) >= n;
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder maxCardinality(s: Subject;n: Nat) <=>
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz # toSet(s) <= n;
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder cardinality(s: Subject;n: Nat) <=>
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder # toSet(s) = n
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder%%} hide Pos,toSet,Set[Object],#__,__eps__,__<=__,__>=__
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maederend
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder-}
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian Maeder
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder
a9e804dbec424ec36e34bab955cbe90edac5baa6Christian Maedermodule Static.AnalysisStructured (ana_SPEC, ana_GENERICITY,
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz ana_VIEW_TYPE, ana_err, isStructured,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ana_RENAMING, ana_RESTRICTION,
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke homogenizeGM, extendMorphism)
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Lueckewhere
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettichimport Driver.Options
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettichimport Data.Maybe
2353f65833a3da763392f771223250cd50b8d873Christian Maederimport Logic.Logic
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Logic.Coerce
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Logic.Comorphism
2353f65833a3da763392f771223250cd50b8d873Christian Maederimport Logic.Grothendieck
2353f65833a3da763392f771223250cd50b8d873Christian Maederimport Static.DevGraph
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Syntax.AS_Structured
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.AS_Annotation
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.Result
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.Id
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Data.Graph.Inductive.Graph
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport qualified Common.Lib.Set as Set
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport qualified Common.Lib.Map as Map
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport qualified Common.Lib.Rel as Rel(image, setInsert)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Data.List hiding (union)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Common.PrettyPrint
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederimport Common.Lib.Pretty
cb2044812811d66efe038d914966e04290be93faChristian Maederimport Control.Monad
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederinsEdgeNub :: LEdge DGLinkLab -> DGraph -> DGraph
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederinsEdgeNub (v, w, l) g =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder if (l, w) `elem` s then g
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder else (p, v, l', (l, w) : s) & g'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder where (Just (p, _, l', s), g') = match v g
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | analyze a SPEC
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- Parameters: global context, local environment,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- the SIMPLE_ID may be a name if the specification shall be named,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- options: here we need the info: shall only the structure be analysed?
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederana_SPEC :: LogicGraph -> GlobalContext -> MaybeNode -> NODE_NAME ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder HetcatsOpts -> SPEC -> Result (SPEC,NodeSig,DGraph)
966519955f5f7111abac20118563132b9dd41165Christian Maeder
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maederana_SPEC lg gctx@(gannos,genv,dg) nsig name opts sp =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case sp of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Basic_spec (G_basic_spec lid bspec) ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do G_sign lid' sigma' <- return (getMaybeSig nsig)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder sigma <- coerceSign lid' lid "Analysis of basic spec" sigma'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (bspec', _sigma_local, sigma_complete, ax) <-
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder if isStructured opts
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder then return (bspec,empty_signature lid, empty_signature lid,[])
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder else do b <- maybeToMonad
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ("no basic analysis for logic "
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++language_name lid)
cb2044812811d66efe038d914966e04290be93faChristian Maeder (basic_analysis lid)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder b (bspec,sigma,gannos)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder incl <- ginclusion lg
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (G_sign lid sigma) (G_sign lid sigma_complete)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let node_contents = DGNode {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_name = name,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_theory = G_theory lid sigma_complete $ toThSens ax,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- no, not only the delta
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_nf = Nothing,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_sigma = Nothing,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_origin = DGBasic }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder node = getNewNode dg
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg' = insNode (node,node_contents) dg
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder link = DGLink {
966519955f5f7111abac20118563132b9dd41165Christian Maeder dgl_morphism = incl,
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder dgl_type = GlobalDef,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_origin = DGExtension }
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dg'' = case nsig of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder EmptyNode _ -> dg'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n,node,link) dg'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return (Basic_spec (G_basic_spec lid bspec'),
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder NodeSig node $ G_sign lid sigma_complete,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg'')
cb2044812811d66efe038d914966e04290be93faChristian Maeder
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder Translation asp ren ->
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder do let sp1 = item asp
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (sp1', NodeSig n' gsigma, dg') <-
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder mor <- ana_RENAMING lg gsigma opts ren
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- ??? check that mor is identity on local env
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let gsigma' = cod Grothendieck mor
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder -- ??? too simplistic for non-comorphism inter-logic translations
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder G_sign lid' gsig <- return gsigma'
966519955f5f7111abac20118563132b9dd41165Christian Maeder let node_contents = DGNode {
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder dgn_name = name,
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder dgn_theory = G_theory lid' gsig noSens,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_nf = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGTranslation }
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder node = getNewNode dg'
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder link = (n',node,DGLink {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_morphism = mor,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_type = GlobalDef,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_origin = DGTranslation })
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return (Translation (replaceAnnoted sp1' asp) ren,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder NodeSig node gsigma',
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder insEdgeNub link $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder insNode (node,node_contents) dg')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
966519955f5f7111abac20118563132b9dd41165Christian Maeder Reduction asp restr ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do let sp1 = item asp
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (sp1', NodeSig n' gsigma',dg') <-
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let gsigma = getMaybeSig nsig
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (hmor,tmor) <- ana_RESTRICTION dg gsigma gsigma' opts restr
cb2044812811d66efe038d914966e04290be93faChristian Maeder -- we treat hiding and revealing differently
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- in order to keep the dg as simple as possible
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case tmor of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do let gsigma'' = dom Grothendieck hmor
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder G_sign lid' gsig <- return gsigma''
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let node_contents = DGNode {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_name = name,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_theory = G_theory lid' gsig noSens,
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder dgn_nf = Nothing,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGHiding }
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder node = getNewNode dg'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder link = (n',node,DGLink {
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder dgl_morphism = hmor,
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder dgl_type = HidingDef,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_origin = DGHiding })
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu return (Reduction (replaceAnnoted sp1' asp) restr,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder NodeSig node gsigma'',
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder insEdgeNub link $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder insNode (node,node_contents) dg')
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Just tmor' -> do
cb2044812811d66efe038d914966e04290be93faChristian Maeder let gsigma1 = dom Grothendieck tmor'
d81905a5b924415c524d702df26204683c82c12eChristian Maeder gsigma'' = cod Grothendieck tmor'
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder G_sign lid1 gsig <- return gsigma1
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder G_sign lid'' gsig'' <- return gsigma''
966519955f5f7111abac20118563132b9dd41165Christian Maeder -- the case with identity translation leads to a simpler dg
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder if tmor' == ide Grothendieck (dom Grothendieck tmor')
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder then do
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder let node1 = getNewNode dg'
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder node_contents1 = DGNode {
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder dgn_name = name,
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder dgn_theory = G_theory lid1 gsig noSens,
5b5f3190cc8d51a7942dda33a1ec45345cca5028Thiemo Wiedemeyer dgn_nf = Nothing,
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder dgn_sigma = Nothing,
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder dgn_origin = DGRevealing }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder link1 = (n',node1,DGLink {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_morphism = hmor,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_type = HidingDef,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGRevealing })
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return (Reduction (replaceAnnoted sp1' asp) restr,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder NodeSig node1 gsigma1,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder insEdgeNub link1 $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder insNode (node1,node_contents1) dg')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder else do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let [node1,node''] = newNodes 2 dg'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder node_contents1 = DGNode {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_name = extName "T" name,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_theory = G_theory lid1 gsig noSens,
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer dgn_nf = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGRevealing }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder link1 = (n',node1,DGLink {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_morphism = hmor,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_type = HidingDef,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGRevealing })
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder node_contents'' = DGNode {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_name = name,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_theory = G_theory lid'' gsig'' noSens,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_nf = Nothing,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_sigma = Nothing,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_origin = DGRevealTranslation }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder link'' = (node1,node'',DGLink {
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder dgl_morphism = tmor',
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_type = GlobalDef,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_origin = DGRevealTranslation })
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return (Reduction (replaceAnnoted sp1' asp) restr,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder NodeSig node'' gsigma'',
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder insEdgeNub link'' $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder insNode (node'',node_contents'') $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder insEdgeNub link1 $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder insNode (node1,node_contents1) dg')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Union [] pos -> adjustPos pos $ fail $ "empty union"
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian Maeder Union asps pos ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do let sps = map item asps
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder (sps',nsigs,dg',_) <-
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let ana r sp' = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (sps1,nsigs,dg',n) <- r
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (sp1,nsig',dg1) <- ana_SPEC lg (gannos,genv,dg')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder nsig n opts sp'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return (sp1:sps1,nsig':nsigs,dg1,inc n)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in foldl ana (return ([],[],dg,extName "U" name)) sps
2353f65833a3da763392f771223250cd50b8d873Christian Maeder let nsigs' = reverse nsigs
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder adj = adjustPos pos
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder gbigSigma <- adj $ gsigManyUnion lg (map getSig nsigs')
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder G_sign lid' gsig <- return gbigSigma
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder let node_contents = DGNode {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_name = name,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_theory = G_theory lid' gsig noSens,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_nf = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGUnion }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder node = getNewNode dg'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder insE dgres (NodeSig n gsigma) = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg1 <- dgres
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder incl <- adj $ ginclusion lg gsigma gbigSigma
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let link = DGLink {
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder dgl_morphism = incl,
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder dgl_type = GlobalDef,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGUnion }
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return (insEdgeNub (n,node,link) dg1)
818b228955ef40dd5a253bd942dd6ab8779ed713Christian Maeder dg'' <- foldl insE (return (insNode (node,node_contents) dg')) nsigs'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return (Union (map (uncurry replaceAnnoted)
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian Maeder (zip (reverse sps') asps))
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich pos,
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich NodeSig node gbigSigma,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg'')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian Maeder Extension asps pos -> do
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich (sps',nsig1',dg1) <- foldl ana (return ([],nsig,dg)) namedSps
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich case nsig1' of
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian Maeder EmptyNode _ -> fail "empty extension"
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich JustNode nsig1 -> return (Extension (map (uncurry replaceAnnoted)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (zip (reverse sps') asps))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder pos, nsig1,dg1)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder namedSps = zip (reverse (name: tail (take (length asps)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (iterate inc (extName "E" name)))))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder asps
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian Maeder ana res (name',asp') = do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (sps', nsig', dg') <- res
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz (sp1', nsig1@(NodeSig n1 sig1), dg1) <-
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ana_SPEC lg (gannos,genv,dg') nsig' name' opts (item asp')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- insert theorem link for semantic annotations
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- take the first semantic annotation
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let anno = find isSemanticAnno $ l_annos asp'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- is the extension going between real nodes?
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dg2 <- case (anno, nsig') of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (Just anno0@(Semantic_anno anno1 _), JustNode (NodeSig n' sig')) -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- any other semantic annotation? that's an error
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder when (any (\an -> isSemanticAnno an && an/=anno0) $ l_annos asp')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (pplain_error () (ptext "Conflicting semantic annotations")
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder pos)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- %implied should not occur here
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder when (anno1==SA_implied)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (pplain_error () (ptext
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian Maeder "Annotation %implied should come after a BASIC-ITEM")
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder pos)
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz if anno1==SA_implies then do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder when (not (is_subgsign sig1 sig')) (pplain_error ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (ptext "Signature must not be extended in presence of %implies")
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder pos)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- insert a theorem link according to p. 319 of the CASL Reference Manual
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return $ insEdgeNub (n1,n',DGLink {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_morphism = ide Grothendieck sig1,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_type = GlobalThm LeftOpen None LeftOpen,
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder dgl_origin = DGExtension }) dg1
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder else do
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian Maeder let anno2 = case anno1 of
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz SA_cons -> Cons
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz SA_def -> Def
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder SA_mono -> Mono
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder _ -> error "Static.AnalysisStructured: this cannot happen"
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder -- insert a theorem link according to p. 319 of the CASL Reference Manual
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder -- the theorem link is trivally proved by the parallel definition link,
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder -- but for clarity, we leave it open here
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder -- the interesting open proof obligation is anno2, of course
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder incl <- ginclusion lg sig' sig1
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich return $ insEdgeNub (n',n1,DGLink {
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke dgl_morphism = incl,
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder dgl_type = GlobalThm LeftOpen anno2 LeftOpen,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGExtension }) dg1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> return dg1
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder return (sp1':sps', JustNode nsig1, dg2)
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder Free_spec asp poss ->
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder do let sp1 = item asp
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder (sp', NodeSig n' gsigma'@(G_sign lid' gsig), dg') <-
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let pos = poss
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let node_contents = DGNode {
2353f65833a3da763392f771223250cd50b8d873Christian Maeder dgn_name = name,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_theory = G_theory lid' gsig noSens, -- delta is empty
f6bb0076b79286b0251c1b2745ed8019b6c80252Christian Maeder dgn_nf = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGFree }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder node = getNewNode dg'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder link = (n',node,DGLink {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_morphism = incl,
f6bb0076b79286b0251c1b2745ed8019b6c80252Christian Maeder dgl_type = FreeDef nsig,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGFree })
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return (Free_spec (replaceAnnoted sp' asp) poss,
f6bb0076b79286b0251c1b2745ed8019b6c80252Christian Maeder NodeSig node gsigma',
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder insEdgeNub link $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder insNode (node,node_contents) dg')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Cofree_spec asp poss ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do let sp1 = item asp
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (sp', NodeSig n' gsigma'@(G_sign lid' gsig), dg') <-
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ana_SPEC lg gctx nsig (inc name) opts sp1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let pos = poss
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let node_contents = DGNode {
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder dgn_name = name,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_theory = G_theory lid' gsig noSens, -- delta is empty
2353f65833a3da763392f771223250cd50b8d873Christian Maeder dgn_nf = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGCofree }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder node = getNewNode dg'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder link = (n',node,DGLink {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_morphism = incl,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_type = CofreeDef nsig,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_origin = DGCofree })
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder return (Cofree_spec (replaceAnnoted sp' asp) poss,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder NodeSig node gsigma',
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder insEdgeNub link $
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder insNode (node,node_contents) dg')
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Local_spec asp asp' poss ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do let sp1 = item asp
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder sp1' = item asp'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (sp2, nsig'@(NodeSig _ (G_sign lid' sigma')), dg') <-
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder ana_SPEC lg gctx nsig (extName "L" name) opts sp1
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder (sp2', NodeSig n'' (G_sign lid'' sigma''), dg'') <-
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder ana_SPEC lg (gannos,genv,dg') (JustNode nsig') (inc name) opts sp1'
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder let gsigma = getMaybeSig nsig
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder G_sign lid sigma <- return gsigma
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder sigma1 <- coerceSign lid' lid "Analysis of local spec" sigma'
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder sigma2 <- coerceSign lid'' lid "Analysis of local spec" sigma''
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder let sys = sym_of lid sigma
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder sys1 = sym_of lid sigma1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sys2 = sym_of lid sigma2
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder pos = poss
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder mor3 <- if isStructured opts then return (ide lid sigma2)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder else adjustPos pos $ cogenerated_sign lid
cb2044812811d66efe038d914966e04290be93faChristian Maeder (sys1 `Set.difference` sys) sigma2
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let sigma3 = dom lid mor3
d81905a5b924415c524d702df26204683c82c12eChristian Maeder -- gsigma2 = G_sign lid sigma2
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder gsigma3 = G_sign lid sigma3
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder sys3 = sym_of lid sigma3
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder when (not( isStructured opts ||
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3))
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder $ pplain_error () (text
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder "attempt to hide the following symbols from the local environment"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder $$ printText ((sys2 `Set.difference` sys1) `Set.difference` sys3))
2353f65833a3da763392f771223250cd50b8d873Christian Maeder pos
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let node_contents = DGNode {
818b228955ef40dd5a253bd942dd6ab8779ed713Christian Maeder dgn_name = name,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgn_theory = G_theory lid sigma3 noSens,
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder dgn_nf = Nothing,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGLocal }
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder node = getNewNode dg''
4a2f7efdf67dfcda0946f1b6373f41976ddea7a4Christian Maeder link = (n'',node,DGLink {
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder dgl_morphism = gEmbed (G_morphism lid mor3),
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder dgl_type = HidingDef,
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder dgl_origin = DGLocal })
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder return (Local_spec (replaceAnnoted sp2 asp)
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder (replaceAnnoted sp2' asp')
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder poss,
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder NodeSig node gsigma3,
ab2f38d9cd1249f6bc9cc5b838dc2fcd76189c0fChristian Maeder insEdgeNub link $
974b0baababf2878820de073b8fad8db68bef08aDominik Luecke insNode (node,node_contents) dg'')
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Closed_spec asp pos ->
966519955f5f7111abac20118563132b9dd41165Christian Maeder do let sp1 = item asp
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder l = getLogic nsig
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder -- analyse spec with empty local env
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (sp', NodeSig n' gsigma', dg') <-
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder ana_SPEC lg gctx (EmptyNode l) (inc name) opts sp1
27b988cb88bfa05fe6f35a853d76ef04f61293efChristian Maeder let gsigma = getMaybeSig nsig
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder adj = adjustPos pos
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
2353f65833a3da763392f771223250cd50b8d873Christian Maeder G_sign lid'' gsig'' <- return gsigma''
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder incl1 <- adj $ ginclusion lg gsigma gsigma''
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder incl2 <- adj $ ginclusion lg gsigma' gsigma''
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let node = getNewNode dg'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder node_contents = DGNode {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_name = name,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_theory = G_theory lid'' gsig'' noSens,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_nf = Nothing,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_sigma = Nothing,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_origin = DGClosed }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder link1 = DGLink {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_morphism = incl1,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_type = GlobalDef,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgl_origin = DGClosedLenv }
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder link2 = (n',node,DGLink {
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgl_morphism = incl2,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgl_type = GlobalDef,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgl_origin = DGClosed })
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder insLink1 = case nsig of
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu EmptyNode _ -> id
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu return (Closed_spec (replaceAnnoted sp' asp) pos,
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu NodeSig node gsigma'',
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu insLink1 $
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu insEdgeNub link2 $
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu insNode (node,node_contents) dg')
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu Qualified_spec (Logic_name ln sublog) asp pos -> do
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu l <- lookupLogic "Static analysis: " (tokStr ln) lg
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu -- analyse spec with empty local env
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu (sp', NodeSig n' gsigma', dg') <-
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu ana_SPEC lg gctx (EmptyNode l) (inc name) opts (item asp)
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu -- construct union with local env
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let gsigma = getMaybeSig nsig
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder adj = adjustPos pos
9dd71ac51c9a6e72bcb126224f9c64131698b636Christian Maeder gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder G_sign lid'' gsig'' <- return gsigma''
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder incl1 <- adj $ ginclusion lg gsigma gsigma''
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder incl2 <- adj $ ginclusion lg gsigma' gsigma''
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder let node = getNewNode dg'
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder node_contents = DGNode {
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder dgn_name = name,
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder dgn_theory = G_theory lid'' gsig'' noSens,
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder dgn_nf = Nothing,
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder dgn_sigma = Nothing,
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder dgn_origin = DGLogicQual }
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder link1 = DGLink {
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder dgl_morphism = incl1,
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder dgl_type = GlobalDef,
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder dgl_origin = DGLogicQualLenv }
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder link2 = (n',node,DGLink {
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder dgl_morphism = incl2,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_type = GlobalDef,
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder dgl_origin = DGLogicQual })
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder insLink1 = case nsig of
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder EmptyNode _ -> id
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder return (Qualified_spec (Logic_name ln sublog) (replaceAnnoted sp' asp) pos,
44f3fc84d88cc5f364e152606779c99e3b8cb895Christian Maeder NodeSig node gsigma'',
44f3fc84d88cc5f364e152606779c99e3b8cb895Christian Maeder insLink1 $
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder insEdgeNub link2 $
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder insNode (node,node_contents) dg')
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder Group asp pos -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (sp',nsig',dg') <- ana_SPEC lg gctx nsig name opts (item asp)
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder return (Group (replaceAnnoted sp' asp) pos,nsig',dg')
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder Spec_inst spname afitargs pos -> do
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder let adj = adjustPos pos
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder case Map.lookup spname genv of
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder Nothing -> fatal_error
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder ("Specification "++ showPretty spname " not found") pos
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder Just (ViewEntry _) ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder fatal_error
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (showPretty spname " is a view, not a specification") pos
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder Just (ArchEntry _) ->
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder fatal_error
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder (showPretty spname
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder " is an architectural, not a structured specification") pos
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder Just (UnitEntry _) ->
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder fatal_error
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder (showPretty spname
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder " is a unit specification, not a structured specification") pos
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just (RefEntry) ->
93bc87ee96c68506945dbad8c704badaa42ecf14Christian Maeder fatal_error
2353f65833a3da763392f771223250cd50b8d873Christian Maeder (showPretty spname
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder " is a refinement specification, not a structured specification") pos
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder Just (SpecEntry gs@(imps,params,_,body@(NodeSig nB gsigmaB))) ->
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder case (\x y -> (x,x-y)) (length afitargs) (length params) of
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder -- the case without parameters leads to a simpler dg
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder (0,0) -> do
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder gsigma@(G_sign lid gsig) <-
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder adj $ gsigUnion lg (getMaybeSig nsig) gsigmaB
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder case nsig of
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- the subcase with empty local env leads to an even simpler dg
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder EmptyNode _ ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- if the node shall not be named and the logic does not change,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder if isInternal name && langNameSig gsigma==langNameSig gsigmaB
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- then just return the body
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then return (sp,body,dg)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- otherwise, we need to create a new one
2353f65833a3da763392f771223250cd50b8d873Christian Maeder else do
2353f65833a3da763392f771223250cd50b8d873Christian Maeder incl <- adj $ ginclusion lg gsigmaB gsigma
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let node = getNewNode dg
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder node_contents = DGNode {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_name = name,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_theory = G_theory lid gsig noSens,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_nf = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGSpecInst spname}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder link = (nB,node,DGLink {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_morphism = incl,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_type = GlobalDef,
2353f65833a3da763392f771223250cd50b8d873Christian Maeder dgl_origin = DGSpecInst spname})
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder return (sp,
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder NodeSig node gsigma,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder insEdgeNub link $
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder insNode (node,node_contents) dg)
528539f3d544c24afe14e979fe51f03e50aa6e9cChristian Maeder
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder -- the subcase with nonempty local env
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder JustNode (NodeSig n sigma) -> do
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder incl1 <- adj $ ginclusion lg sigma gsigma
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder incl2 <- adj $ ginclusion lg gsigmaB gsigma
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let node = getNewNode dg
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder node_contents = DGNode {
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_name = name,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder dgn_theory = G_theory lid gsig noSens,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_nf = Nothing,
59a10395caff224b2ec541f94dac5082a506c00fChristian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGSpecInst spname}
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder link1 = (n,node,DGLink {
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgl_morphism = incl1,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgl_type = GlobalDef,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGSpecInst spname})
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder link2 = (nB,node,DGLink {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_morphism = incl2,
2353f65833a3da763392f771223250cd50b8d873Christian Maeder dgl_type = GlobalDef,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGSpecInst spname})
2353f65833a3da763392f771223250cd50b8d873Christian Maeder return (sp,
2353f65833a3da763392f771223250cd50b8d873Christian Maeder NodeSig node gsigma,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder insEdgeNub link1 $
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder insEdgeNub link2 $
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder insNode (node,node_contents) dg)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- now the case with parameters
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (_,0) -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let fitargs = map item afitargs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (fitargs',dg',args,_) <-
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder foldl anaFitArg (return ([],dg,[],extName "A" name))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (zip params fitargs)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let actualargs = reverse args
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (gsigma',morDelta) <- adj $ apply_GS lg gs actualargs
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder gsigmaRes <- adj $ gsigUnion lg (getMaybeSig nsig) gsigma'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder G_sign lidRes gsigRes <- return gsigmaRes
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder incl1 <- adj $ ginclusion lg (getMaybeSig nsig) gsigmaRes
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder incl2 <- adj $ ginclusion lg gsigma' gsigmaRes
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder morDelta' <- comp Grothendieck (gEmbed morDelta) incl2
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu let node = getNewNode dg'
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu node_contents = DGNode {
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder dgn_name = name,
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder dgn_theory = G_theory lidRes gsigRes noSens,
964ee9fff06b8c821e1d00207f6f185301371be8Christian Maeder dgn_nf = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_sigma = Nothing,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgn_origin = DGSpecInst spname}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder link1 = DGLink {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_morphism = incl1,
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder dgl_type = GlobalDef,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGSpecInst spname}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder insLink1 = case nsig of
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder EmptyNode _ -> id
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder link2 = (nB,node,DGLink {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_morphism = morDelta',
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_type = GlobalDef,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_origin = DGSpecInst spname})
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder parLinks = catMaybes (map (parLink gsigmaRes node) actualargs)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder return (Spec_inst spname
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (map (uncurry replaceAnnoted)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (zip (reverse fitargs') afitargs))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder pos,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder NodeSig node gsigmaRes ,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder foldr insEdgeNub
59a10395caff224b2ec541f94dac5082a506c00fChristian Maeder (insLink1 $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder insEdgeNub link2 $
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder insNode (node,node_contents) dg')
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder parLinks)
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder where
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder anaFitArg res (nsig',fa) = do
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder (fas',dg1,args,name') <- res
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder (fa',dg',arg) <- ana_FIT_ARG lg (gannos,genv,dg1)
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder spname imps nsig' opts name' fa
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder return (fa':fas',dg',arg:args,inc name')
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder parLink gsigma' node (_mor_i, NodeSig nA_i sigA_i) = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder incl <- maybeResult $ ginclusion lg sigA_i gsigma'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let link = DGLink {
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dgl_morphism = incl,
2353f65833a3da763392f771223250cd50b8d873Christian Maeder dgl_type = GlobalDef,
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian Maeder dgl_origin = DGFitSpec }
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder return (nA_i,node,link)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder -- finally the case with conflicting numbers of formal and actual parameters
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian Maeder _ ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder fatal_error
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (showPretty spname " expects "++show (length params)++" arguments"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++" but was given "++show (length afitargs)) pos
2353f65833a3da763392f771223250cd50b8d873Christian Maeder
2353f65833a3da763392f771223250cd50b8d873Christian Maeder
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder Data (Logic lidD) (Logic lidP) asp1 asp2 pos ->
2353f65833a3da763392f771223250cd50b8d873Christian Maeder do let sp1 = item asp1
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder sp2 = item asp2
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder adj = adjustPos pos
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder Comorphism cid <- adj $ logicInclusion lg (Logic lidD) (Logic lidP)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder let lidD' = sourceLogic cid
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder lidP' = targetLogic cid
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (sp1', NodeSig n' (G_sign lid' sigma'), dg1) <-
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder ana_SPEC lg gctx (EmptyNode (Logic lidD)) (inc name) opts sp1
2353f65833a3da763392f771223250cd50b8d873Christian Maeder sigmaD <- adj $ coerceSign lid' lidD' "Analysis of data spec" sigma'
dbc98cd8a9a829e020cfa0a9f3aff89de75caaa9Christian Maeder (sigmaD',sensD') <- adj $ map_sign cid sigmaD
2353f65833a3da763392f771223250cd50b8d873Christian Maeder let gsigmaD' = G_sign lidP' sigmaD'
cb2044812811d66efe038d914966e04290be93faChristian Maeder node_contents = DGNode {
cb2044812811d66efe038d914966e04290be93faChristian Maeder dgn_name = name,
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder dgn_theory = G_theory lidP' sigmaD' $ toThSens sensD',
cb2044812811d66efe038d914966e04290be93faChristian Maeder dgn_nf = Nothing,
2353f65833a3da763392f771223250cd50b8d873Christian Maeder dgn_sigma = Nothing,
cb2044812811d66efe038d914966e04290be93faChristian Maeder dgn_origin = DGData }
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder node = getNewNode dg1
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder link = (n',node,DGLink {
cb2044812811d66efe038d914966e04290be93faChristian Maeder dgl_morphism = GMorphism cid sigmaD (ide lidP' sigmaD'),
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgl_type = GlobalDef,
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dgl_origin = DGData })
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder dg2 = insEdgeNub link $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder insNode (node,node_contents) dg1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder nsig2 = NodeSig node gsigmaD'
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder (sp2',nsig3,dg3) <-
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder ana_SPEC lg (gannos,genv,dg2) (JustNode nsig2) name opts sp2
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder return (Data (Logic lidD) (Logic lidP)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (replaceAnnoted sp1' asp1)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder (replaceAnnoted sp2' asp2)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder pos,
2353f65833a3da763392f771223250cd50b8d873Christian Maeder nsig3,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dg3)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder-- analysis of renamings
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederana_ren1 :: LogicGraph -> GMorphism -> G_mapping -> Result GMorphism
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederana_ren1 _ (GMorphism r sigma mor)
cb2044812811d66efe038d914966e04290be93faChristian Maeder (G_symb_map (G_symb_map_items_list lid sis)) = do
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder let lid2 = targetLogic r
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder rmap <- stat_symb_map_items lid2 sis1
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder mor1 <- induced_from_morphism lid2 rmap (cod lid2 mor)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mor2 <- comp lid2 mor mor1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder return $ GMorphism r sigma mor2
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederana_ren1 lg mor (G_logic_translation (Logic_code tok src tar pos1)) = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let adj = adjustPos pos1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder G_sign srcLid srcSig <- return (cod Grothendieck mor)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder c <- adj $ case tok of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just ctok -> do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Comorphism cid <- lookupComorphism (tokStr ctok) lg
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder when (isJust src && getLogicStr (fromJust src) /=
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder language_name (sourceLogic cid))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (fail (getLogicStr (fromJust src)++"is not the source logic of "
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ language_name cid))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder when (isJust tar && getLogicStr (fromJust tar) /=
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder language_name (targetLogic cid))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (fail (getLogicStr (fromJust tar)++"is not the target logic of "
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ language_name cid))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return (Comorphism cid)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> case tar of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just (Logic_name l _) -> do
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder tarL <- lookupLogic "with logic: " (tokStr l) lg
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder logicInclusion lg (Logic srcLid) tarL
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder Nothing -> fail "with logic: cannot determine comorphism"
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder mor1 <- adj $ gEmbedComorphism c (G_sign srcLid srcSig)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder adj $ comp Grothendieck mor mor1
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder where getLogicStr (Logic_name l _) = tokStr l
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederana_ren :: LogicGraph -> Result GMorphism -> G_mapping -> Result GMorphism
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maederana_ren lg mor_res ren =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do mor <- mor_res
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ana_ren1 lg mor ren
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederana_RENAMING :: LogicGraph -> G_sign -> HetcatsOpts -> RENAMING
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> Result GMorphism
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maederana_RENAMING lg gSigma opts (Renaming ren _) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder if isStructured opts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then return (ide Grothendieck gSigma)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else foldl (ana_ren lg) (return (ide Grothendieck gSigma)) ren
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- analysis of restrictions
2353f65833a3da763392f771223250cd50b8d873Christian Maeder
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederana_restr1 :: DGraph -> G_sign -> GMorphism -> G_hiding -> Result GMorphism
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederana_restr1 _ (G_sign _lid _sigma) (GMorphism cid sigma1 mor)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (G_symb_list (G_symb_items_list lid' sis')) = do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let lid1 = sourceLogic cid
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder lid2 = targetLogic cid
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction" sis'
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder rsys <- stat_symb_items lid1 sis1
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder let sys = sym_of lid1 sigma1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let sys' = Set.filter (\sy -> any (\rsy -> matches lid1 sy rsy) rsys)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sys
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- if sys' `disjoint` () then return ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- else plain_error () "attempt to hide symbols from the local environment" pos
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mor1 <- cogenerated_sign lid1 sys' sigma1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder mor1' <- map_morphism cid mor1
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder mor2 <- comp lid2 mor1' mor
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return $ GMorphism cid (dom lid1 mor1) mor2
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederana_restr1 _dg _gSigma _mor
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder (G_logic_projection (Logic_code _tok _src _tar pos1)) =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder fatal_error "no analysis of logic projections yet" pos1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maederana_restr :: DGraph -> G_sign -> Result GMorphism -> G_hiding
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder -> Result GMorphism
ana_restr dg gSigma mor_res restr =
do mor <- mor_res
ana_restr1 dg gSigma mor restr
ana_RESTRICTION :: DGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION
-> Result (GMorphism, Maybe GMorphism)
ana_RESTRICTION dg gSigma gSigma' opts restr =
ana_RESTRICTION' dg gSigma gSigma' (isStructured opts) restr
ana_RESTRICTION' :: DGraph -> G_sign -> G_sign -> Bool -> RESTRICTION
-> Result (GMorphism, Maybe GMorphism)
ana_RESTRICTION' _ _ gSigma True _ =
return (ide Grothendieck gSigma,Nothing)
ana_RESTRICTION' dg gSigma gSigma' False (Hidden restr _) =
do mor <- foldl (ana_restr dg gSigma)
(return (ide Grothendieck gSigma'))
restr
return (mor,Nothing)
-- ??? Need to check that local env is not affected !
ana_RESTRICTION' _ (G_sign lid sigma) (G_sign lid' sigma')
False (Revealed (G_symb_map_items_list lid1 sis) pos) =
do let sys = sym_of lid sigma -- local env
sys' = sym_of lid' sigma' -- "big" signature
adj = adjustPos pos
sis' <- adj $ coerceSymbMapItemsList lid1 lid'
"Analysis of restriction" sis
rmap <- adj $ stat_symb_map_items lid' sis'
let sys'' =
Set.fromList
[sy | sy <- Set.toList sys', rsy <- Map.keys rmap, matches lid' sy rsy]
-- domain of rmap intersected with sys'
-- domain of rmap should be checked to match symbols from sys' ???
sys1 <- adj $ coerceSymbolSet lid lid' "Analysis of restriction" sys
-- ??? this is too simple in case that local env is translated
-- to a different logic
mor1 <- adj $ generated_sign lid' (sys1 `Set.union` sys'') sigma'
mor2 <- adj $ induced_from_morphism lid' rmap (dom lid' mor1)
return (gEmbed (G_morphism lid' mor1),
Just (gEmbed (G_morphism lid' mor2)))
ana_FIT_ARG :: LogicGraph -> GlobalContext -> SPEC_NAME -> MaybeNode
-> NodeSig -> HetcatsOpts -> NODE_NAME -> FIT_ARG
-> Result (FIT_ARG, DGraph, (G_morphism,NodeSig))
ana_FIT_ARG lg gctx spname nsigI
(NodeSig nP (G_sign lidP sigmaP)) opts name
(Fit_spec asp gsis pos) = do
let adj = adjustPos pos
(sp', nsigA@(NodeSig nA (G_sign lidA sigmaA)), dg') <-
ana_SPEC lg gctx nsigI name opts (item asp)
G_symb_map_items_list lid sis <- homogenizeGM (Logic lidP) gsis
sigmaA' <- adj $ coerceSign lidA lidP "Analysis of fitting argument" sigmaA
mor <- adj $ if isStructured opts then return (ide lidP sigmaP)
else do
rmap <- stat_symb_map_items lid sis
rmap' <- if null sis then return Map.empty
else coerceRawSymbolMap lid lidP
"Analysis of fitting argument" rmap
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 Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI
then return ()
else plain_error () "Fitting morphism must not affect import" ( 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 LeftOpen None LeftOpen,
dgl_origin = DGSpecInst spname})
return (Fit_spec (replaceAnnoted sp' asp) gsis pos,
insEdgeNub link dg',
(G_morphism lidP mor,nsigA)
)
ana_FIT_ARG lg (gannos,genv,dg) spname nsigI (NodeSig nP gsigmaP)
opts name fv@(Fit_view vn afitargs pos) = do
let adj = adjustPos pos
case Map.lookup vn genv of
Nothing -> fatal_error
("View "++ showPretty vn " not found") pos
Just (SpecEntry _) ->
fatal_error
(showPretty spname " is a specification, not a view") pos
Just (ArchEntry _) ->
fatal_error
(showPretty spname
" is an architectural specification, not a view ") pos
Just (UnitEntry _) ->
fatal_error
(showPretty spname
" is a unit specification, not a view") pos
Just (RefEntry) ->
fatal_error
(showPretty spname
" is a refinement specification, not a view") pos
Just (ViewEntry (src,mor,gs@(imps,params,_,target))) -> do
let nSrc = getNode src
nTar = getNode target
gsigmaS = getSig src
gsigmaT = getSig target
gsigmaI = getMaybeSig nsigI
GMorphism cid _ morHom <- return mor
let lid = targetLogic cid
when (not (language_name (sourceLogic cid) == language_name lid))
(fatal_error
"heterogeneous fitting views not yet implemented"
pos)
case (\x y -> (x,x-y)) (length afitargs) (length params) of
-- the case without parameters leads to a simpler dg
(0,0) -> case nsigI of
-- the subcase with empty import leads to a simpler dg
EmptyNode _ -> do
let link = (nP,nSrc,DGLink {
dgl_morphism = ide Grothendieck gsigmaP,
dgl_type = GlobalThm LeftOpen None LeftOpen,
dgl_origin = DGFitView spname})
return (fv,insEdgeNub link dg,(G_morphism lid morHom,target))
-- the subcase with nonempty import
JustNode (NodeSig nI _) -> do
gsigmaIS <- adj $ gsigUnion lg gsigmaI gsigmaS
when (not (is_subgsign gsigmaP gsigmaIS))
(pplain_error ()
(ptext "Parameter does not match source of fittig view."
$$ ptext "Parameter signature:"
$$ printText gsigmaP
$$ text "Source signature of fitting view (united with import):"
$$ printText gsigmaIS) pos)
G_sign lidI sigI1 <- return gsigmaI
sigI <- adj $ coerceSign lidI lid
"Analysis of instantiation with import" sigI1
mor_I <- adj $ morphism_union lid morHom $ ide lid sigI
gsigmaA <- adj $ gsigUnion lg gsigmaI gsigmaT
G_sign lidA gsigA <- return gsigmaA
G_sign lidP gsigP <- return gsigmaP
incl1 <- adj $ ginclusion lg gsigmaI gsigmaA
incl2 <- adj $ ginclusion lg gsigmaT gsigmaA
incl3 <- adj $ ginclusion lg gsigmaI gsigmaP
incl4 <- adj $ ginclusion lg gsigmaS gsigmaP
let [nA,n'] = newNodes 2 dg
node_contentsA = DGNode {
dgn_name = name,
dgn_theory = G_theory lidA gsigA noSens,
dgn_nf = Nothing,
dgn_sigma = Nothing,
dgn_origin = DGFitViewA spname}
node_contents' = DGNode {
dgn_name = inc name,
dgn_theory = G_theory lidP gsigP noSens,
dgn_nf = Nothing,
dgn_sigma = Nothing,
dgn_origin = DGFitView spname}
link = (nP,n',DGLink {
dgl_morphism = ide Grothendieck gsigmaP,
dgl_type = GlobalThm LeftOpen None LeftOpen,
dgl_origin = DGFitView spname})
link1 = (nSrc,n',DGLink {
dgl_morphism = incl4,
dgl_type = GlobalDef,
dgl_origin = DGFitView spname})
link2 = (nTar,nA,DGLink {
dgl_morphism = incl2,
dgl_type = GlobalDef,
dgl_origin = DGFitViewA spname})
link3 = (nI,n',DGLink {
dgl_morphism = incl3,
dgl_type = GlobalDef,
dgl_origin = DGFitViewImp spname})
link4 = (nI,nA,DGLink {
dgl_morphism = incl1,
dgl_type = GlobalDef,
dgl_origin = DGFitViewAImp spname})
return (fv,
insEdgeNub link $
insEdgeNub link1 $
insEdgeNub link2 $
insEdgeNub link3 $
insEdgeNub link4 $
insNode (nA,node_contentsA) $
insNode (n',node_contents') dg,
(G_morphism lid mor_I, NodeSig nA gsigmaA))
-- now the case with parameters
(_,0) -> do
let fitargs = map item afitargs
(fitargs',dg',args,_) <-
foldl anaFitArg (return ([],dg,[],extName "A" name))
(zip params fitargs)
let actualargs = reverse args
(gsigmaA,mor_f) <- adj $ apply_GS lg gs actualargs
let gmor_f = gEmbed mor_f
gsigmaRes <- adj $ gsigUnion lg gsigmaI gsigmaA
G_sign lidRes gsigRes <- return gsigmaRes
mor1 <- adj $ comp Grothendieck mor gmor_f
incl1 <- adj $ ginclusion lg gsigmaA gsigmaRes
mor' <- adj $ comp Grothendieck gmor_f incl1
GMorphism cid1 _ mor1Hom <- return mor1
let lid1 = targetLogic cid1
when (not (language_name (sourceLogic cid1) == language_name lid1))
(fatal_error
("heterogeneous fitting views not yet implemented")
pos)
G_sign lidI sigI1 <- return gsigmaI
sigI <- adj $ coerceSign lidI lid1
"Analysis of instantiation with parameters" sigI1
theta <- adj $ morphism_union lid1 mor1Hom (ide lid1 sigI)
incl2 <- adj $ ginclusion lg gsigmaI gsigmaRes
incl3 <- adj $ ginclusion lg gsigmaI gsigmaP
incl4 <- adj $ ginclusion lg gsigmaS gsigmaP
G_sign lidP gsigP <- return gsigmaP
let [nA,n'] = newNodes 2 dg'
node_contentsA = DGNode {
dgn_name = name,
dgn_theory = G_theory lidRes gsigRes noSens,
dgn_nf = Nothing,
dgn_sigma = Nothing,
dgn_origin = DGFitViewA spname}
node_contents' = DGNode {
dgn_name = extName "V" name,
dgn_theory = G_theory lidP gsigP noSens,
dgn_nf = Nothing,
dgn_sigma = Nothing,
dgn_origin = DGFitView spname}
link = (nP,n',DGLink {
dgl_morphism = ide Grothendieck gsigmaP,
dgl_type = GlobalThm LeftOpen None LeftOpen,
dgl_origin = DGFitView spname})
link1 = (nSrc,n',DGLink {
dgl_morphism = incl4,
dgl_type = GlobalDef,
dgl_origin = DGFitView spname})
link2 = (nTar,nA,DGLink {
dgl_morphism = mor',
dgl_type = GlobalDef,
dgl_origin = DGFitViewA spname})
fitLinks = [link,link1,link2] ++ case nsigI of
EmptyNode _ -> []
JustNode (NodeSig nI _) -> let
link3 = (nI,n',DGLink {
dgl_morphism = incl3,
dgl_type = GlobalDef,
dgl_origin = DGFitViewImp spname})
link4 = (nI,nA,DGLink {
dgl_morphism = incl2,
dgl_type = GlobalDef,
dgl_origin = DGFitViewAImp spname})
in [link3,link4]
parLinks = catMaybes (map (parLink gsigmaRes nA) actualargs)
return (Fit_view vn
(map (uncurry replaceAnnoted)
(zip (reverse fitargs') afitargs))
pos,
foldr insEdgeNub
(insNode (nA,node_contentsA) $
insNode (n',node_contents') dg')
(fitLinks++parLinks),
(G_morphism lid1 theta, NodeSig nA gsigmaRes))
where
anaFitArg res (nsig',fa) = do
(fas',dg1,args,name') <- res
(fa',dg',arg) <- ana_FIT_ARG lg (gannos,genv,dg1)
spname imps nsig' opts name' fa
return (fa':fas',dg',arg:args,inc name')
parLink gsigmaRes node (_mor_i,nsigA_i) = do
let nA_i = getNode nsigA_i
incl <- maybeResult $ ginclusion lg (getSig nsigA_i) gsigmaRes
let link = DGLink {
dgl_morphism = incl,
dgl_type = GlobalDef,
dgl_origin = DGFitView spname }
return (nA_i,node,link)
-- finally the case with conflicting numbers of formal and actual parameters
_ ->
fatal_error
(showPretty spname " expects "++show (length params)++" arguments"
++" but was given "++show (length afitargs)) pos
-- Extension of signature morphisms (for instantitations)
-- first some auxiliary functions
{- not really needed:
-- for an Id, compute the list of components that are relevant for extension
idComponents :: Id -> Set.Set Id -> [Id]
idComponents (Id toks comps pos) ids =
foldl (\x y -> y++x) []
$ map (\id1 -> if id1 `Set.member` ids
then [id1]
else idComponents id1 ids)
comps
--
componentRelation :: Set.Set Id -> Set.Set (Id,[Id])
componentRelation ids =
Set.map (\id -> (id,idComponents id ids)) ids
-}
mapID :: Map.Map Id (Set.Set Id) -> Id -> Result Id
mapID idmap i@(Id toks comps pos1) =
case Map.lookup i idmap of
Nothing -> do
compsnew <- sequence $ map (mapID idmap) comps
return (Id toks compsnew pos1)
Just ids -> case Set.size ids of
0 -> return i
1 -> return $ Set.findMin ids
_ -> pplain_error i
(ptext "Identifier component " <+> printText i
<+> ptext "can be mapped in various ways:"
<+> printText ids) nullRange
extID1 :: Map.Map Id (Set.Set Id) -> Id
-> Result (EndoMap Id) -> Result (EndoMap Id)
extID1 idmap i@(Id toks comps pos1) m = do
m1 <- m
compsnew <- sequence $ map (mapID idmap) comps
if comps==compsnew
then return m1
else return (Map.insert i (Id toks compsnew pos1) m1)
extID :: Set.Set Id -> Map.Map Id (Set.Set Id) -> Result (EndoMap Id)
extID ids idmap = Set.fold (extID1 idmap) (return Map.empty) ids
extendMorphism :: G_sign -- ^ formal parameter
-> G_sign -- ^ body
-> G_sign -- ^ actual parameter
-> G_morphism -- ^ fitting morphism
-> Result(G_sign,G_morphism)
extendMorphism (G_sign lid sigmaP) (G_sign lidB sigmaB1)
(G_sign lidA sigmaA1) (G_morphism lidM fittingMor1) = do
-- for now, only homogeneous instantiations....
sigmaB <- coerceSign lidB lid "Extension of symbol map" sigmaB1
sigmaA <- coerceSign lidA lid "Extension of symbol map" sigmaA1
fittingMor <- coerceMorphism lidM lid "Extension of symbol map" fittingMor1
let symsP = sym_of lid sigmaP
symsB = sym_of lid sigmaB
idsB = Set.map (sym_name lid) symsB
h = symmap_of lid fittingMor
symbMapToRawSymbMap =
Map.foldWithKey (\sy1 sy2 -> Map.insert (symbol_to_raw lid sy1)
(symbol_to_raw lid sy2))
Map.empty
rh = symbMapToRawSymbMap h
idh = Map.foldWithKey
(\sy1 sy2 -> Rel.setInsert (sym_name lid sy1) (sym_name lid sy2))
Map.empty h
idhExt <- extID idsB idh
let rIdExt = Map.foldWithKey
(\id1 id2 -> Map.insert (id_to_raw lid id1) (id_to_raw lid id2))
Map.empty
(foldr (\i -> Map.delete i) idhExt $ Map.keys idh)
r = rh `Map.union` rIdExt
-- do we need combining function catching the clashes???
mor <- induced_from_morphism lid r sigmaB
let hmor = symmap_of lid mor
sigmaAD = cod lid mor
sigma <- final_union lid sigmaA sigmaAD
let illShared = (sym_of lid sigmaA `Set.intersection` sym_of lid sigmaAD )
Set.\\ Rel.image h symsP
when (not (Set.null illShared))
(pplain_error () (ptext
"Symbols shared between actual parameter and body must be in formal parameter"
$$ printText illShared ) nullRange)
let myKernel m = Set.fromDistinctAscList $ comb1 $ Map.assocs m
comb1 [] = []
comb1 (p : qs) =
comb2 p qs [] ++ comb1 qs
comb2 _ [] rs = rs
comb2 p@(a, b) ((c, d) : qs) rs =
comb2 p qs $ if b == d then (a, c) : rs else rs
newIdentifications = myKernel hmor Set.\\ myKernel h
when (not (Set.null newIdentifications))
(pplain_error () (ptext
"Fitting morphism leads to forbidden identifications"
$$ printText newIdentifications) nullRange)
incl <- inclusion lid sigmaAD sigma
mor1 <- comp lid mor incl
return (G_sign lid sigma, G_morphism lid mor1)
apply_GS :: LogicGraph -> ExtGenSig -> [(G_morphism,NodeSig)]
-> Result(G_sign,G_morphism)
apply_GS lg (nsigI,_params,gsigmaP,nsigB) args = do
let mor_i = map fst args
gsigmaA_i = map (getSig . snd) args
gsigmaB = getSig nsigB
gsigmaI = getMaybeSig nsigI
G_sign lidI sigmaI <- return gsigmaI
let idI = ide lidI sigmaI
gsigmaA <- gsigManyUnion lg gsigmaA_i
mor_f <- homogeneousMorManyUnion (G_morphism lidI idI:mor_i)
extendMorphism gsigmaP gsigmaB gsigmaA mor_f
-- | analyze a GENERICITY
-- Parameters: global context, current logic, just-structure-flag, GENERICITY
ana_GENERICITY :: LogicGraph -> GlobalContext -> AnyLogic -> HetcatsOpts
-> NODE_NAME -> GENERICITY
-> Result (GENERICITY, GenericitySig, DGraph)
-- zero parameters,
ana_GENERICITY _ (_,_,dg) l _ _
gen@(Genericity (Params []) (Imported imps) pos) = do
when (not (null imps))
(plain_error () "Parameterless specifications must not have imports"
pos)
return (gen,(EmptyNode l, [], EmptyNode l),dg)
-- one parameter ...
ana_GENERICITY lg gctx@(gannos,genv,_) l opts name
(Genericity (Params [asp]) imps pos) = do
(imps',nsigI,dg') <- ana_IMPORTS lg gctx l opts (extName "I" name) imps
(sp',nsigP,dg'') <- ana_SPEC lg (gannos,genv,dg') nsigI
name opts (item asp)
return (Genericity (Params [replaceAnnoted sp' asp]) imps' pos,
(nsigI, [nsigP], JustNode nsigP),
dg'')
-- ... and more parameters
ana_GENERICITY lg gctx@(gannos,genv,_) l opts name
(Genericity params imps pos) = do
let adj = adjustPos pos
(imps',nsigI,dg') <- ana_IMPORTS lg gctx l opts (extName "I" name) imps
(params',nsigPs,dg'') <-
ana_PARAMS lg (gannos,genv,dg') l nsigI opts (inc name) params
gsigmaP <- adj $ gsigManyUnion lg (map getSig nsigPs)
G_sign lidP gsigP <- return gsigmaP
let node_contents = DGNode {
dgn_name = name,
dgn_theory = G_theory lidP gsigP noSens,
dgn_nf = Nothing,
dgn_sigma = Nothing,
dgn_origin = DGFormalParams }
node = getNewNode dg''
dg''' = insNode (node,node_contents) dg''
inslink dgres (NodeSig n sigma) = do
dg <- dgres
incl <- adj $ ginclusion lg sigma gsigmaP
return (insEdgeNub (n,node,DGLink {
dgl_morphism = incl,
dgl_type = GlobalDef,
dgl_origin = DGFormalParams }) dg)
dg4 <- foldl inslink (return dg''') nsigPs
return (Genericity params' imps' pos,
(nsigI, nsigPs, JustNode $ NodeSig node gsigmaP),
dg4)
ana_PARAMS :: LogicGraph -> GlobalContext -> AnyLogic -> MaybeNode
-> HetcatsOpts -> NODE_NAME -> PARAMS
-> Result (PARAMS, [NodeSig], DGraph)
ana_PARAMS lg (gannos,genv,dg) _ nsigI opts name (Params asps) = do
(sps',pars,dg',_) <- foldl ana (return ([],[],dg,name)) (map item asps)
return (Params (map (uncurry replaceAnnoted)
(zip (reverse sps') asps)),
reverse pars,
dg')
where
ana res sp = do
(sps',pars,dg1,n) <- res
(sp',par,dg') <- ana_SPEC lg (gannos,genv,dg1) nsigI n opts sp
return (sp':sps',par:pars,dg',inc n)
ana_IMPORTS :: LogicGraph -> GlobalContext -> AnyLogic -> HetcatsOpts
-> NODE_NAME -> IMPORTED
-> Result (IMPORTED, MaybeNode, DGraph)
ana_IMPORTS lg gctx@(_, _, dg) l opts name imps@(Imported asps) =
case asps of
[] -> return (imps, EmptyNode l, dg)
_ -> do
let sp = Union asps nullRange
(Union asps' _, nsig', dg') <-
ana_SPEC lg gctx (EmptyNode l) name opts sp
return (Imported asps', JustNode 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 :: LogicGraph -> GlobalContext -> AnyLogic
-> MaybeNode -> HetcatsOpts -> NODE_NAME -> VIEW_TYPE
-> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
ana_VIEW_TYPE lg gctx@(gannos,genv,_) l parSig opts name
(View_type aspSrc aspTar pos) = do
(spSrc',srcNsig,dg') <-
ana_SPEC lg gctx (EmptyNode l) (extName "S" name) opts (item aspSrc)
(spTar',tarNsig,dg'') <-
ana_SPEC lg (gannos,genv,dg') parSig
(extName "T" name) opts (item aspTar)
return (View_type (replaceAnnoted spSrc' aspSrc)
(replaceAnnoted spTar' aspTar)
pos,
(srcNsig,tarNsig),
dg'')
homogenizeGM :: AnyLogic
-> [Syntax.AS_Structured.G_mapping] -> Result G_symb_map_items_list
homogenizeGM (Logic lid) gsis =
foldl homogenize1 (return (G_symb_map_items_list lid [])) gsis
where
homogenize1 res
(Syntax.AS_Structured.G_symb_map (G_symb_map_items_list lid1 sis1)) = do
(G_symb_map_items_list lid2 sis) <- res
sis1' <- coerceSymbMapItemsList lid1 lid2 "" sis1
return (G_symb_map_items_list lid2 (sis++sis1'))
homogenize1 res _ = res
-- | check if structured analysis should be performed
isStructured :: HetcatsOpts -> Bool
isStructured a = case analysis a of Structured -> True
_ -> False
-- | Auxiliary function for not yet implemented features
ana_err :: String -> a
ana_err fname =
error ("*** Analysis of " ++ fname ++ " is not yet implemented!")