{- |
Module      :  ./Syntax/Parse_AS_Architecture.hs
Description :  parser for CASL architectural specifications
Copyright   :  (c) Maciek Makowski, Warsaw University 2003-2004, C. Maeder
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (via imports)

Parser for CASL architectural specifications
   Follows Sect. II:3.1.4 of the CASL Reference Manual plus refinement
   extensions
-}

module Syntax.Parse_AS_Architecture
    ( unitSpec
    , refSpec
    , annotedArchSpec
    ) where

import Logic.Grothendieck (LogicGraph)

import Syntax.AS_Structured
import Syntax.AS_Architecture
import Syntax.Parse_AS_Structured

import Common.AS_Annotation
import Common.AnnoState
import Common.Id
import Common.IRI
import Common.Keywords
import Common.Lexer
import Common.Token

import Text.ParserCombinators.Parsec

-- * Parsing functions

-- | Parse annotated architectural specification
annotedArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC)
annotedArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC)
annotedArchSpec = AParser st (Annoted ARCH_SPEC) -> AParser st (Annoted ARCH_SPEC)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (AParser st (Annoted ARCH_SPEC) -> AParser st (Annoted ARCH_SPEC))
-> (LogicGraph -> AParser st (Annoted ARCH_SPEC))
-> LogicGraph
-> AParser st (Annoted ARCH_SPEC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicGraph -> AParser st (Annoted ARCH_SPEC)
forall st. LogicGraph -> AParser st (Annoted ARCH_SPEC)
archSpec

{- | Parse architectural specification
@
ARCH-SPEC ::= BASIC-ARCH-SPEC | GROUP-ARCH-SPEC
@ -}
archSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC)
archSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC)
archSpec l :: LogicGraph
l = LogicGraph -> AParser st (Annoted ARCH_SPEC)
forall st. LogicGraph -> AParser st (Annoted ARCH_SPEC)
basicArchSpec LogicGraph
l AParser st (Annoted ARCH_SPEC)
-> AParser st (Annoted ARCH_SPEC) -> AParser st (Annoted ARCH_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 ARCH_SPEC)
forall st. LogicGraph -> AParser st (Annoted ARCH_SPEC)
groupArchSpec LogicGraph
l

{- | Parse group architectural specification
@
GROUP-ARCH-SPEC ::= { ARCH-SPEC } | ARCH-SPEC-NAME
@ -}
groupArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC)
groupArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC)
groupArchSpec l :: LogicGraph
l = do
    Token
kOpBr <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBraceT
    Annoted (Annoted ARCH_SPEC)
asp <- AParser st (Annoted ARCH_SPEC)
-> AParser st (Annoted (Annoted ARCH_SPEC))
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st (Annoted ARCH_SPEC)
 -> AParser st (Annoted (Annoted ARCH_SPEC)))
-> AParser st (Annoted ARCH_SPEC)
-> AParser st (Annoted (Annoted ARCH_SPEC))
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st (Annoted ARCH_SPEC)
forall st. LogicGraph -> AParser st (Annoted ARCH_SPEC)
archSpec LogicGraph
l
    Token
kClBr <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
    Annoted ARCH_SPEC -> AParser st (Annoted ARCH_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted ARCH_SPEC -> AParser st (Annoted ARCH_SPEC))
-> Annoted ARCH_SPEC -> AParser st (Annoted ARCH_SPEC)
forall a b. (a -> b) -> a -> b
$ ARCH_SPEC -> Annoted (Annoted ARCH_SPEC) -> Annoted ARCH_SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted
      (Annoted ARCH_SPEC -> Range -> ARCH_SPEC
Group_arch_spec (Annoted (Annoted ARCH_SPEC) -> Annoted ARCH_SPEC
forall a. Annoted a -> a
item Annoted (Annoted ARCH_SPEC)
asp) (Range -> ARCH_SPEC) -> Range -> ARCH_SPEC
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
kOpBr [] Token
kClBr) Annoted (Annoted ARCH_SPEC)
asp
  AParser st (Annoted ARCH_SPEC)
-> AParser st (Annoted ARCH_SPEC) -> AParser st (Annoted ARCH_SPEC)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (ARCH_SPEC_NAME -> Annoted ARCH_SPEC)
-> ParsecT [Char] (AnnoState st) Identity ARCH_SPEC_NAME
-> AParser st (Annoted ARCH_SPEC)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ARCH_SPEC -> Annoted ARCH_SPEC
forall a. a -> Annoted a
emptyAnno (ARCH_SPEC -> Annoted ARCH_SPEC)
-> (ARCH_SPEC_NAME -> ARCH_SPEC)
-> ARCH_SPEC_NAME
-> Annoted ARCH_SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ARCH_SPEC_NAME -> ARCH_SPEC
Arch_spec_name) (LogicGraph -> ParsecT [Char] (AnnoState st) Identity ARCH_SPEC_NAME
forall st. LogicGraph -> GenParser Char st ARCH_SPEC_NAME
hetIRI LogicGraph
l)

{- | Parse basic architectural specification
@
BASIC-ARCH-SPEC ::= unit/units UNIT-DECL-DEFNS
result UNIT-EXPRESSION ;/
@ -}
basicArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC)
basicArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC)
basicArchSpec l :: LogicGraph
l = do
  Token
