AnalysisStructured.hs revision 60dcc32017afaac58218b41feaea23ad4c7a022c
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederModule : $Header$
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian MaederDescription : static analysis of heterogeneous structured specifications
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003-2006
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)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiStatic analysis of CASL (heterogeneous) structured specifications
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski Follows the verfication semantic rules in Chap. IV:4.7
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski of the CASL Reference Manual.
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , anaSublogic
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder , getSpecAnnos
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder , isStructured
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder , anaRenaming
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder , anaRestriction
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder , partitionGmaps
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder , homogenizeGM
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder , extendMorphism
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
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)
be3f5e3e69900ececafea5b010a8400f26af5362Christian MaederinsGTheory dg name orig (G_theory lid 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
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder nth = G_theory lid 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
278af20bd154d99e884bdf8c66d35d36699643c9Christian 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
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian 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
6505786996adb0239e26bb669ea579d630fa46a4Christian MaederanaSublogic :: HetcatsOpts -> Logic_name -> LibName -> DGraph -> LibEnv
aeb4e74b8b3328d8ea15512ec4e1e1b8d0919f01Christian Maeder -> LogicGraph
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder -> Result (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
6505786996adb0239e26bb669ea579d630fa46a4Christian MaederanaSublogic _opts itm@(Logic_name lt ms mt) ln dg libenv lG = do
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder logN@(Logic lid) <- lookupLogic "" (tokStr lt) lG
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder mgs <- case ms of
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Nothing -> return Nothing
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder Just subL -> do
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder let s = tokStr subL
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder case lookup s $ map (\ l -> (sublogicName l, l)) $ all_sublogics lid 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
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder let ssp = tokStr 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) })
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder -> MaybeNode -> NodeName -> HetcatsOpts -> SPEC
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder -> Result (SPEC, NodeSig, DGraph)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaSpecTop conser addSyms lg ln dg nsig name opts sp =
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
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder Spec_inst _ _ _ -> True
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder Group _ _ -> True -- in this case we recurse
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder then anaSpecAux conser addSyms lg ln dg nsig name opts sp else do
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder let provenThmLink =
bd986fa9d0f451b8166efdb9027c153d101aa65bChristian Maeder ThmLink $ Proven (DGRule "static analysis") emptyProofBasis
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (rsp, ns, rdg) <- anaSpec addSyms lg ln dg nsig name opts sp
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder ndg <- createConsLink provenThmLink conser lg rdg nsig ns SeeTarget
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder return (rsp, ns, ndg)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaFreeOrCofreeSpec :: Bool -> LogicGraph -> HetcatsOpts -> LibName -> DGraph
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder -> MaybeNode -> NodeName -> FreeOrCofree -> Annoted SPEC -> Range
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder -> Result (Annoted SPEC, NodeSig, DGraph)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaFreeOrCofreeSpec addSyms lg opts ln dg nsig name dglType asp pos =
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder adjustPos pos $ do
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder (sp', NodeSig n' gsigma, dg') <-
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder anaSpec addSyms lg ln dg nsig (extName (show dglType) name) opts
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder let (ns@(NodeSig node _), dg2) =
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder insGSig dg' 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)
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder{- | analyze a SPEC. The Bool Parameter determines if incoming symbols shall
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maederbe ignored. The options are needed to check: shall only the structure be
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaSpec :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder -> HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, DGraph)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederanaSpec = anaSpecAux None
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaSpecAux :: Conservativity -> Bool -> LogicGraph -> LibName -> DGraph
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder -> MaybeNode -> NodeName -> HetcatsOpts -> SPEC
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder -> Result (SPEC, NodeSig, DGraph)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaSpecAux conser addSyms lg ln dg nsig name opts sp = case sp of
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder Basic_spec (G_basic_spec lid bspec) pos -> adjustPos pos $ do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let curLogic = Logic lid
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)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (getLibId 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"
9bbe44a0670a21990fcaf328661ef03a8efd9fecChristian Maeder diffSig <- case signatureDiff lid sigma_complete sig of
9bbe44a0670a21990fcaf328661ef03a8efd9fecChristian Maeder Result _ (Just ds) -> return ds
9bbe44a0670a21990fcaf328661ef03a8efd9fecChristian Maeder _ -> warning sigma_complete
9bbe44a0670a21990fcaf328661ef03a8efd9fecChristian Maeder "signature difference could not be computed using full one" pos
3f9fabb8ac5cfd9234431ecf19b51ff3e985595aChristian Maeder let gsysd = Set.map (G_symbol lid) sysd
83259a366597461d24e6b9236a8a33e201798e4dChristian Maeder (ns, dg') = insGTheory dg0 name
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder (DGBasicSpec (Just $ G_basic_spec lid bspec')
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder (G_sign lid (mkExtSign diffSig) startSigId) gsysd)
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder $ G_theory lid (ExtSign sigma_complete
c30cfe2a6ab063befdfb47449bc286caee6d8fc3Christian Maeder (if addSyms then Set.union sys sysd else sysd)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz $ symset_of lid sigma_complete)
eaf02872307b4578250fbeb9dc371cac177b0924Ewaryst Schulz startSigId (toThSens ax) startThId
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder 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
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder let (ns, dg') = insGSig dg name DGEmpty (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
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder (sp1', ns'@(NodeSig n' gsigma), dg') <-
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder anaSpec addSyms lg ln dg nsig (extName "Translation" name) opts sp1
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 ()
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder ("nothing renamed by:\n" ++ showDoc ren "") $ getRange ren
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder (fs, dgf) <- if isIdentity mor && isInternal name then return (ns', dg')
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder let (ns@(NodeSig node _), dg'') =
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder insGSig dg' name (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)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Reduction asp restr ->
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski do let sp1 = item asp
b4a750119742b015a815e6f370a7d58e7a4de634Christian Maeder rname = extName "Restriction" name
b4a750119742b015a815e6f370a7d58e7a4de634Christian Maeder (sp1', ns0, dg0) <- anaSpec addSyms lg ln dg nsig rname opts sp1
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)
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder Union asps pos -> do
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (newAsps, _, ns, dg') <- adjustPos pos $ anaUnion addSyms lg ln dg nsig
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder name opts asps
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder return (Union 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
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (sps', nsig1', dg1, _, _) <- foldM (anaExtension lg opts 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
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder name Free asp poss
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder return (Free_spec nasp poss, nsig', dg')
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder Cofree_spec asp poss -> do
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg opts ln dg nsig
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder name Cofree asp poss
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder return (Cofree_spec nasp poss, nsig', dg')
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder Local_spec asp asp' poss -> adjustPos poss $ do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let sp1 = item asp
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski sp1' = item asp'
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder lname = extName "Local" name
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder (sp2, nsig'@(NodeSig _ gsig1), dg') <-
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder anaSpec False lg ln dg nsig (extName "Spec" lname) opts sp1
f8c8c3e92d02616c7a2994b3aa62a541870796d8Christian Maeder (sp2', NodeSig n'' gsig2@(G_sign lid2 sigma2 _), dg'') <- anaSpec False lg
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder ln dg' (JustNode nsig') (extName "Within" lname) opts sp1'
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
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder l = getLogic nsig
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski -- analyse spec with empty local env
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (sp', NodeSig n' gsigma', dg') <- anaSpec False lg ln dg
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (EmptyNode l) (extName "Closed" name) opts sp1
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder gsigma2 <- gsigUnionMaybe lg 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
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder (sp', ns', dg') <- anaSpec addSyms newLG ln dg newNSig qname opts
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') <-
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder anaSpecTop conser addSyms lg ln dg nsig name opts (item asp)
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder return (Group (replaceAnnoted sp' asp) pos, nsig', dg')
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder Spec_inst spname afitargs pos0 -> let
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder pos = if null afitargs then tokPos spname else pos0
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder in 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,
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder EmptyNode _ | isInternal name -> 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
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder gsigma <- gsigUnionMaybe lg 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))) <-
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder anaAllFitArgs lg opts 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
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder return (Spec_inst spname ffitargs pos, ns, dg5)
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder | otherwise -> instMismatchError spname lp la pos
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder _ -> notFoundError "Structured specification" spname pos
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
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
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder (sp1', ns', dg') <- anaSpec False (setCurLogic (language_name lidD) lg)
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder ln dg (EmptyNode lD) dname opts sp1
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
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder gsigma2 <- gsigUnion lg (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) <-
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder anaSpec addSyms lg ln udg (JustNode usig) name opts sp2
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder return (Data lD lP
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted sp1' asp1)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (replaceAnnoted sp2' asp2)
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder pos, nsig3, udg3)
fe9fabab6e959e383a746711b078c8fddbd5e553Christian MaederinstMismatchError :: SIMPLE_ID -> Int -> Int -> Range -> Result a
fe9fabab6e959e383a746711b078c8fddbd5e553Christian MaederinstMismatchError spname lp la = fatal_error $ tokStr spname ++ " expects "
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder ++ show lp ++ " arguments" ++ " but was given " ++ show la
fe9fabab6e959e383a746711b078c8fddbd5e553Christian MaedernotFoundError :: String -> SIMPLE_ID -> Range -> Result a
fe9fabab6e959e383a746711b078c8fddbd5e553Christian MaedernotFoundError str sid = fatal_error $ str ++ " " ++ tokStr sid ++ " not found"
301797af7ed152a6cce563a3303c9fbc4ac16180Christian MaedergsigUnionMaybe :: LogicGraph -> MaybeNode -> G_sign -> Result G_sign
301797af7ed152a6cce563a3303c9fbc4ac16180Christian MaedergsigUnionMaybe lg mn gsig = case mn of
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder EmptyNode _ -> return gsig
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder JustNode ns -> gsigUnion lg (getSig ns) gsig
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaUnion :: Bool -> LogicGraph -> LibName -> DGraph -> MaybeNode -> NodeName
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder -> HetcatsOpts -> [Annoted SPEC]
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaUnion addSyms lg ln dg nsig name opts asps = 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
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (sp1, nsig', dg1) <- anaSpec addSyms lg ln dg' nsig n1 opts 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')
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder let (ns@(NodeSig node _), dg2) = insGSig dg' name 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)
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) ->
627ed7abdbae641636a2d0f2510c0d450f5ee915Christian Maeder let adj1 = adjustPos $ if pos1 == nullRange then pos else pos1
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder G_sign srcLid srcSig ind <- return (cod gmor)
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder c <- case tok of
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder Just ctok -> lookupComorphism (tokStr ctok) lg
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski Nothing -> case tar of
53ea24e19dbd4ca72fd75ab3a3105dc9f99e4f81Christian Maeder Just (Logic_name l _ _) ->
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder lookupLogic "with logic: " (tokStr l) lg
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder >>= logicInclusion lg (Logic srcLid)
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski Nothing -> fail "with logic: cannot determine comorphism"
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder checkSrcOrTarLogic True c src
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder checkSrcOrTarLogic False c tar
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder mor1 <- gEmbedComorphism c (G_sign srcLid srcSig ind)
2701083ab584807a8dec6f2c8bc03237a25d9809Christian Maeder comp gmor mor1
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian MaedercheckSrcOrTarLogic :: Bool -> AnyComorphism -> Maybe Logic_name -> Result ()
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian MaedercheckSrcOrTarLogic b (Comorphism cid) ml = case ml of
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder Nothing -> return ()
53ea24e19dbd4ca72fd75ab3a3105dc9f99e4f81Christian Maeder Just (Logic_name l _ _) -> let s = tokStr l in
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 "
29d0d2c24fe5297b0ab3d48af9f96ce10059b610Christian Maeder ++ language_name cid) (tokPos l)
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
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaFitArg :: LogicGraph -> LibName -> DGraph -> SIMPLE_ID -> MaybeNode
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder -> NodeSig -> HetcatsOpts -> NodeName -> FIT_ARG
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder -> Result (FIT_ARG, DGraph, (G_morphism, NodeSig))
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaFitArg lg ln dg spname nsigI nsigP@(NodeSig nP gsigmaP) opts name fv =
f8fe1f095d5b7fd96bde0784289b001446e60d0bChristian Maeder Fit_spec asp gsis pos -> do
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (sp', nsigA, dg') <- anaSpec False lg ln dg nsigI name opts (item asp)
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'))
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder Fit_view vn afitargs pos -> 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
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder gsigmaIS <- gsigUnionMaybe lg 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 _))) <-
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder anaAllFitArgs lg opts 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
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder _ -> notFoundError "View" vn pos
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaFitArgs :: LogicGraph -> HetcatsOpts -> LibName -> SIMPLE_ID -> 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)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaFitArgs lg opts ln spname imps (fas', dg1, args, name') (nsig', fa) = do
cdcca7a63a02d363730ee1060e2500343da76afaChristian Maeder let n1 = inc name'
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (fa', dg', arg) <- anaFitArg lg ln dg1 spname imps nsig' opts n1 fa
cdcca7a63a02d363730ee1060e2500343da76afaChristian Maeder return (fa' : fas', dg', arg : args, n1)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaAllFitArgs :: LogicGraph -> HetcatsOpts -> LibName -> DGraph -> MaybeNode
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder -> NodeName -> SIMPLE_ID -> ExtGenSig -> [Annoted FIT_ARG]
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder -> Result ([Annoted FIT_ARG], DGraph, (GMorphism, G_sign, NodeSig))
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaAllFitArgs lg opts ln dg nsig name spname
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder gs@(ExtGenSig (GenSig imps params _) _)
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder afitargs = do
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let fitargs = map item afitargs
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (fitargs', dg', args, _) <- foldM (anaFitArgs lg opts 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
301797af7ed152a6cce563a3303c9fbc4ac16180Christian Maeder gsigmaRes <- gsigUnionMaybe lg 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
6157bf81d295795067c177aa870fedff83cbe750Christian MaederextendMorphism :: 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)
6157bf81d295795067c177aa870fedff83cbe750Christian MaederextendMorphism (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
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski symbMapToRawSymbMap =
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder Map.foldWithKey (\ sy1 sy2 -> Map.insert (symbol_to_raw lid sy1)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (symbol_to_raw lid sy2))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski rh = symbMapToRawSymbMap h
152c178f9f9969ce729361a5c61aa4ff2c9ed840Christian Maeder (\ sy1 sy2 -> setInsert (sym_name lid sy1) (sym_name lid sy2))
3476beb5baf84bef7cc7d627b130de9d48700399Christian Maeder idhExt <- extID idsB idh
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder let rIdExt = Map.foldWithKey (\ id1 id2 -> Map.insert
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder (id_to_raw lid id1) (id_to_raw lid id2))
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
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder unless (Set.null illShared)
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
67e7a4ffd0ba22b6ba7f7fd7876f389b2e89df70Christian Maeder (gsig, G_morphism gid mor3 mId) <- extendMorphism gsigmaP' gsigmaB' gsigmaA' $
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder 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
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederhomogenizeGM (Logic lid) gsis =
a80f2865b6b40a922bcccfce0cb0d047edc33e3aChristian Maeder foldM homogenize1 (G_symb_map_items_list lid []) gsis
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 ""
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder-- | check if structured analysis should be performed
7297175957c5ad3c0498032190b1dee9ec5fb873Christian MaederisStructured :: HetcatsOpts -> Bool
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederisStructured a = case analysis a of
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder Structured -> True
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian MaedergetSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian MaedergetSpecAnnos pos a = do
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder let sannos = filter isSemanticAnno $ l_annos a
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder (sanno1, conflict, impliedA, 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,
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder anno1 == SA_implied, anno1 == SA_implies)
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder _ -> (None, False, False, False)
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder when conflict $ plain_error () "Conflicting semantic annotations" pos
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder when impliedA $ plain_error ()
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder "Annotation %implied should come after a BASIC-ITEM" pos
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder return (sanno1, impliesA)
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder-- only consider addSyms for the first spec
b4a750119742b015a815e6f370a7d58e7a4de634Christian MaederanaExtension :: LogicGraph -> HetcatsOpts -> LibName -> Range
6b00a9239fe7c804524099ca3d25f4ffc6079ceeChristian Maeder -> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder -> (NodeName, Annoted SPEC)
6b00a9239fe7c804524099ca3d25f4ffc6079ceeChristian Maeder -> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederanaExtension lg opts ln pos (sps', nsig', dg', conser, addSyms) (name', asp')
4a8f990902448d0562fbe1a98ce685ddbd531d38Christian Maeder (sanno1, impliesA) <- getSpecAnnos pos asp'
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder -- attach conservativity to definition link
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (sp1', nsig1@(NodeSig n1 sig1), dg1) <- anaSpecTop (max conser sanno1)
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder addSyms lg ln dg' nsig' name' opts (item asp')
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)