{- |
Module      :  ./Syntax/Parse_AS_Library.hs
Description :  parser for DOL documents and CASL specification librariess
Copyright   :  (c) Maciek Makowski, 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 specification libraries
   Follows Sect. II:3.1.5 of the CASL Reference Manual.
Parser for DOL documents
   Follows the DOL OMG standard, clause 9.3
-}

module Syntax.Parse_AS_Library (library) where

import Logic.Grothendieck
import Syntax.AS_Structured
import Syntax.AS_Library
import Syntax.Parse_AS_Structured
import Syntax.Parse_AS_Architecture

import Common.AS_Annotation
import Common.AnnoParser
import Common.AnnoState
import Common.Id
import Common.IRI

import Common.Keywords
import Common.Lexer
import Common.LibName
import Common.Parsec
import Common.Token

import Text.ParserCombinators.Parsec
import Data.List
import Data.Maybe (maybeToList)
import qualified Data.Map as Map
import Control.Monad
import qualified Control.Monad.Fail as Fail

import Framework.AS

lGAnnos :: LogicGraph -> AParser st (LogicGraph, [Annotation])
lGAnnos :: LogicGraph -> AParser st (LogicGraph, [Annotation])
lGAnnos lG :: LogicGraph
lG = do
  [Annotation]
as <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
  let (pfx :: Map String IRI
pfx, _) = [Annotation] -> (Map String IRI, [Annotation])
partPrefixes [Annotation]
as
  (LogicGraph, [Annotation]) -> AParser st (LogicGraph, [Annotation])
forall (m :: * -> *) a. Monad m => a -> m a
return (LogicGraph
lG { prefixes :: Map String IRI
prefixes = Map String IRI -> Map String IRI -> Map String IRI
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map String IRI
pfx (Map String IRI -> Map String IRI)
-> Map String IRI -> Map String IRI
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String IRI
prefixes LogicGraph
lG }, [Annotation]
as)

-- * Parsing functions

-- | Parse a library of specifications
library :: LogicGraph -> AParser st LIB_DEFN
library :: LogicGraph -> AParser st LIB_DEFN
library lG :: LogicGraph
lG = do
    (lG1 :: LogicGraph
lG1, an1 :: [Annotation]
an1) <- LogicGraph -> AParser st (LogicGraph, [Annotation])
forall st. LogicGraph -> AParser st (LogicGraph, [Annotation])
lGAnnos LogicGraph
lG
    (ps :: Range
ps, ln :: LibName
ln) <- (Range, LibName)
-> ParsecT String (AnnoState st) Identity (Range, LibName)
-> ParsecT String (AnnoState st) Identity (Range, LibName)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (Range
nullRange, IRI -> LibName
iriLibName IRI
nullIRI) (ParsecT String (AnnoState st) Identity (Range, LibName)
 -> ParsecT String (AnnoState st) Identity (Range, LibName))
-> ParsecT String (AnnoState st) Identity (Range, LibName)
-> ParsecT String (AnnoState st) Identity (Range, LibName)
forall a b. (a -> b) -> a -> b
$ do
      Token
s1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
libraryS 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 "distributed-ontology"
      LibName
n <- LogicGraph -> AParser st LibName
forall st. LogicGraph -> AParser st LibName
libName LogicGraph
lG1
      (Range, LibName)
-> ParsecT String (AnnoState st) Identity (Range, LibName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Range
tokPos Token
s1, LibName
n)
    (lG2 :: LogicGraph
lG2, an2 :: [Annotation]
an2) <- LogicGraph -> AParser st (LogicGraph, [Annotation])
forall st. LogicGraph -> AParser st (LogicGraph, [Annotation])
lGAnnos LogicGraph
lG1
    [Annoted LIB_ITEM]
ls <- LogicGraph -> AParser st [Annoted LIB_ITEM]
forall st. LogicGraph -> AParser st [Annoted LIB_ITEM]
libItems LogicGraph
lG2
    LIB_DEFN -> AParser st LIB_DEFN
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn LibName
ln [Annoted LIB_ITEM]
ls Range
ps ([Annotation]
an1 [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
an2))