kUnit <- [Char] -> CharParser (AnnoState st) Token
forall st. [Char] -> CharParser st Token
pluralKeyword [Char]
unitS
  (declDefn :: [Annoted UNIT_DECL_DEFN]
declDefn, ps :: Range
ps) <- [[Char]]
-> [Token]
-> AParser st UNIT_DECL_DEFN
-> ([Annoted UNIT_DECL_DEFN]
    -> Range -> ([Annoted UNIT_DECL_DEFN], Range))
-> AParser st ([Annoted UNIT_DECL_DEFN], Range)
forall st b a.
[[Char]]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
auxItemList [[Char]
resultS] [] (LogicGraph -> AParser st UNIT_DECL_DEFN
forall st. LogicGraph -> AParser st UNIT_DECL_DEFN
unitDeclDefn LogicGraph
l) (,)
  Token
kResult <- [Char] -> CharParser (AnnoState st) Token
forall st. [Char] -> AParser st Token
asKey [Char]
resultS
  Annoted UNIT_EXPRESSION
expr <- AParser st (Annoted UNIT_EXPRESSION)
-> AParser st (Annoted UNIT_EXPRESSION)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (AParser st (Annoted UNIT_EXPRESSION)
 -> AParser st (Annoted UNIT_EXPRESSION))
-> AParser st (Annoted UNIT_EXPRESSION)
-> AParser st (Annoted UNIT_EXPRESSION)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st (Annoted UNIT_EXPRESSION)
forall st. LogicGraph -> AParser st (Annoted UNIT_EXPRESSION)
unitExpr LogicGraph
l
  (m :: [Token]
m, an :: [Annotation]
an) <- AParser st ([Token], [Annotation])
forall st. AParser st ([Token], [Annotation])
optSemi
  Annoted ARCH_SPEC -> AParser st (Annoted ARCH_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted ARCH_SPEC -> AParser st (Annoted ARCH_SPEC))
-> Annoted ARCH_SPEC -> AParser st (Annoted ARCH_SPEC)
forall a b. (a -> b) -> a -> b
$ ARCH_SPEC -> Annoted ARCH_SPEC
forall a. a -> Annoted a
emptyAnno (ARCH_SPEC -> Annoted ARCH_SPEC) -> ARCH_SPEC -> Annoted ARCH_SPEC
forall a b. (a -> b) -> a -> b
$ [Annoted UNIT_DECL_DEFN]
-> Annoted UNIT_EXPRESSION -> Range -> ARCH_SPEC
Basic_arch_spec [Annoted UNIT_DECL_DEFN]
declDefn (Annoted UNIT_EXPRESSION -> [Annotation] -> Annoted UNIT_EXPRESSION
forall a. Annoted a -> [Annotation] -> Annoted a
appendAnno Annoted UNIT_EXPRESSION
expr [Annotation]
an)
    (Range -> ARCH_SPEC) -> Range -> ARCH_SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
kUnit Range -> Range -> Range
`appRange` Range
ps Range -> Range -> Range
`appRange` [Token] -> Range
catRange (Token
kResult Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
m)

{- | Parse unit declaration or definition
@
UNIT-DECL-DEFN ::= UNIT-DECL | UNIT-DEFN
@ -}
unitDeclDefn :: LogicGraph -> AParser st UNIT_DECL_DEFN
unitDeclDefn :: LogicGraph -> AParser st UNIT_DECL_DEFN
unitDeclDefn l :: LogicGraph
l = do
    ARCH_SPEC_NAME
name <- LogicGraph -> GenParser Char (AnnoState st) ARCH_SPEC_NAME
forall st. LogicGraph -> GenParser Char st ARCH_SPEC_NAME
hetIRI LogicGraph
l
    do Token
c <- AParser st Token
forall st. AParser st Token
colonT     -- unit declaration
       REF_SPEC
decl <- LogicGraph -> AParser st REF_SPEC
forall st. LogicGraph -> AParser st REF_SPEC
refSpec LogicGraph
l
       (gs :: [Annoted UNIT_TERM]
gs, ps :: [Token]
ps) <- ([Annoted UNIT_TERM], [Token])
-> ParsecT
     [Char] (AnnoState st) Identity ([Annoted UNIT_TERM], [Token])
-> ParsecT
     [Char] (AnnoState st) Identity ([Annoted UNIT_TERM], [Token])
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], []) (ParsecT
   [Char] (AnnoState st) Identity ([Annoted UNIT_TERM], [Token])
 -> ParsecT
      [Char] (AnnoState st) Identity ([Annoted UNIT_TERM], [Token]))
-> ParsecT
     [Char] (AnnoState st) Identity ([Annoted UNIT_TERM], [Token])
-> ParsecT
     [Char] (AnnoState st) Identity ([Annoted UNIT_TERM], [Token])
forall a b. (a -> b) -> a -> b
$ do
         Token
kGiven <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
givenS
         (guts :: [Annoted UNIT_TERM]
guts, qs :: [Token]
qs) <- LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
groupUnitTerm LogicGraph
l AParser st (Annoted UNIT_TERM)
-> AParser st Token
-> ParsecT
     [Char] (AnnoState st) Identity ([Annoted UNIT_TERM], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
anComma
         ([Annoted UNIT_TERM], [Token])
-> ParsecT
     [Char] (AnnoState st) Identity ([Annoted UNIT_TERM], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted UNIT_TERM]
guts, Token
kGiven Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
qs)
       UNIT_DECL_DEFN -> AParser st UNIT_DECL_DEFN
