{- |
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 :: GlobalAnnos -> String -> G_theory -> (BasicExtResponse, String)
extendByBasicSpec ga :: GlobalAnnos
ga str :: String
str
  gt :: G_theory
gt@(G_theory lid :: lid
lid syn :: Maybe IRI
syn eSig :: ExtSign sign symbol
eSig@(ExtSign sign :: sign
sign syms :: Set symbol
syms) si :: SigId
si sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _)
  = let tstr :: String
tstr = String -> String
trimLeft String
str in
  if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
tstr then (G_theory -> Int -> Set G_symbol -> Bool -> BasicExtResponse
Success G_theory
gt 0 Set G_symbol
forall a. Set a
Set.empty Bool
True, "") else
  case Maybe IRI -> lid -> Maybe (PrefixMap -> AParser () basic_spec)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)
basicSpecParser Maybe IRI
forall a. Maybe a
Nothing lid
lid of
    Nothing -> (Bool -> BasicExtResponse
Failure Bool
True, "missing basic spec parser")
    Just p :: PrefixMap -> AParser () basic_spec
p -> case lid
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> Maybe
     ((basic_spec, sign, GlobalAnnos)
      -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
basic_analysis lid
lid of
      Nothing -> (Bool -> BasicExtResponse
Failure Bool
True, "missing basic analysis")
      Just f :: (basic_spec, sign, GlobalAnnos)
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
f -> case AParser () basic_spec
-> AnnoState () -> String -> String -> Either ParseError basic_spec
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser (PrefixMap -> AParser () basic_spec
p PrefixMap
forall k a. Map k a
Map.empty AParser () basic_spec
-> ParsecT String (AnnoState ()) Identity ()
-> AParser () basic_spec
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState ()) Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ()) "" String
tstr of
        Left err :: ParseError
err -> (Bool -> BasicExtResponse
Failure Bool
False, ParseError -> String
forall a. Show a => a -> String
show ParseError
err)
        Right bs :: basic_spec
bs -> let
          Result ds :: [Diagnosis]
ds res :: Maybe (basic_spec, ExtSign sign symbol, [Named sentence])
res = (basic_spec, sign, GlobalAnnos)
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
f (basic_spec
bs, sign
sign, GlobalAnnos
ga)
          in case Maybe (basic_spec, ExtSign sign symbol, [Named sentence])
res of
            Just (_, ExtSign sign2 :: sign
sign2 syms2 :: Set symbol
syms2, sens2 :: [Named sentence]
sens2) | Bool -> Bool
not ([Diagnosis] -> Bool
hasErrors [Diagnosis]
ds) ->
              let sameSig :: Bool
sameSig = sign
sign2 sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
== sign
sign
                  finExtSign :: ExtSign sign symbol
finExtSign = sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
sign2 (Set symbol -> ExtSign sign symbol)
-> Set symbol -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set symbol
syms Set symbol
syms2
              in
              (G_theory -> Int -> Set G_symbol -> Bool -> BasicExtResponse
Success (lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
syn (if Bool
sameSig then ExtSign sign symbol
eSig else ExtSign sign symbol
finExtSign)
                      (if Bool
sameSig then SigId
si else SigId
startSigId)
                      (ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
joinSens ([Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence]
sens2) ThSens sentence (AnyComorphism, BasicProof)
sens) ThId
startThId)
                      ([Named sentence] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Named sentence]
sens2)
                      ((symbol -> G_symbol) -> Set symbol -> Set G_symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (lid -> symbol -> G_symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> symbol -> G_symbol
G_symbol lid
lid) (Set symbol -> Set G_symbol) -> Set symbol -> Set G_symbol
forall a b. (a -> b) -> a -> b
$ Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set symbol
syms2 Set symbol
syms)
                      Bool
sameSig
              , if Bool
sameSig then
                   if [Named sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence]
sens2 then "" else
                            Doc -> String
