{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./VSE/Parse.hs
Description :  parsing VSE parts
Copyright   :  (c) C. Maeder, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

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

Parser for VSE logic extension of CASL
-}

module VSE.Parse where

import Common.AnnoState
import Common.DocUtils
import Common.Id
import Common.Lexer
import Common.Result
import Common.Token
import VSE.As
import Text.ParserCombinators.Parsec
import CASL.Formula
import CASL.AS_Basic_CASL
import Data.Char (toUpper, toLower)

declWords :: [String]
declWords :: [String]
declWords = let
  ps :: [String]
ps = ["procedure", "function"]
  rs :: [String]
rs = [String]
ps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
forall a. [a] -> [a] -> [a]
++ "s") [String]
ps
  in [String]
rs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper) [String]
rs

reservedWords :: [String]
reservedWords :: [String]
reservedWords = let
  rs :: [String]
rs =
    [ "in", "out", "begin", "end", "abort", "skip", "return", "declare"
    , "if", "then", "else", "fi", "while", "do", "od"
    , "defprocs", "defprocsend", "restricted" ]
  in [ "<:", ":>"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
declWords [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
rs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper) [String]
rs

keyword :: String -> AParser st Token
keyword :: String -> AParser st Token
keyword s :: String
s = CharParser (AnnoState st) String -> AParser st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser (AnnoState st) String -> AParser st Token)
-> CharParser (AnnoState st) String -> AParser st Token
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser (AnnoState st) String
 -> CharParser (AnnoState st) String)
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall a b. (a -> b) -> a -> b
$ do
   AParser st [Annotation]
forall st. AParser st [Annotation]
annos
   String
str <- CharParser (AnnoState st) String
forall st. CharParser st String
scanAnyWords
   AParser st [Annotation]
forall st. AParser st [Annotation]
lineAnnos
   if (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
str String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s then String -> CharParser (AnnoState st) String
forall (m :: * -> *) a. Monad m => a -> m a
return String
s else String -> CharParser (AnnoState st) String
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected String
str CharParser (AnnoState st) String
-> String -> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
s

vseVarDecl :: AParser st VarDecl
vseVarDecl :: AParser st VarDecl
vseVarDecl = do
  Token
v <- [String] -> GenParser Char (AnnoState st) Token
forall st. [String] -> GenParser Char st Token
varId [String]
reservedWords
  Token
c <- GenParser Char (AnnoState st) Token
forall st. AParser st Token
colonT
  Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
reservedWords
  VarDecl -> AParser st VarDecl -> AParser st VarDecl
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (Token -> Id -> Maybe (TERM ()) -> Range -> VarDecl
VarDecl Token
v Id
s Maybe (TERM ())
forall a. Maybe a
Nothing (Range -> VarDecl) -> Range -> VarDecl
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c) (AParser st VarDecl -> AParser st VarDecl)
-> AParser st VarDecl -> AParser st VarDecl
forall a b. (a -> b) -> a -> b
$ do
    Token
a <- String -> GenParser Char (AnnoState st) Token
forall st. String -> AParser st Token
asKey ":="
    TERM ()
t <- [String] -> AParser st (TERM ())
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
reservedWords
    VarDecl -> AParser st VarDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (VarDecl -> AParser st VarDecl) -> VarDecl -> AParser st VarDecl
forall a b. (a -> b) -> a -> b
$ Token -> Id -> Maybe (TERM ()) -> Range -> VarDecl
VarDecl Token
v Id
s (TERM () -> Maybe (TERM ())
forall a. a -> Maybe a
Just TERM ()
t) (Range -> VarDecl) -> Range -> VarDecl
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
c [] Token
a

fromVarDecl :: [VarDecl] -> Program -> ([VAR_DECL], Program)
fromVarDecl :: [VarDecl] -> Program -> ([VAR_DECL], Program)
fromVarDecl vs :: [VarDecl]
vs p :: Program
p = case [VarDecl]
vs of
  [] -> ([], Program
p)
  VarDecl v :: Token
v s :: Id
s mt :: Maybe (TERM ())
mt r :: Range
r : n :: [VarDecl]
n ->
      let (rs :: [VAR_DECL]
rs, q :: Program
q) = [VarDecl] -> Program -> ([VAR_DECL], Program)
fromVarDecl [VarDecl]
n Program
p
      in ([Token] -> Id -> Range -> VAR_DECL
Var_decl [Token
v] Id
s Range
r VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
rs, case Maybe (TERM ())
mt of
           Nothing -> Program
q
           Just t :: TERM ()
t -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Token -> TERM () -> PlainProgram
Assign Token
v TERM ()
t) Range
r) Program
q) Range
r)

