{- |
Module      :  ./Syntax/Parse_AS_Structured.hs
Description :  parser for DOL OMS and CASL (heterogeneous) structured specifications
Copyright   :  (c) Till Mossakowski, Christian Maeder, Uni Bremen 2002-2016
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Grothendieck)

Parser for CASL (heterogeneous) structured specifications
   Concerning the homogeneous syntax, this follows Sect II:3.1.3
   of the CASL Reference Manual.
Parser for DOL ontologies, models and specifications and networks.
   Follows the DOL OMG standard, clauses 9.4 and 9.5
-}

module Syntax.Parse_AS_Structured
    ( annoParser2
    , basicSpec
    , caslGroupSpec
    , groupSpec
    , aSpec
    , qualification
    , parseMapping
    , parseCorrespondences
    , parseItemsList
    , parseItemsMap
    , translationList
    , renaming
    , restriction
    , hetIRI
    , parseNetwork
    ) where

import Logic.Logic
import Logic.Comorphism
import Logic.Grothendieck
import Logic.KnownIris

import Syntax.AS_Structured

import Common.AS_Annotation
import Common.AnnoState
import Common.AnnoParser
import Common.GlobalAnnotations
import Common.Id
import Common.IRI
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token

import Text.ParserCombinators.Parsec

import Data.Char
import Data.Maybe
import Control.Monad
import qualified Control.Monad.Fail as Fail

expandCurieM :: LogicGraph -> IRI -> GenParser Char st IRI
expandCurieM :: LogicGraph -> IRI -> GenParser Char st IRI
expandCurieM lG :: LogicGraph
lG i :: IRI
i =
  case Map String IRI -> IRI -> Maybe IRI
expandCurie (LogicGraph -> Map String IRI
prefixes LogicGraph
lG) IRI
i of
    Just ei :: IRI
ei -> IRI -> GenParser Char st IRI
forall (m :: * -> *) a. Monad m => a -> m a
return IRI
ei
    Nothing -> IRI -> GenParser Char st IRI
forall (m :: * -> *) a. Monad m => a -> m a
return IRI
i

expandCurieMConservative :: LogicGraph -> IRI -> GenParser Char st IRI
expandCurieMConservative :: LogicGraph -> IRI -> GenParser Char st IRI
expandCurieMConservative lG :: LogicGraph
lG i :: IRI
i = if IRI -> Bool
isSimple IRI
i then IRI -> GenParser Char st IRI
forall (m :: * -> *) a. Monad m => a -> m a
return IRI
i
                                else LogicGraph -> IRI -> GenParser Char st IRI
forall st. LogicGraph -> IRI -> GenParser Char st IRI
expandCurieM LogicGraph
lG IRI
i

hetIriCurie :: GenParser Char st IRI
hetIriCurie :: GenParser Char st IRI
hetIriCurie = GenParser Char st IRI -> GenParser Char st IRI
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char st IRI -> GenParser Char st IRI)
-> GenParser Char st IRI -> GenParser Char st IRI
forall a b. (a -> b) -> a -> b
$ do
  IRI
i <- GenParser Char st IRI
forall st. IRIParser st IRI
iriCurie
  if IRI -> String
