module LF.MorphParser where

import LF.Sign
import LF.Morphism

import Common.Lexer
import Common.Parsec
import Common.AnnoParser (commentLine)

import Text.ParserCombinators.Parsec

import System.Directory
import System.IO.Unsafe

import qualified Data.Map as Map
import Data.Maybe (fromMaybe)


readMorphism :: FilePath -> Morphism
readMorphism :: FilePath -> Morphism
readMorphism file :: FilePath
file =
     let mor :: Maybe Morphism
mor = IO (Maybe Morphism) -> Maybe Morphism
forall a. IO a -> a
unsafePerformIO (IO (Maybe Morphism) -> Maybe Morphism)
-> IO (Maybe Morphism) -> Maybe Morphism
forall a b. (a -> b) -> a -> b
$ FilePath -> IO (Maybe Morphism)
readMorph FilePath
file
     in Morphism -> Maybe Morphism -> Morphism
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> Morphism
forall a. HasCallStack => FilePath -> a
error (FilePath -> Morphism) -> FilePath -> Morphism
forall a b. (a -> b) -> a -> b
$ "readMorphism : Could not read the " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                           "morphism from " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
file) Maybe Morphism
mor

readMorph :: FilePath -> IO (Maybe Morphism)
readMorph :: FilePath -> IO (Maybe Morphism)
readMorph file :: FilePath
file = do
  Bool
e <- FilePath -> IO Bool
doesFileExist FilePath
file
  if Bool
e then do
       FilePath
content <- FilePath -> IO FilePath
readFile FilePath
file
       case GenParser Char () Morphism
-> () -> FilePath -> FilePath -> Either ParseError Morphism
forall tok st a.
GenParser tok st a
-> st -> FilePath -> [tok] -> Either ParseError a
runParser (GenParser Char () Morphism
forall st. CharParser st Morphism
parseMorphism GenParser Char () Morphism
-> ParsecT FilePath () Identity () -> GenParser Char () Morphism
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT FilePath () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) () FilePath
file FilePath
content of
               Right m :: Morphism
m -> Maybe Morphism -> IO (Maybe Morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Morphism -> IO (Maybe Morphism))
-> Maybe Morphism -> IO (Maybe Morphism)
forall a b. (a -> b) -> a -> b
$ Morphism -> Maybe Morphism
forall a. a -> Maybe a
Just Morphism
m
               Left err :: ParseError
err -> FilePath -> IO (Maybe Morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO (Maybe Morphism))
-> FilePath -> IO (Maybe Morphism)
forall a b. (a -> b) -> a -> b
$ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
err
       else Maybe Morphism -> IO (Maybe Morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Morphism
forall a. Maybe a
Nothing


parseMorphism :: CharParser st Morphism
parseMorphism :: CharParser st Morphism
parseMorphism = do
     CharParser st FilePath -> CharParser st FilePath
forall st a. CharParser st a -> CharParser st a
skips (CharParser st FilePath -> CharParser st FilePath)
-> CharParser st FilePath -> CharParser st FilePath
forall a b. (a -> b) -> a -> b
$ ParsecT FilePath st Identity Char
-> CharParser st FilePath -> CharParser st FilePath
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill ParsecT FilePath st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar (FilePath -> CharParser st FilePath
forall s (m :: * -> *) u.
Stream s m Char =>
FilePath -> ParsecT s u m FilePath
string "=")
     FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Morphism"
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '{'
     FilePath
mb <- FilePath -> CharParser st FilePath
forall st. FilePath -> CharParser st FilePath
parseWithEq "morphBase"
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
     FilePath
mm <- FilePath -> CharParser st FilePath
forall st. FilePath -> CharParser st FilePath
parseWithEq "morphModule"
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
     FilePath
mn <- FilePath -> CharParser st FilePath
forall st. FilePath -> CharParser st FilePath
parseWithEq "morphName"
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
     FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "source"
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
     Sign
s <- CharParser st Sign
forall st. CharParser st Sign
parseSignature
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
     FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "target"
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
     Sign
t <- CharParser st Sign
forall st. CharParser st Sign
parseSignature
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
     FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "morphType"
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
     MorphType
mt <- CharParser st MorphType
forall st. CharParser st MorphType
parseMorphType
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
     FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "symMap"
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
     Map Symbol EXP
sm <- CharParser st (Map Symbol EXP)
forall st. CharParser st (Map Symbol EXP)
parseMap
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '}'
     Morphism -> CharParser st Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> CharParser st Morphism)
