0N/ACopyright : (c) Till Mossakowski and Uni Bremen 2003-2006
0N/AMaintainer : till@tzi.de
0N/AStability : provisional
0N/AAnalysis of structured specifications
0N/A Follows the verfication semantic rules in Chap. IV:4.7
0N/A of the CASL Reference Manual.
1472N/A analysis of basic specs: use union of sigs
1472N/A analysis of instantiations:
1472N/A if necessary, translate body along inclusion comorphism
0N/A Improve efficiency by storing local signature fragments only
1879N/A spec <name> not found: line number!
4141N/A Issue warning for unions of non-disjoint signatures
1879N/A (and offer tool for renaming?)
1879N/A Check that translations and reductions do not effect local env
0N/A (Implement new semantics for revealing here)
0N/A Should we use institution independent analysis over the Grothendieck logic?
0N/A abstract syntax + devgraph would have to be changed to homogeneous case
0N/A logic translations are symbol maps in the Grothendieck logic
0N/A Problem with this approach: symbol functor goes into rel,
0N/A and induced_from_morphism gets difficult to implement
0N/A Unions need inclusion morphisms. Should these play a special role?
0N/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 No optimization of heterogeneous unions!
0N/A (or perhaps abandon optimized unions at all and
2941N/A replace compHomInclusion with comp Grothendieck? is this more efficient?)
2941N/A Treatment of translations and reductions along logic translations
2941N/A may local env be translated, and even reduced, along logic translations?
2941N/A if yes: how is local env linked to signature of resulting spec?
2941N/A (important
e.g. for checking that local env is not being renamed?)
2941N/A does signature+comorphism suffice, such that c(local env)\subseteq sig?
2941N/A if no: this means that only closed specs may be translated
2941N/A Revealings without translations: just one arrow
2941N/A Pushouts: only admissible within one logic?
2941N/A Instantiations with formal parameter: add no new internal nodes
2941N/A Union nodes can be extended by a basic spec directly (no new node needed)
2941N/A no new nodes for trivial translations
2941N/A Basic specs: if local env node is otherwise unused, overwrite it with
2941N/A Ensure that just_struct option leads to disabling of various dg operations
2941N/A (show sig, show mor, proving)
2941N/A local: better error message for the following
2941N/Aspec GenCardinality [sort Subject,Object;
2941N/A pred predicate : Subject * Object] =
2941N/A Set [sort Object fit sort Elem |-> Object]
2941N/A reveal Set[Object], #__, __eps__,
2941N/A Nat,0,1,2,3,4,5,6,7,8,9,__@@__,__>=__,__<=__
2941N/A op toSet : Subject -> Set [Object]
2941N/A forall x : Subject; y : Object
2941N/A . predicate (x,y) <=> y eps toSet(x)
2941N/A pred minCardinality(s: Subject;n: Nat) <=>
2941N/A maxCardinality(s: Subject;n: Nat) <=>
2941N/A cardinality(s: Subject;n: Nat) <=>
2941N/A%%} hide Pos,toSet,Set[Object],#__,__eps__,__<=__,__>=__
2941N/A ana_VIEW_TYPE, ana_err, isStructured,
2941N/A ana_RENAMING, ana_RESTRICTION,
2941N/A homogenizeGM, extendMorphism)
0N/AinsEdgeNub :: LEdge DGLinkLab -> DGraph -> DGraph
0N/AinsEdgeNub (v, w, l) g =
0N/A if (l, w) `elem` s then g
0N/A else (p, v, l', (l, w) : s) & g'
0N/A where (Just (p, _, l', s), g') = match v g
0N/A-- Parameters: global context, local environment,
0N/A-- the SIMPLE_ID may be a name if the specification shall be named,
0N/A-- options: here we need the info: shall only the structure be analysed?
0N/Aana_SPEC :: LogicGraph -> GlobalContext -> MaybeNode -> NODE_NAME ->
1753N/A HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, GlobalContext)
0N/Aana_SPEC lg gctx nsig name opts sp =
0N/A let dg = devGraph gctx
342N/A Basic_spec (G_basic_spec lid bspec) ->
342N/A do G_sign lid' sigma' i1 <- return (getMaybeSig nsig)
342N/A sigma <- coerceSign lid' lid "Analysis of basic spec" sigma'
342N/A (bspec', sigma_complete, ax) <-
342N/A then return (bspec, empty_signature lid, [])
0N/A else do b <- maybeToMonad
0N/A ("no basic analysis for logic "
0N/A ++ language_name lid)
0N/A (basic_analysis lid)
0N/A b (bspec, sigma, globalAnnos gctx)
0N/A incl <- ginclusion lg
2941N/A (G_sign lid sigma i1) (G_sign lid sigma_complete (k+1))
0N/A dgn_theory = G_theory lid sigma_complete (k+1) (toThSens ax) 0,
0N/A -- no, not only the delta
0N/A dgn_sigma = Nothing,
0N/A dgn_origin = DGBasic,
0N/A dgn_cons_status = LeftOpen }
0N/A node = getNewNode dg
0N/A dg' = insNode (node,node_contents) dg
0N/A incl' = updateMorIndex (j+1) incl
0N/A dgl_morphism = incl',
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGExtension }
0N/A JustNode (NodeSig n _) -> insEdgeNub (n,node,link) dg'
0N/A return (Basic_spec (G_basic_spec lid bspec'),
0N/A NodeSig node $ G_sign lid sigma_complete (k+1),
0N/A gctx { devGraph = dg''
0N/A (G_sign lid sigma_complete (k+1)) sgMap
0N/A Translation asp ren ->
0N/A do let sp1 = item asp
0N/A (sp1', NodeSig n' gsigma, gctx') <-
0N/A ana_SPEC lg gctx nsig (inc name) opts sp1
0N/A mor <- ana_RENAMING lg nsig gsigma opts 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' gsig ind <- return gsigma'
0N/A let node_contents = DGNode {
0N/A dgn_theory = G_theory lid' gsig ind noSens 0,
0N/A dgn_sigma = Nothing,
0N/A dgn_origin = DGTranslation,
0N/A dgn_cons_status = LeftOpen }
0N/A dg' = devGraph gctx'
0N/A node = getNewNode dg'
0N/A link = (n',node,DGLink {
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGTranslation })
0N/A return (Translation (replaceAnnoted sp1' asp) ren,
0N/A NodeSig node gsigma',
0N/A gctx' { devGraph = insEdgeNub link $
0N/A insNode (node,node_contents) dg' })
0N/A Reduction asp restr ->
0N/A do let sp1 = item asp
0N/A (sp1', NodeSig n' gsigma', gctx') <-
0N/A ana_SPEC lg gctx nsig (inc name) opts sp1
0N/A let gsigma = getMaybeSig nsig
0N/A dg' = devGraph gctx'
0N/A (hmor,tmor) <- ana_RESTRICTION dg gsigma gsigma' opts 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
989N/A G_sign lid' gsig ind <- return gsigma''
0N/A let node_contents = DGNode {
0N/A dgn_theory = G_theory lid' gsig ind noSens 0,
989N/A dgn_cons_status = LeftOpen }
989N/A link = (n',node,DGLink {
989N/A dgl_origin = DGHiding })
989N/A return (Reduction (replaceAnnoted sp1' asp) restr,
0N/A NodeSig node gsigma'',
0N/A gctx' { devGraph = insEdgeNub link $
0N/A insNode (node,node_contents) dg' })
2390N/A let gsigma1 = dom Grothendieck tmor'
2390N/A gsigma'' = cod Grothendieck tmor'
0N/A -- ??? too simplistic for non-comorphism inter-logic reductions
0N/A G_sign lid1 gsig ind <- return gsigma1
1753N/A G_sign lid'' gsig'' ind'' <- return gsigma''
0N/A -- the case with identity translation leads to a simpler dg
0N/A if tmor' == ide Grothendieck (dom Grothendieck tmor')
0N/A dgn_theory = G_theory lid1 gsig ind noSens 0,
0N/A dgn_sigma = Nothing,
0N/A dgn_origin = DGRevealing,
0N/A dgn_cons_status = LeftOpen }
989N/A link1 = (n',node1,DGLink {
0N/A dgl_type = HidingDef,
0N/A dgl_origin = DGRevealing })
989N/A return (Reduction (replaceAnnoted sp1' asp) restr,
0N/A NodeSig node1 gsigma1,
0N/A gctx' { devGraph = insEdgeNub link1 $
0N/A insNode (node1,node_contents1) dg' } )
0N/A let [node1,node''] = newNodes 2 dg'
0N/A node_contents1 = DGNode {
989N/A dgn_name = extName "T" name,
0N/A dgn_theory = G_theory lid1 gsig ind noSens 0,
0N/A dgn_sigma = Nothing,
0N/A dgn_origin = DGRevealing,
0N/A dgn_cons_status = LeftOpen }
342N/A link1 = (n',node1,DGLink {
0N/A dgl_morphism = hmor,
0N/A dgl_type = HidingDef,
0N/A dgl_origin = DGRevealing })
0N/A node_contents'' = DGNode {
2941N/A dgn_theory = G_theory lid'' gsig'' ind'' noSens 0,
2941N/A dgn_origin = DGRevealTranslation,
2941N/A dgn_cons_status = LeftOpen }
2941N/A link'' = (node1,node'',DGLink {
0N/A dgl_morphism = tmor',
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGRevealTranslation })
0N/A return (Reduction (replaceAnnoted sp1' asp) restr,
0N/A NodeSig node'' gsigma'',
0N/A gctx' { devGraph = insEdgeNub link'' $
0N/A insNode (node'',node_contents'') $
0N/A insNode (node1,node_contents1) dg' })
0N/A Union [] pos -> adjustPos pos $ fail $ "empty union"
0N/A do let sps = map item asps
0N/A (sps', nsigs, gctx', _) <-
4141N/A (sp1,nsig',dg1) <- ana_SPEC lg dg' nsig n opts sp'
4141N/A return (sp1:sps1,nsig':nsigs,dg1,inc n)
4141N/A in foldl ana (return ([], [], gctx, extName "U" name)) sps
0N/A dg' = devGraph gctx'
0N/A gbigSigma <- adj $ gsigManyUnion lg (map getSig nsigs')
0N/A G_sign lid' gsig ind <- return gbigSigma
0N/A let node_contents = DGNode {
0N/A dgn_theory = G_theory lid' gsig ind noSens 0,
0N/A dgn_sigma = Nothing,
0N/A dgn_origin = DGUnion,
0N/A dgn_cons_status = LeftOpen }
0N/A node = getNewNode dg'
0N/A insE dgres (NodeSig n gsigma) = do
0N/A incl <- adj $ ginclusion lg gsigma gbigSigma
0N/A dgl_morphism = incl,
0N/A dgl_type = GlobalDef,
0N/A dgl_origin = DGUnion }
0N/A return (insEdgeNub (n,node,link) dg1)
0N/A dg'' <- foldl insE (return (insNode (node,node_contents) dg')) nsigs'
0N/A return (Union (map (uncurry replaceAnnoted)
0N/A (zip (reverse sps') asps))
0N/A NodeSig node gbigSigma,
0N/A gctx' { devGraph = dg'' })
0N/A Extension asps pos -> do
0N/A (sps',nsig1',dg1) <- foldl ana (return ([], nsig, gctx)) namedSps
0N/A EmptyNode _ -> fail "empty extension"
342N/A JustNode nsig1 -> return (Extension (map (uncurry replaceAnnoted)
342N/A (zip (reverse sps') asps))
0N/A namedSps = zip (reverse (name: tail (take (length asps)
1879N/A (iterate inc (extName "E" name)))))
ana res (name',asp') = do
(sps', nsig', dg') <- res
(sp1', nsig1@(NodeSig n1 sig1), gctx1) <-
ana_SPEC lg dg' nsig' name' opts (item asp')
-- insert theorem link for semantic annotations
-- take the first semantic annotation
let anno = find isSemanticAnno $ l_annos asp'
-- is the extension going between real nodes?
dg2 <- case (anno, nsig') of
(Just anno0@(Semantic_anno anno1 _), JustNode (NodeSig n' sig')) -> do
-- any other semantic annotation? that's an error
when (any (\an -> isSemanticAnno an && an/=anno0) $ l_annos asp')
(plain_error () "Conflicting semantic annotations"
-- %implied should not occur here
"Annotation %implied should come after a BASIC-ITEM"
if anno1==SA_implies then do
when (not (isHomSubGsign sig1 sig')) (plain_error ()
"Signature must not be extended in presence of %implies"
-- insert a theorem link according to p. 319 of the CASL Reference Manual
return $ insEdgeNub (n1,n',DGLink {
dgl_morphism = ide Grothendieck sig1,
dgl_type = GlobalThm LeftOpen None LeftOpen,
dgl_origin = DGExtension }) dg1
let anno2 = case anno1 of
-- insert a theorem link according to p. 319 of the CASL Reference Manual
-- the theorem link is trivally proved by the parallel definition link,
-- but for clarity, we leave it open here
-- the interesting open proof obligation is anno2, of course
incl <- ginclusion lg sig' sig1
return $ insEdgeNub (n',n1,DGLink {
dgl_type = GlobalThm LeftOpen anno2 LeftOpen,
dgl_origin = DGExtension }) dg1
return (sp1':sps', JustNode nsig1, gctx1 { devGraph = dg2 })
(sp', NodeSig n' gsigma'@(G_sign lid' gsig ind), gctx') <-
ana_SPEC lg gctx nsig (inc name) opts sp1
incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
let node_contents = DGNode {
dgn_theory = G_theory lid' gsig ind noSens 0, -- delta is empty
dgn_cons_status = LeftOpen }
return (Free_spec (replaceAnnoted sp' asp) poss,
gctx' { devGraph = insEdgeNub link $
insNode (node,node_contents) dg' })
(sp', NodeSig n' gsigma'@(G_sign lid' gsig ind), gctx') <-
ana_SPEC lg gctx nsig (inc name) opts sp1
incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
let node_contents = DGNode {
dgn_theory = G_theory lid' gsig ind noSens 0, -- delta is empty
dgn_cons_status = LeftOpen }
dgl_type = CofreeDef nsig,
return (Cofree_spec (replaceAnnoted sp' asp) poss,
gctx' { devGraph = insEdgeNub link $
insNode (node,node_contents) dg' })
Local_spec asp asp' poss ->
(sp2, nsig'@(NodeSig _ (G_sign lid' sigma' _)), dg') <-
ana_SPEC lg gctx nsig (extName "L" name) opts sp1
(sp2', NodeSig n'' (G_sign lid'' sigma'' _), gctx'') <-
ana_SPEC lg dg' (JustNode nsig') (inc name) opts sp1'
let gsigma = getMaybeSig nsig
G_sign lid sigma _<- return gsigma
sigma1 <- coerceSign lid' lid "Analysis of local spec" sigma'
sigma2 <- coerceSign lid'' lid "Analysis of local spec" sigma''
let sys = sym_of lid sigma
mor3 <- if isStructured opts then return (ide lid sigma2)
else adjustPos pos $ cogenerated_sign lid
let sigma3 = dom lid mor3
-- gsigma2 = G_sign lid sigma2
gsigma3 = G_sign lid sigma3 0
when (not( isStructured opts ||
"attempt to hide the following symbols from the local environment:\n"
let node_contents = DGNode {
dgn_theory = G_theory lid sigma3 0 noSens 0,
dgn_cons_status = LeftOpen }
link = (n'',node,DGLink {
dgl_morphism = gEmbed2 gsigma3 (G_morphism lid mor3 0),
return (Local_spec (replaceAnnoted sp2 asp)
(replaceAnnoted sp2' asp')
gctx'' { devGraph = insEdgeNub link $
insNode (node,node_contents) dg'' })
-- analyse spec with empty local env
(sp', NodeSig n' gsigma', gctx') <-
ana_SPEC lg gctx (EmptyNode l) (inc name) opts sp1
let gsigma = getMaybeSig nsig
gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
G_sign lid'' gsig'' ind <- return gsigma''
incl1 <- adj $ ginclusion lg gsigma gsigma''
incl2 <- adj $ ginclusion lg gsigma' gsigma''
let node = getNewNode dg'
dgn_theory = G_theory lid'' gsig'' ind noSens 0,
dgn_cons_status = LeftOpen }
dgl_origin = DGClosedLenv }
link2 = (n',node,DGLink {
JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
return (Closed_spec (replaceAnnoted sp' asp) pos,
gctx' { devGraph = insLink1 $
insNode (node,node_contents) dg' })
Qualified_spec (Logic_name ln sublog) asp pos -> do
l <- lookupLogic "Static analysis: " (tokStr ln) lg
-- analyse spec with empty local env
(sp', NodeSig n' gsigma', gctx') <-
ana_SPEC lg gctx (EmptyNode l) (inc name) opts (item asp)
-- construct union with local env
let gsigma = getMaybeSig nsig
gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
G_sign lid'' gsig'' ind <- return gsigma''
incl1 <- adj $ ginclusion lg gsigma gsigma''
incl2 <- adj $ ginclusion lg gsigma' gsigma''
let node = getNewNode dg'
dgn_theory = G_theory lid'' gsig'' ind noSens 0,
dgn_origin = DGLogicQual,
dgn_cons_status = LeftOpen }
dgl_origin = DGLogicQualLenv }
link2 = (n',node,DGLink {
dgl_origin = DGLogicQual })
JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
return (Qualified_spec (Logic_name ln sublog)
(replaceAnnoted sp' asp) pos,
gctx' { devGraph = insLink1 $
insNode (node,node_contents) dg' })
(sp',nsig',dg') <- ana_SPEC lg gctx nsig name opts (item asp)
return (Group (replaceAnnoted sp' asp) pos,nsig',dg')
Spec_inst spname afitargs pos -> do
("Specification " ++ spstr ++ " not found") pos
(spstr ++ " is a view, not a specification") pos
" is an architectural, not a structured specification") pos
" is a unit specification, not a structured specification") pos
" is a refinement specification, not a structured specification") pos
Just (SpecEntry gs@(imps,params,_,body@(NodeSig nB gsigmaB))) ->
case (\x y -> (x,x-y)) (length afitargs) (length params) of
-- the case without parameters leads to a simpler dg
gsigma@(G_sign lid gsig ind) <-
adj $ gsigUnion lg (getMaybeSig nsig) gsigmaB
-- the subcase with empty local env leads to an even simpler dg
-- if the node shall not be named and the logic does not change,
if isInternal name && langNameSig gsigma==langNameSig gsigmaB
-- then just return the body
then return (sp, body, gctx)
-- otherwise, we need to create a new one
incl <- adj $ ginclusion lg gsigmaB gsigma
dgn_theory = G_theory lid gsig ind noSens 0,
dgn_origin = DGSpecInst spname,
dgn_cons_status = LeftOpen}
dgl_origin = DGSpecInst spname})
gctx { devGraph = insEdgeNub link $
insNode (node,node_contents) dg })
-- the subcase with nonempty local env
JustNode (NodeSig n sigma) -> do
incl1 <- adj $ ginclusion lg sigma gsigma
incl2 <- adj $ ginclusion lg gsigmaB gsigma
dgn_theory = G_theory lid gsig ind noSens 0,
dgn_origin = DGSpecInst spname,
dgn_cons_status = LeftOpen}
dgl_origin = DGSpecInst spname})
link2 = (nB,node,DGLink {
dgl_origin = DGSpecInst spname})
gctx { devGraph = insEdgeNub link1 $
insNode (node,node_contents) dg })
-- now the case with parameters
let fitargs = map item afitargs
(fitargs', gctx', args, _) <-
foldl anaFitArg (return ([], gctx, [], extName "A" name))
let actualargs = reverse args
(gsigma',morDelta) <- adj $ apply_GS lg gs actualargs
gsigmaRes <- adj $ gsigUnion lg (getMaybeSig nsig) gsigma'
G_sign lidRes gsigRes ind <- return gsigmaRes
incl1 <- adj $ ginclusion lg (getMaybeSig nsig) gsigmaRes
incl2 <- adj $ ginclusion lg gsigma' gsigmaRes
morDelta' <- comp Grothendieck (gEmbed morDelta) incl2
let node = getNewNode dg'
dgn_theory = G_theory lidRes gsigRes ind noSens 0,
dgn_origin = DGSpecInst spname,
dgn_cons_status = LeftOpen}
dgl_origin = DGSpecInst spname}
JustNode (NodeSig n _) -> insEdgeNub (n, node, link1)
link2 = (nB,node,DGLink {
dgl_morphism = morDelta',
dgl_origin = DGSpecInst spname})
parLinks = catMaybes (map (parLink gsigmaRes node) actualargs)
(map (uncurry replaceAnnoted)
(zip (reverse fitargs') afitargs))
gctx' { devGraph = foldr insEdgeNub
insNode (node,node_contents) dg')
anaFitArg res (nsig',fa) = do
(fas',dg1,args,name') <- res
(fa',dg',arg) <- ana_FIT_ARG lg dg1 spname imps nsig' opts name' fa
return (fa':fas',dg',arg:args,inc name')
parLink gsigma' node (_mor_i, NodeSig nA_i sigA_i) = do
incl <- maybeResult $ ginclusion lg sigA_i gsigma'
-- finally the case with conflicting numbers of formal and actual parameters
(spstr ++ " expects " ++ show (length params) ++ " arguments"
++ " but was given " ++ show (length afitargs)) pos
Data (Logic lidD) (Logic lidP) asp1 asp2 pos ->
Comorphism cid <- adj $ logicInclusion lg (Logic lidD) (Logic lidP)
let lidD' = sourceLogic cid
(sp1', NodeSig n' (G_sign lid' sigma' _), gctx1) <-
ana_SPEC lg gctx (EmptyNode (Logic lidD)) (inc name) opts sp1
sigmaD <- adj $ coerceSign lid' lidD' "Analysis of data spec" sigma'
(sigmaD',sensD') <- adj $ map_sign cid sigmaD
let gsigmaD' = G_sign lidP' sigmaD' 0
dgn_theory = G_theory lidP' sigmaD' 0 (toThSens sensD') 0,
dgn_cons_status = LeftOpen }
dgl_morphism = GMorphism cid sigmaD 0 (ide lidP' sigmaD') 0,
insNode (node,node_contents) dg1
nsig2 = NodeSig node gsigmaD'
ana_SPEC lg gctx1 { devGraph = dg2 } (JustNode nsig2) name opts sp2
return (Data (Logic lidD) (Logic lidP)
(replaceAnnoted sp1' asp1)
(replaceAnnoted sp2' asp2)
ana_ren1 :: LogicGraph -> MaybeNode -> Range -> GMorphism -> G_mapping
ana_ren1 _ lenv _pos (GMorphism r sigma ind1 mor ind2)
(G_symb_map (G_symb_map_items_list lid sis)) = do
sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis
rmap <- stat_symb_map_items lid2 sis1
mor1 <- induced_from_morphism lid2 rmap (cod lid2 mor)
JustNode (NodeSig _ (G_sign lidLenv sigmaLenv _)) -> do
-- needs to be changed for logic translations
sigmaLenv' <- coerceSign lidLenv lid2
"Analysis of renaming: logic translations not yet properly handeled"
let sysLenv = sym_of lid2 sigmaLenv'
{- when (not (forbiddenSys ==
Set.empty)) $ plain_error () (
"attempt to rename the following symbols from the local environment:\n"
++ showDoc forbiddenSys "") pos
mor2 <- comp lid2 mor mor1
return $ GMorphism r sigma ind1 mor2 ind2
ana_ren1 lg _ _ mor (G_logic_translation (Logic_code tok src tar pos1)) = do
G_sign srcLid srcSig ind<- return (cod Grothendieck mor)
Comorphism cid <- lookupComorphism (tokStr ctok) lg
when (isJust src && getLogicStr (fromJust src) /=
language_name (sourceLogic cid))
(fail (getLogicStr (fromJust src) ++
"is not the source logic of "
when (isJust tar && getLogicStr (fromJust tar) /=
language_name (targetLogic cid))
(fail (getLogicStr (fromJust tar) ++
"is not the target logic of "
Just (Logic_name l _) -> do
tarL <- lookupLogic "with logic: " (tokStr l) lg
logicInclusion lg (Logic srcLid) tarL
Nothing -> fail "with logic: cannot determine comorphism"
mor1 <- adj $ gEmbedComorphism c (G_sign srcLid srcSig ind)
adj $ comp Grothendieck mor mor1
where getLogicStr (Logic_name l _) = tokStr l
ana_ren :: LogicGraph -> MaybeNode -> Range -> Result GMorphism -> G_mapping
ana_ren lg lenv pos mor_res ren =
ana_ren1 lg lenv pos mor ren
ana_RENAMING :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING
ana_RENAMING lg lenv gSigma opts (Renaming ren pos) =
then return (ide Grothendieck gSigma)
else foldl (ana_ren lg lenv pos) (return (ide Grothendieck gSigma)) ren
-- analysis of restrictions
ana_restr1 :: DGraph -> G_sign -> Range -> GMorphism -> G_hiding
ana_restr1 _ (G_sign lidLenv sigmaLenv _) pos
(GMorphism cid sigma1 _ mor _)
(G_symb_list (G_symb_items_list lid' sis')) = do
let lid1 = sourceLogic cid
sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction" sis'
rsys <- stat_symb_items lid1 sis1
let sys = sym_of lid1 sigma1
sys' =
Set.filter (\sy -> any (\rsy -> matches lid1 sy rsy) rsys)
-- needs to be changed when logic projections are implemented
sigmaLenv' <- coerceSign lidLenv lid1
"Analysis of restriction: logic projections not yet properly handeled"
let sysLenv = sym_of lid1 sigmaLenv'
"attempt to hide the following symbols from the local environment:\n"
++ showDoc forbiddenSys "") pos
mor1 <- cogenerated_sign lid1 sys' sigma1
mor1' <- map_morphism cid mor1
mor2 <- comp lid2 mor1' mor
return $ GMorphism cid (dom lid1 mor1) 0 mor2 0
ana_restr1 _dg _gSigma _mor _pos
(G_logic_projection (Logic_code _tok _src _tar pos1)) =
fatal_error "no analysis of logic projections yet" pos1
ana_restr :: DGraph -> G_sign -> Range -> Result GMorphism -> G_hiding
ana_restr dg gSigma pos mor_res restr =
ana_restr1 dg gSigma pos 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 pos) =
do mor <- foldl (ana_restr dg gSigma pos)
(return (ide Grothendieck gSigma'))
-- ??? 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
sis' <- adj $ coerceSymbMapItemsList lid1 lid'
"Analysis of restriction" sis
rmap <- adj $ stat_symb_map_items lid' sis'
-- 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
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 0),
Just (gEmbed (G_morphism lid' mor2 0)))
ana_FIT_ARG :: LogicGraph -> GlobalContext -> SPEC_NAME -> MaybeNode
-> NodeSig -> HetcatsOpts -> NODE_NAME -> FIT_ARG
-> Result (FIT_ARG, GlobalContext, (G_morphism,NodeSig))
ana_FIT_ARG lg gctx spname nsigI
(NodeSig nP (G_sign lidP sigmaP _)) opts name
(Fit_spec asp gsis pos) = do
(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)
rmap <- stat_symb_map_items lid sis
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
else plain_error () "Fitting morphism must not affect import" pos
-- ??? also output some symbol that is affected
let link = (nP,nA,DGLink {
dgl_morphism = gEmbed (G_morphism lidP mor 0),
dgl_type = GlobalThm LeftOpen None LeftOpen,
dgl_origin = DGSpecInst spname})
return (Fit_spec (replaceAnnoted sp' asp) gsis pos,
gctx { devGraph = insEdgeNub link $ devGraph dg' },
(G_morphism lidP mor 0,nsigA)
ana_FIT_ARG lg gctx spname nsigI (NodeSig nP gsigmaP)
opts name fv@(Fit_view vn afitargs pos) = do
("View " ++ tokStr vn ++ " not found") pos
(spstr ++ " is a specification, not a view") pos
" is an architectural specification, not a view ") pos
" is a unit specification, not a view") pos
" is a refinement specification, not a view") pos
Just (ViewEntry (src,mor,gs@(imps,params,_,target))) -> do
gsigmaI = getMaybeSig nsigI
GMorphism cid _ _ morHom ind<- return mor
let lid = targetLogic cid
when (not (language_name (sourceLogic cid) == language_name lid))
"heterogeneous fitting views not yet implemented"
case (\x y -> (x,x-y)) (length afitargs) (length params) of
-- the case without parameters leads to a simpler dg
-- the subcase with empty import leads to a simpler dg
let link = (nP,nSrc,DGLink {
dgl_morphism = ide Grothendieck gsigmaP,
dgl_type = GlobalThm LeftOpen None LeftOpen,
dgl_origin = DGFitView spname})
return (fv, gctx { devGraph = insEdgeNub link dg },
(G_morphism lid morHom ind, target))
-- the subcase with nonempty import
JustNode (NodeSig nI _) -> do
gsigmaIS <- adj $ gsigUnion lg gsigmaI gsigmaS
when (not (isSubGsign lg gsigmaP gsigmaIS))
("Parameter does not match source of fittig view. "
++ "Parameter signature:\n"
"\nSource signature of fitting view (united with import):\n"
++ showDoc 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 indA <- return gsigmaA
G_sign lidP gsigP indP <- 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_theory = G_theory lidA gsigA indA noSens 0,
dgn_origin = DGFitViewA spname,
dgn_cons_status = LeftOpen}
node_contents' = DGNode {
dgn_theory = G_theory lidP gsigP indP noSens 0,
dgn_origin = DGFitView spname,
dgn_cons_status = LeftOpen}
dgl_morphism = ide Grothendieck gsigmaP,
dgl_type = GlobalThm LeftOpen None LeftOpen,
dgl_origin = DGFitView spname})
link1 = (nSrc,n',DGLink {
dgl_origin = DGFitView spname})
link2 = (nTar,nA,DGLink {
dgl_origin = DGFitViewA spname})
dgl_origin = DGFitViewImp spname})
dgl_origin = DGFitViewAImp spname})
return (fv, gctx { devGraph =
insNode (nA,node_contentsA) $
insNode (n',node_contents') dg },
(G_morphism lid mor_I 0, NodeSig nA gsigmaA))
-- now the case with parameters
let fitargs = map item afitargs
(fitargs', gctx', args,_) <-
foldl anaFitArg (return ([], gctx, [], extName "A" name))
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 indRes<- 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))
("heterogeneous fitting views not yet implemented")
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 indP <- return gsigmaP
node_contentsA = DGNode {
dgn_theory = G_theory lidRes gsigRes indRes noSens 0,
dgn_origin = DGFitViewA spname,
dgn_cons_status = LeftOpen}
node_contents' = DGNode {
dgn_name = extName "V" name,
dgn_theory = G_theory lidP gsigP indP noSens 0,
dgn_origin = DGFitView spname,
dgn_cons_status = LeftOpen}
dgl_morphism = ide Grothendieck gsigmaP,
dgl_type = GlobalThm LeftOpen None LeftOpen,
dgl_origin = DGFitView spname})
link1 = (nSrc,n',DGLink {
dgl_origin = DGFitView spname})
link2 = (nTar,nA,DGLink {
dgl_origin = DGFitViewA spname})
fitLinks = [link,link1,link2] ++ case nsigI of
JustNode (NodeSig nI _) -> let
dgl_origin = DGFitViewImp spname})
dgl_origin = DGFitViewAImp spname})
parLinks = catMaybes (map (parLink gsigmaRes nA) actualargs)
(map (uncurry replaceAnnoted)
(zip (reverse fitargs') afitargs))
gctx' { devGraph = foldr insEdgeNub
(insNode (nA,node_contentsA) $
insNode (n',node_contents') dg')
(fitLinks ++ parLinks) },
(G_morphism lid1 theta 0, NodeSig nA gsigmaRes))
anaFitArg res (nsig',fa) = do
(fas',dg1,args,name') <- res
(fa',dg',arg) <- ana_FIT_ARG lg 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
dgl_origin = DGFitView spname }
-- finally the case with conflicting numbers of formal and actual parameters
(spstr ++ " expects " ++ show (length params) ++ " arguments"
++ " but was given " ++ show (length afitargs)) pos
-- Extension of signature morphisms (for instantitations)
-- first some auxiliary functions
mapID idmap i@(Id toks comps pos1) =
compsnew <- sequence $ map (mapID idmap) comps
return (Id toks compsnew pos1)
Just ids -> if
Set.null ids then return i else
("Identifier component " ++ showId i
" can be mapped in various ways:\n"
++ showDoc ids "") $ getRange i
-> Result (EndoMap Id) -> Result (EndoMap Id)
extID1 idmap i@(Id toks comps pos1) m = do
compsnew <- sequence $ map (mapID idmap) comps
else return (
Map.insert i (Id toks compsnew pos1) m1)
extendMorphism :: G_sign -- ^ formal parameter
-> 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
rh = symbMapToRawSymbMap h
(\sy1 sy2 ->
Rel.setInsert (sym_name lid sy1) (sym_name lid sy2))
(id_to_raw lid id1) (id_to_raw lid id2))
-- do we need combining function catching the clashes???
mor <- induced_from_morphism lid r sigmaB
let hmor = symmap_of lid mor
sigma <- final_union lid sigmaA sigmaAD
(plain_error () ("Symbols shared between actual parameter and body"
++ "\nmust be in formal parameter:\n"
++ showDoc illShared "") nullRange)
comb2 p qs [] ++ comb1 qs
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))
"Fitting morphism leads to forbidden identifications:\n"
++ showDoc newIdentifications "") nullRange)
incl <- inclusion lid sigmaAD sigma
mor1 <- comp lid mor incl
return (G_sign lid sigma 0, G_morphism lid mor1 0)
apply_GS :: LogicGraph -> ExtGenSig -> [(G_morphism,NodeSig)]
-> Result(G_sign,G_morphism)
apply_GS lg (nsigI,_params,gsigmaP,nsigB) args = do
gsigmaA_i = map (getSig . snd) args
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 0: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, GlobalContext)
ana_GENERICITY _ gctx l _ _
gen@(Genericity (Params []) (Imported imps) pos) = do
(plain_error () "Parameterless specifications must not have imports"
return (gen,(EmptyNode l, [], EmptyNode l), gctx)
ana_GENERICITY lg gctx 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 dg' nsigI
return (Genericity (Params [replaceAnnoted sp' asp]) imps' pos,
(nsigI, [nsigP], JustNode nsigP), dg'')
-- ... and more parameters
ana_GENERICITY lg gctx l opts name
(Genericity params imps pos) = do
(imps',nsigI,dg') <- ana_IMPORTS lg gctx l opts (extName "I" name) imps
(params',nsigPs,gctx'') <-
ana_PARAMS lg dg' l nsigI opts (inc name) params
gsigmaP <- adj $ gsigManyUnion lg (map getSig nsigPs)
G_sign lidP gsigP indP <- return gsigmaP
let node_contents = DGNode {
dgn_theory = G_theory lidP gsigP indP noSens 0,
dgn_origin = DGFormalParams,
dgn_cons_status = LeftOpen }
dg''' = insNode (node,node_contents) dg''
inslink dgres (NodeSig n sigma) = do
incl <- adj $ ginclusion lg sigma gsigmaP
return (insEdgeNub (n,node,DGLink {
dgl_origin = DGFormalParams }) dg)
dg4 <- foldl inslink (return dg''') nsigPs
return (Genericity params' imps' pos,
(nsigI, nsigPs, JustNode $ NodeSig node gsigmaP),
ana_PARAMS :: LogicGraph -> GlobalContext -> AnyLogic -> MaybeNode
-> HetcatsOpts -> NODE_NAME -> PARAMS
-> Result (PARAMS, [NodeSig], GlobalContext)
ana_PARAMS lg gctx _ nsigI opts name (Params asps) = do
(sps',pars,dg',_) <- foldl ana (return ([], [], gctx, name))
return (Params (map (uncurry replaceAnnoted)
(zip (reverse sps') asps)),
(sp',par,dg') <- ana_SPEC lg dg1 nsigI n opts sp
return (sp':sps',par:pars,dg',inc n)
ana_IMPORTS :: LogicGraph -> GlobalContext -> AnyLogic -> HetcatsOpts
-> Result (IMPORTED, MaybeNode, GlobalContext)
ana_IMPORTS lg gctx l opts name imps@(Imported asps) =
[] -> return (imps, EmptyNode l, gctx)
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
-- 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), GlobalContext)
ana_VIEW_TYPE lg gctx l parSig opts name
(View_type aspSrc aspTar pos) = do
ana_SPEC lg gctx (EmptyNode l) (extName "S" name) opts (item aspSrc)
(extName "T" name) opts (item aspTar)
return (View_type (replaceAnnoted spSrc' aspSrc)
(replaceAnnoted spTar' aspTar)
(srcNsig, tarNsig), dg'')
-> Result G_symb_map_items_list
homogenizeGM (Logic lid) gsis =
foldl homogenize1 (return (G_symb_map_items_list lid [])) gsis
(G_symb_map_items_list lid2 sis) <- res
sis1' <- coerceSymbMapItemsList lid1 lid2 "" sis1
return $ G_symb_map_items_list lid2 $ sis ++ sis1'
-- | check if structured analysis should be performed
isStructured :: HetcatsOpts -> Bool
isStructured a = case analysis a of
-- | Auxiliary function for not yet implemented features
ana_err f = error $ "*** Analysis of " ++ f ++ " is not yet implemented!"