0N/A{- |

2362N/AModule : $Header$

1008N/ADescription : static analysis of heterogeneous structured specifications

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

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

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

2362N/AStability : provisional

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

2362N/A

1008N/AStatic analysis of CASL (heterogeneous) structured specifications

1008N/A Follows the verfication semantic rules in Chap. IV:4.7

1008N/A of the CASL Reference Manual.

1008N/A-}

1008N/A

1008N/Amodule Static.AnalysisStructured

1008N/A ( anaSpec

1008N/A , anaSpecTop

1008N/A , anaUnion

1008N/A , getSpecAnnos

1008N/A , isStructured

2362N/A , anaRenaming

2362N/A , anaRestriction

2362N/A , homogenizeGM

1008N/A , anaGmaps

1008N/A , insGSig

1008N/A , insLink

1008N/A , extendMorphism

0N/A , insGTheory

0N/A ) where

1821N/A

1821N/Aimport Driver.Options

1821N/A

1821N/Aimport Logic.Logic

1821N/Aimport Logic.ExtSign

1821N/Aimport Logic.Coerce

1821N/Aimport Logic.Comorphism

1821N/Aimport Logic.Grothendieck

1821N/Aimport Logic.Prover

1821N/A

2391N/Aimport Static.DevGraph

1821N/Aimport Static.GTheory

1821N/A

2391N/Aimport Syntax.AS_Structured

1821N/A

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

1821N/Aimport Common.DocUtils

2391N/Aimport Common.ExtSign

1821N/Aimport Common.Id

1821N/Aimport Common.Result

1821N/Aimport Common.Utils (number)

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

1821N/A

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

1821N/Aimport qualified Data.Set as Set

1821N/Aimport qualified Data.Map as Map

1821N/Aimport Data.Maybe

1821N/Aimport Data.List (find)

1821N/A

1821N/Aimport Control.Monad

1008N/A

1008N/AcoerceMaybeNode :: LogicGraph -> DGraph -> MaybeNode -> NodeName -> AnyLogic

1821N/A -> Result (MaybeNode, DGraph)

1008N/AcoerceMaybeNode lg dg mn nn l2 = case mn of

1008N/A EmptyNode _ -> return (EmptyNode l2, dg)

1008N/A JustNode ns -> do

1008N/A (ms, dg2) <- coerceNode lg dg ns nn l2

1008N/A return (JustNode ms, dg2)

1821N/A

1821N/AcoerceNode :: LogicGraph -> DGraph -> NodeSig -> NodeName -> AnyLogic

1821N/A -> Result (NodeSig, DGraph)

1821N/AcoerceNode lg dg ns@(NodeSig n s@(G_sign lid1 _ _)) nn l2@(Logic lid2) =

1821N/A if language_name lid1 == language_name lid2 then return (ns, dg)

1821N/A else do

1821N/A c <- logicInclusion lg (Logic lid1) l2

1821N/A gmor <- gEmbedComorphism c s

2228N/A case find (\ (_, _, l) -> dgl_origin l == SeeTarget

2228N/A && dgl_type l == globalDef

2228N/A && dgl_morphism l == gmor) $ outDG dg n of

2228N/A Nothing -> do

1821N/A let (ms@(NodeSig m _), dg2) =

0N/A insGSig dg (extName "XCoerced" nn) DGTranslation $ cod gmor

2402N/A dg3 = insLink dg2 gmor globalDef SeeTarget n m

2402N/A return (ms, dg3)

2402N/A Just (_, t, _) ->

2402N/A return (NodeSig t $ signOf $ dgn_theory $ labDG dg t, dg)

2402N/A

2402N/AinsGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)

2402N/AinsGTheory dg name orig (G_theory lid sig ind sens tind) =

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

2402N/A (tMap, t) = thMapI dg

2402N/A nind = if ind == startSigId then succ s else ind

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

2402N/A ntind = if tb then succ t else tind

2402N/A nsig = G_sign lid sig nind

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

2402N/A node_contents = newNodeLab name orig nth

2402N/A node = getNewNodeDG dg