-> Morphism -> CharParser st Morphism
forall a b. (a -> b) -> a -> b
$ FilePath
-> FilePath
-> FilePath
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism FilePath
mb FilePath
mm FilePath
mn Sign
s Sign
t MorphType
mt Map Symbol EXP
sm

-- | plain string parser with skip
pkeyword :: String -> CharParser st ()
pkeyword :: FilePath -> CharParser st ()
pkeyword s :: FilePath
s = FilePath -> CharParser st Char -> CharParser st FilePath
forall st. FilePath -> CharParser st Char -> CharParser st FilePath
keywordNotFollowedBy FilePath
s (CharParser st Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum CharParser st Char -> CharParser st Char -> CharParser st Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> CharParser st Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '/') CharParser st FilePath -> CharParser st () -> CharParser st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> CharParser st ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

keywordNotFollowedBy :: String -> CharParser st Char -> CharParser st String
keywordNotFollowedBy :: FilePath -> CharParser st Char -> CharParser st FilePath
keywordNotFollowedBy s :: FilePath
s c :: CharParser st Char
c = CharParser st FilePath -> CharParser st FilePath
forall st a. CharParser st a -> CharParser st a
skips (CharParser st FilePath -> CharParser st FilePath)
-> CharParser st FilePath -> CharParser st FilePath
forall a b. (a -> b) -> a -> b
$ CharParser st FilePath -> CharParser st FilePath
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st FilePath -> CharParser st FilePath)
-> CharParser st FilePath -> CharParser st FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> CharParser st FilePath
forall s (m :: * -> *) u.
Stream s m Char =>
FilePath -> ParsecT s u m FilePath
string FilePath
s CharParser st FilePath
-> ParsecT FilePath st Identity () -> CharParser st FilePath
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser st Char -> ParsecT FilePath st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy CharParser st Char
c

skips :: CharParser st a -> CharParser st a
skips :: CharParser st a -> CharParser st a
skips = (CharParser st a
-> ParsecT FilePath st Identity () -> CharParser st a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT FilePath st Identity () -> ParsecT FilePath st Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany
        (ParsecT FilePath st Identity Char
-> ParsecT FilePath st Identity ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget ParsecT FilePath st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space ParsecT FilePath st Identity ()
-> ParsecT FilePath st Identity ()
-> ParsecT FilePath st Identity ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT FilePath st Identity Annotation
-> ParsecT FilePath st Identity ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget ParsecT FilePath st Identity Annotation
forall st. GenParser Char st Annotation
commentLine ParsecT FilePath st Identity ()
-> ParsecT FilePath st Identity ()
-> ParsecT FilePath st Identity ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT FilePath st Identity ()
forall st. CharParser st ()
nestCommentOut ParsecT FilePath st Identity ()
-> FilePath -> ParsecT FilePath st Identity ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> FilePath -> ParsecT s u m a
<?> ""))

qString :: CharParser st String
qString :: CharParser st FilePath
qString = CharParser st FilePath -> CharParser st FilePath
forall st a. CharParser st a -> CharParser st a
skips CharParser st FilePath
forall st. CharParser st FilePath
endsWithQuot

parensP :: CharParser st a -> CharParser st a
parensP :: CharParser st a -> CharParser st a
parensP p :: CharParser st a
p = ParsecT FilePath st Identity ()
-> ParsecT FilePath st Identity ()
-> CharParser st a
-> CharParser st a
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
between (Char -> ParsecT FilePath st Identity ()
forall st. Char -> CharParser st ()
skipChar '(') (Char -> ParsecT FilePath st Identity ()
forall st. Char -> CharParser st ()
skipChar ')') CharParser st a
p
     CharParser st a -> CharParser st a -> CharParser st a
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st a
p

bracesP :: CharParser st a -> CharParser st a
bracesP :: CharParser st a -> CharParser st a
bracesP = ParsecT FilePath st Identity ()
-> ParsecT FilePath st Identity ()
-> CharParser st a
-> CharParser st a
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
between (Char -> ParsecT FilePath st Identity ()
forall st. Char -> CharParser st ()
skipChar '{') (Char -> ParsecT FilePath st Identity ()
forall st. Char -> CharParser st ()
skipChar '}')

