0N/A{- |

0N/AModule : $Header$

0N/ADescription : static analysis of heterogeneous structured specifications

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

0N/ALicense : GPLv2 or higher, see LICENSE.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 ( anaSpec

0N/A , anaSpecTop

0N/A , anaUnion

0N/A , anaSublogic

0N/A , getSpecAnnos

0N/A , isStructured

0N/A , anaRenaming

0N/A , anaRestriction

0N/A , partitionGmaps

0N/A , homogenizeGM

0N/A , anaGmaps

0N/A , insGSig

0N/A , insLink

0N/A , extendMorphism

0N/A , insGTheory

0N/A , expCurie

0N/A , expandCurieByPath

0N/A , ExpOverrides

0N/A , notFoundError

0N/A , prefixErrorIRI

0N/A ) where

0N/A

0N/Aimport Driver.Options

0N/A

0N/Aimport Logic.Logic

0N/Aimport Logic.ExtSign

0N/Aimport Logic.Coerce

0N/Aimport Logic.Comorphism

0N/Aimport Logic.Grothendieck

0N/Aimport Logic.Prover

0N/A

342N/Aimport Static.DevGraph

342N/Aimport Static.DgUtils

342N/Aimport Static.GTheory

0N/A

0N/Aimport Syntax.AS_Structured

0N/Aimport Syntax.Print_AS_Structured ()

0N/A

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

0N/Aimport Common.Consistency

0N/Aimport Common.DocUtils

0N/Aimport Common.ExtSign

0N/Aimport Common.GlobalAnnotations

0N/Aimport Common.Id

0N/Aimport Common.IRI

0N/Aimport Common.LibName

0N/Aimport Common.Result

0N/Aimport Common.Utils (number)

0N/Aimport Common.Lib.MapSet (imageSet, setInsert)

0N/A

0N/Aimport Data.Graph.Inductive.Graph

0N/Aimport qualified Data.Set as Set

0N/Aimport qualified Data.Map as Map

0N/Aimport Data.Maybe

0N/Aimport Data.List

0N/Aimport Data.Function

0N/A

0N/Aimport Control.Monad

0N/Aimport Proofs.ComputeColimit (insertColimitInGraph)

0N/A

0N/A-- overrides CUIRIE expansion for Download_items

0N/Atype ExpOverrides = Map.Map IRI FilePath

0N/A

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

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

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

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

0N/A JustNode ns -> do

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

0N/A return (JustNode ms, dg2)

0N/A

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

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

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

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

342N/A else do

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

342N/A coerceNodeByComorph c dg ns nn

342N/A

342N/AcoerceNodeByComorph :: AnyComorphism -> DGraph -> NodeSig -> NodeName

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

0N/AcoerceNodeByComorph c dg (NodeSig n s) nn = do

0N/A gmor <- gEmbedComorphism c s

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

0N/A && dgl_type l == globalDef

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

0N/A Nothing -> do

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

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

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

0N/A return (ms, dg3)

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

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

0N/A

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

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

342N/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 syn 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

0N/A link = defDGLink nmor ty orig

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

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

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

0N/A

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

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

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

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

0N/A _ -> case nsig of

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

0N/A incl <- ginclusion lg sig gsig

0N/A return $ insLink dg incl

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

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

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

0N/A in if isDGRef lbl then dg else

0N/A fst $ labelNodeDG

0N/A (node, lbl

0N/A { nodeInfo =

0N/A (nodeInfo lbl)

0N/A { node_cons_status = case getNodeConsStatus lbl of

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

0N/A

0N/AgetNamedSpec :: SPEC_NAME -> LibName -> DGraph -> LibEnv

0N/A -> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))

0N/AgetNamedSpec sp ln dg libenv = case lookupGlobalEnvDG sp dg of

0N/A Just (SpecEntry s@(ExtGenSig (GenSig _ ps _) (NodeSig n _))) -> do

0N/A unless (null ps)

0N/A $ mkError "base theory must not be parameterized" sp

0N/A let t@(refLib, refDG, (_, lbl)) = lookupRefNode libenv ln dg n

0N/A refTok = getName $ dgn_name lbl

0N/A unless (sp == refTok)

0N/A $ appendDiags [mkDiag Warning "renamed base theory" sp]

0N/A if refLib == ln then return (s, t) else

0N/A case lookupGlobalEnvDG refTok refDG of

0N/A Just (SpecEntry s2) -> return (s2, t)

0N/A _ -> mkError "theory reference error" sp

0N/A _ -> mkError "unknown theory" sp

0N/A

0N/AanaSublogic :: HetcatsOpts -> LogicDescr -> LibName -> DGraph -> LibEnv

0N/A -> LogicGraph

0N/A -> Result (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)

0N/AanaSublogic _opts itm@(LogicDescr (Logic_name lt ms mt) _ _) ln dg libenv lG

0N/A = do

0N/A logN@(Logic lid) <- lookupLogic "" lt lG

0N/A mgs <- case ms of

0N/A Nothing -> return Nothing

0N/A Just subL -> do

0N/A let s = tokStr subL

0N/A case parseSublogic lid s of

0N/A Nothing -> fail $ "unknown sublogic of logic " ++ show logN

0N/A ++ ": " ++ s

0N/A Just sl ->

0N/A if sublogicName (top_sublogic lid) == s then do

0N/A warning () ("not a proper sublogic: " ++ s) $ tokPos subL

0N/A return Nothing

0N/A else return $ Just $ G_sublogics lid sl

0N/A let logicLibN = emptyLibName "Logics"

0N/A lG1 = setCurSublogic mgs $ setLogicName itm lG

0N/A case mt of

0N/A Nothing -> return (Nothing, lG1 { currentTargetBase = Nothing })

0N/A Just sp -> do

0N/A let ssp = iriToStringUnsecure sp

0N/A (s, t@(libName, _, (_, lbl))) <- case Map.lookup logicLibN libenv of

0N/A Just dg2 | logicLibN /= ln -> getNamedSpec sp logicLibN dg2 libenv

0N/A _ -> getNamedSpec sp ln dg libenv

0N/A case sublogicOfTh $ globOrLocTh lbl of

0N/A gs2@(G_sublogics lid2 _) -> do

0N/A unless (logN == Logic lid2)

0N/A $ fail $ "the logic of '" ++ ssp

0N/A ++ "' is '" ++ language_name lid2

0N/A ++ "' and not '" ++ shows logN "'!"

0N/A case mgs of

0N/A Nothing -> return ()

0N/A Just gs -> unless (isSublogic gs2 gs)

0N/A $ fail $ "theory '" ++ ssp

0N/A ++ "' has sublogic '" ++ shows gs2 "' and not '"

0N/A ++ shows gs "'!"

0N/A let sbMap = sublogicBasedTheories lG1

0N/A lMap = Map.findWithDefault Map.empty logN sbMap

0N/A nName = getDGNodeName lbl

0N/A nMap <- case Map.lookup sp lMap of

0N/A Nothing -> return $ Map.insert sp (libName, nName) lMap

0N/A Just (prevLib, prevName) -> do

0N/A unless (libName == prevLib)

0N/A $ fail $ "theory '" ++ ssp

342N/A ++ "' should come from library '"

0N/A ++ showDoc prevLib "' and not from '"

0N/A ++ showDoc libName "'!"

0N/A unless (nName == prevName)

0N/A $ fail $ "the original theory name for '" ++ ssp

0N/A ++ "' should be '"

0N/A ++ prevName ++ "' and not '"

0N/A ++ nName ++ "'!"

0N/A return lMap

0N/A return (Just (s, t), lG1

0N/A { sublogicBasedTheories = Map.insert logN nMap sbMap

0N/A , currentTargetBase = Just (libName, nName) })

0N/A

0N/AanaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph

0N/A -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC

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

0N/AanaSpecTop conser addSyms lg ln dg nsig name opts eo sp =

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

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

0N/A Basic_spec _ _ -> True

0N/A Closed_spec _ _ -> True

0N/A Spec_inst {} -> True

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

0N/A _ -> False

0N/A then anaSpecAux conser addSyms lg ln dg nsig name opts eo sp else do

0N/A let provenThmLink =

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

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

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

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

0N/A

0N/AanaFreeOrCofreeSpec :: Bool -> LogicGraph -> HetcatsOpts -> LibName -> DGraph

0N/A -> MaybeNode -> NodeName -> FreeOrCofree -> ExpOverrides -> Annoted SPEC

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

0N/AanaFreeOrCofreeSpec addSyms lg opts ln dg nsig name dglType eo asp pos =

0N/A adjustPos pos $ do

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

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

0N/A $ item asp

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

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

0N/A nsigma = case nsig of

0N/A EmptyNode cl -> emptyG_sign cl

0N/A JustNode nds -> getSig nds

0N/A incl <- ginclusion lg nsigma gsigma

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

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

0N/A SeeTarget n' node)

0N/A

0N/A{- | analyze a SPEC. The Bool Parameter determines if incoming symbols shall

0N/Abe ignored. The options are needed to check: shall only the structure be

342N/Aanalysed? -}

342N/AanaSpec :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName

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

0N/AanaSpec = anaSpecAux None

0N/A

anaSpecAux :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph

-> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC

-> Result (SPEC, NodeSig, DGraph)

anaSpecAux conser addSyms lg ln dg nsig name opts eo sp = case sp of

Basic_spec (G_basic_spec lid bspec) pos -> adjustPos pos $ do

let curLogic = Logic lid

curSL = currentSublogic lg

bsSL = G_sublogics lid $ minSublogic bspec

when (maybe False (`isProperSublogic` bsSL) curSL)

$ fail $ "sublogic expected: " ++ maybe "" show curSL

++ " found: " ++ show bsSL

(nsig', dg0) <- coerceMaybeNode lg dg nsig name curLogic

G_sign lid' sigma' _ <- return $ case nsig' of

EmptyNode cl -> emptyG_sign cl

JustNode ns -> getSig ns

ExtSign sig sys <-

coerceSign lid' lid "Analysis of basic spec" sigma'

(bspec', ExtSign sigma_complete sysd, ax) <-

if isStructured opts

then return (bspec, mkExtSign $ empty_signature lid, [])

else

let res@(Result ds mb) = extBasicAnalysis lid (getName name)

ln bspec sig $ globalAnnos dg0

in case mb of

Nothing | null ds ->

fail "basic analysis failed without giving a reason"

_ -> res

diffSig <- case signatureDiff lid sigma_complete sig of

Result _ (Just ds) -> return ds

_ -> warning sigma_complete

"signature difference could not be computed using full one" pos

let gsysd = Set.map (G_symbol lid) sysd

(ns, dg') = insGTheory dg0 name

(DGBasicSpec (Just $ G_basic_spec lid bspec')

(G_sign lid (mkExtSign diffSig) startSigId) gsysd)

$ G_theory lid (currentSyntax lg) (ExtSign sigma_complete

$ Set.intersection

(if addSyms then Set.union sys sysd else sysd)

$ symset_of lid sigma_complete)

startSigId (toThSens ax) startThId

dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension

return (Basic_spec (G_basic_spec lid bspec') pos, ns, dg'')

EmptySpec pos -> case nsig of

EmptyNode _ -> do

warning () "empty spec" pos

let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)

return (sp, ns, dg')

{- anaSpec should be changed to return a MaybeNode!

Then this duplicate dummy node could be avoided.

Also empty unions could be treated then -}

JustNode ns -> return (sp, ns , dg)

Translation asp ren ->

do let sp1 = item asp

(sp1', ns'@(NodeSig n' gsigma), dg') <-

anaSpec addSyms lg ln dg nsig (extName "Translation" name) opts eo sp1

mor <- anaRenaming lg nsig gsigma opts ren

-- ??? check that mor is identity on local env

when (isIdentity mor) $ warning ()

("nothing renamed by:\n" ++ showDoc ren "") $ getRange ren

(fs, dgf) <- if isIdentity mor && isInternal name then return (ns', dg')

else do

let (ns@(NodeSig node _), dg'') =

insGSig dg' name (DGTranslation $ Renamed ren) $ cod mor

-- ??? too simplistic for non-comorphism inter-logic translations

return (ns, insLink dg'' mor globalDef SeeTarget n' node)

return (Translation (replaceAnnoted sp1' asp) ren, fs, dgf)

Reduction asp restr ->

do let sp1 = item asp

rname = extName "Restriction" name

(sp1', ns0, dg0) <- anaSpec addSyms lg ln dg nsig rname opts eo sp1

rLid <- getRestrLogic restr

p1@(NodeSig n' gsigma', dg') <- coerceNode lg dg0 ns0 rname rLid

(hmor, tmor) <- anaRestriction lg (getMaybeSig nsig) gsigma' opts restr

let noRename = maybe True isIdentity tmor

noHide = isIdentity hmor

when noHide $ (if noRename then warning else hint) ()

("nothing hidden by:\n" ++ showDoc restr "") $ getRange restr

p2@(NodeSig node1 _, dg2) <- if noHide && isInternal name then return p1

else do

let trgSg = dom hmor

hidSyms = Set.difference (symsOfGsign gsigma')

$ symsOfGsign trgSg

orig = DGRestriction (Restricted restr) hidSyms

(ns@(NodeSig node _), dg'') = insGSig dg'

(if noRename then name else extName "Hiding" name)

orig trgSg

-- ??? too simplistic for non-comorphism inter-logic reductions

return (ns, insLink dg'' hmor HidingDefLink SeeTarget n' node)

{- we treat hiding and revealing differently

in order to keep the dg as simple as possible -}

(fs, dgf) <- case tmor of

Just tmor' | not noRename -> do

let (ns@(NodeSig node2 _), dg3) =

insGSig dg2 name DGRevealTranslation $ cod tmor'

return (ns, insLink dg3 tmor' globalDef SeeTarget node1 node2)

Nothing -> return p2

_ -> hint p2 ("nothing renamed by:\n" ++ showDoc restr "")

$ getRange restr

return (Reduction (replaceAnnoted sp1' asp) restr, fs, dgf)

Approximation _ _ -> fail "AnalysisStructured.Approximation"

Minimization asp (Mini cm cv poss) -> do

(nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig

name Minimize eo asp poss

return (Minimization nasp (Mini cm cv poss), nsig', dg')

Union asps pos -> do

(newAsps, _, ns, dg') <- adjustPos pos $ anaUnion addSyms lg ln dg nsig

name opts eo asps

return (Union newAsps pos, ns, dg')

Extension asps pos -> do

let namedSps = map (\ (asp, n) ->

let nn = incBy n (extName "Extension" name) in

if n < length asps then (nn, asp)

else (name { xpath = xpath nn }, asp)) $ number asps

(sps', nsig1', dg1, _, _) <- foldM (anaExtension lg opts eo ln pos)

([], nsig, dg, conser, addSyms) namedSps

case nsig1' of

EmptyNode _ -> fail "empty extension"

JustNode nsig1 -> return (Extension (zipWith replaceAnnoted

(reverse sps') asps)

pos, nsig1, dg1)

Free_spec asp poss -> do

(nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig

name Free eo asp poss

return (Free_spec nasp poss, nsig', dg')

Cofree_spec asp poss -> do

(nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig

name Cofree eo asp poss

return (Cofree_spec nasp poss, nsig', dg')

Minimize_spec asp poss -> do

(nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig

name Minimize eo asp poss

return (Minimize_spec nasp poss, nsig', dg')

Local_spec asp asp' poss -> adjustPos poss $ do

let sp1 = item asp

sp1' = item asp'

lname = extName "Local" name

(sp2, nsig'@(NodeSig _ gsig1), dg') <-

anaSpec False lg ln dg nsig (extName "Spec" lname) opts eo sp1

(sp2', NodeSig n'' gsig2@(G_sign lid2 sigma2 _), dg'') <- anaSpec False lg

ln dg' (JustNode nsig') (extName "Within" lname) opts eo sp1'

let gSigN = getMaybeSig nsig

(G_sign lid sigmaN _, _) <- gSigCoerce lg gSigN (Logic lid2)

sigma <- coerceSign lid lid2 "Analysis of local spec1" sigmaN

(G_sign lid' sigma' _, _) <- gSigCoerce lg gsig1 (Logic lid2)

sigma1 <- coerceSign lid' lid2 "Analysis of local spec2" sigma'

let sys = ext_sym_of lid2 sigma

sys1 = ext_sym_of lid2 sigma1

sys2 = ext_sym_of lid2 sigma2

mor3 <- if isStructured opts then return (ext_ide sigma2)

else ext_cogenerated_sign lid2

(sys1 `Set.difference` sys) sigma2

let sigma3 = dom mor3

gsigma3 = G_sign lid2 (makeExtSign lid2 sigma3) startSigId

sys3 = symset_of lid2 sigma3

unless (isStructured opts

|| sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3)

$ plain_error () (

"illegal use of locally declared symbols: "

++ showDoc ((sys2 `Set.intersection` sys1) `Set.difference` sys3) "")

poss

let hidSyms = Set.difference (symsOfGsign gsig2) $ symsOfGsign gsigma3

orig = DGRestriction NoRestriction hidSyms

(ns@(NodeSig node _), dg2) = insGSig dg'' name orig gsigma3

return (Local_spec (replaceAnnoted sp2 asp)

(replaceAnnoted sp2' asp')

poss, ns,

insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid2 mor3)

HidingDefLink SeeTarget n'' node)

Closed_spec asp pos -> adjustPos pos $ do

let sp1 = item asp

l = getLogic nsig

-- analyse spec with empty local env

(sp', NodeSig n' gsigma', dg') <- anaSpec False lg ln dg

(EmptyNode l) (extName "Closed" name) opts eo sp1

gsigma2 <- gsigUnionMaybe lg addSyms nsig gsigma'

let (ns@(NodeSig node _), dg2) = insGSig dg' name DGClosed gsigma2

incl2 <- ginclusion lg gsigma' gsigma2

let dg3 = insLink dg2 incl2 globalDef SeeTarget n' node

dg4 <- createConsLink DefLink conser lg dg3 nsig ns DGLinkClosedLenv

return (Closed_spec (replaceAnnoted sp' asp) pos, ns, dg4)

Qualified_spec lognm asp pos -> adjustPos pos $ do

let newLG = setLogicName lognm lg

l <- lookupCurrentLogic "Qualified_spec" newLG

let newNSig = case nsig of

EmptyNode _ -> EmptyNode l

_ -> nsig

qname = extName "Qualified" name

(sp', ns', dg') <- anaSpec addSyms newLG ln dg newNSig qname opts eo

$ item asp

(ns, dg2) <- coerceNode lg dg' ns' qname l

return (Qualified_spec lognm asp { item = sp' } pos, ns, dg2)

Group asp pos -> do

(sp', nsig', dg') <-

anaSpecTop conser addSyms lg ln dg nsig name opts eo (item asp)

return (Group (replaceAnnoted sp' asp) pos, nsig', dg')

Spec_inst spname' afitargs pos0 ->

case expCurie (globalAnnos dg) eo spname' of

Nothing -> prefixErrorIRI spname'

Just spname ->

let pos = if null afitargs then iriPos spname else pos0

in adjustPos pos $ case lookupGlobalEnvDG spname dg of

Just (SpecEntry gs@(ExtGenSig (GenSig _ params _)

body@(NodeSig nB gsigmaB))) ->

case (length afitargs, length params) of

-- the case without parameters leads to a simpler dg

(0, 0) -> case nsig of

-- if the node shall not be named and the logic does not change,

EmptyNode _ | isInternal name -> do

dg2 <- createConsLink DefLink conser lg dg nsig body SeeTarget

-- then just return the body

return (sp, body, dg2)

-- otherwise, we need to create a new one

_ -> do

gsigma <- gsigUnionMaybe lg addSyms nsig gsigmaB

let (fsig@(NodeSig node _), dg2) =

insGSig dg name (DGInst spname) gsigma

incl <- ginclusion lg gsigmaB gsigma

let dg3 = case nsig of

JustNode (NodeSig nI _) | nI == nB -> dg2

_ -> insLink dg2 incl globalDef (DGLinkMorph spname) nB node

dg4 <- createConsLink DefLink conser lg dg3 nsig fsig SeeTarget

return (sp, fsig, dg4)

-- now the case with parameters

(la, lp) | la == lp -> do

(ffitargs, dg', (morDelta, gsigmaA, ns@(NodeSig nA gsigmaRes))) <-

anaAllFitArgs lg opts eo ln dg nsig name spname gs afitargs

GMorphism cid _ _ _ _ <- return morDelta

morDelta' <- case nsig of

EmptyNode _

| logicOfGsign gsigmaA == logicOfGsign gsigmaRes

-> return morDelta

_ -> ginclusion lg gsigmaA gsigmaRes >>= comp morDelta

(_, imor) <- gSigCoerce lg gsigmaB $ Logic $ sourceLogic cid

tmor <- gEmbedComorphism imor gsigmaB

morDelta'' <- comp tmor morDelta'

let dg4 = case nsig of

JustNode (NodeSig nI _) | nI == nB -> dg'

_ -> insLink dg' morDelta'' globalDef (DGLinkMorph spname) nB nA

dg5 <- createConsLink DefLink conser lg dg4 nsig ns SeeTarget

return (Spec_inst spname ffitargs pos, ns, dg5)

| otherwise -> instMismatchError spname lp la pos

_ | null afitargs -> case nsig of

EmptyNode _ -> do -- copied from EmptySpec case

warning () ("ignoring missing spec " ++ showDoc spname' "") pos

let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)

return (sp, ns, dg')

JustNode ns -> return (sp, ns , dg) -- ignore

_ -> notFoundError "structured spec" spname

-- analyse "data SPEC1 SPEC2"

Data lD@(Logic lidD) lP asp1 asp2 pos -> adjustPos pos $ do

let sp1 = item asp1

sp2 = item asp2

{- look for the inclusion comorphism from the current logic's data logic

into the current logic itself -}

c <- logicInclusion lg lD lP

let dname = extName "Data" name

-- analyse SPEC1

(sp1', ns', dg') <- anaSpec False (setCurLogic (language_name lidD) lg)

ln dg (EmptyNode lD) dname opts eo sp1

-- force the result to be in the data logic

(ns'', dg'') <- coerceNode lg dg' ns' (extName "Qualified" dname) lD

-- translate SPEC1's signature along the comorphism

(nsig2@(NodeSig node gsigmaD), dg2) <-

coerceNodeByComorph c dg'' ns'' dname

(usig, udg) <- case nsig of

EmptyNode _ -> return (nsig2, dg2)

JustNode ns2 -> do

gsigma2 <- gsigUnion lg addSyms (getSig ns2) gsigmaD

let (ns@(NodeSig node2a _), dg2a) =

insGSig dg2 (extName "Union" name) DGUnion gsigma2

incl2 <- ginclusion lg gsigmaD gsigma2

let dg3 = insLink dg2a incl2 globalDef SeeTarget node node2a

dg4 <- createConsLink DefLink conser lg dg3 nsig ns SeeTarget

return (ns, dg4)

-- analyse SPEC2

(sp2', nsig3, udg3) <-

anaSpec addSyms lg ln udg (JustNode usig) name opts eo sp2

return (Data lD lP

(replaceAnnoted sp1' asp1)

(replaceAnnoted sp2' asp2)

pos, nsig3, udg3)

Combination cItems eItems pos -> adjustPos pos $ do

let getNodes (cN, cE) cItem = let

cEntry = fromMaybe (error $ "No entry for " ++ show cItem)

$ lookupGlobalEnvDG cItem dg

bgraph = dgBody dg

lEdge x y = case filter (\ (_, z, _) -> z == y) $ out bgraph x of

[] -> error "No edge found"

lE : _ -> lE

in case cEntry of

SpecEntry extGenSig -> (getNode (extGenBody extGenSig) : cN, cE)

ViewOrStructEntry True (ExtViewSig ns _gm eGS) -> let

s = getNode ns

t = getNode $ extGenBody eGS

in (cN, lEdge s t : cE)

AlignEntry asig ->

case asig of

AlignMor src _gmor tar -> let

s = getNode src

t = getNode tar

in ([s, t] ++ cN, lEdge s t : cE)

AlignSpan src _phi1 tar1 _phi2 tar2 -> let

s = getNode src

t1 = getNode tar1

t2 = getNode tar2

in ([s, t1, t2] ++ cN, [lEdge s t1, lEdge s t2] ++ cE)

_ -> error $ show cItem

++ "is not an ontology, a view or an alignment"

addGDefLinks (cN, cE) n = let

oEdges = filter (\ (_, y, l) -> elem y cN

&& isGlobalDef (dgl_type l))

$ out (dgBody dg) n

in (nub cN, nub $ oEdges ++ cE)

addLinks (cN, cE) = foldl addGDefLinks (cN, cE) cN

(cNodes, cEdges) = addLinks . foldl getNodes ([], []) $ getItems cItems

(eNodes, eEdges) = foldl getNodes ([], []) eItems

(cNodes', cEdges') = (cNodes \\ eNodes, cEdges \\ eEdges)

le = Map.insert ln dg Map.empty -- cheating!!!

(ns, dg') <- insertColimitInGraph le dg cNodes' cEdges' name

return (sp, ns, dg')

getItems :: [LABELED_ONTO_OR_INTPR_REF] -> [IRI]

getItems [] = []

getItems (Labeled _ i : r) = i : getItems r

instMismatchError :: IRI -> Int -> Int -> Range -> Result a

instMismatchError spname lp la = fatal_error $ iriToStringUnsecure spname

++ " expects " ++ show lp ++ " arguments" ++ " but was given " ++ show la

notFoundError :: String -> IRI -> Result a

notFoundError str sid = fatal_error (str ++ " '" ++ iriToStringUnsecure sid

++ "' or '" ++ iriToStringShortUnsecure sid ++ "' not found") $ iriPos sid

gsigUnionMaybe :: LogicGraph -> Bool -> MaybeNode -> G_sign -> Result G_sign

gsigUnionMaybe lg both mn gsig = case mn of

EmptyNode _ -> return gsig

JustNode ns -> gsigUnion lg both (getSig ns) gsig

anaUnion :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName

-> HetcatsOpts -> ExpOverrides -> [Annoted SPEC]

-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)

anaUnion addSyms lg ln dg nsig name opts eo asps = case asps of

[] -> fail "empty union"

_ -> do

let sps = map item asps

(sps', nsigs, dg', _) <-

let ana (sps1, nsigs, dg', n) sp' = do

let n1 = inc n

(sp1, nsig', dg1) <-

anaSpec addSyms lg ln dg' nsig n1 opts eo sp'

return (sp1 : sps1, nsig' : nsigs, dg1, n1)

in foldM ana ([], [], dg, extName "Union" name) sps

let newAsps = zipWith replaceAnnoted (reverse sps') asps

case nsigs of

[ns] -> return (newAsps, nsigs, ns, dg')

_ -> do

let nsigs' = reverse nsigs

gbigSigma <- gsigManyUnion lg (map getSig nsigs')

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

insE dgl (NodeSig n gsigma) = do

incl <- ginclusion lg gsigma gbigSigma

return $ insLink dgl incl globalDef SeeTarget n node

dg3 <- foldM insE dg2 nsigs'

return (newAsps, nsigs', ns, dg3)

-- analysis of renamings

anaRen :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism

-> G_mapping -> Result GMorphism

anaRen lg opts lenv pos gmor@(GMorphism r sigma ind1 mor _) gMapping =

adjustPos pos $ case gMapping of

G_symb_map (G_symb_map_items_list lid sis) ->

let lid2 = targetLogic r in

if language_name lid2 == language_name lid then

if isStructured opts then return gmor else do

sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis

src@(ExtSign sig _) <- return $ makeExtSign lid2 $ cod mor

rmap <- stat_symb_map_items lid2 sig Nothing sis1

mor1 <- ext_induced_from_morphism lid2 rmap src

case lenv of

EmptyNode _ -> return ()

JustNode (NodeSig _ sigLenv) -> do

-- needs to be changed for logic translations

(G_sign lid1 sigmaLenv1 _, _) <-

gSigCoerce lg sigLenv (Logic lid2)

sigmaLenv' <- coerceSign lid1 lid2 "" sigmaLenv1

let sysLenv = ext_sym_of lid2 sigmaLenv'

m = symmap_of lid2 mor1

isChanged sy = case Map.lookup sy m of

Just sy' -> sy /= sy'

Nothing -> False

forbiddenSys = Set.filter isChanged sysLenv

unless (Set.null forbiddenSys) $ plain_error () (

"attempt to rename the following symbols from " ++

"the local environment:\n" ++ showDoc forbiddenSys "") pos

mor2 <- comp mor mor1

return $ GMorphism r sigma ind1 mor2 startMorId

else do

comor <- logicInclusion lg (Logic lid2) (Logic lid)

gmorTrans <- gEmbedComorphism comor $ cod gmor

newMor <- comp gmor gmorTrans

anaRen lg opts lenv pos newMor gMapping

G_logic_translation (Logic_code tok src tar pos1) ->

let pos2 = if pos1 == nullRange then pos else pos1

adj1 = adjustPos pos2

in adj1 $ do

G_sign srcLid srcSig ind <- return (cod gmor)

c <- case tok of

Just c -> lookupComorphism c lg

Nothing -> case tar of

Just (Logic_name l _ _) ->

lookupLogic "with logic: " l lg

>>= logicInclusion lg (Logic srcLid)

Nothing -> fail "with logic: cannot determine comorphism"

checkSrcOrTarLogic pos2 True c src

checkSrcOrTarLogic pos2 False c tar

mor1 <- gEmbedComorphism c (G_sign srcLid srcSig ind)

comp gmor mor1

checkSrcOrTarLogic :: Range -> Bool -> AnyComorphism -> Maybe Logic_name

-> Result ()

checkSrcOrTarLogic pos b (Comorphism cid) ml = case ml of

Nothing -> return ()

Just (Logic_name s _ _) ->

when (s /= if b then language_name $ sourceLogic cid

else language_name $ targetLogic cid)

$ plain_error () (s ++ " is is not the "

++ (if b then "source" else "target") ++ " logic of "

++ language_name cid) pos

anaRenaming :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING

-> Result GMorphism

anaRenaming lg lenv gSigma opts (Renaming ren pos) =

foldM (anaRen lg opts lenv pos) (ide gSigma) ren

getRestrLogic :: RESTRICTION -> Result AnyLogic

getRestrLogic restr = case restr of

Revealed (G_symb_map_items_list lid _) _ -> return $ Logic lid

Hidden l _ -> case l of

[] -> error "getRestrLogic"

h : _ -> case h of

G_symb_list (G_symb_items_list lid _) -> return $ Logic lid

G_logic_projection (Logic_code _ _ _ pos1) ->

fatal_error "no analysis of logic projections yet" pos1

-- analysis of restrictions

anaRestr :: LogicGraph -> G_sign -> Range -> GMorphism -> G_hiding

-> Result GMorphism

anaRestr lg sigEnv pos (GMorphism cid (ExtSign sigma1 sys1) _ mor _) gh =

case gh of

G_symb_list (G_symb_items_list lid' sis') -> do

let lid1 = sourceLogic cid

sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction1" sis'

rsys <- stat_symb_items lid1 sigma1 sis1

let sys = symset_of lid1 sigma1

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

unmatched = filter ( \ rsy -> Set.null $ Set.filter

( \ sy -> matches lid1 sy rsy) sys') rsys

unless (null unmatched)

$ plain_error () ("attempt to hide unknown symbols:\n"

++ showDoc unmatched "") pos

-- needs to be changed when logic projections are implemented

(G_sign lidE sigmaLenv0 _, _) <- gSigCoerce lg sigEnv (Logic lid1)

sigmaLenv' <- coerceSign lidE lid1 "" sigmaLenv0

let sysLenv = ext_sym_of lid1 sigmaLenv'

forbiddenSys = sys' `Set.intersection` sysLenv

unless (Set.null forbiddenSys)

$ plain_error () (

"attempt to hide the following symbols from the local environment:\n"

++ showDoc forbiddenSys "") pos

mor1 <- cogenerated_sign lid1 sys' sigma1

mor1' <- map_morphism cid mor1

mor2 <- comp mor1' mor

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

case Map.lookup sy $ symmap_of lid1 mor1 of

Nothing -> id

Just sy1 -> Set.insert sy1) Set.empty sys1)

startSigId mor2 startMorId

G_logic_projection (Logic_code _ _ _ pos1) ->

fatal_error "no analysis of logic projections yet" pos1

anaRestriction :: LogicGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION

-> Result (GMorphism, Maybe GMorphism)

anaRestriction lg gSigma gSigma'@(G_sign lid0 sig0 _) opts restr =

if isStructured opts then return (ide gSigma, Nothing) else

case restr of

Hidden rstr pos -> do

mor <- foldM (anaRestr lg gSigma pos) (ide gSigma') rstr

return (mor, Nothing)

Revealed (G_symb_map_items_list lid1 sis) pos -> adjustPos pos $ do

(G_sign lid sigma _, _) <- gSigCoerce lg gSigma (Logic lid1)

sigma0 <- coerceSign lid lid1 "reveal1" sigma

sigma1 <- coerceSign lid0 lid1 "reveal2" sig0

let sys = ext_sym_of lid1 sigma0 -- local env

sys' = ext_sym_of lid1 sigma1 -- "big" signature

rmap <- stat_symb_map_items lid1 (plainSign sigma1) Nothing sis

let sys'' = Set.fromList

[sy | sy <- Set.toList sys', rsy <-

Map.keys rmap, matches lid1 sy rsy]

{- domain of rmap intersected with sys'

rmap is checked by ext_induced_from_morphism below -}

mor1 <- ext_generated_sign lid1 (sys `Set.union` sys'') sigma1

let extsig1 = makeExtSign lid1 $ dom mor1

mor2 <- ext_induced_from_morphism lid1 rmap extsig1

return (gEmbed2 (G_sign lid1 extsig1 startSigId)

$ G_morphism lid1 mor1 startMorId

, Just $ gEmbed $ mkG_morphism lid1 mor2)

partitionGmaps :: [G_mapping] -> ([G_mapping], [G_mapping])

partitionGmaps l = let

(hs, rs) = span (\ sm -> case sm of

G_symb_map _ -> True

G_logic_translation _ -> False) $ reverse l

in (reverse rs, reverse hs)

anaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign

-> [G_mapping] -> Result G_morphism

anaGmaps lg opts pos psig@(G_sign lidP sigmaP _) asig@(G_sign lidA sigmaA _)

gsis = adjustPos pos $ if isStructured opts

then return $ mkG_morphism lidP $ ext_ide sigmaP

else if null gsis then do

(G_sign lidP' sigmaP' _, _) <- gSigCoerce lg psig (Logic lidA)

sigmaA' <- coerceSign lidA lidP' "anaGmaps" sigmaA

fmap (mkG_morphism lidP') $

ext_induced_from_to_morphism lidP' Map.empty sigmaP' sigmaA'

else do

cl <- lookupCurrentLogic "anaGmaps" lg

G_symb_map_items_list lid sis <- homogenizeGM cl gsis

(G_sign lidP' sigmaP'' _, _) <- gSigCoerce lg psig (Logic lid)

sigmaP' <- coerceSign lidP' lid "anaGmaps1" sigmaP''

(G_sign lidA' sigmaA'' _, _) <- gSigCoerce lg asig (Logic lid)

sigmaA' <- coerceSign lidA' lid "anaGmaps2" sigmaA''

rmap <- stat_symb_map_items lid (plainSign sigmaP')

(Just $ plainSign sigmaA') sis

fmap (mkG_morphism lid)

$ ext_induced_from_to_morphism lid rmap sigmaP' sigmaA'

{-

let symI = sym_of lidP sigmaI'

symmap_mor = symmap_of lidP mor

-- are symbols of the imports left untouched?

if Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI

then return ()

else plain_error () "Fitting morphism must not affect import" pos

-- does not work

-- also output symbols that are affected

-}

anaFitArg :: LogicGraph -> LibName -> DGraph -> IRI -> MaybeNode

-> NodeSig -> HetcatsOpts -> NodeName -> ExpOverrides -> FIT_ARG

-> Result (FIT_ARG, DGraph, (G_morphism, NodeSig))

anaFitArg lg ln dg spname nsigI nsigP@(NodeSig nP gsigmaP) opts name eo fv =

let ga = globalAnnos dg in

case fv of

Fit_spec asp gsis pos -> do

(sp', nsigA, dg') <- anaSpec False lg ln dg nsigI name opts eo (item asp)

(_, Comorphism aid) <-

logicUnion lg (getNodeLogic nsigP) (getNodeLogic nsigA)

let tl = Logic $ targetLogic aid

(nsigA'@(NodeSig nA' gsigA'), dg'') <- coerceNode lg dg' nsigA name tl

(gsigmaP', pmor) <- gSigCoerce lg gsigmaP tl

tmor <- gEmbedComorphism pmor gsigmaP

gmor <- anaGmaps lg opts pos gsigmaP' gsigA' gsis

eGmor <- comp tmor $ gEmbed gmor

return ( Fit_spec (replaceAnnoted sp' asp) gsis pos

, if nP == nA' && isInclusion eGmor then dg'' else

insLink dg'' eGmor globalThm

(DGLinkInst spname $ Fitted gsis) nP nA'

, (gmor, nsigA'))

Fit_view vn' afitargs pos -> case expCurie ga eo vn' of

Nothing -> prefixErrorIRI vn'

Just vn -> case lookupGlobalEnvDG vn dg of

Just (ViewOrStructEntry _ (ExtViewSig (NodeSig nSrc gsigmaS) mor

gs@(ExtGenSig (GenSig _ params _) target@(NodeSig nTar _))))

-> adjustPos pos $ do

GMorphism cid _ _ morHom ind <- return mor

let lid = targetLogic cid

pname = dgn_name $ labDG dg nP

gsigmaI = getMaybeSig nsigI

dg5 <- do

gsigmaIS <- gsigUnionMaybe lg True nsigI gsigmaS

unless (isSubGsign lg gsigmaP gsigmaIS

&& isSubGsign lg gsigmaIS gsigmaP)

(plain_error ()

("Parameter does not match source of fittig view. "

++ "Parameter signature:\n"

++ showDoc gsigmaP

"\nSource signature of fitting view (united with import):\n"

++ showDoc gsigmaIS "") pos)

(dg4, iSrc) <- case nsigI of

EmptyNode _ -> return (dg, nSrc)

JustNode (NodeSig nI _) -> do

inclI <- ginclusion lg gsigmaI gsigmaIS

inclS <- ginclusion lg gsigmaS gsigmaIS

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

{xpath = xpath pname} (DGFitView vn) gsigmaIS

dg2 = insLink dg1 inclI globalDef

(DGLinkFitViewImp vn) nI n'

return (insLink dg2 inclS globalDef

(DGLinkFitViewImp vn) nSrc n', n')

if nP == iSrc then return dg4 else do

gmor <- ginclusion lg gsigmaP gsigmaIS

return $ insLink dg4 gmor globalThm (DGLinkFitView vn) nP iSrc

case (length afitargs, length params) of

-- the case without parameters leads to a simpler dg

(0, 0) -> return (fv, dg5, (G_morphism lid morHom ind, target))

-- now the case with parameters

(la, lp) | la == lp -> do

(ffitargs, dg', (gmor_f, _, ns@(NodeSig nA _))) <-

anaAllFitArgs lg opts eo ln dg5 (EmptyNode $ Logic lid)

name vn gs afitargs

mor1 <- comp mor gmor_f

GMorphism cid1 _ _ theta _ <- return mor1

let lid1 = targetLogic cid1

when (language_name (sourceLogic cid1) /= language_name lid1)

$ fatal_error "heterogeneous fitting views not yet implemented"

pos

let dg9 = insLink dg' gmor_f globalDef (DGLinkMorph vn) nTar nA

return (Fit_view vn ffitargs pos, dg9, (mkG_morphism lid1 theta, ns))

| otherwise -> instMismatchError spname lp la pos

_ -> notFoundError "view" vn

anaFitArgs :: LogicGraph -> HetcatsOpts -> ExpOverrides -> LibName -> IRI

-> MaybeNode

-> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)

-> (NodeSig, FIT_ARG)

-> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)

anaFitArgs lg opts eo ln spname imps (fas', dg1, args, name') (nsig', fa) = do

let n1 = inc name'

(fa', dg', arg) <- anaFitArg lg ln dg1 spname imps nsig' opts n1 eo fa

return (fa' : fas', dg', arg : args, n1)

anaAllFitArgs :: LogicGraph -> HetcatsOpts -> ExpOverrides -> LibName -> DGraph

-> MaybeNode

-> NodeName -> IRI -> ExtGenSig -> [Annoted FIT_ARG]

-> Result ([Annoted FIT_ARG], DGraph, (GMorphism, G_sign, NodeSig))

anaAllFitArgs lg opts eo ln dg nsig name spname

gs@(ExtGenSig (GenSig imps params _) _)

afitargs = do

let fitargs = map item afitargs

(fitargs', dg', args, _) <- foldM (anaFitArgs lg opts eo ln spname imps)

([], dg, [], extName "Actuals" name) (zip params fitargs)

let actualargs = reverse args

(gsigma', morDelta) <- applyGS lg gs actualargs

gsigmaRes <- gsigUnionMaybe lg True nsig gsigma'

let (ns, dg2) = insGSig dg' name (DGInst spname) gsigmaRes

dg3 <- foldM (parLink lg nsig (DGLinkInstArg spname) ns) dg2

$ map snd actualargs

return ( zipWith replaceAnnoted (reverse fitargs') afitargs, dg3

, (morDelta, gsigma', ns))

parLink :: LogicGraph -> MaybeNode -> DGLinkOrigin -> NodeSig -> DGraph

-> NodeSig -> Result DGraph

parLink lg nsig orig (NodeSig node gsigma') dg (NodeSig nA_i sigA_i) =

case nsig of

JustNode (NodeSig nI _) | nI == nA_i -> return dg

-- actual parameter will be included via import

_ -> do

incl <- ginclusion lg sigA_i gsigma'

return $ insLink dg incl globalDef orig nA_i node

{- Extension of signature morphisms (for instantitations)

first some auxiliary functions -}

mapID :: Map.Map Id (Set.Set Id) -> Id -> Result Id

mapID idmap i@(Id toks comps pos1) =

case Map.lookup i idmap of

Nothing -> do

compsnew <- mapM (mapID idmap) comps

return (Id toks compsnew pos1)

Just ids -> case Set.toList ids of

[] -> return i

[h] -> return h

_ -> plain_error i

("Identifier component " ++ showId i

" can be mapped in various ways:\n"

++ showDoc ids "") $ getRange i

extID1 :: Map.Map Id (Set.Set Id) -> Id

-> Result (EndoMap Id) -> Result (EndoMap Id)

extID1 idmap i@(Id toks comps pos1) m = do

m1 <- m

compsnew <- mapM (mapID idmap) comps

return $ if comps == compsnew then m1 else

Map.insert i (Id toks compsnew pos1) m1

extID :: Set.Set Id -> Map.Map Id (Set.Set Id) -> Result (EndoMap Id)

extID ids idmap = Set.fold (extID1 idmap) (return Map.empty) ids

extendMorphism :: Bool -- ^ check sharing (False for lambda expressions)

-> G_sign -- ^ formal parameter

-> G_sign -- ^ body

-> G_sign -- ^ actual parameter

-> G_morphism -- ^ fitting morphism

-> Result (G_sign, G_morphism)

extendMorphism sharing (G_sign lid sigmaP _) (G_sign lidB sigmaB1 _)

(G_sign lidA sigmaA1 _) (G_morphism lidM fittingMor1 _) = do

-- for now, only homogeneous instantiations....

sigmaB@(ExtSign _ sysB) <-

coerceSign lidB lid "Extension of symbol map1" sigmaB1

sigmaA <- coerceSign lidA lid "Extension of symbol map2" sigmaA1

fittingMor <- coerceMorphism lidM lid "Extension of symbol map3" fittingMor1

let symsP = ext_sym_of lid sigmaP

symsB = ext_sym_of lid sigmaB

idsB = Set.map (sym_name lid) symsB

h = symmap_of lid fittingMor

symbMapToRawSymbMap = Map.foldWithKey

(on Map.insert $ symbol_to_raw lid) Map.empty

rh = symbMapToRawSymbMap h

idh = Map.foldWithKey (on setInsert $ sym_name lid) Map.empty h

idhExt <- extID idsB idh

let rIdExt = Map.foldWithKey (on Map.insert $ id_to_raw lid) Map.empty

(foldr Map.delete idhExt $ Map.keys idh)

r = rh `Map.union` rIdExt

-- do we need combining function catching the clashes???

mor <- ext_induced_from_morphism lid r sigmaB

let hmor = symmap_of lid mor

sigmaAD = ExtSign (cod mor) $ Set.map (\ sy ->

Map.findWithDefault sy sy hmor) sysB

sigma <- ext_signature_union lid sigmaA sigmaAD

let illShared = (ext_sym_of lid sigmaA `Set.intersection`

ext_sym_of lid sigmaAD )

Set.\\ imageSet h symsP

unless (Set.null illShared || not sharing)

$ plain_error () ("Symbols shared between actual parameter and body"

++ "\nmust be in formal parameter:\n"

++ showDoc illShared "") nullRange

let myKernel = Set.fromDistinctAscList . comb1 . Map.toList

comb1 [] = []

comb1 (p : qs) =

comb2 p qs [] ++ comb1 qs

comb2 _ [] rs = rs

comb2 p@(a, b) ((c, d) : qs) rs =

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

newIdentifications = myKernel hmor Set.\\ myKernel h

unless (Set.null newIdentifications)

$ warning () (

"Fitting morphism may lead to forbidden identifications:\n"

++ showDoc newIdentifications "") nullRange

incl <- ext_inclusion lid sigmaAD sigma

mor1 <- comp mor incl

return (G_sign lid sigma startSigId, mkG_morphism lid mor1)

applyGS :: LogicGraph -> ExtGenSig -> [(G_morphism, NodeSig)]

-> Result (G_sign, GMorphism)

applyGS lg (ExtGenSig (GenSig nsigI _ gsigmaP) nsigB) args = do

let mor_i = map fst args

gsigmaA_i = map (getSig . snd) args

gsigmaB = getSig nsigB

gsigmaA@(G_sign lidA _ _) <- gsigManyUnion lg gsigmaA_i

(Comorphism bid, Comorphism uid) <-

logicUnion lg (getNodeLogic nsigB) (Logic lidA)

let cl = Logic $ targetLogic uid

G_morphism lidG mor0 _ <- case nsigI of

EmptyNode _ -> homogeneousMorManyUnion mor_i

JustNode (NodeSig _ gsigmaI) -> do

(G_sign lidI sigmaI _, _) <- gSigCoerce lg gsigmaI (Logic lidA)

let idI = ext_ide sigmaI

homogeneousMorManyUnion $ mkG_morphism lidI idI : mor_i

(gsigmaP', _) <- gSigCoerce lg (getMaybeSig gsigmaP) cl

(gsigmaB', _) <- gSigCoerce lg gsigmaB cl

(gsigmaA', Comorphism aid) <- gSigCoerce lg gsigmaA cl

mor1 <- coerceMorphism lidG (sourceLogic aid) "applyGS" mor0

mor2 <- map_morphism aid mor1

(gsig, G_morphism gid mor3 mId) <- extendMorphism True gsigmaP' gsigmaB'

gsigmaA' $ G_morphism (targetLogic aid) mor2 startMorId

case gsigmaB of

G_sign lidB sigB indB -> do

sigB' <- coerceSign lidB (sourceLogic bid) "applyGS2" sigB

mor4 <- coerceMorphism gid (targetLogic bid) "applyGS3" mor3

return (gsig, GMorphism bid sigB' indB mor4 mId)

homogenizeGM :: AnyLogic -> [G_mapping] -> Result G_symb_map_items_list

homogenizeGM (Logic lid) =

foldM homogenize1 (G_symb_map_items_list lid [])

where

homogenize1 (G_symb_map_items_list lid2 sis) sm = case sm of

G_symb_map (G_symb_map_items_list lid1 sis1) -> do

sis1' <- coerceSymbMapItemsList lid1 lid2 "homogenizeGM" sis1

return $ G_symb_map_items_list lid2 $ sis ++ sis1'

G_logic_translation lc ->

fail $ "translation not supported by " ++ showDoc lc ""

-- | check if structured analysis should be performed

isStructured :: HetcatsOpts -> Bool

isStructured a = case analysis a of

Structured -> True

_ -> False

getSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)

getSpecAnnos pos a = do

let sannos = filter isSemanticAnno $ l_annos a

(sanno1, conflict, impliesA) = case sannos of

f@(Semantic_anno anno1 _) : r -> (case anno1 of

SA_cons -> Cons

SA_def -> Def

SA_mono -> Mono

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

anno1 == SA_implies || anno1 == SA_implied)

_ -> (None, False, False)

when conflict $ plain_error () "Conflicting semantic annotations" pos

return (sanno1, impliesA)

-- only consider addSyms for the first spec

anaExtension :: LogicGraph -> HetcatsOpts -> ExpOverrides -> LibName -> Range

-> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)

-> (NodeName, Annoted SPEC)

-> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)

anaExtension lg opts eo ln pos (sps', nsig', dg', conser, addSyms) (name', asp')

= do

(sanno1, impliesA) <- getSpecAnnos pos asp'

-- attach conservativity to definition link

(sp1', nsig1@(NodeSig n1 sig1), dg1) <- anaSpecTop (max conser sanno1)

addSyms lg ln dg' nsig' name' opts eo (item asp')

dg2 <- if impliesA then case nsig' of

JustNode (NodeSig n' sig') -> do

-- is the extension going between real nodes?

unless (isHomSubGsign sig1 sig') $ plain_error ()

"Signature must not be extended in presence of %implies" pos

-- insert a theorem link according to p. 319 of the CASL Reference Manual

return $ insLink dg1 (ide sig1) globalThm DGImpliesLink n1 n'

_ -> return dg1

else return dg1

return (sp1' : sps', JustNode nsig1, dg2, None, True)

-- BEGIN CURIE expansion

expCurie :: GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI

expCurie ga eo i =

let pm = prefix_map ga

in case Map.lookup i eo of

Nothing -> expandCurie pm i

Just path -> expandCurieByPath path i

expandCurieByPath :: FilePath -> IRI -> Maybe IRI

expandCurieByPath path i = case parseIRIReference $ path ++ "?" of

Nothing -> Nothing

Just p -> expandCurie (Map.singleton "" p) i

prefixErrorIRI :: IRI -> Result a

prefixErrorIRI i = fatal_error ("No prefix found for CURIE " ++

iriToStringUnsecure i ++ " or expansion does not yield a valid IRI.")

$ iriPos i

-- END CURIE expansion