iriToStringUnsecure IRI
i String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`
     ([String]
casl_reserved_words [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_fops [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> String -> String
forall a. a -> [a] -> [a]
: []) ")(,|;")
    then String -> GenParser Char st IRI
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected (String -> GenParser Char st IRI)
-> String -> GenParser Char st IRI
forall a b. (a -> b) -> a -> b
$ IRI -> String
forall a. Show a => a -> String
show IRI
i
    else IRI -> GenParser Char st IRI
forall (m :: * -> *) a. Monad m => a -> m a
return IRI
i

hetIRI :: LogicGraph -> GenParser Char st IRI
hetIRI :: LogicGraph -> GenParser Char st IRI
hetIRI lG :: LogicGraph
lG = (GenParser Char st IRI
forall st. IRIParser st IRI
hetIriCurie GenParser Char st IRI
-> (IRI -> GenParser Char st IRI) -> GenParser Char st IRI
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LogicGraph -> IRI -> GenParser Char st IRI
forall st. LogicGraph -> IRI -> GenParser Char st IRI
expandCurieM LogicGraph
lG) GenParser Char st IRI
-> ParsecT String st Identity () -> GenParser Char st IRI
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String st Identity ()
forall st. CharParser st ()
skipSmart

-- | parse annotations and then still call an annotation parser
annoParser2 :: AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 :: AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 =
  ([Annotation] -> Annoted a -> Annoted a)
-> ParsecT String (AnnoState st) Identity [Annotation]
-> AParser st (Annoted a)
-> AParser st (Annoted a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\ x :: [Annotation]
x (Annoted y :: a
y pos :: Range
pos l :: [Annotation]
l r :: [Annotation]
r) -> a -> Range -> [Annotation] -> [Annotation] -> Annoted a
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted a
y Range
pos ([Annotation]
x [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
l) [Annotation]
r) ParsecT String (AnnoState st) Identity [Annotation]
forall st. AParser st [Annotation]
annos

-- * logic and encoding names

-- within sublogics we allow some further symbol characters
sublogicChars :: AParser st String
sublogicChars :: AParser st String
sublogicChars = ParsecT String (AnnoState st) Identity Char -> AParser st String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String (AnnoState st) Identity Char -> AParser st String)
-> ParsecT String (AnnoState st) Identity Char -> AParser st String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy ((Char -> Bool) -> ParsecT String (AnnoState st) Identity Char)
-> (Char -> Bool) -> ParsecT String (AnnoState st) Identity Char
forall a b. (a -> b) -> a -> b
$ \ c :: Char
c -> Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Char
c ":./\\" Bool -> Bool -> Bool
&& Char -> Bool
isSignChar Char
c
    Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "_'" Bool -> Bool -> Bool
|| Char -> Bool
isAlphaNum Char
c

lookupLogicM :: IRI -> AParser st String
lookupLogicM :: IRI -> AParser st String
lookupLogicM i :: IRI
i = if IRI -> Bool
isSimple IRI
i
                 then String -> AParser st String
forall (m :: * -> *) a. Monad m => a -> m a
return String
l
                 else case String -> Maybe String
lookupLogicName String
l of
                   Just s :: String
s -> String -> AParser st String
forall (m :: * -> *) a. Monad m => a -> m a
return String
s
                   Nothing -> String -> AParser st String
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> AParser st String) -> String -> AParser st String
forall a b. (a -> b) -> a -> b
$ "logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
forall a. Show a => a -> String
show IRI
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found"
  where l :: String
l = IRI -> String
iriToStringUnsecure IRI
i

{- keep these identical in order to
decide after seeing ".", ":" or "->" what was meant -}
logicName :: LogicGraph -> AParser st Logic_name
logicName :: LogicGraph -> AParser st Logic_name
logicName l :: LogicGraph
l = do
      IRI
i <- GenParser Char (AnnoState st) IRI
forall st. IRIParser st IRI
hetIriCurie GenParser Char (AnnoState st) IRI
-> (IRI -> GenParser Char (AnnoState st) IRI)
-> GenParser Char (AnnoState st) IRI
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LogicGraph -> IRI -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> IRI -> GenParser Char st IRI
expandCurieMConservative LogicGraph
l
      let (ft :: String
ft, rt :: String
rt) = if IRI -> Bool
isSimple IRI
i then (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '.') (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ IRI -> String
iFragment IRI
i else ( IRI -> String
iFragment IRI
i, [])
      (e :: IRI
e, ms :: Maybe Token
ms) <- if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
rt then (IRI, Maybe Token)
-> ParsecT String (AnnoState st) Identity (IRI, Maybe Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI
i, Maybe Token
forall a. Maybe a
Nothing)
         else do
           String
s <- AParser st String
forall st. AParser st String
sublogicChars -- try more sublogic characters
           (IRI, Maybe Token)
-> ParsecT String (AnnoState st) Identity (IRI, Maybe Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI
i { iFragment :: String
iFragment = String
ft},
                   Token -> Maybe Token
forall a. a -> Maybe a
Just (Token -> Maybe Token)
-> (String -> Token) -> String -> Maybe Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Token
mkSimpleId (String -> Maybe Token) -> String -> Maybe Token
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
tail String
rt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)
      CharParser (AnnoState st) ()
forall st. CharParser st ()
skipSmart
      -- an optional spec name for a sublogic based on a theory #171
      Maybe IRI
mt <- GenParser Char (AnnoState st) IRI
-> ParsecT String (AnnoState st) Identity (Maybe IRI)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe
            (GenParser Char (AnnoState st) IRI
 -> ParsecT String (AnnoState st) Identity (Maybe IRI))
-> GenParser Char (AnnoState st) IRI
-> ParsecT String (AnnoState st) Identity (Maybe IRI)
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '(' ParsecT String (AnnoState st) Identity Char
-> GenParser Char (AnnoState st) IRI
-> GenParser Char (AnnoState st) IRI
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (GenParser Char (AnnoState st) IRI
forall st. IRIParser st IRI
iriCurie GenParser Char (AnnoState st) IRI
-> (IRI -> GenParser Char (AnnoState st) IRI)
-> GenParser Char (AnnoState st) IRI
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LogicGraph -> IRI -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> IRI -> GenParser Char st IRI
expandCurieMConservative LogicGraph
l) GenParser Char (AnnoState st) IRI
-> ParsecT String (AnnoState st) Identity Token
-> GenParser Char (AnnoState st) IRI
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
cParenT
      String
lo <- IRI -> AParser st String
forall st. IRI -> AParser st String
lookupLogicM IRI
e
      Logic_name -> AParser st Logic_name
forall (m :: * -> *) a. Monad m => a -> m a
return (Logic_name -> AParser st Logic_name)
-> Logic_name -> AParser st Logic_name
forall a b. (a -> b) -> a -> b
$ String -> Maybe Token -> Maybe IRI -> Logic_name
Logic_name String
lo Maybe Token
ms Maybe IRI
mt

qualification :: LogicGraph -> AParser st (Token, LogicDescr)
qualification :: LogicGraph -> AParser st (Token, LogicDescr)
qualification l :: LogicGraph
l =
  ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity LogicDescr
-> AParser st (Token, LogicDescr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
logicS) (LogicGraph -> ParsecT String (AnnoState st) Identity LogicDescr
forall st. LogicGraph -> AParser st LogicDescr
logicDescr LogicGraph
l)
  AParser st (Token, LogicDescr)
-> AParser st (Token, LogicDescr) -> AParser st (Token, LogicDescr)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
s <- String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
serializationS ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey "language"
    IRI
i <- IRIParser (AnnoState st) IRI
forall st. IRIParser st IRI
iriCurie
    CharParser (AnnoState st) ()
forall st. CharParser st ()
skipSmart
    (Token, LogicDescr) -> AParser st (Token, LogicDescr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
s,
      (if Token -> String
tokStr Token
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
serializationS then IRI -> LogicDescr
SyntaxQual else IRI -> LogicDescr
LanguageQual) IRI
i)

logicDescr :: LogicGraph -> AParser st LogicDescr
logicDescr :: LogicGraph -> AParser st LogicDescr
logicDescr l :: LogicGraph
l = do
  n :: Logic_name
n@(Logic_name ln :: String
ln _ _) <- LogicGraph -> AParser st Logic_name
forall st. LogicGraph -> AParser st Logic_name
logicName LogicGraph
l
  LogicDescr -> AParser st LogicDescr -> AParser st LogicDescr
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (Logic_name -> LogicDescr
nameToLogicDescr Logic_name
n) (AParser st LogicDescr -> AParser st LogicDescr)
-> AParser st LogicDescr -> AParser st LogicDescr
forall a b. (a -> b) -> a -> b
$ do
     Token
r <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
serializationS
     Either ParseError IRI
sp <- CharParser (AnnoState st) IRI
-> CharParser (AnnoState st) (Either ParseError IRI)
forall st a. CharParser st a -> CharParser st (Either ParseError a)
sneakAhead CharParser (AnnoState st) IRI
forall st. IRIParser st IRI
iriCurie
     case Either ParseError IRI
sp of
       Left _ -> CharParser (AnnoState st) IRI
forall st. IRIParser st IRI
iriCurie CharParser (AnnoState st) IRI
-> AParser st LogicDescr -> AParser st LogicDescr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> AParser st LogicDescr
forall a. HasCallStack => String -> a
error "logicDescr" -- reproduce the error
       Right s :: IRI
s -> do
         IRI
s' <- if IRI -> Bool
isSimple IRI
s then IRI -> CharParser (AnnoState st) IRI
forall (m :: * -> *) a. Monad m => a -> m a
return IRI
s else LogicGraph -> IRI -> CharParser (AnnoState st) IRI
forall st. LogicGraph -> IRI -> GenParser Char st IRI
expandCurieMConservative LogicGraph
l IRI
s
         let ld :: LogicDescr
ld = Logic_name -> Maybe IRI -> Range -> LogicDescr
LogicDescr Logic_name
n (IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
s') (Range -> LogicDescr) -> Range -> LogicDescr
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
r
         (Logic lid :: lid
lid, sm :: Maybe IRI
sm) <- String
-> LogicGraph
-> ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI)
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m (AnyLogic, Maybe IRI)
lookupCurrentSyntax "logicDescr" (LogicGraph
 -> ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI))
-> LogicGraph
-> ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI)
forall a b. (a -> b) -> a -> b
$ LogicDescr -> LogicGraph -> LogicGraph
setLogicName LogicDescr
ld LogicGraph
l
         case Maybe IRI
-> lid -> Maybe (Map String IRI -> AParser Any 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 (Map String IRI -> AParser st basic_spec)
basicSpecParser Maybe IRI
sm lid
lid of
           Just _ -> CharParser (AnnoState st) IRI
forall st. IRIParser st IRI
iriCurie CharParser (AnnoState st) IRI
-> ParsecT String (AnnoState st) Identity ()
-> ParsecT String (AnnoState st) Identity ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String (AnnoState st) Identity ()
forall st. CharParser st ()
skipSmart ParsecT String (AnnoState st) Identity ()
-> AParser st LogicDescr -> AParser st LogicDescr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LogicDescr -> AParser st LogicDescr
forall (m :: * -> *) a. Monad m => a -> m a
return LogicDescr
ld -- consume and return
           Nothing -> String -> AParser st LogicDescr
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected ("serialization \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
forall a. Show a => a -> String
show IRI
s
                       String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\" for logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
ln)
                      AParser st LogicDescr
-> AParser st LogicDescr -> AParser st LogicDescr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [AParser st LogicDescr] -> AParser st LogicDescr
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> AParser st LogicDescr)
-> [String] -> [AParser st LogicDescr]
forall a b. (a -> b) -> [a] -> [b]
map (\ pn :: String
pn -> AParser st LogicDescr
forall tok st a. GenParser tok st a
pzero AParser st LogicDescr -> String -> AParser st LogicDescr
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> '"' Char -> String -> String
forall a. a -> [a] -> [a]
: String
pn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"")
                                  ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null)
                                   (lid -> [String]
forall lid basic_spec symbol symb_items symb_map_items.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> [String]
basicSpecSyntaxes lid
lid)))

-- * parse Logic_code

parseLogic :: String -> LogicGraph -> AParser st (Logic_code, LogicGraph)
parseLogic :: String -> LogicGraph -> AParser st (Logic_code, LogicGraph)
parseLogic altKw :: String
altKw lG :: LogicGraph
lG = do
   Logic_code
lc <- String -> LogicGraph -> AParser st Logic_code
forall st. String -> LogicGraph -> AParser st Logic_code
parseLogicAux String
altKw LogicGraph
lG
   case Logic_code
lc of
     Logic_code _ _ (Just l :: Logic_name
l) _ ->
         (Logic_code, LogicGraph) -> AParser st (Logic_code, LogicGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Logic_code
lc, LogicDescr -> LogicGraph -> LogicGraph
setLogicName (Logic_name -> LogicDescr
nameToLogicDescr Logic_name
l) LogicGraph
lG)
     Logic_code (Just c :: String
c) _ _ _ -> do
         LogicGraph
nLg <- String -> LogicGraph -> AParser st LogicGraph
forall st. String -> LogicGraph -> AParser st LogicGraph
lookupAndSetComorphismName String
c LogicGraph
lG
         (Logic_code, LogicGraph) -> AParser st (Logic_code, LogicGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Logic_code
lc, LogicGraph
nLg)
     _ -> (Logic_code, LogicGraph) -> AParser st (Logic_code, LogicGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Logic_code
lc, LogicGraph
lG)

parseLogicAux :: String -> LogicGraph -> AParser st Logic_code
parseLogicAux :: String -> LogicGraph -> AParser st Logic_code
parseLogicAux altKw :: String
altKw lG :: LogicGraph
lG =
    do Token
l <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
logicS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
altKw
       do
           Token
f <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
funS  -- parse at least a logic target after "logic"
           Logic_name
t <- LogicGraph -> AParser st Logic_name
forall st. LogicGraph -> AParser st Logic_name
logicName LogicGraph
lG
           Logic_code -> AParser st Logic_code
forall (m :: * -> *) a. Monad m => a -> m a
return (Logic_code -> AParser st Logic_code)
-> Logic_code -> AParser st Logic_code
forall a b. (a -> b) -> a -> b
$ Maybe String
-> Maybe Logic_name -> Maybe Logic_name -> Range -> Logic_code
Logic_code Maybe String
forall a. Maybe a
Nothing Maybe Logic_name
forall a. Maybe a
Nothing (Logic_name -> Maybe Logic_name
forall a. a -> Maybe a
Just Logic_name
t)
                                       (Range -> Logic_code) -> Range -> Logic_code
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
l Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
f
         AParser st Logic_code
-> AParser st Logic_code -> AParser st Logic_code
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
          Logic_name
e <- LogicGraph -> AParser st Logic_name
forall st. LogicGraph -> AParser st Logic_name
logicName LogicGraph
lG
               -- try to parse encoding or logic source after "logic"
          case Logic_name
e of
              Logic_name f :: String
f Nothing Nothing ->
                      do Token
c <- AParser st Token
forall st. AParser st Token
colonT
                         LogicGraph -> Maybe String -> [Token] -> AParser st Logic_code
forall st.
LogicGraph -> Maybe String -> [Token] -> AParser st Logic_code
parseLogAfterColon LogicGraph
lG (String -> Maybe String
forall a. a -> Maybe a
Just String
f) [Token
l, Token
c]
                      AParser st Logic_code
-> AParser st Logic_code -> AParser st Logic_code
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
forall st.
LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
parseOptLogTarget LogicGraph
lG Maybe String
forall a. Maybe a
Nothing (Logic_name -> Maybe Logic_name
forall a. a -> Maybe a
Just Logic_name
e) [Token
l]
                      AParser st Logic_code
-> AParser st Logic_code -> AParser st Logic_code
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Logic_code -> AParser st Logic_code
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
-> Maybe Logic_name -> Maybe Logic_name -> Range -> Logic_code
Logic_code (String -> Maybe String
forall a. a -> Maybe a
Just String
f) Maybe Logic_name
forall a. Maybe a
Nothing Maybe Logic_name
forall a. Maybe a
Nothing
                                  (Range -> Logic_code) -> Range -> Logic_code
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
l)
              _ -> LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
forall st.
LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
parseOptLogTarget LogicGraph
lG Maybe String
forall a. Maybe a
Nothing (Logic_name -> Maybe Logic_name
forall a. a -> Maybe a
Just Logic_name
e) [Token
l]

-- parse optional logic source and target after a colon (given an encoding e)
parseLogAfterColon :: LogicGraph -> Maybe String -> [Token]
                      -> AParser st Logic_code
parseLogAfterColon :: LogicGraph -> Maybe String -> [Token] -> AParser st Logic_code
parseLogAfterColon lG :: LogicGraph
lG e :: Maybe String
e l :: [Token]
l = LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
forall st.
LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
parseOptLogTarget LogicGraph
lG Maybe String
e Maybe Logic_name
forall a. Maybe a
Nothing [Token]
l
    AParser st Logic_code
-> AParser st Logic_code -> AParser st Logic_code
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do Logic_name
s <- LogicGraph -> AParser st Logic_name
forall st. LogicGraph -> AParser st Logic_name
logicName LogicGraph
lG
       LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
forall st.
LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
parseOptLogTarget LogicGraph
lG Maybe String
e (Logic_name -> Maybe Logic_name
forall a. a -> Maybe a
Just Logic_name
s) [Token]
l
         AParser st Logic_code
-> AParser st Logic_code -> AParser st Logic_code
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Logic_code -> AParser st Logic_code
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
-> Maybe Logic_name -> Maybe Logic_name -> Range -> Logic_code
Logic_code Maybe String
e (Logic_name -> Maybe Logic_name
forall a. a -> Maybe a
Just Logic_name
s) Maybe Logic_name
forall a. Maybe a
Nothing (Range -> Logic_code) -> Range -> Logic_code
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
l)

-- parse an optional logic target (given encoding e or source s)
parseOptLogTarget :: LogicGraph -> Maybe String -> Maybe Logic_name -> [Token]
                  -> AParser st Logic_code
parseOptLogTarget :: LogicGraph
-> Maybe String
-> Maybe Logic_name
-> [Token]
-> AParser st Logic_code
parseOptLogTarget lG :: LogicGraph
lG e :: Maybe String
e s :: Maybe Logic_name
s l :: [Token]
l =
    do Token
f <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
funS
       let p :: Range
p = [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
l [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
f]
       do Logic_name
t <- LogicGraph -> AParser st Logic_name
forall st. LogicGraph -> AParser st Logic_name
logicName LogicGraph
lG
          Logic_code -> AParser st Logic_code
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
-> Maybe Logic_name -> Maybe Logic_name -> Range -> Logic_code
Logic_code Maybe String
e Maybe Logic_name
s (Logic_name -> Maybe Logic_name
forall a. a -> Maybe a
Just Logic_name
t) Range
p)
        AParser st Logic_code
-> AParser st Logic_code -> AParser st Logic_code
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Logic_code -> AParser st Logic_code
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
-> Maybe Logic_name -> Maybe Logic_name -> Range -> Logic_code
Logic_code Maybe String
e Maybe Logic_name
s Maybe Logic_name
forall a. Maybe a
Nothing Range
p)

plainComma :: AParser st Token
plainComma :: AParser st Token
plainComma = AParser st Token
forall st. AParser st Token
anComma AParser st Token -> AParser st Token -> AParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`notFollowedWith` String -> AParser st Token
forall st. String -> AParser st Token
asKey String
logicS

-- * parse G_mapping

callSymParser :: Bool -> Maybe (PrefixMap -> AParser st a) -> PrefixMap -> String -> String ->
                 AParser st ([a], [Token])
callSymParser :: Bool
-> Maybe (Map String IRI -> AParser st a)
-> Map String IRI
-> String
-> String
-> AParser st ([a], [Token])
callSymParser oneOnly :: Bool
oneOnly p :: Maybe (Map String IRI -> AParser st a)
p pm :: Map String IRI
pm name :: String
name itemType :: String
itemType = case Maybe (Map String IRI -> AParser st a)
p of
    Nothing ->
        String -> AParser st ([a], [Token])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> AParser st ([a], [Token]))
-> String -> AParser st ([a], [Token])
forall a b. (a -> b) -> a -> b
$ "no symbol" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
itemType String -> String -> String
forall a. [a] -> [a] -> [a]
++ " parser for language " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
    Just pa :: Map String IRI -> AParser st a
pa -> if Bool
oneOnly then do
        a
s <- Map String IRI -> AParser st a
pa Map String IRI
pm
        ([a], [Token]) -> AParser st ([a], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([a
s], [])
      else AParser st a
-> GenParser Char (AnnoState st) Token -> AParser st ([a], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy (Map String IRI -> AParser st a
pa Map String IRI
pm) GenParser Char (AnnoState st) Token
forall st. AParser st Token
plainComma

parseItemsMap :: AnyLogic -> PrefixMap -> AParser st (G_symb_map_items_list, [Token])
parseItemsMap :: AnyLogic
-> Map String IRI -> AParser st (G_symb_map_items_list, [Token])
parseItemsMap (Logic lid :: lid
lid) pm :: Map String IRI
pm = do
      (cs :: [symb_map_items]
cs, ps :: [Token]
ps) <- Bool
-> Maybe (Map String IRI -> AParser st symb_map_items)
-> Map String IRI
-> String
-> String
-> AParser st ([symb_map_items], [Token])
forall st a.
Bool
-> Maybe (Map String IRI -> AParser st a)
-> Map String IRI
-> String
-> String
-> AParser st ([a], [Token])
callSymParser Bool
False (lid -> Maybe (Map String IRI -> AParser st 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 (Map String IRI -> AParser st symb_map_items)
parse_symb_map_items lid
lid) Map String IRI
pm
                  (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid) " maps"
      (G_symb_map_items_list, [Token])
-> AParser st (G_symb_map_items_list, [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (lid -> [symb_map_items] -> G_symb_map_items_list
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 -> [symb_map_items] -> G_symb_map_items_list
G_symb_map_items_list lid
lid [symb_map_items]
cs, [Token]
ps)


parseMapping :: LogicGraph -> AParser st ([G_mapping], [Token])
parseMapping :: LogicGraph -> AParser st ([G_mapping], [Token])
parseMapping =
  String
-> (Logic_code -> G_mapping)
-> (G_symb_map_items_list -> G_mapping)
-> (AnyLogic
    -> Map String IRI -> AParser st (G_symb_map_items_list, [Token]))
-> LogicGraph
-> AParser st ([G_mapping], [Token])
forall a t st.
String
-> (Logic_code -> a)
-> (t -> a)
-> (AnyLogic -> Map String IRI -> AParser st (t, [Token]))
-> LogicGraph
-> AParser st ([a], [Token])
parseMapOrHide "translation" Logic_code -> G_mapping
G_logic_translation G_symb_map_items_list -> G_mapping
G_symb_map AnyLogic
-> Map String IRI -> AParser st (G_symb_map_items_list, [Token])
forall st.
AnyLogic
-> Map String IRI -> AParser st (G_symb_map_items_list, [Token])
parseItemsMap

parseMapOrHide :: String -> (Logic_code -> a) -> (t -> a)
               -> (AnyLogic -> PrefixMap -> AParser st (t, [Token])) -> LogicGraph
               -> AParser st ([a], [Token])
parseMapOrHide :: String
-> (Logic_code -> a)
-> (t -> a)
-> (AnyLogic -> Map String IRI -> AParser st (t, [Token]))
-> LogicGraph
-> AParser st ([a], [Token])
parseMapOrHide altKw :: String
altKw constrLogic :: Logic_code -> a
constrLogic constrMap :: t -> a
constrMap pa :: AnyLogic -> Map String IRI -> AParser st (t, [Token])
pa lG :: LogicGraph
lG =
    do (n :: Logic_code
n, nLg :: LogicGraph
nLg) <- String -> LogicGraph -> AParser st (Logic_code, LogicGraph)
forall st.
String -> LogicGraph -> AParser st (Logic_code, LogicGraph)
parseLogic String
altKw LogicGraph
lG
       do AParser st Token
forall st. AParser st Token
anComma
          (gs :: [a]
gs, ps :: [Token]
ps) <- String
-> (Logic_code -> a)
-> (t -> a)
-> (AnyLogic -> Map String IRI -> AParser st (t, [Token]))
-> LogicGraph
-> AParser st ([a], [Token])
forall a t st.
String
-> (Logic_code -> a)
-> (t -> a)
-> (AnyLogic -> Map String IRI -> AParser st (t, [Token]))
-> LogicGraph
-> AParser st ([a], [Token])
parseMapOrHide String
altKw Logic_code -> a
constrLogic t -> a
constrMap AnyLogic -> Map String IRI -> AParser st (t, [Token])
pa LogicGraph
nLg
          ([a], [Token]) -> AParser st ([a], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (Logic_code -> a
constrLogic Logic_code
n a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
gs, [Token]
ps)
        AParser st ([a], [Token])
-> AParser st ([a], [Token]) -> AParser st ([a], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([a], [Token]) -> AParser st ([a], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Logic_code -> a
constrLogic Logic_code
n], [])
    AParser st ([a], [Token])
-> AParser st ([a], [Token]) -> AParser st ([a], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      AnyLogic
l <- String
-> LogicGraph -> ParsecT String (AnnoState st) Identity AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "parseMapOrHide" LogicGraph
lG
      (m :: t
m, ps :: [Token]
ps) <- AnyLogic -> Map String IRI -> AParser st (t, [Token])
pa AnyLogic
l (Map String IRI -> AParser st (t, [Token]))
-> Map String IRI -> AParser st (t, [Token])
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String IRI
prefixes LogicGraph
lG
      do AParser st Token
forall st. AParser st Token
anComma
         (gs :: [a]
gs, qs :: [Token]
qs) <- String
-> (Logic_code -> a)
-> (t -> a)
-> (AnyLogic -> Map String IRI -> AParser st (t, [Token]))
-> LogicGraph
-> AParser st ([a], [Token])
forall a t st.
String
-> (Logic_code -> a)
-> (t -> a)
-> (AnyLogic -> Map String IRI -> AParser st (t, [Token]))
-> LogicGraph
-> AParser st ([a], [Token])
parseMapOrHide String
altKw Logic_code -> a
constrLogic t -> a
constrMap AnyLogic -> Map String IRI -> AParser st (t, [Token])
pa LogicGraph
lG
         ([a], [Token]) -> AParser st ([a], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (t -> a
constrMap t
m a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
gs, [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
qs)
        AParser st ([a], [Token])
-> AParser st ([a], [Token]) -> AParser st ([a], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([a], [Token]) -> AParser st ([a], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([t -> a
constrMap t
m], [Token]
ps)

-- * parse G_hiding

parseItemsList :: AnyLogic -> PrefixMap -> AParser st (G_symb_items_list, [Token])
parseItemsList :: AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
parseItemsList (Logic lid :: lid
lid) pm :: Map String IRI
pm = do
      (cs :: [symb_items]
cs, ps :: [Token]
ps) <- Bool
-> Maybe (Map String IRI -> AParser st symb_items)
-> Map String IRI
-> String
-> String
-> AParser st ([symb_items], [Token])
forall st a.
Bool
-> Maybe (Map String IRI -> AParser st a)
-> Map String IRI
-> String
-> String
-> AParser st ([a], [Token])
callSymParser Bool
False (lid -> Maybe (Map String IRI -> AParser st 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 (Map String IRI -> AParser st symb_items)
parse_symb_items lid
lid) Map String IRI
pm
                  (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid) ""
      (G_symb_items_list, [Token])
-> AParser st (G_symb_items_list, [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (lid -> [symb_items] -> G_symb_items_list
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 -> [symb_items] -> G_symb_items_list
G_symb_items_list lid
lid [symb_items]
cs, [Token]
ps)

parseSingleSymb :: AnyLogic -> PrefixMap -> AParser st (G_symb_items_list, [Token])
parseSingleSymb :: AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
parseSingleSymb (Logic lid :: lid
lid) pm :: Map String IRI
pm = do
      (cs :: [symb_items]
cs, ps :: [Token]
ps) <- Bool
-> Maybe (Map String IRI -> AParser st symb_items)
-> Map String IRI
-> String
-> String
-> AParser st ([symb_items], [Token])
forall st a.
Bool
-> Maybe (Map String IRI -> AParser st a)
-> Map String IRI
-> String
-> String
-> AParser st ([a], [Token])
callSymParser Bool
True (lid -> Maybe (Map String IRI -> AParser st 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 (Map String IRI -> AParser st symb_items)
parseSingleSymbItem lid
lid) Map String IRI
pm
                  (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid) ""
      (G_symb_items_list, [Token])
-> AParser st (G_symb_items_list, [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (lid -> [symb_items] -> G_symb_items_list
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 -> [symb_items] -> G_symb_items_list
G_symb_items_list lid
lid [symb_items]
cs, [Token]
ps)

parseHiding :: LogicGraph -> AParser st ([G_hiding], [Token])
parseHiding :: LogicGraph -> AParser st ([G_hiding], [Token])
parseHiding = 
  String
-> (Logic_code -> G_hiding)
-> (G_symb_items_list -> G_hiding)
-> (AnyLogic
    -> Map String IRI -> AParser st (G_symb_items_list, [Token]))
-> LogicGraph
-> AParser st ([G_hiding], [Token])
forall a t st.
String
-> (Logic_code -> a)
-> (t -> a)
-> (AnyLogic -> Map String IRI -> AParser st (t, [Token]))
-> LogicGraph
-> AParser st ([a], [Token])
parseMapOrHide "along" Logic_code -> G_hiding
G_logic_projection G_symb_items_list -> G_hiding
G_symb_list AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
forall st.
AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
parseItemsList

-- * specs

-- "then" is associative, therefore flatten extensions

flatExts :: [Annoted SPEC] -> [Annoted SPEC]
flatExts :: [Annoted SPEC] -> [Annoted SPEC]
flatExts = (Annoted SPEC -> [Annoted SPEC])
-> [Annoted SPEC] -> [Annoted SPEC]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Annoted SPEC -> [Annoted SPEC])
 -> [Annoted SPEC] -> [Annoted SPEC])
-> (Annoted SPEC -> [Annoted SPEC])
-> [Annoted SPEC]
-> [Annoted SPEC]
forall a b. (a -> b) -> a -> b
$ \ as :: Annoted SPEC
as -> case Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
as of
   Extension sps :: [Annoted SPEC]
sps _ -> [Annoted SPEC]
sps
   Group sp :: Annoted SPEC
sp _ -> case [Annoted SPEC] -> [Annoted SPEC]
flatExts [Annoted SPEC
sp] of
     [_] -> [Annoted SPEC
as]
     sps :: [Annoted SPEC]
sps -> [Annoted SPEC]
sps
   _ -> [Annoted SPEC
as]

spec :: LogicGraph -> AParser st (Annoted SPEC)
spec :: LogicGraph -> AParser st (Annoted SPEC)
spec l :: LogicGraph
l = do
  Annoted SPEC
sp1 <- AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
specThen LogicGraph
l)
  Annoted SPEC
-> AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option Annoted SPEC
sp1 (AParser st (Annoted SPEC) -> AParser st (Annoted SPEC))
-> AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ do
    Token
k <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "bridge"
    [RENAMING]
rs <- ParsecT String (AnnoState st) Identity RENAMING
-> ParsecT String (AnnoState st) Identity [RENAMING]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (LogicGraph -> ParsecT String (AnnoState st) Identity RENAMING
forall st. LogicGraph -> AParser st RENAMING
renaming LogicGraph
l)
    Annoted SPEC
sp2 <- AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
specThen LogicGraph
l)
    Annoted SPEC -> AParser st (Annoted SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> AParser st (Annoted SPEC))
-> (Range -> Annoted SPEC) -> Range -> AParser st (Annoted SPEC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPEC -> Annoted SPEC
forall a. a -> Annoted a
emptyAnno (SPEC -> Annoted SPEC) -> (Range -> SPEC) -> Range -> Annoted SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SPEC -> [RENAMING] -> Annoted SPEC -> Range -> SPEC
Bridge Annoted SPEC
sp1 [RENAMING]
rs Annoted SPEC
sp2 (Range -> AParser st (Annoted SPEC))
-> Range -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
k

specThen :: LogicGraph -> AParser st (Annoted SPEC)
specThen :: LogicGraph -> AParser st (Annoted SPEC)
specThen l :: LogicGraph
l = do
  (sps :: [Annoted SPEC]
sps, ps :: [Token]
ps) <- AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
specA LogicGraph
l) AParser st (Annoted SPEC)
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Annoted SPEC], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` String -> GenParser Char (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
thenS
  Annoted SPEC -> AParser st (Annoted SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> AParser st (Annoted SPEC))
-> Annoted SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ case [Annoted SPEC]
sps of
    [sp :: Annoted SPEC
sp] -> Annoted SPEC
sp
    _ -> SPEC -> Annoted SPEC
forall a. a -> Annoted a
emptyAnno ([Annoted SPEC] -> Range -> SPEC
Extension ([Annoted SPEC] -> [Annoted SPEC]
flatExts [Annoted SPEC]
sps) (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
ps)

specA :: LogicGraph -> AParser st (Annoted SPEC)
specA :: LogicGraph -> AParser st (Annoted SPEC)
specA l :: LogicGraph
l = do
  Annoted SPEC
sp <- AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (AParser st (Annoted SPEC) -> AParser st (Annoted SPEC))
-> AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
specB LogicGraph
l
  Annoted SPEC
-> AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option Annoted SPEC
sp (AParser st (Annoted SPEC) -> AParser st (Annoted SPEC))
-> AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ do
    Token
t <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
andS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
intersectS
    (sps :: [Annoted SPEC]
sps, ts :: [Token]
ts) <- AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
specB LogicGraph
l) AParser st (Annoted SPEC)
-> AParser st Token
-> GenParser Char (AnnoState st) ([Annoted SPEC], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` String -> AParser st Token
forall st. String -> AParser st Token
asKey (Token -> String
tokStr Token
t)
    let cons :: [Annoted SPEC] -> Range -> SPEC
cons = case Token -> String
tokStr Token
t of
                 "and" -> [Annoted SPEC] -> Range -> SPEC
Union
                 _ -> [Annoted SPEC] -> Range -> SPEC
Intersection
    Annoted SPEC -> AParser st (Annoted SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> AParser st (Annoted SPEC))
-> Annoted SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ SPEC -> Annoted SPEC
forall a. a -> Annoted a
emptyAnno ([Annoted SPEC] -> Range -> SPEC
cons (Annoted SPEC
sp Annoted SPEC -> [Annoted SPEC] -> [Annoted SPEC]
forall a. a -> [a] -> [a]
: [Annoted SPEC]
sps) (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange (Token
t Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ts))

specB :: LogicGraph -> AParser st (Annoted SPEC)
specB :: LogicGraph -> AParser st (Annoted SPEC)
specB l :: LogicGraph
l = do
    Token
p1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
localS
    Annoted SPEC
sp1 <- LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
    Token
p2 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
withinS
    Annoted SPEC
sp2 <- AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (AParser st (Annoted SPEC) -> AParser st (Annoted SPEC))
-> AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
specB LogicGraph
l
    Annoted SPEC -> AParser st (Annoted SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC -> Annoted SPEC
forall a. a -> Annoted a
emptyAnno (SPEC -> Annoted SPEC) -> SPEC -> Annoted SPEC
forall a b. (a -> b) -> a -> b
$ Annoted SPEC -> Annoted SPEC -> Range -> SPEC
Local_spec Annoted SPEC
sp1 Annoted SPEC
sp2 (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p1 Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
p2)
  AParser st (Annoted SPEC)
-> AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
specC LogicGraph
l

specC :: LogicGraph -> AParser st (Annoted SPEC)
specC :: LogicGraph -> AParser st (Annoted SPEC)
specC lG :: LogicGraph
lG = do
    let spD :: AParser st (Annoted SPEC)
spD = AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st SPEC -> AParser st (Annoted SPEC))
-> AParser st SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
specD LogicGraph
lG
        rest :: ParsecT String (AnnoState st) Identity (Annoted SPEC)
rest = ParsecT String (AnnoState st) Identity (Annoted SPEC)
forall st. AParser st (Annoted SPEC)
spD ParsecT String (AnnoState st) Identity (Annoted SPEC)
-> (Annoted SPEC
    -> ParsecT String (AnnoState st) Identity (Annoted SPEC))
-> ParsecT String (AnnoState st) Identity (Annoted SPEC)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Annoted SPEC -> AParser st SPEC]
-> Annoted SPEC
-> ParsecT String (AnnoState st) Identity (Annoted SPEC)
forall b st.
[Annoted b -> AParser st b] -> Annoted b -> AParser st (Annoted b)
translationList
          [ ((EXTRACTION -> SPEC)
-> ParsecT String (AnnoState st) Identity EXTRACTION
-> AParser st SPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` LogicGraph -> ParsecT String (AnnoState st) Identity EXTRACTION
forall st. LogicGraph -> AParser st EXTRACTION
extraction LogicGraph
lG) ((EXTRACTION -> SPEC) -> AParser st SPEC)
-> (Annoted SPEC -> EXTRACTION -> SPEC)
-> Annoted SPEC
-> AParser st SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SPEC -> EXTRACTION -> SPEC
Extraction
          , ((RENAMING -> SPEC)
-> ParsecT String (AnnoState st) Identity RENAMING
-> AParser st SPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` LogicGraph -> ParsecT String (AnnoState st) Identity RENAMING
forall st. LogicGraph -> AParser st RENAMING
renaming LogicGraph
lG) ((RENAMING -> SPEC) -> AParser st SPEC)
-> (Annoted SPEC -> RENAMING -> SPEC)
-> Annoted SPEC
-> AParser st SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SPEC -> RENAMING -> SPEC
Translation
          , ((RESTRICTION -> SPEC)
-> ParsecT String (AnnoState st) Identity RESTRICTION
-> AParser st SPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` LogicGraph -> ParsecT String (AnnoState st) Identity RESTRICTION
forall st. LogicGraph -> AParser st RESTRICTION
restriction LogicGraph
lG) ((RESTRICTION -> SPEC) -> AParser st SPEC)
-> (Annoted SPEC -> RESTRICTION -> SPEC)
-> Annoted SPEC
-> AParser st SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SPEC -> RESTRICTION -> SPEC
Reduction
          , ((APPROXIMATION -> SPEC)
-> ParsecT String (AnnoState st) Identity APPROXIMATION
-> AParser st SPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` LogicGraph -> ParsecT String (AnnoState st) Identity APPROXIMATION
forall st. LogicGraph -> AParser st APPROXIMATION
approximation LogicGraph
lG) ((APPROXIMATION -> SPEC) -> AParser st SPEC)
-> (Annoted SPEC -> APPROXIMATION -> SPEC)
-> Annoted SPEC
-> AParser st SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SPEC -> APPROXIMATION -> SPEC
Approximation
          , ((FILTERING -> SPEC)
-> ParsecT String (AnnoState st) Identity FILTERING
-> AParser st SPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` LogicGraph -> ParsecT String (AnnoState st) Identity FILTERING
forall st. LogicGraph -> AParser st FILTERING
filtering LogicGraph
lG) ((FILTERING -> SPEC) -> AParser st SPEC)
-> (Annoted SPEC -> FILTERING -> SPEC)
-> Annoted SPEC
-> AParser st SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SPEC -> FILTERING -> SPEC
Filtering
          , ((MINIMIZATION -> SPEC)
-> ParsecT String (AnnoState st) Identity MINIMIZATION
-> AParser st SPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` LogicGraph -> ParsecT String (AnnoState st) Identity MINIMIZATION
forall st. LogicGraph -> AParser st MINIMIZATION
minimization LogicGraph
lG) ((MINIMIZATION -> SPEC) -> AParser st SPEC)
-> (Annoted SPEC -> MINIMIZATION -> SPEC)
-> Annoted SPEC
-> AParser st SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted SPEC -> MINIMIZATION -> SPEC
Minimization]
    l :: AnyLogic
l@(Logic lid :: lid
lid) <- String
-> LogicGraph -> ParsecT String (AnnoState st) Identity AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "specC" LogicGraph
lG
    {- if the current logic has an associated data_logic,
    parse "data SPEC1 SPEC2", where SPEC1 is in the data_logic
    SPEC1 needs to be a basic spec or a grouped spec
    SPEC2 is in the currrent logic -}
    case lid -> Maybe AnyLogic
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 AnyLogic
data_logic lid
lid of
          Nothing -> AParser st (Annoted SPEC)
forall st. AParser st (Annoted SPEC)
rest
          Just lD :: AnyLogic
lD@(Logic dl :: lid
dl) -> do
              Token
p1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
dataS -- not a keyword
              Annoted SPEC
sp1 <- AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st SPEC -> AParser st (Annoted SPEC))
-> AParser st SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
forall st. LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
basicSpec LogicGraph
lG (AnyLogic
lD, Maybe IRI
forall a. Maybe a
Nothing)
                  AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
caslGroupSpec (String -> LogicGraph -> LogicGraph
setCurLogic (lid -> String
forall lid. Language lid => lid -> String
language_name lid
dl) LogicGraph
lG)
              Annoted SPEC
sp2 <- AParser st (Annoted SPEC)
forall st. AParser st (Annoted SPEC)
spD
              Annoted SPEC -> AParser st (Annoted SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC -> Annoted SPEC
forall a. a -> Annoted a
emptyAnno (SPEC -> Annoted SPEC) -> SPEC -> Annoted SPEC
forall a b. (a -> b) -> a -> b
$ AnyLogic
-> AnyLogic -> Annoted SPEC -> Annoted SPEC -> Range -> SPEC
Data AnyLogic
lD AnyLogic
l Annoted SPEC
sp1 Annoted SPEC
sp2 (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p1)
            AParser st (Annoted SPEC)
-> AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st (Annoted SPEC)
forall st. AParser st (Annoted SPEC)
rest

translationList :: [Annoted b -> AParser st b] -> Annoted b
  -> AParser st (Annoted b)
translationList :: [Annoted b -> AParser st b] -> Annoted b -> AParser st (Annoted b)
translationList cs :: [Annoted b -> AParser st b]
cs sp :: Annoted b
sp =
     do b
sp' <- [AParser st b] -> AParser st b
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([AParser st b] -> AParser st b) -> [AParser st b] -> AParser st b
forall a b. (a -> b) -> a -> b
$ ((Annoted b -> AParser st b) -> AParser st b)
-> [Annoted b -> AParser st b] -> [AParser st b]
forall a b. (a -> b) -> [a] -> [b]
map ((Annoted b -> AParser st b) -> Annoted b -> AParser st b
forall a b. (a -> b) -> a -> b
$ Annoted b
sp) [Annoted b -> AParser st b]
cs
        [Annoted b -> AParser st b] -> Annoted b -> AParser st (Annoted b)
forall b st.
[Annoted b -> AParser st b] -> Annoted b -> AParser st (Annoted b)
translationList [Annoted b -> AParser st b]
cs (b -> Annoted b
forall a. a -> Annoted a
emptyAnno b
sp')
     AParser st (Annoted b)
-> AParser st (Annoted b) -> AParser st (Annoted b)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Annoted b -> AParser st (Annoted b)
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted b
sp

{- | Parse renaming
@
RENAMING ::= with SYMB-MAP-ITEMS-LIST
@
SYMB-MAP-ITEMS-LIST is parsed using parseMapping -}
renaming :: LogicGraph -> AParser st RENAMING
renaming :: LogicGraph -> AParser st RENAMING
renaming l :: LogicGraph
l =
    do Token
kWith <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
withS
       (mappings :: [G_mapping]
mappings, commas :: [Token]
commas) <- LogicGraph -> AParser st ([G_mapping], [Token])
forall st. LogicGraph -> AParser st ([G_mapping], [Token])
parseMapping LogicGraph
l
       RENAMING -> AParser st RENAMING
forall (m :: * -> *) a. Monad m => a -> m a
return ([G_mapping] -> Range -> RENAMING
Renaming [G_mapping]
mappings (Range -> RENAMING) -> Range -> RENAMING
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
kWith Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
commas)

{- | Parse restriction
@
RESTRICTION ::= hide SYMB-ITEMS-LIST
              | reveal SYMB-MAP-ITEMS-LIST
@
SYMB-ITEMS-LIST is parsed using parseHiding; SYMB-MAP-ITEMS-LIST is
parsed using parseItemsMap -}
restriction :: LogicGraph -> AParser st RESTRICTION
restriction :: LogicGraph -> AParser st RESTRICTION
restriction lg :: LogicGraph
lg =
        -- hide
    do Token
kHide <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
hideS
       (symbs :: [G_hiding]
symbs, commas :: [Token]
commas) <- LogicGraph -> AParser st ([G_hiding], [Token])
forall st. LogicGraph -> AParser st ([G_hiding], [Token])
parseHiding LogicGraph
lg
       RESTRICTION -> AParser st RESTRICTION
forall (m :: * -> *) a. Monad m => a -> m a
return ([G_hiding] -> Range -> RESTRICTION
Hidden [G_hiding]
symbs ([Token] -> Range
catRange (Token
kHide Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
commas)))
    AParser st RESTRICTION
-> AParser st RESTRICTION -> AParser st RESTRICTION
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- reveal
    do Token
kReveal <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
revealS
       AnyLogic
nl <- String
-> LogicGraph -> ParsecT String (AnnoState st) Identity AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "reveal" LogicGraph
lg
       (mappings :: G_symb_map_items_list
mappings, commas :: [Token]
commas) <- AnyLogic
-> Map String IRI -> AParser st (G_symb_map_items_list, [Token])
forall st.
AnyLogic
-> Map String IRI -> AParser st (G_symb_map_items_list, [Token])
parseItemsMap AnyLogic
nl (Map String IRI -> AParser st (G_symb_map_items_list, [Token]))
-> Map String IRI -> AParser st (G_symb_map_items_list, [Token])
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String IRI
prefixes LogicGraph
lg
       RESTRICTION -> AParser st RESTRICTION
forall (m :: * -> *) a. Monad m => a -> m a
return (G_symb_map_items_list -> Range -> RESTRICTION
Revealed G_symb_map_items_list
mappings ([Token] -> Range
catRange (Token
kReveal Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
commas)))

-- | Parse approximation
approximation :: LogicGraph -> AParser st APPROXIMATION
approximation :: LogicGraph -> AParser st APPROXIMATION
approximation lg :: LogicGraph
lg =
 do Token
p1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
forgetS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
keepS
    (hs :: [G_hiding]
hs, _) <- LogicGraph -> AParser st ([G_hiding], [Token])
forall st. LogicGraph -> AParser st ([G_hiding], [Token])
parseHiding LogicGraph
lg
    Maybe IRI
li <- ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity (Maybe IRI)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String (AnnoState st) Identity IRI
 -> ParsecT String (AnnoState st) Identity (Maybe IRI))
-> ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity (Maybe IRI)
forall a b. (a -> b) -> a -> b
$ String -> AParser st Token
forall st. String -> AParser st Token
asKey String
keepS AParser st Token
-> ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LogicGraph -> ParsecT String (AnnoState st) Identity IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lg
    APPROXIMATION -> AParser st APPROXIMATION
forall (m :: * -> *) a. Monad m => a -> m a
return (APPROXIMATION -> AParser st APPROXIMATION)
-> APPROXIMATION -> AParser st APPROXIMATION
forall a b. (a -> b) -> a -> b
$ Bool -> [G_hiding] -> Maybe IRI -> Range -> APPROXIMATION
ForgetOrKeep (Token -> String
tokStr Token
p1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
keepS) [G_hiding]
hs Maybe IRI
li (Range -> APPROXIMATION) -> Range -> APPROXIMATION
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p1

minimization :: LogicGraph -> AParser st MINIMIZATION
minimization :: LogicGraph -> AParser st MINIMIZATION
minimization lg :: LogicGraph
lg = do
   Token
p <- AParser st Token
forall st. AParser st Token
minimizeKey AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
freeS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
cofreeS
   ([IRI]
cm) <- ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity [IRI]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (LogicGraph -> ParsecT String (AnnoState st) Identity IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lg)
   (cv :: [IRI]
cv, p2 :: [Token]
p2) <- ([IRI], [Token])
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], []) (ParsecT String (AnnoState st) Identity ([IRI], [Token])
 -> ParsecT String (AnnoState st) Identity ([IRI], [Token]))
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
forall a b. (a -> b) -> a -> b
$ do
       Token
p3 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
varsS
       [IRI]
ct <- ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity [IRI]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (LogicGraph -> ParsecT String (AnnoState st) Identity IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lg)
       ([IRI], [Token])
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([IRI]
ct, [Token
p3])
   MINIMIZATION -> AParser st MINIMIZATION
forall (m :: * -> *) a. Monad m => a -> m a
return (MINIMIZATION -> AParser st MINIMIZATION)
-> ([Token] -> MINIMIZATION) -> [Token] -> AParser st MINIMIZATION
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> [IRI] -> [IRI] -> Range -> MINIMIZATION
Mini Token
p [IRI]
cm [IRI]
cv (Range -> MINIMIZATION)
-> ([Token] -> Range) -> [Token] -> MINIMIZATION
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st MINIMIZATION)
-> [Token] -> AParser st MINIMIZATION
forall a b. (a -> b) -> a -> b
$ Token
p Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
p2

extraction :: LogicGraph -> AParser st EXTRACTION
extraction :: LogicGraph -> AParser st EXTRACTION
extraction lg :: LogicGraph
lg = do
  Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
extractS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
removeS
  (is :: [IRI]
is,commas :: [Token]
commas) <- GenParser Char (AnnoState st) IRI
-> AParser st Token
-> GenParser Char (AnnoState st) ([IRI], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy (LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lg) AParser st Token
forall st. CharParser st Token
commaT
  EXTRACTION -> AParser st EXTRACTION
forall (m :: * -> *) a. Monad m => a -> m a
return (EXTRACTION -> AParser st EXTRACTION)
-> (Range -> EXTRACTION) -> Range -> AParser st EXTRACTION
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [IRI] -> Range -> EXTRACTION
ExtractOrRemove (Token -> String
tokStr Token
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
extractS) [IRI]
is (Range -> AParser st EXTRACTION) -> Range -> AParser st EXTRACTION
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange (Token
pToken -> [Token] -> [Token]
forall a. a -> [a] -> [a]
:[Token]
commas)

filtering :: LogicGraph -> AParser st FILTERING
filtering :: LogicGraph -> AParser st FILTERING
filtering lg :: LogicGraph
lg = do
  Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
selectS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
rejectS
  Token -> LogicGraph -> AParser st FILTERING
forall st. Token -> LogicGraph -> AParser st FILTERING
filtering_aux Token
p LogicGraph
lg

filtering_aux :: Token -> LogicGraph -> AParser st FILTERING
filtering_aux :: Token -> LogicGraph -> AParser st FILTERING
filtering_aux p :: Token
p lg :: LogicGraph
lg =
  do 
    (AnyLogic, Maybe IRI)
s <- String
-> LogicGraph
-> ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI)
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m (AnyLogic, Maybe IRI)
lookupCurrentSyntax "filtering" LogicGraph
lg
    Basic_spec bs :: G_basic_spec
bs _ <- LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
forall st. LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
basicSpec LogicGraph
lg (AnyLogic, Maybe IRI)
s
    FILTERING -> AParser st FILTERING
forall (m :: * -> *) a. Monad m => a -> m a
return (FILTERING -> AParser st FILTERING)
-> (Range -> FILTERING) -> Range -> AParser st FILTERING
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> G_basic_spec -> Range -> FILTERING
FilterBasicSpec (Token -> String
tokStr Token
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
selectS) G_basic_spec
bs (Range -> AParser st FILTERING) -> Range -> AParser st FILTERING
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p
 AParser st FILTERING
-> AParser st FILTERING -> AParser st FILTERING
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
  do
    (AnyLogic, Maybe IRI)
s <- String
-> LogicGraph
-> ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI)
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m (AnyLogic, Maybe IRI)
lookupCurrentSyntax "filtering" LogicGraph
lg
    (g_symb_items_list :: G_symb_items_list
g_symb_items_list,ps :: [Token]
ps) <- AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
forall st.
AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
parseItemsList ((AnyLogic, Maybe IRI) -> AnyLogic
forall a b. (a, b) -> a
fst (AnyLogic, Maybe IRI)
s) (Map String IRI -> AParser st (G_symb_items_list, [Token]))
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String IRI
prefixes LogicGraph
lg
    FILTERING -> AParser st FILTERING
forall (m :: * -> *) a. Monad m => a -> m a
return (FILTERING -> AParser st FILTERING)
-> (Range -> FILTERING) -> Range -> AParser st FILTERING
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> G_symb_items_list -> Range -> FILTERING
FilterSymbolList (Token -> String
tokStr Token
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
selectS) 
               G_symb_items_list
g_symb_items_list (Range -> AParser st FILTERING) -> Range -> AParser st FILTERING
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange (Token
p Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)

groupSpecLookhead :: LogicGraph -> AParser st IRI
groupSpecLookhead :: LogicGraph -> AParser st IRI
groupSpecLookhead lG :: LogicGraph
lG =
  let tok2IRI :: ParsecT String (AnnoState st) Identity Token -> AParser st IRI
tok2IRI = (Token -> IRI)
-> ParsecT String (AnnoState st) Identity Token -> AParser st IRI
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> IRI
simpleIdToIRI in
  ParsecT String (AnnoState st) Identity Token -> AParser st IRI
tok2IRI ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
oBraceT AParser st IRI -> AParser st IRI -> AParser st IRI
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st IRI -> AParser st IRI -> AParser st IRI
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
followedWith (LogicGraph -> AParser st IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lG AParser st IRI
-> ParsecT String (AnnoState st) Identity [Annotation]
-> AParser st IRI
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity [Annotation]
forall st. AParser st [Annotation]
annos)
  ([AParser st IRI] -> AParser st IRI
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> AParser st IRI) -> [String] -> [AParser st IRI]
forall a b. (a -> b) -> [a] -> [b]
map (ParsecT String (AnnoState st) Identity Token -> AParser st IRI
tok2IRI (ParsecT String (AnnoState st) Identity Token -> AParser st IRI)
-> (String -> ParsecT String (AnnoState st) Identity Token)
-> String
-> AParser st IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey) [String]
criticalKeywords)
   AParser st IRI -> AParser st IRI -> AParser st IRI
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String (AnnoState st) Identity Token -> AParser st IRI
tok2IRI ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
cBraceT AParser st IRI -> AParser st IRI -> AParser st IRI
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String (AnnoState st) Identity Token -> AParser st IRI
tok2IRI ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
oBracketT AParser st IRI -> AParser st IRI -> AParser st IRI
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String (AnnoState st) Identity Token -> AParser st IRI
tok2IRI ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
cBracketT
   AParser st IRI -> AParser st IRI -> AParser st IRI
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT String (AnnoState st) Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof ParsecT String (AnnoState st) Identity ()
-> AParser st IRI -> AParser st IRI
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IRI -> AParser st IRI
forall (m :: * -> *) a. Monad m => a -> m a
return IRI
nullIRI))

minimizeKey :: AParser st Token
minimizeKey :: AParser st Token
minimizeKey = [AParser st Token] -> AParser st Token
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([AParser st Token] -> AParser st Token)
-> [AParser st Token] -> AParser st Token
forall a b. (a -> b) -> a -> b
$ (String -> AParser st Token) -> [String] -> [AParser st Token]
forall a b. (a -> b) -> [a] -> [b]
map String -> AParser st Token
forall st. String -> AParser st Token
asKey [String
minimizeS, String
closedworldS, "maximize"]

specD :: LogicGraph -> AParser st SPEC
           -- do some lookahead for free spec, to avoid clash with free type
specD :: LogicGraph -> AParser st SPEC
specD l :: LogicGraph
l = do
    Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
freeS AParser st Token
-> GenParser Char (AnnoState st) IRI -> AParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> AParser st IRI
groupSpecLookhead LogicGraph
l
    Annoted SPEC
sp <- AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st SPEC -> AParser st (Annoted SPEC))
-> AParser st SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l
    SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Free_spec Annoted SPEC
sp (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p)
  AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
cofreeS AParser st Token
-> GenParser Char (AnnoState st) IRI -> AParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> AParser st IRI
groupSpecLookhead LogicGraph
l
    Annoted SPEC
sp <- AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st SPEC -> AParser st (Annoted SPEC))
-> AParser st SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l
    SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Cofree_spec Annoted SPEC
sp (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p)
  AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
p <- AParser st Token
forall st. AParser st Token
minimizeKey AParser st Token
-> GenParser Char (AnnoState st) IRI -> AParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> AParser st IRI
groupSpecLookhead LogicGraph
l
    Annoted SPEC
sp <- AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st SPEC -> AParser st (Annoted SPEC))
-> AParser st SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l
    SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Minimize_spec Annoted SPEC
sp (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p)
  AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
closedS AParser st Token
-> GenParser Char (AnnoState st) IRI -> AParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> AParser st IRI
groupSpecLookhead LogicGraph
l
    Annoted SPEC
sp <- AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st SPEC -> AParser st (Annoted SPEC))
-> AParser st SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l
    SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Closed_spec Annoted SPEC
sp (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p)
  AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
specE LogicGraph
l

specE :: LogicGraph -> AParser st SPEC
specE :: LogicGraph -> AParser st SPEC
specE l :: LogicGraph
l = LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
logicSpec LogicGraph
l
      AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
combineSpec LogicGraph
l
      AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead (LogicGraph -> ParsecT String (AnnoState st) Identity IRI
forall st. LogicGraph -> AParser st IRI
groupSpecLookhead LogicGraph
l) ParsecT String (AnnoState st) Identity IRI
-> AParser st SPEC -> AParser st SPEC
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l)
      AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String
-> LogicGraph
-> ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI)
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m (AnyLogic, Maybe IRI)
lookupCurrentSyntax "basic spec" LogicGraph
l ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI)
-> ((AnyLogic, Maybe IRI) -> AParser st SPEC) -> AParser st SPEC
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
forall st. LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
basicSpec LogicGraph
l)

-- | call a logic specific parser if it exists
callParser :: Maybe (AParser st a) -> String -> String -> AParser st a
callParser :: Maybe (AParser st a) -> String -> String -> AParser st a
callParser p :: Maybe (AParser st a)
p name :: String
name itemType :: String
itemType =
  AParser st a -> Maybe (AParser st a) -> AParser st a
forall a. a -> Maybe a -> a
fromMaybe (String -> AParser st a
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected (String -> AParser st a) -> String -> AParser st a
forall a b. (a -> b) -> a -> b
$ "no " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
itemType String -> String -> String
forall a. [a] -> [a] -> [a]
++ " parser for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name) Maybe (AParser st a)
p

basicSpec :: LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
basicSpec :: LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
basicSpec lG :: LogicGraph
lG (Logic lid :: lid
lid, sm :: Maybe IRI
sm) = do
    Pos
p <- GenParser Char (AnnoState st) Pos
forall tok st. GenParser tok st Pos
getPos
    basic_spec
bspec <- Maybe (AParser st basic_spec)
-> String -> String -> AParser st basic_spec
forall st a.
Maybe (AParser st a) -> String -> String -> AParser st a
callParser
             (((Map String IRI -> AParser st basic_spec)
 -> AParser st basic_spec)
-> Maybe (Map String IRI -> AParser st basic_spec)
-> Maybe (AParser st basic_spec)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (\ ps :: Map String IRI -> AParser st basic_spec
ps -> Map String IRI -> AParser st basic_spec
ps (LogicGraph -> Map String IRI
prefixes LogicGraph
lG)) (Maybe IRI -> lid -> Maybe (Map String IRI -> AParser st 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 (Map String IRI -> AParser st basic_spec)
basicSpecParser Maybe IRI
sm lid
lid))
             (lid -> Maybe IRI -> String
forall lid. Language lid => lid -> Maybe IRI -> String
showSyntax lid
lid Maybe IRI
sm) "basic specification"
    Pos
q <- GenParser Char (AnnoState st) Pos
forall tok st. GenParser tok st Pos
getPos
    SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC -> AParser st SPEC) -> SPEC -> AParser st SPEC
forall a b. (a -> b) -> a -> b
$ G_basic_spec -> Range -> SPEC
Basic_spec (lid -> basic_spec -> G_basic_spec
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 -> basic_spec -> G_basic_spec
G_basic_spec lid
lid basic_spec
bspec) (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ [Pos] -> Range
Range [Pos
p, Pos
q]

logicSpec :: LogicGraph -> AParser st SPEC
logicSpec :: LogicGraph -> AParser st SPEC
logicSpec lG :: LogicGraph
lG = do
   (s1 :: Token
s1, ln :: LogicDescr
ln) <- LogicGraph -> AParser st (Token, LogicDescr)
forall st. LogicGraph -> AParser st (Token, LogicDescr)
qualification LogicGraph
lG
   AParser st (Token, LogicDescr)
-> ParsecT String (AnnoState st) Identity [(Token, LogicDescr)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (AParser st (Token, LogicDescr)
 -> ParsecT String (AnnoState st) Identity [(Token, LogicDescr)])
-> AParser st (Token, LogicDescr)
-> ParsecT String (AnnoState st) Identity [(Token, LogicDescr)]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st (Token, LogicDescr)
forall st. LogicGraph -> AParser st (Token, LogicDescr)
qualification LogicGraph
lG -- ignore multiple qualifications for now
   Token
s2 <- AParser st Token
forall st. AParser st Token
colonT
   Annoted SPEC
sp <- AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st SPEC -> AParser st (Annoted SPEC))
-> AParser st SPEC -> AParser st (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
specD (LogicGraph -> AParser st SPEC) -> LogicGraph -> AParser st SPEC
forall a b. (a -> b) -> a -> b
$ LogicDescr -> LogicGraph -> LogicGraph
setLogicName LogicDescr
ln LogicGraph
lG
   SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC -> AParser st SPEC) -> SPEC -> AParser st SPEC
forall a b. (a -> b) -> a -> b
$ LogicDescr -> Annoted SPEC -> Range -> SPEC
Qualified_spec LogicDescr
ln Annoted SPEC
sp (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
s1 [] Token
s2

combineSpec :: LogicGraph -> AParser st SPEC
combineSpec :: LogicGraph -> AParser st SPEC
combineSpec lG :: LogicGraph
lG = do
    Token
s1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
combineS
    Network
n <- LogicGraph -> AParser st Network
forall st. LogicGraph -> AParser st Network
parseNetwork LogicGraph
lG
    SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC -> AParser st SPEC) -> SPEC -> AParser st SPEC
forall a b. (a -> b) -> a -> b
$ Network -> Range -> SPEC
Combination Network
n (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
s1

parseNetwork :: LogicGraph -> AParser st Network
parseNetwork :: LogicGraph -> AParser st Network
parseNetwork lG :: LogicGraph
lG = do
    (oir :: [LABELED_ONTO_OR_INTPR_REF]
oir, ps1 :: [Token]
ps1) <- GenParser Char (AnnoState st) LABELED_ONTO_OR_INTPR_REF
-> GenParser Char (AnnoState st) Token
-> GenParser
     Char (AnnoState st) ([LABELED_ONTO_OR_INTPR_REF], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy (LogicGraph
-> GenParser Char (AnnoState st) LABELED_ONTO_OR_INTPR_REF
forall st. LogicGraph -> AParser st LABELED_ONTO_OR_INTPR_REF
parseLabeled LogicGraph
lG) GenParser Char (AnnoState st) Token
forall st. CharParser st Token
commaT
    (exl :: [IRI]
exl, ps :: [Token]
ps) <- ([IRI], [Token])
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], []) (ParsecT String (AnnoState st) Identity ([IRI], [Token])
 -> ParsecT String (AnnoState st) Identity ([IRI], [Token]))
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
forall a b. (a -> b) -> a -> b
$ do
          Token
s2 <- String -> GenParser Char (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
excludingS
          (e :: [IRI]
e, ps2 :: [Token]
ps2) <- GenParser Char (AnnoState st) IRI
-> GenParser Char (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy (LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lG) GenParser Char (AnnoState st) Token
forall st. CharParser st Token
commaT
          ([IRI], [Token])
-> ParsecT String (AnnoState st) Identity ([IRI], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([IRI]
e, Token
s2 Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps2)
    Network -> AParser st Network
forall (m :: * -> *) a. Monad m => a -> m a
return (Network -> AParser st Network) -> Network -> AParser st Network
forall a b. (a -> b) -> a -> b
$ [LABELED_ONTO_OR_INTPR_REF] -> [IRI] -> Range -> Network
Network [LABELED_ONTO_OR_INTPR_REF]
oir [IRI]
exl (Range -> Network) -> Range -> Network
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
ps1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
ps

parseLabeled :: LogicGraph -> AParser st LABELED_ONTO_OR_INTPR_REF
parseLabeled :: LogicGraph -> AParser st LABELED_ONTO_OR_INTPR_REF
parseLabeled lG :: LogicGraph
lG = do
    Maybe Token
x <- Maybe Token
-> ParsecT String (AnnoState st) Identity (Maybe Token)
-> ParsecT String (AnnoState st) Identity (Maybe Token)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option Maybe Token
forall a. Maybe a
Nothing (ParsecT String (AnnoState st) Identity (Maybe Token)
 -> ParsecT String (AnnoState st) Identity (Maybe Token))
-> ParsecT String (AnnoState st) Identity (Maybe Token)
-> ParsecT String (AnnoState st) Identity (Maybe Token)
forall a b. (a -> b) -> a -> b
$ do
        Token
str <- GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char (AnnoState st) Token
forall st. CharParser st Token
simpleId GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` GenParser Char (AnnoState st) Token
forall st. AParser st Token
colonT)
        GenParser Char (AnnoState st) Token
forall st. AParser st Token
colonT
        Maybe Token -> ParsecT String (AnnoState st) Identity (Maybe Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Token
 -> ParsecT String (AnnoState st) Identity (Maybe Token))
-> Maybe Token
-> ParsecT String (AnnoState st) Identity (Maybe Token)
forall a b. (a -> b) -> a -> b
$ Token -> Maybe Token
forall a. a -> Maybe a
Just Token
str
    IRI
y <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lG
    LABELED_ONTO_OR_INTPR_REF -> AParser st LABELED_ONTO_OR_INTPR_REF
forall (m :: * -> *) a. Monad m => a -> m a
return (LABELED_ONTO_OR_INTPR_REF -> AParser st LABELED_ONTO_OR_INTPR_REF)
-> LABELED_ONTO_OR_INTPR_REF
-> AParser st LABELED_ONTO_OR_INTPR_REF
forall a b. (a -> b) -> a -> b
$ Maybe Token -> IRI -> LABELED_ONTO_OR_INTPR_REF
Labeled Maybe Token
x IRI
y

lookupAndSetComorphismName :: String -> LogicGraph -> AParser st LogicGraph
lookupAndSetComorphismName :: String -> LogicGraph -> AParser st LogicGraph
lookupAndSetComorphismName c :: String
c lg :: LogicGraph
lg = do
    Comorphism cid :: cid
cid <- String
-> LogicGraph
-> ParsecT String (AnnoState st) Identity AnyComorphism
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyComorphism
lookupComorphism String
c LogicGraph
lg
    LogicGraph -> AParser st LogicGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (LogicGraph -> AParser st LogicGraph)
-> LogicGraph -> AParser st LogicGraph
forall a b. (a -> b) -> a -> b
$ String -> LogicGraph -> LogicGraph
setCurLogic (lid2 -> String
forall lid. Language lid => lid -> String
language_name (lid2 -> String) -> lid2 -> String
forall a b. (a -> b) -> a -> b
$ cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) LogicGraph
lg

aSpec :: LogicGraph -> AParser st (Annoted SPEC)
aSpec :: LogicGraph -> AParser st (Annoted SPEC)
aSpec = AParser st (Annoted SPEC) -> AParser st (Annoted SPEC)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (AParser st (Annoted SPEC) -> AParser st (Annoted SPEC))
-> (LogicGraph -> AParser st (Annoted SPEC))
-> LogicGraph
-> AParser st (Annoted SPEC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
spec

-- | grouped spec or spec-inst without optional DOL import
caslGroupSpec :: LogicGraph -> AParser st SPEC
caslGroupSpec :: LogicGraph -> AParser st SPEC
caslGroupSpec = Bool -> LogicGraph -> AParser st SPEC
forall st. Bool -> LogicGraph -> AParser st SPEC
groupSpecAux Bool
False

-- | grouped spec or spec-inst with optional import
groupSpec :: LogicGraph -> AParser st SPEC
groupSpec :: LogicGraph -> AParser st SPEC
groupSpec = Bool -> LogicGraph -> AParser st SPEC
forall st. Bool -> LogicGraph -> AParser st SPEC
groupSpecAux Bool
True

groupSpecAux :: Bool -> LogicGraph -> AParser st SPEC
groupSpecAux :: Bool -> LogicGraph -> AParser st SPEC
groupSpecAux withImport :: Bool
withImport l :: LogicGraph
l = do
    Token
b <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBraceT
    do
      Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
      SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC -> AParser st SPEC) -> SPEC -> AParser st SPEC
forall a b. (a -> b) -> a -> b
$ Range -> SPEC
EmptySpec (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token
b, Token
c]
     AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      Annoted SPEC
a <- LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
      AParser st ()
forall st. AParser st ()
addAnnos
      Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
      SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC -> AParser st SPEC) -> SPEC -> AParser st SPEC