bracketsP :: CharParser st a -> CharParser st a
bracketsP :: CharParser st a -> CharParser st a
bracketsP = ParsecT FilePath st Identity ()
-> ParsecT FilePath st Identity ()
-> CharParser st a
-> CharParser st a
forall s (m :: * -> *) t u open close a.
Stream s m t =>
ParsecT s u m open
-> ParsecT s u m close -> ParsecT s u m a -> ParsecT s u m a
between (Char -> ParsecT FilePath st Identity ()
forall st. Char -> CharParser st ()
skipChar '[') (Char -> ParsecT FilePath st Identity ()
forall st. Char -> CharParser st ()
skipChar ']')

endsWithQuot :: CharParser st String
endsWithQuot :: CharParser st FilePath
endsWithQuot = do
     Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '"'
     ParsecT FilePath st Identity Char
-> CharParser st FilePath -> CharParser st FilePath
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill ParsecT FilePath st Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar (FilePath -> CharParser st FilePath
forall s (m :: * -> *) u.
Stream s m Char =>
FilePath -> ParsecT s u m FilePath
string "\"")

commaP :: CharParser st ()
commaP :: CharParser st ()
commaP = Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ',' CharParser st () -> CharParser st () -> CharParser st ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> CharParser st ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

sepByComma :: CharParser st a -> CharParser st [a]
sepByComma :: CharParser st a -> CharParser st [a]
sepByComma p :: CharParser st a
p = CharParser st a
-> ParsecT FilePath st Identity () -> CharParser st [a]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
sepBy1 CharParser st a
p ParsecT FilePath st Identity ()
forall st. CharParser st ()
commaP

skipChar :: Char -> CharParser st ()
skipChar :: Char -> CharParser st ()
skipChar = ParsecT FilePath st Identity Char -> CharParser st ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (ParsecT FilePath st Identity Char -> CharParser st ())
-> (Char -> ParsecT FilePath st Identity Char)
-> Char
-> CharParser st ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParsecT FilePath st Identity Char
-> ParsecT FilePath st Identity Char
forall st a. CharParser st a -> CharParser st a
skips (ParsecT FilePath st Identity Char
 -> ParsecT FilePath st Identity Char)
-> (Char -> ParsecT FilePath st Identity Char)
-> Char
-> ParsecT FilePath st Identity Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ParsecT FilePath st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char

parseWithEq :: String -> CharParser st String
parseWithEq :: FilePath -> CharParser st FilePath
parseWithEq s :: FilePath
s = do
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword FilePath
s
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
    CharParser st FilePath
forall st. CharParser st FilePath
qString

parseSym :: CharParser st Symbol
parseSym :: CharParser st Symbol
parseSym = do
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Symbol"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '{'
    FilePath
sb <- FilePath -> CharParser st FilePath
forall st. FilePath -> CharParser st FilePath
parseWithEq "symBase"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
    FilePath
sm <- FilePath -> CharParser st FilePath
forall st. FilePath -> CharParser st FilePath
parseWithEq "symModule"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
    FilePath
sn <- FilePath -> CharParser st FilePath
forall st. FilePath -> CharParser st FilePath
parseWithEq "symName"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '}'
    Symbol -> CharParser st Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> CharParser st Symbol) -> Symbol -> CharParser st Symbol
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> Symbol
Symbol FilePath
sb FilePath
sm FilePath
sn

parse1Context :: CharParser st CONTEXT
parse1Context :: CharParser st CONTEXT
parse1Context = do
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '('
    FilePath
v <- CharParser st FilePath
forall st. CharParser st FilePath
qString
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
    EXP
e <- CharParser st EXP
forall st. CharParser st EXP
parseExp
    () -> CharParser st () -> CharParser st ()
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option () (CharParser st () -> CharParser st ())
-> CharParser st () -> CharParser st ()
forall a b. (a -> b) -> a -> b
$ Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ')'
    CONTEXT -> CharParser st CONTEXT
forall (m :: * -> *) a. Monad m => a -> m a
return [(FilePath
v, EXP
e)]

