0N/ADescription : static analysis of heterogeneous structured specifications
0N/ACopyright : (c) Till Mossakowski and Uni Bremen 2003-2006
0N/AMaintainer : till@informatik.uni-bremen.de
0N/AStability : provisional
0N/AStatic analysis of CASL (heterogeneous) structured specifications
0N/A Follows the verfication semantic rules in Chap. IV:4.7
0N/A of the CASL Reference Manual.
0N/A-- overrides CUIRIE expansion for Download_items
0N/AcoerceMaybeNode :: LogicGraph -> DGraph -> MaybeNode -> NodeName -> AnyLogic
0N/A -> Result (MaybeNode, DGraph)
0N/AcoerceMaybeNode lg dg mn nn l2 = case mn of
0N/A EmptyNode _ -> return (EmptyNode l2, dg)
0N/A (ms, dg2) <- coerceNode lg dg ns nn l2
0N/A return (JustNode ms, dg2)
0N/AcoerceNode :: LogicGraph -> DGraph -> NodeSig -> NodeName -> AnyLogic
0N/A -> Result (NodeSig, DGraph)
0N/AcoerceNode lg dg ns@(NodeSig _ (G_sign lid1 _ _)) nn l2@(Logic lid2) =
0N/A if language_name lid1 == language_name lid2 then return (ns, dg)
0N/A c <- logicInclusion lg (Logic lid1) l2
0N/A coerceNodeByComorph c dg ns nn
0N/AcoerceNodeByComorph :: AnyComorphism -> DGraph -> NodeSig -> NodeName
0N/A -> Result (NodeSig, DGraph)
642N/AcoerceNodeByComorph c dg (NodeSig n s) nn = do
642N/A gmor <- gEmbedComorphism c s
642N/A case find (\ (_, _, l) -> dgl_origin l == SeeTarget
642N/A && dgl_type l == globalDef
642N/A && dgl_morphism l == gmor) $ outDG dg n of
642N/A let (ms@(NodeSig m _), dg2) =
642N/A insGSig dg (extName "XCoerced" nn) DGLogicCoercion $ cod gmor
642N/A dg3 = insLink dg2 gmor globalDef SeeTarget n m
642N/A return (NodeSig t $ signOf $ dgn_theory $ labDG dg t, dg)
0N/AinsGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
0N/AinsGTheory dg name orig (G_theory lid syn sig ind sens tind) =
481N/A let (sgMap, s) = sigMapI dg
0N/A (tMap, t) = thMapI dg
0N/A nind = if ind == startSigId then succ s else ind
0N/A ntind = if tb then succ t else tind
0N/A nsig = G_sign lid sig nind
0N/A nth = G_theory lid 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 ind == startSigId
0N/A $ insNodeDG (node, node_contents) dg)
0N/AinsGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
0N/AinsGSig dg name orig (G_sign lid sig ind) =
0N/A insGTheory dg name orig $ noSensGTheory lid sig ind
0N/AinsLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node
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 (toG_morphism nmor) mrMap else id) $
0N/A (G_sign (sourceLogic cid) sign nsi) sgMap else id)
0N/A $ insLEdgeNubDG (n, t, link) dg
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 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 { node_cons_status = case getNodeConsStatus lbl of
0N/A ConsStatus c d th -> ConsStatus (max c conser) d th }}) dg
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 $ 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]
1080N/A if refLib == ln then return (s, t) else
1080N/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/AanaSublogic :: HetcatsOpts -> LogicDescr -> LibName -> DGraph -> LibEnv
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 logN@(Logic lid) <- lookupLogic "" lt lG
0N/A Nothing -> return Nothing
0N/A case parseSublogic lid s of
0N/A Nothing -> fail $ "unknown sublogic of logic " ++ show logN
0N/A if sublogicName (top_sublogic lid) == s then do
0N/A warning () ("not a proper sublogic: " ++ s) $ tokPos subL
0N/A else return $ Just $ G_sublogics lid sl
0N/A let logicLibN = emptyLibName "Logics"
642N/A lG1 = setCurSublogic mgs $ setLogicName itm lG
642N/A Nothing -> return (Nothing, lG1 { currentTargetBase = Nothing })
0N/A let ssp = iriToStringUnsecure sp
0N/A (s, t@(libName, _, (_, lbl))) <- case
Map.lookup logicLibN libenv of
113N/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 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 let sbMap = sublogicBasedTheories lG1
0N/A nName = getDGNodeName lbl
0N/A Just (prevLib, prevName) -> do
0N/A unless (libName == prevLib)
0N/A $ fail $ "theory '" ++ ssp
0N/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 ++ prevName ++ "' and not '"
0N/A return (Just (s, t), lG1
0N/A , currentTargetBase = Just (libName, nName) })
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 then anaSpecAux conser addSyms lg ln dg nsig name opts eo sp else do
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/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 (sp', NodeSig n' gsigma, dg') <-
0N/A anaSpec addSyms lg ln dg nsig (extName (show dglType) name) opts eo
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{- | 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
0N/AanaSpec :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName
0N/A -> HetcatsOpts -> ExpOverrides -> SPEC -> Result (SPEC, NodeSig, DGraph)
0N/AanaSpec = anaSpecAux None
2062N/AanaSpecAux :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph
2062N/A -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC
0N/A -> Result (SPEC, NodeSig, DGraph)
0N/AanaSpecAux conser addSyms lg ln dg nsig name opts eo sp = case sp of
0N/A Basic_spec (G_basic_spec lid bspec) pos -> adjustPos pos $ do
0N/A let curLogic = Logic lid
0N/A curSL = currentSublogic lg
0N/A bsSL = G_sublogics lid $ minSublogic bspec
0N/A when (maybe False (`isProperSublogic` bsSL) curSL)
0N/A $ fail $ "sublogic expected: " ++ maybe "" show curSL
0N/A ++ " found: " ++ show bsSL
0N/A (nsig', dg0) <- coerceMaybeNode lg dg nsig name curLogic
0N/A G_sign lid' sigma' _ <- return $ case nsig' of
0N/A EmptyNode cl -> emptyG_sign cl
0N/A JustNode ns -> getSig ns
0N/A coerceSign lid' lid "Analysis of basic spec" sigma'
0N/A (bspec', ExtSign sigma_complete sysd, ax) <-
0N/A if isStructured opts
0N/A then return (bspec, mkExtSign $ empty_signature lid, [])
0N/A let res@(Result ds mb) = extBasicAnalysis lid (getName name)
0N/A ln bspec sig $ globalAnnos dg0
0N/A Nothing | null ds ->
0N/A fail "basic analysis failed without giving a reason"
0N/A diffSig <- case signatureDiff lid sigma_complete sig of
0N/A Result _ (Just ds) -> return ds
0N/A _ -> warning sigma_complete
1080N/A "signature difference could not be computed using full one" pos
0N/A (ns, dg') = insGTheory dg0 name
0N/A (DGBasicSpec (Just $ G_basic_spec lid bspec')
0N/A (G_sign lid (mkExtSign diffSig) startSigId) gsysd)
0N/A $ G_theory lid (currentSyntax lg) (ExtSign sigma_complete
0N/A $ symset_of lid sigma_complete)
0N/A startSigId (toThSens ax) startThId
0N/A dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension
0N/A return (Basic_spec (G_basic_spec lid bspec') pos, ns, dg'')
0N/A EmptySpec pos -> case nsig of
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 {- anaSpec 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', ns'@(NodeSig n' gsigma), dg') <-
0N/A anaSpec addSyms lg ln dg nsig (extName "Translation" name) opts eo sp1
0N/A mor <- anaRenaming lg nsig gsigma opts ren
0N/A -- ??? check that mor is identity on local env
1833N/A when (isIdentity mor) $ warning ()
0N/A ("nothing renamed by:\n" ++ showDoc ren "") $ getRange ren
0N/A (fs, dgf) <- if isIdentity mor && isInternal name then return (ns', dg')
0N/A let (ns@(NodeSig node _), dg'') =
113N/A insGSig dg' name (DGTranslation $ Renamed ren) $ cod mor
642N/A -- ??? too simplistic for non-comorphism inter-logic translations
642N/A return (ns, insLink dg'' mor globalDef SeeTarget n' node)
858N/A return (Translation (replaceAnnoted sp1' asp) ren, fs, dgf)
642N/A rname = extName "Restriction" name
642N/A (sp1', ns0, dg0) <- anaSpec addSyms lg ln dg nsig rname opts eo sp1
642N/A rLid <- getRestrLogic restr
642N/A p1@(NodeSig n' gsigma', dg') <- coerceNode lg dg0 ns0 rname rLid
642N/A (hmor, tmor) <- anaRestriction lg (getMaybeSig nsig) gsigma' opts restr
642N/A let noRename = maybe True isIdentity tmor
642N/A noHide = isIdentity hmor
642N/A when noHide $ (if noRename then warning else hint) ()
642N/A ("nothing hidden by:\n" ++ showDoc restr "") $ getRange restr
642N/A p2@(NodeSig node1 _, dg2) <- if noHide && isInternal name then return p1
642N/A orig = DGRestriction (Restricted restr) hidSyms
113N/A (ns@(NodeSig node _), dg'') = insGSig dg'
0N/A (if noRename then name else extName "Hiding" name)
0N/A -- ??? too simplistic for non-comorphism inter-logic reductions
0N/A return (ns, insLink dg'' hmor HidingDefLink SeeTarget n' node)
0N/A {- we treat hiding and revealing differently
0N/A in order to keep the dg as simple as possible -}
0N/A (fs, dgf) <- case tmor of
0N/A Just tmor' | not noRename -> do
0N/A let (ns@(NodeSig node2 _), dg3) =
0N/A insGSig dg2 name DGRevealTranslation $ cod tmor'
0N/A return (ns, insLink dg3 tmor' globalDef SeeTarget node1 node2)
0N/A Nothing -> return p2
0N/A _ -> hint p2 ("nothing renamed by:\n" ++ showDoc restr "")
0N/A return (Reduction (replaceAnnoted sp1' asp) restr, fs, dgf)
0N/A Minimization asp (Mini cm cv poss) -> do
0N/A (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig
0N/A name Minimize eo asp poss
0N/A return (Minimization nasp (Mini cm cv poss), nsig', dg')
0N/A Union asps pos -> do
0N/A (newAsps, _, ns, dg') <- adjustPos pos $ anaUnion addSyms lg ln dg nsig
0N/A return (Union newAsps pos, ns, dg')
0N/A Extension asps pos -> do
0N/A let namedSps = map (\ (asp, n) ->
0N/A let nn = incBy n (extName "Extension" name) in
0N/A if n < length asps then (nn, asp)
0N/A else (name { xpath = xpath nn }, asp)) $ number asps
0N/A (sps', nsig1', dg1, _, _) <- foldM (anaExtension lg opts eo ln pos)
0N/A ([], nsig, dg, conser, addSyms) namedSps
0N/A EmptyNode _ -> fail "empty extension"
0N/A JustNode nsig1 -> return (Extension (zipWith replaceAnnoted
0N/A (reverse sps') asps)
0N/A Free_spec asp poss -> do
845N/A (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig
0N/A name Free eo asp poss
0N/A return (Free_spec nasp poss, nsig', dg')
0N/A Cofree_spec asp poss -> do
0N/A (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig
0N/A name Cofree eo asp poss
0N/A return (Cofree_spec nasp poss, nsig', dg')
0N/A Minimize_spec asp poss -> do
0N/A (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig
0N/A name Minimize eo asp poss
0N/A return (Minimize_spec nasp poss, nsig', dg')
0N/A Local_spec asp asp' poss -> adjustPos poss $ do
0N/A lname = extName "Local" name
0N/A (sp2, nsig'@(NodeSig _ gsig1), dg') <-
0N/A anaSpec False lg ln dg nsig (extName "Spec" lname) opts eo sp1
0N/A (sp2', NodeSig n'' gsig2@(G_sign lid2 sigma2 _), dg'') <- anaSpec False lg
0N/A ln dg' (JustNode nsig') (extName "Within" lname) opts eo sp1'
0N/A let gSigN = getMaybeSig nsig
0N/A (G_sign lid sigmaN _, _) <- gSigCoerce lg gSigN (Logic lid2)
0N/A sigma <- coerceSign lid lid2 "Analysis of local spec1" sigmaN
0N/A (G_sign lid' sigma' _, _) <- gSigCoerce lg gsig1 (Logic lid2)
0N/A sigma1 <- coerceSign lid' lid2 "Analysis of local spec2" sigma'
0N/A let sys = ext_sym_of lid2 sigma
0N/A sys1 = ext_sym_of lid2 sigma1
0N/A sys2 = ext_sym_of lid2 sigma2
0N/A mor3 <- if isStructured opts then return (ext_ide sigma2)
0N/A else ext_cogenerated_sign lid2
0N/A let sigma3 = dom mor3
0N/A gsigma3 = G_sign lid2 (makeExtSign lid2 sigma3) startSigId
0N/A sys3 = symset_of lid2 sigma3
0N/A unless (isStructured opts
0N/A "illegal use of locally declared symbols: "
0N/A orig = DGRestriction NoRestriction hidSyms
0N/A (ns@(NodeSig node _), dg2) = insGSig dg'' name orig gsigma3
0N/A return (Local_spec (replaceAnnoted sp2 asp)
0N/A (replaceAnnoted sp2' asp')
0N/A insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid2 mor3)
0N/A HidingDefLink SeeTarget n'' node)
0N/A Closed_spec asp pos -> adjustPos pos $ do
0N/A -- analyse spec with empty local env
0N/A (sp', NodeSig n' gsigma', dg') <- anaSpec False lg ln dg
0N/A (EmptyNode l) (extName "Closed" name) opts eo sp1
0N/A gsigma2 <- gsigUnionMaybe lg addSyms nsig gsigma'
0N/A let (ns@(NodeSig node _), dg2) = insGSig dg' name DGClosed gsigma2
0N/A incl2 <- ginclusion lg gsigma' gsigma2
0N/A let dg3 = insLink dg2 incl2 globalDef SeeTarget n' node
1879N/A dg4 <- createConsLink DefLink conser lg dg3 nsig ns DGLinkClosedLenv
1879N/A 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
qname = extName "Qualified" name
(sp', ns', dg') <- anaSpec addSyms newLG ln dg newNSig qname opts eo
(ns, dg2) <- coerceNode lg dg' ns' qname l
return (Qualified_spec lognm asp { item = sp' } pos, ns, dg2)
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'
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
-- 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
-- otherwise, we need to create a new one
gsigma <- gsigUnionMaybe lg addSyms nsig gsigmaB
let (fsig@(NodeSig node _), dg2) =
insGSig dg name (DGInst spname) gsigma
incl <- ginclusion lg gsigmaB gsigma
JustNode (NodeSig nI _) | nI == nB -> dg2
_ -> insLink dg2 incl globalDef (DGLinkMorph spname) nB node
dg4 <- createConsLink DefLink conser lg dg3 nsig fsig SeeTarget
-- 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
| logicOfGsign gsigmaA == logicOfGsign gsigmaRes
_ -> ginclusion lg gsigmaA gsigmaRes >>= comp morDelta
(_, imor) <- gSigCoerce lg gsigmaB $ Logic $ sourceLogic cid
tmor <- gEmbedComorphism imor gsigmaB
morDelta'' <- comp tmor morDelta'
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
warning () ("ignoring missing spec " ++ showDoc spname' "") pos
EmptyNode _ -> do -- copied from EmptySpec case
let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)
JustNode ns -> return (sp, ns , dg)
_ -> notFoundError "structured spec" spname
-- analyse "data SPEC1 SPEC2"
Data lD@(Logic lidD) lP asp1 asp2 pos -> adjustPos pos $ do
{- 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
(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)
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
anaSpec addSyms lg ln udg (JustNode usig) name opts eo sp2
(replaceAnnoted sp1' asp1)
(replaceAnnoted sp2' asp2)
Combination cItems eItems pos -> adjustPos pos $ do
let getNodes (cN, cE) cItem = let
cEntry = fromMaybe (error $ "No entry for " ++ show cItem)
$ lookupGlobalEnvDG cItem dg
lEdge x y = case filter (\ (_, z, _) -> z == y) $ out bgraph x of
[] -> error "No edge found"
SpecEntry extGenSig -> let
n = getNode $ extGenBody extGenSig
in if elem n cN then (cN, cE) else (n : cN, cE)
ViewOrStructEntry True (ExtViewSig ns _gm eGS) -> let
t = getNode $ extGenBody eGS
in (nub $ s : t : cN, lEdge s t : cE)
AlignMor src _gmor tar -> let
in (nub $ s : t : cN, lEdge s t : cE)
AlignSpan src _phi1 tar1 _phi2 tar2 -> let
in (nub $ [s, t1, t2] ++ cN, [lEdge s t1, lEdge s t2] ++ cE)
++ "is not an ontology, a view or an alignment"
addGDefLinks (cN, iN, cE) n = let
allGDef = all $ \ (_, _, l) -> isGlobalDef $ dgl_type l
gDefPaths x y = filter allGDef $ getPathsTo x y g
nPaths = concat $ concatMap (gDefPaths n) cN
nNodes = concatMap (\ (x, y, _) -> [x, y]) nPaths
in (cN, nub $ iN ++ nNodes, nub $ nPaths ++ cE)
addLinks (cN, cE) = foldl addGDefLinks (cN, [], cE) cN
(cNodes, iNodes, cEdges) =
addLinks . foldl getNodes ([], []) $ getItems cItems
(eNodes, eEdges) = foldl getNodes ([], []) eItems
(cNodes', cEdges') = (nub (cNodes ++ iNodes) \\ eNodes,
(ns, dg') <- insertColimitInGraph le dg cNodes' cEdges' name
getItems :: [LABELED_ONTO_OR_INTPR_REF] -> [IRI]
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
let ana (sps1, nsigs, dg', n) sp' = do
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
[ns] -> return (newAsps, nsigs, ns, dg')
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)
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
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'
unless (
Set.null forbiddenSys) $ plain_error () (
"attempt to rename the following symbols from " ++
"the local environment:\n" ++ showDoc forbiddenSys "") pos
return $ GMorphism r sigma ind1 mor2 startMorId
comor <- logicInclusion lg (Logic lid2) (Logic lid)
gmorTrans <- gEmbedComorphism comor $ cod gmor
newMor <- comp gmor gmorTrans
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
G_sign srcLid srcSig ind <- return (cod gmor)
Just c -> lookupComorphism c lg
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)
checkSrcOrTarLogic :: Range -> Bool -> AnyComorphism -> Maybe Logic_name
checkSrcOrTarLogic pos b (Comorphism cid) ml = case ml of
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
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
[] -> error "getRestrLogic"
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
anaRestr lg sigEnv pos (GMorphism cid (ExtSign sigma1 sys1) _ mor _) gh =
G_symb_list (G_symb_items_list lid' sis') -> do
let lid1 = sourceLogic cid
sis1 <- coerceSymbItemsList lid' lid1 "Analysis of 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
( \ sy -> matches lid1 sy rsy) sys') rsys
$ 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'
"attempt to hide the following symbols from the local environment:\n"
++ showDoc forbiddenSys "") pos
mor1 <- cogenerated_sign lid1 sys' sigma1
mor1' <- map_morphism cid mor1
return $ GMorphism cid (ExtSign (dom mor1) $
Set.fold (\ sy ->
startSigId mor2 startMorId
G_logic_projection (Logic_code _ _ _ 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
mor <- foldM (anaRestr lg gSigma pos) (ide gSigma') rstr
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
{- 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])
(hs, rs) = span (\ sm -> case sm of
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'
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
$ 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
else plain_error () "Fitting morphism must not affect import" pos
-- 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
Fit_spec asp gsis pos -> do
(sp', nsigA, dg') <- anaSpec False lg ln dg nsigI name opts eo (item asp)
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'
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 _))))
GMorphism cid _ _ morHom ind <- return mor
let lid = targetLogic cid
pname = dgn_name $ labDG dg nP
gsigmaI = getMaybeSig nsigI
gsigmaIS <- gsigUnionMaybe lg True nsigI gsigmaS
unless (isSubGsign lg gsigmaP gsigmaIS
&& isSubGsign lg gsigmaIS gsigmaP)
("Parameter does not match source of fittig view. "
++ "Parameter signature:\n"
"\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)
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"
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
-> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)
-> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)
anaFitArgs lg opts eo ln spname imps (fas', dg1, args, name') (nsig', fa) = do
(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
-> 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 _) _)
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
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) =
JustNode (NodeSig nI _) | nI == nA_i -> return dg
-- actual parameter will be included via import
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 idmap i@(Id toks comps pos1) =
compsnew <- mapM (mapID idmap) comps
return (Id toks compsnew pos1)
("Identifier component " ++ showId i
" can be mapped in various ways:\n"
++ showDoc ids "") $ getRange i
-> Result (EndoMap Id) -> Result (EndoMap Id)
extID1 idmap i@(Id toks comps pos1) m = do
compsnew <- mapM (mapID idmap) comps
return $ if comps == compsnew then m1 else
extendMorphism :: Bool -- ^ check sharing (False for lambda expressions)
-> G_sign -- ^ formal parameter
-> 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
rh = symbMapToRawSymbMap h
-- do we need combining function catching the clashes???
mor <- ext_induced_from_morphism lid r sigmaB
let hmor = symmap_of lid mor
sigmaAD = ExtSign (cod mor) $
Set.map (\ sy ->
sigma <- ext_signature_union lid sigmaA sigmaAD
unless (
Set.null illShared || not sharing)
$ plain_error () ("Symbols shared between actual parameter and body"
++ "\nmust be in formal parameter:\n"
++ showDoc illShared "") nullRange
comb2 p qs [] ++ comb1 qs
comb2 p@(a, b) ((c, d) : qs) rs =
comb2 p qs $ if b == d then (a, c) : rs else rs
newIdentifications = myKernel hmor Set.\\ myKernel h
"Fitting morphism may lead to forbidden identifications:\n"
++ showDoc newIdentifications "") nullRange
incl <- ext_inclusion lid sigmaAD sigma
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
gsigmaA_i = map (getSig . snd) args
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)
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
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 [])
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
getSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)
let sannos = filter isSemanticAnno $ l_annos a
(sanno1, conflict, impliesA) = case sannos of
f@(Semantic_anno anno1 _) : r -> (case anno1 of
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')
(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 (sp1' : sps', JustNode nsig1, dg2, None, True)
expCurie :: GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI
Nothing -> expandCurie pm i
Just path -> expandCurieByPath path i
expandCurieByPath :: FilePath -> IRI -> Maybe IRI
expandCurieByPath path i = case parseIRIReference $ path ++ "?" of
prefixErrorIRI :: IRI -> Result a
prefixErrorIRI i = fatal_error ("No prefix found for CURIE " ++
iriToStringUnsecure i ++ " or expansion does not yield a valid IRI.")