program :: AParser st Program
program :: AParser st Program
program = do
    Token
t <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "abort"
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Abort (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
t
  AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
t <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "skip"
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Skip (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
t
  AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
r <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "return"
    TERM ()
t <- [String] -> AParser st (TERM ())
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
reservedWords
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (TERM () -> PlainProgram
Return TERM ()
t) (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
r
  AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
b <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "begin"
    Program
p <- AParser st Program
forall st. AParser st Program
programSeq
    Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "end"
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged ([VAR_DECL] -> Program -> PlainProgram
Block [] Program
p) (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
b [] Token
e
  AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
d <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "declare"
    (vs :: [VarDecl]
vs, ps :: [Token]
ps) <- GenParser Char (AnnoState st) VarDecl
-> AParser st Token
-> GenParser Char (AnnoState st) ([VarDecl], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy GenParser Char (AnnoState st) VarDecl
forall st. AParser st VarDecl
vseVarDecl AParser st Token
forall st. CharParser st Token
commaT
    Token
s <- AParser st Token
forall st. AParser st Token
anSemi
    Program
p <- AParser st Program
forall st. AParser st Program
programSeq
    let (cs :: [VAR_DECL]
cs, q :: Program
q) = [VarDecl] -> Program -> ([VAR_DECL], Program)
fromVarDecl [VarDecl]
vs Program
p
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged ([VAR_DECL] -> Program -> PlainProgram
Block [VAR_DECL]
cs Program
q) (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
d [Token]
ps Token
s
  AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
i <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "if"
    FORMULA ()
c <- [String] -> AParser st (FORMULA ())
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
reservedWords
    Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "then"
    Program
t <- AParser st Program
forall st. AParser st Program
programSeq
    do Token
r <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "fi"
       let s :: Range
s = Token -> [Token] -> Token -> Range
toRange Token
i [Token
p] Token
r
       Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> Program -> PlainProgram
If FORMULA ()
c Program
t (Program -> PlainProgram) -> Program -> PlainProgram
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Skip Range
s) Range
s
     AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
       Token
q <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "else"
       Program
e <- AParser st Program
forall st. AParser st Program
programSeq
       Token
r <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "fi"
       Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> Program -> PlainProgram
If FORMULA ()
c Program
t Program
e) (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
i [Token
p, Token
q] Token
r
  AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
w <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "while"
    FORMULA ()
c <- [String] -> AParser st (FORMULA ())
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
reservedWords
    Token
d <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "do"
    Program
p <- AParser st Program
forall st. AParser st Program
programSeq
    Token
o <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "od"
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> PlainProgram
While FORMULA ()
c Program
p) (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
w [Token
d] Token
o
  AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (v :: Token
v, a :: Token
a) <- GenParser Char (AnnoState st) (Token, Token)
-> GenParser Char (AnnoState st) (Token, Token)
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char (AnnoState st) (Token, Token)
 -> GenParser Char (AnnoState st) (Token, Token))
-> GenParser Char (AnnoState st) (Token, Token)
-> GenParser Char (AnnoState st) (Token, Token)
forall a b. (a -> b) -> a -> b
$ do
         Token
v <- [String] -> AParser st Token
forall st. [String] -> GenParser Char st Token
varId [String]
reservedWords
         Token
a <- String -> AParser st Token
forall st. String -> AParser st Token
asKey ":="
         (Token, Token) -> GenParser Char (AnnoState st) (Token, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
v, Token
a)
    TERM ()
t <- [String] -> AParser st (TERM ())
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
reservedWords
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Token -> TERM () -> PlainProgram
Assign Token
v TERM ()
t) (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
a
  AParser st Program -> AParser st Program -> AParser st Program
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    TERM ()
t <- [String] -> AParser st (TERM ())
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
reservedWords
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program)
-> ([Pos] -> Program) -> [Pos] -> AParser st Program
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> PlainProgram
Call (FORMULA () -> PlainProgram) -> FORMULA () -> PlainProgram
forall a b. (a -> b) -> a -> b
$ TERM () -> FORMULA ()
forall f. TERM f -> FORMULA f
Mixfix_formula TERM ()
t) (Range -> Program) -> ([Pos] -> Range) -> [Pos] -> Program
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pos] -> Range
Range ([Pos] -> AParser st Program) -> [Pos] -> AParser st Program
forall a b. (a -> b) -> a -> b
$ TERM () -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM ()
t

programSeq :: AParser st Program
programSeq :: AParser st Program
programSeq = do
  Program
p1 <- AParser st Program
forall st. AParser st Program
program
  Program -> AParser st Program -> AParser st Program
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option Program
p1 (AParser st Program -> AParser st Program)
-> AParser st Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ do
    Token
s <- CharParser (AnnoState st) Token
forall st. CharParser st Token
semiT
    Program
p2 <- AParser st Program
forall st. AParser st Program
programSeq
    Program -> AParser st Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> AParser st Program) -> Program -> AParser st Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq Program
