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 file =

let mor = unsafePerformIO $ readMorph file

in fromMaybe (error $ "readMorphism : Could not read the " ++

"morphism from " ++ show file) mor

readMorph :: FilePath -> IO (Maybe Morphism)

readMorph file = do

e <- doesFileExist file

if e then do

content <- readFile file

case runParser (parseMorphism << eof) () file content of

Right m -> return $ Just m

Left err -> error $ show err

else return Nothing

parseMorphism :: CharParser st Morphism

parseMorphism = do

skips $ manyTill anyChar (string "=")

pkeyword "Morphism"

skipChar '{'

mb <- parseWithEq "morphBase"

skipChar ','

mm <- parseWithEq "morphModule"

skipChar ','

mn <- parseWithEq "morphName"

skipChar ','

pkeyword "source"

skipChar '='

s <- parseSignature

skipChar ','

pkeyword "target"

skipChar '='

t <- parseSignature

skipChar ','

pkeyword "morphType"

skipChar '='

mt <- parseMorphType

skipChar ','

pkeyword "symMap"

skipChar '='

sm <- parseMap

skipChar '}'

return $ Morphism mb mm mn s t mt sm

-- | plain string parser with skip

pkeyword :: String -> CharParser st ()

pkeyword s = keywordNotFollowedBy s (alphaNum <|> char '/') >> return ()

keywordNotFollowedBy :: String -> CharParser st Char -> CharParser st String

keywordNotFollowedBy s c = skips $ try $ string s << notFollowedBy c

skips :: CharParser st a -> CharParser st a

skips = (<< skipMany

(forget space <|> forget commentLine <|> nestCommentOut <?> ""))

qString :: CharParser st String

qString = skips endsWithQuot

parensP :: CharParser st a -> CharParser st a

parensP p = between (skipChar '(') (skipChar ')') p

<|> p

bracesP :: CharParser st a -> CharParser st a

bracesP = between (skipChar '{') (skipChar '}')

bracketsP :: CharParser st a -> CharParser st a

bracketsP = between (skipChar '[') (skipChar ']')

endsWithQuot :: CharParser st String

endsWithQuot = do

skipChar '"'

manyTill anyChar (string "\"")

commaP :: CharParser st ()

commaP = skipChar ',' >> return ()

sepByComma :: CharParser st a -> CharParser st [a]

sepByComma p = sepBy1 p commaP

skipChar :: Char -> CharParser st ()

skipChar = forget . skips . char

parseWithEq :: String -> CharParser st String

parseWithEq s = do

pkeyword s

skipChar '='

qString

parseSym :: CharParser st Symbol

parseSym = do

pkeyword "Symbol"

skipChar '{'

sb <- parseWithEq "symBase"

skipChar ','

sm <- parseWithEq "symModule"

skipChar ','

sn <- parseWithEq "symName"

skipChar '}'

return $ Symbol sb sm sn

parse1Context :: CharParser st CONTEXT

parse1Context = do

skipChar '('

v <- qString

skipChar ','

e <- parseExp

option () $ skipChar ')'

return [(v, e)]

parseExp :: CharParser st EXP

parseExp = (pkeyword "Type" >> return Type)

<|> do

pkeyword "Var"

fmap Var qString

<|> do

pkeyword "Const"

fmap Const parseSym

<|> do

pkeyword "Appl"

ex <- parensP parseExp

exl <- bracketsP $ option [] $ sepByComma parseExp

return $ Appl ex exl

<|> do

pkeyword "Func"

exl <- bracketsP $ option [] $ sepByComma parseExp

ex <- parensP parseExp

return $ Func exl ex

<|> do

ty <- choice $ map (\ ty -> pkeyword ty >> return ty)

["Pi", "Lamb"]

c <- bracketsP $ option [] $ sepByComma parse1Context

e <- parensP parseExp

return $ (case ty of

"Pi" -> Pi

"Lamb" -> Lamb

_ -> error "Pi or Lamb expected.\n") (concat c) e

parseDef :: CharParser st DEF

parseDef = do

pkeyword "Def"

skipChar '{'

pkeyword "getSym"

skipChar '='

sym <- parseSym

skipChar ','

pkeyword "getType"

skipChar '='

tp <- parseExp

skipChar ','

pkeyword "getValue"

skipChar '='

val <- (pkeyword "Nothing" >> return Nothing)

<|> do pkeyword "Just"

e <- parensP parseExp

return $ Just e

skipChar '}'

return $ Def sym tp val

parseSignature :: CharParser st Sign

parseSignature = do

pkeyword "Sign"

skipChar '{'

sb <- parseWithEq "sigBase"

skipChar ','

sm <- parseWithEq "sigModule"

skipChar ','

pkeyword "getDefs"

skipChar '='

sd <- bracketsP $ option [] $ sepByComma parseDef

skipChar '}'

return $ Sign sb sm sd

parseMorphType :: CharParser st MorphType

parseMorphType =

choice $ map (\ t -> pkeyword (show t) >> return t)

[Definitional, Postulated, Unknown ]

parse1Map :: CharParser st (Symbol, EXP)

parse1Map = do

skipChar '('

s <- parseSym

skipChar ','

e <- parseExp

skipChar ')'

return (s, e)

parseMap :: CharParser st (Map.Map Symbol EXP)

parseMap = do

pkeyword "fromList"

fmap Map.fromList $ bracketsP $ option [] $ sepByComma parse1Map