0N/A{- |

1879N/AModule : $Header$

0N/ADescription : static analysis of heterogeneous structured specifications

0N/ACopyright : (c) Till Mossakowski and Uni Bremen 2003-2006

0N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

0N/AMaintainer : till@informatik.uni-bremen.de

0N/AStability : provisional

0N/APortability : non-portable (imports Logic.Grothendieck)

0N/A

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/A-}

0N/A

0N/Amodule Static.AnalysisStructured

0N/A ( ana_SPEC

0N/A , isStructured

0N/A , ana_RENAMING

1472N/A , ana_RESTRICTION

1472N/A , ana_Gmaps

1472N/A , homogenizeGM

0N/A , insGSig

0N/A , insLink

0N/A , extendMorphism

1879N/A ) where

1879N/A

1879N/Aimport Driver.Options

1879N/Aimport Logic.Logic

1879N/Aimport Logic.ExtSign

1879N/Aimport Logic.Coerce

1879N/Aimport Logic.Comorphism

1879N/Aimport Logic.Grothendieck

1879N/Aimport Logic.Prover

1879N/Aimport Static.DevGraph

1879N/Aimport Static.GTheory

1879N/Aimport Syntax.AS_Structured

1879N/Aimport Common.Result

1879N/Aimport Common.Id

1879N/Aimport Common.ExtSign

1879N/Aimport Common.AS_Annotation hiding (isAxiom, isDef)

1879N/Aimport qualified Data.Set as Set

1879N/Aimport qualified Data.Map as Map

1879N/Aimport qualified Common.Lib.Rel as Rel(image, setInsert)

1879N/Aimport Data.Graph.Inductive.Graph as Graph (Node)

1879N/Aimport Common.DocUtils

1879N/Aimport Data.Maybe

1879N/Aimport Data.List (find)

0N/Aimport Control.Monad

0N/A

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 tb = tind == startThId && not (Map.null sens)

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 tb then setThMapDG $ Map.insert (succ t) nth tMap else id) $

0N/A (if ind == startSigId

0N/A then setSigMapDG $ Map.insert (succ s) nsig sgMap else id)

0N/A $ insNodeDG (node, node_contents) dg)

0N/A

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

0N/A

0N/AinsLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node

0N/A -> DGraph

0N/AinsLink dg (GMorphism cid sign si mor mi) ty orig n t =

0N/A let (sgMap, s) = sigMapI dg

0N/A (mrMap, m) = morMapI dg

0N/A nsi = if si == startSigId then succ s else si

0N/A nmi = if mi == startMorId then succ m else mi

0N/A nmor = GMorphism cid sign nsi mor nmi

113N/A link = DGLink

113N/A { dgl_morphism = nmor

113N/A , dgl_type = ty

113N/A , dgl_origin = orig

113N/A , dgl_id = defaultEdgeId }

113N/A in (if mi == startMorId then setMorMapDG $ Map.insert (succ m)

113N/A (toG_morphism nmor) mrMap else id) $

113N/A (if si == startSigId then setSigMapDG $ Map.insert (succ s)

0N/A (G_sign (sourceLogic cid) sign nsi) sgMap else id)

0N/A $ insLEdgeNubDG (n, t, link) dg

113N/A

113N/A-- | analyze a SPEC

113N/A-- first Parameter determines if incoming symbols shall be ignored

113N/A-- options: here we need the info: shall only the structure be analysed?

113N/Aana_SPEC :: Bool -> LogicGraph -> DGraph -> MaybeNode -> NodeName ->

0N/A HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, DGraph)

0N/Aana_SPEC addSyms lg dg nsig name opts sp = case sp of

0N/A Basic_spec (G_basic_spec lid bspec) pos ->

0N/A do let adj = adjustPos pos

0N/A curLogic = Logic lid

0N/A G_sign lid' sigma' _ <- case nsig of

0N/A EmptyNode _ -> return $ emptyG_sign curLogic

0N/A JustNode ns -> gSigCoerce lg "Basic_spec" (getSig ns) curLogic

0N/A ExtSign sig sys <-

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 else do

0N/A b <- maybeToMonad

0N/A ("no basic analysis for logic " ++ language_name lid)

0N/A (basic_analysis lid)

0N/A b (bspec, sig, globalAnnos dg)

