d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescuDescription : static analysis of DOL OMS and heterogeneous structured specifications
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescuCopyright : (c) Till Mossakowski and Uni Magdeburg 2003-2016
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederStability : provisional
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederPortability : non-portable (imports Logic.Grothendieck)
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescuStatic analysis of DOL OMS and networks and
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu CASL (heterogeneous) structured specifications
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu Follows the semantics of DOL OMS and networks,
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu DOL OMG standard, clauses 10.2.2 and 10.2.3
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu , anaIntersect
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , anaSublogic
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder , getSpecAnnos
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder , anaRenaming
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder , anaRestriction
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder , partitionGmaps
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder , homogenizeGM
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder , extendMorphism
329f09824e0b9202d1327e52358912eddac8ad38Christian Maeder , expandCurieByPath
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa , ExpOverrides
076d5429ce08d87ebced34c308d41225e0d12cdeChristian Maeder , notFoundError
d9435c21e9292561d38b689c1a0e5ab52982277aChristian Maeder , prefixErrorIRI
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu , networkDiagram
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maederimport Common.AS_Annotation hiding (isAxiom, isDef)
152c178f9f9969ce729361a5c61aa4ff2c9ed840Christian Maederimport Common.Lib.MapSet (imageSet, setInsert)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
61fd362000bd36e5230f1bdb69cfa06dc766f3e6Christian Maederimport Proofs.ComputeColimit (insertColimitInGraph)
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa-- overrides CUIRIE expansion for Download_items
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksatype ExpOverrides = Map.Map IRI FilePath
95c27038582e8a2ce24923bee69ef15931b8b87bChristian MaedercoerceMaybeNode :: LogicGraph -> DGraph -> MaybeNode -> NodeName -> AnyLogic
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder -> Result (MaybeNode, DGraph)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian MaedercoerceMaybeNode lg dg mn nn l2 = case mn of
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder EmptyNode _ -> return (EmptyNode l2, dg)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder JustNode ns -> do
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder (ms, dg2) <- coerceNode lg dg ns nn l2
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder return (JustNode ms, dg2)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian MaedercoerceNode :: LogicGraph -> DGraph -> NodeSig -> NodeName -> AnyLogic
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder -> Result (NodeSig, DGraph)
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian MaedercoerceNode lg dg ns@(NodeSig _ (G_sign lid1 _ _)) nn l2@(Logic lid2) =
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder if language_name lid1 == language_name lid2 then return (ns, dg)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder c <- logicInclusion lg (Logic lid1) l2
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian Maeder coerceNodeByComorph c dg ns nn
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian MaedercoerceNodeByComorph :: AnyComorphism -> DGraph -> NodeSig -> NodeName
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian Maeder -> Result (NodeSig, DGraph)
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian MaedercoerceNodeByComorph c dg (NodeSig n s) nn = do
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder gmor <- gEmbedComorphism c s
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder case find (\ (_, _, l) -> dgl_origin l == SeeTarget
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder && dgl_type l == globalDef
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder && dgl_morphism l == gmor) $ outDG dg n of
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder Nothing -> do
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder let (ms@(NodeSig m _), dg2) =
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder insGSig dg (extName "XCoerced" nn) DGLogicCoercion $ cod gmor
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder dg3 = insLink dg2 gmor globalDef SeeTarget n m
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder return (ms, dg3)
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder Just (_, t, _) ->
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder return (NodeSig t $ signOf $ dgn_theory $ labDG dg t, dg)
7688e20f844fe88f75c04016841ebb5e5e3d927fChristian MaederinsGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian MaederinsGTheory dg name orig (G_theory lid syn sig ind sens tind) =
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder let (sgMap, s) = sigMapI dg
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder (tMap, t) = thMapI dg
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder nind = if ind == startSigId then succ s else ind
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder tb = tind == startThId && not (Map.null sens)
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder ntind = if tb then succ t else tind
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder nsig = G_sign lid sig nind
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder nth = G_theory lid syn sig nind sens ntind
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder node_contents = newNodeLab name orig nth
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder node = getNewNodeDG dg
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder in (NodeSig node nsig,
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder (if tb then setThMapDG $ Map.insert (succ t) nth tMap else id) $
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder (if ind == startSigId
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder then setSigMapDG $ Map.insert (succ s) nsig sgMap else id)
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder $ insNodeDG (node, node_contents) dg)
7688e20f844fe88f75c04016841ebb5e5e3d927fChristian MaederinsGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
be3f5e3e69900ececafea5b010a8400f26af5362Christian MaederinsGSig dg name orig (G_sign lid sig ind) =
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder insGTheory dg name orig $ noSensGTheory lid sig ind
8528053a6a766c3614276df0f59fb2a2e8ab6d18Christian MaederinsLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node
0d0047d6eb457b56ff10987569769a420754a56fChristian MaederinsLink dg (GMorphism cid sign si mor mi) ty orig n t =
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder let (sgMap, s) = sigMapI dg
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder (mrMap, m) = morMapI dg
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder nsi = if si == startSigId then succ s else si
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder nmi = if mi == startMorId then succ m else mi
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder nmor = GMorphism cid sign nsi mor nmi
d11391a2447a2005329a95b5d770f24e62bf5b63Christian Maeder link = defDGLink nmor ty orig
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder in (if mi == startMorId then setMorMapDG $ Map.insert (succ m)
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder (toG_morphism nmor) mrMap else id) $
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder (if si == startSigId then setSigMapDG $ Map.insert (succ s)
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder (G_sign (sourceLogic cid) sign nsi) sgMap else id)
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder $ insLEdgeNubDG (n, t, link) dg
278af20bd154d99e884bdf8c66d35d36699643c9Christian MaedercreateConsLink :: LinkKind -> Conservativity -> LogicGraph -> DGraph
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder -> MaybeNode -> NodeSig -> DGLinkOrigin -> Result DGraph
0a899fdf30f8a0702034d68cc348264562baa01dChristian MaedercreateConsLink lk conser lg dg nsig (NodeSig node gsig) orig = case nsig of
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder EmptyNode _ | conser == None -> return dg
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder _ -> case nsig of
0a899fdf30f8a0702034d68cc348264562baa01dChristian Maeder JustNode (NodeSig n sig) -> do
3086cb15387bd2d08398aad31b8b7a891d45d249Christian Maeder incl <- ginclusion lg sig gsig
3086cb15387bd2d08398aad31b8b7a891d45d249Christian Maeder return $ insLink dg incl
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder (ScopedLink Global lk $ mkConsStatus conser) orig n node
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder EmptyNode _ -> -- add conservativity to the target node
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder return $ let lbl = labDG dg node
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder in if isDGRef lbl then dg else
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder fst $ labelNodeDG
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder (nodeInfo lbl)
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder { node_cons_status = case getNodeConsStatus lbl of
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder ConsStatus c d th -> ConsStatus (max c conser) d th }}) dg
6505786996adb0239e26bb669ea579d630fa46a4Christian MaedergetNamedSpec :: SPEC_NAME -> LibName -> DGraph -> LibEnv
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder -> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
6505786996adb0239e26bb669ea579d630fa46a4Christian MaedergetNamedSpec sp ln dg libenv = case lookupGlobalEnvDG sp dg of
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder Just (SpecEntry s@(ExtGenSig (GenSig _ ps _) (NodeSig n _))) -> do
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder unless (null ps)
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder $ mkError "base theory must not be parameterized" sp
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder let t@(refLib, refDG, (_, lbl)) = lookupRefNode libenv ln dg n
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder refTok = getName $ dgn_name lbl
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder unless (sp == refTok)
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder $ appendDiags [mkDiag Warning "renamed base theory" sp]
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder if refLib == ln then return (s, t) else
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder case lookupGlobalEnvDG refTok refDG of
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder Just (SpecEntry s2) -> return (s2, t)
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder _ -> mkError "theory reference error" sp
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder _ -> mkError "unknown theory" sp
6c244f12ab0dc7ba1baf1413266093886a570e13Christian MaederanaSublogic :: HetcatsOpts -> LogicDescr -> LibName -> DGraph -> LibEnv
aeb4e74b8b3328d8ea15512ec4e1e1b8d0919f01Christian Maeder -> LogicGraph
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder -> Result (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
dc62afbf79603699b39b2387f48298634f642e67cmaederanaSublogic _opts itm ln dg libenv lG
dc62afbf79603699b39b2387f48298634f642e67cmaeder = case itm of
dc62afbf79603699b39b2387f48298634f642e67cmaeder LogicDescr (Logic_name lt ms mt) _ _ -> do
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze logN@(Logic lid) <- lookupLogic "" lt lG
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder mgs <- case ms of
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Nothing -> return Nothing
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Just subL -> do
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder let s = tokStr subL
e0c2bc4ba02902c20dae5c2e7a9bc25dbcfdfa49Christian Maeder case parseSublogic lid s of
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Nothing -> fail $ "unknown sublogic of logic " ++ show logN
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder if sublogicName (top_sublogic lid) == s then do
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder warning () ("not a proper sublogic: " ++ s) $ tokPos subL
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder return Nothing
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder else return $ Just $ G_sublogics lid sl
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder let logicLibN = emptyLibName "Logics"
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder lG1 = setCurSublogic mgs $ setLogicName itm lG
9b4d59bb654421c8fe405636bba0f12e09c65641Christian Maeder Nothing -> return (Nothing, lG1 { currentTargetBase = Nothing })
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Just sp -> do
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa let ssp = iriToStringUnsecure sp
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder (s, t@(libName, _, (_, lbl))) <- case Map.lookup logicLibN libenv of
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Just dg2 | logicLibN /= ln -> getNamedSpec sp logicLibN dg2 libenv
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder _ -> getNamedSpec sp ln dg libenv
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder case sublogicOfTh $ globOrLocTh lbl of
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder gs2@(G_sublogics lid2 _) -> do
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder unless (logN == Logic lid2)
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder $ fail $ "the logic of '" ++ ssp
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder ++ "' is '" ++ language_name lid2
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder ++ "' and not '" ++ shows logN "'!"
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Nothing -> return ()
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Just gs -> unless (isSublogic gs2 gs)
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder $ fail $ "theory '" ++ ssp
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder ++ "' has sublogic '" ++ shows gs2 "' and not '"
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder ++ shows gs "'!"
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder let sbMap = sublogicBasedTheories lG1
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder lMap = Map.findWithDefault Map.empty logN sbMap
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder nName = getDGNodeName lbl
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder nMap <- case Map.lookup sp lMap of
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder Nothing -> return $ Map.insert sp (libName, nName) lMap
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder Just (prevLib, prevName) -> do
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder unless (libName == prevLib)
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder $ fail $ "theory '" ++ ssp
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder ++ "' should come from library '"
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder ++ showDoc prevLib "' and not from '"
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder ++ showDoc libName "'!"
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder unless (nName == prevName)
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder $ fail $ "the original theory name for '" ++ ssp
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder ++ "' should be '"
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder ++ prevName ++ "' and not '"
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder ++ nName ++ "'!"
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder return (Just (s, t), lG1
9b4d59bb654421c8fe405636bba0f12e09c65641Christian Maeder { sublogicBasedTheories = Map.insert logN nMap sbMap
9b4d59bb654421c8fe405636bba0f12e09c65641Christian Maeder , currentTargetBase = Just (libName, nName) })
dc62afbf79603699b39b2387f48298634f642e67cmaeder _ -> return (Nothing, lG)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibEnv -> LibName -> DGraph
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder -> Result (SPEC, NodeSig, DGraph)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaSpecTop conser addSyms lg libEnv ln dg nsig name opts eo sp pos =
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder if conser == None || case sp of
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder -- for these cases def-links are re-used
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder Basic_spec _ _ -> True
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder Closed_spec _ _ -> True
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder Spec_inst {} -> True
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder Group _ _ -> True -- in this case we recurse
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu then anaSpecAux conser addSyms True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg nsig name opts eo sp pos
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder let provenThmLink =
bd986fa9d0f451b8166efdb9027c153d101aa65bChristian Maeder ThmLink $ Proven (DGRule "static analysis") emptyProofBasis
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (rsp, ns, rdg) <- anaSpec addSyms True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg nsig name opts eo sp pos
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder ndg <- createConsLink provenThmLink conser lg rdg nsig ns SeeTarget
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder return (rsp, ns, ndg)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaFreeOrCofreeSpec :: Bool -> LogicGraph -> LibEnv -> HetcatsOpts -> LibName -> DGraph
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder -> MaybeNode -> NodeName -> FreeOrCofree -> ExpOverrides -> Annoted SPEC
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder -> Range -> Result (Annoted SPEC, NodeSig, DGraph)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig name dglType eo asp pos =
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder adjustPos pos $ do
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder let sp = item asp
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder iPos = getRange sp
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder (sp', NodeSig n' gsigma, dg') <-
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu anaSpec addSyms True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg nsig (extName (show dglType) name) opts eo
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder let (ns@(NodeSig node _), dg2) =
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder insGSig dg' (setSrcRange pos name) (DGFreeOrCofree dglType) gsigma
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder nsigma = case nsig of
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder EmptyNode cl -> emptyG_sign cl
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder JustNode nds -> getSig nds
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder incl <- ginclusion lg nsigma gsigma
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder return (replaceAnnoted sp' asp, ns,
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder insLink dg2 incl (FreeOrCofreeDefLink dglType nsig)
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder SeeTarget n' node)
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu{- | analyze a SPEC. The first Bool Parameter determines if incoming symbols shall
7e347662208dee528a752c84bec8a59ff7bdff31mcodescube ignored while the second determines if the nodes should be optimized away for specifications without parameters. The options are needed to check: shall only the structure be
7e347662208dee528a752c84bec8a59ff7bdff31mcodescuanaSpec :: Bool -> Bool-> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder -> Result (SPEC, NodeSig, DGraph)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederanaSpec = anaSpecAux None
7e347662208dee528a752c84bec8a59ff7bdff31mcodescuanaSpecAux :: Conservativity -> Bool -> Bool
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu -> LogicGraph -> LibEnv -> LibName -> DGraph
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder -> Result (SPEC, NodeSig, DGraph)
7e347662208dee528a752c84bec8a59ff7bdff31mcodescuanaSpecAux conser addSyms optNodes lg
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu libEnv ln dg nsig name opts eo sp rg = case sp of
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder Basic_spec (G_basic_spec lid bspec) pos -> adjustPos pos $ do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let curLogic = Logic lid
f154f985ca01a20f0ea780fbc92ab55169c1e86bChristian Maeder curSL = currentSublogic lg
f154f985ca01a20f0ea780fbc92ab55169c1e86bChristian Maeder bsSL = G_sublogics lid $ minSublogic bspec
f154f985ca01a20f0ea780fbc92ab55169c1e86bChristian Maeder when (maybe False (`isProperSublogic` bsSL) curSL)
f154f985ca01a20f0ea780fbc92ab55169c1e86bChristian Maeder $ fail $ "sublogic expected: " ++ maybe "" show curSL
f154f985ca01a20f0ea780fbc92ab55169c1e86bChristian Maeder ++ " found: " ++ show bsSL
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder (nsig', dg0) <- coerceMaybeNode lg dg nsig name curLogic
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder G_sign lid' sigma' _ <- return $ case nsig' of
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder EmptyNode cl -> emptyG_sign cl
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder JustNode ns -> getSig ns
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder ExtSign sig sys <-
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder coerceSign lid' lid "Analysis of basic spec" sigma'
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder (bspec', ExtSign sigma_complete sysd, ax) <-
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder if isStructured opts
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder then return (bspec, mkExtSign $ empty_signature lid, [])
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder let res@(Result ds mb) = extBasicAnalysis lid (getName name)
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder ln bspec sig $ globalAnnos dg0
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder in case mb of
d75d2d11170f1339ebe37d9d9c06aff148637b13Christian Maeder Nothing | null ds ->
d75d2d11170f1339ebe37d9d9c06aff148637b13Christian Maeder fail "basic analysis failed without giving a reason"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa diffSig <- case signatureDiff lid sigma_complete sig of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Result _ (Just ds) -> return ds
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa _ -> warning sigma_complete
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa "signature difference could not be computed using full one" pos
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let gsysd = Set.map (G_symbol lid) sysd
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (ns, dg') = insGTheory dg0 (setSrcRange rg name)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (DGBasicSpec (Just $ G_basic_spec lid bspec')
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (G_sign lid (mkExtSign diffSig) startSigId) gsysd)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ G_theory lid (currentSyntax lg) (ExtSign sigma_complete
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (if addSyms then Set.union sys sysd else sysd)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ symset_of lid sigma_complete)
ec60f8ca1475c7be6b0187e389472ff3dad7a2eamscodescu startSigId (toThSens ax) startThId
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa return (Basic_spec (G_basic_spec lid bspec') pos, ns, dg'')
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian Maeder EmptySpec pos -> case nsig of
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian Maeder EmptyNode _ -> do
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian Maeder warning () "empty spec" pos
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder let (ns, dg') = insGSig dg (setSrcRange rg name) DGEmpty
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder (getMaybeSig nsig)
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder return (sp, ns, dg')
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder {- anaSpec should be changed to return a MaybeNode!
1c8c2b04b40b5c054da07b8d059e5ef29d4dbc32Christian Maeder Then this duplicate dummy node could be avoided.
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian Maeder Also empty unions could be treated then -}
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder JustNode ns -> return (sp, ns , dg)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Translation asp ren ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder rPos = getRange ren
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp1', ns'@(NodeSig n' gsigma), dg') <-
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu anaSpec addSyms optNodes lg libEnv ln dg nsig
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (extName "Translation" name) opts eo sp1 rPos
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder mor <- anaRenaming lg nsig gsigma opts ren
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- ??? check that mor is identity on local env
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder when (isIdentity mor) $ warning ()
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder ("nothing renamed by:\n" ++ showDoc ren "") rPos
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder (fs, dgf) <- if isIdentity mor && isInternal name then return (ns', dg')
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder let (ns@(NodeSig node _), dg'') = insGSig dg' (setSrcRange rg name)
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder (DGTranslation $ Renamed ren) $ cod mor
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- ??? too simplistic for non-comorphism inter-logic translations
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder return (ns, insLink dg'' mor globalDef SeeTarget n' node)
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder return (Translation (replaceAnnoted sp1' asp) ren, fs, dgf)
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu Extraction asp extr -> do
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu let sp0 = item asp
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu rname = extName "Extension" name
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp', nsig', dg0) <- anaSpec addSyms optNodes lg libEnv
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu ln dg nsig rname opts eo sp0 rg
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu (ns', dg1) <- anaExtraction lg libEnv ln dg0 nsig' name rg extr
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu return (Extraction (replaceAnnoted sp' asp) extr, ns', dg1)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Reduction asp restr ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
b4a750119742b015a815e6f370a7d58e7a4de634Christian Maeder rname = extName "Restriction" name
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp1', ns0, dg0) <- anaSpec addSyms optNodes lg libEnv
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu ln dg nsig rname opts eo sp1 rg
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder rLid <- getRestrLogic restr
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder p1@(NodeSig n' gsigma', dg') <- coerceNode lg dg0 ns0 rname rLid
b4a750119742b015a815e6f370a7d58e7a4de634Christian Maeder (hmor, tmor) <- anaRestriction lg (getMaybeSig nsig) gsigma' opts restr
e44da4d9d6af17dd91b3542fb3a1522439fe7c18Christian Maeder let noRename = maybe True isIdentity tmor
e44da4d9d6af17dd91b3542fb3a1522439fe7c18Christian Maeder noHide = isIdentity hmor
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder when noHide $ (if noRename then warning else hint) ()
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder ("nothing hidden by:\n" ++ showDoc restr "") $ getRange restr
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder p2@(NodeSig node1 _, dg2) <- if noHide && isInternal name then return p1
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht let trgSg = dom hmor
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht hidSyms = Set.difference (symsOfGsign gsigma')
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht $ symsOfGsign trgSg
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht orig = DGRestriction (Restricted restr) hidSyms
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht (ns@(NodeSig node _), dg'') = insGSig dg'
e44da4d9d6af17dd91b3542fb3a1522439fe7c18Christian Maeder (if noRename then name else extName "Hiding" name)
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder -- ??? too simplistic for non-comorphism inter-logic reductions
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder return (ns, insLink dg'' hmor HidingDefLink SeeTarget n' node)
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder {- we treat hiding and revealing differently
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder in order to keep the dg as simple as possible -}
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder (fs, dgf) <- case tmor of
e44da4d9d6af17dd91b3542fb3a1522439fe7c18Christian Maeder Just tmor' | not noRename -> do
f223a90d51db0fb060381211cfc07fc5b0672f58Christian Maeder let (ns@(NodeSig node2 _), dg3) =
f223a90d51db0fb060381211cfc07fc5b0672f58Christian Maeder insGSig dg2 name DGRevealTranslation $ cod tmor'
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder return (ns, insLink dg3 tmor' globalDef SeeTarget node1 node2)
f223a90d51db0fb060381211cfc07fc5b0672f58Christian Maeder Nothing -> return p2
f223a90d51db0fb060381211cfc07fc5b0672f58Christian Maeder _ -> hint p2 ("nothing renamed by:\n" ++ showDoc restr "")
f223a90d51db0fb060381211cfc07fc5b0672f58Christian Maeder $ getRange restr
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder return (Reduction (replaceAnnoted sp1' asp) restr, fs, dgf)
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu Filtering asp filtering -> do
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu let sp1 = item asp
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu rname = extName "Filtering" name
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp', nsig', dg') <- anaSpec addSyms optNodes lg libEnv ln dg
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu nsig rname opts eo sp1 rg
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu (nf, dgF) <- anaFiltering lg libEnv ln dg' nsig' name filtering
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu return (Filtering (replaceAnnoted sp' asp) filtering, nf, dgF)
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu -- error "analysis of filterings not yet implemented"
dc62afbf79603699b39b2387f48298634f642e67cmaeder Minimization asp (Mini kw cm cv poss) -> do
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig
e8b91b8571b73f2381bed87cb3ea95c76a4201b2Marcel Zirbel name Minimize eo asp poss
dc62afbf79603699b39b2387f48298634f642e67cmaeder return (Minimization nasp (Mini kw cm cv poss), nsig', dg')
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder Union asps pos -> do
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (newAsps, _, ns, dg') <- adjustPos pos $ anaUnion addSyms lg libEnv ln dg nsig
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder name opts eo asps rg
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder return (Union newAsps pos, ns, dg')
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu Intersection asps pos -> do
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (newAsps, _, ns, dg') <- adjustPos pos $ anaIntersect addSyms lg libEnv ln dg nsig
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu name opts eo asps rg
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu return (Intersection newAsps pos, ns, dg')
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Extension asps pos -> do
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder let namedSps = map (\ (asp, n) ->
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder let nn = incBy n (extName "Extension" name) in
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder if n < length asps then (nn, asp)
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder else (name { xpath = xpath nn }, asp)) $ number asps
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (sps', nsig1', dg1, _, _) <- foldM (anaExtension lg libEnv opts eo ln pos)
6b00a9239fe7c804524099ca3d25f4ffc6079ceeChristian Maeder ([], nsig, dg, conser, addSyms) namedSps
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder case nsig1' of
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder EmptyNode _ -> fail "empty extension"
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder JustNode nsig1 -> return (Extension (zipWith replaceAnnoted
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder (reverse sps') asps)
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder pos, nsig1, dg1)
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder Free_spec asp poss -> do
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder name Free eo asp poss
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder return (Free_spec nasp poss, nsig', dg')
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder Cofree_spec asp poss -> do
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder name Cofree eo asp poss
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder return (Cofree_spec nasp poss, nsig', dg')
8b130bc25851c830d22a51ba03c8f2b778a6904fMarcel Zirbel Minimize_spec asp poss -> do
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig
8b130bc25851c830d22a51ba03c8f2b778a6904fMarcel Zirbel name Minimize eo asp poss
8b130bc25851c830d22a51ba03c8f2b778a6904fMarcel Zirbel return (Minimize_spec nasp poss, nsig', dg')
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder Local_spec asp asp' poss -> adjustPos poss $ do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let sp1 = item asp
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder pos1 = getRange sp1
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski sp1' = item asp'
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder pos1' = getRange sp1'
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder lname = extName "Local" name
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder (sp2, nsig'@(NodeSig _ gsig1), dg') <-
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu anaSpec False True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg nsig (extName "Spec" lname) opts eo sp1 pos1
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp2', NodeSig n'' gsig2@(G_sign lid2 sigma2 _), dg'') <-
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu anaSpec False True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg' (JustNode nsig') (extName "Within" lname) opts eo sp1' pos1'
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder let gSigN = getMaybeSig nsig
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder (G_sign lid sigmaN _, _) <- gSigCoerce lg gSigN (Logic lid2)
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder sigma <- coerceSign lid lid2 "Analysis of local spec1" sigmaN
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder (G_sign lid' sigma' _, _) <- gSigCoerce lg gsig1 (Logic lid2)
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder sigma1 <- coerceSign lid' lid2 "Analysis of local spec2" sigma'
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder let sys = ext_sym_of lid2 sigma
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder sys1 = ext_sym_of lid2 sigma1
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder sys2 = ext_sym_of lid2 sigma2
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder mor3 <- if isStructured opts then return (ext_ide sigma2)
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder else ext_cogenerated_sign lid2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (sys1 `Set.difference` sys) sigma2
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder let sigma3 = dom mor3
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder gsigma3 = G_sign lid2 (makeExtSign lid2 sigma3) startSigId
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz sys3 = symset_of lid2 sigma3
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder unless (isStructured opts
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder || sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3)
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder $ plain_error () (
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder "illegal use of locally declared symbols: "
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder ++ showDoc ((sys2 `Set.intersection` sys1) `Set.difference` sys3) "")
f8c8c3e92d02616c7a2994b3aa62a541870796d8Christian Maeder let hidSyms = Set.difference (symsOfGsign gsig2) $ symsOfGsign gsigma3
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht orig = DGRestriction NoRestriction hidSyms
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht (ns@(NodeSig node _), dg2) = insGSig dg'' name orig gsigma3
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski return (Local_spec (replaceAnnoted sp2 asp)
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski (replaceAnnoted sp2' asp')
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid2 mor3)
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder HidingDefLink SeeTarget n'' node)
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder Closed_spec asp pos -> adjustPos pos $ do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let sp1 = item asp
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder pos1 = getRange sp1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder l = getLogic nsig
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski -- analyse spec with empty local env
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp', NodeSig n' gsigma', dg') <- anaSpec False True lg libEnv ln dg
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder (EmptyNode l) (extName "Closed" name) opts eo sp1 pos1
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian Maeder gsigma2 <- gsigUnionMaybe lg addSyms nsig gsigma'
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder let (ns@(NodeSig node _), dg2) = insGSig dg' name DGClosed gsigma2
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder incl2 <- ginclusion lg gsigma' gsigma2
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder let dg3 = insLink dg2 incl2 globalDef SeeTarget n' node
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder dg4 <- createConsLink DefLink conser lg dg3 nsig ns DGLinkClosedLenv
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder return (Closed_spec (replaceAnnoted sp' asp) pos, ns, dg4)
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder Qualified_spec lognm asp pos -> adjustPos pos $ do
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder let newLG = setLogicName lognm lg
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder l <- lookupCurrentLogic "Qualified_spec" newLG
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder let newNSig = case nsig of
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder EmptyNode _ -> EmptyNode l
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder qname = extName "Qualified" name
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp', ns', dg') <- anaSpec addSyms optNodes newLG libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg newNSig qname opts eo
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder (item asp) pos
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder (ns, dg2) <- coerceNode lg dg' ns' qname l
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder return (Qualified_spec lognm asp { item = sp' } pos, ns, dg2)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Group asp pos -> do
63fb549acb4eddfd045bb55da66c1fd4ff5b1ac5Christian Maeder (sp', nsig', dg') <-
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu anaSpecTop conser addSyms lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg nsig name opts eo (item asp) rg
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder return (Group (replaceAnnoted sp' asp) pos, nsig', dg')
dc62afbf79603699b39b2387f48298634f642e67cmaeder Spec_inst spname' afitargs mImp pos0 -> do
b8bbe51da2883ef86242bccb3ee6744ba5922f08Christian Maeder spname <- expCurieR (globalAnnos dg) eo spname'
b8bbe51da2883ef86242bccb3ee6744ba5922f08Christian Maeder let pos = if null afitargs then iriPos spname else pos0
b8bbe51da2883ef86242bccb3ee6744ba5922f08Christian Maeder adjustPos pos $ case lookupGlobalEnvDG spname dg of
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder Just (SpecEntry gs@(ExtGenSig (GenSig _ params _)
ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder body@(NodeSig nB gsigmaB))) ->
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder case (length afitargs, length params) of
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- the case without parameters leads to a simpler dg
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder (0, 0) -> case nsig of
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder -- if the node shall not be named and the logic does not change,
e24628ebf98f8c4dc43cd1758468e956700d603cmcodescu EmptyNode _ | isInternal name && optNodes -> do
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder dg2 <- createConsLink DefLink conser lg dg nsig body SeeTarget
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder -- then just return the body
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder return (sp, body, dg2)
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder -- otherwise, we need to create a new one
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian Maeder gsigma <- gsigUnionMaybe lg addSyms nsig gsigmaB
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder let (fsig@(NodeSig node _), dg2) =
c5653d37b37dcc025ff6dd1eada95ae67116e699Christian Maeder insGSig dg name (DGInst spname) gsigma
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder incl <- ginclusion lg gsigmaB gsigma
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder let dg3 = case nsig of
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder JustNode (NodeSig nI _) | nI == nB -> dg2
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder _ -> insLink dg2 incl globalDef (DGLinkMorph spname) nB node
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder dg4 <- createConsLink DefLink conser lg dg3 nsig fsig SeeTarget
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder return (sp, fsig, dg4)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- now the case with parameters
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder (la, lp) | la == lp -> do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder (ffitargs, dg', (morDelta, gsigmaA, ns@(NodeSig nA gsigmaRes))) <-
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu anaAllFitArgs lg libEnv opts eo ln dg nsig name spname gs afitargs
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder GMorphism cid _ _ _ _ <- return morDelta
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder morDelta' <- case nsig of
58665d6a311aec23a2a6afd33f83b6911f4a9b6fChristian Maeder | logicOfGsign gsigmaA == logicOfGsign gsigmaRes
58665d6a311aec23a2a6afd33f83b6911f4a9b6fChristian Maeder -> return morDelta
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder _ -> ginclusion lg gsigmaA gsigmaRes >>= comp morDelta
06afcb70f335c6de74007dc5d6bb19a7d06de457Christian Maeder (_, imor) <- gSigCoerce lg gsigmaB $ Logic $ sourceLogic cid
06afcb70f335c6de74007dc5d6bb19a7d06de457Christian Maeder tmor <- gEmbedComorphism imor gsigmaB
06afcb70f335c6de74007dc5d6bb19a7d06de457Christian Maeder morDelta'' <- comp tmor morDelta'
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder let dg4 = case nsig of
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder JustNode (NodeSig nI _) | nI == nB -> dg'
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder _ -> insLink dg' morDelta'' globalDef (DGLinkMorph spname) nB nA
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder dg5 <- createConsLink DefLink conser lg dg4 nsig ns SeeTarget
dc62afbf79603699b39b2387f48298634f642e67cmaeder return (Spec_inst spname ffitargs mImp pos, ns, dg5)
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder | otherwise -> instMismatchError spname lp la pos
d687e0d953247ab99d8f2027466bd3c2962e3ba1Christian Maeder _ | null afitargs -> do
d687e0d953247ab99d8f2027466bd3c2962e3ba1Christian Maeder warning () ("ignoring missing spec " ++ showDoc spname' "") pos
6f52b2f195d946649597c21e5888c70ccfeeb81eChristian Maeder EmptyNode _ -> do -- copied from EmptySpec case
6f52b2f195d946649597c21e5888c70ccfeeb81eChristian Maeder let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)
6f52b2f195d946649597c21e5888c70ccfeeb81eChristian Maeder return (sp, ns, dg')
d687e0d953247ab99d8f2027466bd3c2962e3ba1Christian Maeder JustNode ns -> return (sp, ns , dg)
6f52b2f195d946649597c21e5888c70ccfeeb81eChristian Maeder _ -> notFoundError "structured spec" spname
ba5c87b3f4a921f0932a08de48a3aedd3ca4d25bTill Mossakowski -- analyse "data SPEC1 SPEC2"
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder Data lD@(Logic lidD) lP asp1 asp2 pos -> adjustPos pos $ do
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder let sp1 = item asp1
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder pos1 = getRange sp1
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski sp2 = item asp2
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder {- look for the inclusion comorphism from the current logic's data logic
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder into the current logic itself -}
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder c <- logicInclusion lg lD lP
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian Maeder let dname = extName "Data" name
ba5c87b3f4a921f0932a08de48a3aedd3ca4d25bTill Mossakowski -- analyse SPEC1
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp1', ns', dg') <- anaSpec False True (setCurLogic (language_name lidD) lg)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu libEnv ln dg (EmptyNode lD) dname opts eo sp1 pos1
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder -- force the result to be in the data logic
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder (ns'', dg'') <- coerceNode lg dg' ns' (extName "Qualified" dname) lD
ba5c87b3f4a921f0932a08de48a3aedd3ca4d25bTill Mossakowski -- translate SPEC1's signature along the comorphism
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian Maeder (nsig2@(NodeSig node gsigmaD), dg2) <-
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder coerceNodeByComorph c dg'' ns'' dname
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder (usig, udg) <- case nsig of
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder EmptyNode _ -> return (nsig2, dg2)
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder JustNode ns2 -> do
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian Maeder gsigma2 <- gsigUnion lg addSyms (getSig ns2) gsigmaD
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder let (ns@(NodeSig node2a _), dg2a) =
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder insGSig dg2 (extName "Union" name) DGUnion gsigma2
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder incl2 <- ginclusion lg gsigmaD gsigma2
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder let dg3 = insLink dg2a incl2 globalDef SeeTarget node node2a
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder dg4 <- createConsLink DefLink conser lg dg3 nsig ns SeeTarget
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder return (ns, dg4)
ba5c87b3f4a921f0932a08de48a3aedd3ca4d25bTill Mossakowski -- analyse SPEC2
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder (sp2', nsig3, udg3) <-
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu anaSpec addSyms optNodes lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu udg (JustNode usig) name opts eo sp2 rg
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder return (Data lD lP
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted sp1' asp1)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted sp2' asp2)
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder pos, nsig3, udg3)
72b8c0349a58cf0eb361cb5bb410d95a0372900acmaeder Combination (Network cItems eItems _) pos -> adjustPos pos $ do
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu let (cNodes', cEdges') = networkDiagram dg cItems eItems
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu (ns, dg') <- insertColimitInGraph libEnv ln dg cNodes' cEdges' name
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu return (sp, ns, dg')
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu _ -> fail $ "AnalysisStructured: " ++ show (prettyLG lg sp)
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu-- | build the diagram of a network specified as a list of network elements to be added
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu-- | and a list of network elements to be removed
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescunetworkDiagram :: DGraph
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu -> [LABELED_ONTO_OR_INTPR_REF]
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu -> ([Node], [(Node, Node, DGLinkLab)])
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescunetworkDiagram dg cItems eItems = let
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu -- add to/remove from a list of nodes and a list of edges
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu -- the graph of a network element
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu -- if remove is true, nElem gets removed
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu getNodes remove (cN, cE) nElem = let
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu cEntry = fromMaybe (error $ "No entry for " ++ show nElem)
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu $ lookupGlobalEnvDG nElem dg
64c1fbfdbd96b2ca16510c54aad75e70af0dc0d4Mihai Codescu bgraph = dgBody dg
0c7a5718636b5ac4cd96688a004237554908d226Mihai Codescu lEdge x y m = case filter (\ (_, z, l) -> (z == y) &&
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder (dgl_morphism l == m) ) $
0c7a5718636b5ac4cd96688a004237554908d226Mihai Codescu out bgraph x of
3309ee889ed2b18e7d5d2ec7dfec07c92f0afd37mcodescu [] -> error $ "No edge found:\n x:" ++ show x ++ "\n y: " ++ show y
c407b24867ead99e2a96fc382058a7ee52379d82mcodescu in case cEntry of
366fdbbb365440e63a90302d65a2311400bb0fadChristian Maeder SpecEntry extGenSig -> let
450423c9f0a895858fca35a122783120df27eb4bMihai Codescu n = getNode $ extGenBody extGenSig
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu in if remove then
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu (n:cN, nub $ cE ++ out bgraph n ++ inn bgraph n)
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu -- remove all incoming and outgoing edges of n
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu else if elem n cN then (cN, cE) else (n : cN, cE)
0c7a5718636b5ac4cd96688a004237554908d226Mihai Codescu ViewOrStructEntry True (ExtViewSig ns gm eGS) -> let
fb891ddc67e73a126dfca1664396ec75068fd8cbMihai Codescu s = getNode ns
6f52b2f195d946649597c21e5888c70ccfeeb81eChristian Maeder t = getNode $ extGenBody eGS
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu in if remove
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu then (cN, lEdge s t gm : cE)
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu -- keep the nodes and remove just the edge
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu else(nub $ s : t : cN, lEdge s t gm : cE)
6f52b2f195d946649597c21e5888c70ccfeeb81eChristian Maeder AlignEntry asig ->
3309ee889ed2b18e7d5d2ec7dfec07c92f0afd37mcodescu AlignMor src gmor tar -> let
64c1fbfdbd96b2ca16510c54aad75e70af0dc0d4Mihai Codescu s = getNode src
64c1fbfdbd96b2ca16510c54aad75e70af0dc0d4Mihai Codescu t = getNode tar
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder in (nub $ s : t : cN, lEdge s t gmor : cE)
3309ee889ed2b18e7d5d2ec7dfec07c92f0afd37mcodescu AlignSpan src phi1 tar1 phi2 tar2 -> let
64c1fbfdbd96b2ca16510c54aad75e70af0dc0d4Mihai Codescu s = getNode src
64c1fbfdbd96b2ca16510c54aad75e70af0dc0d4Mihai Codescu t1 = getNode tar1
6f52b2f195d946649597c21e5888c70ccfeeb81eChristian Maeder t2 = getNode tar2
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder in (nub $ [s, t1, t2] ++ cN,
0c7a5718636b5ac4cd96688a004237554908d226Mihai Codescu [lEdge s t1 phi1, lEdge s t2 phi2] ++ cE)
d500a2dce0d9ebcc9645492af851667d1fbba9d2mcodescu WAlign src1 i1 sig1 src2 i2 sig2 tar1 tar2 bri -> let
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder s1 = getNode src1
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu s2 = getNode src2
e40758c36e3e5312669558ad189b24b3eaf10c59Mihai Codescu t1 = getNode tar1
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder t2 = getNode tar2
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder b = getNode bri
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu in if remove then
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu (nub $ s1 : s2 : b : cN,
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu [lEdge s1 b i1, lEdge s1 t1 sig1,
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu lEdge s2 b i2, lEdge s2 t2 sig2] ++ cE)
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu else (nub $ s1 : s2 : t1 : t2 : b : cN,
3309ee889ed2b18e7d5d2ec7dfec07c92f0afd37mcodescu [lEdge s1 b i1, lEdge s1 t1 sig1,
3309ee889ed2b18e7d5d2ec7dfec07c92f0afd37mcodescu lEdge s2 b i2, lEdge s2 t2 sig2] ++ cE)
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu NetworkEntry diag -> let
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu dnodes = nodes diag
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu ledges = labEdges diag
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu dgedges = map (\(x,y, (_, m)) -> lEdge x y m) ledges
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu in (dnodes, dgedges)
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu _ -> error $ show nElem
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu ++ " is not an OMS, a view, a network or an alignment"
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu -- also add the implicit elements: paths of global def. links,
e69f2676b133abcc72bc62a780d3762fd608a1ddmcodescu -- hiding def. links, inclusions of DOL intersections
30cd8eefefc81e17c3f7b862d63ccb310057b14aMihai Codescu addGDefLinks (cN, iN, cE) n = let
450423c9f0a895858fca35a122783120df27eb4bMihai Codescu g = dgBody dg
366fdbbb365440e63a90302d65a2311400bb0fadChristian Maeder allGDef = all $ \ (_, _, l) -> isGlobalDef $ dgl_type l
450423c9f0a895858fca35a122783120df27eb4bMihai Codescu gDefPaths x y = filter allGDef $ getPathsTo x y g
450423c9f0a895858fca35a122783120df27eb4bMihai Codescu nPaths = concat $ concatMap (gDefPaths n) cN
366fdbbb365440e63a90302d65a2311400bb0fadChristian Maeder nNodes = concatMap (\ (x, y, _) -> [x, y]) nPaths
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder hideLinks = filter (\ (_, _, l) -> dgl_type l == HidingDefLink)
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu $ concatMap (inn g) $ cN ++ nNodes
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder hNodes = map (\ (x, _, _) -> x) hideLinks
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu implicitNodes = nub $ iN ++ nNodes ++ hNodes
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu intersectLinks = filter (\ (_, _, l) -> dgl_origin l == DGLinkIntersect)
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu $ concatMap (inn g) $ cN ++ implicitNodes
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu in (cN, implicitNodes
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu , nub $ nPaths ++ cE ++ hideLinks ++ intersectLinks)
30cd8eefefc81e17c3f7b862d63ccb310057b14aMihai Codescu addLinks (cN, cE) = foldl addGDefLinks (cN, [], cE) cN
366fdbbb365440e63a90302d65a2311400bb0fadChristian Maeder (cNodes, iNodes, cEdges) =
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu addLinks . foldl (getNodes False) ([], []) $ getItems cItems
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu (eNodes, eEdges) = foldl (getNodes True) ([], []) eItems
366fdbbb365440e63a90302d65a2311400bb0fadChristian Maeder (cNodes', cEdges') = (nub (cNodes ++ iNodes) \\ eNodes,
30cd8eefefc81e17c3f7b862d63ccb310057b14aMihai Codescu cEdges \\ eEdges)
2fffd97efb53c792854c1557a87fd4f994e5a2b3mcodescu in (cNodes', cEdges')
02d61a52f776972238eef73fa8b752fd15e1f5ddMarcel ZirbelgetItems :: [LABELED_ONTO_OR_INTPR_REF] -> [IRI]
02d61a52f776972238eef73fa8b752fd15e1f5ddMarcel ZirbelgetItems [] = []
61fd362000bd36e5230f1bdb69cfa06dc766f3e6Christian MaedergetItems (Labeled _ i : r) = i : getItems r
ea8e98e298f33f9362293f392c8fb192722b8904Eugen KuksainstMismatchError :: IRI -> Int -> Int -> Range -> Result a
ea8e98e298f33f9362293f392c8fb192722b8904Eugen KuksainstMismatchError spname lp la = fatal_error $ iriToStringUnsecure spname
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa ++ " expects " ++ show lp ++ " arguments" ++ " but was given " ++ show la
076d5429ce08d87ebced34c308d41225e0d12cdeChristian MaedernotFoundError :: String -> IRI -> Result a
076d5429ce08d87ebced34c308d41225e0d12cdeChristian MaedernotFoundError str sid = fatal_error (str ++ " '" ++ iriToStringUnsecure sid
076d5429ce08d87ebced34c308d41225e0d12cdeChristian Maeder ++ "' or '" ++ iriToStringShortUnsecure sid ++ "' not found") $ iriPos sid
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian MaedergsigUnionMaybe :: LogicGraph -> Bool -> MaybeNode -> G_sign -> Result G_sign
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian MaedergsigUnionMaybe lg both mn gsig = case mn of
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder EmptyNode _ -> return gsig
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian Maeder JustNode ns -> gsigUnion lg both (getSig ns) gsig
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescuanaExtraction :: LogicGraph -> LibEnv -> LibName -> DGraph -> NodeSig -> NodeName -> Range ->
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu EXTRACTION -> Result (NodeSig, DGraph)
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescuanaExtraction lg libEnv ln dg nsig name rg (ExtractOrRemove b iris _) = if not b then
d5b702e995509f5bca70434c3649a9bd75454d79mcodescu fail "analysis of remove not implemented yet"
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu let dg0 = markHiding libEnv dg
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu n = getNode nsig
d500a2dce0d9ebcc9645492af851667d1fbba9d2mcodescu if labelHasHiding $ labDG dg0 n then
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu fail "cannot extract module from a non-flattenable OMS"
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu let dgThm = computeDGraphTheories libEnv ln dg0
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu gth = case (globalTheory . labDG dgThm) n of
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu Nothing -> error "not able to compute theory"
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu Just th -> th
66d28f86d616f3b0eabbbdc2318b46dc9057c695mcodescu mTh <- case gth of
74ae828c3bd071373c1474eeb8567585135e500dmcodescu G_theory lid syntax (ExtSign sig _) _ gsens _ -> do
74ae828c3bd071373c1474eeb8567585135e500dmcodescu let nsens = toNamedList gsens
66d28f86d616f3b0eabbbdc2318b46dc9057c695mcodescu (msig, msens) <- extract_module lid iris (sig, nsens)
74ae828c3bd071373c1474eeb8567585135e500dmcodescu return $ G_theory lid syntax
74ae828c3bd071373c1474eeb8567585135e500dmcodescu (ExtSign msig $ foldl Set.union Set.empty $ sym_of lid msig) startSigId
66d28f86d616f3b0eabbbdc2318b46dc9057c695mcodescu (toThSens msens) startThId
66d28f86d616f3b0eabbbdc2318b46dc9057c695mcodescu let (nsig', dg') = insGTheory dg (setSrcRange rg name) DGExtract mTh
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu incl <- ginclusion lg (getSig nsig') (getSig nsig)
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu let dg'' = insLink dg' incl globalThm SeeSource (getNode nsig') n
b091c4dea1b7100eea1c1e61cfd534e85e43c5c3mcodescu return (nsig', dg'')
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaUnion :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaUnion addSyms lg libEnv ln dg nsig name opts eo asps rg = case asps of
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder [] -> fail "empty union"
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder let sps = map item asps
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder (sps', nsigs, dg', _) <-
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder let ana (sps1, nsigs, dg', n) sp' = do
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder let n1 = inc n
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder (sp1, nsig', dg1) <-
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu anaSpec addSyms True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg' nsig n1 opts eo sp' $ getRange sp'
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder return (sp1 : sps1, nsig' : nsigs, dg1, n1)
22250d2b3c9f86fe19cba665d71c301de03db142Christian Maeder in foldM ana ([], [], dg, extName "Union" name) sps
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder let newAsps = zipWith replaceAnnoted (reverse sps') asps
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder case nsigs of
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder [ns] -> return (newAsps, nsigs, ns, dg')
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder let nsigs' = reverse nsigs
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder gbigSigma <- gsigManyUnion lg (map getSig nsigs')
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder let (ns@(NodeSig node _), dg2) = insGSig dg' (setSrcRange rg name)
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder DGUnion gbigSigma
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder insE dgl (NodeSig n gsigma) = do
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder incl <- ginclusion lg gsigma gbigSigma
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder return $ insLink dgl incl globalDef SeeTarget n node
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder dg3 <- foldM insE dg2 nsigs'
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder return (newAsps, nsigs', ns, dg3)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaIntersect :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaIntersect addSyms lg libEnv ln dg nsig name opts eo asps rg = case asps of
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu [] -> fail "empty intersection"
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu let sps = map item asps
431eff6083370269f3a37767bcde001f389ac927mcodescu ana (sps1, nsigs, dg', n) sp' = do
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu let n1 = inc n
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (sp1, nsig', dg1) <-
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu anaSpec addSyms True lg libEnv ln dg' nsig n1 opts eo sp' $
431eff6083370269f3a37767bcde001f389ac927mcodescu getRange sp'
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu return (sp1 : sps1, nsig' : nsigs, dg1, n1)
431eff6083370269f3a37767bcde001f389ac927mcodescu (sps', nsigs, dg', _) <-
431eff6083370269f3a37767bcde001f389ac927mcodescu foldM ana ([], [], dg, extName "Intersect" name) sps
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu let newAsps = zipWith replaceAnnoted (reverse sps') asps
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu case nsigs of
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu [ns] -> return (newAsps, nsigs, ns, dg')
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu let nsigs' = reverse nsigs
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu labelHidings = map labelHasHiding $ map (\n -> labDG (markHiding libEnv dg) $ getNode n) nsigs'
d5a225e7c58f6a8ab7b5acda22841784a19e261fmcodescu hasHiding = foldl (\x y -> x || y) False labelHidings
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu case hasHiding of
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu True -> fail "Intersection is defined only for flattenable theories"
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu False -> do
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu let dgThm = computeDGraphTheories libEnv ln dg
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu theo:theos = map (\x -> case (globalTheory . labDG dgThm . getNode) x of
1aac973ee8f1d431f097c83797771b72d1f9e05fmcodescu Nothing -> error $ "not able to compute theory of node" ++ (show $ getNode x)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu Just th -> th) nsigs'
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu gbigSigma <- gsigManyIntersect lg (map getSig nsigs')
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu gth <- foldM (intersectG_sentences gbigSigma) theo theos
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu let (ns@(NodeSig node _), dg2) = insGTheory dg' (setSrcRange rg name)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu DGIntersect gth
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu insE dgl (NodeSig n gsigma) = do
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu incl <- ginclusion lg gbigSigma gsigma
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu return $ insLink dgl incl globalThm DGLinkIntersect node n
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu dg3 <- foldM insE dg2 nsigs'
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu return (newAsps, nsigs', ns, dg3)
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescuanaFiltering :: LogicGraph -> LibEnv -> LibName -> DGraph -> NodeSig -> NodeName-> FILTERING
74ae828c3bd071373c1474eeb8567585135e500dmcodescu -> Result (NodeSig, DGraph)
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescuanaFiltering lg libEnv ln dg nsig nname filtering = case filtering of
74ae828c3bd071373c1474eeb8567585135e500dmcodescu FilterSymbolList selectOrReject (G_symb_items_list lidS sItems) _ ->
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu if not selectOrReject then do
c4fb83732e318acadfa1276c6a11edf2dbea4ac4mcodescu let strs = concatMap (symb_items_name lidS) sItems
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu dgThm = computeDGraphTheories libEnv ln dg
74ae828c3bd071373c1474eeb8567585135e500dmcodescu case (globalTheory . labDG dgThm . getNode) nsig of
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu Nothing -> error "error computing theory"
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu Just t -> t
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu G_theory l1 ser1 sig1 ind1 sens1 ind1' -> do
74ae828c3bd071373c1474eeb8567585135e500dmcodescu let gth' = G_theory l1 ser1 sig1 ind1
74ae828c3bd071373c1474eeb8567585135e500dmcodescu (foldl (\m x -> Map.delete x m) sens1 strs) ind1'
fd5f47169d0cdb3ce37ce51489d84458cebbc5a9mcodescu let (ns@(NodeSig node gsigma), dg') = insGTheory dg nname DGEmpty gth'
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu gmor <- ginclusion lg gsigma $ getSig nsig
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu let dg2 = insLink dg' gmor globalThm SeeSource node $ getNode nsig
a2f07df650cfeb9f69a6116df58ce4769cc13b59mcodescu return (ns, dg2)
1aac973ee8f1d431f097c83797771b72d1f9e05fmcodescu else error "analysis of select not implemented yet"
74ae828c3bd071373c1474eeb8567585135e500dmcodescu FilterBasicSpec _ _ _ -> error "filtering a basic spec not implemented yet"
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of renamings
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederanaRen :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder -> G_mapping -> Result GMorphism
6505786996adb0239e26bb669ea579d630fa46a4Christian MaederanaRen lg opts lenv pos gmor@(GMorphism r sigma ind1 mor _) gMapping =
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder adjustPos pos $ case gMapping of
1805f9816e3414ab184fb8546ab1abc6241f04cdChristian Maeder G_symb_map (G_symb_map_items_list lid sis) ->
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder let lid2 = targetLogic r in
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder if language_name lid2 == language_name lid then
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder if isStructured opts then return gmor else do
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis
80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder src@(ExtSign sig _) <- return $ makeExtSign lid2 $ cod mor
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder rmap <- stat_symb_map_items lid2 sig Nothing sis1
80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder mor1 <- ext_induced_from_morphism lid2 rmap src
1805f9816e3414ab184fb8546ab1abc6241f04cdChristian Maeder EmptyNode _ -> return ()
20f242685d34882b97b7447426c50cfc5ac710cfChristian Maeder JustNode (NodeSig _ sigLenv) -> do
1805f9816e3414ab184fb8546ab1abc6241f04cdChristian Maeder -- needs to be changed for logic translations
20f242685d34882b97b7447426c50cfc5ac710cfChristian Maeder (G_sign lid1 sigmaLenv1 _, _) <-
20f242685d34882b97b7447426c50cfc5ac710cfChristian Maeder gSigCoerce lg sigLenv (Logic lid2)
20f242685d34882b97b7447426c50cfc5ac710cfChristian Maeder sigmaLenv' <- coerceSign lid1 lid2 "" sigmaLenv1
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder let sysLenv = ext_sym_of lid2 sigmaLenv'
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder m = symmap_of lid2 mor1
1805f9816e3414ab184fb8546ab1abc6241f04cdChristian Maeder isChanged sy = case Map.lookup sy m of
1805f9816e3414ab184fb8546ab1abc6241f04cdChristian Maeder Just sy' -> sy /= sy'
1805f9816e3414ab184fb8546ab1abc6241f04cdChristian Maeder Nothing -> False
1805f9816e3414ab184fb8546ab1abc6241f04cdChristian Maeder forbiddenSys = Set.filter isChanged sysLenv
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder unless (Set.null forbiddenSys) $ plain_error () (
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder "attempt to rename the following symbols from " ++
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder "the local environment:\n" ++ showDoc forbiddenSys "") pos
ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder mor2 <- comp mor mor1
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder return $ GMorphism r sigma ind1 mor2 startMorId
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder comor <- logicInclusion lg (Logic lid2) (Logic lid)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder gmorTrans <- gEmbedComorphism comor $ cod gmor
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder newMor <- comp gmor gmorTrans
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder anaRen lg opts lenv pos newMor gMapping
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder G_logic_translation (Logic_code tok src tar pos1) ->
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze let pos2 = if pos1 == nullRange then pos else pos1
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze adj1 = adjustPos pos2
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder G_sign srcLid srcSig ind <- return (cod gmor)
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder c <- case tok of
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze Just c -> lookupComorphism c lg
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski Nothing -> case tar of
53ea24e19dbd4ca72fd75ab3a3105dc9f99e4f81Christian Maeder Just (Logic_name l _ _) ->
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze lookupLogic "with logic: " l lg
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder >>= logicInclusion lg (Logic srcLid)
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski Nothing -> fail "with logic: cannot determine comorphism"
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze checkSrcOrTarLogic pos2 True c src
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze checkSrcOrTarLogic pos2 False c tar
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder mor1 <- gEmbedComorphism c (G_sign srcLid srcSig ind)
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder comp gmor mor1
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. SchulzecheckSrcOrTarLogic :: Range -> Bool -> AnyComorphism -> Maybe Logic_name
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. SchulzecheckSrcOrTarLogic pos b (Comorphism cid) ml = case ml of
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder Nothing -> return ()
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze Just (Logic_name s _ _) ->
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder when (s /= if b then language_name $ sourceLogic cid
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder else language_name $ targetLogic cid)
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder $ plain_error () (s ++ " is is not the "
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder ++ (if b then "source" else "target") ++ " logic of "
d0916b96ca9f90822c0bb6062b13d5de83bf410aSoeren D. Schulze ++ language_name cid) pos
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederanaRenaming :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder -> Result GMorphism
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederanaRenaming lg lenv gSigma opts (Renaming ren pos) =
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder foldM (anaRen lg opts lenv pos) (ide gSigma) ren
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian MaedergetRestrLogic :: RESTRICTION -> Result AnyLogic
b4a750119742b015a815e6f370a7d58e7a4de634Christian MaedergetRestrLogic restr = case restr of
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder Revealed (G_symb_map_items_list lid _) _ -> return $ Logic lid
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder Hidden l _ -> case l of
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder [] -> error "getRestrLogic"
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder h : _ -> case h of
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder G_symb_list (G_symb_items_list lid _) -> return $ Logic lid
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder G_logic_projection (Logic_code _ _ _ pos1) ->
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder fatal_error "no analysis of logic projections yet" pos1
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- analysis of restrictions
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian MaederanaRestr :: LogicGraph -> G_sign -> Range -> GMorphism -> G_hiding
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder -> Result GMorphism
333c50750432f91e80aa5608be64a07f17cbb1c1Christian MaederanaRestr lg sigEnv pos (GMorphism cid (ExtSign sigma1 sys1) _ mor _) gh =
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder G_symb_list (G_symb_items_list lid' sis') -> do
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder let lid1 = sourceLogic cid
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction1" sis'
80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder rsys <- stat_symb_items lid1 sigma1 sis1
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz let sys = symset_of lid1 sigma1
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder sys' = Set.filter (\ sy -> any (matches lid1 sy) rsys) sys
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder unmatched = filter ( \ rsy -> Set.null $ Set.filter
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder ( \ sy -> matches lid1 sy rsy) sys') rsys
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder unless (null unmatched)
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder $ plain_error () ("attempt to hide unknown symbols:\n"
62607bfd8541a700d18aee4f9cdb037aded5ab0bChristian Maeder ++ showDoc unmatched "") pos
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder -- needs to be changed when logic projections are implemented
333c50750432f91e80aa5608be64a07f17cbb1c1Christian Maeder (G_sign lidE sigmaLenv0 _, _) <- gSigCoerce lg sigEnv (Logic lid1)
333c50750432f91e80aa5608be64a07f17cbb1c1Christian Maeder sigmaLenv' <- coerceSign lidE lid1 "" sigmaLenv0
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let sysLenv = ext_sym_of lid1 sigmaLenv'
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder forbiddenSys = sys' `Set.intersection` sysLenv
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder unless (Set.null forbiddenSys)
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder $ plain_error () (
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder "attempt to hide the following symbols from the local environment:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc forbiddenSys "") pos
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder mor1 <- cogenerated_sign lid1 sys' sigma1
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder mor1' <- map_morphism cid mor1
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder mor2 <- comp mor1' mor
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder return $ GMorphism cid (ExtSign (dom mor1) $ Set.fold (\ sy ->
de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder case Map.lookup sy $ symmap_of lid1 mor1 of
de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder Nothing -> id
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder Just sy1 -> Set.insert sy1) Set.empty sys1)
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder startSigId mor2 startMorId
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder G_logic_projection (Logic_code _ _ _ pos1) ->
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder fatal_error "no analysis of logic projections yet" pos1
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian MaederanaRestriction :: LogicGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder -> Result (GMorphism, Maybe GMorphism)
78411227baa6b3c462c27cd0b8ec2f7ef318e961Christian MaederanaRestriction lg gSigma gSigma'@(G_sign lid0 sig0 _) opts restr =
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder if isStructured opts then return (ide gSigma, Nothing) else
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder case restr of
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder Hidden rstr pos -> do
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder mor <- foldM (anaRestr lg gSigma pos) (ide gSigma') rstr
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder return (mor, Nothing)
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder Revealed (G_symb_map_items_list lid1 sis) pos -> adjustPos pos $ do
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder (G_sign lid sigma _, _) <- gSigCoerce lg gSigma (Logic lid1)
78411227baa6b3c462c27cd0b8ec2f7ef318e961Christian Maeder sigma0 <- coerceSign lid lid1 "reveal1" sigma
78411227baa6b3c462c27cd0b8ec2f7ef318e961Christian Maeder sigma1 <- coerceSign lid0 lid1 "reveal2" sig0
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder let sys = ext_sym_of lid1 sigma0 -- local env
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder sys' = ext_sym_of lid1 sigma1 -- "big" signature
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder rmap <- stat_symb_map_items lid1 (plainSign sigma1) Nothing sis
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder [sy | sy <- Set.toList sys', rsy <-
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder Map.keys rmap, matches lid1 sy rsy]
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder {- domain of rmap intersected with sys'
78411227baa6b3c462c27cd0b8ec2f7ef318e961Christian Maeder rmap is checked by ext_induced_from_morphism below -}
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder mor1 <- ext_generated_sign lid1 (sys `Set.union` sys'') sigma1
e143a5fe284b80280b0465ab5f41161f305ea257Till Mossakowski let extsig1 = makeExtSign lid1 $ dom mor1
6892075087077b9a2f9baa1663be4afcee2e7254Christian Maeder mor2 <- ext_induced_from_morphism lid1 rmap extsig1
78411227baa6b3c462c27cd0b8ec2f7ef318e961Christian Maeder return (gEmbed2 (G_sign lid1 extsig1 startSigId)
78411227baa6b3c462c27cd0b8ec2f7ef318e961Christian Maeder $ G_morphism lid1 mor1 startMorId
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder , Just $ gEmbed $ mkG_morphism lid1 mor2)
953127f27b7854580057a92e8269fd7a8716a800Christian MaederpartitionGmaps :: [G_mapping] -> ([G_mapping], [G_mapping])
953127f27b7854580057a92e8269fd7a8716a800Christian MaederpartitionGmaps l = let
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder (hs, rs) = span (\ sm -> case sm of
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder G_symb_map _ -> True
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder G_logic_translation _ -> False) $ reverse l
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder in (reverse rs, reverse hs)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederanaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder -> [G_mapping] -> Result G_morphism
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian MaederanaGmaps lg opts pos psig@(G_sign lidP sigmaP _) asig@(G_sign lidA sigmaA _)
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder gsis = adjustPos pos $ if isStructured opts
f8fe1f095d5b7fd96bde0784289b001446e60d0bChristian Maeder then return $ mkG_morphism lidP $ ext_ide sigmaP
f8fe1f095d5b7fd96bde0784289b001446e60d0bChristian Maeder else if null gsis then do
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder (G_sign lidP' sigmaP' _, _) <- gSigCoerce lg psig (Logic lidA)
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder sigmaA' <- coerceSign lidA lidP' "anaGmaps" sigmaA
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder fmap (mkG_morphism lidP') $
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder ext_induced_from_to_morphism lidP' Map.empty sigmaP' sigmaA'
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder cl <- lookupCurrentLogic "anaGmaps" lg
f8fe1f095d5b7fd96bde0784289b001446e60d0bChristian Maeder G_symb_map_items_list lid sis <- homogenizeGM cl gsis
ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder (G_sign lidP' sigmaP'' _, _) <- gSigCoerce lg psig (Logic lid)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder sigmaP' <- coerceSign lidP' lid "anaGmaps1" sigmaP''
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder (G_sign lidA' sigmaA'' _, _) <- gSigCoerce lg asig (Logic lid)
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder sigmaA' <- coerceSign lidA' lid "anaGmaps2" sigmaA''
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder rmap <- stat_symb_map_items lid (plainSign sigmaP')
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder (Just $ plainSign sigmaA') sis
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder fmap (mkG_morphism lid)
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder $ ext_induced_from_to_morphism lid rmap sigmaP' sigmaA'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let symI = sym_of lidP sigmaI'
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder symmap_mor = symmap_of lidP mor
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- are symbols of the imports left untouched?
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder if Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder then return ()
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder else plain_error () "Fitting morphism must not affect import" pos
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder -- does not work
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder -- also output symbols that are affected
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaFitArg :: LogicGraph -> LibEnv -> LibName -> DGraph -> IRI -> MaybeNode
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder -> NodeSig -> HetcatsOpts -> NodeName -> ExpOverrides -> FIT_ARG
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder -> Result (FIT_ARG, DGraph, (G_morphism, NodeSig))
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaFitArg lg libEnv ln dg spname nsigI nsigP@(NodeSig nP gsigmaP) opts name eo fv =
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder let ga = globalAnnos dg in
f8fe1f095d5b7fd96bde0784289b001446e60d0bChristian Maeder Fit_spec asp gsis pos -> do
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu (sp', nsigA, dg') <- anaSpec False True lg libEnv ln
7e347662208dee528a752c84bec8a59ff7bdff31mcodescu dg nsigI name opts eo (item asp) pos
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder (_, Comorphism aid) <-
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder logicUnion lg (getNodeLogic nsigP) (getNodeLogic nsigA)
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder let tl = Logic $ targetLogic aid
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder (nsigA'@(NodeSig nA' gsigA'), dg'') <- coerceNode lg dg' nsigA name tl
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder (gsigmaP', pmor) <- gSigCoerce lg gsigmaP tl
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder tmor <- gEmbedComorphism pmor gsigmaP
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder gmor <- anaGmaps lg opts pos gsigmaP' gsigA' gsis
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder eGmor <- comp tmor $ gEmbed gmor
c528d35d975276f43d31dec4db9b4e1bf08e1fe2Christian Maeder return ( Fit_spec (replaceAnnoted sp' asp) gsis pos
5fe604bfecb45b5cf2a5c1db003d39d670423476Christian Maeder , if nP == nA' && isInclusion eGmor then dg'' else
38e6a7281140deb96436868d396e1a0a3c934c2cChristian Maeder insLink dg'' eGmor globalThm
38e6a7281140deb96436868d396e1a0a3c934c2cChristian Maeder (DGLinkInst spname $ Fitted gsis) nP nA'
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder , (gmor, nsigA'))
b8bbe51da2883ef86242bccb3ee6744ba5922f08Christian Maeder Fit_view vn' afitargs pos -> do
b8bbe51da2883ef86242bccb3ee6744ba5922f08Christian Maeder vn <- expCurieR ga eo vn'
b8bbe51da2883ef86242bccb3ee6744ba5922f08Christian Maeder case lookupGlobalEnvDG vn dg of
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder Just (ViewOrStructEntry _ (ExtViewSig (NodeSig nSrc gsigmaS) mor
691ca0c9c7b21d58170be61c9c58899c5594fb2fChristian Maeder gs@(ExtGenSig (GenSig _ params _) target@(NodeSig nTar _))))
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder -> adjustPos pos $ do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder GMorphism cid _ _ morHom ind <- return mor
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let lid = targetLogic cid
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder pname = dgn_name $ labDG dg nP
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder gsigmaI = getMaybeSig nsigI
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian Maeder gsigmaIS <- gsigUnionMaybe lg True nsigI gsigmaS
1b2649da700cc49d0d49e463e3962c07770f6204Christian Maeder unless (isSubGsign lg gsigmaP gsigmaIS
1b2649da700cc49d0d49e463e3962c07770f6204Christian Maeder && isSubGsign lg gsigmaIS gsigmaP)
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder (plain_error ()
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ("Parameter does not match source of fittig view. "
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ "Parameter signature:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc gsigmaP
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder "\nSource signature of fitting view (united with import):\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc gsigmaIS "") pos)
8ecf5884934cad4efbcd60b92671b74e4aaeb62bChristian Maeder (dg4, iSrc) <- case nsigI of
8ecf5884934cad4efbcd60b92671b74e4aaeb62bChristian Maeder EmptyNode _ -> return (dg, nSrc)
8ecf5884934cad4efbcd60b92671b74e4aaeb62bChristian Maeder JustNode (NodeSig nI _) -> do
8ecf5884934cad4efbcd60b92671b74e4aaeb62bChristian Maeder inclI <- ginclusion lg gsigmaI gsigmaIS
8ecf5884934cad4efbcd60b92671b74e4aaeb62bChristian Maeder inclS <- ginclusion lg gsigmaS gsigmaIS
8ecf5884934cad4efbcd60b92671b74e4aaeb62bChristian Maeder let (NodeSig n' _, dg1) = insGSig dg (extName "View" name)
c5653d37b37dcc025ff6dd1eada95ae67116e699Christian Maeder {xpath = xpath pname} (DGFitView vn) gsigmaIS
8ecf5884934cad4efbcd60b92671b74e4aaeb62bChristian Maeder dg2 = insLink dg1 inclI globalDef
c5653d37b37dcc025ff6dd1eada95ae67116e699Christian Maeder (DGLinkFitViewImp vn) nI n'
13d0d9a3df7f3998f3c18c2fccbf2e3bbacbd4b5Christian Maeder return (insLink dg2 inclS globalDef
13d0d9a3df7f3998f3c18c2fccbf2e3bbacbd4b5Christian Maeder (DGLinkFitViewImp vn) nSrc n', n')
3eac470608bf2b665e810145d757622700d0cae5Christian Maeder if nP == iSrc then return dg4 else do
3eac470608bf2b665e810145d757622700d0cae5Christian Maeder gmor <- ginclusion lg gsigmaP gsigmaIS
3eac470608bf2b665e810145d757622700d0cae5Christian Maeder return $ insLink dg4 gmor globalThm (DGLinkFitView vn) nP iSrc
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder case (length afitargs, length params) of
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder -- the case without parameters leads to a simpler dg
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder (0, 0) -> return (fv, dg5, (G_morphism lid morHom ind, target))
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder -- now the case with parameters
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder (la, lp) | la == lp -> do
691ca0c9c7b21d58170be61c9c58899c5594fb2fChristian Maeder (ffitargs, dg', (gmor_f, _, ns@(NodeSig nA _))) <-
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu anaAllFitArgs lg libEnv opts eo ln dg5 (EmptyNode $ Logic lid)
c5653d37b37dcc025ff6dd1eada95ae67116e699Christian Maeder name vn gs afitargs
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder mor1 <- comp mor gmor_f
691ca0c9c7b21d58170be61c9c58899c5594fb2fChristian Maeder GMorphism cid1 _ _ theta _ <- return mor1
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let lid1 = targetLogic cid1
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder when (language_name (sourceLogic cid1) /= language_name lid1)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder $ fatal_error "heterogeneous fitting views not yet implemented"
13d0d9a3df7f3998f3c18c2fccbf2e3bbacbd4b5Christian Maeder let dg9 = insLink dg' gmor_f globalDef (DGLinkMorph vn) nTar nA
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder return (Fit_view vn ffitargs pos, dg9, (mkG_morphism lid1 theta, ns))
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder | otherwise -> instMismatchError spname lp la pos
076d5429ce08d87ebced34c308d41225e0d12cdeChristian Maeder _ -> notFoundError "view" vn
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaFitArgs :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> IRI
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa -> MaybeNode
cdcca7a63a02d363730ee1060e2500343da76afaChristian Maeder -> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)
cdcca7a63a02d363730ee1060e2500343da76afaChristian Maeder -> (NodeSig, FIT_ARG)
cdcca7a63a02d363730ee1060e2500343da76afaChristian Maeder -> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaFitArgs lg libEnv opts eo ln spname imps (fas', dg1, args, name') (nsig', fa) = do
cdcca7a63a02d363730ee1060e2500343da76afaChristian Maeder let n1 = inc name'
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (fa', dg', arg) <- anaFitArg lg libEnv ln dg1 spname imps nsig' opts n1 eo fa
cdcca7a63a02d363730ee1060e2500343da76afaChristian Maeder return (fa' : fas', dg', arg : args, n1)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaAllFitArgs :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> DGraph
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa -> MaybeNode
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -> NodeName -> IRI -> ExtGenSig -> [Annoted FIT_ARG]
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder -> Result ([Annoted FIT_ARG], DGraph, (GMorphism, G_sign, NodeSig))
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaAllFitArgs lg libEnv opts eo ln dg nsig name spname
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder gs@(ExtGenSig (GenSig imps params _) _)
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder afitargs = do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let fitargs = map item afitargs
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu (fitargs', dg', args, _) <- foldM (anaFitArgs lg libEnv opts eo ln spname imps)
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder ([], dg, [], extName "Actuals" name) (zip params fitargs)
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let actualargs = reverse args
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder (gsigma', morDelta) <- applyGS lg gs actualargs
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian Maeder gsigmaRes <- gsigUnionMaybe lg True nsig gsigma'
c5653d37b37dcc025ff6dd1eada95ae67116e699Christian Maeder let (ns, dg2) = insGSig dg' name (DGInst spname) gsigmaRes
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian Maeder dg3 <- foldM (parLink lg nsig (DGLinkInstArg spname) ns) dg2
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian Maeder $ map snd actualargs
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder return ( zipWith replaceAnnoted (reverse fitargs') afitargs, dg3
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder , (morDelta, gsigma', ns))
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian MaederparLink :: LogicGraph -> MaybeNode -> DGLinkOrigin -> NodeSig -> DGraph
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian Maeder -> NodeSig -> Result DGraph
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian MaederparLink lg nsig orig (NodeSig node gsigma') dg (NodeSig nA_i sigA_i) =
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian Maeder JustNode (NodeSig nI _) | nI == nA_i -> return dg
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian Maeder -- actual parameter will be included via import
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian Maeder incl <- ginclusion lg sigA_i gsigma'
1d10e9a6a3b03c7aa4306ff936ccaeacf474059aChristian Maeder return $ insLink dg incl globalDef orig nA_i node
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder{- Extension of signature morphisms (for instantitations)
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maederfirst some auxiliary functions -}
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaedermapID :: Map.Map Id (Set.Set Id) -> Id -> Result Id
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaedermapID idmap i@(Id toks comps pos1) =
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder case Map.lookup i idmap of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> do
0dcb86310998e097d3b15608f980f0a89a11a322Christian Maeder compsnew <- mapM (mapID idmap) comps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (Id toks compsnew pos1)
e2e17b0b9cfa80cd17495911be5572e420806611Christian Maeder Just ids -> case Set.toList ids of
e2e17b0b9cfa80cd17495911be5572e420806611Christian Maeder [] -> return i
e2e17b0b9cfa80cd17495911be5572e420806611Christian Maeder [h] -> return h
e2e17b0b9cfa80cd17495911be5572e420806611Christian Maeder _ -> plain_error i
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ("Identifier component " ++ showId i
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder " can be mapped in various ways:\n"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ showDoc ids "") $ getRange i
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder -> Result (EndoMap Id) -> Result (EndoMap Id)
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaederextID1 idmap i@(Id toks comps pos1) m = do
0dcb86310998e097d3b15608f980f0a89a11a322Christian Maeder compsnew <- mapM (mapID idmap) comps
0dcb86310998e097d3b15608f980f0a89a11a322Christian Maeder return $ if comps == compsnew then m1 else
0dcb86310998e097d3b15608f980f0a89a11a322Christian Maeder Map.insert i (Id toks compsnew pos1) m1
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederextID :: Set.Set Id -> Map.Map Id (Set.Set Id) -> Result (EndoMap Id)
3476beb5baf84bef7cc7d627b130de9d48700399Christian MaederextID ids idmap = Set.fold (extID1 idmap) (return Map.empty) ids
87ad371ce86a15cd4424f59fa2fb8393f496cca4Mihai CodescuextendMorphism :: Bool -- ^ check sharing (False for lambda expressions)
87ad371ce86a15cd4424f59fa2fb8393f496cca4Mihai Codescu -> G_sign -- ^ formal parameter
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -> G_sign -- ^ body
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -> G_sign -- ^ actual parameter
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -> G_morphism -- ^ fitting morphism
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder -> Result (G_sign, G_morphism)
87ad371ce86a15cd4424f59fa2fb8393f496cca4Mihai CodescuextendMorphism sharing (G_sign lid sigmaP _) (G_sign lidB sigmaB1 _)
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder (G_sign lidA sigmaA1 _) (G_morphism lidM fittingMor1 _) = do
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder -- for now, only homogeneous instantiations....
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder sigmaB@(ExtSign _ sysB) <-
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder coerceSign lidB lid "Extension of symbol map1" sigmaB1
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder sigmaA <- coerceSign lidA lid "Extension of symbol map2" sigmaA1
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder fittingMor <- coerceMorphism lidM lid "Extension of symbol map3" fittingMor1
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder let symsP = ext_sym_of lid sigmaP
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder symsB = ext_sym_of lid sigmaB
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder idsB = Set.map (sym_name lid) symsB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski h = symmap_of lid fittingMor
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder symbMapToRawSymbMap = Map.foldWithKey
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder (on Map.insert $ symbol_to_raw lid) Map.empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski rh = symbMapToRawSymbMap h
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder idh = Map.foldWithKey (on setInsert $ sym_name lid) Map.empty h
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder idhExt <- extID idsB idh
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder let rIdExt = Map.foldWithKey (on Map.insert $ id_to_raw lid) Map.empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski r = rh `Map.union` rIdExt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- do we need combining function catching the clashes???
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder mor <- ext_induced_from_morphism lid r sigmaB
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let hmor = symmap_of lid mor
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder sigmaAD = ExtSign (cod mor) $ Set.map (\ sy ->
3cb09c6460a2262e392c759e363bf645f913a47aChristian Maeder sigma <- ext_signature_union lid sigmaA sigmaAD
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let illShared = (ext_sym_of lid sigmaA `Set.intersection`
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ext_sym_of lid sigmaAD )
152c178f9f9969ce729361a5c61aa4ff2c9ed840Christian Maeder Set.\\ imageSet h symsP
2641573964f34ef1b269cc89e8b8608dfc122959Christian Maeder unless (Set.null illShared || not sharing)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder $ plain_error () ("Symbols shared between actual parameter and body"
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder ++ "\nmust be in formal parameter:\n"
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder ++ showDoc illShared "") nullRange
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder let myKernel = Set.fromDistinctAscList . comb1 . Map.toList
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian Maeder comb1 [] = []
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder comb1 (p : qs) =
f9690de9acb57e279b8ad5792d71b48ffbb807e7Christian Maeder comb2 p qs [] ++ comb1 qs
f9690de9acb57e279b8ad5792d71b48ffbb807e7Christian Maeder comb2 _ [] rs = rs
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder comb2 p@(a, b) ((c, d) : qs) rs =
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder comb2 p qs $ if b == d then (a, c) : rs else rs
ed20c3b1e992d174a2cbb2077e61817527f8e061Christian Maeder newIdentifications = myKernel hmor Set.\\ myKernel h
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder unless (Set.null newIdentifications)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder $ warning () (
6010f37233a15cb25960c86afaa4a23bbaa6a86cChristian Maeder "Fitting morphism may lead to forbidden identifications:\n"
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder ++ showDoc newIdentifications "") nullRange
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder incl <- ext_inclusion lid sigmaAD sigma
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder mor1 <- comp mor incl
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder return (G_sign lid sigma startSigId, mkG_morphism lid mor1)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederapplyGS :: LogicGraph -> ExtGenSig -> [(G_morphism, NodeSig)]
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder -> Result (G_sign, GMorphism)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederapplyGS lg (ExtGenSig (GenSig nsigI _ gsigmaP) nsigB) args = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let mor_i = map fst args
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaA_i = map (getSig . snd) args
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder gsigmaB = getSig nsigB
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder gsigmaA@(G_sign lidA _ _) <- gsigManyUnion lg gsigmaA_i
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder (Comorphism bid, Comorphism uid) <-
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder logicUnion lg (getNodeLogic nsigB) (Logic lidA)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder let cl = Logic $ targetLogic uid
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder G_morphism lidG mor0 _ <- case nsigI of
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder EmptyNode _ -> homogeneousMorManyUnion mor_i
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder JustNode (NodeSig _ gsigmaI) -> do
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder (G_sign lidI sigmaI _, _) <- gSigCoerce lg gsigmaI (Logic lidA)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder let idI = ext_ide sigmaI
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder homogeneousMorManyUnion $ mkG_morphism lidI idI : mor_i
ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder (gsigmaP', _) <- gSigCoerce lg (getMaybeSig gsigmaP) cl
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder (gsigmaB', _) <- gSigCoerce lg gsigmaB cl
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder (gsigmaA', Comorphism aid) <- gSigCoerce lg gsigmaA cl
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder mor1 <- coerceMorphism lidG (sourceLogic aid) "applyGS" mor0
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder mor2 <- map_morphism aid mor1
2641573964f34ef1b269cc89e8b8608dfc122959Christian Maeder (gsig, G_morphism gid mor3 mId) <- extendMorphism True gsigmaP' gsigmaB'
2641573964f34ef1b269cc89e8b8608dfc122959Christian Maeder gsigmaA' $ G_morphism (targetLogic aid) mor2 startMorId
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder case gsigmaB of
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder G_sign lidB sigB indB -> do
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder sigB' <- coerceSign lidB (sourceLogic bid) "applyGS2" sigB
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder mor4 <- coerceMorphism gid (targetLogic bid) "applyGS3" mor3
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder return (gsig, GMorphism bid sigB' indB mor4 mId)
953127f27b7854580057a92e8269fd7a8716a800Christian MaederhomogenizeGM :: AnyLogic -> [G_mapping] -> Result G_symb_map_items_list
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian MaederhomogenizeGM (Logic lid) =
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder foldM homogenize1 (G_symb_map_items_list lid [])
6892075087077b9a2f9baa1663be4afcee2e7254Christian Maeder homogenize1 (G_symb_map_items_list lid2 sis) sm = case sm of
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder G_symb_map (G_symb_map_items_list lid1 sis1) -> do
60dcc32017afaac58218b41feaea23ad4c7a022cChristian Maeder sis1' <- coerceSymbMapItemsList lid1 lid2 "homogenizeGM" sis1
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder return $ G_symb_map_items_list lid2 $ sis ++ sis1'
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder G_logic_translation lc ->
6892075087077b9a2f9baa1663be4afcee2e7254Christian Maeder fail $ "translation not supported by " ++ showDoc lc ""
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian MaedergetSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian MaedergetSpecAnnos pos a = do
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder let sannos = filter isSemanticAnno $ l_annos a
2f5ff26a09d68be0b09eec62126c84637d102f4cMarcel Zirbel (sanno1, conflict, impliesA) = case sannos of
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder f@(Semantic_anno anno1 _) : r -> (case anno1 of
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder SA_cons -> Cons
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder SA_def -> Def
dbbcdfeafa68c87e0b2be0096788844e2be08345Christian Maeder SA_mono -> Mono
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder _ -> None, any (/= f) r,
2f5ff26a09d68be0b09eec62126c84637d102f4cMarcel Zirbel anno1 == SA_implies || anno1 == SA_implied)
2f5ff26a09d68be0b09eec62126c84637d102f4cMarcel Zirbel _ -> (None, False, False)
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder when conflict $ plain_error () "Conflicting semantic annotations" pos
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder return (sanno1, impliesA)
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder-- only consider addSyms for the first spec
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaExtension :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> Range
6b00a9239fe7c804524099ca3d25f4ffc6079ceeChristian Maeder -> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder -> (NodeName, Annoted SPEC)
6b00a9239fe7c804524099ca3d25f4ffc6079ceeChristian Maeder -> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescuanaExtension lg libEnv opts eo ln pos (sps', nsig', dg', conser, addSyms) (name', asp')
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder (sanno1, impliesA) <- getSpecAnnos pos asp'
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder -- attach conservativity to definition link
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder let sp = item asp'
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (sp1', nsig1@(NodeSig n1 sig1), dg1) <- anaSpecTop (max conser sanno1)
42e78fd3454812d4f98b06154fdabc5ec3488718mcodescu addSyms lg libEnv ln dg' nsig' name' opts eo sp $ getRange sp
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder dg2 <- if impliesA then case nsig' of
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder JustNode (NodeSig n' sig') -> do
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder -- is the extension going between real nodes?
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder unless (isHomSubGsign sig1 sig') $ plain_error ()
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder "Signature must not be extended in presence of %implies" pos
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder -- insert a theorem link according to p. 319 of the CASL Reference Manual
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder return $ insLink dg1 (ide sig1) globalThm DGImpliesLink n1 n'
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder _ -> return dg1
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder else return dg1
6b00a9239fe7c804524099ca3d25f4ffc6079ceeChristian Maeder return (sp1' : sps', JustNode nsig1, dg2, None, True)
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder-- BEGIN CURIE expansion
b8bbe51da2883ef86242bccb3ee6744ba5922f08Christian MaederexpCurieR :: GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
b8bbe51da2883ef86242bccb3ee6744ba5922f08Christian MaederexpCurieR ga eo i = maybe (prefixErrorIRI i) return $ expCurie ga eo i
f8065e835104ae5eaa148e9b37a81e768990724bEugen KuksaexpCurie :: GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI
f8065e835104ae5eaa148e9b37a81e768990724bEugen KuksaexpCurie ga eo i =
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa let pm = prefix_map ga
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder in case Map.lookup i eo of
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa Nothing -> expandCurie pm i
329f09824e0b9202d1327e52358912eddac8ad38Christian Maeder Just path -> expandCurieByPath path i
329f09824e0b9202d1327e52358912eddac8ad38Christian MaederexpandCurieByPath :: FilePath -> IRI -> Maybe IRI
be7add16c3f4e230929bcb948a67a710c6a4d222Christian MaederexpandCurieByPath path i = case parseIRIReference $ path ++ "?" of
c5b4efccb69bee7186a47bc436d8d1895da80abbChristian Maeder Nothing -> Nothing
329f09824e0b9202d1327e52358912eddac8ad38Christian Maeder Just p -> expandCurie (Map.singleton "" p) i
f8065e835104ae5eaa148e9b37a81e768990724bEugen KuksaprefixErrorIRI :: IRI -> Result a
f8065e835104ae5eaa148e9b37a81e768990724bEugen KuksaprefixErrorIRI i = fatal_error ("No prefix found for CURIE " ++
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa iriToStringUnsecure i ++ " or expansion does not yield a valid IRI.")
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder-- END CURIE expansion