forall a b. (a -> b) -> a -> b
$ Annoted SPEC -> Range -> SPEC
Group Annoted SPEC
a (Range -> SPEC) -> Range -> SPEC
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token
b, Token
c]
  AParser st SPEC -> AParser st SPEC -> AParser st SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    IRI
n <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
    (f :: [Annoted FIT_ARG]
f, ps :: Range
ps) <- LogicGraph -> AParser st ([Annoted FIT_ARG], Range)
forall st. LogicGraph -> AParser st ([Annoted FIT_ARG], Range)
fitArgs LogicGraph
l
    Maybe IRI
mi <- if Bool
withImport then GenParser Char (AnnoState st) IRI
-> ParsecT String (AnnoState st) Identity (Maybe IRI)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l) else Maybe IRI -> ParsecT String (AnnoState st) Identity (Maybe IRI)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IRI
forall a. Maybe a
Nothing
    SPEC -> AParser st SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> [Annoted FIT_ARG] -> Maybe IRI -> Range -> SPEC
Spec_inst IRI
n [Annoted FIT_ARG]
f Maybe IRI
mi Range
ps)

fitArgs :: LogicGraph -> AParser st ([Annoted FIT_ARG], Range)
fitArgs :: LogicGraph -> AParser st ([Annoted FIT_ARG], Range)
fitArgs l :: LogicGraph
l = do
  [(Annoted FIT_ARG, Range)]