forall (m :: * -> *) a. Monad m => a -> m a
return (UNIT_DECL_DEFN -> AParser st UNIT_DECL_DEFN)
-> UNIT_DECL_DEFN -> AParser st UNIT_DECL_DEFN
forall a b. (a -> b) -> a -> b
$ ARCH_SPEC_NAME
-> REF_SPEC -> [Annoted UNIT_TERM] -> Range -> UNIT_DECL_DEFN
Unit_decl ARCH_SPEC_NAME
name REF_SPEC
decl [Annoted UNIT_TERM]
gs (Range -> UNIT_DECL_DEFN) -> Range -> UNIT_DECL_DEFN
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps
     AParser st UNIT_DECL_DEFN
-> AParser st UNIT_DECL_DEFN -> AParser st UNIT_DECL_DEFN
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- unit definition
     LogicGraph -> ARCH_SPEC_NAME -> AParser st UNIT_DECL_DEFN
forall st.
LogicGraph -> ARCH_SPEC_NAME -> AParser st UNIT_DECL_DEFN
unitDefn' LogicGraph
l ARCH_SPEC_NAME
name

{- | Parse unit declaration
@
UNIT-REF ::= UNIT-NAME : REF-SPEC
@ -}
unitRef :: LogicGraph -> AParser st UNIT_REF
unitRef :: LogicGraph -> AParser st UNIT_REF
unitRef l :: LogicGraph
l = do
  ARCH_SPEC_NAME
name <- LogicGraph -> GenParser Char (AnnoState st) ARCH_SPEC_NAME
forall st. LogicGraph -> GenParser Char st ARCH_SPEC_NAME
hetIRI LogicGraph
l
  Token
sep1 <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
toS
  REF_SPEC
usp <- LogicGraph -> AParser st REF_SPEC
forall st. LogicGraph -> AParser st REF_SPEC
refSpec LogicGraph
l
  UNIT_REF -> AParser st UNIT_REF
forall (m :: * -> *) a. Monad m => a -> m a
return (UNIT_REF -> AParser st UNIT_REF)
-> UNIT_REF -> AParser st UNIT_REF
forall a b. (a -> b) -> a -> b
$ ARCH_SPEC_NAME -> REF_SPEC -> Range -> UNIT_REF
Unit_ref ARCH_SPEC_NAME
name REF_SPEC
usp (Range -> UNIT_REF) -> Range -> UNIT_REF
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
sep1

{- | Parse unit specification
@
UNIT-SPEC ::= GROUP-SPEC
GROUP-SPEC * .. * GROUP-SPEC -> GROUP-SPEC
closed UNIT-SPEC
@ -}
unitSpec :: LogicGraph -> AParser st UNIT_SPEC
unitSpec :: LogicGraph -> AParser st UNIT_SPEC
unitSpec l :: LogicGraph
l =
       -- closed unit spec
    do Token
kClosed <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
closedS
       UNIT_SPEC
uSpec <- LogicGraph -> AParser st UNIT_SPEC
forall st. LogicGraph -> AParser st UNIT_SPEC
unitSpec LogicGraph
l
       UNIT_SPEC -> AParser st UNIT_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (UNIT_SPEC -> AParser st UNIT_SPEC)
-> UNIT_SPEC -> AParser st UNIT_SPEC
forall a b. (a -> b) -> a -> b
$ UNIT_SPEC -> Range -> UNIT_SPEC
Closed_unit_spec UNIT_SPEC
uSpec (Range -> UNIT_SPEC) -> Range -> UNIT_SPEC
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
kClosed
    AParser st UNIT_SPEC
-> AParser st UNIT_SPEC -> AParser st UNIT_SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> {- unit type
     NOTE: this can also be a spec name. If this is the case, this unit spec
           will be converted on the static analysis stage.
           See Static.AnalysisArchitecture.ana_UNIT_SPEC. -}
    do gps :: ([Annoted SPEC], [Token])