forall a. Show a => a -> String
show ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Named sentence -> Doc) -> [Named sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> Named sentence -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid
lid) [Named sentence]
sens2)
                       else "")
            _ -> (Bool -> BasicExtResponse
Failure Bool
False, Int -> [Diagnosis] -> String
showRelDiags 1 [Diagnosis]
ds)

deleteHiddenSymbols :: String -> G_sign -> Result G_sign
deleteHiddenSymbols :: String -> G_sign -> Result G_sign
deleteHiddenSymbols syms :: String
syms gs :: G_sign
gs@(G_sign lid :: lid
lid (ExtSign sig :: sign
sig _) _) = let
  str :: String
str = String -> String
trimLeft String
syms in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
str then G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return G_sign
gs else
    case lid -> Maybe (PrefixMap -> AParser () symb_items)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> Maybe (PrefixMap -> AParser st symb_items)
parse_symb_items lid
lid of
      Nothing -> String -> Result G_sign
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result G_sign) -> String -> Result G_sign
forall a b. (a -> b) -> a -> b
$ "no symbol parser for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
      Just sbpa :: PrefixMap -> AParser () symb_items
sbpa -> case GenParser Char (AnnoState ()) [symb_items]
-> AnnoState ()
-> String
-> String
-> Either ParseError [symb_items]
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser (AParser () symb_items
-> ParsecT String (AnnoState ()) Identity Token
-> GenParser Char (AnnoState ()) [symb_items]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 (PrefixMap -> AParser () symb_items
sbpa PrefixMap
forall a. Monoid a => a
mempty) ParsecT String (AnnoState ()) Identity Token
forall st. AParser st Token
anComma GenParser Char (AnnoState ()) [symb_items]
-> ParsecT String (AnnoState ()) Identity ()
-> GenParser Char (AnnoState ()) [symb_items]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState ()) Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)
                   (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ()) "" String
str of
        Left err :: ParseError
err -> String -> Result G_sign
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result G_sign) -> String -> Result G_sign
forall a b. (a -> b) -> a -> b
$ ParseError -> String
forall a. Show a => a -> String
show ParseError
err
        Right sms :: [symb_items]
sms -> do
          [raw_symbol]
rm <- lid -> sign -> [symb_items] -> Result [raw_symbol]
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> [symb_items] -> Result [raw_symbol]
stat_symb_items lid
lid sign
sig [symb_items]
sms
          let sym1 :: Set symbol
sym1 = lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
lid sign
sig
              sym2 :: Set symbol
sym2 = (symbol -> Bool) -> Set symbol -> Set symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ s :: symbol
s -> (raw_symbol -> Bool) -> [raw_symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (lid -> symbol -> raw_symbol -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol -> Bool
matches lid
lid symbol
s) [raw_symbol]
rm) Set symbol
sym1
          sign
sig2 <- (morphism -> sign) -> Result morphism -> Result sign
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom (Result morphism -> Result sign) -> Result morphism -> Result sign
forall a b. (a -> b) -> a -> b
$ lid -> Set symbol -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Set symbol -> sign -> Result morphism
cogenerated_sign lid
lid Set symbol
sym2 sign
sig
          G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig2) SigId
startSigId

-- | reconstruct the morphism from symbols maps
getMorphism :: G_sign
  -> String -- ^ the symbol mappings
  -> Result G_morphism
getMorphism :: G_sign -> String -> Result G_morphism
getMorphism (G_sign lid :: lid
lid (ExtSign sig :: sign
sig _) _) syms :: String
syms =
    let str :: String
str = String -> String
trimLeft String
syms in
    if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
str then G_morphism -> Result G_morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (G_morphism -> Result G_morphism)
-> G_morphism -> Result G_morphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> G_morphism
mkG_morphism lid
lid (morphism -> G_morphism) -> morphism -> G_morphism
forall a b. (a -> b) -> a -> b
$ sign -> morphism
forall object morphism.
Category object morphism =>
object -> morphism
ide sign
sig else
    case lid -> Maybe (PrefixMap -> AParser () symb_map_items)