2402N/A in (NodeSig node nsig,

2402N/A (if tb then setThMapDG $ Map.insert (succ t) nth tMap else id) $

2402N/A (if ind == startSigId

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

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

1008N/A

1821N/AinsGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)

1821N/AinsGSig dg name orig (G_sign lid sig ind) =

1821N/A insGTheory dg name orig $ noSensGTheory lid sig ind

2228N/A

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

2228N/A -> DGraph

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

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

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

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

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

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

2228N/A link = DGLink

2402N/A { dgl_morphism = nmor

2402N/A , dgl_type = ty

2402N/A , dgl_origin = orig

2402N/A , dgl_id = defaultEdgeId }

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

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

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

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

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

2402N/A

2402N/AcreateConsLink :: LinkKind -> Conservativity -> LogicGraph -> DGraph

2402N/A -> MaybeNode -> NodeSig -> DGLinkOrigin -> Result DGraph

2402N/AcreateConsLink lk conser lg dg nsig (NodeSig node gsig) orig = case nsig of

2402N/A EmptyNode _ | conser == None -> return dg

2402N/A _ -> case nsig of

2402N/A JustNode (NodeSig n sig)-> do

2402N/A let Result _ mIncl = ginclusion lg sig gsig

2402N/A case mIncl of

2402N/A Just incl ->

2402N/A return $ insLink dg incl

2402N/A (ScopedLink Global lk $ mkConsStatus conser) orig n node

1821N/A Nothing -> do

2228N/A unless (conser == None) $ warning ()

2228N/A "ingoring conservativity annotation between non-subsignatures"

2228N/A nullRange

2228N/A return dg

2228N/A EmptyNode _ -> -- add conservativity to the target node

2228N/A return $ let lbl = labDG dg node

2228N/A in if isDGRef lbl then dg else

2228N/A fst $ labelNodeDG

2228N/A (node, lbl

2228N/A { nodeInfo =

2228N/A (nodeInfo lbl)

1821N/A { node_cons_status = case getNodeConsStatus lbl of

1821N/A ConsStatus c d th -> ConsStatus (max c conser) d th }}) dg

1821N/A

2228N/AanaSpecTop :: Conservativity -> Bool -> LogicGraph -> DGraph -> MaybeNode

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

2228N/AanaSpecTop conser addSyms lg dg nsig name opts sp =

2228N/A if conser == None || case sp of

2228N/A -- for these cases def-links are re-used

1821N/A Basic_spec _ _ -> True

2228N/A Closed_spec _ _ -> True

1821N/A Spec_inst _ _ _ -> True

2228N/A Group _ _ -> True -- in this case we recurse

2228N/A _ -> False

1821N/A then anaSpecAux conser addSyms lg dg nsig name opts sp else do

2228N/A let provenThmLink =

1821N/A ThmLink $ Proven (DGRule "static analysis") emptyProofBasis

1821N/A (rsp, ns, rdg) <- anaSpec addSyms lg dg nsig name opts sp

1821N/A ndg <- createConsLink provenThmLink conser lg rdg nsig ns SeeTarget

1821N/A return (rsp, ns, ndg)

1821N/A

1821N/AanaQualSpec :: Bool -> LogicGraph -> HetcatsOpts -> DGraph

1821N/A -> MaybeNode -> NodeName -> Annoted SPEC -> Range

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

1821N/AanaQualSpec addSyms lg opts dg nsig name asp pos = do

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

2228N/A anaSpec addSyms lg dg nsig (extName "Qualified" name) opts $ item asp

1821N/A let (ns@(NodeSig node gsigma'), dg2) =

1821N/A insGSig dg' name DGLogicQual gsigma

1821N/A incl <- adjustPos pos $ ginclusion lg gsigma gsigma'

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

1821N/A insLink dg2 incl globalDef SeeTarget n' node)

1821N/A

1821N/AanaFreeOrCofreeSpec :: Bool -> LogicGraph -> HetcatsOpts -> DGraph

1821N/A -> MaybeNode -> NodeName -> FreeOrCofree -> Annoted SPEC -> Range

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

1821N/AanaFreeOrCofreeSpec addSyms lg opts dg nsig name dglType asp pos = do

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

0N/A anaSpec addSyms lg dg nsig (extName (show dglType) name) opts

0N/A $ item asp

2228N/A let (ns@(NodeSig node gsigma'), dg2) =

2228N/A insGSig dg' name (DGFreeOrCofree dglType) gsigma

2228N/A nsigma <- return $ case nsig of

2228N/A EmptyNode cl -> emptyG_sign cl

2228N/A JustNode nds -> getSig nds

2228N/A incl <- adjustPos pos $ ginclusion lg nsigma gsigma'

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

1821N/A insLink dg2 incl (FreeOrCofreeDefLink dglType nsig)

0N/A SeeTarget n' node)

1008N/A

1008N/A-- | analyze a SPEC

1008N/A-- Bool Parameter determines if incoming symbols shall be ignored

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

2228N/AanaSpec :: Bool -> LogicGraph -> DGraph -> MaybeNode -> NodeName

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

2228N/AanaSpec = anaSpecAux None

2228N/A

0N/AanaSpecAux :: Conservativity -> Bool -> LogicGraph -> DGraph -> MaybeNode

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

1008N/AanaSpecAux conser addSyms lg dg nsig name opts sp = case sp of

1008N/A Basic_spec (G_basic_spec lid bspec) pos -> adjustPos pos $ do

2228N/A let curLogic = Logic lid

2228N/A (nsig', dg0) <- coerceMaybeNode lg dg nsig name curLogic

2228N/A G_sign lid' sigma' _ <- return $ case nsig' of

2228N/A EmptyNode cl -> emptyG_sign cl

2228N/A JustNode ns -> getSig ns

2228N/A ExtSign sig sys <-

2228N/A coerceSign lid' lid "Analysis of basic spec" sigma'

1008N/A (bspec', ExtSign sigma_complete sysd, ax) <-

1008N/A if isStructured opts

1008N/A then return (bspec, mkExtSign $ empty_signature lid, [])

1008N/A else do

1008N/A b <- maybeToMonad

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

1821N/A (basic_analysis lid)

1008N/A b (bspec, sig, globalAnnos dg0)

1008N/A let gsysd = Set.map (G_symbol lid) sysd

0N/A (ns, dg') = insGTheory dg0 name (DGBasicSpec gsysd)

0N/A $ G_theory lid (ExtSign sigma_complete

1008N/A $ Set.intersection

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

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

1008N/A dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension

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

0N/A EmptySpec pos -> case nsig of

1821N/A EmptyNode _ -> do

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

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

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

1821N/A {- anaSpec should be changed to return a MaybeNode!

1821N/A Then this duplicate dummy node could be avoided.

1821N/A Also empty unions could be treated then -}

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

1821N/A Translation asp ren ->

1821N/A do let sp1 = item asp

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

1821N/A anaSpec addSyms lg dg nsig (extName "Translation" name) opts sp1

1821N/A mor <- anaRenaming lg nsig gsigma opts ren

1821N/A -- ??? check that mor is identity on local env

1821N/A let (ns@(NodeSig node _), dg'') =

2402N/A insGSig dg' name DGTranslation $ cod mor

2402N/A -- ??? too simplistic for non-comorphism inter-logic translations

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

2391N/A insLink dg'' mor globalDef SeeTarget n' node)

2391N/A Reduction asp restr ->

1008N/A do let sp1 = item asp

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

1008N/A anaSpec addSyms lg dg nsig (extName "Restriction" name) opts sp1

1008N/A let gsigma = getMaybeSig nsig

1008N/A (hmor, tmor) <- anaRestriction gsigma gsigma' opts restr

0N/A -- we treat hiding and revealing differently

1008N/A -- in order to keep the dg as simple as possible

1008N/A case tmor of

2391N/A Nothing ->

1008N/A do let (ns@(NodeSig node _), dg'') =

1008N/A insGSig dg' name DGHiding $ dom hmor

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

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

1821N/A insLink dg'' hmor HidingDefLink SeeTarget n' node)

1821N/A Just tmor' -> do

1821N/A let gsigma1 = dom tmor'

1821N/A gsigma'' = cod tmor'

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

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

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

1947N/A then do

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

1947N/A insGSig dg' name DGRevealing gsigma1

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

1947N/A insLink dg'' hmor HidingDefLink SeeTarget n' node1)

1947N/A else do

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

1947N/A insGSig dg' (extName "Revealing" name) DGRevealing gsigma1

1821N/A (ns@(NodeSig node2 _), dg3) =

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

1947N/A dg4 = insLink dg3 hmor HidingDefLink SeeTarget n' node1

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

1947N/A insLink dg4 tmor' globalDef SeeTarget node1 node2)

1947N/A Union asps pos -> do

1821N/A (newAsps, _, ns, dg') <- adjustPos pos $ anaUnion addSyms lg dg nsig

2017N/A name opts asps

1821N/A return (Union newAsps pos, ns, dg')

1821N/A Extension asps pos -> do

1821N/A let namedSps = map (\ (asp, n) ->

1821N/A let nn = incBy n (extName "Extension" name) in

1821N/A if n < length asps then (nn, asp)

1821N/A else (name { xpath = xpath nn }, asp)) $ number asps

1821N/A (sps', nsig1', dg1, _, _) <- foldM (anaExtension lg opts pos)

1821N/A ([], nsig, dg, conser, addSyms) namedSps

1947N/A case nsig1' of

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

1821N/A JustNode nsig1 -> return (Extension (zipWith replaceAnnoted

1821N/A (reverse sps') asps)

1947N/A pos, nsig1,dg1)

1947N/A Free_spec asp poss -> do

1947N/A (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts dg nsig name

1821N/A Free asp poss

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

1821N/A Cofree_spec asp poss -> do

1821N/A (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts dg nsig name

1821N/A Cofree asp poss

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

1821N/A Local_spec asp asp' poss -> adjustPos poss $ do

1821N/A let sp1 = item asp

1821N/A sp1' = item asp'

1821N/A lname = extName "Local" name

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

2203N/A anaSpec False lg dg nsig (extName "Spec" lname) opts sp1

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

1821N/A anaSpec False lg dg' (JustNode nsig') (extName "Within" lname) opts sp1'

1008N/A let gsigma = getMaybeSig nsig

1008N/A G_sign lid sigma _ <- return gsigma

0N/A sigma1 <- coerceSign lid' lid "Analysis of local spec" sigma'

1008N/A sigma2 <- coerceSign lid'' lid "Analysis of local spec" sigma''

1008N/A let sys = ext_sym_of lid sigma

1008N/A sys1 = ext_sym_of lid sigma1

0N/A sys2 = ext_sym_of lid sigma2

1008N/A mor3 <- if isStructured opts then return (ext_ide sigma2)

1008N/A else ext_cogenerated_sign lid

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

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

1008N/A unless (isStructured opts

1008N/A || sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3)

1008N/A $ plain_error () (

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

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

1008N/A poss

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

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

1934N/A (replaceAnnoted sp2' asp')

1934N/A poss, ns,

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

1934N/A HidingDefLink SeeTarget n'' node)

1934N/A Closed_spec asp pos -> adjustPos pos $ do

1008N/A let sp1 = item asp

1008N/A l = getLogic nsig

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

1008N/A (sp', NodeSig n' gsigma', dg') <- -- choose a unique starting letter

1821N/A anaSpec False lg dg (EmptyNode l) (extName "Closed" name) opts sp1

1821N/A let gsigma = getMaybeSig nsig

1821N/A gsigma'' <- gsigUnion lg gsigma gsigma'

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

1821N/A incl2 <- ginclusion lg gsigma' gsigma2

1821N/A let dg3 = insLink dg2 incl2 globalDef SeeTarget n' node

1821N/A dg4 <- createConsLink DefLink conser lg dg3 nsig ns DGLinkClosedLenv

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

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

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

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

1821N/A let newNSig = case nsig of

1821N/A EmptyNode _ -> EmptyNode l

1821N/A _ -> nsig

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

1821N/A anaQualSpec addSyms lg opts dg newNSig name asp pos

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

1821N/A Group asp pos -> do

1934N/A (sp', nsig', dg') <-

1821N/A anaSpecTop conser addSyms lg dg nsig name opts (item asp)

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

1821N/A Spec_inst spname afitargs pos0 -> let

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

1934N/A spstr = tokStr spname

1821N/A in adjustPos pos $ case lookupGlobalEnvDG spname dg of

1821N/A Just (SpecEntry gs@(ExtGenSig (GenSig _ params _)

1934N/A body@(NodeSig nB gsigmaB))) ->

1821N/A case (\ x y -> (x , x - y)) (length afitargs) (length params) of

1934N/A -- the case without parameters leads to a simpler dg

2500N/A (0, 0) -> case nsig of

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

1934N/A EmptyNode _ | isInternal name -> do

1934N/A dg2 <- createConsLink DefLink conser lg dg nsig body SeeTarget

2228N/A -- then just return the body

1934N/A return (sp, body, dg2)

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

1821N/A _ -> do

1821N/A gsigma <- case nsig of

1821N/A EmptyNode _ -> return gsigmaB

1821N/A JustNode (NodeSig _ sig) -> gsigUnion lg sig gsigmaB

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

1821N/A insGSig dg name (DGSpecInst spname) gsigma

1821N/A incl <- ginclusion lg gsigmaB gsigma'

1821N/A let dg3 = insLink dg2 incl globalDef SeeTarget nB node

1008N/A dg4 <- createConsLink DefLink conser lg dg3 nsig fsig SeeTarget

1008N/A return (sp, fsig, dg4)

1934N/A -- now the case with parameters

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

1934N/A (ffitargs, dg', (morDelta, gsigmaA, ns@(NodeSig nA gsigmaRes))) <-

1934N/A anaAllFitArgs lg opts dg nsig name spname gs afitargs

1821N/A GMorphism cid _ _ _ _ <- return morDelta

1821N/A morDelta' <- case nsig of

3740N/A EmptyNode _ -> return morDelta

3740N/A _ -> do

1821N/A incl2 <- ginclusion lg gsigmaA gsigmaRes

1821N/A comp morDelta incl2

3740N/A (_, imor) <- gSigCoerce lg gsigmaB $ Logic $ sourceLogic cid

3740N/A tmor <- gEmbedComorphism imor gsigmaB

1821N/A morDelta'' <- comp tmor morDelta'

1821N/A let dg4 = insLink dg' morDelta'' globalDef SeeTarget nB nA

2017N/A dg5 <- createConsLink DefLink conser lg dg4 nsig ns SeeTarget

1821N/A return (Spec_inst spname ffitargs pos, ns, dg5)

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

1821N/A _ ->

1821N/A fatal_error

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

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

1821N/A _ -> fatal_error

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

1821N/A

1821N/A -- analyse "data SPEC1 SPEC2"

1821N/A Data (Logic lidD) (Logic lidP) asp1 asp2 pos -> adjustPos pos $ do

1821N/A let sp1 = item asp1

3740N/A sp2 = item asp2

1821N/A -- look for the inclusion comorphism from the current logic's data logic

1821N/A -- into the current logic itself

1821N/A Comorphism cid <- logicInclusion lg (Logic lidD) (Logic lidP)

1821N/A let lidD' = sourceLogic cid

3740N/A lidP' = targetLogic cid

3740N/A dname = extName "Data" name

1821N/A -- analyse SPEC1

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

1821N/A anaSpec False lg dg (EmptyNode (Logic lidD)) dname opts sp1

1821N/A -- force the result to be in the data logic

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

1821N/A -- translate SPEC1's signature along the comorphism

1821N/A (sigmaD', sensD') <- ext_map_sign cid sigmaD

3740N/A -- create a development graph link for this translation

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

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

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

2017N/A (ext_ide sigmaD') startMorId)

2017N/A globalDef SeeTarget n' node

2017N/A -- analyse SPEC2

1821N/A (sp2', nsig3, dg3) <-

3740N/A anaSpec addSyms lg dg2 (JustNode nsig2) name opts sp2

1821N/A return (Data (Logic lidD) (Logic lidP)

1821N/A (replaceAnnoted sp1' asp1)

2017N/A (replaceAnnoted sp2' asp2)

1934N/A pos, nsig3, dg3)

1934N/A

1934N/AanaUnion :: Bool -> LogicGraph -> DGraph -> MaybeNode -> NodeName

1821N/A -> HetcatsOpts -> [Annoted SPEC]

1821N/A -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)

3740N/AanaUnion addSyms lg dg nsig name opts asps = case asps of

1821N/A [] -> fail "empty union"

1821N/A _ -> do

1821N/A let sps = map item asps

1821N/A (sps', nsigs, dg', _) <-

3740N/A let ana (sps1, nsigs, dg', n) sp' = do

1821N/A let n1 = inc n

1821N/A (sp1, nsig', dg1) <- anaSpec addSyms lg dg' nsig n1 opts sp'

1821N/A return (sp1 : sps1, nsig' : nsigs, dg1, n1)

1821N/A in foldM ana ([], [], dg, extName "Union" name) sps

1821N/A let newAsps = zipWith replaceAnnoted (reverse sps') asps

3740N/A case nsigs of

1821N/A [ns] -> return (newAsps, nsigs, ns, dg')

1821N/A _ -> do

1821N/A let nsigs' = reverse nsigs

1821N/A gbigSigma <- gsigManyUnion lg (map getSig nsigs')

1821N/A let (ns@(NodeSig node _), dg2) = insGSig dg' name DGUnion gbigSigma

3740N/A insE dgl (NodeSig n gsigma) = do

1821N/A incl <- ginclusion lg gsigma gbigSigma

1821N/A return $ insLink dgl incl globalDef SeeTarget n node

2017N/A dg3 <- foldM insE dg2 nsigs'

1934N/A return (newAsps, nsigs', ns, dg3)

1934N/A

1934N/AanaFitArgs :: LogicGraph -> HetcatsOpts -> SPEC_NAME -> MaybeNode

1821N/A -> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)

1821N/A -> (NodeSig, FIT_ARG)

3740N/A -> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)

1821N/AanaFitArgs lg opts spname imps (fas', dg1, args, name') (nsig', fa) = do

1821N/A let n1 = inc name'

1821N/A (fa', dg', arg) <- anaFitArg lg dg1 spname imps nsig' opts n1 fa

1821N/A return (fa' : fas', dg', arg : args, n1)

3740N/A

3740N/AparLink :: LogicGraph -> DGLinkOrigin -> NodeSig -> DGraph -> NodeSig

1821N/A -> Result DGraph

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

1821N/A incl <- ginclusion lg sigA_i gsigma'

1821N/A return $ insLink dg incl globalDef orig nA_i node

1821N/A

1821N/A-- analysis of renamings

3740N/AanaRen :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism

1821N/A -> G_mapping -> Result GMorphism

1821N/AanaRen lg opts lenv pos gmor@(GMorphism r sigma ind1 mor _) gmap =

1821N/A adjustPos pos $ case gmap of

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

3740N/A let lid2 = targetLogic r in

1821N/A if language_name lid2 == language_name lid then

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

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

1821N/A rmap <- stat_symb_map_items lid2 sis1

3740N/A mor1 <- ext_induced_from_morphism lid2 rmap $ makeExtSign lid2 $ cod mor

3740N/A case lenv of

2402N/A EmptyNode _ -> return ()

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

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

2546N/A sigmaLenv' <- coerceSign lidLenv lid2

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

3740N/A sigmaLenv -- see Calculi/Time/FlowOfTime.casl line 305

2546N/A let sysLenv = ext_sym_of lid2 sigmaLenv'

1821N/A m = symmap_of lid2 mor1

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

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

1934N/A Nothing -> False

1934N/A forbiddenSys = Set.filter isChanged sysLenv

1821N/A unless (Set.null forbiddenSys) $ plain_error () (

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

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

3740N/A mor2 <- comp mor mor1

1821N/A return $ GMorphism r sigma ind1 mor2 startMorId

1821N/A else do

1821N/A comor <- logicInclusion lg (Logic lid2) (Logic lid)

1821N/A gmorTrans <- gEmbedComorphism comor $ cod gmor

3740N/A newMor <- comp gmor gmorTrans

1821N/A anaRen lg opts lenv pos newMor gmap

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

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

1821N/A in adj1 $ do

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

3740N/A c <- case tok of

1821N/A Just ctok -> do

2017N/A let getLogicStr (Logic_name l _) = tokStr l

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

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

1821N/A language_name (sourceLogic cid))

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

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

2402N/A ++ language_name cid))

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

1821N/A language_name (targetLogic cid))

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

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

1934N/A ++ language_name cid))

1934N/A return (Comorphism cid)

1821N/A Nothing -> case tar of

1821N/A Just (Logic_name l _) ->

1821N/A lookupLogic "with logic: " (tokStr l) lg

3740N/A >>= logicInclusion lg (Logic srcLid)

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

1821N/A mor1 <- gEmbedComorphism c (G_sign srcLid srcSig ind)

1821N/A comp gmor mor1

1821N/A

3740N/AanaRenaming :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING

1821N/A -> Result GMorphism

1821N/AanaRenaming lg lenv gSigma opts (Renaming ren pos) =

2017N/A foldM (anaRen lg opts lenv pos) (ide gSigma) ren

1821N/A

3740N/A-- analysis of restrictions

1940N/AanaRestr :: G_sign -> Range -> GMorphism -> G_hiding -> Result GMorphism

2017N/AanaRestr (G_sign lidLenv sigmaLenv _) pos

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

2017N/A case gh of

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

3740N/A let lid1 = sourceLogic cid

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

3740N/A rsys <- stat_symb_items lid1 sis1

2402N/A let sys = sym_of lid1 sigma1

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

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

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

1934N/A unless (null unmatched)

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

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

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

1821N/A sigmaLenv' <- coerceSign lidLenv lid1

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

1821N/A sigmaLenv

1821N/A let sysLenv = ext_sym_of lid1 sigmaLenv'

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

1821N/A unless (Set.null forbiddenSys)

1821N/A $ plain_error () (

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

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

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

1821N/A mor1' <- map_morphism cid mor1

1821N/A mor2 <- comp mor1' mor

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

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

1821N/A Nothing -> id

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

1821N/A startSigId mor2 startMorId

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

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

1821N/A

1821N/AanaRestriction :: G_sign -> G_sign -> HetcatsOpts -> RESTRICTION

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

1821N/AanaRestriction gSigma@(G_sign lid sigma _)

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

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

2020N/A case restr of

1821N/A Hidden rstr pos -> do

1821N/A mor <- foldM (anaRestr gSigma pos) (ide gSigma') rstr

1821N/A return (mor, Nothing)

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

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

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

2020N/A in adjustPos pos $ do

2017N/A sis' <- coerceSymbMapItemsList lid1 lid'

2020N/A "Analysis of restriction" sis

2020N/A rmap <- stat_symb_map_items lid' sis'

1821N/A let sys'' =

2020N/A Set.fromList

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

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

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

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

1821N/A sys1 <- coerceSymbolSet lid lid' "Analysis of restriction" sys

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

1821N/A -- to a different logic

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

1821N/A mor2 <- ext_induced_from_morphism lid' rmap $ makeExtSign lid' $ dom mor1

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

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

1821N/A

1821N/AanaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign

1821N/A -> [G_mapping] -> Result G_morphism

1821N/AanaGmaps lg opts pos psig@(G_sign lidP sigmaP _) (G_sign lidA sigmaA _) gsis

1821N/A = adjustPos pos $ if isStructured opts

1821N/A then return $ mkG_morphism lidP $ ext_ide sigmaP

1821N/A else if null gsis then do

1821N/A sigmaA' <- coerceSign lidA lidP "anaGmaps" sigmaA

1821N/A fmap (mkG_morphism lidP) $

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

1821N/A else do

1947N/A cl <- lookupCurrentLogic "anaGmaps" lg

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

2402N/A rmap <- stat_symb_map_items lid sis

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

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

2402N/A (G_sign lidP' sigmaP'' _, _) <- gSigCoerce lg psig (Logic lid)

2402N/A sigmaP' <- coerceSign lidP' lid "anaGmaps1" sigmaP''

2402N/A sigmaA' <- coerceSign lidA lid "anaGmaps2" sigmaA

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

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

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

2402N/A $ ext_induced_from_to_morphism lid rmap sigmaP' sigmaA'

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

2402N/A {-

2402N/A let symI = sym_of lidP sigmaI'

2402N/A symmap_mor = symmap_of lidP mor

2402N/A -- are symbols of the imports left untouched?

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

2402N/A then return ()

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

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

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

1008N/A

1008N/AanaFitArg :: LogicGraph -> DGraph -> SPEC_NAME -> MaybeNode -> NodeSig

1008N/A -> HetcatsOpts -> NodeName -> FIT_ARG

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

1008N/AanaFitArg lg dg spname nsigI (NodeSig nP gsigmaP) opts name fv = case fv of

1008N/A Fit_spec asp gsis pos -> do

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

1008N/A anaSpec False lg dg nsigI name opts (item asp)

1008N/A gmor <- anaGmaps lg opts pos gsigmaP gsigA gsis

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

1008N/A insLink dg' (gEmbed gmor) globalThm

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

1008N/A Fit_view vn afitargs pos -> case lookupGlobalEnvDG vn dg of

1008N/A Just (ViewEntry (ExtViewSig (NodeSig nSrc gsigmaS) mor

1008N/A gs@(ExtGenSig (GenSig _ params _) target@(NodeSig nTar _))))

1008N/A -> adjustPos pos $ do

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

1008N/A let lid = targetLogic cid

1008N/A spstr = tokStr spname

1008N/A pname = dgn_name $ labDG dg nP

1008N/A gsigmaI = getMaybeSig nsigI

1008N/A dg5 <- do

1008N/A gsigmaIS <- gsigUnion lg gsigmaI gsigmaS

1008N/A unless (isSubGsign lg gsigmaP gsigmaIS

1008N/A && isSubGsign lg gsigmaIS gsigmaP)

1008N/A (plain_error ()

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

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

1008N/A ++ showDoc gsigmaP

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

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

1254N/A (dg4, iSrc) <- case nsigI of

2402N/A EmptyNode _ -> return (dg, nSrc)

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

1254N/A inclI <- ginclusion lg gsigmaI gsigmaIS

1254N/A inclS <- ginclusion lg gsigmaS gsigmaIS

1254N/A let (NodeSig n' _, dg1) = insGSig dg (extName "View" name)

1254N/A {xpath = xpath pname} (DGFitView spname) gsigmaIS

1254N/A dg2 = insLink dg1 inclI globalDef

1254N/A (DGLinkFitViewImp spname) nI n'

1254N/A return (insLink dg2 inclS globalDef SeeTarget nSrc n', n')

1254N/A gmor <- ginclusion lg gsigmaP gsigmaIS

1254N/A return $ insLink dg4 gmor globalThm (DGLinkFitView spname) nP iSrc

1254N/A case (\ x y -> (x, x - y)) (length afitargs) (length params) of

1254N/A -- the case without parameters leads to a simpler dg

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

1254N/A return (fv, dg5, (G_morphism lid morHom ind, target))

1254N/A -- now the case with parameters

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

1008N/A (ffitargs, dg', (gmor_f, _, ns@(NodeSig nA _))) <-

1008N/A anaAllFitArgs lg opts dg5 (EmptyNode $ Logic lid)

1008N/A name spname gs afitargs

1008N/A mor1 <- comp mor gmor_f

1008N/A GMorphism cid1 _ _ theta _ <- return mor1

1008N/A let lid1 = targetLogic cid1

1008N/A when (language_name (sourceLogic cid1) /= language_name lid1)

1008N/A $ fatal_error "heterogeneous fitting views not yet implemented"

1008N/A pos

1008N/A let dg9 = insLink dg' gmor_f globalDef SeeTarget nTar nA

1008N/A return (Fit_view vn ffitargs pos, dg9, (mkG_morphism lid1 theta, ns))

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

1008N/A _ -> fatal_error

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

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

1008N/A _ -> fatal_error ("View " ++ tokStr vn ++ " not found") pos

1008N/A

1008N/AanaAllFitArgs :: LogicGraph -> HetcatsOpts -> DGraph -> MaybeNode -> NodeName

1008N/A -> SPEC_NAME -> ExtGenSig -> [Annoted FIT_ARG]

1008N/A -> Result ([Annoted FIT_ARG], DGraph, (GMorphism, G_sign, NodeSig))

1008N/AanaAllFitArgs lg opts dg nsig name spname

1008N/A gs@(ExtGenSig (GenSig imps params _) _)

1008N/A afitargs = do

1008N/A let fitargs = map item afitargs

1008N/A (fitargs', dg', args, _) <- foldM (anaFitArgs lg opts spname imps)

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

1008N/A let actualargs = reverse args

1008N/A (gsigma', morDelta) <- applyGS lg gs actualargs

1008N/A gsigmaRes <- gsigUnion lg (getMaybeSig nsig) gsigma'

1008N/A let (ns, dg2) = insGSig dg' name (DGSpecInst spname) gsigmaRes

1008N/A dg3 <- foldM (parLink lg DGLinkFitSpec ns) dg2 $ map snd args

1008N/A return ( zipWith replaceAnnoted (reverse fitargs') afitargs, dg3

1008N/A , (morDelta, gsigma', ns))

1008N/A

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

1008N/A-- first some auxiliary functions

1008N/A

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

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

1008N/A case Map.lookup i idmap of

1008N/A Nothing -> do

1008N/A compsnew <- mapM (mapID idmap) comps

1008N/A return (Id toks compsnew pos1)

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

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

1008N/A plain_error i

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

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

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

1008N/A

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

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

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

1008N/A m1 <- m

1008N/A compsnew <- mapM (mapID idmap) comps

1008N/A return $ if comps == compsnew then m1 else

1008N/A Map.insert i (Id toks compsnew pos1) m1

1008N/A

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

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

1008N/A

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

1008N/A -> G_sign -- ^ body

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

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

1008N/A -> Result(G_sign, GMorphism)

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

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

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

1008N/A sigmaB@(ExtSign _ sysB) <-

1008N/A coerceSign lidB lid "Extension of symbol map1" sigmaB1

1008N/A sigmaA <- coerceSign lidA lid "Extension of symbol map2" sigmaA1

1008N/A fittingMor <- coerceMorphism lidM lid "Extension of symbol map3" fittingMor1

1008N/A let symsP = ext_sym_of lid sigmaP

1008N/A symsB = ext_sym_of lid sigmaB

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

1008N/A h = symmap_of lid fittingMor

1008N/A symbMapToRawSymbMap =

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

1008N/A (symbol_to_raw lid sy2))

1008N/A Map.empty

1008N/A rh = symbMapToRawSymbMap h

1008N/A idh = Map.foldWithKey

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

1008N/A Map.empty h

1008N/A idhExt <- extID idsB idh

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

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

1008N/A Map.empty

1008N/A (foldr Map.delete idhExt $ Map.keys idh)

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

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

1008N/A mor <- ext_induced_from_morphism lid r sigmaB

1008N/A let hmor = symmap_of lid mor

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

1008N/A Map.findWithDefault sy sy hmor) sysB

1008N/A sigma <- ext_signature_union lid sigmaA sigmaAD

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

1008N/A ext_sym_of lid sigmaAD )

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

1008N/A unless (Set.null illShared)

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

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

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

1008N/A let myKernel = Set.fromDistinctAscList . comb1 . Map.toList

1008N/A comb1 [] = []

1008N/A comb1 (p : qs) =

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

1008N/A comb2 _ [] rs = rs

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

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

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

1008N/A unless (Set.null newIdentifications)

1008N/A $ warning () (

1008N/A "Fitting morphism may lead to forbidden identifications:\n"

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

1008N/A incl <- ext_inclusion lid sigmaAD sigma

1008N/A mor1 <- comp mor incl

1008N/A return (G_sign lid sigma startSigId, gEmbed $ mkG_morphism lid mor1)

1008N/A

1008N/AapplyGS :: LogicGraph -> ExtGenSig -> [(G_morphism, NodeSig)]

1008N/A -> Result(G_sign, GMorphism)

1008N/AapplyGS lg (ExtGenSig (GenSig nsigI _ gsigmaP) nsigB) args = do

1008N/A let mor_i = map fst args

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

1008N/A gsigmaB = getSig nsigB

1008N/A gsigmaA@(G_sign lidA _ _) <- gsigManyUnion lg gsigmaA_i

1008N/A (_, Comorphism uid) <- logicUnion lg (getNodeLogic nsigB) (Logic lidA)

1008N/A let cl = Logic $ targetLogic uid

1008N/A G_morphism lidG mor0 _ <- case nsigI of

1008N/A EmptyNode _ -> homogeneousMorManyUnion mor_i

1008N/A JustNode (NodeSig _ gsigmaI) -> do

1008N/A (G_sign lidI sigmaI _, _) <- gSigCoerce lg gsigmaI (Logic lidA)

1008N/A let idI = ext_ide sigmaI

1008N/A homogeneousMorManyUnion $ mkG_morphism lidI idI : mor_i

1008N/A (gsigmaP', _) <- gSigCoerce lg (getMaybeSig gsigmaP) cl

1008N/A (gsigmaB', _) <- gSigCoerce lg gsigmaB cl

1008N/A (gsigmaA', Comorphism aid) <- gSigCoerce lg gsigmaA cl

1008N/A mor1 <- coerceMorphism lidG (sourceLogic aid) "applyGS" mor0

1008N/A mor2 <- map_morphism aid mor1

1008N/A extendMorphism gsigmaP' gsigmaB' gsigmaA' $

1008N/A G_morphism (targetLogic aid) mor2 startMorId

1008N/A

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

1008N/A -> Result G_symb_map_items_list

1008N/AhomogenizeGM (Logic lid) gsis =

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

1008N/A where

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

1008N/A Syntax.AS_Structured.G_symb_map (G_symb_map_items_list lid1 sis1) -> do

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

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

1008N/A _ -> return itl2

1008N/A

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

1008N/AisStructured :: HetcatsOpts -> Bool

1008N/AisStructured a = case analysis a of

1008N/A Structured -> True

1008N/A _ -> False

1008N/A

1008N/AgetSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)

1008N/AgetSpecAnnos pos a = do

1008N/A let sannos = filter isSemanticAnno $ l_annos a

1008N/A (sanno1, conflict, impliedA, impliesA) = case sannos of

1008N/A f@(Semantic_anno anno1 _) : r -> (case anno1 of

1008N/A SA_cons -> Cons

1008N/A SA_def -> Def

1008N/A SA_mono -> Mono

1008N/A _ -> None, any (/= f) r,

1008N/A anno1 == SA_implied, anno1 == SA_implies)

1008N/A _ -> (None, False, False, False)

1008N/A when conflict $ plain_error () "Conflicting semantic annotations" pos

1008N/A when impliedA $ plain_error ()

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

1008N/A return (sanno1, impliesA)

1008N/A

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

1008N/AanaExtension

1008N/A :: LogicGraph -> HetcatsOpts -> Range

1008N/A -> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)

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

1008N/A -> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)

1008N/AanaExtension lg opts pos (sps', nsig', dg', conser, addSyms) (name', asp')

1008N/A = do

1008N/A (sanno1, impliesA) <- getSpecAnnos pos asp'

1008N/A -- attach conservativity to definition link

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

1008N/A anaSpecTop (max conser sanno1) addSyms lg dg' nsig' name' opts (item asp')

1008N/A dg2 <- if impliesA then case nsig' of

1008N/A JustNode (NodeSig n' sig') -> do

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

1008N/A unless (isHomSubGsign sig1 sig') $ plain_error ()

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

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

1008N/A return $ insLink dg1 (ide sig1) globalThm DGImpliesLink n1 n'

1008N/A _ -> return dg1

1008N/A else return dg1

1008N/A return (sp1' : sps', JustNode nsig1, dg2, None, True)

1008N/A