gps@(gs :: Annoted SPEC
gs : gss :: [Annoted SPEC]
gss, _) <- 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
caslGroupSpec 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` AParser st Token
forall st. CharParser st Token
crossT
       let rest :: AParser st UNIT_SPEC
rest = LogicGraph -> ([Annoted SPEC], [Token]) -> AParser st UNIT_SPEC
forall st.
LogicGraph -> ([Annoted SPEC], [Token]) -> AParser st UNIT_SPEC
unitRestType LogicGraph
l ([Annoted SPEC], [Token])
gps
       if [Annoted SPEC] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted SPEC]
gss then
            UNIT_SPEC -> AParser st UNIT_SPEC -> AParser st UNIT_SPEC
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ( {- case item gs of
                    Spec_inst sn [] _ -> Spec_name sn -- annotations are lost
                    _ -> -} [Annoted SPEC] -> Annoted SPEC -> Range -> UNIT_SPEC
Unit_type [] Annoted SPEC
gs Range
nullRange) AParser st UNIT_SPEC
forall st. AParser st UNIT_SPEC
rest
            else AParser st UNIT_SPEC
forall st. AParser st UNIT_SPEC
rest

unitRestType :: LogicGraph -> ([Annoted SPEC], [Token]) -> AParser st UNIT_SPEC
unitRestType :: LogicGraph -> ([Annoted SPEC], [Token]) -> AParser st UNIT_SPEC
unitRestType l :: LogicGraph
l (gs :: [Annoted SPEC]
gs, ps :: [Token]
ps) = do
    Token
a <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
funS -- see Note
    Annoted SPEC
g <- 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
caslGroupSpec LogicGraph
l
    UNIT_SPEC -> AParser st UNIT_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC] -> Annoted SPEC -> Range -> UNIT_SPEC
Unit_type [Annoted SPEC]
gs Annoted SPEC
g (Range -> UNIT_SPEC) -> Range -> UNIT_SPEC
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
a]))

{- Note: the minus from funS (and crossT) would be misinterpreted as
optional ImportName for spec-insts, aka OMSRef in DOL, if we do not
exclude "-" as keyword or do not restrict unit-specs to use mere CASL
group-specs. -}

refSpec :: LogicGraph -> AParser st REF_SPEC
refSpec :: LogicGraph -> AParser st REF_SPEC
refSpec l :: LogicGraph
l = do
  (rs :: [REF_SPEC]
rs, ps :: [Token]
ps) <- LogicGraph -> AParser st REF_SPEC
forall st. LogicGraph -> AParser st REF_SPEC
basicRefSpec LogicGraph
l AParser st REF_SPEC
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([REF_SPEC], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` [Char] -> GenParser Char (AnnoState st) Token
forall st. [Char] -> AParser st Token
asKey [Char]
thenS
  REF_SPEC -> AParser st REF_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (REF_SPEC -> AParser st REF_SPEC)
-> REF_SPEC -> AParser st REF_SPEC
forall a b. (a -> b) -> a -> b
$ if [REF_SPEC] -> Bool
forall a. [a] -> Bool
isSingle [REF_SPEC]
rs then [REF_SPEC] -> REF_SPEC
forall a. [a] -> a
head [REF_SPEC]
rs else [REF_SPEC] -> Range -> REF_SPEC
Compose_ref [REF_SPEC]
rs (Range -> REF_SPEC) -> Range -> REF_SPEC
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
ps

{- | Parse refinement specification
@
REF-SPEC ::= UNIT_SPEC
UNIT_SPEC [bahav..] refined [via SYMB-MAP-ITEMS*] to REF-SPEC
arch spec GROUP-ARCH-SPEC
{ UNIT-DECL, ..., UNIT-DECL }
@ -}
basicRefSpec :: LogicGraph -> AParser st REF_SPEC
basicRefSpec :: LogicGraph -> AParser st REF_SPEC
basicRefSpec l :: LogicGraph
l = -- component spec
    do Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBraceT CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` (CharParser (AnnoState st) Token
forall st. CharParser st Token
simpleId CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Char] -> CharParser (AnnoState st) Token
forall st. [Char] -> AParser st Token
asKey [Char]
toS)
       (us :: [UNIT_REF]
us, ps :: [Token]
ps) <- LogicGraph -> AParser st UNIT_REF
forall st. LogicGraph -> AParser st UNIT_REF
unitRef LogicGraph
l AParser st UNIT_REF
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([UNIT_REF], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` CharParser (AnnoState st) Token
forall st. AParser st Token
anComma
       Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
       REF_SPEC -> AParser st REF_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return ([UNIT_REF] -> Range -> REF_SPEC
Component_ref [UNIT_REF]
us (Range -> REF_SPEC) -> Range -> REF_SPEC
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
c [Token]
ps Token
o)
    AParser st REF_SPEC -> AParser st REF_SPEC -> AParser st REF_SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- architectural spec
    do Token
kArch <- [Char] -> CharParser (AnnoState st) Token
forall st. [Char] -> AParser st Token
asKey [Char]
archS
       Token
kSpec <- [Char] -> CharParser (AnnoState st) Token
forall st. [Char] -> AParser st Token
asKey [Char]
specS
       Annoted ARCH_SPEC
asp <- LogicGraph -> AParser st (Annoted ARCH_SPEC)
forall st. LogicGraph -> AParser st (Annoted ARCH_SPEC)
groupArchSpec LogicGraph
l
       REF_SPEC -> AParser st REF_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted ARCH_SPEC -> Range -> REF_SPEC
Arch_unit_spec Annoted ARCH_SPEC
asp (Token -> [Token] -> Token -> Range
toRange Token
kArch [] Token
kSpec))
    AParser st REF_SPEC -> AParser st REF_SPEC -> AParser st REF_SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- unit spec
    do UNIT_SPEC
uSpec <- LogicGraph -> AParser st UNIT_SPEC
forall st. LogicGraph -> AParser st UNIT_SPEC
unitSpec LogicGraph
l
       LogicGraph -> UNIT_SPEC -> AParser st REF_SPEC
forall st. LogicGraph -> UNIT_SPEC -> AParser st REF_SPEC
refinedRestSpec LogicGraph
l UNIT_SPEC
uSpec AParser st REF_SPEC -> AParser st REF_SPEC -> AParser st REF_SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> REF_SPEC -> AParser st REF_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (UNIT_SPEC -> REF_SPEC
Unit_spec UNIT_SPEC
uSpec)

