{- |
Module      :  ./CASL/Parse_AS_Basic.hs
Description :  Parsing CASL's SIG-ITEMS, BASIC-ITEMS and BASIC-SPEC
Copyright   :  (c) Christian Maeder, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Parser for CASL basic specifications (SIG-ITEMS, BASIC-ITEMS, BASIC-SPEC)
   Follows Sect. II:3.1 of the CASL Reference Manual.
-}

{-
   http://www.cofi.info/Documents/CASL/Summary/
   from 25 March 2001

   C.2.1 Basic Specifications with Subsorts
-}

module CASL.Parse_AS_Basic where

import Common.AS_Annotation
import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.GlobalAnnotations (PrefixMap)

import CASL.AS_Basic_CASL
import CASL.Formula
import CASL.SortItem
import CASL.OpItem

import Text.ParserCombinators.Parsec

-- * signature items

sortItems, typeItems, opItems, predItems, sigItems
    :: (AParsable s, TermParser f) => [String] -> AParser st (SIG_ITEMS s f)
sortItems :: [String] -> AParser st (SIG_ITEMS s f)
sortItems ks :: [String]
ks = [String]
-> String
-> ([String] -> AParser st (SORT_ITEM f))
-> ([Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f)
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ks String
esortS [String] -> AParser st (SORT_ITEM f)
forall f st. TermParser f => [String] -> AParser st (SORT_ITEM f)
sortItem (SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
PossiblyEmptySorts)
    AParser st (SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f) -> AParser st (SIG_ITEMS s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> String
-> ([String] -> AParser st (SORT_ITEM f))
-> ([Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f)
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ks String
sortS [String] -> AParser st (SORT_ITEM f)
forall f st. TermParser f => [String] -> AParser st (SORT_ITEM f)
sortItem (SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
NonEmptySorts)
typeItems :: [String] -> AParser st (SIG_ITEMS s f)
typeItems ks :: [String]
ks = [String]
-> String
-> ([String] -> AParser st DATATYPE_DECL)
-> ([Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f)
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ks String
typeS [String] -> AParser st DATATYPE_DECL
forall st. [String] -> AParser st DATATYPE_DECL
datatype (SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
Datatype_items SortsKind
NonEmptySorts)
    AParser st (SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f) -> AParser st (SIG_ITEMS s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> String
-> ([String] -> AParser st DATATYPE_DECL)
-> ([Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f)
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ks String
etypeS [String] -> AParser st DATATYPE_DECL
forall st. [String] -> AParser st DATATYPE_DECL
datatype (SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> SIG_ITEMS s f
Datatype_items SortsKind
PossiblyEmptySorts)

opItems :: [String] -> AParser st (SIG_ITEMS s f)
opItems ks :: [String]
ks = [String]
-> String
-> ([String] -> AParser st (OP_ITEM f))
-> ([Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f)
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ks String
opS [String] -> AParser st (OP_ITEM f)
forall f st. TermParser f => [String] -> AParser st (OP_ITEM f)
opItem [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
Op_items
predItems :: [String] -> AParser st (SIG_ITEMS s f)
predItems ks :: [String]
ks = [String]
-> String
-> ([String] -> AParser st (PRED_ITEM f))
-> ([Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f)
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ks String
predS [String] -> AParser st (PRED_ITEM f)
forall f st. TermParser f => [String] -> AParser st (PRED_ITEM f)
predItem [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
Pred_items
sigItems :: [String] -> AParser st (SIG_ITEMS s f)
sigItems ks :: [String]
ks = (s -> SIG_ITEMS s f)
-> ParsecT String (AnnoState st) Identity s
-> AParser st (SIG_ITEMS s f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s -> SIG_ITEMS s f
forall s f. s -> SIG_ITEMS s f
Ext_SIG_ITEMS ParsecT String (AnnoState st) Identity s
forall a st. AParsable a => AParser st a
aparser AParser st (SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f) -> AParser st (SIG_ITEMS s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
           [String] -> AParser st (SIG_ITEMS s f)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
sortItems [String]
ks AParser st (SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f) -> AParser st (SIG_ITEMS s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (SIG_ITEMS s f)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
opItems [String]
ks AParser st (SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f) -> AParser st (SIG_ITEMS s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (SIG_ITEMS s f)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
predItems [String]
ks AParser st (SIG_ITEMS s f)
-> AParser st (SIG_ITEMS s f) -> AParser st (SIG_ITEMS s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st (SIG_ITEMS s f)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
typeItems [String]
ks

-- * helpers

datatypeToFreetype :: (AParsable b, AParsable s, TermParser f) =>
                      SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
datatypeToFreetype :: SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
datatypeToFreetype d :: SIG_ITEMS s f
d pos :: Range
pos =
   case SIG_ITEMS s f
d of
     Datatype_items sk :: SortsKind
sk ts :: [Annoted DATATYPE_DECL]
ts ps :: Range
ps -> SortsKind -> [Annoted DATATYPE_DECL] -> Range -> BASIC_ITEMS b s f
forall b s f.
SortsKind -> [Annoted DATATYPE_DECL] -> Range -> BASIC_ITEMS b s f
Free_datatype SortsKind
sk [Annoted DATATYPE_DECL]
ts (Range
pos Range -> Range -> Range
`appRange` Range
ps)
     _ -> String -> BASIC_ITEMS b s f
forall a. HasCallStack => String -> a
error "datatypeToFreetype"

axiomToLocalVarAxioms :: (AParsable b, AParsable s, TermParser f) =>
     BASIC_ITEMS b s f -> [Annotation] -> [VAR_DECL] -> Range
     -> BASIC_ITEMS b s f
axiomToLocalVarAxioms :: BASIC_ITEMS b s f
-> [Annotation] -> [VAR_DECL] -> Range -> BASIC_ITEMS b s f
axiomToLocalVarAxioms ai :: BASIC_ITEMS b s f
ai a :: [Annotation]
a vs :: [VAR_DECL]
vs posl :: Range
posl =
   case BASIC_ITEMS b s f
ai of
     Axiom_items (Annoted ft :: FORMULA f
ft qs :: Range
qs as :: [Annotation]
as rs :: [Annotation]
rs : fs :: [Annoted (FORMULA f)]
fs) ds :: Range
ds ->
         let aft :: Annoted (FORMULA f)
aft = FORMULA f
-> Range -> [Annotation] -> [Annotation] -> Annoted (FORMULA f)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted FORMULA f
ft Range
qs ([Annotation]
a [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
as) [Annotation]
rs
             in [VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Local_var_axioms [VAR_DECL]
vs (Annoted (FORMULA f)
aft Annoted (FORMULA f)
-> [Annoted (FORMULA f)] -> [Annoted (FORMULA f)]
forall a. a -> [a] -> [a]
: [Annoted (FORMULA f)]
fs) (Range
posl Range -> Range -> Range
`appRange` Range
ds)
     _ -> String -> BASIC_ITEMS b s f
forall a. HasCallStack => String -> a
error "axiomToLocalVarAxioms"

-- * basic items

basicItems :: (AParsable b, AParsable s, TermParser f) =>
              [String] -> AParser st (BASIC_ITEMS b s f)
basicItems :: [String] -> AParser st (BASIC_ITEMS b s f)
basicItems ks :: [String]
ks = (b -> BASIC_ITEMS b s f)
-> ParsecT String (AnnoState st) Identity b
-> AParser st (BASIC_ITEMS b s f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> BASIC_ITEMS b s f
forall b s f. b -> BASIC_ITEMS b s f
Ext_BASIC_ITEMS ParsecT String (AnnoState st) Identity b
forall a st. AParsable a => AParser st a
aparser AParser st (BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f) -> AParser st (BASIC_ITEMS b s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (SIG_ITEMS s f -> BASIC_ITEMS b s f)
-> ParsecT String (AnnoState st) Identity (SIG_ITEMS s f)
-> AParser st (BASIC_ITEMS b s f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items ([String] -> ParsecT String (AnnoState st) Identity (SIG_ITEMS s f)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
sigItems [String]
ks)
  AParser st (BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f) -> AParser st (BASIC_ITEMS b s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
f <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
freeS
    SIG_ITEMS s f
ti <- [String] -> ParsecT String (AnnoState st) Identity (SIG_ITEMS s f)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
typeItems [String]
ks
    BASIC_ITEMS b s f -> AParser st (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
forall b s f.
(AParsable b, AParsable s, TermParser f) =>
SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
datatypeToFreetype SIG_ITEMS s f
ti (Token -> Range
tokPos Token
f))
  AParser st (BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f) -> AParser st (BASIC_ITEMS b s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
g <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
generatedS
    do SIG_ITEMS s f
t <- [String] -> ParsecT String (AnnoState st) Identity (SIG_ITEMS s f)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
typeItems [String]
ks
       BASIC_ITEMS b s f -> AParser st (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
Sort_gen [SIG_ITEMS s f
-> Range -> [Annotation] -> [Annotation] -> Annoted (SIG_ITEMS s f)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted SIG_ITEMS s f
t Range
nullRange [] []] (Range -> BASIC_ITEMS b s f) -> Range -> BASIC_ITEMS b s f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
g)
      AParser st (BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f) -> AParser st (BASIC_ITEMS b s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
        Token
o <- AParser st Token
forall st. CharParser st Token
oBraceT
        [Annoted (SIG_ITEMS s f)]
is <- ParsecT String (AnnoState st) Identity (SIG_ITEMS s f)
-> AParser st [Annoted (SIG_ITEMS s f)]
forall st a. AParser st a -> AParser st [Annoted a]
annosParser ([String] -> ParsecT String (AnnoState st) Identity (SIG_ITEMS s f)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
sigItems [String]
ks)
        Token
c <- AParser st Token
forall st. CharParser st Token
cBraceT
        [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
lineAnnos
        BASIC_ITEMS b s f -> AParser st (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
Sort_gen ([Annoted (SIG_ITEMS s f)] -> [Annoted (SIG_ITEMS s f)]
forall a. [a] -> [a]
init [Annoted (SIG_ITEMS s f)]
is [Annoted (SIG_ITEMS s f)]
-> [Annoted (SIG_ITEMS s f)] -> [Annoted (SIG_ITEMS s f)]
forall a. [a] -> [a] -> [a]
++ [Annoted (SIG_ITEMS s f) -> [Annotation] -> Annoted (SIG_ITEMS s f)
forall a. Annoted a -> [Annotation] -> Annoted a
appendAnno ([Annoted (SIG_ITEMS s f)] -> Annoted (SIG_ITEMS s f)
forall a. [a] -> a
last [Annoted (SIG_ITEMS s f)]
is) [Annotation]
a])
                (Token -> [Token] -> Token -> Range
toRange Token
g [Token
o] Token
c))
  AParser st (BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f) -> AParser st (BASIC_ITEMS b s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
v <- String -> AParser st Token
forall st. String -> CharParser st Token
pluralKeyword String
varS
    (vs :: [VAR_DECL]
vs, ps :: [Token]
ps) <- [String] -> AParser st ([VAR_DECL], [Token])
forall st. [String] -> AParser st ([VAR_DECL], [Token])
varItems [String]
ks
    BASIC_ITEMS b s f -> AParser st (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([VAR_DECL] -> Range -> BASIC_ITEMS b s f
forall b s f. [VAR_DECL] -> Range -> BASIC_ITEMS b s f
Var_items [VAR_DECL]
vs ([Token] -> Range
catRange (Token
v Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)))
  AParser st (BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f) -> AParser st (BASIC_ITEMS b s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
f <- AParser st Token
forall st. AParser st Token
forallT
    (vs :: [VAR_DECL]
vs, ps :: [Token]
ps) <- [String] -> AParser st ([VAR_DECL], [Token])
forall st. [String] -> AParser st ([VAR_DECL], [Token])
varDecls [String]
ks
    [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
    BASIC_ITEMS b s f
ai <- Bool -> [String] -> AParser st (BASIC_ITEMS b s f)
forall b s f st.
(AParsable b, AParsable s, TermParser f) =>
Bool -> [String] -> AParser st (BASIC_ITEMS b s f)
dotFormulae Bool
True [String]
ks
    BASIC_ITEMS b s f -> AParser st (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEMS b s f
-> [Annotation] -> [VAR_DECL] -> Range -> BASIC_ITEMS b s f
forall b s f.
(AParsable b, AParsable s, TermParser f) =>
BASIC_ITEMS b s f
-> [Annotation] -> [VAR_DECL] -> Range -> BASIC_ITEMS b s f
axiomToLocalVarAxioms BASIC_ITEMS b s f
ai [Annotation]
a [VAR_DECL]
vs (Range -> BASIC_ITEMS b s f) -> Range -> BASIC_ITEMS b s f
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange (Token
f Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps))
  AParser st (BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f) -> AParser st (BASIC_ITEMS b s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Bool -> [String] -> AParser st (BASIC_ITEMS b s f)
forall b s f st.
(AParsable b, AParsable s, TermParser f) =>
Bool -> [String] -> AParser st (BASIC_ITEMS b s f)
dotFormulae Bool
True [String]
ks
  AParser st (BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f) -> AParser st (BASIC_ITEMS b s f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> String
-> ([String] -> AParser st (FORMULA f))
-> ([Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f)
-> AParser st (BASIC_ITEMS b s f)
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ks String
axiomS [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f. [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Axiom_items

varItems :: [String] -> AParser st ([VAR_DECL], [Token])
varItems :: [String] -> AParser st ([VAR_DECL], [Token])
varItems ks :: [String]
ks =
    do VAR_DECL
v <- [String] -> AParser st VAR_DECL
forall st. [String] -> AParser st VAR_DECL
varDecl [String]
ks
       do Token
s <- AParser st Token
forall st. AParser st Token
trySemiOrComma
          do [String] -> AParser st ()
forall st. [String] -> AParser st ()
tryItemEnd ([String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
startKeyword)
             ([VAR_DECL], [Token]) -> AParser st ([VAR_DECL], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([VAR_DECL
v], [Token
s])
            AParser st ([VAR_DECL], [Token])
-> AParser st ([VAR_DECL], [Token])
-> AParser st ([VAR_DECL], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
              (vs :: [VAR_DECL]
vs, ts :: [Token]
ts) <- [String] -> AParser st ([VAR_DECL], [Token])
forall st. [String] -> AParser st ([VAR_DECL], [Token])
varItems [String]
ks
              ([VAR_DECL], [Token]) -> AParser st ([VAR_DECL], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (VAR_DECL
v VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
vs, Token
s Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ts)
         AParser st ([VAR_DECL], [Token])
-> AParser st ([VAR_DECL], [Token])
-> AParser st ([VAR_DECL], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([VAR_DECL], [Token]) -> AParser st ([VAR_DECL], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([VAR_DECL
v], [])

dotFormulae :: (AParsable b, AParsable s, TermParser f) =>
  Bool -> [String] -> AParser st (BASIC_ITEMS b s f)
dotFormulae :: Bool -> [String] -> AParser st (BASIC_ITEMS b s f)
dotFormulae requireDot :: Bool
requireDot ks :: [String]
ks =
    do Token
d <- (if Bool
requireDot then ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall a. a -> a
id else Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (Token
 -> ParsecT String (AnnoState st) Identity Token
 -> ParsecT String (AnnoState st) Identity Token)
-> Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId ".") ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
dotT
       (fs :: [Annoted (FORMULA f)]
fs, ds :: [Token]
ds) <- [String] -> AParser st (Annoted (FORMULA f))
forall f st.
TermParser f =>
[String] -> AParser st (Annoted (FORMULA f))
aFormula [String]
ks AParser st (Annoted (FORMULA f))
-> ParsecT String (AnnoState st) Identity Token
-> GenParser Char (AnnoState st) ([Annoted (FORMULA f)], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
dotT
       (m :: [Token]
m, an :: [Annotation]
an) <- AParser st ([Token], [Annotation])
forall st. AParser st ([Token], [Annotation])
optSemi
       let ps :: Range
ps = [Token] -> Range
catRange (Token
d Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ds)
           ns :: [Annoted (FORMULA f)]
ns = [Annoted (FORMULA f)] -> [Annoted (FORMULA f)]
forall a. [a] -> [a]
init [Annoted (FORMULA f)]
fs [Annoted (FORMULA f)]
-> [Annoted (FORMULA f)] -> [Annoted (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [Annoted (FORMULA f) -> [Annotation] -> Annoted (FORMULA f)
forall a. Annoted a -> [Annotation] -> Annoted a
appendAnno ([Annoted (FORMULA f)] -> Annoted (FORMULA f)
forall a. [a] -> a
last [Annoted (FORMULA f)]
fs) [Annotation]
an]
       BASIC_ITEMS b s f -> AParser st (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEMS b s f -> AParser st (BASIC_ITEMS b s f))
-> BASIC_ITEMS b s f -> AParser st (BASIC_ITEMS b s f)
forall a b. (a -> b) -> a -> b
$ [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f. [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Axiom_items [Annoted (FORMULA f)]
ns (Range
ps Range -> Range -> Range
`appRange` [Token] -> Range
catRange [Token]
m)

aFormula :: TermParser f => [String] -> AParser st (Annoted (FORMULA f))
aFormula :: [String] -> AParser st (Annoted (FORMULA f))
aFormula = AParser st (FORMULA f) -> AParser st (Annoted (FORMULA f))
forall st a. AParser st a -> AParser st (Annoted a)
allAnnoParser (AParser st (FORMULA f) -> AParser st (Annoted (FORMULA f)))
-> ([String] -> AParser st (FORMULA f))
-> [String]
-> AParser st (Annoted (FORMULA f))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula

-- * basic spec

basicSpec :: (TermParser f, AParsable s, AParsable b) =>
             [String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec :: [String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec bi :: [String]
bi _ = (([Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f)
-> ParsecT
     String (AnnoState st) Identity [Annoted (BASIC_ITEMS b s f)]
-> AParser st (BASIC_SPEC b s f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
Basic_spec (ParsecT
   String (AnnoState st) Identity [Annoted (BASIC_ITEMS b s f)]
 -> AParser st (BASIC_SPEC b s f))
-> ([String]
    -> ParsecT
         String (AnnoState st) Identity [Annoted (BASIC_ITEMS b s f)])
-> [String]
-> AParser st (BASIC_SPEC b s f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st (BASIC_ITEMS b s f)
-> ParsecT
     String (AnnoState st) Identity [Annoted (BASIC_ITEMS b s f)]
forall st a. AParser st a -> AParser st [Annoted a]
annosParser (AParser st (BASIC_ITEMS b s f)
 -> ParsecT
      String (AnnoState st) Identity [Annoted (BASIC_ITEMS b s f)])
-> ([String] -> AParser st (BASIC_ITEMS b s f))
-> [String]
-> ParsecT
     String (AnnoState st) Identity [Annoted (BASIC_ITEMS b s f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> AParser st (BASIC_ITEMS b s f)
forall b s f st.
(AParsable b, AParsable s, TermParser f) =>
[String] -> AParser st (BASIC_ITEMS b s f)
basicItems) [String]
bi