parseExp :: CharParser st EXP
parseExp :: CharParser st EXP
parseExp = (FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Type" CharParser st () -> CharParser st EXP -> CharParser st EXP
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> EXP -> CharParser st EXP
forall (m :: * -> *) a. Monad m => a -> m a
return EXP
Type)
   CharParser st EXP -> CharParser st EXP -> CharParser st EXP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Var"
    (FilePath -> EXP)
-> ParsecT FilePath st Identity FilePath -> CharParser st EXP
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FilePath -> EXP
Var ParsecT FilePath st Identity FilePath
forall st. CharParser st FilePath
qString
   CharParser st EXP -> CharParser st EXP -> CharParser st EXP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Const"
    (Symbol -> EXP)
-> ParsecT FilePath st Identity Symbol -> CharParser st EXP
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Symbol -> EXP
Const ParsecT FilePath st Identity Symbol
forall st. CharParser st Symbol
parseSym
   CharParser st EXP -> CharParser st EXP -> CharParser st EXP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Appl"
    EXP
ex <- CharParser st EXP -> CharParser st EXP
forall st a. CharParser st a -> CharParser st a
parensP CharParser st EXP
forall st. CharParser st EXP
parseExp
    [EXP]
exl <- CharParser st [EXP] -> CharParser st [EXP]
forall st a. CharParser st a -> CharParser st a
bracketsP (CharParser st [EXP] -> CharParser st [EXP])
-> CharParser st [EXP] -> CharParser st [EXP]
forall a b. (a -> b) -> a -> b
$ [EXP] -> CharParser st [EXP] -> CharParser st [EXP]
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option [] (CharParser st [EXP] -> CharParser st [EXP])
-> CharParser st [EXP] -> CharParser st [EXP]
forall a b. (a -> b) -> a -> b
$ CharParser st EXP -> CharParser st [EXP]
forall st a. CharParser st a -> CharParser st [a]
sepByComma CharParser st EXP
forall st. CharParser st EXP
parseExp
    EXP -> CharParser st EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> CharParser st EXP) -> EXP -> CharParser st EXP
forall a b. (a -> b) -> a -> b
$ EXP -> [EXP] -> EXP
Appl EXP
ex [EXP]
exl
   CharParser st EXP -> CharParser st EXP -> CharParser st EXP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Func"
    [EXP]
exl <- CharParser st [EXP] -> CharParser st [EXP]
forall st a. CharParser st a -> CharParser st a
bracketsP (CharParser st [EXP] -> CharParser st [EXP])
-> CharParser st [EXP] -> CharParser st [EXP]
forall a b. (a -> b) -> a -> b
$ [EXP] -> CharParser st [EXP] -> CharParser st [EXP]
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option [] (CharParser st [EXP] -> CharParser st [EXP])
-> CharParser st [EXP] -> CharParser st [EXP]
forall a b. (a -> b) -> a -> b
$ CharParser st EXP -> CharParser st [EXP]
forall st a. CharParser st a -> CharParser st [a]
sepByComma CharParser st EXP
forall st. CharParser st EXP
parseExp
    EXP
ex <- CharParser st EXP -> CharParser st EXP
forall st a. CharParser st a -> CharParser st a
parensP CharParser st EXP
forall st. CharParser st EXP
parseExp
    EXP -> CharParser st EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> CharParser st EXP) -> EXP -> CharParser st EXP
forall a b. (a -> b) -> a -> b
$ [EXP] -> EXP -> EXP
Func [EXP]
exl EXP
ex
   CharParser st EXP -> CharParser st EXP -> CharParser st EXP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    FilePath
ty <- [ParsecT FilePath st Identity FilePath]
-> ParsecT FilePath st Identity FilePath
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([ParsecT FilePath st Identity FilePath]
 -> ParsecT FilePath st Identity FilePath)
