0N/ADescription : static analysis of heterogeneous structured specifications
0N/ACopyright : (c) Till Mossakowski and Uni Bremen 2003-2006
0N/AMaintainer : till@informatik.uni-bremen.de
0N/AStability : provisional
0N/AStatic analysis of CASL (heterogeneous) structured specifications
0N/A Follows the verfication semantic rules in Chap. IV:4.7
0N/A of the CASL Reference Manual.
0N/AcoerceMaybeNode :: LogicGraph -> DGraph -> MaybeNode -> NodeName -> AnyLogic
0N/A -> Result (MaybeNode, DGraph)
0N/AcoerceMaybeNode lg dg mn nn l2 = case mn of
0N/A EmptyNode _ -> return (EmptyNode l2, dg)
0N/A (ms, dg2) <- coerceNode lg dg ns nn l2
0N/A return (JustNode ms, dg2)
0N/AcoerceNode :: LogicGraph -> DGraph -> NodeSig -> NodeName -> AnyLogic
0N/A -> Result (NodeSig, DGraph)
0N/AcoerceNode lg dg ns@(NodeSig n s@(G_sign lid1 _ _)) nn l2@(Logic lid2) =
0N/A if language_name lid1 == language_name lid2 then return (ns, dg)
0N/A c <- logicInclusion lg (Logic lid1) l2
0N/A gmor <- gEmbedComorphism c s
0N/A case find (\ (_, _, l) -> dgl_origin l == SeeTarget
0N/A && dgl_type l == globalDef
0N/A && dgl_morphism l == gmor) $ outDG dg n of
0N/A let (ms@(NodeSig m _), dg2) =
0N/A insGSig dg (inc nn) DGTranslation $ cod gmor
0N/A dg3 = insLink dg2 gmor globalDef SeeTarget n m
0N/A return (NodeSig t $ signOf $ dgn_theory $ labDG dg t, dg)
0N/AinsGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
0N/AinsGTheory dg name orig (G_theory lid sig ind sens tind) =
0N/A let (sgMap, s) = sigMapI dg
0N/A (tMap, t) = thMapI dg
0N/A nind = if ind == startSigId then succ s else ind
0N/A ntind = if tb then succ t else tind
0N/A nsig = G_sign lid sig nind
0N/A nth = G_theory lid sig nind sens ntind
0N/A node_contents = newNodeLab name orig nth
0N/A node = getNewNodeDG dg
0N/A in (NodeSig node nsig,
0N/A (if ind == startSigId
0N/A $ insNodeDG (node, node_contents) dg)
0N/AinsGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
0N/AinsGSig dg name orig (G_sign lid sig ind) =
0N/A insGTheory dg name orig $ noSensGTheory lid sig ind
642N/AinsLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node
642N/AinsLink dg (GMorphism cid sign si mor mi) ty orig n t =
642N/A let (sgMap, s) = sigMapI dg
642N/A (mrMap, m) = morMapI dg
642N/A nsi = if si == startSigId then succ s else si
642N/A nmi = if mi == startMorId then succ m else mi
642N/A nmor = GMorphism cid sign nsi mor nmi
2597N/A (toG_morphism nmor) mrMap else id) $
2597N/A (G_sign (sourceLogic cid) sign nsi) sgMap else id)
2597N/A $ insLEdgeNubDG (n, t, link) dg
2597N/AcreateConsLink :: LinkKind -> Conservativity -> LogicGraph -> DGraph
0N/A -> MaybeNode -> NodeSig -> DGLinkOrigin -> Result DGraph
0N/AcreateConsLink lk conser lg dg nsig (NodeSig node gsig) orig = case nsig of
481N/A EmptyNode _ | conser == None -> return dg
0N/A JustNode (NodeSig n sig)-> do
0N/A let Result _ mIncl = ginclusion lg sig gsig
0N/A return $ insLink dg incl
0N/A (ScopedLink Global lk $ mkConsStatus conser) orig n node
0N/A unless (conser == None) $ do
0N/A "ingoring conservativity annotation between non-subsignatures"
0N/A EmptyNode _ -> -- add conservativity to the target node
0N/A return $ let lbl = labDG dg node
0N/A in if isDGRef lbl then dg else
0N/A { node_cons_status = case getNodeConsStatus lbl of
0N/A ConsStatus c d th -> ConsStatus (max c conser) d th }}) dg
0N/AanaSpecTop :: Conservativity -> Bool -> LogicGraph -> DGraph -> MaybeNode
0N/A -> NodeName -> HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, DGraph)
0N/AanaSpecTop conser addSyms lg dg nsig name opts sp =
0N/A if conser == None || case sp of
0N/A -- for these cases def-links are re-used
0N/A Basic_spec _ _ -> True
0N/A Closed_spec _ _ -> True
0N/A Spec_inst _ _ _ -> True
0N/A Group _ _ -> True -- in this case we recurse
0N/A then anaSpecAux conser addSyms lg dg nsig name opts sp else do
0N/A ThmLink $ Proven (DGRule "static analysis") emptyProofBasis
0N/A (rsp, ns, rdg) <- ana_SPEC addSyms lg dg nsig name opts sp
0N/A ndg <- createConsLink provenThmLink conser lg rdg nsig ns SeeTarget
0N/A return (rsp, ns, ndg)
0N/AanaPlainSpec :: Bool -> LogicGraph -> HetcatsOpts -> DGraph
0N/A -> MaybeNode -> NodeName -> DGOrigin -> DGLinkType -> Annoted SPEC -> Range
0N/A -> Result (Annoted SPEC, NodeSig, DGraph)
0N/AanaPlainSpec addSyms lg opts dg nsig name orig dglType asp pos = do
0N/A (sp', NodeSig n' gsigma, dg') <-
0N/A ana_SPEC addSyms lg dg nsig (inc name) opts $ item asp
0N/A let (ns@(NodeSig node gsigma'), dg2) = insGSig dg' name orig gsigma
0N/A incl <- adjustPos pos $ ginclusion lg gsigma gsigma'
0N/A return (replaceAnnoted sp' asp, ns,
0N/A insLink dg2 incl dglType SeeTarget n' node)
0N/A-- Bool Parameter determines if incoming symbols shall be ignored
0N/A-- options: here we need the info: shall only the structure be analysed?
0N/Aana_SPEC :: Bool -> LogicGraph -> DGraph -> MaybeNode
0N/A -> NodeName -> HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, DGraph)
0N/Aana_SPEC = anaSpecAux None
0N/AanaSpecAux :: Conservativity -> Bool -> LogicGraph -> DGraph -> MaybeNode
0N/A -> NodeName -> HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, DGraph)
0N/AanaSpecAux conser addSyms lg dg nsig name opts sp = case sp of
0N/A Basic_spec (G_basic_spec lid bspec) pos ->
0N/A (nsig', dg0) <- coerceMaybeNode lg dg nsig name curLogic
0N/A G_sign lid' sigma' _ <- return $ case nsig' of
0N/A EmptyNode cl -> emptyG_sign cl
0N/A JustNode ns -> getSig ns
0N/A adj $ coerceSign lid' lid "Analysis of basic spec" sigma'
0N/A (bspec', ExtSign sigma_complete sysd, ax) <- adj $
0N/A if isStructured opts
0N/A then return (bspec, mkExtSign $ empty_signature lid, [])
0N/A ("no basic analysis for logic " ++ language_name lid)
0N/A (basic_analysis lid)
0N/A b (bspec, sig, globalAnnos dg0)
0N/A let (ns, dg') = insGTheory dg0 name DGBasic
0N/A $ G_theory lid (ExtSign sigma_complete
0N/A $ sym_of lid sigma_complete) startSigId (toThSens ax) startThId
0N/A dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension
0N/A return (Basic_spec (G_basic_spec lid bspec') pos, ns, dg'')
0N/A EmptySpec pos -> case nsig of
642N/A warning () "empty spec" pos
642N/A let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)
0N/A {- ana_SPEC should be changed to return a MaybeNode!
0N/A Then this duplicate dummy node could be avoided.
0N/A Also empty unions could be treated then -}
113N/A JustNode ns -> return (sp, ns ,dg)
0N/A Translation asp ren ->
0N/A do let sp1 = item asp
0N/A (sp1', NodeSig n' gsigma, dg') <-
0N/A ana_SPEC addSyms lg dg 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 (ns@(NodeSig node _), dg'') =
0N/A insGSig dg' name DGTranslation $ cod mor
0N/A -- ??? too simplistic for non-comorphism inter-logic translations
0N/A return (Translation (replaceAnnoted sp1' asp) ren, ns,
0N/A insLink dg'' mor globalDef SeeTarget n' node)
0N/A Reduction asp restr ->
0N/A do let sp1 = item asp
0N/A (sp1', NodeSig n' gsigma', dg') <-
0N/A ana_SPEC addSyms lg dg nsig (inc name) opts sp1
0N/A let gsigma = getMaybeSig nsig
0N/A (hmor, tmor) <- ana_RESTRICTION 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 (ns@(NodeSig node _), dg'') =
0N/A insGSig dg' name DGHiding $ dom hmor
0N/A -- ??? too simplistic for non-comorphism inter-logic reductions
0N/A return (Reduction (replaceAnnoted sp1' asp) restr, ns,
0N/A insLink dg'' hmor HidingDefLink SeeTarget n' node)
0N/A let gsigma1 = dom tmor'
0N/A gsigma'' = cod tmor'
0N/A -- ??? too simplistic for non-comorphism inter-logic reductions
0N/A -- the case with identity translation leads to a simpler dg
0N/A if tmor' == ide (dom tmor')
0N/A let (ns@(NodeSig node1 _), dg'') =
0N/A insGSig dg' name DGRevealing gsigma1
0N/A return (Reduction (replaceAnnoted sp1' asp) restr, ns,
0N/A insLink dg'' hmor HidingDefLink SeeTarget n' node1)
0N/A let (NodeSig node1 _, dg'') =
0N/A insGSig dg' (extName "T" name) DGRevealing gsigma1
0N/A (ns@(NodeSig node2 _), dg3) =
0N/A insGSig dg'' name DGRevealTranslation gsigma''
0N/A dg4 = insLink dg3 hmor HidingDefLink SeeTarget n' node1
0N/A return (Reduction (replaceAnnoted sp1' asp) restr, ns,
0N/A insLink dg4 tmor' globalDef SeeTarget node1 node2)
0N/A Union [] pos -> adjustPos pos $ fail $ "empty union"
0N/A do let sps = map item asps
0N/A (sps', nsigs, dg', _) <-
0N/A let ana (sps1, nsigs, dg', n) sp' = do
0N/A (sp1, nsig', dg1) <- ana_SPEC addSyms lg dg' nsig n opts sp'
0N/A return (sp1 : sps1, nsig' : nsigs, dg1, inc n)
0N/A in foldM ana ([], [], dg, extName "U" name) sps
0N/A let nsigs' = reverse nsigs
0N/A gbigSigma <- adj $ gsigManyUnion lg (map getSig nsigs')
0N/A let (ns@(NodeSig node _), dg2) = insGSig dg' name DGUnion gbigSigma
0N/A insE dgl (NodeSig n gsigma) = do
0N/A incl <- adj $ ginclusion lg gsigma gbigSigma
0N/A return $ insLink dgl incl globalDef SeeTarget n node
0N/A dg3 <- foldM insE dg2 nsigs'
0N/A return (Union (map (uncurry replaceAnnoted)
0N/A (zip (reverse sps') asps))
0N/A Extension asps pos -> do
0N/A (sps', nsig1', dg1, _, _) <- foldM (ana_Extension lg opts pos)
0N/A ([], nsig, dg, conser, addSyms) namedSps
0N/A EmptyNode _ -> fail "empty extension"
0N/A JustNode nsig1 -> return (Extension (map (uncurry replaceAnnoted)
0N/A (zip (reverse sps') asps))
0N/A namedSps = zip (reverse (name: tail (take (length asps)
0N/A (iterate inc (extName "E" name)))))
0N/A Free_spec asp poss -> do
2062N/A (nasp, nsig', dg') <- anaPlainSpec addSyms lg opts dg nsig name
2062N/A DGFree (FreeOrCofreeDefLink Free nsig) asp poss
0N/A return (Free_spec nasp poss, nsig', dg')
0N/A Cofree_spec asp poss -> do
0N/A (nasp, nsig', dg') <- anaPlainSpec addSyms lg opts dg nsig name
0N/A DGCofree (FreeOrCofreeDefLink Cofree nsig) asp poss
0N/A return (Cofree_spec nasp poss, nsig', dg')
0N/A Local_spec asp asp' poss ->
0N/A do let sp1 = item asp
0N/A adj = adjustPos poss
0N/A (sp2, nsig'@(NodeSig _ (G_sign lid' sigma' _)), dg') <-
0N/A ana_SPEC False lg dg nsig (extName "L" name) opts sp1
0N/A (sp2', NodeSig n'' (G_sign lid'' sigma'' _), dg'') <-
0N/A ana_SPEC False lg dg' (JustNode nsig') (inc name) opts sp1'
0N/A let gsigma = getMaybeSig nsig
0N/A G_sign lid sigma _ <- return gsigma
0N/A sigma1 <- adj $ coerceSign lid' lid "Analysis of local spec" sigma'
0N/A sigma2 <- adj $ coerceSign lid'' lid "Analysis of local spec" sigma''
0N/A let sys = ext_sym_of lid sigma
0N/A sys1 = ext_sym_of lid sigma1
0N/A sys2 = ext_sym_of lid sigma2
0N/A mor3 <- if isStructured opts then return (ext_ide sigma2)
0N/A else adj $ ext_cogenerated_sign lid
0N/A let sigma3 = dom mor3
0N/A -- gsigma2 = G_sign lid sigma2
0N/A gsigma3 = G_sign lid (makeExtSign lid sigma3) startSigId
0N/A sys3 = sym_of lid sigma3
0N/A when (not( isStructured opts ||
0N/A "illegal use of locally declared symbols: "
0N/A let (ns@(NodeSig node _), dg2) = insGSig dg'' name DGLocal gsigma3
0N/A return (Local_spec (replaceAnnoted sp2 asp)
0N/A (replaceAnnoted sp2' asp')
0N/A insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid mor3)
0N/A HidingDefLink SeeTarget n'' node)
0N/A Closed_spec asp pos ->
0N/A do let sp1 = item asp
0N/A -- analyse spec with empty local env
0N/A (sp', NodeSig n' gsigma', dg') <-
0N/A ana_SPEC False lg dg (EmptyNode l) (inc name) opts sp1
0N/A let gsigma = getMaybeSig nsig
0N/A gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
0N/A let (ns@(NodeSig node gsigma2), dg2) = insGSig dg' name DGClosed gsigma''
0N/A incl2 <- adj $ ginclusion lg gsigma' gsigma2
0N/A let dg3 = insLink dg2 incl2 globalDef SeeTarget n' node
0N/A dg4 <- createConsLink DefLink conser lg dg3 nsig ns DGLinkClosedLenv
0N/A return (Closed_spec (replaceAnnoted sp' asp) pos, ns, dg4)
0N/A Qualified_spec lognm@(Logic_name ln _) asp pos -> do
0N/A let newLG = lg { currentLogic = tokStr ln }
1833N/A l <- lookupCurrentLogic "Qualified_spec" newLG
0N/A let newNSig = case nsig of
0N/A EmptyNode _ -> EmptyNode l
0N/A (nasp, nsig', dg') <-
113N/A anaPlainSpec addSyms lg opts dg newNSig name DGLogicQual
642N/A return (Qualified_spec lognm nasp pos, nsig', dg')
642N/A anaSpecTop conser addSyms lg dg nsig name opts (item asp)
642N/A return (Group (replaceAnnoted sp' asp) pos, nsig', dg')
642N/A Spec_inst spname afitargs pos0 -> let
642N/A pos = if null afitargs then tokPos spname else pos0
642N/A in case lookupGlobalEnvDG spname dg of
642N/A Just (SpecEntry gs@(ExtGenSig (GenSig imps params _)
642N/A body@(NodeSig nB gsigmaB))) ->
642N/A case (\ x y -> (x , x - y)) (length afitargs) (length params) of
642N/A -- the case without parameters leads to a simpler dg
642N/A -- if the node shall not be named and the logic does not change,
642N/A EmptyNode _ | isInternal name -> do
642N/A dg2 <- createConsLink DefLink conser lg dg nsig body SeeTarget
642N/A -- then just return the body
0N/A -- otherwise, we need to create a new one
0N/A gsigma <- case nsig of
0N/A EmptyNode _ -> return gsigmaB
0N/A JustNode (NodeSig _ sig) -> adj $ gsigUnion lg sig gsigmaB
0N/A let (fsig@(NodeSig node gsigma'), dg2) =
0N/A insGSig dg name (DGSpecInst spname) gsigma
0N/A incl <- adj $ ginclusion lg gsigmaB gsigma'
0N/A let dg3 = insLink dg2 incl globalDef SeeTarget nB node
0N/A dg4 <- createConsLink DefLink conser lg dg3 nsig fsig SeeTarget
0N/A return (sp, fsig, dg4)
0N/A -- now the case with parameters
0N/A let fitargs = map item afitargs
0N/A (fitargs', dg', args, _) <- adj $ foldM (anaFitArg lg opts spname imps)
0N/A ([], dg, [], extName "A" name) (zip params fitargs)
0N/A let actualargs = reverse args
0N/A (gsigma', morDelta@(GMorphism cid _ _ _ _)) <-
0N/A adj $ apply_GS lg gs actualargs
0N/A gsigmaRes <- case nsig of
0N/A EmptyNode _ -> return gsigma'
0N/A JustNode (NodeSig _ sigma) -> adj $ gsigUnion lg sigma gsigma'
0N/A let (ns@(NodeSig node gsigmaRes'), dg2) =
0N/A insGSig dg' name (DGSpecInst spname) gsigmaRes
0N/A dg3 <- foldM (parLink lg DGLinkFitSpec gsigmaRes' node) dg2
0N/A morDelta' <- case nsig of
0N/A EmptyNode _ -> return morDelta
0N/A incl2 <- adj $ ginclusion lg gsigma' gsigmaRes'
0N/A (_, imor) <- gSigCoerce lg gsigmaB $ Logic $ sourceLogic cid
0N/A tmor <- gEmbedComorphism imor gsigmaB
0N/A morDelta'' <- comp tmor morDelta'
0N/A let dg4 = insLink dg3 morDelta'' globalDef SeeTarget nB node
0N/A dg5 <- createConsLink DefLink conser lg dg4 nsig ns SeeTarget
0N/A return (Spec_inst spname
2597N/A (map (uncurry replaceAnnoted)
2597N/A (zip (reverse fitargs') afitargs))
2911N/A -- finally the case with conflicting numbers of formal and actual parameters
2911N/A (spstr ++ " expects " ++ show (length params) ++ " arguments"
2911N/A ++ " but was given " ++ show (length afitargs)) pos
0N/A ("Structured specification " ++ spstr ++ " not found") pos
0N/A -- analyse "data SPEC1 SPEC2"
3233N/A Data (Logic lidD) (Logic lidP) asp1 asp2 pos -> do
0N/A -- look for the inclusion comorphism from the current logic's data logic
0N/A -- into the current logic itself
0N/A Comorphism cid <- adj $ logicInclusion lg (Logic lidD) (Logic lidP)
0N/A let lidD' = sourceLogic cid
0N/A lidP' = targetLogic cid
0N/A (sp1', NodeSig n' (G_sign lid' sigma' _), dg') <-
0N/A ana_SPEC False lg dg (EmptyNode (Logic lidD)) dname opts sp1
0N/A -- force the result to be in the data logic
0N/A sigmaD <- adj $ coerceSign lid' lidD' "Analysis of data spec" sigma'
0N/A -- translate SPEC1's signature along the comorphism
0N/A (sigmaD', sensD') <- adj $ ext_map_sign cid sigmaD
0N/A -- create a development graph link for this translation
0N/A let (nsig2@(NodeSig node _), dg1) = insGTheory dg' dname DGData
2677N/A $ G_theory lidP' sigmaD' startSigId (toThSens sensD') startThId
0N/A dg2 = insLink dg1 (GMorphism cid sigmaD startSigId
0N/A (ext_ide sigmaD') startMorId)
0N/A globalDef SeeTarget n' node
0N/A (sp2', nsig3, dg3) <-
0N/A ana_SPEC addSyms lg dg2 (JustNode nsig2) name opts sp2
0N/A return (Data (Logic lidD) (Logic lidP)
0N/A (replaceAnnoted sp1' asp1)
0N/A (replaceAnnoted sp2' asp2)
0N/AanaFitArg :: LogicGraph -> HetcatsOpts -> SPEC_NAME -> MaybeNode
0N/A -> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)
0N/A -> (NodeSig, FIT_ARG)
0N/A -> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)
0N/AanaFitArg lg opts spname imps (fas', dg1, args, name') (nsig', fa) = do
0N/A (fa', dg', arg) <- ana_FIT_ARG lg dg1 spname imps nsig' opts name' fa
0N/A return (fa' : fas', dg', arg : args , inc name')
0N/AparLink :: LogicGraph -> DGLinkOrigin -> G_sign -> Node -> DGraph -> NodeSig
0N/AparLink lg orig gsigma' node dg (NodeSig nA_i sigA_i)= do
0N/A incl <- ginclusion lg sigA_i gsigma'
0N/A return $ insLink dg incl globalDef orig nA_i node
0N/A-- analysis of renamings
0N/Aana_ren :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism
0N/A -> G_mapping -> Result GMorphism
0N/Aana_ren lg opts lenv pos gmor@(GMorphism r sigma ind1 mor _) gmap =
0N/A let adj = adjustPos pos in case gmap of
0N/A G_symb_map (G_symb_map_items_list lid sis) ->
1879N/A let lid2 = targetLogic r in
1879N/A adj $ if language_name lid2 == language_name lid then
if isStructured opts then return gmor else do
sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis
rmap <- stat_symb_map_items lid2 sis1
mor1 <- ext_induced_from_morphism lid2 rmap $ makeExtSign lid2 $ cod 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 properly handeled"
let sysLenv = ext_sym_of lid2 sigmaLenv'
when (not $
Set.null forbiddenSys) $ plain_error () (
"attempt to rename the following symbols from " ++
"the local environment:\n" ++ showDoc forbiddenSys "") pos
return $ GMorphism r sigma ind1 mor2 startMorId
comor <- logicInclusion lg (Logic lid2) (Logic lid)
gmorTrans <- gEmbedComorphism comor $ cod gmor
newMor <- comp gmor gmorTrans
ana_ren lg opts lenv pos newMor gmap
G_logic_translation (Logic_code tok src tar pos1) ->
let adj1 = adjustPos $ if pos1 == nullRange then pos else pos1
G_sign srcLid srcSig ind <- return (cod gmor)
let getLogicStr (Logic_name l _) = tokStr l
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 <- gEmbedComorphism c (G_sign srcLid srcSig ind)
ana_RENAMING :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING
ana_RENAMING lg lenv gSigma opts (Renaming ren pos) =
foldM (ana_ren lg opts lenv pos) (ide gSigma) ren
-- analysis of restrictions
ana_restr :: G_sign -> Range -> GMorphism -> G_hiding -> Result GMorphism
ana_restr (G_sign lidLenv sigmaLenv _) pos
(GMorphism cid (ExtSign sigma1 sys1) _ mor _) gh =
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 (matches lid1 sy) rsys) sys
( \ sy -> matches lid1 sy rsy) sys') rsys
when (not $ null unmatched)
$ plain_error () ("attempt to hide unknown symbols:\n"
++ showDoc unmatched "") pos
-- needs to be changed when logic projections are implemented
sigmaLenv' <- coerceSign lidLenv lid1
"Analysis of restriction: logic projections not properly handeled"
let sysLenv = ext_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
return $ GMorphism cid (ExtSign (dom mor1) $
Set.fold (\ sy ->
startSigId mor2 startMorId
G_logic_projection (Logic_code _tok _src _tar pos1) ->
fatal_error "no analysis of logic projections yet" pos1
ana_RESTRICTION :: G_sign -> G_sign -> HetcatsOpts -> RESTRICTION
-> Result (GMorphism, Maybe GMorphism)
ana_RESTRICTION gSigma@(G_sign lid sigma _)
gSigma'@(G_sign lid' sigma' _) opts restr =
if isStructured opts then return (ide gSigma, Nothing) else
mor <- foldM (ana_restr gSigma pos) (ide gSigma') rstr
Revealed (G_symb_map_items_list lid1 sis) pos ->
let sys = ext_sym_of lid sigma -- local env
sys' = ext_sym_of lid' sigma' -- "big" signature
sis' <- coerceSymbMapItemsList lid1 lid'
"Analysis of restriction" sis
rmap <- stat_symb_map_items lid' sis'
-- domain of rmap intersected with sys'
-- domain of rmap should be checked to match symbols from sys' ???
sys1 <- coerceSymbolSet lid lid' "Analysis of restriction" sys
-- ??? this is too simple in case that local env is translated
mor1 <- ext_generated_sign lid' (sys1 `
Set.union` sys'') sigma'
mor2 <- ext_induced_from_morphism lid' rmap $ makeExtSign lid' $ dom mor1
return (gEmbed (mkG_morphism lid' mor1),
Just (gEmbed (mkG_morphism lid' mor2)))
ana_Gmaps :: LogicGraph -> HetcatsOpts -> Range
-> G_sign -> G_sign -> [G_mapping] -> Result G_morphism
ana_Gmaps lg opts pos psig@(G_sign lidP sigmaP _) (G_sign lidA sigmaA _) gsis
adj $ if isStructured opts
then return $ mkG_morphism lidP $ ext_ide sigmaP
else if null gsis then do
sigmaA' <- coerceSign lidA lidP "ana_Gmaps" sigmaA
fmap (mkG_morphism lidP) $
ext_induced_from_to_morphism lidP
Map.empty sigmaP sigmaA'
cl <- lookupCurrentLogic "ana_Gmaps" lg
G_symb_map_items_list lid sis <- homogenizeGM cl gsis
rmap <- stat_symb_map_items lid sis
(\ s -> matches lid s r) $ ext_sym_of lid sig
(G_sign lidP' sigmaP'' _, _) <- gSigCoerce lg psig (Logic lid)
sigmaP' <- coerceSign lidP' lid "ana_Gmaps1" sigmaP''
sigmaA' <- coerceSign lidA lid "ana_Gmaps2" sigmaA
let unknowns = filter (noMatch sigmaP') (
Map.keys rmap)
if null unknowns then fmap (mkG_morphism lid)
$ ext_induced_from_to_morphism lid rmap sigmaP' sigmaA'
else fatal_error ("unknown symbols " ++ showDoc unknowns "") pos
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
ana_FIT_ARG :: LogicGraph -> DGraph -> SPEC_NAME -> MaybeNode
-> NodeSig -> HetcatsOpts -> NodeName -> FIT_ARG
-> Result (FIT_ARG, DGraph, (G_morphism,NodeSig))
ana_FIT_ARG lg dg spname nsigI (NodeSig nP gsigmaP) opts name fv = case fv of
Fit_spec asp gsis pos -> do
(sp', nsigA@(NodeSig nA gsigA), dg') <-
ana_SPEC False lg dg nsigI name opts (item asp)
gmor <- ana_Gmaps lg opts pos gsigmaP gsigA gsis
return (Fit_spec (replaceAnnoted sp' asp) gsis pos,
insLink dg' (gEmbed gmor) globalThm
(DGLinkSpecInst spname) nP nA, (gmor, nsigA))
Fit_view vn afitargs pos -> let
in case lookupGlobalEnvDG vn dg of
Just (ViewEntry (ExtViewSig src mor
gs@(ExtGenSig (GenSig imps params _) target))) -> do
gsigmaI = getMaybeSig nsigI
GMorphism cid _ _ morHom ind <- return mor
let lid = targetLogic cid
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
gmor <- ginclusion lg gsigmaP gsigmaS
return (fv, insLink dg gmor globalThm (DGLinkFitView spname)
nP nSrc, (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 _, _) <- adj $ gSigCoerce lg gsigmaI (Logic lid)
sigI <- adj $ coerceSign lidI lid
"Analysis of instantiation with import" sigI1
mor_I <- adj $ morphism_union lid morHom $ ext_ide sigI
gsigmaA <- adj $ gsigUnion lg gsigmaI gsigmaT
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 (ns@(NodeSig nA _), dg1) =
insGSig dg name (DGFitViewA spname) gsigmaA
insGSig dg1 (inc name) (DGFitView spname) gsigmaP
dg3 = insLink dg2 incl1 globalDef
(DGLinkFitViewAImp spname) nI nA
dg4 = insLink dg3 incl3 globalDef
(DGLinkFitViewImp spname) nI n'
dg5 = insLink dg4 incl2 globalDef SeeTarget nTar nA
dg6 = insLink dg5 incl4 globalDef SeeTarget nSrc n'
dg7 = insLink dg6 (ide gsigmaP)
globalThm SeeTarget nP n'
return (fv, dg7, (mkG_morphism lid mor_I, ns))
-- now the case with parameters
let fitargs = map item afitargs
(fitargs', dg', args,_) <- foldM (anaFitArg lg opts spname imps)
([], dg, [], extName "A" name) (zip params fitargs)
let actualargs = reverse args
(gsigmaA, gmor_f) <- adj $ apply_GS lg gs actualargs
gsigmaRes <- adj $ gsigUnion lg gsigmaI gsigmaA
mor1 <- adj $ comp mor gmor_f
incl1 <- adj $ ginclusion lg gsigmaA gsigmaRes
mor' <- adj $ comp 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 (ext_ide sigI)
incl2 <- adj $ ginclusion lg gsigmaI gsigmaRes
incl3 <- adj $ ginclusion lg gsigmaI gsigmaP
incl4 <- adj $ ginclusion lg gsigmaS gsigmaP
let (ns@(NodeSig nA _), dg1) =
insGSig dg' name (DGFitViewA spname) gsigmaRes
insGSig dg1 (extName "V" name) (DGFitView spname) gsigmaP
dg3 <- foldM (parLink lg (DGLinkFitView spname) gsigmaRes nA) dg2
JustNode (NodeSig nI _) -> let
dg3a = insLink dg3 incl2 globalDef
(DGLinkFitViewAImp spname) nI nA
in insLink dg3a incl3 globalDef (DGLinkFitViewImp spname) nI n'
dg5 = insLink dg4 mor' globalDef SeeTarget nTar nA
dg6 = insLink dg5 incl4 globalDef SeeTarget nSrc n'
dg7 = insLink dg6 (ide gsigmaP) globalThm SeeTarget nP n'
(map (uncurry replaceAnnoted)
(zip (reverse fitargs') afitargs))
pos, dg7, (mkG_morphism lid1 theta, ns))
-- finally the case with conflicting numbers of formal and actual parameters
(spstr ++ " expects " ++ show (length params) ++ " arguments"
++ " but was given " ++ show (length afitargs)) pos
("View " ++ tokStr vn ++ " not found") pos
-- Extension of signature morphisms (for instantitations)
-- first some auxiliary functions
mapID idmap i@(Id toks comps pos1) =
compsnew <- mapM (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 <- mapM (mapID idmap) comps
return $ if comps == compsnew then m1 else
extendMorphism :: G_sign -- ^ formal parameter
-> G_sign -- ^ actual parameter
-> G_morphism -- ^ fitting morphism
-> Result(G_sign, GMorphism)
extendMorphism (G_sign lid sigmaP _) (G_sign lidB sigmaB1 _)
(G_sign lidA sigmaA1 _) (G_morphism lidM fittingMor1 _) = do
-- for now, only homogeneous instantiations....
sigmaB@(ExtSign _ sysB) <-
coerceSign lidB lid "Extension of symbol map1" sigmaB1
sigmaA <- coerceSign lidA lid "Extension of symbol map2" sigmaA1
fittingMor <- coerceMorphism lidM lid "Extension of symbol map3" fittingMor1
let symsP = ext_sym_of lid sigmaP
symsB = ext_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 <- ext_induced_from_morphism lid r sigmaB
let hmor = symmap_of lid mor
sigmaAD = ExtSign (cod mor) $
Set.map (\ sy ->
sigma <- ext_signature_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 <- ext_inclusion lid sigmaAD sigma
return (G_sign lid sigma startSigId, gEmbed $ mkG_morphism lid mor1)
apply_GS :: LogicGraph -> ExtGenSig -> [(G_morphism, NodeSig)]
-> Result(G_sign, GMorphism)
apply_GS lg (ExtGenSig (GenSig nsigI _ gsigmaP) nsigB) args = do
gsigmaA_i = map (getSig . snd) args
gsigmaA@(G_sign lidA _ _) <- gsigManyUnion lg gsigmaA_i
(_, Comorphism uid) <- logicUnion lg (getNodeLogic nsigB) (Logic lidA)
let cl = Logic $ targetLogic uid
G_morphism lidG mor0 _ <- case nsigI of
EmptyNode _ -> homogeneousMorManyUnion mor_i
JustNode (NodeSig _ gsigmaI) -> do
(G_sign lidI sigmaI _, _) <- gSigCoerce lg gsigmaI (Logic lidA)
homogeneousMorManyUnion $ mkG_morphism lidI idI : mor_i
(gsigmaP', _) <- gSigCoerce lg (getMaybeSig gsigmaP) cl
(gsigmaB', _) <- gSigCoerce lg gsigmaB cl
(gsigmaA', Comorphism aid) <- gSigCoerce lg gsigmaA cl
mor1 <- coerceMorphism lidG (sourceLogic aid) "apply_GS" mor0
mor2 <- map_morphism aid mor1
extendMorphism gsigmaP' gsigmaB' gsigmaA' $
G_morphism (targetLogic aid) mor2 startMorId
-> Result G_symb_map_items_list
homogenizeGM (Logic lid) gsis =
foldM homogenize1 (G_symb_map_items_list lid []) gsis
homogenize1 itl2@(G_symb_map_items_list lid2 sis) sm = case sm of
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
getSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)
let sannos = filter isSemanticAnno $ l_annos a
(sanno1, conflict, impliedA, impliesA) = case sannos of
f@(Semantic_anno anno1 _) : r -> (case anno1 of
anno1 == SA_implied, anno1 == SA_implies)
_ -> (None, False, False, False)
when conflict $ plain_error () "Conflicting semantic annotations" pos
when impliedA $ plain_error ()
"Annotation %implied should come after a BASIC-ITEM" pos
return (sanno1, impliesA)
-- only consider addSyms for the first spec
:: LogicGraph -> HetcatsOpts -> Range
-> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
-> (NodeName, Annoted SPEC)
-> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
ana_Extension lg opts pos (sps', nsig', dg', conser, addSyms) (name', asp')
(sanno1, impliesA) <- getSpecAnnos pos asp'
-- attach conservativity to definition link
(sp1', nsig1@(NodeSig n1 sig1), dg1) <-
anaSpecTop (max conser sanno1) addSyms lg dg' nsig' name' opts (item asp')
dg2 <- if impliesA then case nsig' of
JustNode (NodeSig n' sig') -> do
-- is the extension going between real nodes?
when (not $ isHomSubGsign sig1 sig') $ plain_error ()
"Signature must not be extended in presence of %implies" pos
-- insert a theorem link according to p. 319 of the CASL Reference Manual
return $ insLink dg1 (ide sig1) globalThm DGImpliesLink n1 n'
return (sp1' : sps', JustNode nsig1, dg2, None, True)