fas <- ParsecT String (AnnoState st) Identity (Annoted FIT_ARG, Range)
-> ParsecT
     String (AnnoState st) Identity [(Annoted FIT_ARG, Range)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (LogicGraph
-> ParsecT String (AnnoState st) Identity (Annoted FIT_ARG, Range)
forall st. LogicGraph -> AParser st (Annoted FIT_ARG, Range)
fitArg LogicGraph
l)
  let (fas1 :: [Annoted FIT_ARG]
fas1, ps :: [Range]
ps) = [(Annoted FIT_ARG, Range)] -> ([Annoted FIT_ARG], [Range])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Annoted FIT_ARG, Range)]
fas
  ([Annoted FIT_ARG], Range) -> AParser st ([Annoted FIT_ARG], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted FIT_ARG]
fas1, (Range -> Range) -> [Range] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange Range -> Range
forall a. a -> a
id [Range]
ps)

fitArg :: LogicGraph -> AParser st (Annoted FIT_ARG, Range)
fitArg :: LogicGraph -> AParser st (Annoted FIT_ARG, Range)
fitArg l :: LogicGraph
l = do
  Token
b <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
  Annoted FIT_ARG
fa <- AParser st FIT_ARG -> AParser st (Annoted FIT_ARG)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (LogicGraph -> AParser st FIT_ARG
forall st. LogicGraph -> AParser st FIT_ARG
fittingArg LogicGraph
l)
  Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
  (Annoted FIT_ARG, Range) -> AParser st (Annoted FIT_ARG, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted FIT_ARG
fa, Token -> [Token] -> Token -> Range
toRange Token
b [] Token
c)