-> [ParsecT FilePath st Identity FilePath]
-> ParsecT FilePath st Identity FilePath
forall a b. (a -> b) -> a -> b
$ (FilePath -> ParsecT FilePath st Identity FilePath)
-> [FilePath] -> [ParsecT FilePath st Identity FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (\ ty :: FilePath
ty -> FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword FilePath
ty CharParser st ()
-> ParsecT FilePath st Identity FilePath
-> ParsecT FilePath st Identity FilePath
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FilePath -> ParsecT FilePath st Identity FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
ty)
               ["Pi", "Lamb"]
    [CONTEXT]
c <- CharParser st [CONTEXT] -> CharParser st [CONTEXT]
forall st a. CharParser st a -> CharParser st a
bracketsP (CharParser st [CONTEXT] -> CharParser st [CONTEXT])
-> CharParser st [CONTEXT] -> CharParser st [CONTEXT]
forall a b. (a -> b) -> a -> b
$ [CONTEXT] -> CharParser st [CONTEXT] -> CharParser st [CONTEXT]
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option [] (CharParser st [CONTEXT] -> CharParser st [CONTEXT])
-> CharParser st [CONTEXT] -> CharParser st [CONTEXT]
forall a b. (a -> b) -> a -> b
$ CharParser st CONTEXT -> CharParser st [CONTEXT]
forall st a. CharParser st a -> CharParser st [a]
sepByComma CharParser st CONTEXT
forall st. CharParser st CONTEXT
parse1Context
    EXP
e <- CharParser st EXP -> CharParser st EXP
forall st a. CharParser st a -> CharParser st a
parensP CharParser st EXP
forall st. CharParser st EXP
parseExp
    EXP -> CharParser st EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> CharParser st EXP) -> EXP -> CharParser st EXP
forall a b. (a -> b) -> a -> b
$ (case FilePath
ty of
        "Pi" -> CONTEXT -> EXP -> EXP
Pi
        "Lamb" -> CONTEXT -> EXP -> EXP
Lamb
        _ -> FilePath -> CONTEXT -> EXP -> EXP
forall a. HasCallStack => FilePath -> a
error "Pi or Lamb expected.\n") ([CONTEXT] -> CONTEXT
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [CONTEXT]
c) EXP
e

parseDef :: CharParser st DEF
parseDef :: CharParser st DEF
parseDef = do
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Def"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '{'
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "getSym"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
    Symbol
sym <- CharParser st Symbol
forall st. CharParser st Symbol
parseSym
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "getType"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
    EXP
tp <- CharParser st EXP
forall st. CharParser st EXP
parseExp
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "getValue"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
    Maybe EXP
val <- (FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Nothing" CharParser st ()
-> ParsecT FilePath st Identity (Maybe EXP)
-> ParsecT FilePath st Identity (Maybe EXP)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe EXP -> ParsecT FilePath st Identity (Maybe EXP)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe EXP
forall a. Maybe a
Nothing)
             ParsecT FilePath st Identity (Maybe EXP)
-> ParsecT FilePath st Identity (Maybe EXP)
-> ParsecT FilePath st Identity (Maybe EXP)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Just"
                    EXP
e <- CharParser st EXP -> CharParser st EXP
forall st a. CharParser st a -> CharParser st a
parensP CharParser st EXP
forall st. CharParser st EXP
parseExp
                    Maybe EXP -> ParsecT FilePath st Identity (Maybe EXP)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe EXP -> ParsecT FilePath st Identity (Maybe EXP))
-> Maybe EXP -> ParsecT FilePath st Identity (Maybe EXP)
forall a b. (a -> b) -> a -> b
$ EXP -> Maybe EXP
forall a. a -> Maybe a
Just EXP
e
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '}'
    DEF -> CharParser st DEF
forall (m :: * -> *) a. Monad m => a -> m a
return (DEF -> CharParser st DEF) -> DEF -> CharParser st DEF
forall a b. (a -> b) -> a -> b
$ Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
sym EXP
tp Maybe EXP
val

parseSignature :: CharParser st Sign
parseSignature :: CharParser st Sign
parseSignature = do
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "Sign"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '{'
    FilePath
sb <- FilePath -> CharParser st FilePath
forall st. FilePath -> CharParser st FilePath
parseWithEq "sigBase"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
    FilePath
sm <- FilePath -> CharParser st FilePath
forall st. FilePath -> CharParser st FilePath
parseWithEq "sigModule"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
    FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "getDefs"
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '='
    [DEF]