forall lid basic_spec symbol symb_items symb_map_items st.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> Maybe (PrefixMap -> AParser st symb_map_items)
parse_symb_map_items lid
lid of
      Nothing -> String -> Result G_morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result G_morphism) -> String -> Result G_morphism
forall a b. (a -> b) -> a -> b
$ "no symbol map parser for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
      Just smpa :: PrefixMap -> AParser () symb_map_items
smpa -> case GenParser Char (AnnoState ()) [symb_map_items]
-> AnnoState ()
-> String
-> String
-> Either ParseError [symb_map_items]
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser (AParser () symb_map_items
-> ParsecT String (AnnoState ()) Identity Token
-> GenParser Char (AnnoState ()) [symb_map_items]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 (PrefixMap -> AParser () symb_map_items
smpa PrefixMap
forall a. Monoid a => a
mempty) ParsecT String (AnnoState ()) Identity Token
forall st. AParser st Token
anComma GenParser Char (AnnoState ()) [symb_map_items]
-> ParsecT String (AnnoState ()) Identity ()
-> GenParser Char (AnnoState ()) [symb_map_items]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState ()) Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)
                   (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ()) "" String
str of
        Left err :: ParseError
err -> String -> Result G_morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result G_morphism) -> String -> Result G_morphism
forall a b. (a -> b) -> a -> b
$ ParseError -> String
forall a. Show a => a -> String
show ParseError
err
        Right sms :: [symb_map_items]
sms -> do
          EndoMap raw_symbol
rm <- lid
-> sign
-> Maybe sign
-> [symb_map_items]
-> Result (EndoMap raw_symbol)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> sign
-> Maybe sign
-> [symb_map_items]
-> Result (EndoMap raw_symbol)
stat_symb_map_items lid
lid sign
sig Maybe sign
forall a. Maybe a
Nothing [symb_map_items]
sms
          (morphism -> G_morphism) -> Result morphism -> Result G_morphism
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (lid -> morphism -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> G_morphism
mkG_morphism lid
lid) (Result morphism -> Result G_morphism)
-> Result morphism -> Result G_morphism
forall a b. (a -> b) -> a -> b
$ lid -> EndoMap raw_symbol -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> EndoMap raw_symbol -> sign -> Result morphism
induced_from_morphism lid
lid EndoMap raw_symbol
rm sign
sig

-- | get the gmorphism for a gmorphism name
translateByGName :: LogicGraph -> G_sign
  -> String -- ^ the name of the morphism
  -> Result GMorphism
translateByGName :: LogicGraph -> G_sign -> String -> Result GMorphism
translateByGName lg :: LogicGraph
lg gsig :: G_sign
gsig gname :: String
gname =
  let str :: String
str = String -> String
trim String
gname in
  if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
str then LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
gsig G_sign
gsig else do
    AnyComorphism
cmor <- String -> LogicGraph -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyComorphism
lookupComorphism String
str LogicGraph
lg
    AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism AnyComorphism
cmor G_sign
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 :: LogicGraph -> G_sign -> String -> String -> Result GMorphism
getGMorphism lg :: LogicGraph
lg gsig :: G_sign
gsig gname :: String
gname syms :: String
syms = do
  GMorphism
gmor1 <- LogicGraph -> G_sign -> String -> Result GMorphism
translateByGName LogicGraph
lg G_sign
gsig String
gname
  GMorphism
gmor2 <- (G_morphism -> GMorphism) -> Result G_morphism -> Result GMorphism
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap G_morphism -> GMorphism
gEmbed (Result G_morphism -> Result GMorphism)
-> Result G_morphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ G_sign -> String -> Result G_morphism
getMorphism (GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
gmor1) String
syms
  GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms GMorphism
gmor1 GMorphism
gmor2