fittingArg :: LogicGraph -> AParser st FIT_ARG
fittingArg :: LogicGraph -> AParser st FIT_ARG
fittingArg l :: LogicGraph
l = do
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
viewS
    IRI
vn <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
    (fa :: [Annoted FIT_ARG]
fa, ps :: Range
ps) <- LogicGraph -> AParser st ([Annoted FIT_ARG], Range)
forall st. LogicGraph -> AParser st ([Annoted FIT_ARG], Range)
fitArgs LogicGraph
l
    FIT_ARG -> AParser st FIT_ARG
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> [Annoted FIT_ARG] -> Range -> FIT_ARG
Fit_view IRI
vn [Annoted FIT_ARG]
fa (Token -> Range
tokPos Token
s Range -> Range -> Range
`appRange` Range
ps))
  AParser st FIT_ARG -> AParser st FIT_ARG -> AParser st FIT_ARG
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Annoted SPEC
sp <- LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
    (symbit :: [G_mapping]
symbit, ps :: Range
ps) <- ([G_mapping], Range)
-> ParsecT String (AnnoState st) Identity ([G_mapping], Range)
-> ParsecT String (AnnoState st) Identity ([G_mapping], Range)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], Range
nullRange) (ParsecT String (AnnoState st) Identity ([G_mapping], Range)
 -> ParsecT String (AnnoState st) Identity ([G_mapping], Range))
