0N/A{- |

1879N/AModule : ./Static/FromXmlUtils.hs

0N/ADescription : theory datastructure for development graphs

0N/ACopyright : (c) Christian Maeder, Simon Ulbricht, Uni Bremen 20011

0N/ALicense : GPLv2 or higher, see LICENSE.txt

0N/AMaintainer : maeder@dfki.de

0N/AStability : provisional

0N/APortability : non-portable(Logic)

0N/A

0N/Atheory datastructure for development graphs

0N/A-}

0N/Amodule Static.FromXmlUtils where

0N/A

0N/Aimport Static.GTheory

0N/A

0N/Aimport Logic.Prover

0N/Aimport Logic.Logic

0N/Aimport Logic.Grothendieck

1472N/A

1472N/Aimport Common.AnnoState

1472N/Aimport Common.Doc

0N/Aimport Common.ExtSign

0N/Aimport Common.GlobalAnnotations

0N/Aimport Common.Parsec

91N/Aimport Common.Result

0N/Aimport Common.Utils

0N/A

0N/Aimport Text.ParserCombinators.Parsec

0N/A

0N/Aimport qualified Data.Set as Set

1879N/Aimport qualified Data.Map as Map

0N/A

1879N/Adata BasicExtResponse = Failure Bool -- True means fatal (give up)

0N/A | Success G_theory Int (Set.Set G_symbol) Bool

1879N/A

1879N/AextendByBasicSpec :: GlobalAnnos -> String -> G_theory

1879N/A -> (BasicExtResponse, String)

1879N/AextendByBasicSpec ga str

1879N/A gt@(G_theory lid syn eSig@(ExtSign sign syms) si sens _)

1879N/A = let tstr = trimLeft str in

1879N/A if null tstr then (Success gt 0 Set.empty True, "") else

1879N/A case basicSpecParser Nothing lid of

1879N/A Nothing -> (Failure True, "missing basic spec parser")

1879N/A Just p -> case basic_analysis lid of

1879N/A Nothing -> (Failure True, "missing basic analysis")

1879N/A Just f -> case runParser (p Map.empty << eof) (emptyAnnos ()) "" tstr of

1879N/A Left err -> (Failure False, show err)

1879N/A Right bs -> let

1879N/A Result ds res = f (bs, sign, ga)

0N/A in case res of

0N/A Just (_, ExtSign sign2 syms2, sens2) | not (hasErrors ds) ->

1879N/A let sameSig = sign2 == sign

1879N/A finExtSign = ExtSign sign2 $ Set.union syms syms2

0N/A in

0N/A (Success (G_theory lid syn (if sameSig then eSig else finExtSign)

0N/A (if sameSig then si else startSigId)

1879N/A (joinSens (toThSens sens2) sens) startThId)

1879N/A (length sens2)

1879N/A (Set.map (G_symbol lid) $ Set.difference syms2 syms)

1879N/A sameSig

1879N/A , if sameSig then

0N/A if null sens2 then "" else

0N/A show (vcat $ map (print_named lid) sens2)

1879N/A else "")

0N/A _ -> (Failure False, showRelDiags 1 ds)

0N/A

0N/AdeleteHiddenSymbols :: String -> G_sign -> Result G_sign

0N/AdeleteHiddenSymbols syms gs@(G_sign lid (ExtSign sig _) _) = let

0N/A str = trimLeft syms in if null str then return gs else

1879N/A case parse_symb_items lid of

0N/A Nothing -> fail $ "no symbol parser for " ++ language_name lid

0N/A Just sbpa -> case runParser (sepBy1 sbpa anComma << eof)

0N/A (emptyAnnos ()) "" str of

0N/A Left err -> fail $ show err

0N/A Right sms -> do

0N/A rm <- stat_symb_items lid sig sms

1879N/A let sym1 = symset_of lid sig

0N/A sym2 = Set.filter (\ s -> any (matches lid s) rm) sym1

0N/A sig2 <- fmap dom $ cogenerated_sign lid sym2 sig

0N/A return $ G_sign lid (mkExtSign sig2) startSigId

1879N/A

1879N/A-- | reconstruct the morphism from symbols maps

0N/AgetMorphism :: G_sign

1879N/A -> String -- ^ the symbol mappings

0N/A -> Result G_morphism

1879N/AgetMorphism (G_sign lid (ExtSign sig _) _) syms =

1934N/A let str = trimLeft syms in

0N/A if null str then return $ mkG_morphism lid $ ide sig else

0N/A case parse_symb_map_items lid of

0N/A Nothing -> fail $ "no symbol map parser for " ++ language_name lid

659N/A Just smpa -> case runParser (sepBy1 smpa anComma << eof)

1934N/A (emptyAnnos ()) "" str of

1879N/A Left err -> fail $ show err

1879N/A Right sms -> do

1879N/A rm <- stat_symb_map_items lid sig Nothing sms

1879N/A fmap (mkG_morphism lid) $ induced_from_morphism lid rm sig

1879N/A

1879N/A-- | get the gmorphism for a gmorphism name

1879N/AtranslateByGName :: LogicGraph -> G_sign

1879N/A -> String -- ^ the name of the morphism

1879N/A -> Result GMorphism

1879N/AtranslateByGName lg gsig gname =

1879N/A let str = trim gname in

1879N/A if null str then ginclusion lg gsig gsig else do

0N/A cmor <- lookupComorphism str lg

0N/A gEmbedComorphism cmor gsig

0N/A

1879N/A-- | get the gmorphism for a gmorphism name with symbols maps

1879N/AgetGMorphism :: LogicGraph -> G_sign

1879N/A -> String -- ^ the name of the gmorphism

1879N/A -> String -- ^ the symbol mappings

1879N/A -> Result GMorphism

1879N/AgetGMorphism lg gsig gname syms = do

1879N/A gmor1 <- translateByGName lg gsig gname

1879N/A gmor2 <- fmap gEmbed $ getMorphism (cod gmor1) syms

0N/A composeMorphisms gmor1 gmor2

0N/A