0N/A let (ns@(NodeSig node gsig), dg') = insGTheory dg name DGBasic

0N/A $ G_theory lid (ExtSign sigma_complete

0N/A $ Set.intersection

0N/A (if addSyms then Set.union sys sysd else sysd)

0N/A $ sym_of lid sigma_complete) startSigId (toThSens ax) startThId

0N/A dg'' <- case nsig of

0N/A EmptyNode _ -> return dg'

0N/A JustNode jn@(NodeSig n _) -> do

0N/A incl <- adj $ ginclusion lg (getSig jn) gsig

0N/A return $ insLink dg' incl GlobalDef DGLinkExtension n node

0N/A return (Basic_spec (G_basic_spec lid bspec') pos, ns, dg'')

0N/A EmptySpec pos -> case nsig of

0N/A EmptyNode _ -> do

0N/A warning () "empty spec" pos

0N/A let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)

0N/A return (sp, ns, dg')

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 -}

342N/A JustNode ns -> return (sp, ns, dg)

845N/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 case tmor of

0N/A Nothing ->

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 HidingDef SeeTarget n' node)

342N/A Just tmor' -> do

342N/A let gsigma1 = dom tmor'

342N/A gsigma'' = cod tmor'

342N/A -- ??? too simplistic for non-comorphism inter-logic reductions

342N/A -- the case with identity translation leads to a simpler dg

263N/A if tmor' == ide (dom tmor')

342N/A then do

342N/A let (ns@(NodeSig node1 _), dg'') =

342N/A insGSig dg' name DGRevealing gsigma1

263N/A return (Reduction (replaceAnnoted sp1' asp) restr, ns,

0N/A insLink dg'' hmor HidingDef SeeTarget n' node1)

0N/A else do

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''

263N/A dg4 = insLink dg3 hmor HidingDef 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 Union asps pos ->

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 adj = adjustPos pos

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 pos, ns, dg3)

0N/A Extension asps pos -> do

0N/A (sps', nsig1', dg1, _, _, _, _) <-

0N/A foldM ana_Extension ([], nsig, dg, lg, opts, pos, addSyms) namedSps

0N/A case nsig1' of

0N/A EmptyNode _ -> fail "empty extension"

0N/A JustNode nsig1 -> return (Extension (map (uncurry replaceAnnoted)

0N/A (zip (reverse sps') asps))

0N/A pos, nsig1,dg1)

0N/A where

0N/A namedSps = zip (reverse (name: tail (take (length asps)

0N/A (iterate inc (extName "E" name)))))

0N/A asps

0N/A Free_spec asp poss -> do

0N/A (nasp, nsig', dg') <-

0N/A anaPlainSpec addSyms lg opts dg nsig name DGFree (FreeDef nsig)

0N/A asp poss

0N/A return (Free_spec nasp poss, nsig', dg')

0N/A Cofree_spec asp poss -> do

0N/A (nasp, nsig', dg') <-

0N/A anaPlainSpec addSyms lg opts dg nsig name DGCofree (CofreeDef nsig)

0N/A 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

517N/A sp1' = item asp'

517N/A (sp2, nsig'@(NodeSig _ (G_sign lid' sigma' _)), dg') <-

517N/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 <- coerceSign lid' lid "Analysis of local spec" sigma'

0N/A sigma2 <- 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 adjustPos poss $ ext_cogenerated_sign lid

0N/A (sys1 `Set.difference` sys) sigma2

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 sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3))

0N/A $ plain_error () (

0N/A "illegal use of locally declared symbols: "

0N/A ++ showDoc ((sys2 `Set.intersection` sys1) `Set.difference` sys3) "")

0N/A poss

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 poss, ns,

0N/A insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid mor3)

0N/A HidingDef SeeTarget n'' node)

0N/A Closed_spec asp pos ->

0N/A do let sp1 = item asp

0N/A l = getLogic nsig

342N/A adj = adjustPos pos

342N/A -- analyse spec with empty local env

342N/A (sp', NodeSig n' gsigma', dg') <-

342N/A ana_SPEC False lg dg (EmptyNode l) (inc name) opts sp1

342N/A gsigma'' <- case nsig of

342N/A EmptyNode _ -> return gsigma'

342N/A JustNode ns -> adj $ gsigUnion lg (getSig ns) gsigma'

0N/A let (ns@(NodeSig node gsigma2), dg2) = insGSig dg' name DGClosed gsigma''

0N/A incl1 <- adj $ ginclusion lg (getMaybeSig nsig) gsigma2

0N/A incl2 <- adj $ ginclusion lg gsigma' gsigma2

0N/A let dg3 = insLink dg2 incl2 GlobalDef SeeTarget n' node

0N/A return (Closed_spec (replaceAnnoted sp' asp) pos, ns, case nsig of

0N/A EmptyNode _ -> dg3

0N/A JustNode (NodeSig n _) ->

0N/A insLink dg3 incl1 GlobalDef DGLinkClosedLenv n node)

0N/A Qualified_spec lognm@(Logic_name ln _) asp pos -> do

0N/A let newLG = lg { currentLogic = tokStr ln }

0N/A l <- lookupCurrentLogic "Qualified_spec" newLG

0N/A let newNSig = case nsig of

0N/A EmptyNode _ -> EmptyNode l

0N/A _ -> nsig

0N/A (nasp, nsig', dg') <-

0N/A anaPlainSpec addSyms lg opts dg newNSig name DGLogicQual GlobalDef

0N/A asp pos

0N/A return (Qualified_spec lognm nasp pos, nsig', dg')

0N/A Group asp pos -> do

0N/A (sp', nsig', dg') <- ana_SPEC addSyms lg dg nsig name opts (item asp)

0N/A return (Group (replaceAnnoted sp' asp) pos, nsig', dg')

0N/A Spec_inst spname afitargs pos0 -> let

0N/A pos = if null afitargs then tokPos spname else pos0

0N/A adj = adjustPos pos

0N/A spstr = tokStr spname

0N/A in case lookupGlobalEnvDG spname dg of

0N/A Just (SpecEntry gs@(ExtGenSig imps params _ body@(NodeSig nB gsigmaB))) ->

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 (0, 0) -> do

0N/A case nsig of

0N/A -- the subcase with empty local env leads to an even simpler dg

0N/A EmptyNode _ ->

0N/A -- if the node shall not be named and the logic does not change,

0N/A if isInternal name

0N/A -- then just return the body

0N/A then return (sp, body, dg)

0N/A -- otherwise, we need to create a new one

0N/A else do

0N/A let (fsig@(NodeSig node gsigma'), dg2) =

0N/A insGSig dg name (DGSpecInst spname) gsigmaB

0N/A incl <- adj $ ginclusion lg gsigmaB gsigma'

0N/A let dg3 = insLink dg2 incl GlobalDef SeeTarget nB node

0N/A return (sp, fsig, dg3)

0N/A -- the subcase with nonempty local env

0N/A JustNode (NodeSig n sigma) -> do

0N/A gsigma <- adj $ gsigUnion lg sigma 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 incl2 <- adj $ ginclusion lg sigma gsigma'

0N/A return (sp, fsig,

0N/A insLink dg3 incl2 GlobalDef SeeTarget n node)

0N/A -- now the case with parameters

0N/A (_, 0) -> do

0N/A let fitargs = map item afitargs

0N/A (fitargs', dg', args, _) <- adj $ foldM

0N/A (anaFitArg lg opts spname imps gsigmaB)

0N/A ([], dg, [], extName "A" name) (zip params fitargs)

0N/A let actualargs = reverse args

0N/A (gsigma', morDelta) <- adj $ apply_GS lg gs actualargs

0N/A gsigmaRes <- case nsig of

0N/A EmptyNode _ -> return gsigma'

0N/A JustNode nsi -> adj $ gsigUnion lg (getSig nsi) gsigma'

342N/A let (nsr@(NodeSig node gsigmaRes'), dg2) =

0N/A insGSig dg' name (DGSpecInst spname) gsigmaRes

0N/A incl2 <- adj $ ginclusion lg gsigma' gsigmaRes'

0N/A morDelta' <- comp (gEmbed morDelta) incl2

0N/A dg3 <- foldM (parLink lg DGLinkFitSpec gsigmaRes' node) dg2

0N/A $ map snd args

342N/A let dg4 = insLink dg3 morDelta' GlobalDef SeeTarget nB node

0N/A dg5 <- case nsig of

0N/A EmptyNode _ -> return dg4

0N/A JustNode nsi@(NodeSig n _) -> do

0N/A incl1 <- adj $ ginclusion lg (getSig nsi) gsigmaRes'

0N/A return $ insLink dg4 incl1 GlobalDef SeeTarget n node

0N/A return (Spec_inst spname

0N/A (map (uncurry replaceAnnoted)

0N/A (zip (reverse fitargs') afitargs))

0N/A pos, nsr, dg5)

0N/A -- finally the case with conflicting numbers of formal and actual parameters

0N/A _ ->

0N/A fatal_error

0N/A (spstr ++ " expects " ++ show (length params) ++ " arguments"

0N/A ++ " but was given " ++ show (length afitargs)) pos

0N/A _ -> fatal_error

0N/A ("Structured specification " ++ spstr ++ " not found") pos

0N/A Data (Logic lidD) (Logic lidP) asp1 asp2 pos -> do

0N/A let sp1 = item asp1

0N/A sp2 = item asp2

0N/A adj = adjustPos pos

0N/A Comorphism cid <-

0N/A adj $ logicInclusion lg "Data" (Logic lidD) (Logic lidP)

0N/A let lidD' = sourceLogic cid

342N/A lidP' = targetLogic cid

342N/A (sp1', NodeSig n' (G_sign lid' sigma' _), dg') <-

0N/A ana_SPEC False lg dg (EmptyNode (Logic lidD)) (inc name) opts sp1

0N/A sigmaD <- adj $ coerceSign lid' lidD' "Analysis of data spec" sigma'

0N/A (sigmaD',sensD') <- adj $ ext_map_sign cid sigmaD

0N/A let (nsig2@(NodeSig node _), dg1) = insGTheory dg' name DGData

0N/A $ G_theory lidP' sigmaD' startSigId (toThSens sensD') startThId

0N/A dg2 = insLink dg1 (GMorphism cid sigmaD startSigId

342N/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/A pos, nsig3, dg3)

0N/A

0N/AanaPlainSpec :: Bool -> LogicGraph -> HetcatsOpts -> DGraph -> MaybeNode

0N/A -> 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 (getMaybeSig nsig) gsigma'

0N/A return (replaceAnnoted sp' asp, ns,

0N/A insLink dg2 incl dglType SeeTarget n' node)

0N/A

0N/AanaFitArg :: LogicGraph -> HetcatsOpts -> SPEC_NAME -> MaybeNode

0N/A -> G_sign -- ^ body signature

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 bsig (fas', dg1, args, name') (nsig', fa) = do

0N/A (fa', dg', arg) <- ana_FIT_ARG lg dg1 spname imps bsig nsig' opts name' fa

0N/A return (fa' : fas', dg', arg : args , inc name')

0N/A

0N/AparLink :: LogicGraph -> DGLinkOrigin -> G_sign -> Node -> DGraph -> NodeSig

0N/A -> Result DGraph

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

0N/A-- analysis of renamings

0N/Aana_ren :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism

347N/A -> G_mapping -> Result GMorphism

347N/Aana_ren lg opts lenv pos gmor@(GMorphism r _ _ mor _) gmap =

347N/A let adj = adjustPos pos in case gmap of

263N/A G_symb_map (G_symb_map_items_list lid sis) ->

356N/A if isStructured opts then return gmor else do

0N/A let lid2 = targetLogic r

0N/A extCod = mkExtSign $ cod mor

0N/A G_sign lid3 (ExtSign codom _) _ <- gSigCoerce lg "ana_ren1"

0N/A (G_sign lid2 extCod startSigId) (Logic lid)

0N/A sis1 <- adj $ coerceSymbMapItemsList lid lid3 "ana_ren1" sis

0N/A rmap <- adj $ stat_symb_map_items lid3 sis1

0N/A mor1 <- adj $ induced_from_morphism lid3 rmap codom

0N/A case lenv of

0N/A EmptyNode _ -> return ()

0N/A JustNode (NodeSig _ (G_sign lidLenv sigmaLenv _)) -> do

0N/A -- needs to be changed for logic translations

0N/A sigmaLenv' <- coerceSign lidLenv lid3

0N/A "Analysis of renaming: logic translations not properly handeled"

0N/A sigmaLenv

0N/A let sysLenv = ext_sym_of lid3 sigmaLenv'

0N/A m = symmap_of lid3 mor1

0N/A isChanged sy = case Map.lookup sy m of

0N/A Just sy' -> sy /= sy'

0N/A Nothing -> False

0N/A forbiddenSys = Set.filter isChanged sysLenv

0N/A when (not $ Set.null forbiddenSys) $ plain_error () (

0N/A "attempt to rename the following symbols from " ++

0N/A "the local environment:\n" ++ showDoc forbiddenSys "") pos

0N/A Comorphism i <- logicInclusion lg "ana_ren" (Logic lid2) (Logic lid3)

0N/A ext <- coerceSign lid2 (sourceLogic i) "ana_ren2" extCod

0N/A mor1' <- coerceMorphism lid3 (targetLogic i) "ana_ren3" mor1

0N/A gmor1 <- return $ GMorphism i ext startSigId mor1' startMorId

0N/A adj $ comp gmor gmor1

0N/A G_logic_translation (Logic_code tok src tar pos1) -> do

0N/A let adj1 = adjustPos $ if pos1 == nullRange then pos else pos1

0N/A G_sign srcLid srcSig ind<- return (cod gmor)

0N/A c <- adj1 $ case tok of

0N/A Just ctok -> do

0N/A Comorphism cid <- lookupComorphism (tokStr ctok) lg

0N/A when (isJust src && getLogicStr (fromJust src) /=

0N/A language_name (sourceLogic cid))

0N/A (fail (getLogicStr (fromJust src) ++

0N/A "is not the source logic of "

0N/A ++ language_name cid))

0N/A when (isJust tar && getLogicStr (fromJust tar) /=

0N/A language_name (targetLogic cid))

0N/A (fail (getLogicStr (fromJust tar) ++

0N/A "is not the target logic of "

0N/A ++ language_name cid))

0N/A return (Comorphism cid)

438N/A Nothing -> case tar of

0N/A Just (Logic_name l _) -> do

0N/A tarL <- lookupLogic "with logic: " (tokStr l) lg

0N/A logicInclusion lg "trans" (Logic srcLid) tarL

0N/A Nothing -> fail "with logic: cannot determine comorphism"

0N/A mor1 <- adj1 $ gEmbedComorphism c (G_sign srcLid srcSig ind)

0N/A adj $ comp gmor mor1

0N/A where getLogicStr (Logic_name l _) = tokStr l

0N/A

0N/Aana_RENAMING :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING

0N/A -> Result GMorphism

0N/Aana_RENAMING lg lenv gSigma opts (Renaming ren pos) =

0N/A foldM (ana_ren lg opts lenv pos) (ide gSigma) ren

0N/A

0N/A-- analysis of restrictions

0N/Aana_restr :: G_sign -> Range -> GMorphism -> G_hiding -> Result GMorphism

0N/Aana_restr (G_sign lidLenv sigmaLenv _) pos

0N/A (GMorphism cid (ExtSign sigma1 sys1) _ mor _) gh =

0N/A case gh of

0N/A G_symb_list (G_symb_items_list lid' sis') -> do

0N/A let lid1 = sourceLogic cid

0N/A sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction" sis'

0N/A rsys <- stat_symb_items lid1 sis1

0N/A let sys = sym_of lid1 sigma1

0N/A sys' = Set.filter (\ sy -> any (matches lid1 sy) rsys) sys

0N/A unmatched = filter ( \ rsy -> Set.null $ Set.filter

0N/A ( \ sy -> matches lid1 sy rsy) sys') rsys

0N/A when (not $ null unmatched)

0N/A $ plain_error () ("attempt to hide unknown symbols:\n"

0N/A ++ showDoc unmatched "") pos

0N/A -- needs to be changed when logic projections are implemented

0N/A sigmaLenv' <- coerceSign lidLenv lid1

0N/A "Analysis of restriction: logic projections not properly handeled"

0N/A sigmaLenv

0N/A let sysLenv = ext_sym_of lid1 sigmaLenv'

0N/A forbiddenSys = sys' `Set.intersection` sysLenv

0N/A when (not $ Set.null forbiddenSys)

0N/A $ plain_error () (

0N/A "attempt to hide the following symbols from the local environment:\n"

0N/A ++ showDoc forbiddenSys "") pos

0N/A mor1 <- cogenerated_sign lid1 sys' sigma1

0N/A mor1' <- map_morphism cid mor1

0N/A mor2 <- comp mor1' mor

0N/A return $ GMorphism cid (ExtSign (dom mor1) $ Set.fold (\ sy ->

0N/A case Map.lookup sy $ symmap_of lid1 mor1 of

0N/A Nothing -> id

0N/A Just sy1 -> Set.insert sy1) Set.empty sys1)

0N/A startSigId mor2 startMorId

0N/A G_logic_projection (Logic_code _tok _src _tar pos1) ->

0N/A fatal_error "no analysis of logic projections yet" pos1

0N/A

0N/Aana_RESTRICTION :: G_sign -> G_sign -> HetcatsOpts -> RESTRICTION

0N/A -> Result (GMorphism, Maybe GMorphism)

0N/Aana_RESTRICTION gSigma@(G_sign lid sigma _)

0N/A gSigma'@(G_sign lid' sigma' _) opts restr =

0N/A if isStructured opts then return (ide gSigma, Nothing) else

0N/A case restr of

0N/A Hidden rstr pos -> do

0N/A mor <- foldM (ana_restr gSigma pos) (ide gSigma') rstr

0N/A return (mor, Nothing)

0N/A Revealed (G_symb_map_items_list lid1 sis) pos -> do

0N/A let sys = ext_sym_of lid sigma -- local env

0N/A sys' = ext_sym_of lid' sigma' -- "big" signature

0N/A adj = adjustPos pos

0N/A sis' <- adj $ coerceSymbMapItemsList lid1 lid'

0N/A "Analysis of restriction" sis

0N/A rmap <- adj $ stat_symb_map_items lid' sis'

0N/A let sys'' =

0N/A Set.fromList

0N/A [sy | sy <- Set.toList sys', rsy <-

0N/A Map.keys rmap, matches lid' sy rsy]

0N/A -- domain of rmap intersected with sys'

0N/A -- domain of rmap should be checked to match symbols from sys' ???

0N/A sys1 <- adj $ coerceSymbolSet lid lid' "Analysis of restriction" sys

0N/A -- ??? this is too simple in case that local env is translated

0N/A -- to a different logic

0N/A mor1 <- adj $ ext_generated_sign lid' (sys1 `Set.union` sys'') sigma'

0N/A mor2 <- adj $ induced_from_morphism lid' rmap (dom mor1)

0N/A return (gEmbed (mkG_morphism lid' mor1),

0N/A Just (gEmbed (mkG_morphism lid' mor2)))

0N/A

0N/Aana_Gmaps :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range

0N/A -> G_sign -> G_sign -> [G_mapping] -> Result G_morphism

0N/Aana_Gmaps lg opts _ pos gsigP@(G_sign lidP sigmaP _)

0N/A gsigA@(G_sign lidA sigmaA _) gsis = do

0N/A let adj = adjustPos pos

438N/A adj $ if isStructured opts then return $ mkG_morphism lidP $ ext_ide sigmaP

0N/A else if null gsis then do

0N/A sigmaA' <- adj $ coerceSign lidA lidP "ana_Gmaps" sigmaA

0N/A fmap (mkG_morphism lidP) $

0N/A ext_induced_from_to_morphism lidP Map.empty sigmaP sigmaA'

0N/A else do

0N/A cl <- lookupCurrentLogic "ana_Gmaps" lg

0N/A G_symb_map_items_list lid sis <- homogenizeGM cl gsis

0N/A rmap <- stat_symb_map_items lid sis

0N/A let llid = Logic lid

0N/A noMatch sig r = Set.null $ Set.filter

0N/A (\ s -> matches lid s r) $ ext_sym_of lid sig

0N/A G_sign lidS sigmaS _ <- gSigCoerce lg "ana_Gmaps P" gsigP llid

0N/A G_sign lidT sigmaT _ <- gSigCoerce lg "ana_Gmaps A" gsigA llid

0N/A sigmaS' <- adj $ coerceSign lidS lid "ana_Gmaps1" sigmaS

0N/A sigmaT' <- adj $ coerceSign lidT lid "ana_Gmaps2" sigmaT

0N/A let unknowns = filter (noMatch sigmaS') (Map.keys rmap)

0N/A ++ filter (noMatch sigmaT') (Map.elems rmap)

0N/A if null unknowns then fmap (mkG_morphism lid)

0N/A $ ext_induced_from_to_morphism lid rmap sigmaS' sigmaT'

0N/A else fatal_error ("unknown symbols " ++ showDoc unknowns "") pos

0N/A {-

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?

342N/A if Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI

0N/A then return ()

0N/A else plain_error () "Fitting morphism must not affect import" pos

0N/A -} -- ??? does not work

0N/A -- ??? also output some symbol that is affected

0N/A

0N/Aana_FIT_ARG :: LogicGraph -> DGraph -> SPEC_NAME -> MaybeNode

0N/A -> G_sign -> NodeSig -> HetcatsOpts -> NodeName -> FIT_ARG

0N/A -> Result (FIT_ARG, DGraph, (G_morphism, NodeSig))

0N/Aana_FIT_ARG lg dg spname nsigI _bsig (NodeSig nP gsigmaP) opts name fv =

0N/A case fv of

0N/A Fit_spec asp gsis pos -> do

0N/A (sp', nsigA@(NodeSig nA gsigA), dg') <-

0N/A ana_SPEC False lg dg nsigI name opts (item asp)

0N/A gmor <- ana_Gmaps lg opts nsigI pos gsigmaP gsigA gsis

0N/A return (Fit_spec (replaceAnnoted sp' asp) gsis pos,

0N/A insLink dg' (gEmbed gmor) (GlobalThm LeftOpen None LeftOpen)

0N/A (DGLinkSpecInst spname) nP nA, (gmor, nsigA))

0N/A Fit_view vn afitargs pos -> let

0N/A adj = adjustPos pos

0N/A spstr = tokStr spname

0N/A in case lookupGlobalEnvDG vn dg of

0N/A Just (ViewEntry (ExtViewSig src mor gs@(ExtGenSig imps params _ target)))

0N/A -> do

0N/A let nSrc = getNode src

0N/A nTar = getNode target

0N/A gsigmaS = getSig src

0N/A gsigmaT = getSig target

0N/A gsigmaI = getMaybeSig nsigI

0N/A GMorphism cid _ _ morHom ind <- return mor

0N/A let lid = targetLogic cid

0N/A when (not (language_name (sourceLogic cid) == language_name lid))

0N/A (fatal_error

0N/A "heterogeneous fitting views not yet implemented"

0N/A pos)

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 (0, 0) -> case nsigI of

0N/A -- the subcase with empty import leads to a simpler dg

0N/A EmptyNode _ ->

0N/A return (fv, insLink dg (ide gsigmaP)

0N/A (GlobalThm LeftOpen None LeftOpen) (DGLinkFitView spname)

0N/A nP nSrc, (G_morphism lid morHom ind, target))

0N/A -- the subcase with nonempty import

0N/A JustNode (NodeSig nI _) -> do

0N/A gsigmaIS <- adj $ gsigUnion lg gsigmaI gsigmaS

0N/A when (not (isSubGsign lg gsigmaP gsigmaIS))

0N/A (plain_error ()

0N/A ("Parameter does not match source of fittig view. "

0N/A ++ "Parameter signature:\n"

0N/A ++ showDoc gsigmaP

0N/A "\nSource signature of fitting view (united with import):\n"

0N/A ++ showDoc gsigmaIS "") pos)

0N/A G_sign lidI sigI1 _ <- return gsigmaI

0N/A sigI <- adj $ coerceSign lidI lid

0N/A "Analysis of instantiation with import" sigI1

0N/A mor_I <- adj $ morphism_union lid morHom $ ext_ide sigI

0N/A gsigmaA <- adj $ gsigUnion lg gsigmaI gsigmaT

0N/A incl1 <- adj $ ginclusion lg gsigmaI gsigmaA

0N/A incl2 <- adj $ ginclusion lg gsigmaT gsigmaA

0N/A incl3 <- adj $ ginclusion lg gsigmaI gsigmaP

0N/A incl4 <- adj $ ginclusion lg gsigmaS gsigmaP

0N/A let (ns@(NodeSig nA _), dg1) =

0N/A insGSig dg name (DGFitViewA spname) gsigmaA

342N/A (NodeSig n' _, dg2) =

342N/A insGSig dg1 (inc name) (DGFitView spname) gsigmaP

342N/A dg3 = insLink dg2 incl1 GlobalDef

0N/A (DGLinkFitViewAImp spname) nI nA

342N/A dg4 = insLink dg3 incl3 GlobalDef

342N/A (DGLinkFitViewImp spname) nI n'

0N/A dg5 = insLink dg4 incl2 GlobalDef SeeTarget nTar nA

342N/A dg6 = insLink dg5 incl4 GlobalDef SeeTarget nSrc n'

0N/A dg7 = insLink dg6 (ide gsigmaP)

342N/A (GlobalThm LeftOpen None LeftOpen) SeeTarget nP n'

0N/A return (fv, dg7, (mkG_morphism lid mor_I, ns))

0N/A -- now the case with parameters

0N/A (_, 0) -> do

342N/A let fitargs = map item afitargs

0N/A (fitargs', dg', args,_) <- foldM (anaFitArg lg opts spname imps gsigmaT)

0N/A ([], dg, [], extName "A" name) (zip params fitargs)

342N/A let actualargs = reverse args

342N/A (gsigmaA,mor_f) <- adj $ apply_GS lg gs actualargs

342N/A let gmor_f = gEmbed mor_f

342N/A gsigmaRes <- adj $ gsigUnion lg gsigmaI gsigmaA

342N/A mor1 <- adj $ comp mor gmor_f

342N/A incl1 <- adj $ ginclusion lg gsigmaA gsigmaRes

342N/A mor' <- adj $ comp gmor_f incl1

342N/A GMorphism cid1 _ _ mor1Hom _<- return mor1

0N/A let lid1 = targetLogic cid1

113N/A when (not (language_name (sourceLogic cid1) == language_name lid1))

0N/A (fatal_error

342N/A ("heterogeneous fitting views not yet implemented")

342N/A pos)

342N/A G_sign lidI sigI1 _<- return gsigmaI

0N/A sigI <- adj $ coerceSign lidI lid1

113N/A "Analysis of instantiation with parameters" sigI1

342N/A theta <- adj $ morphism_union lid1 mor1Hom (ext_ide sigI)

113N/A incl2 <- adj $ ginclusion lg gsigmaI gsigmaRes

342N/A incl3 <- adj $ ginclusion lg gsigmaI gsigmaP

0N/A incl4 <- adj $ ginclusion lg gsigmaS gsigmaP

342N/A let (ns@(NodeSig nA _), dg1) =

0N/A insGSig dg' name (DGFitViewA spname) gsigmaRes

342N/A (NodeSig n' _, dg2) =

342N/A insGSig dg1 (extName "V" name) (DGFitView spname) gsigmaP

342N/A dg3 <- foldM (parLink lg (DGLinkFitView spname) gsigmaRes nA) dg2

342N/A $ map snd args

342N/A let dg4 = case nsigI of

0N/A EmptyNode _ -> dg3

342N/A JustNode (NodeSig nI _) -> let

342N/A dg3a = insLink dg3 incl2 GlobalDef

0N/A (DGLinkFitViewAImp spname) nI nA

0N/A in insLink dg3a incl3 GlobalDef (DGLinkFitViewImp spname) nI n'

0N/A dg5 = insLink dg4 mor' GlobalDef SeeTarget nTar nA

342N/A dg6 = insLink dg5 incl4 GlobalDef SeeTarget nSrc n'

342N/A dg7 = insLink dg6 (ide gsigmaP)

342N/A (GlobalThm LeftOpen None LeftOpen) SeeTarget nP n'

0N/A return (Fit_view vn

342N/A (map (uncurry replaceAnnoted)

342N/A (zip (reverse fitargs') afitargs))

113N/A pos, dg7, (mkG_morphism lid1 theta, ns))

342N/A-- finally the case with conflicting numbers of formal and actual parameters

342N/A _ ->

342N/A fatal_error

342N/A (spstr ++ " expects " ++ show (length params) ++ " arguments"

113N/A ++ " but was given " ++ show (length afitargs)) pos

342N/A _ -> fatal_error

0N/A ("View " ++ tokStr vn ++ " not found") pos

356N/A

356N/A-- Extension of signature morphisms (for instantitations)

356N/A-- first some auxiliary functions

356N/A

356N/AmapID :: Map.Map Id (Set.Set Id) -> Id -> Result Id

356N/AmapID idmap i@(Id toks comps pos1) =

356N/A case Map.lookup i idmap of

356N/A Nothing -> do

0N/A compsnew <- sequence $ map (mapID idmap) comps

356N/A return (Id toks compsnew pos1)

0N/A Just ids -> if Set.null ids then return i else

0N/A if Set.null $ Set.deleteMin ids then return $ Set.findMin ids else

356N/A plain_error i

0N/A ("Identifier component " ++ showId i

356N/A " can be mapped in various ways:\n"

0N/A ++ showDoc ids "") $ getRange i

356N/A

356N/AextID1 :: Map.Map Id (Set.Set Id) -> Id

356N/A -> Result (EndoMap Id) -> Result (EndoMap Id)

0N/AextID1 idmap i@(Id toks comps pos1) m = do

356N/A m1 <- m

0N/A compsnew <- sequence $ map (mapID idmap) comps

356N/A if comps==compsnew

113N/A then return m1

113N/A else return (Map.insert i (Id toks compsnew pos1) m1)

113N/A

356N/AextID :: Set.Set Id -> Map.Map Id (Set.Set Id) -> Result (EndoMap Id)

356N/AextID ids idmap = Set.fold (extID1 idmap) (return Map.empty) ids

356N/A

0N/AextendMorphism :: LogicGraph

113N/A -> G_sign -- ^ formal parameter

113N/A -> G_sign -- ^ body

356N/A -> G_sign -- ^ actual parameter

356N/A -> G_morphism -- ^ fitting morphism

0N/A -> Result(G_sign,G_morphism)

356N/AextendMorphism lg gsigP gsigB gsigA (G_morphism lid fittingMor _) = do

356N/A let llid = Logic lid

356N/A G_sign lidP sigmaP1 _ <- gSigCoerce lg "extendMorphism P" gsigP llid

356N/A ExtSign sigmaP _ <- coerceSign lidP lid "extendMorphismP" sigmaP1

356N/A G_sign lidB sigmaB1 _ <- gSigCoerce lg "extendMorphism B" gsigB llid

356N/A ExtSign sigmaB sysB <- coerceSign lidB lid "extendMorphismB" sigmaB1

356N/A let symsP = sym_of lid sigmaP

356N/A symsB = sym_of lid sigmaB

356N/A idsB = Set.map (sym_name lid) symsB

356N/A h = symmap_of lid fittingMor

0N/A symbMapToRawSymbMap =

356N/A Map.foldWithKey (\sy1 sy2 -> Map.insert (symbol_to_raw lid sy1)

356N/A (symbol_to_raw lid sy2))

356N/A Map.empty

356N/A rh = symbMapToRawSymbMap h

356N/A idh = Map.foldWithKey

356N/A (\sy1 sy2 -> Rel.setInsert (sym_name lid sy1) (sym_name lid sy2))

356N/A Map.empty h

356N/A idhExt <- extID idsB idh

356N/A let rIdExt = Map.foldWithKey (\id1 id2 -> Map.insert

356N/A (id_to_raw lid id1) (id_to_raw lid id2))

0N/A Map.empty

0N/A (foldr (\i -> Map.delete i) idhExt $ Map.keys idh)

0N/A r = rh `Map.union` rIdExt

0N/A -- do we need combining function catching the clashes???

0N/A mor <- induced_from_morphism lid r sigmaB

0N/A let hmor = symmap_of lid mor

356N/A sigmaAD = ExtSign (cod mor) $ Set.map (\ sy ->

0N/A Map.findWithDefault sy sy $ symmap_of lid mor) sysB

0N/A G_sign lidA sigmaA1 _ <- gSigCoerce lg "extendMorphism A" gsigA llid

356N/A sigmaA <- coerceSign lidA lid "extendMorphismA" sigmaA1

113N/A sigma <- ext_final_union lid sigmaA sigmaAD

113N/A let illShared = (ext_sym_of lid sigmaA `Set.intersection`

356N/A ext_sym_of lid sigmaAD )

356N/A Set.\\ Rel.image h symsP

356N/A when (not (Set.null illShared))

356N/A (plain_error () ("Symbols shared between actual parameter and body"

0N/A ++ "\nmust be in formal parameter:\n"

356N/A ++ showDoc illShared "") nullRange)

0N/A let myKernel m = Set.fromDistinctAscList $ comb1 $ Map.toList m

356N/A comb1 [] = []

356N/A comb1 (p : qs) =

0N/A comb2 p qs [] ++ comb1 qs

342N/A comb2 _ [] rs = rs

342N/A comb2 p@(a, b) ((c, d) : qs) rs =

0N/A comb2 p qs $ if b == d then (a, c) : rs else rs

356N/A newIdentifications = myKernel hmor Set.\\ myKernel h

0N/A when (not (Set.null newIdentifications))

0N/A (plain_error () (

0N/A "Fitting morphism leads to forbidden identifications:\n"

0N/A ++ showDoc newIdentifications "") nullRange)

0N/A incl <- ext_inclusion lid sigmaAD sigma

342N/A mor1 <- comp mor incl

356N/A return (G_sign lid sigma startSigId, mkG_morphism lid mor1)

0N/A

0N/Aapply_GS :: LogicGraph -> ExtGenSig -> [(G_morphism,NodeSig)]

0N/A -> Result(G_sign,G_morphism)

0N/Aapply_GS lg (ExtGenSig nsigI _ gsigmaP nsigB) args = do

0N/A let mor_i = map fst args

263N/A gsigmaA_i = map (getSig . snd) args

263N/A gsigmaB = getSig nsigB

0N/A gsigmaA <- gsigManyUnion lg gsigmaA_i

0N/A mor_f <- case nsigI of

0N/A EmptyNode _ -> homogeneousMorManyUnion mor_i

0N/A JustNode ns -> do

0N/A G_sign lidI sigmaI _<- return $ getSig ns

0N/A homogeneousMorManyUnion $ mkG_morphism lidI (ext_ide sigmaI) : mor_i

0N/A extendMorphism lg gsigmaP gsigmaB gsigmaA mor_f

0N/A

263N/A-- | homogenize an

263N/AhomogenizeGM :: AnyLogic -> [Syntax.AS_Structured.G_mapping]

263N/A -> Result G_symb_map_items_list

263N/AhomogenizeGM (Logic lid) gsis =

0N/A foldM homogenize1 (G_symb_map_items_list lid []) gsis

0N/A where

0N/A homogenize1 itl2@(G_symb_map_items_list lid2 sis) sm = case sm of

0N/A Syntax.AS_Structured.G_symb_map r@(G_symb_map_items_list lid1 sis1) ->

0N/A if null sis then return r else do

0N/A sis1' <- coerceSymbMapItemsList lid1 lid2 "homogenizeGM" sis1

263N/A return $ G_symb_map_items_list lid2 $ sis ++ sis1'

263N/A _ -> return itl2

263N/A

263N/A-- | check if structured analysis should be performed

356N/AisStructured :: HetcatsOpts -> Bool

0N/AisStructured a = case analysis a of

0N/A Structured -> True

0N/A _ -> False

0N/A

0N/A-- only consider addSyms for the first spec

342N/Aana_Extension

342N/A :: ([SPEC], MaybeNode, DGraph, LogicGraph, HetcatsOpts, Range, Bool)

0N/A -> (NodeName, Annoted SPEC)

0N/A -> Result ([SPEC], MaybeNode, DGraph, LogicGraph, HetcatsOpts, Range, Bool)

0N/Aana_Extension (sps', nsig', dg', lg, opts, pos, addSyms) (name',asp') = do

0N/A (sp1', nsig1@(NodeSig n1 sig1), dg1) <-

0N/A ana_SPEC addSyms lg dg' nsig' name' opts (item asp')

0N/A let anno = find isSemanticAnno $ l_annos asp'

263N/A -- is the extension going between real nodes?

263N/A dg2 <- case (anno, nsig') of

263N/A (Just anno0@(Semantic_anno anno1 _), JustNode (NodeSig n' sig')) -> do

263N/A -- any other semantic annotation? that's an error

263N/A when (any (\an -> isSemanticAnno an && an/=anno0) $ l_annos asp')

263N/A (plain_error () "Conflicting semantic annotations"

263N/A pos)

263N/A -- %implied should not occur here

263N/A when (anno1==SA_implied)

263N/A (plain_error ()

263N/A "Annotation %implied should come after a BASIC-ITEM"

263N/A pos)

263N/A if anno1==SA_implies then do

263N/A when (not (isHomSubGsign sig1 sig')) (plain_error ()

263N/A "Signature must not be extended in presence of %implies"

263N/A pos)

263N/A -- insert a theorem link according to p. 319 of the CASL Reference Manual

263N/A return $ insLink dg1 (ide sig1)

263N/A (GlobalThm LeftOpen None LeftOpen) DGLinkExtension n1 n'

263N/A else do

263N/A let anno2 = case anno1 of

0N/A SA_cons -> Cons

0N/A SA_def -> Def

0N/A SA_mono -> Mono

0N/A _ -> error "Static.AnalysisStructured: this cannot happen"

0N/A -- insert a theorem link according to p. 319 of the CASL Reference Manual

0N/A -- the theorem link is trivally proved by the parallel definition link,

0N/A -- but for clarity, we leave it open here

0N/A -- the interesting open proof obligation is anno2, of course

0N/A incl <- ginclusion lg sig' sig1

0N/A return $ insLink dg1 incl (GlobalThm LeftOpen anno2 LeftOpen)

0N/A DGLinkExtension n' n1

0N/A _ -> return dg1

0N/A return (sp1' : sps', JustNode nsig1, dg2, lg, opts, pos, True)

0N/A