content: {- |
  Module      :  ./Static/FromXmlUtils.hs
  Description :  theory datastructure for development graphs
  Copyright   :  (c) Christian Maeder, Simon Ulbricht, Uni Bremen 20011
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  theory datastructure for development graphs
  -}
  module Static.FromXmlUtils where
  
  import Static.GTheory
  
  import Logic.Prover
  import Logic.Logic
  import Logic.Grothendieck
  
  import Common.AnnoState
  import Common.Doc
  import Common.ExtSign
  import Common.GlobalAnnotations
  import Common.Parsec
  import Common.Result
  import Common.Utils
  
  import Text.ParserCombinators.Parsec
  
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  import qualified Control.Monad.Fail as Fail
  
  data BasicExtResponse = Failure Bool  -- True means fatal (give up)
    | Success G_theory Int (Set.Set G_symbol) Bool
  
  extendByBasicSpec :: GlobalAnnos -> String -> G_theory
    -> (BasicExtResponse, String)
  extendByBasicSpec ga str
    gt@(G_theory lid syn eSig@(ExtSign sign syms) si sens _)
    = let tstr = trimLeft str in
    if null tstr then (Success gt 0 Set.empty True, "") else
    case basicSpecParser Nothing lid of
      Nothing -> (Failure True, "missing basic spec parser")
      Just p -> case basic_analysis lid of
        Nothing -> (Failure True, "missing basic analysis")
        Just f -> case runParser (p Map.empty << eof) (emptyAnnos ()) "" tstr of
          Left err -> (Failure False, show err)
          Right bs -> let
            Result ds res = f (bs, sign, ga)
            in case res of
              Just (_, ExtSign sign2 syms2, sens2) | not (hasErrors ds) ->
                let sameSig = sign2 == sign
                    finExtSign = ExtSign sign2 $ Set.union syms syms2
                in
                (Success (G_theory lid syn (if sameSig then eSig else finExtSign)
                        (if sameSig then si else startSigId)
                        (joinSens (toThSens sens2) sens) startThId)
                        (length sens2)
                        (Set.map (G_symbol lid) $ Set.difference syms2 syms)
                        sameSig
                , if sameSig then
                     if null sens2 then "" else
                              show (vcat $ map (print_named lid) sens2)
                         else "")
              _ -> (Failure False, showRelDiags 1 ds)
  
  deleteHiddenSymbols :: String -> G_sign -> Result G_sign
  deleteHiddenSymbols syms gs@(G_sign lid (ExtSign sig _) _) = let
    str = trimLeft syms in if null str then return gs else
      case parse_symb_items lid of
        Nothing -> Fail.fail $ "no symbol parser for " ++ language_name lid
        Just sbpa -> case runParser (sepBy1 (sbpa mempty) anComma << eof)
                     (emptyAnnos ()) "" str of
          Left err -> Fail.fail $ show err
          Right sms -> do
            rm <- stat_symb_items lid sig sms
            let sym1 = symset_of lid sig
                sym2 = Set.filter (\ s -> any (matches lid s) rm) sym1
            sig2 <- fmap dom $ cogenerated_sign lid sym2 sig
            return $ G_sign lid (mkExtSign sig2) startSigId
  
  -- | reconstruct the morphism from symbols maps
  getMorphism :: G_sign
    -> String -- ^ the symbol mappings
    -> Result G_morphism
  getMorphism (G_sign lid (ExtSign sig _) _) syms =
      let str = trimLeft syms in
      if null str then return $ mkG_morphism lid $ ide sig else
      case parse_symb_map_items lid of
        Nothing -> Fail.fail $ "no symbol map parser for " ++ language_name lid
        Just smpa -> case runParser (sepBy1 (smpa mempty) anComma << eof)
                     (emptyAnnos ()) "" str of
          Left err -> Fail.fail $ show err
          Right sms -> do
            rm <- stat_symb_map_items lid sig Nothing sms
            fmap (mkG_morphism lid) $ induced_from_morphism lid rm sig
  
  -- | get the gmorphism for a gmorphism name
  translateByGName :: LogicGraph -> G_sign
    -> String -- ^ the name of the morphism
    -> Result GMorphism
  translateByGName lg gsig gname =
    let str = trim gname in
    if null str then ginclusion lg gsig gsig else do
      cmor <- lookupComorphism str lg
      gEmbedComorphism cmor gsig
  
  -- | get the gmorphism for a gmorphism name with symbols maps
  getGMorphism :: LogicGraph -> G_sign
    -> String -- ^ the name of the gmorphism
    -> String -- ^ the symbol mappings
    -> Result GMorphism
  getGMorphism lg gsig gname syms = do
    gmor1 <- translateByGName lg gsig gname
    gmor2 <- fmap gEmbed $ getMorphism (cod gmor1) syms
    composeMorphisms gmor1 gmor2
  