da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinmodule LF.MorphParser where

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport LF.Sign

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport LF.Morphism

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport Common.Lexer

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport Common.Parsec

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport Common.AnnoParser (commentLine)

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport Text.ParserCombinators.Parsec

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport System.Directory

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport System.IO.Unsafe

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport Debug.Trace

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinimport qualified Data.Map as Map

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinreadMorphism :: FilePath -> Morphism

7c2fbfb345896881c631598ee3852ce9ce33fb07April ChinreadMorphism file | trace ("readMorphism called on " ++ file ++ "\n") False = undefined

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinreadMorphism file =

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza let mor = unsafePerformIO $ readMorph file

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin in case mor of

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin Just m -> m

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin Nothing -> error $ "readMorphism : Could not read the " ++

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chin "morphism from " ++ (show file)

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazareadMorph :: FilePath -> IO (Maybe Morphism)

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinreadMorph file = do

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza e <- doesFileExist file

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin if e then do

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin content <- readFile file

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

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin Right m -> return $ Just m

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin Left err -> fail $ show err

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin else return Nothing

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chin

7c2fbfb345896881c631598ee3852ce9ce33fb07April ChinparseMorphism :: CharParser st Morphism

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazaparseMorphism = do

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza skips $ manyTill anyChar (string "=")

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza pkeyword "Morphism"

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza skipChar '{'

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin mb <- parseWithEq "morphBase"

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar ','

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin mm <- parseWithEq "morphModule"

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar ','

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin mn <- parseWithEq "morphName"

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar ','

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin pkeyword "source"

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar '='

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin s <- parseSignature

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar ','

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin pkeyword "target"

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar '='

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin t <- parseSignature

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar ','

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin pkeyword "morphType"

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar '='

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin mt <- parseMorphType

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar ','

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin pkeyword "symMap"

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chin skipChar '='

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chin sm <- parseMap

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar '}'

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin return $ Morphism mb mm mn s t mt sm

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chin-- | plain string parser with skip

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chinpkeyword :: String -> CharParser st ()

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chinpkeyword s = keywordNotFollowedBy s (alphaNum <|> char '/') >> return ()

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinkeywordNotFollowedBy :: String -> CharParser st Char -> CharParser st String

7c2fbfb345896881c631598ee3852ce9ce33fb07April ChinkeywordNotFollowedBy s c = skips $ try $ string s << notFollowedBy c

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chin

7c2fbfb345896881c631598ee3852ce9ce33fb07April Chinskips :: CharParser st a -> CharParser st a

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinskips = (<< skipMany

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

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazaqString :: CharParser st String

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazaqString = skips endsWithQuot

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazaparensP :: CharParser st a -> CharParser st a

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazaparensP p = between (skipChar '(') (skipChar ')') p

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza <|> p

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazabracesP :: CharParser st a -> CharParser st a

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazabracesP = between (skipChar '{') (skipChar '}')

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazabracketsP :: CharParser st a -> CharParser st a

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane PrazabracketsP = between (skipChar '[') (skipChar ']')

ead1f93ee620d7580f7e53350fe5a884fc4f158aLiane Praza

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinendsWithQuot :: CharParser st String

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chinendsWithQuot = do

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin skipChar '"'

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin manyTill anyChar (string "\"") >>= return

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chin

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chincommaP :: CharParser st ()

da2e3ebdc1edfbc5028edf1354e7dd2fa69a7968chincommaP = 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 >>= return

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

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

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