-> ParsecT String (AnnoState st) Identity ([G_mapping], Range)
-> ParsecT String (AnnoState st) Identity ([G_mapping], Range)
forall a b. (a -> b) -> a -> b
$ do
        Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
fitS
        (m :: [G_mapping]
m, qs :: [Token]
qs) <- LogicGraph -> AParser st ([G_mapping], [Token])
forall st. LogicGraph -> AParser st ([G_mapping], [Token])
parseMapping LogicGraph
l
        ([G_mapping], Range)
-> ParsecT String (AnnoState st) Identity ([G_mapping], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([G_mapping]
m, [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
s Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
qs)
    FIT_ARG -> AParser st FIT_ARG
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> [G_mapping] -> Range -> FIT_ARG
Fit_spec Annoted SPEC
sp [G_mapping]
symbit Range
ps)


parseCorrespondences :: LogicGraph -> AParser st [CORRESPONDENCE]
parseCorrespondences :: LogicGraph -> AParser st [CORRESPONDENCE]
parseCorrespondences l :: LogicGraph
l = CharParser (AnnoState st) CORRESPONDENCE
-> AParser st [CORRESPONDENCE]
forall st a. CharParser st a -> CharParser st [a]
commaSep1 (CharParser (AnnoState st) CORRESPONDENCE
 -> AParser st [CORRESPONDENCE])
-> CharParser (AnnoState st) CORRESPONDENCE
-> AParser st [CORRESPONDENCE]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> CharParser (AnnoState st) CORRESPONDENCE
forall st. LogicGraph -> AParser st CORRESPONDENCE
correspondence LogicGraph
l

correspondence :: LogicGraph -> AParser st CORRESPONDENCE
correspondence :: LogicGraph -> AParser st CORRESPONDENCE
correspondence l :: LogicGraph
l = do
    String -> AParser st Token
forall st. String -> AParser st Token
asKey "*"
    CORRESPONDENCE -> AParser st CORRESPONDENCE
forall (m :: * -> *) a. Monad m => a -> m a
return CORRESPONDENCE
Default_correspondence
  AParser st CORRESPONDENCE
-> AParser st CORRESPONDENCE -> AParser st CORRESPONDENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    String -> AParser st Token
forall st. String -> AParser st Token
asKey String
relationS
    Maybe RELATION_REF
rref <- ParsecT String (AnnoState st) Identity RELATION_REF
-> ParsecT String (AnnoState st) Identity (Maybe RELATION_REF)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String (AnnoState st) Identity RELATION_REF
 -> ParsecT String (AnnoState st) Identity (Maybe RELATION_REF))