-- | Parse library name
-- For expanding the iri of the library name the empty prefix is to `"file://"
-- to parse the it as an individual file. Otherwise the default empty prefix
-- would be used.
libName :: LogicGraph -> AParser st LibName
libName :: LogicGraph -> AParser st LibName
libName lG :: LogicGraph
lG = (IRI -> Maybe VersionNumber -> LibName)
-> ParsecT String (AnnoState st) Identity IRI
-> ParsecT String (AnnoState st) Identity (Maybe VersionNumber)
-> AParser st LibName
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 IRI -> Maybe VersionNumber -> LibName
mkLibName (LogicGraph -> ParsecT String (AnnoState st) Identity IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
lG')
  (ParsecT String (AnnoState st) Identity (Maybe VersionNumber)
 -> AParser st LibName)
-> ParsecT String (AnnoState st) Identity (Maybe VersionNumber)
-> AParser st LibName
forall a b. (a -> b) -> a -> b
$ if LogicGraph -> Bool
dolOnly LogicGraph
lG then Maybe VersionNumber
-> ParsecT String (AnnoState st) Identity (Maybe VersionNumber)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe VersionNumber
forall a. Maybe a
Nothing else ParsecT String (AnnoState st) Identity VersionNumber
-> ParsecT String (AnnoState st) Identity (Maybe VersionNumber)
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 VersionNumber
forall st. AParser st VersionNumber
version
  where
    fileIRI :: IRI
fileIRI = IRI
nullIRI { iriScheme :: String
iriScheme = "file://"}
    pm :: Map String IRI
pm = String -> IRI -> Map String IRI -> Map String IRI
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert "" IRI
fileIRI (Map String IRI -> Map String IRI)
-> Map String IRI -> Map String IRI
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String IRI
prefixes LogicGraph
lG
    lG' :: LogicGraph
lG' = LogicGraph
lG {prefixes :: Map String IRI
prefixes = Map String IRI
pm}

-- | Parse the library version
version :: AParser st VersionNumber
version :: AParser st VersionNumber
version = do
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
versionS
    Pos
pos <- GenParser Char (AnnoState st) Pos
forall tok st. GenParser tok st Pos
getPos
    [String]
n <- ParsecT String (AnnoState st) Identity String
-> ParsecT String (AnnoState st) Identity String
-> ParsecT String (AnnoState st) Identity [String]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 (ParsecT String (AnnoState st) Identity Char
-> ParsecT String (AnnoState st) Identity String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit) (String -> ParsecT String (AnnoState st) Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
dotS)
    CharParser (AnnoState st) ()
forall st. CharParser st ()
skip
    VersionNumber -> AParser st VersionNumber
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> Range -> VersionNumber
VersionNumber [String]
n (Token -> Range
tokPos Token
s Range -> Range -> Range
`appRange` [Pos] -> Range
Range [Pos
pos]))

-- | Parse the library elements
libItems :: LogicGraph -> AParser st [Annoted LIB_ITEM]
libItems :: LogicGraph -> AParser st [Annoted LIB_ITEM]
libItems l :: LogicGraph
l =
     (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 [Annoted LIB_ITEM] -> AParser st [Annoted LIB_ITEM]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Annoted LIB_ITEM] -> AParser st [Annoted LIB_ITEM]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
    AParser st [Annoted LIB_ITEM]
-> AParser st [Annoted LIB_ITEM] -> AParser st [Annoted LIB_ITEM]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      LIB_ITEM
r <- LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
libItem LogicGraph
l
      [Annotation]
la <- AParser st [Annotation]
forall st. AParser st [Annotation]
lineAnnos
      (l' :: LogicGraph
l', an :: [Annotation]
an) <- LogicGraph -> AParser st (LogicGraph, [Annotation])
forall st. LogicGraph -> AParser st (LogicGraph, [Annotation])
lGAnnos LogicGraph
l
      [Annoted LIB_ITEM]
is <- LogicGraph -> AParser st [Annoted LIB_ITEM]
forall st. LogicGraph -> AParser st [Annoted LIB_ITEM]
libItems (case LIB_ITEM
r of
             Logic_decl logD :: LogicDescr
logD _ ->
                 LogicDescr -> LogicGraph -> LogicGraph
setLogicName LogicDescr
logD LogicGraph
l'
             _ -> LogicGraph
l')
      case [Annoted LIB_ITEM]
is of
        [] -> [Annoted LIB_ITEM] -> AParser st [Annoted LIB_ITEM]
forall (m :: * -> *) a. Monad m => a -> m a
return [LIB_ITEM
-> Range -> [Annotation] -> [Annotation] -> Annoted LIB_ITEM
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted LIB_ITEM
r Range
nullRange [] ([Annotation] -> Annoted LIB_ITEM)
-> [Annotation] -> Annoted LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Annotation]
la [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
an]
        Annoted i :: LIB_ITEM
i p :: Range
p nl :: [Annotation]
nl ra :: [Annotation]
ra : rs :: [Annoted LIB_ITEM]
rs ->
          [Annoted LIB_ITEM] -> AParser st [Annoted LIB_ITEM]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted LIB_ITEM] -> AParser st [Annoted LIB_ITEM])
-> [Annoted LIB_ITEM] -> AParser st [Annoted LIB_ITEM]
forall a b. (a -> b) -> a -> b
$ LIB_ITEM
-> Range -> [Annotation] -> [Annotation] -> Annoted LIB_ITEM
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted LIB_ITEM
r Range
nullRange [] [Annotation]
la Annoted LIB_ITEM -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. a -> [a] -> [a]
: LIB_ITEM
-> Range -> [Annotation] -> [Annotation] -> Annoted LIB_ITEM
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted LIB_ITEM
i Range
p ([Annotation]
an [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
nl) [Annotation]
ra Annoted LIB_ITEM -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. a -> [a] -> [a]
: [Annoted LIB_ITEM]
rs

dolImportItem :: LogicGraph -> AParser st LIB_ITEM
dolImportItem :: LogicGraph -> AParser st LIB_ITEM
dolImportItem l :: LogicGraph
l = do
    Token
s1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "import"
    LibName
iln <- LogicGraph -> AParser st LibName
forall st. LogicGraph -> AParser st LibName
libName LogicGraph
l
    LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName -> DownloadItems -> Range -> LIB_ITEM
Download_items LibName
iln ([ItemNameMap] -> DownloadItems
ItemMaps []) (Range -> LIB_ITEM) -> Range -> LIB_ITEM
forall a b. (a -> b) -> a -> b
$ Token -> Range
forall a. GetRange a => a -> Range
getRange Token
s1)

networkDefn :: LogicGraph -> AParser st LIB_ITEM
networkDefn :: LogicGraph -> AParser st LIB_ITEM
networkDefn l :: LogicGraph
l = do
    Token
kGraph <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "network"
    IRI
name <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
    Token
kEqu <- AParser st Token
forall st. AParser st Token
equalT
    Network
n <- LogicGraph -> AParser st Network
forall st. LogicGraph -> AParser st Network
parseNetwork LogicGraph
l
    Token
kEnd <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
endS
    LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> Network -> Range -> LIB_ITEM
Network_defn IRI
name Network
n
         (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Token
kGraph, Token
kEqu, Token
kEnd]

-- CASL spec-defn or DOL OMSDefn
specDefn :: LogicGraph -> AParser st LIB_ITEM
specDefn :: LogicGraph -> AParser st LIB_ITEM
specDefn l :: LogicGraph
l = do
    Token
s <- [ParsecT String (AnnoState st) Identity Token]
-> ParsecT String (AnnoState st) Identity Token
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([ParsecT String (AnnoState st) Identity Token]
 -> ParsecT String (AnnoState st) Identity Token)
-> [ParsecT String (AnnoState st) Identity Token]
-> ParsecT String (AnnoState st) Identity Token
forall a b. (a -> b) -> a -> b
$ (String -> ParsecT String (AnnoState st) Identity Token)
-> [String] -> [ParsecT String (AnnoState st) Identity Token]
forall a b. (a -> b) -> [a] -> [b]
map String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey
      ["specification", String
specS, String
ontologyS, "onto", "model", "OMS", String
patternS]
    IRI
n <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
    GENERICITY
g <- LogicGraph -> AParser st GENERICITY
forall st. LogicGraph -> AParser st GENERICITY
generics LogicGraph
l
    Token
e <- ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
equalT
    Annoted SPEC
a <- LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
    Maybe Token
q <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
    LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> GENERICITY -> Annoted SPEC -> Range -> LIB_ITEM
Spec_defn IRI
n GENERICITY
g Annoted SPEC
a
      (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Token
s, Token
e] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
q

-- CASL view-defn or DOL IntprDefn
viewDefn :: LogicGraph -> AParser st LIB_ITEM
viewDefn :: LogicGraph -> AParser st LIB_ITEM
viewDefn l :: LogicGraph
l = do
    Token
s1 <- [ParsecT String (AnnoState st) Identity Token]
-> ParsecT String (AnnoState st) Identity Token
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([ParsecT String (AnnoState st) Identity Token]
 -> ParsecT String (AnnoState st) Identity Token)
-> [ParsecT String (AnnoState st) Identity Token]
-> ParsecT String (AnnoState st) Identity Token
forall a b. (a -> b) -> a -> b
$ (String -> ParsecT String (AnnoState st) Identity Token)
-> [String] -> [ParsecT String (AnnoState st) Identity Token]
forall a b. (a -> b) -> [a] -> [b]
map String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey [String
viewS, String
interpretationS, String
refinementS]
    IRI
vn <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
    do
       Token
kEqu <- ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
equalT
       REF_SPEC
rsp <- LogicGraph -> AParser st REF_SPEC
forall st. LogicGraph -> AParser st REF_SPEC
refSpec LogicGraph
l
       Maybe Token
kEnd <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> REF_SPEC -> Range -> LIB_ITEM
Ref_spec_defn IRI
vn REF_SPEC
rsp
                   (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Token
s1, Token
kEqu] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
kEnd
      AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
       GENERICITY
g <- LogicGraph -> AParser st GENERICITY
forall st. LogicGraph -> AParser st GENERICITY
generics LogicGraph
l
       [Annotation]
_ <- GenParser Char (AnnoState st) [Annotation]
forall st. GenParser Char st [Annotation]
annotations -- TODO: store annotations
       Token
s2 <- ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
colonT
       VIEW_TYPE
vt <- LogicGraph -> AParser st VIEW_TYPE
forall st. LogicGraph -> AParser st VIEW_TYPE
viewType LogicGraph
l
       (symbMap :: [G_mapping]
symbMap, ps :: [Token]
ps) <- ([G_mapping], [Token])
-> ParsecT String (AnnoState st) Identity ([G_mapping], [Token])
-> ParsecT String (AnnoState st) Identity ([G_mapping], [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 ([G_mapping], [Token])
 -> ParsecT String (AnnoState st) Identity ([G_mapping], [Token]))
-> ParsecT String (AnnoState st) Identity ([G_mapping], [Token])
-> ParsecT String (AnnoState st) Identity ([G_mapping], [Token])
forall a b. (a -> b) -> a -> b
$ do
         Token
s <- ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
equalT
         (m :: [G_mapping]
m, _) <- LogicGraph
-> ParsecT String (AnnoState st) Identity ([G_mapping], [Token])
forall st. LogicGraph -> AParser st ([G_mapping], [Token])
parseMapping LogicGraph
l
         ([G_mapping], [Token])
-> ParsecT String (AnnoState st) Identity ([G_mapping], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([G_mapping]
m, [Token
s])
       Maybe Token
q <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range -> LIB_ITEM
View_defn IRI
vn GENERICITY
g VIEW_TYPE
vt [G_mapping]
symbMap
         (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Token
s1, Token
s2] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
q

entailDefn :: LogicGraph -> AParser st LIB_ITEM
entailDefn :: LogicGraph -> AParser st LIB_ITEM
entailDefn l :: LogicGraph
l = do
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
entailmentS
  IRI
n <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
  Token
e <- AParser st Token
forall st. AParser st Token
equalT
  ENTAIL_TYPE
et <- LogicGraph -> AParser st ENTAIL_TYPE
forall st. LogicGraph -> AParser st ENTAIL_TYPE
entailType LogicGraph
l
  Maybe Token
q <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
  LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> ENTAIL_TYPE -> Range -> LIB_ITEM
Entail_defn IRI
n ENTAIL_TYPE
et (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Token
s, Token
e] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
q

queryDefn :: LogicGraph -> AParser st LIB_ITEM
queryDefn :: LogicGraph -> AParser st LIB_ITEM
queryDefn l :: LogicGraph
l = do
  Token
q <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "query"
  IRI
n <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
  Token
e <- AParser st Token
forall st. AParser st Token
equalT
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
selectS
  AnyLogic
lg <- String
-> LogicGraph -> ParsecT String (AnnoState st) Identity AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "query-defn" LogicGraph
l
  (vs :: G_symb_items_list
vs, cs :: [Token]
cs) <- 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
lg (LogicGraph -> Map String IRI
prefixes LogicGraph
l)
  Token
w <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
whereS
  Basic_spec bs :: G_basic_spec
bs _ <- String
-> LogicGraph
-> ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI)
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m (AnyLogic, Maybe IRI)
lookupCurrentSyntax "query-defn" LogicGraph
l ParsecT String (AnnoState st) Identity (AnyLogic, Maybe IRI)
-> ((AnyLogic, Maybe IRI)
    -> ParsecT String (AnnoState st) Identity SPEC)
-> ParsecT String (AnnoState st) Identity SPEC
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LogicGraph
-> (AnyLogic, Maybe IRI)
-> ParsecT String (AnnoState st) Identity SPEC
forall st. LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC
basicSpec LogicGraph
l
  Token
i <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
inS
  Annoted SPEC
oms <- LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
  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
$ String -> AParser st Token
forall st. String -> AParser st Token
asKey "along" AParser st Token
-> GenParser Char (AnnoState st) IRI
-> GenParser Char (AnnoState st) IRI
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
  Maybe Token
o <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
  LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI
-> G_symb_items_list
-> G_basic_spec
-> Annoted SPEC
-> Maybe IRI
-> Range
-> LIB_ITEM
Query_defn IRI
n G_symb_items_list
vs G_basic_spec
bs Annoted SPEC
oms Maybe IRI
mt (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange
    ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Token
q, Token
e, Token
s, Token
w] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
i] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
o

substDefn :: LogicGraph -> AParser st LIB_ITEM
substDefn :: LogicGraph -> AParser st LIB_ITEM
substDefn l :: LogicGraph
l = do
  Token
q <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "substitution"
  IRI
n <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
  Token
c <- AParser st Token
forall st. AParser st Token
colonT
  VIEW_TYPE
vt <- LogicGraph -> AParser st VIEW_TYPE
forall st. LogicGraph -> AParser st VIEW_TYPE
viewType LogicGraph
l
  Token
e <- AParser st Token
forall st. AParser st Token
equalT
  AnyLogic
lg <- String
-> LogicGraph -> ParsecT String (AnnoState st) Identity AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "subst-defn" LogicGraph
l
  (m :: G_symb_map_items_list
m, cs :: [Token]
cs) <- 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
lg (LogicGraph -> Map String IRI
prefixes LogicGraph
l)
  Maybe Token
o <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
  LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> VIEW_TYPE -> G_symb_map_items_list -> Range -> LIB_ITEM
Subst_defn IRI
n VIEW_TYPE
vt G_symb_map_items_list
m (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange
    ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Token
q, Token
c, Token
e] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
o

resultDefn :: LogicGraph -> AParser st LIB_ITEM
resultDefn :: LogicGraph -> AParser st LIB_ITEM
resultDefn l :: LogicGraph
l = do
  Token
q <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
resultS
  IRI
n <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
  (sns :: [IRI]
sns, cs :: [Token]
cs) <- 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
l) AParser st Token
forall st. AParser st Token
anComma
  Token
f <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
forS
  IRI
r <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
  [Annotation]
a <- GenParser Char (AnnoState st) [Annotation]
forall st. GenParser Char st [Annotation]
annotations
  Maybe Token
o <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
  LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> [IRI] -> IRI -> Bool -> Range -> LIB_ITEM
Result_defn IRI
n [IRI]
sns IRI
r ((Annotation -> Bool) -> [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> Annotation -> Bool
identAnno "complete") [Annotation]
a)
    (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ Token
q Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
f] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
o

-- | Parse an element of the library
libItem :: LogicGraph -> AParser st LIB_ITEM
libItem :: LogicGraph -> AParser st LIB_ITEM
libItem l :: LogicGraph
l = LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
specDefn LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
viewDefn LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
dolImportItem LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
entailDefn LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
queryDefn LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
substDefn LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
resultDefn LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- equiv defn
    do Token
s1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
equivalenceS
       IRI
en <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
       Token
s2 <- AParser st Token
forall st. AParser st Token
colonT
       EQUIV_TYPE
et <- LogicGraph -> AParser st EQUIV_TYPE
forall st. LogicGraph -> AParser st EQUIV_TYPE
equivType LogicGraph
l
       Token
s3 <- AParser st Token
forall st. AParser st Token
equalT
       OmsOrNetwork
sp <- (Annoted SPEC -> OmsOrNetwork)
-> ParsecT String (AnnoState st) Identity (Annoted SPEC)
-> ParsecT String (AnnoState st) Identity OmsOrNetwork
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Annoted SPEC -> OmsOrNetwork
MkOms (ParsecT String (AnnoState st) Identity (Annoted SPEC)
 -> ParsecT String (AnnoState st) Identity OmsOrNetwork)
-> ParsecT String (AnnoState st) Identity (Annoted SPEC)
-> ParsecT String (AnnoState st) Identity OmsOrNetwork
forall a b. (a -> b) -> a -> b
$ LogicGraph -> ParsecT String (AnnoState st) Identity (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
       Maybe Token
ep <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> EQUIV_TYPE -> OmsOrNetwork -> Range -> LIB_ITEM
Equiv_defn IRI
en EQUIV_TYPE
et OmsOrNetwork
sp
         (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ Token
s1 Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: Token
s2 Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: Token
s3 Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
ep
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- align defn
    do Token
s1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
alignmentS
       IRI
an <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
       Maybe ALIGN_ARITIES
ar <- ParsecT String (AnnoState st) Identity ALIGN_ARITIES
-> ParsecT String (AnnoState st) Identity (Maybe ALIGN_ARITIES)
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 ALIGN_ARITIES
forall st. AParser st ALIGN_ARITIES
alignArities
       Token
s2 <- AParser st Token
forall st. AParser st Token
colonT
       VIEW_TYPE
at <- LogicGraph -> AParser st VIEW_TYPE
forall st. LogicGraph -> AParser st VIEW_TYPE
viewType LogicGraph
l
       (corresps :: [CORRESPONDENCE]
corresps, ps :: [Token]
ps, sem :: AlignSem
sem) <- ([CORRESPONDENCE], [Token], AlignSem)
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([CORRESPONDENCE], [Token], AlignSem)
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([CORRESPONDENCE], [Token], AlignSem)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], [], AlignSem
SingleDomain) (ParsecT
   String
   (AnnoState st)
   Identity
   ([CORRESPONDENCE], [Token], AlignSem)
 -> ParsecT
      String
      (AnnoState st)
      Identity
      ([CORRESPONDENCE], [Token], AlignSem))
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([CORRESPONDENCE], [Token], AlignSem)
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([CORRESPONDENCE], [Token], AlignSem)
forall a b. (a -> b) -> a -> b
$ do
         Token
s <- AParser st Token
forall st. AParser st Token
equalT
         [CORRESPONDENCE]
cs <- LogicGraph -> AParser st [CORRESPONDENCE]
forall st. LogicGraph -> AParser st [CORRESPONDENCE]
parseCorrespondences LogicGraph
l
         AlignSem
aSem <- AlignSem
-> ParsecT String (AnnoState st) Identity AlignSem
-> ParsecT String (AnnoState st) Identity AlignSem
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option AlignSem
SingleDomain (ParsecT String (AnnoState st) Identity AlignSem
 -> ParsecT String (AnnoState st) Identity AlignSem)
-> ParsecT String (AnnoState st) Identity AlignSem
-> ParsecT String (AnnoState st) Identity AlignSem
forall a b. (a -> b) -> a -> b
$ do
            Token
_ <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "assuming"
            [ParsecT String (AnnoState st) Identity AlignSem]
-> ParsecT String (AnnoState st) Identity AlignSem
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([ParsecT String (AnnoState st) Identity AlignSem]
 -> ParsecT String (AnnoState st) Identity AlignSem)
-> [ParsecT String (AnnoState st) Identity AlignSem]
-> ParsecT String (AnnoState st) Identity AlignSem
forall a b. (a -> b) -> a -> b
$ (AlignSem -> ParsecT String (AnnoState st) Identity AlignSem)
-> [AlignSem] -> [ParsecT String (AnnoState st) Identity AlignSem]
forall a b. (a -> b) -> [a] -> [b]
map (\ d :: AlignSem
d -> String -> AParser st Token
forall st. String -> AParser st Token
asKey (AlignSem -> String
forall a. Show a => a -> String
show AlignSem
d) AParser st Token
-> ParsecT String (AnnoState st) Identity AlignSem
-> ParsecT String (AnnoState st) Identity AlignSem
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AlignSem -> ParsecT String (AnnoState st) Identity AlignSem
forall (m :: * -> *) a. Monad m => a -> m a
return AlignSem
d)
              [AlignSem
forall a. Bounded a => a
minBound .. AlignSem
forall a. Bounded a => a
maxBound]
         ([CORRESPONDENCE], [Token], AlignSem)
-> ParsecT
     String
     (AnnoState st)
     Identity
     ([CORRESPONDENCE], [Token], AlignSem)
forall (m :: * -> *) a. Monad m => a -> m a
return ([CORRESPONDENCE]
cs, [Token
s], AlignSem
aSem)
       Maybe Token
q <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI
-> Maybe ALIGN_ARITIES
-> VIEW_TYPE
-> [CORRESPONDENCE]
-> AlignSem
-> Range
-> LIB_ITEM
Align_defn IRI
an Maybe ALIGN_ARITIES
ar VIEW_TYPE
at [CORRESPONDENCE]
corresps AlignSem
sem
         (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ [Token
s1, Token
s2] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
q
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- module defn
    do Token
s1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
moduleS
       IRI
mn <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
       [Annotation]
_ <- GenParser Char (AnnoState st) [Annotation]
forall st. GenParser Char st [Annotation]
annotations -- TODO: store annotations
       Token
s2 <- AParser st Token
forall st. AParser st Token
colonT
       MODULE_TYPE
mt <- LogicGraph -> AParser st MODULE_TYPE
forall st. LogicGraph -> AParser st MODULE_TYPE
moduleType LogicGraph
l
       Token
s3 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
forS
       G_symb_items_list
rs <- LogicGraph -> AParser st G_symb_items_list
forall st. LogicGraph -> AParser st G_symb_items_list
restrictionSignature LogicGraph
l
       Maybe Token
kEnd <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> ([Token] -> LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> MODULE_TYPE -> G_symb_items_list -> Range -> LIB_ITEM
Module_defn IRI
mn MODULE_TYPE
mt G_symb_items_list
rs
         (Range -> LIB_ITEM) -> ([Token] -> Range) -> [Token] -> LIB_ITEM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Token] -> Range
catRange ([Token] -> AParser st LIB_ITEM) -> [Token] -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ Token
s1 Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: Token
s2 Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: Token
s3 Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
kEnd
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- unit spec
    do Token
kUnit <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
unitS
       Token
kSpec <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
specS
       IRI
name <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
       Token
kEqu <- AParser st Token
forall st. AParser st Token
equalT
       UNIT_SPEC
usp <- LogicGraph -> AParser st UNIT_SPEC
forall st. LogicGraph -> AParser st UNIT_SPEC
unitSpec LogicGraph
l
       Maybe Token
kEnd <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> UNIT_SPEC -> Range -> LIB_ITEM
Unit_spec_defn IRI
name UNIT_SPEC
usp
                ([Token] -> Range
catRange ([Token
kUnit, Token
kSpec, Token
kEqu] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
kEnd)))
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> AParser st LIB_ITEM
forall st. LogicGraph -> AParser st LIB_ITEM
networkDefn LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- arch spec
    do Token
kArch <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
archS
       Token
kASpec <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
specS
       IRI
name <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
       Token
kEqu <- AParser st Token
forall st. AParser st Token
equalT
       Annoted ARCH_SPEC
asp <- LogicGraph -> AParser st (Annoted ARCH_SPEC)
forall st. LogicGraph -> AParser st (Annoted ARCH_SPEC)
annotedArchSpec LogicGraph
l
       Maybe Token
kEnd <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> Annoted ARCH_SPEC -> Range -> LIB_ITEM
Arch_spec_defn IRI
name Annoted ARCH_SPEC
asp
                ([Token] -> Range
catRange ([Token
kArch, Token
kASpec, Token
kEqu] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
kEnd)))
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- download
    do Token
s1 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
fromS
       LibName
iln <- LogicGraph -> AParser st LibName
forall st. LogicGraph -> AParser st LibName
libName LogicGraph
l
       Token
s2 <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
getS
       (il :: DownloadItems
il, ps :: [Token]
ps) <- LogicGraph -> AParser st (DownloadItems, [Token])
forall st. LogicGraph -> AParser st (DownloadItems, [Token])
downloadItems LogicGraph
l
       Maybe Token
q <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName -> DownloadItems -> Range -> LIB_ITEM
Download_items LibName
iln DownloadItems
il
                ([Token] -> Range
catRange ([Token
s1, Token
s2] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
q)))
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- use (to be removed eventually)
    do String -> AParser st Token
forall st. String -> AParser st Token
asKey "use"
       (IRI -> LIB_ITEM)
-> GenParser Char (AnnoState st) IRI -> AParser st LIB_ITEM
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> IRI -> LIB_ITEM
addDownloadAux Bool
False) (GenParser Char (AnnoState st) IRI -> AParser st LIB_ITEM)
-> GenParser Char (AnnoState st) IRI -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- logic
    do (s :: Token
s, logD :: LogicDescr
logD) <- LogicGraph -> AParser st (Token, LogicDescr)
forall st. LogicGraph -> AParser st (Token, LogicDescr)
qualification LogicGraph
l
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM -> AParser st LIB_ITEM)
-> LIB_ITEM -> AParser st LIB_ITEM
forall a b. (a -> b) -> a -> b
$ LogicDescr -> Range -> LIB_ITEM
Logic_decl LogicDescr
logD (Range -> LIB_ITEM) -> Range -> LIB_ITEM
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
s
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- newlogic
    do (n :: IRI
n, s1 :: Token
s1) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
newlogicP
       Token
s2 <- AParser st Token
forall st. AParser st Token
equalT
       (ml :: FRAM
ml, s3 :: Token
s3) <- AParser st (FRAM, Token)
forall st. AParser st (FRAM, Token)
metaP
       (s :: IRI
s, s4 :: Token
s4) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
syntaxP
       (m :: IRI
m, s5 :: Token
s5) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
modelsP
       (f :: IRI
f, s6 :: Token
s6) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
foundationP
       (p :: IRI
p, s7 :: Token
s7) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
proofsP
       (pa :: Token
pa, s8 :: Token
s8) <- AParser st (Token, Token)
forall st. AParser st (Token, Token)
patternsP
       Maybe Token
q <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
       LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (LogicDef -> Range -> LIB_ITEM
Newlogic_defn (IRI -> FRAM -> IRI -> IRI -> IRI -> IRI -> Token -> LogicDef
LogicDef IRI
n FRAM
ml IRI
s IRI
m IRI
f IRI
p Token
pa)
          ([Token] -> Range
catRange ([Token
s1, Token
s2, Token
s3, Token
s4, Token
s5, Token
s6, Token
s7, Token
s8] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
q)))
   AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- newcomorphism
     do (n :: IRI
n, s1 :: Token
s1) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
newcomorphismP
        Token
s2 <- AParser st Token
forall st. AParser st Token
equalT
        (ml :: FRAM
ml, s3 :: Token
s3) <- AParser st (FRAM, Token)
forall st. AParser st (FRAM, Token)
metaP
        (s :: IRI
s, s4 :: Token
s4) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
sourceP
        (t :: IRI
t, s5 :: Token
s5) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
targetP
        (sv :: IRI
sv, s6 :: Token
s6) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
syntaxP
        (pv :: IRI
pv, s8 :: Token
s8) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
proofsP
        (mv :: IRI
mv, s7 :: Token
s7) <- AParser st (IRI, Token)
forall st. AParser st (IRI, Token)
modelsP
        Maybe Token
q <- AParser st (Maybe Token)
forall st. AParser st (Maybe Token)
optEnd
        LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (ComorphismDef -> Range -> LIB_ITEM
Newcomorphism_defn (IRI -> FRAM -> IRI -> IRI -> IRI -> IRI -> IRI -> ComorphismDef
ComorphismDef IRI
n FRAM
ml IRI
s IRI
t IRI
sv IRI
pv IRI
mv)
           ([Token] -> Range
catRange ([Token
s1, Token
s2, Token
s3, Token
s4, Token
s5, Token
s6, Token
s7, Token
s8] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Maybe Token -> [Token]
forall a. Maybe a -> [a]
maybeToList Maybe Token
q)))
  AParser st LIB_ITEM -> AParser st LIB_ITEM -> AParser st LIB_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- just a spec (turned into "spec spec = sp")
     do Pos
p1 <- GenParser Char (AnnoState st) Pos
forall tok st. GenParser tok st Pos
getPos
        Annoted SPEC
a <- LogicGraph -> ParsecT String (AnnoState st) Identity (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
        Pos
p2 <- GenParser Char (AnnoState st) Pos
forall tok st. GenParser tok st Pos
getPos
        if Pos
p1 Pos -> Pos -> Bool
forall a. Eq a => a -> a -> Bool
== Pos
p2 then String -> AParser st LIB_ITEM
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "cannot parse spec" else
          LIB_ITEM -> AParser st LIB_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> GENERICITY -> Annoted SPEC -> Range -> LIB_ITEM
Spec_defn IRI
nullIRI
               (PARAMS -> IMPORTED -> Range -> GENERICITY
Genericity ([Annoted SPEC] -> PARAMS
Params []) ([Annoted SPEC] -> IMPORTED
Imported []) Range
nullRange) Annoted SPEC
a Range
nullRange)

downloadItems :: LogicGraph -> AParser st (DownloadItems, [Token])
downloadItems :: LogicGraph -> AParser st (DownloadItems, [Token])
downloadItems l :: LogicGraph
l = do
    (il :: [ItemNameMap]
il, ps :: [Token]
ps) <- GenParser Char (AnnoState st) ItemNameMap
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([ItemNameMap], [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) ItemNameMap
forall st. LogicGraph -> AParser st ItemNameMap
itemNameOrMap LogicGraph
l) GenParser Char (AnnoState st) Token
forall st. AParser st Token
anSemiOrComma
    (DownloadItems, [Token]) -> AParser st (DownloadItems, [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ItemNameMap] -> DownloadItems
ItemMaps [ItemNameMap]
il, [Token]
ps)
  AParser st (DownloadItems, [Token])
-> AParser st (DownloadItems, [Token])
-> AParser st (DownloadItems, [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
s <- String -> GenParser Char (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
mapsTo
    IRI
i <- LogicGraph -> GenParser Char (AnnoState st) IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
    (DownloadItems, [Token]) -> AParser st (DownloadItems, [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> DownloadItems
UniqueItem IRI
i, [Token
s])

entailType :: LogicGraph -> AParser st ENTAIL_TYPE
entailType :: LogicGraph -> AParser st ENTAIL_TYPE
entailType l :: LogicGraph
l = do
    OmsOrNetwork
sp1 <- LogicGraph -> AParser st OmsOrNetwork
forall st. LogicGraph -> AParser st OmsOrNetwork
omsOrNetwork LogicGraph
l
    do
        Token
r <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
entailsS
        OmsOrNetwork
sp2 <- LogicGraph -> AParser st OmsOrNetwork
forall st. LogicGraph -> AParser st OmsOrNetwork
omsOrNetwork LogicGraph
l
        ENTAIL_TYPE -> AParser st ENTAIL_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (ENTAIL_TYPE -> AParser st ENTAIL_TYPE)
-> ENTAIL_TYPE -> AParser st ENTAIL_TYPE
forall a b. (a -> b) -> a -> b
$ OmsOrNetwork -> OmsOrNetwork -> Range -> ENTAIL_TYPE
Entail_type OmsOrNetwork
sp1 OmsOrNetwork
sp2 (Range -> ENTAIL_TYPE) -> Range -> ENTAIL_TYPE
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
r
      AParser st ENTAIL_TYPE
-> AParser st ENTAIL_TYPE -> AParser st ENTAIL_TYPE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> case OmsOrNetwork
sp1 of
            MkOms (Annoted (Spec_inst n :: IRI
n [] Nothing _) _ _ _) -> do
              Token
i <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
inS
              Network
nw <- LogicGraph -> AParser st Network
forall st. LogicGraph -> AParser st Network
parseNetwork LogicGraph
l
              Token
r <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
entailsS
              SPEC
g <- LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l
              ENTAIL_TYPE -> AParser st ENTAIL_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (ENTAIL_TYPE -> AParser st ENTAIL_TYPE)
-> (Range -> ENTAIL_TYPE) -> Range -> AParser st ENTAIL_TYPE
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IRI -> Network -> SPEC -> Range -> ENTAIL_TYPE
OMSInNetwork IRI
n Network
nw SPEC
g (Range -> AParser st ENTAIL_TYPE)
-> Range -> AParser st ENTAIL_TYPE
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token
i, Token
r]
            _ -> String -> AParser st ENTAIL_TYPE
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "OMSName expected"

omsOrNetwork :: LogicGraph -> AParser st OmsOrNetwork
omsOrNetwork :: LogicGraph -> AParser st OmsOrNetwork
omsOrNetwork l :: LogicGraph
l = (SPEC -> OmsOrNetwork)
-> ParsecT String (AnnoState st) Identity SPEC
-> AParser st OmsOrNetwork
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Annoted SPEC -> OmsOrNetwork
MkOms (Annoted SPEC -> OmsOrNetwork)
-> (SPEC -> Annoted SPEC) -> SPEC -> OmsOrNetwork
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPEC -> Annoted SPEC
forall a. a -> Annoted a
emptyAnno) (ParsecT String (AnnoState st) Identity SPEC
 -> AParser st OmsOrNetwork)
-> ParsecT String (AnnoState st) Identity SPEC
-> AParser st OmsOrNetwork
forall a b. (a -> b) -> a -> b
$ LogicGraph -> ParsecT String (AnnoState st) Identity SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l

equivType :: LogicGraph -> AParser st EQUIV_TYPE
equivType :: LogicGraph -> AParser st EQUIV_TYPE
equivType l :: LogicGraph
l = do
    OmsOrNetwork
sp1 <- LogicGraph -> AParser st OmsOrNetwork
forall st. LogicGraph -> AParser st OmsOrNetwork
omsOrNetwork LogicGraph
l
    Token
r <- AParser st Token
forall st. AParser st Token
equiT
    OmsOrNetwork
sp2 <- LogicGraph -> AParser st OmsOrNetwork
forall st. LogicGraph -> AParser st OmsOrNetwork
omsOrNetwork LogicGraph
l
    EQUIV_TYPE -> AParser st EQUIV_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (EQUIV_TYPE -> AParser st EQUIV_TYPE)
-> EQUIV_TYPE -> AParser st EQUIV_TYPE
forall a b. (a -> b) -> a -> b
$ OmsOrNetwork -> OmsOrNetwork -> Range -> EQUIV_TYPE
Equiv_type OmsOrNetwork
sp1 OmsOrNetwork
sp2 (Range -> EQUIV_TYPE) -> Range -> EQUIV_TYPE
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
r

alignArities :: AParser st ALIGN_ARITIES
alignArities :: AParser st ALIGN_ARITIES
alignArities = do
  String -> AParser st Token
forall st. String -> AParser st Token
asKey String
alignArityForwardS
  ALIGN_ARITY
f <- AParser st ALIGN_ARITY
forall st. AParser st ALIGN_ARITY
alignArity
  String -> AParser st Token
forall st. String -> AParser st Token
asKey String
alignArityBackwardS
  ALIGN_ARITY
b <- AParser st ALIGN_ARITY
forall st. AParser st ALIGN_ARITY
alignArity
  ALIGN_ARITIES -> AParser st ALIGN_ARITIES
forall (m :: * -> *) a. Monad m => a -> m a
return (ALIGN_ARITIES -> AParser st ALIGN_ARITIES)
-> ALIGN_ARITIES -> AParser st ALIGN_ARITIES
forall a b. (a -> b) -> a -> b
$ ALIGN_ARITY -> ALIGN_ARITY -> ALIGN_ARITIES
Align_arities ALIGN_ARITY
f ALIGN_ARITY
b

alignArity :: AParser st ALIGN_ARITY
alignArity :: AParser st ALIGN_ARITY
alignArity = [AParser st ALIGN_ARITY] -> AParser st ALIGN_ARITY
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([AParser st ALIGN_ARITY] -> AParser st ALIGN_ARITY)
-> [AParser st ALIGN_ARITY] -> AParser st ALIGN_ARITY
forall a b. (a -> b) -> a -> b
$ (ALIGN_ARITY -> AParser st ALIGN_ARITY)
-> [ALIGN_ARITY] -> [AParser st ALIGN_ARITY]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: ALIGN_ARITY
a -> String -> AParser st Token
forall st. String -> AParser st Token
asKey (ALIGN_ARITY -> String
showAlignArity ALIGN_ARITY
a) AParser st Token
-> AParser st ALIGN_ARITY -> AParser st ALIGN_ARITY
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ALIGN_ARITY -> AParser st ALIGN_ARITY
forall (m :: * -> *) a. Monad m => a -> m a
return ALIGN_ARITY
a)
  [ALIGN_ARITY
forall a. Bounded a => a
minBound .. ALIGN_ARITY
forall a. Bounded a => a
maxBound]

-- | Parse view type also used in alignments
viewType :: LogicGraph -> AParser st VIEW_TYPE
viewType :: LogicGraph -> AParser st VIEW_TYPE
viewType l :: LogicGraph
l = do
    Annoted SPEC
sp1 <- AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l)
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
toS
    Annoted SPEC
sp2 <- AParser st SPEC -> AParser st (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l)
    VIEW_TYPE -> AParser st VIEW_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (VIEW_TYPE -> AParser st VIEW_TYPE)
-> VIEW_TYPE -> AParser st VIEW_TYPE
forall a b. (a -> b) -> a -> b
$ Annoted SPEC -> Annoted SPEC -> Range -> VIEW_TYPE
View_type Annoted SPEC
sp1 Annoted SPEC
sp2 (Range -> VIEW_TYPE) -> Range -> VIEW_TYPE
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
s

moduleType :: LogicGraph -> AParser st MODULE_TYPE
moduleType :: LogicGraph -> AParser st MODULE_TYPE
moduleType l :: LogicGraph
l = do
  Annoted SPEC
sp1 <- LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
ofS
  Annoted SPEC
sp2 <- LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
  MODULE_TYPE -> AParser st MODULE_TYPE
forall (m :: * -> *) a. Monad m => a -> m a
return (MODULE_TYPE -> AParser st MODULE_TYPE)
-> MODULE_TYPE -> AParser st MODULE_TYPE
forall a b. (a -> b) -> a -> b
$ Annoted SPEC -> Annoted SPEC -> Range -> MODULE_TYPE
Module_type Annoted SPEC
sp1 Annoted SPEC
sp2 (Token -> Range
tokPos Token
s)

restrictionSignature :: LogicGraph -> AParser st G_symb_items_list
restrictionSignature :: LogicGraph -> AParser st G_symb_items_list
restrictionSignature lG :: LogicGraph
lG = do
  AnyLogic
l <- String
-> LogicGraph -> ParsecT String (AnnoState st) Identity AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "restrictionSignature" LogicGraph
lG
  ((G_symb_items_list, [Token]) -> G_symb_items_list)
-> ParsecT
     String (AnnoState st) Identity (G_symb_items_list, [Token])
-> AParser st G_symb_items_list
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (G_symb_items_list, [Token]) -> G_symb_items_list
forall a b. (a, b) -> a
fst (ParsecT
   String (AnnoState st) Identity (G_symb_items_list, [Token])
 -> AParser st G_symb_items_list)
-> ParsecT
     String (AnnoState st) Identity (G_symb_items_list, [Token])
-> AParser st G_symb_items_list
forall a b. (a -> b) -> a -> b
$ AnyLogic
-> Map String IRI
-> ParsecT
     String (AnnoState st) Identity (G_symb_items_list, [Token])
forall st.
AnyLogic
-> Map String IRI -> AParser st (G_symb_items_list, [Token])
parseItemsList AnyLogic
l (LogicGraph -> Map String IRI
prefixes LogicGraph
lG)


simpleIdOrDDottedId :: GenParser Char st Token
simpleIdOrDDottedId :: GenParser Char st Token
simpleIdOrDDottedId = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ (String -> String -> String)
-> CharParser st String
-> CharParser st String
-> CharParser st String
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 String -> String -> String
forall a. [a] -> [a] -> [a]
(++)
  ([String] -> CharParser st String -> CharParser st String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
casl_structured_reserved_words CharParser st String
forall st. CharParser st String
scanAnyWords)
  (CharParser st String -> CharParser st String)
-> CharParser st String -> CharParser st String
forall a b. (a -> b) -> a -> b
$ CharParser st String -> CharParser st String
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (CharParser st String -> CharParser st String)
-> CharParser st String -> CharParser st String
forall a b. (a -> b) -> a -> b
$ CharParser st String -> CharParser st String
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st String -> CharParser st String)
-> CharParser st String -> CharParser st String
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string ".." CharParser st String
-> CharParser st String -> CharParser st String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> CharParser st String
forall st. CharParser st String
scanAnyWords

-- | Parse item name or name map
itemNameOrMap :: LogicGraph -> AParser st ItemNameMap
itemNameOrMap :: LogicGraph -> AParser st ItemNameMap
itemNameOrMap l :: LogicGraph
l = do
    IRI
i1 <- (Token -> IRI)
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity IRI
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> IRI
simpleIdToIRI ParsecT String (AnnoState st) Identity Token
forall st. GenParser Char st Token
simpleIdOrDDottedId 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
<|> LogicGraph -> ParsecT String (AnnoState st) Identity IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
    Maybe IRI
i2 <- 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
$ do
        Token
_ <- String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
mapsTo
        if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf ".." (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ IRI -> String
iriToStringUnsecure IRI
i1
            then (Token -> IRI)
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity IRI
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> IRI
simpleIdToIRI ParsecT String (AnnoState st) Identity Token
forall st. GenParser Char st Token
simpleIdOrDDottedId
            else LogicGraph -> ParsecT String (AnnoState st) Identity IRI
forall st. LogicGraph -> GenParser Char st IRI
hetIRI LogicGraph
l
    ItemNameMap -> AParser st ItemNameMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ItemNameMap -> AParser st ItemNameMap)
-> ItemNameMap -> AParser st ItemNameMap
forall a b. (a -> b) -> a -> b
$ IRI -> Maybe IRI -> ItemNameMap
ItemNameMap IRI
i1 Maybe IRI
i2

optEnd :: AParser st (Maybe Token)
optEnd :: AParser st (Maybe Token)
optEnd = AParser st (Maybe Token) -> AParser st (Maybe Token)
forall tok st a. GenParser tok st a -> GenParser tok st a
try
    (AParser st ()
forall st. AParser st ()
addAnnos AParser st ()
-> AParser st (Maybe Token) -> AParser st (Maybe Token)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String (AnnoState st) Identity Token
-> AParser st (Maybe Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser (AnnoState st) String
 -> ParsecT String (AnnoState st) Identity Token)
-> CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity Token
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st a. CharParser st a -> CharParser st a
keyWord (CharParser (AnnoState st) String
 -> CharParser (AnnoState st) String)
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall a b. (a -> b) -> a -> b
$ String -> CharParser (AnnoState st) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
endS))
    AParser st (Maybe Token)
-> AParser st () -> AParser st (Maybe Token)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< AParser st ()
forall st. AParser st ()
addLineAnnos

generics :: LogicGraph -> AParser st GENERICITY
generics :: LogicGraph -> AParser st GENERICITY
generics l :: LogicGraph
l = do
    (pa :: [Annoted SPEC]
pa, ps1 :: Range
ps1) <- LogicGraph -> AParser st ([Annoted SPEC], Range)
forall st. LogicGraph -> AParser st ([Annoted SPEC], Range)
params LogicGraph
l
    (imp :: [Annoted SPEC]
imp, ps2 :: Range
ps2) <- ([Annoted SPEC], Range)
-> AParser st ([Annoted SPEC], Range)
-> AParser st ([Annoted SPEC], 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) (LogicGraph -> AParser st ([Annoted SPEC], Range)
forall st. LogicGraph -> AParser st ([Annoted SPEC], Range)
imports LogicGraph
l)
    GENERICITY -> AParser st GENERICITY
forall (m :: * -> *) a. Monad m => a -> m a
return (GENERICITY -> AParser st GENERICITY)
-> GENERICITY -> AParser st GENERICITY
forall a b. (a -> b) -> a -> b
$ PARAMS -> IMPORTED -> Range -> GENERICITY
Genericity ([Annoted SPEC] -> PARAMS
Params [Annoted SPEC]
pa) ([Annoted SPEC] -> IMPORTED
Imported [Annoted SPEC]
imp) (Range -> GENERICITY) -> Range -> GENERICITY
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange Range
ps1 Range
ps2

params :: LogicGraph -> AParser st ([Annoted SPEC], Range)
params :: LogicGraph -> AParser st ([Annoted SPEC], Range)
params l :: LogicGraph
l = do
    [(Annoted SPEC, Range)]
pas <- ParsecT String (AnnoState st) Identity (Annoted SPEC, Range)
-> ParsecT String (AnnoState st) Identity [(Annoted SPEC, Range)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (LogicGraph
-> ParsecT String (AnnoState st) Identity (Annoted SPEC, Range)
forall st. LogicGraph -> AParser st (Annoted SPEC, Range)
param LogicGraph
l)
    let (pas1 :: [Annoted SPEC]
pas1, ps :: [Range]
ps) = [(Annoted SPEC, Range)] -> ([Annoted SPEC], [Range])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Annoted SPEC, Range)]
pas
    ([Annoted SPEC], Range) -> AParser st ([Annoted SPEC], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC]
pas1, (Range -> Range) -> [Range] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange Range -> Range
forall a. a -> a
id [Range]
ps)

param :: LogicGraph -> AParser st (Annoted SPEC, Range)
param :: LogicGraph -> AParser st (Annoted SPEC, Range)
param l :: LogicGraph
l = do
    Token
b <- CharParser (AnnoState st) Token
forall st. GenParser Char st Token
oBracketT
    Annoted SPEC
pa <- LogicGraph -> AParser st (Annoted SPEC)
forall st. LogicGraph -> AParser st (Annoted SPEC)
aSpec LogicGraph
l
    Token
c <- CharParser (AnnoState st) Token
forall st. GenParser Char st Token
cBracketT
    (Annoted SPEC, Range) -> AParser st (Annoted SPEC, Range)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC
pa, Token -> [Token] -> Token -> Range
toRange Token
b [] Token
c)

imports :: LogicGraph -> AParser st ([Annoted SPEC], Range)
imports :: LogicGraph -> AParser st ([Annoted SPEC], Range)
imports l :: LogicGraph
l = do
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
givenS
    (sps :: [Annoted SPEC]
sps, ps :: [Token]
ps) <- GenParser Char (AnnoState 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 (AParser st SPEC -> GenParser Char (AnnoState st) (Annoted SPEC)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st SPEC -> GenParser Char (AnnoState st) (Annoted SPEC))
-> AParser st SPEC -> GenParser Char (AnnoState st) (Annoted SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st SPEC
forall st. LogicGraph -> AParser st SPEC
groupSpec LogicGraph
l) AParser st Token
forall st. AParser st Token
anComma
    ([Annoted SPEC], Range) -> AParser st ([Annoted SPEC], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC]
sps, [Token] -> Range
catRange (Token
s Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps))

newlogicP :: AParser st (IRI, Token)
newlogicP :: AParser st (IRI, Token)
newlogicP = do
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
newlogicS
  Token
n <- AParser st Token
forall st. GenParser Char st Token
simpleId
  (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> IRI
simpleIdToIRI Token
n, Token
s)

metaP :: AParser st (FRAM, Token)
metaP :: AParser st (FRAM, Token)
metaP = do
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
metaS
  FRAM
f <- AParser st FRAM
forall st. AParser st FRAM
framP
  (FRAM, Token) -> AParser st (FRAM, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (FRAM
f, Token
s)

framP :: AParser st FRAM
framP :: AParser st FRAM
framP = do
    String -> AParser st Token
forall st. String -> AParser st Token
asKey String
lfS
    FRAM -> AParser st FRAM
forall (m :: * -> *) a. Monad m => a -> m a
return FRAM
LF
  AParser st FRAM -> AParser st FRAM -> AParser st FRAM
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
isabelleS
    FRAM -> AParser st FRAM
forall (m :: * -> *) a. Monad m => a -> m a
return FRAM
Isabelle
  AParser st FRAM -> AParser st FRAM -> AParser st FRAM
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
maudeS
    FRAM -> AParser st FRAM
forall (m :: * -> *) a. Monad m => a -> m a
return FRAM
Maude

syntaxP :: AParser st (IRI, Token)
syntaxP :: AParser st (IRI, Token)
syntaxP = do
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
syntaxS
  Token
t <- AParser st Token
forall st. GenParser Char st Token
simpleIdOrDDottedId
  (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> IRI
simpleIdToIRI Token
t, Token
s)

modelsP :: AParser st (IRI, Token)
modelsP :: AParser st (IRI, Token)
modelsP = do
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
modelsS
    Token
m <- AParser st Token
forall st. GenParser Char st Token
simpleIdOrDDottedId
    (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> IRI
simpleIdToIRI Token
m, Token
s)
  AParser st (IRI, Token)
-> AParser st (IRI, Token) -> AParser st (IRI, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI
nullIRI, Token
nullTok)

foundationP :: AParser st (IRI, Token)
foundationP :: AParser st (IRI, Token)
foundationP = do
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
foundationS
    Token
f <- AParser st Token
forall st. GenParser Char st Token
simpleId
    (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> IRI
simpleIdToIRI Token
f, Token
s)
  AParser st (IRI, Token)
-> AParser st (IRI, Token) -> AParser st (IRI, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI
nullIRI, Token
nullTok)

proofsP :: AParser st (IRI, Token)
proofsP :: AParser st (IRI, Token)
proofsP = do
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
proofsS
    Token
p <- AParser st Token
forall st. GenParser Char st Token
simpleIdOrDDottedId
    (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> IRI
simpleIdToIRI Token
p, Token
s)
  AParser st (IRI, Token)
-> AParser st (IRI, Token) -> AParser st (IRI, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI
nullIRI, Token
nullTok)

patternsP :: AParser st (Token, Token)
patternsP :: AParser st (Token, Token)
patternsP = do
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
patternsS
    Token
p <- AParser st Token
forall st. GenParser Char st Token
simpleId
    (Token, Token) -> AParser st (Token, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
p, Token
s)
  AParser st (Token, Token)
-> AParser st (Token, Token) -> AParser st (Token, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token, Token) -> AParser st (Token, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
nullTok, Token
nullTok)

newcomorphismP :: AParser st (IRI, Token)
newcomorphismP :: AParser st (IRI, Token)
newcomorphismP = do
  -- add newcomorphismS = "newcomorphism" in
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
newcomorphismS
  Token
n <- AParser st Token
forall st. GenParser Char st Token
simpleId
  (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> IRI
simpleIdToIRI Token
n, Token
s)

sourceP :: AParser st (IRI, Token)
sourceP :: AParser st (IRI, Token)
sourceP = do
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
sourceS
  Token
sl <- AParser st Token
forall st. GenParser Char st Token
simpleIdOrDDottedId
  (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> IRI
simpleIdToIRI Token
sl, Token
s)

targetP :: AParser st (IRI, Token)
targetP :: AParser st (IRI, Token)
targetP = do
  Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
targetS
  Token
tl <- AParser st Token
forall st. GenParser Char st Token
simpleIdOrDDottedId
  (IRI, Token) -> AParser st (IRI, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> IRI
simpleIdToIRI Token
tl, Token
s)