sd <- CharParser st [DEF] -> CharParser st [DEF]
forall st a. CharParser st a -> CharParser st a
bracketsP (CharParser st [DEF] -> CharParser st [DEF])
-> CharParser st [DEF] -> CharParser st [DEF]
forall a b. (a -> b) -> a -> b
$ [DEF] -> CharParser st [DEF] -> CharParser st [DEF]
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option [] (CharParser st [DEF] -> CharParser st [DEF])
-> CharParser st [DEF] -> CharParser st [DEF]
forall a b. (a -> b) -> a -> b
$ CharParser st DEF -> CharParser st [DEF]
forall st a. CharParser st a -> CharParser st [a]
sepByComma CharParser st DEF
forall st. CharParser st DEF
parseDef
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '}'
    Sign -> CharParser st Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> CharParser st Sign) -> Sign -> CharParser st Sign
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [DEF] -> Sign
Sign FilePath
sb FilePath
sm [DEF]
sd

parseMorphType :: CharParser st MorphType
parseMorphType :: CharParser st MorphType
parseMorphType =
     [CharParser st MorphType] -> CharParser st MorphType
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([CharParser st MorphType] -> CharParser st MorphType)
-> [CharParser st MorphType] -> CharParser st MorphType
forall a b. (a -> b) -> a -> b
$ (MorphType -> CharParser st MorphType)
-> [MorphType] -> [CharParser st MorphType]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: MorphType
t -> FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword (MorphType -> FilePath
forall a. Show a => a -> FilePath
show MorphType
t) CharParser st ()
-> CharParser st MorphType -> CharParser st MorphType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MorphType -> CharParser st MorphType
forall (m :: * -> *) a. Monad m => a -> m a
return MorphType
t)
          [MorphType
Definitional, MorphType
Postulated, MorphType
Unknown ]

parse1Map :: CharParser st (Symbol, EXP)
parse1Map :: CharParser st (Symbol, EXP)
parse1Map = do
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar '('
    Symbol
s <- CharParser st Symbol
forall st. CharParser st Symbol
parseSym
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ','
    EXP
e <- CharParser st EXP
forall st. CharParser st EXP
parseExp
    Char -> CharParser st ()
forall st. Char -> CharParser st ()
skipChar ')'
    (Symbol, EXP) -> CharParser st (Symbol, EXP)
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
s, EXP
e)

parseMap :: CharParser st (Map.Map Symbol EXP)
parseMap :: CharParser st (Map Symbol EXP)
parseMap = do
     FilePath -> CharParser st ()
forall st. FilePath -> CharParser st ()
pkeyword "fromList"
     ([(Symbol, EXP)] -> Map Symbol EXP)
-> ParsecT FilePath st Identity [(Symbol, EXP)]
-> CharParser st (Map Symbol EXP)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Symbol, EXP)] -> Map Symbol EXP
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (ParsecT FilePath st Identity [(Symbol, EXP)]
 -> CharParser st (Map Symbol EXP))
-> ParsecT FilePath st Identity [(Symbol, EXP)]
-> CharParser st (Map Symbol EXP)
forall a b. (a -> b) -> a -> b
$ ParsecT FilePath st Identity [(Symbol, EXP)]
-> ParsecT FilePath st Identity [(Symbol, EXP)]
forall st a. CharParser st a -> CharParser st a
bracketsP (ParsecT FilePath st Identity [(Symbol, EXP)]
 -> ParsecT FilePath st Identity [(Symbol, EXP)])
-> ParsecT FilePath st Identity [(Symbol, EXP)]
-> ParsecT FilePath st Identity [(Symbol, EXP)]
forall a b. (a -> b) -> a -> b
$ [(Symbol, EXP)]
-> ParsecT FilePath st Identity [(Symbol, EXP)]
-> ParsecT FilePath st Identity [(Symbol, EXP)]
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option [] (ParsecT FilePath st Identity [(Symbol, EXP)]
 -> ParsecT FilePath st Identity [(Symbol, EXP)])
-> ParsecT FilePath st Identity [(Symbol, EXP)]
-> ParsecT FilePath st Identity [(Symbol, EXP)]
forall a b. (a -> b) -> a -> b
$ CharParser st (Symbol, EXP)
-> ParsecT FilePath st Identity [(Symbol, EXP)]
forall st a. CharParser st a -> CharParser st [a]
sepByComma CharParser st (Symbol, EXP)
forall st. CharParser st (Symbol, EXP)
parse1Map