refinedRestSpec :: LogicGraph -> UNIT_SPEC -> AParser st REF_SPEC
refinedRestSpec :: LogicGraph -> UNIT_SPEC -> AParser st REF_SPEC
refinedRestSpec l :: LogicGraph
l u :: UNIT_SPEC
u = do
      Token
b <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
behaviourallyS
      LogicGraph -> Range -> UNIT_SPEC -> AParser st REF_SPEC
forall st. LogicGraph -> Range -> UNIT_SPEC -> AParser st REF_SPEC
onlyRefinedRestSpec LogicGraph
l (Token -> Range
tokPos Token
b) UNIT_SPEC
u
    AParser st REF_SPEC -> AParser st REF_SPEC -> AParser st REF_SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> Range -> UNIT_SPEC -> AParser st REF_SPEC
forall st. LogicGraph -> Range -> UNIT_SPEC -> AParser st REF_SPEC
onlyRefinedRestSpec LogicGraph
l Range
nullRange UNIT_SPEC
u

onlyRefinedRestSpec :: LogicGraph -> Range -> UNIT_SPEC -> AParser st REF_SPEC
onlyRefinedRestSpec :: LogicGraph -> Range -> UNIT_SPEC -> AParser st REF_SPEC
onlyRefinedRestSpec l :: LogicGraph
l b :: Range
b u :: UNIT_SPEC
u = do
    Token
r <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
refinedS
    (ms :: [G_mapping]
ms, ps :: [Token]
ps) <- ([G_mapping], [Token])
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
-> ParsecT [Char] (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 [Char] (AnnoState st) Identity ([G_mapping], [Token])
 -> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token]))
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
forall a b. (a -> b) -> a -> b
$ do
      Token
v <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
viaS -- not a keyword
      (m :: [G_mapping]
m, ts :: [Token]
ts) <- LogicGraph
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
forall st. LogicGraph -> AParser st ([G_mapping], [Token])
parseMapping LogicGraph
l
      ([G_mapping], [Token])
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([G_mapping]
m, Token
v Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ts)
    Token
t <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
toS
    REF_SPEC
rsp <- LogicGraph -> AParser st REF_SPEC
forall st. LogicGraph -> AParser st REF_SPEC
refSpec LogicGraph
l
    REF_SPEC -> AParser st REF_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return (REF_SPEC -> AParser st REF_SPEC)
-> REF_SPEC -> AParser st REF_SPEC
forall a b. (a -> b) -> a -> b
$ Bool -> UNIT_SPEC -> [G_mapping] -> REF_SPEC -> Range -> REF_SPEC
Refinement (Range -> Bool
isNullRange Range
b) UNIT_SPEC
u [G_mapping]
ms REF_SPEC
rsp (Range
b Range -> Range -> Range
`appRange` Token -> [Token] -> Token -> Range
toRange Token
r [Token]
ps Token
t)

{- | Parse group unit term
@
GROUP-UNIT-TERM ::= UNIT-NAME
UNIT-NAME FIT-ARG-UNITS
{ UNIT-TERM }
@ -}
groupUnitTerm :: LogicGraph -> AParser st (Annoted UNIT_TERM)
groupUnitTerm :: LogicGraph -> AParser st (Annoted UNIT_TERM)
groupUnitTerm l :: LogicGraph
l = AParser st UNIT_TERM -> AParser st (Annoted UNIT_TERM)
forall st a. AParser st a -> AParser st (Annoted a)
annoParser (AParser st UNIT_TERM -> AParser st (Annoted UNIT_TERM))
-> AParser st UNIT_TERM -> AParser st (Annoted UNIT_TERM)
forall a b. (a -> b) -> a -> b
$
        -- unit name/application
    do ARCH_SPEC_NAME
name <- LogicGraph -> GenParser Char (AnnoState st) ARCH_SPEC_NAME
forall st. LogicGraph -> GenParser Char st ARCH_SPEC_NAME
hetIRI LogicGraph
l
       [FIT_ARG_UNIT]
args <- ParsecT [Char] (AnnoState st) Identity FIT_ARG_UNIT
-> ParsecT [Char] (AnnoState st) Identity [FIT_ARG_UNIT]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (LogicGraph -> ParsecT [Char] (AnnoState st) Identity FIT_ARG_UNIT
forall st. LogicGraph -> AParser st FIT_ARG_UNIT
fitArgUnit LogicGraph
l)
       UNIT_TERM -> AParser st UNIT_TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (ARCH_SPEC_NAME -> [FIT_ARG_UNIT] -> Range -> UNIT_TERM
Unit_appl ARCH_SPEC_NAME
name [FIT_ARG_UNIT]
args Range
nullRange)
    AParser st UNIT_TERM
-> AParser st UNIT_TERM -> AParser st UNIT_TERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- unit term in brackets
    do Token
lbr <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBraceT
       Annoted UNIT_TERM
ut <- LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTerm LogicGraph
l
       Token
rbr <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
       UNIT_TERM -> AParser st UNIT_TERM
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted UNIT_TERM -> Range -> UNIT_TERM
Group_unit_term Annoted UNIT_TERM
ut ([Token] -> Range
catRange [Token
lbr, Token
rbr]))

{- | Parse an argument for unit application.
@
FIT-ARG-UNIT ::= [ UNIT-TERM ]
[ UNIT-TERM fit SYMB-MAP-ITEMS-LIST ]
@
The SYMB-MAP-ITEMS-LIST is parsed using parseItemsMap. -}
fitArgUnit :: LogicGraph -> AParser st FIT_ARG_UNIT
fitArgUnit :: LogicGraph -> AParser st FIT_ARG_UNIT
fitArgUnit l :: LogicGraph
l = do
  Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
  Annoted UNIT_TERM