p1 Program
p2) (Range -> Program) -> Range -> Program
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
s

procKind :: AParser st (ProcKind, Token)
procKind :: AParser st (ProcKind, Token)
procKind = do
    Token
k <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "procedure"
    (ProcKind, Token) -> AParser st (ProcKind, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProcKind
Proc, Token
k)
  AParser st (ProcKind, Token)
-> AParser st (ProcKind, Token) -> AParser st (ProcKind, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
k <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "function"
    (ProcKind, Token) -> AParser st (ProcKind, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProcKind
Func, Token
k)

defproc :: AParser st Defproc
defproc :: AParser st Defproc
defproc = do
  (pk :: ProcKind
pk, q :: Token
q) <- AParser st (ProcKind, Token)
forall st. AParser st (ProcKind, Token)
procKind
  Id
i <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId [String]
reservedWords
  Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT
  (ts :: [Token]
ts, ps :: [Token]
ps) <- ([Token], [Token])
-> ParsecT String (AnnoState st) Identity ([Token], [Token])
-> ParsecT String (AnnoState st) Identity ([Token], [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 ([Token], [Token])
 -> ParsecT String (AnnoState st) Identity ([Token], [Token]))
-> ParsecT String (AnnoState st) Identity ([Token], [Token])
-> ParsecT String (AnnoState st) Identity ([Token], [Token])
forall a b. (a -> b) -> a -> b
$
       [String] -> CharParser (AnnoState st) Token
forall st. [String] -> GenParser Char st Token
varId [String]
reservedWords CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity ([Token], [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. CharParser st Token
commaT
  Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT
  Program
p <- AParser st Program
forall st. AParser st Program
program
  Defproc -> AParser st Defproc
forall (m :: * -> *) a. Monad m => a -> m a
return (Defproc -> AParser st Defproc) -> Defproc -> AParser st Defproc
forall a b. (a -> b) -> a -> b
$ ProcKind -> Id -> [Token] -> Program -> Range -> Defproc
Defproc ProcKind
pk Id
i [Token]
ts Program
p (Range -> Defproc) -> Range -> Defproc
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
q (Token
o Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps) Token
c

boxOrDiamandProg :: AParser st (Token, BoxOrDiamond, Program, Token)
boxOrDiamandProg :: AParser st (Token, BoxOrDiamond, Program, Token)
boxOrDiamandProg = do
    Token
o <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "<:"
    Program
p <- AParser st Program
forall st. AParser st Program
programSeq
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey ":>"
    (Token, BoxOrDiamond, Program, Token)
-> AParser st (Token, BoxOrDiamond, Program, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
o, BoxOrDiamond
Diamond, Program
p, Token
c)
  AParser st (Token, BoxOrDiamond, Program, Token)
-> AParser st (Token, BoxOrDiamond, Program, Token)
-> AParser st (Token, BoxOrDiamond, Program, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
o <- String -> AParser st Token
forall st. String -> AParser st Token
asKey "[:"
    Program
p <- AParser st Program
forall st. AParser st Program
programSeq
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey ":]"
    (Token, BoxOrDiamond, Program, Token)
-> AParser st (Token, BoxOrDiamond, Program, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token
o, BoxOrDiamond
Box, Program
p, Token
c)

dlformula :: AParser st Dlformula
dlformula :: AParser st Dlformula
dlformula = do
    Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "defprocs"
    (ps :: [Defproc]
ps, qs :: [Token]
qs) <- GenParser Char (AnnoState st) Defproc
-> AParser st Token
-> GenParser Char (AnnoState st) ([Defproc], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy GenParser Char (AnnoState st) Defproc
forall st. AParser st Defproc
defproc AParser st Token
forall st. CharParser st Token
semiT
    Token
q <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "defprocsend"
    Dlformula -> AParser st Dlformula
forall (m :: * -> *) a. Monad m => a -> m a
return (Dlformula -> AParser st Dlformula)
-> Dlformula -> AParser st Dlformula
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Dlformula
forall a. a -> Range -> Ranged a
Ranged ([Defproc] -> VSEforms
Defprocs [Defproc]
ps) (Range -> Dlformula) -> Range -> Dlformula
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
p [Token]
qs Token
q
  AParser st Dlformula
-> AParser st Dlformula -> AParser st Dlformula
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
   (o :: Token
o, b :: BoxOrDiamond
b, p :: Program
p, c :: Token
c) <- AParser st (Token, BoxOrDiamond, Program, Token)
forall st. AParser st (Token, BoxOrDiamond, Program, Token)
boxOrDiamandProg
   FORMULA Dlformula
f <- [String] -> AParser st (FORMULA Dlformula)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
reservedWords
   Dlformula -> AParser st Dlformula
forall (m :: * -> *) a. Monad m => a -> m a
return (Dlformula -> AParser st Dlformula)
-> Dlformula -> AParser st Dlformula
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Dlformula
forall a. a -> Range -> Ranged a
Ranged (BoxOrDiamond -> Program -> FORMULA Dlformula -> VSEforms
Dlformula BoxOrDiamond
b Program
p FORMULA Dlformula
f) (Range -> Dlformula) -> Range -> Dlformula
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c

param :: AParser st Procparam
param :: AParser st Procparam
param = do
    Paramkind
k <- (String -> AParser st Token
forall st. String -> AParser st Token
keyword "in" AParser st Token
-> ParsecT String (AnnoState st) Identity Paramkind
-> ParsecT String (AnnoState st) Identity Paramkind
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Paramkind -> ParsecT String (AnnoState st) Identity Paramkind
forall (m :: * -> *) a. Monad m => a -> m a
return Paramkind
In) ParsecT String (AnnoState st) Identity Paramkind
-> ParsecT String (AnnoState st) Identity Paramkind
-> ParsecT String (AnnoState st) Identity Paramkind
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
keyword "out" AParser st Token
-> ParsecT String (AnnoState st) Identity Paramkind
-> ParsecT String (AnnoState st) Identity Paramkind
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Paramkind -> ParsecT String (AnnoState st) Identity Paramkind
forall (m :: * -> *) a. Monad m => a -> m a
return Paramkind
Out)
    Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
reservedWords
    Procparam -> AParser st Procparam
forall (m :: * -> *) a. Monad m => a -> m a
return (Procparam -> AParser st Procparam)
-> Procparam -> AParser st Procparam
forall a b. (a -> b) -> a -> b
$ Paramkind -> Id -> Procparam
Procparam Paramkind
k Id
s

profile :: AParser st Profile
profile :: AParser st Profile
profile = do
  (ps :: [Procparam]
ps, _) <- ([Procparam], [Token])
-> ParsecT String (AnnoState st) Identity ([Procparam], [Token])
-> ParsecT String (AnnoState st) Identity ([Procparam], [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 ([Procparam], [Token])
 -> ParsecT String (AnnoState st) Identity ([Procparam], [Token]))
-> ParsecT String (AnnoState st) Identity ([Procparam], [Token])
-> ParsecT String (AnnoState st) Identity ([Procparam], [Token])
forall a b. (a -> b) -> a -> b
$ GenParser Char (AnnoState st) Procparam
-> GenParser Char (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity ([Procparam], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy GenParser Char (AnnoState st) Procparam
forall st. AParser st Procparam
param GenParser Char (AnnoState st) Token
forall st. CharParser st Token
commaT
  Maybe Id
m <- ParsecT String (AnnoState st) Identity Id
-> ParsecT String (AnnoState st) Identity (Maybe Id)
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 Id
 -> ParsecT String (AnnoState st) Identity (Maybe Id))
-> ParsecT String (AnnoState st) Identity Id
-> ParsecT String (AnnoState st) Identity (Maybe Id)
forall a b. (a -> b) -> a -> b
$ String -> GenParser Char (AnnoState st) Token
forall st. String -> AParser st Token
asKey "->" GenParser Char (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity Id
-> ParsecT String (AnnoState st) Identity Id
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [String] -> ParsecT String (AnnoState st) Identity Id
forall st. [String] -> GenParser Char st Id
sortId [String]
reservedWords
  Profile -> AParser st Profile
forall (m :: * -> *) a. Monad m => a -> m a
return (Profile -> AParser st Profile) -> Profile -> AParser st Profile
forall a b. (a -> b) -> a -> b
$ [Procparam] -> Maybe Id -> Profile
Profile [Procparam]
ps Maybe Id
m

procdecl :: AParser st Sigentry
procdecl :: AParser st Sigentry
procdecl = do
  Id
i <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId [String]
reservedWords
  Token
c <- AParser st Token
forall st. AParser st Token
colonT
  Profile
p <- AParser st Profile
forall st. AParser st Profile
profile
  Sigentry -> AParser st Sigentry
forall (m :: * -> *) a. Monad m => a -> m a
return (Sigentry -> AParser st Sigentry)
-> Sigentry -> AParser st Sigentry
forall a b. (a -> b) -> a -> b
$ Id -> Profile -> Range -> Sigentry
Procedure Id
i Profile
p (Range -> Sigentry) -> Range -> Sigentry
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c

procdecls :: AParser st Procdecls
procdecls :: AParser st Procdecls
procdecls = do
  Token
k <- String -> AParser st Token
forall st. String -> AParser st Token
keyword "procedures" 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
keyword "procedure"
  [String]
-> [Token]
-> AParser st Sigentry
-> ([Annoted Sigentry] -> Range -> Procdecls)
-> AParser st Procdecls
forall st b a.
[String]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
auxItemList ([String]
declWords [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
startKeyword) [Token
k] AParser st Sigentry
forall st. AParser st Sigentry
procdecl [Annoted Sigentry] -> Range -> Procdecls
Procdecls

instance TermParser Dlformula where
  termParser :: Bool -> AParser st Dlformula
termParser = AParser st Dlformula -> Bool -> AParser st Dlformula
forall st a. AParser st a -> Bool -> AParser st a
aToTermParser AParser st Dlformula
forall st. AParser st Dlformula
dlformula

instance AParsable Procdecls where
  aparser :: AParser st Procdecls
aparser = AParser st Procdecls
forall st. AParser st Procdecls
procdecls

-- | just for testing
testParse :: String -> String
testParse :: String -> String
testParse str :: String
str = case GenParser Char (AnnoState ()) (FORMULA Dlformula)
-> AnnoState ()
-> String
-> String
-> Either ParseError (FORMULA Dlformula)
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser ([String] -> GenParser Char (AnnoState ()) (FORMULA Dlformula)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [] :: AParser () Sentence)
    (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ()) "" String
str of
  Left err :: ParseError
err -> ParseError -> String
showErr ParseError
err
  Right ps :: FORMULA Dlformula
ps -> FORMULA Dlformula -> String -> String
forall a. Pretty a => a -> String -> String
showDoc FORMULA Dlformula
ps ""