0N/A{- |

3845N/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 , homogenizeGM

1472N/A , extendMorphism

0N/A ) where

0N/A

0N/Aimport Driver.Options

1879N/Aimport Logic.Logic

1879N/Aimport Logic.Coerce

1879N/Aimport Logic.Comorphism

1879N/Aimport Logic.Grothendieck

1879N/Aimport Logic.Prover

1879N/Aimport Static.DevGraph

1879N/Aimport Static.GTheory

0N/Aimport Syntax.AS_Structured

0N/Aimport Common.Result

0N/Aimport Common.Id

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

0N/Aimport qualified Data.Set as Set

0N/Aimport qualified Data.Map as Map

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

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

0N/Aimport Common.DocUtils

0N/Aimport Data.Maybe

0N/Aimport Data.List hiding (union)

0N/Aimport Control.Monad

0N/A

0N/AinsGTheory :: DGraph -> NODE_NAME -> 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 == 0 then s + 1 else ind

0N/A tb = tind == 0 && not (Map.null sens)

113N/A ntind = if tb then t + 1 else tind

0N/A nsig = G_sign lid sig nind

0N/A nth = G_theory lid sig nind sens ntind

3845N/A node_contents = newNodeLab name orig nth

3845N/A node = getNewNodeDG dg

3845N/A in (NodeSig node nsig,

3845N/A (if tb then setThMapDG $ Map.insert (t+1) nth tMap else id) $

3845N/A (if ind == 0 then setSigMapDG $ Map.insert (s+1) nsig sgMap else id)

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

0N/A

0N/AinsGSig :: DGraph -> NODE_NAME -> 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/A-- | analyze a SPEC

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 -> DGraph -> MaybeNode -> NODE_NAME ->

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

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

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

2772N/A do G_sign lid' sigma' i1 <- return (getMaybeSig nsig)

0N/A let adj = adjustPos pos

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

0N/A (bspec', sigma_complete, ax) <- adj $

0N/A if isStructured opts

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

113N/A (basic_analysis lid)

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

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

0N/A gTh = G_theory lid sigma_complete 0 (toThSens ax) 0

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

3845N/A incl <- adj $ ginclusion lg (G_sign lid sigma i1) gsig

3845N/A let incl' = updateMorIndex (m+1) incl

3845N/A link = DGLink { dgl_morphism = incl'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGExtension

0N/A , dgl_id = defaultEdgeID

0N/A }

0N/A dg'' = case nsig of

0N/A EmptyNode _ -> dg'

0N/A JustNode (NodeSig n _) -> insLEdgeNubDG (n,node,link) dg'

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

0N/A setMorMapDG (Map.insert (m+1) (toG_morphism incl') mrMap) 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 -}

0N/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 lg dg nsig (inc name) opts sp1

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

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 (ns@(NodeSig node _), dg'') = insGSig dg' name DGTranslation gsigma'

0N/A mor' = updateMorIndex (m+1) mor

0N/A link = (n',node,DGLink

0N/A { dgl_morphism = mor'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGTranslation

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A return (Translation (replaceAnnoted sp1' asp) ren, ns,

0N/A setMorMapDG (Map.insert (m+1) (toG_morphism mor') mrMap)

0N/A (insLEdgeNubDG link dg''))

0N/A Reduction asp restr ->

0N/A do let sp1 = item asp

0N/A (sp1', NodeSig n' gsigma', dg') <-

0N/A ana_SPEC lg dg nsig (inc name) opts sp1

0N/A let gsigma = getMaybeSig nsig

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

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 let hmor' = updateMorIndex (m+1) hmor

0N/A case tmor of

0N/A Nothing ->

0N/A do let gsigma'' = dom Grothendieck hmor

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

0N/A (ns@(NodeSig node _), dg'') = insGSig dg' name DGHiding gsigma''

0N/A link = (n',node,DGLink

0N/A { dgl_morphism = hmor'

0N/A , dgl_type = HidingDef

0N/A , dgl_origin = DGHiding

0N/A , dgl_id = defaultEdgeID

0N/A })

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

0N/A setMorMapDG (Map.insert (m+1) (toG_morphism hmor') mrMap)

0N/A (insLEdgeNubDG link dg''))

0N/A Just tmor' -> do

0N/A let gsigma1 = dom Grothendieck tmor'

0N/A gsigma'' = cod Grothendieck 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 Grothendieck (dom Grothendieck tmor')

0N/A then do

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

0N/A insGSig dg' name DGRevealing gsigma1

0N/A link1 = (n',node1,DGLink

0N/A { dgl_morphism = hmor'

0N/A , dgl_type = HidingDef

0N/A , dgl_origin = DGRevealing

0N/A , dgl_id = defaultEdgeID

0N/A })

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

0N/A setMorMapDG (Map.insert (m+1) (toG_morphism hmor')

0N/A mrMap) (insLEdgeNubDG link1 dg''))

0N/A else do

0N/A let (NodeSig node1 _, dg'') =

0N/A insGSig dg' (extName "T" name) DGRevealing gsigma1

0N/A (ns@(NodeSig node'' _), dg3) =

0N/A insGSig dg'' name DGRevealTranslation gsigma''

0N/A link1 = (n',node1,DGLink

0N/A { dgl_morphism = hmor'

0N/A , dgl_type = HidingDef

0N/A , dgl_origin = DGRevealing

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A link'' = (node1, node'',DGLink

0N/A { dgl_morphism = tmor'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGRevealTranslation

0N/A , dgl_id = defaultEdgeID

0N/A })

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

0N/A setMorMapDG (Map.insert (m+1) (toG_morphism hmor')

1009N/A mrMap)

0N/A (insLEdgeNubDG link'' $ insLEdgeNubDG link1 dg3))

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 r sp' = do

0N/A (sps1,nsigs,dg',n) <- r

0N/A (sp1,nsig',dg1) <- ana_SPEC lg dg' nsig n opts sp'

0N/A return (sp1:sps1,nsig':nsigs,dg1,inc n)

0N/A in foldl ana (return ([], [], 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 mdg (NodeSig n gsigma) = do

0N/A dgl <- mdg

0N/A let (mrMapl, ml) = morMapI dgl

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

0N/A let incl' = updateMorIndex (ml+1) incl

0N/A link = DGLink

0N/A { dgl_morphism = incl'

820N/A , dgl_type = GlobalDef

820N/A , dgl_origin = DGUnion

820N/A , dgl_id = defaultEdgeID

820N/A }

820N/A return $ setMorMapDG (Map.insert (ml+1)

113N/A (toG_morphism incl') mrMapl)

163N/A (insLEdgeNubDG (n, node, link) dgl)

163N/A dg3 <- foldl insE (return dg2) nsigs'

113N/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 foldl ana_Extension (return ([], nsig, dg, lg, opts, pos)) namedSps

0N/A case nsig1' of

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

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

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

0N/A pos, nsig1,dg1)

0N/A where

4122N/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') <-

3845N/A anaPlainSpec lg opts dg nsig name DGFree (FreeDef nsig) asp poss

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

0N/A Cofree_spec asp poss -> do

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

113N/A anaPlainSpec lg opts dg nsig name DGCofree (CofreeDef nsig) asp poss

113N/A return (Cofree_spec nasp poss, nsig', dg')

163N/A Local_spec asp asp' poss ->

163N/A do let sp1 = item asp

113N/A sp1' = item asp'

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

113N/A ana_SPEC lg dg nsig (extName "L" name) opts sp1

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

113N/A ana_SPEC lg dg' (JustNode nsig') (inc name) opts sp1'

113N/A let gsigma = getMaybeSig nsig

113N/A (mrMap, m) = morMapI dg''

113N/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 = sym_of lid sigma

221N/A sys1 = sym_of lid sigma1

221N/A sys2 = sym_of lid sigma2

827N/A pos = poss

827N/A mor3 <- if isStructured opts then return (ide lid sigma2)

827N/A else adjustPos pos $ cogenerated_sign lid

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

827N/A let sigma3 = dom lid mor3

221N/A -- gsigma2 = G_sign lid sigma2

221N/A gsigma3 = G_sign lid sigma3 0

221N/A sys3 = sym_of lid sigma3

221N/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 pos

0N/A let (ns@(NodeSig node _), dg2) = insGSig dg'' name DGLocal gsigma3

0N/A link = (n'', node, DGLink

0N/A { dgl_morphism = gEmbed2 gsigma3 (G_morphism lid 0 mor3 (m+1) 0)

0N/A , dgl_type = HidingDef

0N/A , dgl_origin = DGLocal

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A return (Local_spec (replaceAnnoted sp2 asp)

0N/A (replaceAnnoted sp2' asp')

0N/A poss, ns,

0N/A setMorMapDG (Map.insert (m+1) (G_morphism lid 0 mor3 (m+1) 0)

0N/A mrMap) $ insLEdgeNubDG link dg2)

0N/A Closed_spec asp pos ->

0N/A do let sp1 = item asp

0N/A l = getLogic nsig

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

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

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

0N/A let gsigma = getMaybeSig nsig

0N/A adj = adjustPos pos

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

0N/A gsigma'' <- adj $ gsigUnion lg gsigma gsigma'

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

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

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

0N/A let incl1' = updateMorIndex (m+1) incl1

0N/A incl2' = updateMorIndex (m+2) incl2

0N/A link1 = DGLink

0N/A { dgl_morphism = incl1'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGClosedLenv

0N/A , dgl_id = defaultEdgeID

0N/A }

0N/A link2 = (n',node,DGLink

0N/A { dgl_morphism = incl2'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGClosed

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A insLink1 = case nsig of

0N/A EmptyNode _ -> id

0N/A JustNode (NodeSig n _) -> insLEdgeNubDG (n, node, link1)

0N/A morMap1 = Map.insert (m+1) (toG_morphism incl1') mrMap

0N/A morMap2 = Map.insert (m+2) (toG_morphism incl2') morMap1

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

0N/A setMorMapDG morMap2 $

0N/A (insLink1 $ insLEdgeNubDG link2 dg2))

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 lg opts dg newNSig name DGLogicQual GlobalDef 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 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 (mrMap, m) = morMapI dg

0N/A in case lookupGlobalEnvDG spname dg of

0N/A Just (SpecEntry gs@(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 gsigma <- adj $ gsigUnion lg (getMaybeSig nsig) 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 incl1 = updateMorIndex (m+1) incl

0N/A link = (nB, node, DGLink

0N/A { dgl_morphism = incl1

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGSpecInst spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A morMap1 = Map.insert (m+1) (toG_morphism incl1) mrMap

0N/A dg3 = setMorMapDG morMap1 $ insLEdgeNubDG link dg2

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 && langNameSig gsigma' == langNameSig gsigmaB

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 return (sp, fsig, dg3)

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

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

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

0N/A let incl2' = updateMorIndex (m+2) incl2

0N/A link2 = (n,node,DGLink

0N/A { dgl_morphism = incl2'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGSpecInst spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A morMap2 = Map.insert (m+2) (toG_morphism incl2') morMap1

0N/A return (sp, fsig, setMorMapDG morMap2 $ insLEdgeNubDG link2 dg3)

0N/A -- now the case with parameters

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

0N/A let fitargs = map item afitargs

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

0N/A adj $ foldl (anaFitArg lg opts spname imps)

0N/A (return ([], dg, [], extName "A" name))

0N/A (zip params fitargs)

0N/A let actualargs = reverse args

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

0N/A gsigmaRes <- adj $ gsigUnion lg (getMaybeSig nsig) gsigma'

0N/A let (ns@(NodeSig node gsigmaRes'), dg2) =

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

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

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

0N/A let incl1' = updateMorIndex (m+1) incl1

0N/A incl2' = updateMorIndex (m+2) incl2

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

0N/A let link1 = DGLink

0N/A { dgl_morphism = incl1'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGSpecInst spname

0N/A , dgl_id = defaultEdgeID

0N/A }

0N/A insLink1 = case nsig of

0N/A EmptyNode _ -> id

0N/A JustNode (NodeSig n _) -> insLEdgeNubDG (n, node, link1)

0N/A link2 = (nB,node,DGLink

0N/A { dgl_morphism = morDelta'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGSpecInst spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A parLinks = catMaybes $

0N/A map (parLink lg DGFitSpec gsigmaRes' node . snd) actualargs

0N/A morMap1 = Map.insert (m+1) (toG_morphism incl1') mrMap

0N/A morMap2 = Map.insert (m+2) (toG_morphism incl2') morMap1

0N/A return (Spec_inst spname

0N/A (map (uncurry replaceAnnoted)

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

0N/A pos, ns,

0N/A setMorMapDG morMap2 $ foldr insLEdgeNubDG

0N/A (insLink1 $ insLEdgeNubDG link2 dg2)

0N/A parLinks)

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 <- 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 lg dg (EmptyNode (Logic lidD)) (inc name) opts sp1

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

1009N/A (sigmaD',sensD') <- adj $ map_sign cid sigmaD

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

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

0N/A link = (n',node,DGLink

0N/A { dgl_morphism = GMorphism cid sigmaD 0 (ide lidP' sigmaD') 0

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGData

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A dg2 = insLEdgeNubDG link dg1

0N/A (sp2',nsig3,dg3) <- ana_SPEC 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,

0N/A nsig3, dg3)

624N/A

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

0N/A -> DGOrigin -> DGLinkType -> Annoted SPEC -> Range

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

0N/AanaPlainSpec lg opts dg nsig name orig dglType asp pos = do

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

0N/A ana_SPEC 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 let (mrMap, m) = morMapI dg'

0N/A incl' = updateMorIndex (m+1) incl

0N/A link = (n', node, DGLink

0N/A { dgl_morphism = incl'

0N/A , dgl_type = dglType

0N/A , dgl_origin = orig

0N/A , dgl_id = defaultEdgeID })

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

0N/A setMorMapDG (Map.insert (m+1) (toG_morphism incl') mrMap)

0N/A $ insLEdgeNubDG link dg2)

0N/A

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

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

0N/A -> (NodeSig, FIT_ARG)

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

0N/AanaFitArg lg opts spname imps res (nsig', fa) = do

0N/A (fas', dg1, args, name') <- res

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

0N/AparLink :: LogicGraph -> DGOrigin -> G_sign -> Node -> NodeSig

0N/A -> Maybe (Node, Node, DGLinkLab)

0N/AparLink lg orig gsigma' node (NodeSig nA_i sigA_i) = do

0N/A incl <- maybeResult $ ginclusion lg sigA_i gsigma'

145N/A let link = DGLink

0N/A { dgl_morphism = incl

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = orig

0N/A , dgl_id = defaultEdgeID }

0N/A return (nA_i, node, link)

0N/A

1009N/A-- analysis of renamings

0N/A

0N/Aana_ren1 :: LogicGraph -> MaybeNode -> Range -> GMorphism -> G_mapping

0N/A -> Result GMorphism

0N/Aana_ren1 _ lenv _pos (GMorphism r sigma ind1 mor _)

0N/A (G_symb_map (G_symb_map_items_list lid sis)) = do

0N/A let lid2 = targetLogic r

0N/A sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis

0N/A rmap <- stat_symb_map_items lid2 sis1

0N/A mor1 <- induced_from_morphism lid2 rmap (cod lid2 mor)

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 lid2

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

0N/A sigmaLenv

0N/A let sysLenv = sym_of lid2 sigmaLenv'

0N/A m = symmap_of lid2 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 return ()

0N/A{- when (not (forbiddenSys == Set.empty)) $ plain_error () (

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

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

0N/A-}

0N/A mor2 <- comp lid2 mor mor1

0N/A return $ GMorphism r sigma ind1 mor2 0

0N/A

0N/Aana_ren1 lg _ _ mor (G_logic_translation (Logic_code tok src tar pos1)) = do

0N/A let adj = adjustPos pos1

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

0N/A c <- adj $ 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)

0N/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 (Logic srcLid) tarL

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

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

0N/A adj $ comp Grothendieck mor mor1

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

0N/A

0N/Aana_ren :: LogicGraph -> MaybeNode -> Range -> Result GMorphism -> G_mapping

0N/A -> Result GMorphism

0N/Aana_ren lg lenv pos mor_res ren =

0N/A do mor <- mor_res

0N/A ana_ren1 lg lenv pos mor ren

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 if isStructured opts

0N/A then return (ide Grothendieck gSigma)

0N/A else foldl (ana_ren lg lenv pos) (return (ide Grothendieck gSigma)) ren

0N/A

0N/A-- analysis of restrictions

0N/A

0N/Aana_restr1 :: DGraph -> G_sign -> Range -> GMorphism -> G_hiding

0N/A -> Result GMorphism

0N/Aana_restr1 _ (G_sign lidLenv sigmaLenv _) pos

0N/A (GMorphism cid sigma1 _ mor _)

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

0N/A let lid1 = sourceLogic cid

0N/A lid2 = targetLogic 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 yet properly handeled"

820N/A sigmaLenv

820N/A let sysLenv = sym_of lid1 sigmaLenv'

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

820N/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

3845N/A mor2 <- comp lid2 mor1' mor

3845N/A return $ GMorphism cid (dom lid1 mor1) 0 mor2 0

3845N/A

3845N/Aana_restr1 _dg _gSigma _mor _pos

3845N/A (G_logic_projection (Logic_code _tok _src _tar pos1)) =

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

3845N/A

3845N/Aana_restr :: DGraph -> G_sign -> Range -> Result GMorphism -> G_hiding

3845N/A -> Result GMorphism

3845N/Aana_restr dg gSigma pos mor_res restr =

3845N/A do mor <- mor_res

3845N/A ana_restr1 dg gSigma pos mor restr

3845N/A

3845N/Aana_RESTRICTION :: DGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION

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

3845N/Aana_RESTRICTION dg gSigma gSigma' opts restr =

3845N/A ana_RESTRICTION' dg gSigma gSigma' (isStructured opts) restr

3845N/A

3845N/Aana_RESTRICTION' :: DGraph -> G_sign -> G_sign -> Bool -> RESTRICTION

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

3845N/Aana_RESTRICTION' _ _ gSigma True _ =

3845N/A return (ide Grothendieck gSigma,Nothing)

3845N/Aana_RESTRICTION' dg gSigma gSigma' False (Hidden restr pos) =

3845N/A do mor <- foldl (ana_restr dg gSigma pos)

3845N/A (return (ide Grothendieck gSigma'))

3845N/A restr

3845N/A return (mor,Nothing)

3845N/A -- ??? Need to check that local env is not affected !

3845N/Aana_RESTRICTION' _ (G_sign lid sigma _) (G_sign lid' sigma' si')

3845N/A False (Revealed (G_symb_map_items_list lid1 sis) pos) =

3845N/A do let sys = sym_of lid sigma -- local env

3845N/A sys' = sym_of lid' sigma' -- "big" signature

3845N/A adj = adjustPos pos

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

3845N/A "Analysis of restriction" sis

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

3845N/A let sys'' =

3845N/A Set.fromList

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

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

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

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

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

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

3845N/A -- to a different logic

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

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

3845N/A return (gEmbed (G_morphism lid' si' mor1 0 0),

3845N/A Just (gEmbed (G_morphism lid' 0 mor2 0 0)))

3845N/A

3845N/A

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

3845N/A -> NodeSig -> HetcatsOpts -> NODE_NAME -> FIT_ARG

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

3845N/Aana_FIT_ARG lg dg spname nsigI

3845N/A (NodeSig nP (G_sign lidP sigmaP _)) opts name

3845N/A (Fit_spec asp gsis pos) = do

3845N/A let adj = adjustPos pos

3845N/A (sp', nsigA@(NodeSig nA (G_sign lidA sigmaA _)), dg') <-

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

3845N/A G_symb_map_items_list lid sis <- homogenizeGM (Logic lidP) gsis

3845N/A sigmaA' <- adj $ coerceSign lidA lidP "Analysis of fitting argument" sigmaA

3845N/A mor <- adj $ if isStructured opts then return (ide lidP sigmaP)

0N/A else do

0N/A rmap <- stat_symb_map_items lid sis

0N/A rmap' <- if null sis then return Map.empty

0N/A else coerceRawSymbolMap lid lidP

0N/A "Analysis of fitting argument" rmap

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

113N/A (\ s -> matches lidP s r) $ sym_of lidP sig

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

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

0N/A if null unknowns then

0N/A induced_from_to_morphism lidP rmap' sigmaP sigmaA'

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?

0N/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 let link = (nP,nA,DGLink

0N/A { dgl_morphism = gEmbed (G_morphism lidP 0 mor 0 0)

0N/A , dgl_type = GlobalThm LeftOpen None LeftOpen

0N/A , dgl_origin = DGSpecInst spname

0N/A , dgl_id = defaultEdgeID

0N/A })

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

0N/A insLEdgeNubDG link dg',

0N/A (G_morphism lidP 0 mor 0 0,nsigA)

0N/A )

306N/A

306N/Aana_FIT_ARG lg dg spname nsigI (NodeSig nP gsigmaP)

0N/A opts name fv@(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 (src, mor, gs@(imps, params, _, target))) -> 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 _ -> do

0N/A let link = (nP,nSrc,DGLink

0N/A { dgl_morphism = ide Grothendieck gsigmaP

0N/A , dgl_type = GlobalThm LeftOpen None LeftOpen

0N/A , dgl_origin = DGFitView spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A return (fv, insLEdgeNubDG link dg,

0N/A (G_morphism lid 0 morHom ind 0, 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 $ ide lid 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

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

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

0N/A link = (nP,n',DGLink

0N/A { dgl_morphism = ide Grothendieck gsigmaP

0N/A , dgl_type = GlobalThm LeftOpen None LeftOpen

0N/A , dgl_origin = DGFitView spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A link1 = (nSrc,n',DGLink

0N/A { dgl_morphism = incl4

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGFitView spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A link2 = (nTar,nA,DGLink

0N/A { dgl_morphism = incl2

163N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGFitViewA spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A link3 = (nI,n',DGLink

0N/A { dgl_morphism = incl3

223N/A , dgl_type = GlobalDef

223N/A , dgl_origin = DGFitViewImp spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A link4 = (nI,nA,DGLink

0N/A { dgl_morphism = incl1

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGFitViewAImp spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A return (fv, insLEdgeNubDG link $

163N/A insLEdgeNubDG link1 $

0N/A insLEdgeNubDG link2 $

223N/A insLEdgeNubDG link3 $

223N/A insLEdgeNubDG link4 dg2,

223N/A (G_morphism lid 0 mor_I 0 0, ns))

223N/A -- now the case with parameters

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

0N/A let fitargs = map item afitargs

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

223N/A foldl (anaFitArg lg opts spname imps)

223N/A (return ([], dg, [], extName "A" name))

0N/A (zip params fitargs)

0N/A let actualargs = reverse args

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

0N/A let gmor_f = gEmbed mor_f

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

0N/A mor1 <- adj $ comp Grothendieck mor gmor_f

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

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

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

0N/A let lid1 = targetLogic cid1

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

0N/A (fatal_error

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

0N/A pos)

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

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

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

0N/A theta <- adj $ morphism_union lid1 mor1Hom (ide lid1 sigI)

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

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

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

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

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

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

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

992N/A link = (nP,n',DGLink

0N/A { dgl_morphism = ide Grothendieck gsigmaP

0N/A , dgl_type = GlobalThm LeftOpen None LeftOpen

0N/A , dgl_origin = DGFitView spname

0N/A , dgl_id = defaultEdgeID

163N/A })

163N/A link1 = (nSrc,n',DGLink

163N/A { dgl_morphism = incl4

163N/A , dgl_type = GlobalDef

163N/A , dgl_origin = DGFitView spname

223N/A , dgl_id = defaultEdgeID

223N/A })

223N/A link2 = (nTar,nA,DGLink

0N/A { dgl_morphism = mor'

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGFitViewA spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A fitLinks = [link,link1,link2] ++ case nsigI of

0N/A EmptyNode _ -> []

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

0N/A link3 = (nI,n',DGLink

0N/A { dgl_morphism = incl3

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGFitViewImp spname

306N/A , dgl_id = defaultEdgeID

0N/A })

0N/A link4 = (nI,nA,DGLink

0N/A { dgl_morphism = incl2

0N/A , dgl_type = GlobalDef

0N/A , dgl_origin = DGFitViewAImp spname

0N/A , dgl_id = defaultEdgeID

0N/A })

0N/A in [link3,link4]

0N/A parLinks = catMaybes $ map

0N/A (parLink lg (DGFitView spname) gsigmaRes nA . snd) actualargs

0N/A return (Fit_view vn

0N/A (map (uncurry replaceAnnoted)

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

0N/A pos,

0N/A foldr insLEdgeNubDG dg2

0N/A (fitLinks ++ parLinks),

0N/A (G_morphism lid1 0 theta 0 0, ns))

0N/A

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 ("View " ++ tokStr vn ++ " not found") pos

0N/A

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

0N/A-- first some auxiliary functions

0N/A

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

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

0N/A case Map.lookup i idmap of

0N/A Nothing -> do

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

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

0N/A plain_error i

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

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

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

0N/A

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

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

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

0N/A m1 <- m

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

0N/A if comps==compsnew

0N/A then return m1

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

0N/A

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

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

0N/A

0N/AextendMorphism :: G_sign -- ^ formal parameter

223N/A -> G_sign -- ^ body

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

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

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

0N/AextendMorphism (G_sign lid sigmaP _) (G_sign lidB sigmaB1 _)

0N/A (G_sign lidA sigmaA1 _) (G_morphism lidM _ fittingMor1 _ _) = do

0N/A -- for now, only homogeneous instantiations....

0N/A sigmaB <- coerceSign lidB lid "Extension of symbol map" sigmaB1

0N/A sigmaA <- coerceSign lidA lid "Extension of symbol map" sigmaA1

0N/A fittingMor <- coerceMorphism lidM lid "Extension of symbol map" fittingMor1

0N/A let symsP = sym_of lid sigmaP

223N/A symsB = sym_of lid sigmaB

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

306N/A h = symmap_of lid fittingMor

0N/A symbMapToRawSymbMap =

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

0N/A (symbol_to_raw lid sy2))

0N/A Map.empty

0N/A rh = symbMapToRawSymbMap h

0N/A idh = Map.foldWithKey

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

0N/A Map.empty h

0N/A idhExt <- extID idsB idh

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

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

0N/A sigmaAD = cod lid mor

0N/A sigma <- final_union lid sigmaA sigmaAD

1681N/A let illShared = (sym_of lid sigmaA `Set.intersection` sym_of lid sigmaAD )

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

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

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

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

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

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

1681N/A comb1 [] = []

1681N/A comb1 (p : qs) =

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

1681N/A comb2 _ [] rs = rs

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

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

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

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

1681N/A (plain_error () (

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

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

0N/A incl <- inclusion lid sigmaAD sigma

0N/A mor1 <- comp lid mor incl

0N/A return (G_sign lid sigma 0, G_morphism lid 0 mor1 0 0)

0N/A

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

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

0N/Aapply_GS lg (nsigI,_params,gsigmaP,nsigB) args = do

0N/A let mor_i = map fst args

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

0N/A gsigmaB = getSig nsigB

0N/A gsigmaI = getMaybeSig nsigI

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

0N/A let idI = ide lidI sigmaI

223N/A gsigmaA <- gsigManyUnion lg gsigmaA_i

0N/A mor_f <- homogeneousMorManyUnion (G_morphism lidI 0 idI 0 0:mor_i)

223N/A extendMorphism gsigmaP gsigmaB gsigmaA mor_f

0N/A

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

0N/A -> Result G_symb_map_items_list

0N/AhomogenizeGM (Logic lid) gsis =

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

0N/A where

223N/A homogenize1 res

0N/A (Syntax.AS_Structured.G_symb_map (G_symb_map_items_list lid1 sis1)) = do

0N/A (G_symb_map_items_list lid2 sis) <- res

366N/A sis1' <- coerceSymbMapItemsList lid1 lid2 "" sis1

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

0N/A homogenize1 res _ = res

306N/A

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

0N/AisStructured :: HetcatsOpts -> Bool

0N/AisStructured a = case analysis a of

0N/A Structured -> True

0N/A _ -> False

0N/A

0N/Aana_Extension :: Result ([SPEC],MaybeNode, DGraph,

163N/A LogicGraph, HetcatsOpts, Range)

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

0N/A Result ([SPEC], MaybeNode, DGraph,

0N/A LogicGraph, HetcatsOpts, Range)

0N/Aana_Extension res (name',asp') = do

0N/A (sps', nsig', dg',lg,opts, pos) <- res

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

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

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

0N/A mrMapl = morMap dg1

0N/A ml = if Map.null mrMapl then 0 else fst $ Map.findMax mrMapl

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

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

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

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

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

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

820N/A pos)

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

0N/A when (anno1==SA_implied)

0N/A (plain_error ()

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

0N/A pos)

0N/A if anno1==SA_implies then do

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

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

0N/A pos)

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

0N/A return $ insLEdgeNubDG (n1, n', DGLink

0N/A { dgl_morphism = ide Grothendieck sig1

0N/A , dgl_type = GlobalThm LeftOpen None LeftOpen

0N/A , dgl_origin = DGExtension

0N/A , dgl_id = defaultEdgeID

0N/A }) dg1

0N/A else do

555N/A let anno2 = case anno1 of

555N/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 let incl' = updateMorIndex (ml+1) incl

0N/A return $ setMorMapDG (Map.insert (ml+1) (toG_morphism incl')

0N/A mrMapl )

0N/A (insLEdgeNubDG (n', n1, DGLink

0N/A { dgl_morphism = incl'

0N/A , dgl_type = GlobalThm LeftOpen anno2 LeftOpen

306N/A , dgl_origin = DGExtension

0N/A , dgl_id = defaultEdgeID

0N/A }) dg1)

0N/A _ -> return dg1

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

0N/A