ut <- LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTerm LogicGraph
l
  (fargs :: [G_mapping]
fargs, qs :: [Token]
qs) <- ([G_mapping], [Token])
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
-> ParsecT [Char] (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 [Char] (AnnoState st) Identity ([G_mapping], [Token])
 -> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token]))
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
forall a b. (a -> b) -> a -> b
$ do
    Token
kFit <- [Char] -> CharParser (AnnoState st) Token
forall st. [Char] -> AParser st Token
asKey [Char]
fitS
    (smis :: [G_mapping]
smis, ps :: [Token]
ps) <- LogicGraph
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
forall st. LogicGraph -> AParser st ([G_mapping], [Token])
parseMapping LogicGraph
l
    ([G_mapping], [Token])
-> ParsecT [Char] (AnnoState st) Identity ([G_mapping], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([G_mapping]
smis, Token
kFit Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)
  Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
  FIT_ARG_UNIT -> AParser st FIT_ARG_UNIT
forall (m :: * -> *) a. Monad m => a -> m a
return (FIT_ARG_UNIT -> AParser st FIT_ARG_UNIT)
-> FIT_ARG_UNIT -> AParser st FIT_ARG_UNIT
forall a b. (a -> b) -> a -> b
$ Annoted UNIT_TERM -> [G_mapping] -> Range -> FIT_ARG_UNIT
Fit_arg_unit Annoted UNIT_TERM
ut [G_mapping]
fargs (Range -> FIT_ARG_UNIT) -> Range -> FIT_ARG_UNIT
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token]
qs Token
c

{- | Parse unit term.
@
UNIT-TERM ::= UNIT-TERM RENAMING
UNIT-TERM RESTRICTION
UNIT-TERM and ... and UNIT-TERM
local UNIT-DEFNS within UNIT-TERM
GROUP-UNIT-TERM
@
This will be done by subsequent functions in order to preserve
the operator precedence; see other 'unitTerm*' functions. -}
unitTerm :: LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTerm :: LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTerm = LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermAmalgamation

{- | Parse unit amalgamation.
@
UNIT-TERM-AMALGAMATION ::= UNIT-TERM-LOCAL and ... and UNIT-TERM-LOCAL
@ -}
unitTermAmalgamation :: LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermAmalgamation :: LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermAmalgamation l :: LogicGraph
l = do
    (uts :: [Annoted UNIT_TERM]
uts, toks :: [Token]
toks) <- AParser st (Annoted UNIT_TERM) -> AParser st (Annoted UNIT_TERM)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermLocal LogicGraph
l) AParser st (Annoted UNIT_TERM)
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Annoted UNIT_TERM], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` [Char] -> GenParser Char (AnnoState st) Token
forall st. [Char] -> AParser st Token
asKey [Char]
andS
    Annoted UNIT_TERM -> AParser st (Annoted UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted UNIT_TERM -> AParser st (Annoted UNIT_TERM))
-> Annoted UNIT_TERM -> AParser st (Annoted UNIT_TERM)
forall a b. (a -> b) -> a -> b
$ case [Annoted UNIT_TERM]
uts of
      [ut :: Annoted UNIT_TERM
ut] -> Annoted UNIT_TERM
ut
      _ -> UNIT_TERM -> Annoted UNIT_TERM
forall a. a -> Annoted a
emptyAnno (UNIT_TERM -> Annoted UNIT_TERM) -> UNIT_TERM -> Annoted UNIT_TERM
forall a b. (a -> b) -> a -> b
$ [Annoted UNIT_TERM] -> Range -> UNIT_TERM
Amalgamation [Annoted UNIT_TERM]
uts (Range -> UNIT_TERM) -> Range -> UNIT_TERM
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
toks

{- | Parse local unit term
@
UNIT-TERM-LOCAL ::= local UNIT-DEFNS within UNIT-TERM-LOCAL
UNIT-TERM-TRANS-RED
@ -}
unitTermLocal :: LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermLocal :: LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermLocal l :: LogicGraph
l =
        -- local unit
    do Token
kLocal <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
localS
       (uDefns :: [Annoted UNIT_DECL_DEFN]
uDefns, ps :: Range
ps) <- [[Char]]
-> [Token]
-> AParser st UNIT_DECL_DEFN
-> ([Annoted UNIT_DECL_DEFN]
    -> Range -> ([Annoted UNIT_DECL_DEFN], Range))
-> AParser st ([Annoted UNIT_DECL_DEFN], Range)
forall st b a.
[[Char]]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
auxItemList [[Char]
withinS] [] (LogicGraph -> AParser st UNIT_DECL_DEFN
forall st. LogicGraph -> AParser st UNIT_DECL_DEFN
unitDefn LogicGraph
l) (,)
       Token
kWithin <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
withinS
       Annoted UNIT_TERM
uTerm <- LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermLocal LogicGraph
l
       Annoted UNIT_TERM -> AParser st (Annoted UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted UNIT_TERM -> AParser st (Annoted UNIT_TERM))
-> Annoted UNIT_TERM -> AParser st (Annoted UNIT_TERM)
forall a b. (a -> b) -> a -> b
$ UNIT_TERM -> Annoted UNIT_TERM
forall a. a -> Annoted a
emptyAnno (UNIT_TERM -> Annoted UNIT_TERM) -> UNIT_TERM -> Annoted UNIT_TERM
forall a b. (a -> b) -> a -> b
$ [Annoted UNIT_DECL_DEFN] -> Annoted UNIT_TERM -> Range -> UNIT_TERM
Local_unit [Annoted UNIT_DECL_DEFN]
uDefns Annoted UNIT_TERM
uTerm
         (Range -> UNIT_TERM) -> Range -> UNIT_TERM
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
kLocal Range -> Range -> Range
`appRange` Range
ps Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
kWithin
    AParser st (Annoted UNIT_TERM)
-> AParser st (Annoted UNIT_TERM) -> AParser st (Annoted UNIT_TERM)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> -- translation/reduction
       LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermTransRed LogicGraph
l

{- | Parse translation or reduction unit term
The original grammar
@
UNIT-TERM-TRANS-RED ::= UNIT-TERM-TRANS-RED RENAMING
UNIT-TERM-TRANS-RED RESTRICTION
GROUP-UNIT-TERM
@ -}

unitTermTransRed :: LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermTransRed :: LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTermTransRed l :: LogicGraph
l = LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
groupUnitTerm LogicGraph
l AParser st (Annoted UNIT_TERM)
-> (Annoted UNIT_TERM -> AParser st (Annoted UNIT_TERM))
-> AParser st (Annoted UNIT_TERM)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    [Annoted UNIT_TERM -> AParser st UNIT_TERM]
-> Annoted UNIT_TERM -> AParser st (Annoted UNIT_TERM)
forall b st.
[Annoted b -> AParser st b] -> Annoted b -> AParser st (Annoted b)
translationList
      [ ((RENAMING -> UNIT_TERM)
-> ParsecT [Char] (AnnoState st) Identity RENAMING
-> AParser st UNIT_TERM
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` LogicGraph -> ParsecT [Char] (AnnoState st) Identity RENAMING
forall st. LogicGraph -> AParser st RENAMING
renaming LogicGraph
l) ((RENAMING -> UNIT_TERM) -> AParser st UNIT_TERM)
-> (Annoted UNIT_TERM -> RENAMING -> UNIT_TERM)
-> Annoted UNIT_TERM
-> AParser st UNIT_TERM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted UNIT_TERM -> RENAMING -> UNIT_TERM
Unit_translation
      , ((RESTRICTION -> UNIT_TERM)
-> ParsecT [Char] (AnnoState st) Identity RESTRICTION
-> AParser st UNIT_TERM
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` LogicGraph -> ParsecT [Char] (AnnoState st) Identity RESTRICTION
forall st. LogicGraph -> AParser st RESTRICTION
restriction LogicGraph
l) ((RESTRICTION -> UNIT_TERM) -> AParser st UNIT_TERM)
-> (Annoted UNIT_TERM -> RESTRICTION -> UNIT_TERM)
-> Annoted UNIT_TERM
-> AParser st UNIT_TERM
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted UNIT_TERM -> RESTRICTION -> UNIT_TERM
Unit_reduction]

{- | Parse unit expression
@
UNIT-EXPRESSION ::= lambda UNIT-BINDINGS "." UNIT-TERM
UNIT-TERM
@ -}
unitExpr :: LogicGraph -> AParser st (Annoted UNIT_EXPRESSION)
unitExpr :: LogicGraph -> AParser st (Annoted UNIT_EXPRESSION)
unitExpr l :: LogicGraph
l = do
  (bindings :: [UNIT_BINDING]
bindings, poss :: Range
poss) <- ([UNIT_BINDING], Range)
-> ParsecT [Char] (AnnoState st) Identity ([UNIT_BINDING], Range)
-> ParsecT [Char] (AnnoState st) Identity ([UNIT_BINDING], 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 [Char] (AnnoState st) Identity ([UNIT_BINDING], Range)
 -> ParsecT [Char] (AnnoState st) Identity ([UNIT_BINDING], Range))
-> ParsecT [Char] (AnnoState st) Identity ([UNIT_BINDING], Range)
-> ParsecT [Char] (AnnoState st) Identity ([UNIT_BINDING], Range)
forall a b. (a -> b) -> a -> b
$ do
    Token
kLambda <- [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
lambdaS
    (bindings :: [UNIT_BINDING]
bindings, poss :: [Token]
poss) <- LogicGraph -> AParser st UNIT_BINDING
forall st. LogicGraph -> AParser st UNIT_BINDING
unitBinding LogicGraph
l AParser st UNIT_BINDING
-> AParser st Token
-> GenParser Char (AnnoState st) ([UNIT_BINDING], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
anSemi
    Token
kDot <- AParser st Token
forall st. AParser st Token
dotT
    ([UNIT_BINDING], Range)
-> ParsecT [Char] (AnnoState st) Identity ([UNIT_BINDING], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([UNIT_BINDING]
bindings, Token -> [Token] -> Token -> Range
toRange Token
kLambda [Token]
poss Token
kDot)
  Annoted UNIT_TERM
ut <- LogicGraph -> AParser st (Annoted UNIT_TERM)
forall st. LogicGraph -> AParser st (Annoted UNIT_TERM)
unitTerm LogicGraph
l
  Annoted UNIT_EXPRESSION -> AParser st (Annoted UNIT_EXPRESSION)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted UNIT_EXPRESSION -> AParser st (Annoted UNIT_EXPRESSION))
-> Annoted UNIT_EXPRESSION -> AParser st (Annoted UNIT_EXPRESSION)
forall a b. (a -> b) -> a -> b
$ UNIT_EXPRESSION -> Annoted UNIT_EXPRESSION
forall a. a -> Annoted a
emptyAnno (UNIT_EXPRESSION -> Annoted UNIT_EXPRESSION)
-> UNIT_EXPRESSION -> Annoted UNIT_EXPRESSION
forall a b. (a -> b) -> a -> b
$ [UNIT_BINDING] -> Annoted UNIT_TERM -> Range -> UNIT_EXPRESSION
Unit_expression [UNIT_BINDING]
bindings Annoted UNIT_TERM
ut Range
poss

{- | Parse unit binding
@
UNIT-BINDING ::= UNIT-NAME : UNIT-SPEC
@ -}
unitBinding :: LogicGraph -> AParser st UNIT_BINDING
unitBinding :: LogicGraph -> AParser st UNIT_BINDING
unitBinding l :: LogicGraph
l = do
  ARCH_SPEC_NAME
name <- LogicGraph -> GenParser Char (AnnoState st) ARCH_SPEC_NAME
forall st. LogicGraph -> GenParser Char st ARCH_SPEC_NAME
hetIRI LogicGraph
l
  Token
kCol <- AParser st Token
forall st. AParser st Token
colonT
  UNIT_SPEC
usp <- LogicGraph -> AParser st UNIT_SPEC
forall st. LogicGraph -> AParser st UNIT_SPEC
unitSpec LogicGraph
l
  UNIT_BINDING -> AParser st UNIT_BINDING
forall (m :: * -> *) a. Monad m => a -> m a
return (UNIT_BINDING -> AParser st UNIT_BINDING)
-> UNIT_BINDING -> AParser st UNIT_BINDING
forall a b. (a -> b) -> a -> b
$ ARCH_SPEC_NAME -> UNIT_SPEC -> Range -> UNIT_BINDING
Unit_binding ARCH_SPEC_NAME
name UNIT_SPEC
usp (Range -> UNIT_BINDING) -> Range -> UNIT_BINDING
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
kCol

{- | Parse an unit definition
@
UNIT-DEFN ::= UNIT-NAME = UNIT-EXPRESSION
@ -}
unitDefn :: LogicGraph -> AParser st UNIT_DECL_DEFN
unitDefn :: LogicGraph -> AParser st UNIT_DECL_DEFN
unitDefn l :: LogicGraph
l = LogicGraph -> GenParser Char (AnnoState st) ARCH_SPEC_NAME
forall st. LogicGraph -> GenParser Char st ARCH_SPEC_NAME
hetIRI LogicGraph
l GenParser Char (AnnoState st) ARCH_SPEC_NAME
-> (ARCH_SPEC_NAME -> AParser st UNIT_DECL_DEFN)
-> AParser st UNIT_DECL_DEFN
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LogicGraph -> ARCH_SPEC_NAME -> AParser st UNIT_DECL_DEFN
forall st.
LogicGraph -> ARCH_SPEC_NAME -> AParser st UNIT_DECL_DEFN
unitDefn' LogicGraph
l

unitDefn' :: LogicGraph -> IRI -> AParser st UNIT_DECL_DEFN
unitDefn' :: LogicGraph -> ARCH_SPEC_NAME -> AParser st UNIT_DECL_DEFN
unitDefn' l :: LogicGraph
l name :: ARCH_SPEC_NAME
name = do
  Token
kEqu <- AParser st Token
forall st. AParser st Token
equalT
  Annoted UNIT_EXPRESSION
expr <- AParser st (Annoted UNIT_EXPRESSION)
-> AParser st (Annoted UNIT_EXPRESSION)
forall st a. AParser st (Annoted a) -> AParser st (Annoted a)
annoParser2 (AParser st (Annoted UNIT_EXPRESSION)
 -> AParser st (Annoted UNIT_EXPRESSION))
-> AParser st (Annoted UNIT_EXPRESSION)
-> AParser st (Annoted UNIT_EXPRESSION)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> AParser st (Annoted UNIT_EXPRESSION)
forall st. LogicGraph -> AParser st (Annoted UNIT_EXPRESSION)
unitExpr LogicGraph
l
  UNIT_DECL_DEFN -> AParser st UNIT_DECL_DEFN
forall (m :: * -> *) a. Monad m => a -> m a
return (UNIT_DECL_DEFN -> AParser st UNIT_DECL_DEFN)
-> UNIT_DECL_DEFN -> AParser st UNIT_DECL_DEFN
forall a b. (a -> b) -> a -> b
$ ARCH_SPEC_NAME -> UNIT_EXPRESSION -> Range -> UNIT_DECL_DEFN
Unit_defn ARCH_SPEC_NAME
name (Annoted UNIT_EXPRESSION -> UNIT_EXPRESSION
forall a. Annoted a -> a
item Annoted UNIT_EXPRESSION
expr) (Range -> UNIT_DECL_DEFN) -> Range -> UNIT_DECL_DEFN
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
kEqu