0N/A Copyright : (c) Till Mossakowski and Uni Bremen 2003
0N/A Licence : All rights reserved.
0N/A Maintainer : hets@tzi.de
0N/A Stability : provisional
0N/A Analysis of structured specifications
0N/A Follows the extended static semantic rules in:
0N/A T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
0N/A CASL Proof calculus.
1472N/A To appear in the CASL book.
0N/A Option: only the structure is analysed
0N/A Check that translations and reductions do not effect local env
1879N/A Unions (already in the parser) need unions of logics
1879N/A = suprema in the lattice of default logic inclusions!
1879N/A (also needed by closed specs)
1879N/A Should we use institution independent analysis over the Grothendieck logic?
1879N/A abstract syntax + devgraph would have to be changed to homogeneous case
1879N/A logic translations are symbol maps in the Grothendieck logic
1879N/A Problem with this approach: symbol functor goes into rel,
1879N/A and induced_from_morphism gets difficult to implement
1879N/A Unions need inclusion morphisms. Should these play a special role?
1879N/A At least we need a function delivering the inclusion morphism
0N/A between two (sub)signatures.
0N/A In most logics, inclusions could be represented specially, such
0N/A that composition for them becomes fast.
0N/A Should we even identify an inclusion subcategory?
0N/A Then inclusions are represented by pair of signatures
0N/A (Non-inclusions could be specially displayed in the DG)
0N/A Treatment of translations and reductions along logic translations
0N/A (see WADT 02 paper).
0N/A may local env be translated, and even reduced, along logic translations?
0N/A if yes: how is local env linked to signature of resulting spec?
0N/A (important
e.g. for checking that local env is not being renamed?)
0N/A does signature+comorphism suffice, such that c(local env)\subseteq sig?
0N/A if no: this means that only closed specs may be translated
0N/A Revealings wihout translations: just one arrow
0N/A Pushouts: only admissible within one logic?
0N/A Union nodes can be extended by a basic spec directly (no new node needed)
0N/A Also: free, cofree nodes
0N/AlookupNode n dg = lab' $ context n dg
0N/AsetFilter p s = fromList (filter p (toList s))
0N/AsetAny p s = any p (toList s)
3863N/AsetAll p s = all p (toList s)
0N/As1 `disjoint` s2 = s1 `intersection` s2 == empty
0N/A-- Parameters: global context, local environment,
0N/A-- the SIMPLE_ID may be a name if the specification shall be named,
0N/A-- flag: shall only the structure be analysed?
0N/Aana_SPEC :: GlobalContext -> NodeSig -> Maybe SIMPLE_ID -> Bool -> SPEC
0N/A -> Result (NodeSig,DGraph)
0N/Aana_SPEC gctx@(gannos,genv,dg) nsig name just_struct sp =
0N/A Basic_spec (G_basic_spec lid bspec) ->
0N/A do G_sign lid' sigma' <- return (getSig nsig)
0N/A sigma <- rcoerce lid' lid nullPos sigma'
0N/A (sigma_local, sigma_complete, ax) <-
0N/A then return (empty_signature lid, empty_signature lid,[])
0N/A else do b <- maybeToResult nullPos
0N/A ("no basic analysis for logic "
0N/A ++language_name lid)
0N/A (basic_analysis lid)
0N/A b (bspec,sigma,gannos)
0N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lid sigma_local, -- only the delta
0N/A dgn_sens = G_l_sentence lid ax,
0N/A dgn_origin = DGBasic }
0N/A [node] = newNodes 0 dg
0N/A dg' = insNode (node,node_contents) dg
0N/A dgl_morphism = undefined, -- where to get it from ???
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGExtension }
0N/A NodeSig (n,_) -> insEdge (n,node,link) dg'
0N/A return (NodeSig (node,G_sign lid sigma_complete),dg'')
0N/A Translation asp ren ->
0N/A do let sp = item asp
0N/A (nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
0N/A n' <- maybeToResult nullPos
0N/A "Internal error: Translation of empty spec" (getNode nsig')
0N/A mor <- ana_RENAMING dg (getSig nsig') ren
0N/A -- ??? check that mor is identity on local env
0N/A let gsigma' = cod Grothendieck mor
0N/A -- ??? too simplistic for non-comorphism inter-logic translations
0N/A G_sign lid' sigma' <- return gsigma'
0N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty
0N/A dgn_sens = G_l_sentence lid' [],
0N/A dgn_origin = DGTranslation }
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGTranslation })
0N/A return (NodeSig(node,gsigma'),
0N/A insNode (node,node_contents) dg')
0N/A Reduction asp restr ->
0N/A do let sp = item asp
0N/A (nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
0N/A let gsigma = getSig nsig
0N/A gsigma' = getSig nsig'
0N/A n' <- maybeToResult nullPos
0N/A "Internal error: Reduction of empty spec" (getNode nsig')
0N/A (hmor,tmor) <- ana_RESTRICTION dg gsigma gsigma' restr
0N/A -- we treat hiding and revealing differently
0N/A -- in order to keep the dg as simple as possible
0N/A do let gsigma' = dom Grothendieck hmor
0N/A -- ??? too simplistic for non-comorphism inter-logic reductions
0N/A G_sign lid' sigma' <- return gsigma'
0N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lid' (empty_signature lid'),
0N/A dgn_sens = G_l_sentence lid' [],
0N/A dgn_origin = DGHiding }
0N/A [node] = newNodes 0 dg'
0N/A link = (n',node,DGLink {
0N/A dgl_morphism = hmor,
0N/A dgl_type = HidingDef,
0N/A dgl_origin = DGHiding })
0N/A return (NodeSig(node,gsigma'),
0N/A insNode (node,node_contents) dg')
0N/A do let gsigma1 = dom Grothendieck tmor'
0N/A gsigma'' = cod Grothendieck tmor'
0N/A -- ??? too simplistic for non-comorphism inter-logic reductions
0N/A G_sign lid1 sigma1 <- return gsigma1
1808N/A G_sign lid'' sigma'' <- return gsigma''
1808N/A let [node1,node''] = newNodes 1 dg'
0N/A node_contents1 = DGNode {
1808N/A dgn_sign = G_sign lid1 (empty_signature lid1),
0N/A dgn_sens = G_l_sentence lid1 [],
1145N/A dgl_origin = DGRevealing })
0N/A dgn_sign = G_sign lid'' (empty_signature lid''),
0N/A dgn_sens = G_l_sentence lid'' [],
0N/A dgn_origin = DGRevealTranslation }
0N/A link'' = (node1,node'',DGLink {
0N/A dgl_morphism = tmor',
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGRevealTranslation })
0N/A return (NodeSig(node'',gsigma''),
0N/A insNode (node'',node_contents'') $
0N/A insNode (node1,node_contents1) dg')
0N/A Union [] pos -> return (nsig,dg)
0N/A do let sps = map item asps
0N/A (nsigs,dg') <- let ana r sp = do
0N/A (nsig,dg1) <- ana_SPEC gctx nsig Nothing just_struct sp
0N/A return (nsig:nsigs,dg1)
2984N/A in foldl ana (return ([],dg)) sps
0N/A let nsigs' = reverse nsigs
0N/A nodes = catMaybes (map getNode nsigs')
0N/A G_sign lid' bigSigma <-
0N/A homogeneousGsigManyUnion (headPos pos) (map getSig nsigs')
0N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lid' (empty_signature lid'),
0N/A dgn_sens = G_l_sentence lid' [],
0N/A dgn_origin = DGUnion }
0N/A [node] = newNodes 0 dg'
0N/A dgl_morphism = undefined, -- ??? how to get it?
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGUnion }
0N/A return (let insE dg n = insEdge (n,node,link) dg -- link should vary
0N/A in (NodeSig(node,G_sign lid' bigSigma),
0N/A foldl insE (insNode (node,node_contents) dg') nodes))
0N/A Extension [] pos -> return (nsig,dg)
0N/A Extension asps pos ->
0N/A foldl ana (return (nsig,dg)) namedSps
0N/A namedSps = zip (map (\_ -> Nothing) (tail asps) ++ [name]) (map item asps)
0N/A ana res (name,sp) = do
0N/A ana_SPEC (gannos,genv,dg) nsig name just_struct sp
0N/A Free_spec asp pos ->
0N/A do let sp = item asp
0N/A (nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
0N/A n' <- maybeToResult nullPos
0N/A "Internal error: Free spec over empty spec" (getNode nsig')
0N/A let gsigma' = getSig nsig'
0N/A G_sign lid' sigma' <- return gsigma'
0N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty
0N/A dgn_sens = G_l_sentence lid' [],
0N/A dgn_origin = DGFree }
0N/A [node] = newNodes 0 dg'
0N/A link = (n',node,DGLink {
0N/A dgl_morphism = undefined, -- ??? inclusion
0N/A dgl_type = FreeDef nsig,
0N/A dgl_origin = DGFree })
0N/A return (NodeSig(node,gsigma'),
0N/A insNode (node,node_contents) dg')
0N/A Cofree_spec asp pos ->
0N/A do let sp = item asp
0N/A (nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
0N/A n' <- maybeToResult nullPos
0N/A "Internal error: Free spec over empty spec" (getNode nsig')
0N/A let gsigma' = getSig nsig'
0N/A G_sign lid' sigma' <- return gsigma'
0N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty
0N/A dgn_sens = G_l_sentence lid' [],
0N/A dgn_origin = DGCofree }
0N/A [node] = newNodes 0 dg'
0N/A link = (n',node,DGLink {
0N/A dgl_morphism = undefined, -- ??? inclusion
0N/A dgl_type = CofreeDef nsig,
0N/A dgl_origin = DGCofree })
0N/A return (NodeSig(node,gsigma'),
0N/A insNode (node,node_contents) dg')
0N/A Local_spec asp asp' pos ->
0N/A do let sp = item asp
0N/A (nsig',dg') <- ana_SPEC gctx nsig Nothing just_struct sp
0N/A (nsig'',dg'') <- ana_SPEC (gannos,genv,dg') nsig' Nothing just_struct sp'
0N/A n'' <- maybeToResult nullPos
0N/A "Internal error: Local spec over empty spec" (getNode nsig'')
0N/A let gsigma = getSig nsig
0N/A gsigma' = getSig nsig'
0N/A gsigma'' = getSig nsig''
0N/A G_sign lid sigma <- return gsigma
0N/A G_sign lid' sigma' <- return gsigma'
0N/A G_sign lid'' sigma'' <- return gsigma''
0N/A sigma1 <- rcoerce lid' lid nullPos sigma'
0N/A sigma2 <- rcoerce lid'' lid nullPos sigma''
0N/A let sys = sym_of lid sigma
0N/A sys1 = sym_of lid sigma1
0N/A sys2 = sym_of lid sigma2
0N/A mor3 <- cogenerated_sign lid (toList (sys1 `difference` sys)) sigma2
0N/A let sigma3 = dom lid mor3
0N/A gsigma2 = G_sign lid sigma2
113N/A gsigma3 = G_sign lid sigma3
0N/A sys3 = sym_of lid sigma3
0N/A if sys2 `difference` sys1 `subset` sys3 then return ()
0N/A "attempt to hide symbols from the local environment" (headPos pos)
0N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lid (empty_signature lid), -- delta is empty
0N/A dgn_sens = G_l_sentence lid [],
0N/A dgn_origin = DGLocal }
0N/A [node] = newNodes 0 dg''
0N/A link = (n'',node,DGLink {
0N/A dgl_morphism = gEmbed (G_morphism lid mor3),
0N/A dgl_type = HidingDef,
0N/A dgl_origin = DGLocal })
0N/A return (NodeSig(node,gsigma3),
0N/A insNode (node,node_contents) dg'')
0N/A Closed_spec asp pos ->
0N/A do let sp = item asp
0N/A (nsig',dg') <- ana_SPEC gctx (EmptyNode l) Nothing just_struct sp
0N/A n' <- maybeToResult nullPos
0N/A "Internal error: Closed spec over empty spec" (getNode nsig')
0N/A let gsigma = getSig nsig
0N/A gsigma' = getSig nsig'
0N/A gsigma'' <- homogeneousGsigUnion (headPos pos) gsigma gsigma'
0N/A -- also allow different logics???
0N/A G_sign lid'' sigma'' <- return gsigma''
0N/A let [node] = newNodes 0 dg'
0N/A node_contents = DGNode {
0N/A dgn_sign = G_sign lid'' (empty_signature lid''),
0N/A dgn_sens = G_l_sentence lid'' [],
0N/A dgn_origin = DGClosed }
0N/A link1 = (n',node,DGLink {
0N/A dgl_morphism = inclusion gsigma' gsigma'',
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGClosed })
0N/A dgl_morphism = inclusion gsigma' gsigma'',
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGClosedLenv }
0N/A insLink2 = case (getNode nsig) of
0N/A Just n -> insEdge (n,node,link2)
0N/A return (NodeSig(node,gsigma''),
0N/A insNode (node,node_contents) dg')
0N/A ana_SPEC gctx nsig name just_struct (item asp)
1808N/A Spec_inst spname afitargs pos ->
1808N/A Nothing -> plain_error (nsig,dg)
1808N/A ("Specification "++ showPretty spname " not found") (headPos pos)
1808N/A (showPretty spname " is a view, not a specification") (headPos pos)
0N/A plain_error (nsig,dg)
0N/A " is an architectural, not a structured specification") (headPos pos)
0N/A Just (UnitEntry _) ->
0N/A plain_error (nsig,dg)
0N/A " is a unit specification, not a structured specification") (headPos pos)
0N/A Just (SpecEntry gs@(imps,params,gSigmaP,body)) ->
0N/A case (\x y -> (x,x-y)) (length afitargs) (length params) of
0N/A -- the case without parameters leads to a simpler dg
0N/A let gsigmaB = getSig body
0N/A gsigma <- homogeneousGsigUnion (headPos pos) (getSig nsig) gsigmaB
0N/A G_sign lid sigma <- return gsigma
0N/A nB <- maybeToResult (headPos pos)
0N/A "Internal error: empty body spec" (getNode body)
0N/A case (getNode nsig) of
0N/A -- the case with empty local env leads to an even simpler dg
0N/A Nothing -> case name of
0N/A -- if the node shall not be named, just return the body
0N/A Nothing -> return (body,dg)
0N/A -- if the node shall be named, we need to create a new one
0N/A let [node] = newNodes 0 dg
0N/A node_contents = DGNode {
263N/A dgn_sign = G_sign lid (empty_signature lid),
263N/A dgn_sens = G_l_sentence lid [],
0N/A dgn_origin = DGSpecInst spname}
0N/A link = (nB,node,DGLink {
0N/A dgl_morphism = inclusion gsigmaB gsigma,
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGSpecInst spname})
0N/A in return (NodeSig(node,gsigma),
2988N/A insNode (node,node_contents) dg)
2988N/A -- the case with nonempty local env
0N/A let [node] = newNodes 0 dg
0N/A node_contents = DGNode {
0N/A dgn_sign = G_sign lid (empty_signature lid),
0N/A dgn_sens = G_l_sentence lid [],
0N/A dgn_origin = DGSpecInst spname}
0N/A link1 = (n,node,DGLink {
0N/A dgl_morphism = inclusion (getSig nsig) gsigma,
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGSpecInst spname})
0N/A link2 = (nB,node,DGLink {
0N/A dgl_morphism = inclusion gsigmaB gsigma,
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGSpecInst spname})
0N/A in return (NodeSig(node,gsigma),
0N/A insNode (node,node_contents) dg)
0N/A -- now the general case: with parameters
0N/A let fitargs = map item afitargs
0N/A (dg',args) <- foldl ana (return (dg,[])) (zip params fitargs)
0N/A let actualargs = reverse args
0N/A (gsigma',mor_f) <- apply_GS (headPos pos) gs actualargs
0N/A G_sign lid' sigma' <- return gsigma'
0N/A gsigmaRes <- homogeneousGsigUnion (headPos pos) (getSig nsig) gsigma'
0N/A nB <- maybeToResult (headPos pos)
0N/A "Internal error: empty body spec" (getNode body)
0N/A let [node] = newNodes 0 dg'
0N/A node_contents = DGNode {
0N/A dgn_sign = G_sign lid' (empty_signature lid'),
0N/A dgn_sens = G_l_sentence lid' [],
0N/A dgn_origin = DGSpecInst spname}
0N/A dgl_morphism = inclusion (getSig nsig) gsigma',
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGSpecInst spname}
0N/A insLink1 = case (getNode nsig) of
0N/A Just n -> insEdge (n,node,link1)
0N/A link2 = (nB,node,DGLink {
0N/A dgl_morphism = inclusion (getSig body) gsigma',
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGSpecInst spname})
0N/A parLinks = catMaybes (map (parLink node) actualargs)
0N/A return (NodeSig(node,gsigma'),
0N/A insNode (node,node_contents) dg')
0N/A ana res (nsig,fa) = do
0N/A (dg',arg) <- ana_FIT_ARG (gannos,genv,dg) spname imps nsig just_struct fa
0N/A return (dg',arg:args)
0N/A parLink node (mor_i,nsigA_i) = do
0N/A nA_i <- getNode nsigA_i
0N/A dgl_morphism = gEmbed mor_i,
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGClosed }
0N/A return (nA_i,node,link)
0N/A -- finally the case with conflicting numbers of formal and actual parameters
0N/A plain_error (nsig,dg)
0N/A (showPretty spname " expects "++show (length params)++" arguments"
0N/A ++" but was given "++show (length afitargs)) (headPos pos)
0N/A Qualified_spec logname asp pos ->
0N/A ana_err "logic qualified specs"
0N/A Data (Logic lid1) asp1 asp2 pos ->
0N/A do let sp1 = item asp1
0N/A (nsig1,dg1) <- ana_SPEC gctx (EmptyNode lid1) Nothing just_struct sp1
0N/A (nsig2,dg2) <- ana_SPEC (gannos,genv,dg1) nsig1 Nothing just_struct sp2
0N/A n' <- maybeToResult nullPos
0N/A "Internal error: Free spec over empty spec" (getNode nsig')
0N/A let gsigma' = getSig nsig'
0N/A G_sign lid' sigma' <- return gsigma'
0N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty
0N/A dgn_sens = G_l_sentence lid' [],
263N/A [node] = newNodes 0 dg'
263N/A link = (n',node,DGLink {
263N/A dgl_morphism = undefined, -- ??? inclusion
0N/A dgl_type = FreeDef nsig,
0N/A dgl_origin = DGFree })
0N/A return (NodeSig(node,gsigma'),
0N/A insNode (node,node_contents) dg')
0N/A-- analysis of renamings
0N/Aana_ren1 dg (GMorphism lid1 lid2 r sigma mor)
0N/A (G_symb_map (G_symb_map_items_list lid sis),pos) = do
0N/A sis1 <- rcoerce lid2 lid pos sis
0N/A rmap <- stat_symb_map_items lid2 sis1
0N/A mor1 <- induced_from_morphism lid2 rmap (cod lid2 mor)
0N/A mor2 <- maybeToResult pos
0N/A "renaming: signature morphism composition failed"
0N/A (comp lid2 mor mor1)
0N/A return (GMorphism lid1 lid2 r sigma mor2)
0N/Aana_ren1 dg mor (G_logic_translation (Logic_code tok src tar pos1),pos2) =
0N/A fatal_error "no analysis of logic translations yet" pos2
0N/Aana_ren :: DGraph -> Result GMorphism -> (G_mapping,Pos) -> Result GMorphism
0N/Aana_ren dg mor_res ren =
0N/Aana_RENAMING :: DGraph -> G_sign -> RENAMING -> Result GMorphism
0N/Aana_RENAMING dg gSigma (Renaming ren pos) =
0N/A foldl (ana_ren dg) (return (ide Grothendieck gSigma)) ren'
0N/A ren' = zip ren (tail (pos ++ repeat nullPos))
517N/A-- analysis of restrictions
517N/Aana_restr1 dg (G_sign lid sigma) (GMorphism lid1 lid2 r sigma1 mor)
517N/A (G_symb_list (G_symb_items_list lid' sis'),pos) = do
517N/A sis1 <- rcoerce lid1 lid' pos sis'
0N/A rsys <- stat_symb_items lid1 sis1
0N/A let sys = sym_of lid1 sigma1
0N/A let sys' = filter (\sy -> any (\rsy -> matches lid1 sy rsy) rsys)
0N/A-- if sys' `disjoint` () then return ()
0N/A-- else plain_error () "attempt to hide symbols from the local environment" pos
0N/A mor1 <- cogenerated_sign lid1 sys' sigma1
0N/A mor1' <- maybeToResult pos
0N/A ("restriction: could not map morphism along" ++ repr_name r)
0N/A (map_morphism r mor1)
0N/A mor2 <- maybeToResult pos
0N/A "restriction: signature morphism composition failed"
0N/A (comp lid2 mor1' mor)
0N/A return (GMorphism lid1 lid2 r (dom lid1 mor1) mor2)
0N/Aana_restr1 dg gSigma mor
0N/A (G_logic_projection (Logic_code tok src tar pos1),pos2) =
0N/A fatal_error "no analysis of logic projections yet" pos2
0N/Aana_restr :: DGraph -> G_sign -> Result GMorphism -> (G_hiding,Pos)
0N/Aana_restr dg gSigma mor_res restr =
0N/A ana_restr1 dg gSigma mor restr
0N/Aana_RESTRICTION :: DGraph -> G_sign -> G_sign -> RESTRICTION
0N/A -> Result (GMorphism, Maybe GMorphism)
0N/Aana_RESTRICTION dg gSigma gSigma' (Hidden restr pos) =
0N/A do mor <- foldl (ana_restr dg gSigma)
0N/A (return (ide Grothendieck gSigma'))
0N/A return (mor,Nothing)
0N/A restr' = zip restr (tail (pos ++ repeat nullPos))
0N/Aana_RESTRICTION dg gSigma@(G_sign lid sigma) gSigma'@(G_sign lid' sigma')
0N/A (Revealed (G_symb_map_items_list lid1 sis) pos) =
0N/A do let sys = sym_of lid sigma
0N/A sys' = sym_of lid' sigma'
0N/A sis' <- rcoerce lid1 lid' (headPos pos) sis
0N/A rmap <- stat_symb_map_items lid' sis'
0N/A [sy | sy <- toList sys', rsy <-
Map.keys rmap, matches lid' sy rsy]
0N/A sys1 <- rcoerce lid lid' (headPos pos) sys
0N/A -- ??? this is too simple in case that local env is translated
0N/A -- to a different logic
3679N/A if sys1 `disjoint` sys'' then return ()
0N/A else plain_error () "attempt to hide symbols from the local environment" (headPos pos)
0N/A mor1 <- generated_sign lid' (toList (sys1 `union` sys'')) sigma'
0N/A mor2 <- induced_from_morphism lid' rmap (dom lid' mor1)
0N/A return (gEmbed (G_morphism lid' mor1),
0N/A Just (gEmbed (G_morphism lid' mor2)))
0N/Aana_FIT_ARG gctx@(gannos,genv,dg) spname nsigI nsigP just_struct (Fit_spec asp gsis pos) = do
0N/A nP <- maybeToResult nullPos
0N/A "Internal error: empty parameter spec" (getNode nsigP)
0N/A (nsigA,dg') <- ana_SPEC gctx nsigI Nothing just_struct (item asp)
0N/A nA <- maybeToResult nullPos
0N/A "Internal error: empty argument spec" (getNode nsigA)
0N/A let gsigmaP = getSig nsigP
0N/A gsigmaA = getSig nsigA
0N/A gsigmaI = getSig nsigI
0N/A G_sign lidP sigmaP <- return gsigmaP
0N/A G_sign lidA sigmaA <- return gsigmaA
0N/A G_sign lidI sigmaI <- return gsigmaI
0N/A G_symb_map_items_list lid sis <- return gsis
0N/A rmap <- stat_symb_map_items lid sis
0N/A sigmaA' <- rcoerce lidA lidP (headPos pos) sigmaA
0N/A sigmaI' <- rcoerce lidI lidP (headPos pos) sigmaI
0N/A rmap' <- rcoerce lid lidP (headPos pos) rmap
0N/A mor <- induced_from_to_morphism lidP rmap' sigmaP sigmaA'
0N/A let symI = sym_of lidP sigmaI'
0N/A symmap_mor = symmap_of lidP mor
0N/A -- are symbols of the imports left untouched?
0N/A {- if setAll (\sy -> lookupFM symmap_mor sy == Just sy) symI
0N/A else plain_error () "Fitting morphism must not affect import" (headPos pos)
0N/A -} -- ??? does not work
0N/A -- ??? also output some symbol that is affected
0N/A let link = (nP,nA,DGLink {
0N/A dgl_morphism = gEmbed (G_morphism lidP mor),
0N/A dgl_type = GlobalThm False,
0N/A dgl_origin = DGSpecInst spname})
0N/A return (insEdge link dg',
0N/A (G_morphism lidP mor,nsigA)
271N/Aana_FIT_ARG gctx@(gannos,genv,dg) spname nsigI nsigP just_struct (Fit_view vn fas pos ans) = do
271N/A G_sign lid sigma <- return (getSig nsigP)
271N/A return (dg,(G_morphism lid (ide lid sigma),nsigP))
271N/A -- ??? Needs to be implemented
0N/AextendMorphism :: Pos -> G_sign -> G_sign -> G_sign -> G_morphism
0N/A -> Result(G_sign,G_morphism)
0N/AextendMorphism pos gsigma gsigma' gsigmaA mor =
0N/A return (gsigmaA,mor) -- ??? needs to be implemented
271N/Aapply_GS :: Pos -> ExtGenSig -> [(G_morphism,NodeSig)] -> Result(G_sign,G_morphism)
271N/Aapply_GS pos (nsigI,params,gsigmaP,nsigB) args = do
271N/A let mor_i = map fst args
271N/A gsigmaA_i = map (getSig . snd) args
0N/A gsigmaB = getSig nsigB
0N/A gsigmaI = getSig nsigI
0N/A G_sign lidI sigmaI <- return gsigmaI
0N/A let idI = ide lidI sigmaI
0N/A gsigmaA <- homogeneousGsigManyUnion pos gsigmaA_i
0N/A mor_f <- homogeneousMorManyUnion pos (G_morphism lidI idI:mor_i)
0N/A extendMorphism pos gsigmaP gsigmaB gsigmaA mor_f
0N/A-- | analyze a GENERICITY
0N/A-- Parameters: global context, current logic, just-structure-flag, GENERICITY
0N/Aana_GENERICITY :: GlobalContext -> AnyLogic -> Bool -> GENERICITY
0N/A -> Result (ExtGenSig,DGraph)
0N/Aana_GENERICITY (_,_,dg) l@(Logic lid) _
0N/A (Genericity (Params []) (Imported []) pos) =
0N/A return ((EmptyNode l,[],G_sign lid (empty_signature lid),EmptyNode l),dg)
0N/Aana_GENERICITY gctx@(gannos,genv,_) l just_struct (Genericity (Params [asp]) imps pos) = do
0N/A (nsigI,dg') <- ana_IMPORTS gctx l just_struct imps
0N/A (nsigP,dg'') <- ana_SPEC (gannos,genv,dg') nsigI Nothing just_struct (item asp)
0N/A return ((nsigI,[nsigP],getSig nsigP,nsigP),
271N/Aana_GENERICITY gctx@(gannos,genv,_) l just_struct (Genericity params imps pos) = do
0N/A (nsigI,dg') <- ana_IMPORTS gctx l just_struct imps
0N/A (nsigPs,dg'') <- ana_PARAMS (gannos,genv,dg') l nsigI just_struct params
0N/A gsigmaP <- homogeneousGsigManyUnion (headPos pos) (map getSig nsigPs)
0N/A G_sign lidP sigmaP <- return gsigmaP
271N/A let node_contents = DGNode {
0N/A dgn_sign = G_sign lidP (empty_signature lidP),
0N/A dgn_sens = G_l_sentence lidP [],
0N/A dgn_origin = DGFormalParams }
0N/A [node] = newNodes 0 dg''
0N/A dg''' = insNode (node,node_contents) dg''
0N/A case getNode nsig of
0N/A Just n -> insEdge (n,node,DGLink {
0N/A dgl_morphism = inclusion (getSig nsig) gsigmaP,
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGFormalParams }) dg
0N/A return ((nsigI,nsigPs,gsigmaP,NodeSig(node,gsigmaP)),
0N/A foldl inslink dg''' nsigPs)
0N/Aana_PARAMS :: GlobalContext -> AnyLogic -> NodeSig -> Bool -> PARAMS
0N/A -> Result ([NodeSig],DGraph)
0N/Aana_PARAMS gctx@(gannos,genv,dg) l nsigI just_struct (Params asps) = do
0N/A (pars,dg') <- foldl ana (return ([],dg)) (map item asps)
0N/A return (reverse pars,dg')
0N/A (par,dg') <- ana_SPEC (gannos,genv,dg) nsigI Nothing just_struct sp
0N/A return (par:pars,dg')
0N/Aana_IMPORTS :: GlobalContext -> AnyLogic -> Bool -> IMPORTED
0N/A -> Result (NodeSig,DGraph)
0N/Aana_IMPORTS gctx l just_struct (Imported asps) = do
0N/A let sp = Union asps (map (\_ -> nullPos) asps)
0N/A ana_SPEC gctx (EmptyNode l) Nothing just_struct sp
0N/A -- ??? emptyExplicit stuff needs to be added here
0N/A-- | analyze a VIEW_TYPE
0N/A-- The first three arguments give the global context
0N/A-- The AnyLogic is the current logic
0N/A-- The NodeSig is the signature of the parameter of the view
0N/A-- flag, whether just the structure shall be analysed
0N/Aana_VIEW_TYPE:: GlobalContext -> AnyLogic -> NodeSig -> Bool -> VIEW_TYPE
0N/A -> Result ((NodeSig,NodeSig),DGraph)
0N/Aana_VIEW_TYPE gctx@(gannos,genv,_) l parSig just_struct
0N/A (View_type aspSrc aspTar pos) = do
0N/A (srcNsig,dg') <- ana_SPEC gctx (EmptyNode l) Nothing just_struct (item aspSrc)
0N/A (tarNsig,dg'') <- ana_SPEC (gannos,genv,dg') parSig Nothing just_struct (item aspTar)
0N/A return ((srcNsig,tarNsig),dg'')
0N/A-- | Auxiliary function for not yet implemented features
0N/Aana_err :: String -> a
0N/A error ("*** Analysis of " ++ fname ++ " is not yet implemented!")