-> ParsecT String (AnnoState st) Identity RELATION_REF
-> ParsecT String (AnnoState st) Identity (Maybe RELATION_REF)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> ParsecT String (AnnoState st) Identity RELATION_REF
forall st. LogicGraph -> AParser st RELATION_REF
relationRef LogicGraph
l
    Maybe Double
conf <- ParsecT String (AnnoState st) Identity Double
-> ParsecT String (AnnoState st) Identity (Maybe Double)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT String (AnnoState st) Identity Double
forall st. AParser st Double
confidence
    AParser st Token
forall st. CharParser st Token
oBraceT
    [CORRESPONDENCE]
cs <- LogicGraph -> AParser st [CORRESPONDENCE]
forall st. LogicGraph -> AParser st [CORRESPONDENCE]
parseCorrespondences LogicGraph
l
    AParser st Token
forall st. CharParser st Token
cBraceT
    CORRESPONDENCE -> AParser st CORRESPONDENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (CORRESPONDENCE -> AParser st CORRESPONDENCE)
-> CORRESPONDENCE -> AParser st CORRESPONDENCE
forall a b. (a -> b) -> a -> b
$ Maybe RELATION_REF
-> Maybe Double -> [CORRESPONDENCE] -> CORRESPONDENCE
Correspondence_block Maybe RELATION_REF
rref Maybe Double
conf [CORRESPONDENCE]
cs
  AParser st CORRESPONDENCE
-> AParser st CORRESPONDENCE -> AParser st CORRESPONDENCE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (mcid :: Maybe Annotation
mcid, eRef :: G_symb_items_list
eRef, mrRef :: Maybe RELATION_REF
mrRef, mconf :: Maybe Double
mconf, toer :: G_symb_items_list
toer) <- LogicGraph
-> AParser
     st
     (Maybe Annotation, G_symb_items_list, Maybe RELATION_REF,
      Maybe Double, G_symb_items_list)
forall st.
LogicGraph
-> AParser
     st
     (Maybe Annotation, G_symb_items_list, Maybe RELATION_REF,
      Maybe Double, G_symb_items_list)
corr1 LogicGraph
l
    {- trace (concat ["\t", show mcid, "    \t", show eRef, "\t", show mrRef,
       "    \t", show mconf, "   \t", show toer]) $ return ()
    only commented out for future debugging purposes -}
    CORRESPONDENCE -> AParser st CORRESPONDENCE
