FromXmlUtils.hs revision feeab95fdf7ec92bcce607c104d9dc98e0e6ea90
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : theory datastructure for development graphs
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Christian Maeder, Simon Ulbricht, Uni Bremen 20011
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : maeder@dfki.de
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable(Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedertheory datastructure for development graphs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport qualified Data.Set as Set
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowskiimport qualified Data.Map as Map
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederdata BasicExtResponse = Failure Bool -- True means fatal (give up)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Success G_theory Int (Set.Set G_symbol) Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiextendByBasicSpec :: GlobalAnnos -> String -> G_theory
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> (BasicExtResponse, String)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederextendByBasicSpec ga str
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder gt@(G_theory lid syn eSig@(ExtSign sign syms) si sens _)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder = let tstr = trimLeft str in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if null tstr then (Success gt 0 Set.empty True, "") else
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case basicSpecParser Nothing lid of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> (Failure True, "missing basic spec parser")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just p -> case basic_analysis lid of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> (Failure True, "missing basic analysis")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just f -> case runParser (p Map.empty << eof) (emptyAnnos ()) "" tstr of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Left err -> (Failure False, show err)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Right bs -> let
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Result ds res = f (bs, sign, ga)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in case res of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just (_, ExtSign sign2 syms2, sens2) | not (hasErrors ds) ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let sameSig = sign2 == sign
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski finExtSign = ExtSign sign2 $ Set.union syms syms2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Success (G_theory lid syn (if sameSig then eSig else finExtSign)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (if sameSig then si else startSigId)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (joinSens (toThSens sens2) sens) startThId)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (length sens2)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Set.map (G_symbol lid) $ Set.difference syms2 syms)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , if sameSig then
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if null sens2 then "" else
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder show (vcat $ map (print_named lid) sens2)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> (Failure False, showRelDiags 1 ds)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskideleteHiddenSymbols :: String -> G_sign -> Result G_sign
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederdeleteHiddenSymbols syms gs@(G_sign lid (ExtSign sig _) _) = let
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder str = trimLeft syms in if null str then return gs else
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case parse_symb_items lid of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Nothing -> fail $ "no symbol parser for " ++ language_name lid
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Just sbpa -> case runParser (sepBy1 sbpa anComma << eof)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski (emptyAnnos ()) "" str of
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Left err -> fail $ show err
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Right sms -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder rm <- stat_symb_items lid sig sms
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let sym1 = symset_of lid sig
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sym2 = Set.filter (\ s -> any (matches lid s) rm) sym1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sig2 <- fmap dom $ cogenerated_sign lid sym2 sig
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder return $ G_sign lid (mkExtSign sig2) startSigId
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | reconstruct the morphism from symbols maps
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedergetMorphism :: G_sign
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -> String -- ^ the symbol mappings
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -> Result G_morphism
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedergetMorphism (G_sign lid (ExtSign sig _) _) syms =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder let str = trimLeft syms in
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder if null str then return $ mkG_morphism lid $ ide sig else
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case parse_symb_map_items lid of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Nothing -> fail $ "no symbol map parser for " ++ language_name lid
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just smpa -> case runParser (sepBy1 smpa anComma << eof)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (emptyAnnos ()) "" str of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Left err -> fail $ show err
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Right sms -> do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder rm <- stat_symb_map_items lid sig Nothing sms
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder fmap (mkG_morphism lid) $ induced_from_morphism lid rm sig
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- | get the gmorphism for a gmorphism name
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedertranslateByGName :: LogicGraph -> G_sign
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -> String -- ^ the name of the morphism
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder -> Result GMorphism
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertranslateByGName lg gsig gname =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let str = trim gname in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if null str then ginclusion lg gsig gsig else do
10a2cf8d9887524acde19d4ea59f8fea3a7f3258Till Mossakowski cmor <- lookupComorphism str lg
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski gEmbedComorphism cmor gsig
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | get the gmorphism for a gmorphism name with symbols maps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedergetGMorphism :: LogicGraph -> G_sign
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -> String -- ^ the name of the gmorphism
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -> String -- ^ the symbol mappings
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder -> Result GMorphism
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedergetGMorphism lg gsig gname syms = do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder gmor1 <- translateByGName lg gsig gname
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder gmor2 <- fmap gEmbed $ getMorphism (cod gmor1) syms
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder composeMorphisms gmor1 gmor2