2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovmodule LF.MorphParser where

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport LF.Sign

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport LF.Morphism

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport Common.Lexer

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport Common.Parsec

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport Common.AnnoParser (commentLine)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport Text.ParserCombinators.Parsec

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatovimport System.Directory

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatovimport System.IO.Unsafe

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport qualified Data.Map as Map

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Maybe (fromMaybe)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovreadMorphism :: FilePath -> Morphism

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovreadMorphism file =

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov let mor = unsafePerformIO $ readMorph file

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in fromMaybe (error $ "readMorphism : Could not read the " ++

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "morphism from " ++ show file) mor

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovreadMorph :: FilePath -> IO (Maybe Morphism)

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovreadMorph file = do

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov e <- doesFileExist file

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov if e then do

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov content <- readFile file

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

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov Right m -> return $ Just m

1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov Left err -> error $ show err

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov else return Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovparseMorphism :: CharParser st Morphism

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovparseMorphism = do

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skips $ manyTill anyChar (string "=")

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pkeyword "Morphism"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar '{'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mb <- parseWithEq "morphBase"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar ','

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov mm <- parseWithEq "morphModule"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar ','

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov mn <- parseWithEq "morphName"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar ','

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov pkeyword "source"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar '='

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov s <- parseSignature

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar ','

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov pkeyword "target"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar '='

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov t <- parseSignature

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar ','

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov pkeyword "morphType"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar '='

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov mt <- parseMorphType

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar ','

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov pkeyword "symMap"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar '='

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov sm <- parseMap

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skipChar '}'

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov return $ Morphism mb mm mn s t mt sm

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov-- | plain string parser with skip

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovpkeyword :: String -> CharParser st ()

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovpkeyword s = keywordNotFollowedBy s (alphaNum <|> char '/') >> return ()

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovkeywordNotFollowedBy :: String -> CharParser st Char -> CharParser st String

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovkeywordNotFollowedBy s c = skips $ try $ string s << notFollowedBy c

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovskips :: CharParser st a -> CharParser st a

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovskips = (<< skipMany

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov (forget space <|> forget commentLine <|> nestCommentOut <?> ""))

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovqString :: CharParser st String

4291a11e37b6be55b237493ac75b2b54173ce983Iulia IgnatovqString = skips endsWithQuot

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparensP :: CharParser st a -> CharParser st a

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovparensP p = between (skipChar '(') (skipChar ')') p

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov <|> p

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovbracesP :: CharParser st a -> CharParser st a

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovbracesP = between (skipChar '{') (skipChar '}')

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovbracketsP :: CharParser st a -> CharParser st a

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovbracketsP = between (skipChar '[') (skipChar ']')

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

4291a11e37b6be55b237493ac75b2b54173ce983Iulia IgnatovendsWithQuot :: CharParser st String

4291a11e37b6be55b237493ac75b2b54173ce983Iulia IgnatovendsWithQuot = do

4291a11e37b6be55b237493ac75b2b54173ce983Iulia Ignatov skipChar '"'

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder manyTill anyChar (string "\"")

4291a11e37b6be55b237493ac75b2b54173ce983Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovcommaP :: CharParser st ()

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovcommaP = skipChar ',' >> return ()

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovsepByComma :: CharParser st a -> CharParser st [a]

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovsepByComma p = sepBy1 p commaP

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovskipChar :: Char -> CharParser st ()

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovskipChar = forget . skips . char

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseWithEq :: String -> CharParser st String

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseWithEq s = do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword s

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder skipChar '='

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder qString

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseSym :: CharParser st Symbol

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederparseSym = do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Symbol"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '{'

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sb <- parseWithEq "symBase"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ','

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sm <- parseWithEq "symModule"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ','

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sn <- parseWithEq "symName"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '}'

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Symbol sb sm sn

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovparse1Context :: CharParser st CONTEXT

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovparse1Context = do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '('

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov v <- qString

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ','

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov e <- parseExp

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov option () $ skipChar ')'

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return [(v, e)]

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseExp :: CharParser st EXP

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederparseExp = (pkeyword "Type" >> return Type)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov <|> do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Var"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov fmap Var qString

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder <|> do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Const"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov fmap Const parseSym

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov <|> do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Appl"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov ex <- parensP parseExp

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov exl <- bracketsP $ option [] $ sepByComma parseExp

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Appl ex exl

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov <|> do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Func"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov exl <- bracketsP $ option [] $ sepByComma parseExp

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov ex <- parensP parseExp

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Func exl ex

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov <|> do

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

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov ["Pi", "Lamb"]

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov c <- bracketsP $ option [] $ sepByComma parse1Context

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder e <- parensP parseExp

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ (case ty of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Pi" -> Pi

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov "Lamb" -> Lamb

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

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseDef :: CharParser st DEF

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseDef = do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Def"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '{'

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "getSym"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '='

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sym <- parseSym

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ','

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "getType"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '='

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov tp <- parseExp

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ','

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "getValue"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '='

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder val <- (pkeyword "Nothing" >> return Nothing)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov <|> do pkeyword "Just"

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov e <- parensP parseExp

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Just e

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '}'

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Def sym tp val

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseSignature :: CharParser st Sign

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseSignature = do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Sign"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '{'

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sb <- parseWithEq "sigBase"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ','

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sm <- parseWithEq "sigModule"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ','

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "getDefs"

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '='

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sd <- bracketsP $ option [] $ sepByComma parseDef

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '}'

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Sign sb sm sd

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseMorphType :: CharParser st MorphType

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederparseMorphType =

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

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov [Definitional, Postulated, Unknown ]

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovparse1Map :: CharParser st (Symbol, EXP)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovparse1Map = do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar '('

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov s <- parseSym

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ','

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov e <- parseExp

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov skipChar ')'

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return (s, e)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseMap :: CharParser st (Map.Map Symbol EXP)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseMap = do

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "fromList"

1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov fmap Map.fromList $ bracketsP $ option [] $ sepByComma parse1Map