MorphParser.hs revision 1584a6ae7a65f19507aae1dfc2a7a3669a90ba5f
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport Common.AnnoParser (commentLine)
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovimport qualified Data.Map as Map
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovreadMorphism :: FilePath -> Morphism
4291a11e37b6be55b237493ac75b2b54173ce983Iulia IgnatovreadMorphism file | trace ("readMorphism called on " ++ file ++ "\n") False = undefined
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovreadMorphism file =
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov let mor = unsafePerformIO $ readMorph file
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov in case mor of
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov Nothing -> error $ "readMorphism : Could not read the " ++
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov "morphism from " ++ (show file)
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovreadMorph :: FilePath -> IO (Maybe Morphism)
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia IgnatovreadMorph file | trace ("readMorph called on " ++ file ++ "\n") False = undefined
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovreadMorph file = do
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov e <- doesFileExist file
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
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovparseMorphism :: CharParser st Morphism
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parseMorphism | trace ("parse morphism\n") False = undefined
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovparseMorphism = do
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov skips $ manyTill anyChar (string "=")
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov pkeyword "Morphism"
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov mb <- parseWithEq "morphBase"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov mm <- parseWithEq "morphModule"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov mn <- parseWithEq "morphName"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov pkeyword "source"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov s <- parseSignature
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov pkeyword "target"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov t <- parseSignature
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov pkeyword "morphType"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov mt <- parseMorphType
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov pkeyword "symMap"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov sm <- parseMap
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov return $ Morphism mb mm mn s t mt sm
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov-- | plain string parser with skip
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovpkeyword :: String -> CharParser st ()
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- pkeyword s | trace s False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovpkeyword s = keywordNotFollowedBy s (alphaNum <|> char '/') >> return ()
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovkeywordNotFollowedBy :: String -> CharParser st Char -> CharParser st String
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- keywordNotFollowedBy s _ | trace ("keywordNotFollowedBy " ++ s ++ "\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovkeywordNotFollowedBy s c = skips $ try $ string s << notFollowedBy c
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovskips :: CharParser st a -> CharParser st a
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovskips = (<< skipMany
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov (forget space <|> forget commentLine <|> nestCommentOut <?> ""))
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovqString :: CharParser st String
4291a11e37b6be55b237493ac75b2b54173ce983Iulia IgnatovqString = skips endsWithQuot
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparensP :: CharParser st a -> CharParser st a
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia IgnatovparensP p = between (skipChar '(') (skipChar ')') p
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovbracesP :: CharParser st a -> CharParser st a
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovbracesP = between (skipChar '{') (skipChar '}')
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovbracketsP :: CharParser st a -> CharParser st a
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovbracketsP = between (skipChar '[') (skipChar ']')
4291a11e37b6be55b237493ac75b2b54173ce983Iulia IgnatovendsWithQuot :: CharParser st String
4291a11e37b6be55b237493ac75b2b54173ce983Iulia IgnatovendsWithQuot = do
4291a11e37b6be55b237493ac75b2b54173ce983Iulia Ignatov manyTill anyChar (string "\"") >>= return
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovcommaP :: CharParser st ()
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovcommaP = skipChar ',' >> return ()
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovsepByComma :: CharParser st a -> CharParser st [a]
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- sepByComma _ | trace ("sepByComma\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovsepByComma p = sepBy1 p commaP
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovskipChar :: Char -> CharParser st ()
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovskipChar = forget . skips . char
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseWithEq :: String -> CharParser st String
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parseWithEq s | trace ("parseWithEq" ++ s ++ "\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseWithEq s = do
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov qString >>= return
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseSym :: CharParser st Symbol
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parseSym | trace ("parseSym\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Symbol"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sb <- parseWithEq "symBase"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sm <- parseWithEq "symModule"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sn <- parseWithEq "symName"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Symbol sb sm sn
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovparse1Context :: CharParser st CONTEXT
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parse1Context | trace ("parse1Context\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovparse1Context = do
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov e <- parseExp
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov option () $ skipChar ')'
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return [(v, e)]
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseExp :: CharParser st EXP
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parseExp | trace ("parseExp\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Type" >> return Type
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Var"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov fmap Var qString
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Const"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov fmap Const parseSym
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Appl"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov ex <- parensP parseExp
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov exl <- bracketsP $ option [] $ sepByComma parseExp
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Appl ex exl
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Func"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov exl <- bracketsP $ option [] $ sepByComma parseExp
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov ex <- parensP parseExp
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Func exl ex
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov ty <- choice $ map (\ ty -> pkeyword ty >> return ty)
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov ["Pi", "Lamb"]
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov c <- bracketsP $ option [] $ sepByComma parse1Context
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov e <- parensP parseExp
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ (case ty of
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov "Lamb" -> Lamb
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov _ -> error $ "Pi or Lamb expected.\n") (concat c) e
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseDef :: CharParser st DEF
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parseDef | trace ("parseDef\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Def"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "getSym"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sym <- parseSym
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "getType"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov tp <- parseExp
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "getValue"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov val <- do pkeyword "Nothing" >> return Nothing
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov <|> do pkeyword "Just"
b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov e <- parensP parseExp
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Just e
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Def sym tp val
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseSignature :: CharParser st Sign
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parseSignature | trace ("parseSignature\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseSignature = do
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "Sign"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sb <- parseWithEq "sigBase"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sm <- parseWithEq "sigModule"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "getDefs"
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov sd <- bracketsP $ option [] $ sepByComma parseDef
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return $ Sign sb sm sd
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseMorphType :: CharParser st MorphType
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parseMorphType | trace ("parseMorphType\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseMorphType = do
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov choice $ map (\ t -> pkeyword (show t) >> return t)
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov [Definitional, Postulated, Unknown ]
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovparse1Map :: CharParser st (Symbol, EXP)
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parse1Map | trace ("parse1Map\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatovparse1Map = do
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov s <- parseSym
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov e <- parseExp
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov return (s, e)
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia IgnatovparseMap :: CharParser st (Map.Map Symbol EXP)
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov-- parseMap | trace ("parseMap\n") False = undefined
2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov pkeyword "fromList"
1584a6ae7a65f19507aae1dfc2a7a3669a90ba5fIulia Ignatov fmap Map.fromList $ bracketsP $ option [] $ sepByComma parse1Map