forall (m :: * -> *) a. Monad m => a -> m a
return (CORRESPONDENCE -> AParser st CORRESPONDENCE)
-> CORRESPONDENCE -> AParser st CORRESPONDENCE
forall a b. (a -> b) -> a -> b
$ Maybe Annotation
-> G_symb_items_list
-> G_symb_items_list
-> Maybe RELATION_REF
-> Maybe Double
-> CORRESPONDENCE
Single_correspondence Maybe Annotation
mcid G_symb_items_list
eRef G_symb_items_list
toer Maybe RELATION_REF
mrRef Maybe Double
mconf

corr1 :: LogicGraph
      -> AParser st ( Maybe Annotation, G_symb_items_list
                    , Maybe RELATION_REF, Maybe CONFIDENCE, G_symb_items_list)
corr1 :: LogicGraph
-> AParser
     st
     (Maybe Annotation, G_symb_items_list, Maybe RELATION_REF,
      Maybe Double, G_symb_items_list)
corr1 l :: LogicGraph
l = do
    AnyLogic
al <- String
-> LogicGraph -> ParsecT String (AnnoState st) Identity AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "correspondence" LogicGraph
l
    (eRef :: G_symb_items_list
eRef, _) <- AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
forall st.
AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
parseSingleSymb AnyLogic
al (Map String IRI -> AParser st (G_symb_items_list, [Token]))
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String IRI
prefixes LogicGraph
l
    (mrRef :: Maybe RELATION_REF
mrRef, mconf :: Maybe Double
mconf, toer :: G_symb_items_list
toer) <- LogicGraph
-> AParser st (Maybe RELATION_REF, Maybe Double, G_symb_items_list)
forall st.
LogicGraph
-> AParser st (Maybe RELATION_REF, Maybe Double, G_symb_items_list)
corr2 LogicGraph
l
    [Annotation]
cids <- GenParser Char (AnnoState st) [Annotation]
forall st. GenParser Char st [Annotation]
annotations
    if Bool -> Bool
not ([Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annotation]
cids Bool -> Bool -> Bool
|| [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Annotation] -> [Annotation]
forall a. [a] -> [a]
tail [Annotation]
cids))
      then String
-> AParser
     st
     (Maybe Annotation, G_symb_items_list, Maybe RELATION_REF,
      Maybe Double, G_symb_items_list)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "more than one correspondence id"
      else (Maybe Annotation, G_symb_items_list, Maybe RELATION_REF,
 Maybe Double, G_symb_items_list)
-> AParser
     st
     (Maybe Annotation, G_symb_items_list, Maybe RELATION_REF,
      Maybe Double, G_symb_items_list)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annotation] -> Maybe Annotation
forall a. [a] -> Maybe a
listToMaybe [Annotation]
cids, G_symb_items_list
eRef, Maybe RELATION_REF
mrRef, Maybe Double
mconf, G_symb_items_list
toer)

corr2 :: LogicGraph
      -> AParser st (Maybe RELATION_REF, Maybe CONFIDENCE, G_symb_items_list)
corr2 :: LogicGraph
-> AParser st (Maybe RELATION_REF, Maybe Double, G_symb_items_list)
corr2 l :: LogicGraph
l = do
    Maybe RELATION_REF
rRef <- ParsecT String (AnnoState st) Identity RELATION_REF
-> ParsecT String (AnnoState st) Identity (Maybe RELATION_REF)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String (AnnoState st) Identity RELATION_REF
 -> ParsecT String (AnnoState st) Identity (Maybe RELATION_REF))
-> (ParsecT String (AnnoState st) Identity RELATION_REF
    -> ParsecT String (AnnoState st) Identity RELATION_REF)
-> ParsecT String (AnnoState st) Identity RELATION_REF
-> ParsecT String (AnnoState st) Identity (Maybe RELATION_REF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParsecT String (AnnoState st) Identity RELATION_REF
-> ParsecT String (AnnoState st) Identity RELATION_REF
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String (AnnoState st) Identity RELATION_REF
 -> ParsecT String (AnnoState st) Identity (Maybe RELATION_REF))
-> ParsecT String (AnnoState st) Identity RELATION_REF
-> ParsecT String (AnnoState st) Identity (Maybe RELATION_REF)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> ParsecT String (AnnoState st) Identity RELATION_REF
forall st. LogicGraph -> AParser st RELATION_REF
relationRefWithLookAhead LogicGraph
l
    (mconf :: Maybe Double
mconf, toer :: G_symb_items_list
toer) <- LogicGraph -> AParser st (Maybe Double, G_symb_items_list)
forall st.
LogicGraph -> AParser st (Maybe Double, G_symb_items_list)
corr3 LogicGraph
l
    (Maybe RELATION_REF, Maybe Double, G_symb_items_list)
-> AParser st (Maybe RELATION_REF, Maybe Double, G_symb_items_list)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe RELATION_REF
rRef, Maybe Double
mconf, G_symb_items_list
toer)

corr3 :: LogicGraph -> AParser st (Maybe CONFIDENCE, G_symb_items_list)
corr3 :: LogicGraph -> AParser st (Maybe Double, G_symb_items_list)
corr3 l :: LogicGraph
l = do
    AnyLogic
al <- String
-> LogicGraph -> ParsecT String (AnnoState st) Identity AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "corr3" LogicGraph
l
    Maybe Double
conf <- ParsecT String (AnnoState st) Identity Double
-> ParsecT String (AnnoState st) Identity (Maybe Double)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String (AnnoState st) Identity Double
 -> ParsecT String (AnnoState st) Identity (Maybe Double))
-> ParsecT String (AnnoState st) Identity Double
-> ParsecT String (AnnoState st) Identity (Maybe Double)
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity Double
-> ParsecT String (AnnoState st) Identity Double
forall tok st a. GenParser tok st a -> GenParser tok st a
try ParsecT String (AnnoState st) Identity Double
forall st. AParser st Double
confidence
    (sym :: G_symb_items_list
sym, _) <- AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
forall st.
AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
parseSingleSymb AnyLogic
al (Map String IRI -> AParser st (G_symb_items_list, [Token]))
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String IRI
prefixes LogicGraph
l
    (Maybe Double, G_symb_items_list)
-> AParser st (Maybe Double, G_symb_items_list)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Double
conf, G_symb_items_list
sym)

relationRefWithLookAhead :: LogicGraph -> AParser st RELATION_REF
relationRefWithLookAhead :: LogicGraph -> AParser st RELATION_REF
relationRefWithLookAhead lG :: LogicGraph
lG = do
    RELATION_REF
r <- LogicGraph -> AParser st RELATION_REF
forall st. LogicGraph -> AParser st RELATION_REF
relationRef LogicGraph
lG
    ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead (AParser st Char
forall st. AParser st Char
confidenceBegin AParser st Char
-> ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IRI -> ParsecT String (AnnoState st) Identity IRI
forall (m :: * -> *) a. Monad m => a -> m a
return IRI
nullIRI)
      ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead (ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String (AnnoState st) Identity IRI
 -> ParsecT String (AnnoState st) Identity IRI)
-> ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity IRI
forall a b. (a -> b) -> a -> b
$ LogicGraph -> ParsecT String (AnnoState st) Identity IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lG)
    RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION_REF
r

relationRef :: LogicGraph -> AParser st RELATION_REF
relationRef :: LogicGraph -> AParser st RELATION_REF
relationRef lG :: LogicGraph
lG = do
      String -> AParser st Token
forall st. String -> AParser st Token
asKey ">"
      RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION_REF
Subsumes
    AParser st RELATION_REF
-> AParser st RELATION_REF -> AParser st RELATION_REF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      String -> AParser st Token
forall st. String -> AParser st Token
asKey "<"
      RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION_REF
IsSubsumed
    AParser st RELATION_REF
-> AParser st RELATION_REF -> AParser st RELATION_REF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      String -> AParser st Token
forall st. String -> AParser st Token
asKey "="
      RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION_REF
Equivalent
    AParser st RELATION_REF
-> AParser st RELATION_REF -> AParser st RELATION_REF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      String -> AParser st Token
forall st. String -> AParser st Token
asKey "%"
      RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION_REF
Incompatible
    AParser st RELATION_REF
-> AParser st RELATION_REF -> AParser st RELATION_REF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      AParser st Token -> AParser st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (AParser st Token -> AParser st Token)
-> AParser st Token -> AParser st Token
forall a b. (a -> b) -> a -> b
$ String -> AParser st Token
forall st. String -> AParser st Token
asKey "ni"
      RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION_REF
HasInstance
    AParser st RELATION_REF
-> AParser st RELATION_REF -> AParser st RELATION_REF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      AParser st Token -> AParser st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (AParser st Token -> AParser st Token)
-> AParser st Token -> AParser st Token
forall a b. (a -> b) -> a -> b
$ String -> AParser st Token
forall st. String -> AParser st Token
asKey "in"
      RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION_REF
InstanceOf
     AParser st RELATION_REF
-> AParser st RELATION_REF -> AParser st RELATION_REF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      AParser st Token -> AParser st Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (AParser st Token -> AParser st Token)
-> AParser st Token -> AParser st Token
forall a b. (a -> b) -> a -> b
$ String -> AParser st Token
forall st. String -> AParser st Token
asKey String
mapsTo
      RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION_REF
DefaultRelation
 AParser st RELATION_REF
-> AParser st RELATION_REF -> AParser st RELATION_REF
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    IRI
i <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lG
    RELATION_REF -> AParser st RELATION_REF
forall (m :: * -> *) a. Monad m => a -> m a
return (RELATION_REF -> AParser st RELATION_REF)
-> RELATION_REF -> AParser st RELATION_REF
forall a b. (a -> b) -> a -> b
$ IRI -> RELATION_REF
Iri IRI
i

confidenceBegin :: AParser st Char
confidenceBegin :: AParser st Char
confidenceBegin = Char -> AParser st Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '0' AParser st Char -> AParser st Char -> AParser st Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> AParser st Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '1'

confidence :: AParser st Double
confidence :: AParser st Double
confidence = AParser st Double
forall st. AParser st Double
confidenceNumber AParser st Double
-> ParsecT String (AnnoState st) Identity () -> AParser st Double
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. CharParser st ()
skipSmart

confidenceNumber :: AParser st Double
confidenceNumber :: AParser st Double
confidenceNumber = do
    Char
d1 <- Char -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '0'
    Double -> AParser st Double -> AParser st Double
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option 0 (AParser st Double -> AParser st Double)
-> AParser st Double -> AParser st Double
forall a b. (a -> b) -> a -> b
$ do
          Char
d2 <- Char -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.'
          String
ds <- ParsecT String (AnnoState st) Identity Char
-> ParsecT String (AnnoState st) Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
          Double -> AParser st Double
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> AParser st Double) -> Double -> AParser st Double
forall a b. (a -> b) -> a -> b
$ String -> Double
forall a. Read a => String -> a
read (String -> Double) -> String -> Double
forall a b. (a -> b) -> a -> b
$ Char
d1 Char -> String -> String
forall a. a -> [a] -> [a]
: Char
d2 Char -> String -> String
forall a. a -> [a] -> [a]
: String
ds
  AParser st Double -> AParser st Double -> AParser st Double
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Char -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '1'
    Double -> AParser st Double -> AParser st Double
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option 1 (AParser st Double -> AParser st Double)
-> AParser st Double -> AParser st Double
forall a b. (a -> b) -> a -> b
$ do
          Char -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.'
          ParsecT String (AnnoState st) Identity Char
-> ParsecT String (AnnoState st) Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String (AnnoState st) Identity Char
 -> ParsecT String (AnnoState st) Identity String)
-> ParsecT String (AnnoState st) Identity Char
-> ParsecT String (AnnoState st) Identity String
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '0'
          Double -> AParser st Double
forall (m :: * -> *) a. Monad m => a -> m a
return 1