module IRTS.LParser where import Core.CoreParser import Core.TT import IRTS.Lang import IRTS.Simplified import IRTS.Bytecode import IRTS.CodegenC import IRTS.Defunctionalise import Paths_idris import Text.ParserCombinators.Parsec import Text.ParserCombinators.Parsec.Error import Text.ParserCombinators.Parsec.Expr import Text.ParserCombinators.Parsec.Language import qualified Text.ParserCombinators.Parsec.Token as PTok import Data.List import Control.Monad.State import Debug.Trace import Data.Maybe import System.FilePath type TokenParser a = PTok.TokenParser a type LParser = GenParser Char () lexer :: TokenParser () lexer = PTok.makeTokenParser idrisDef whiteSpace= PTok.whiteSpace lexer lexeme = PTok.lexeme lexer symbol = PTok.symbol lexer natural = PTok.natural lexer parens = PTok.parens lexer semi = PTok.semi lexer comma = PTok.comma lexer identifier= PTok.identifier lexer reserved = PTok.reserved lexer operator = PTok.operator lexer reservedOp= PTok.reservedOp lexer integer = PTok.integer lexer float = PTok.float lexer strlit = PTok.stringLiteral lexer chlit = PTok.charLiteral lexer lchar = lexeme.char fovm :: FilePath -> IO () fovm f = do defs <- parseFOVM f let (nexttag, tagged) = addTags 0 (liftAll defs) let ctxtIn = addAlist tagged emptyContext let defuns = defunctionalise nexttag ctxtIn putStrLn $ showSep "\n" (map show (toAlist defuns)) let checked = checkDefs defuns (toAlist defuns) -- print checked case checked of OK c -> codegenC c "a.out" True ["math.h"] "" "" TRACE Error e -> fail $ show e parseFOVM :: FilePath -> IO [(Name, LDecl)] parseFOVM fname = do -- putStrLn $ "Reading " ++ fname fp <- readFile fname case runParser pProgram () fname fp of Left err-> fail (show err) Right x -> return x pProgram :: LParser [(Name, LDecl)] pProgram = do fs <- many1 pLDecl eof return fs pLDecl :: LParser (Name, LDecl) pLDecl = do reserved "data" n <- iName [] ar <- natural return (n, LConstructor n (-1) (fromInteger ar)) <|> do reserved "fun" n <- iName [] lchar '(' args <- sepBy (iName []) (lchar ',') lchar ')' lchar '=' def <- pLExp return (n, LFun n args def) pLExp = buildExpressionParser optable pLExp' optable = [[binary "*" (\x y -> LOp LTimes [x,y]) AssocLeft, binary "/" (\x y -> LOp LDiv [x,y]) AssocLeft, binary "*." (\x y -> LOp LFTimes [x,y]) AssocLeft, binary "/." (\x y -> LOp LFDiv [x,y]) AssocLeft, binary "*:" (\x y -> LOp LBTimes [x,y]) AssocLeft, binary "/:" (\x y -> LOp LBDiv [x,y]) AssocLeft ], [ binary "+" (\x y -> LOp LPlus [x,y]) AssocLeft, binary "-" (\x y -> LOp LMinus [x,y]) AssocLeft, binary "++" (\x y -> LOp LStrConcat [x,y]) AssocLeft, binary "+." (\x y -> LOp LFPlus [x,y]) AssocLeft, binary "-." (\x y -> LOp LFMinus [x,y]) AssocLeft, binary "+:" (\x y -> LOp LBPlus [x,y]) AssocLeft, binary "-:" (\x y -> LOp LBMinus [x,y]) AssocLeft ], [ binary "==" (\x y -> LOp LEq [x, y]) AssocNone, binary "==." (\x y -> LOp LFEq [x, y]) AssocNone, binary "<" (\x y -> LOp LLt [x, y]) AssocNone, binary "<." (\x y -> LOp LFLt [x, y]) AssocNone, binary ">" (\x y -> LOp LGt [x, y]) AssocNone, binary ">." (\x y -> LOp LFGt [x, y]) AssocNone, binary "<=" (\x y -> LOp LLe [x, y]) AssocNone, binary "<=." (\x y -> LOp LFLe [x, y]) AssocNone, binary ">=" (\x y -> LOp LGe [x, y]) AssocNone, binary ">=." (\x y -> LOp LFGe [x, y]) AssocNone, binary "==:" (\x y -> LOp LBEq [x, y]) AssocNone, binary "<:" (\x y -> LOp LBLt [x, y]) AssocNone, binary ">:" (\x y -> LOp LBGt [x, y]) AssocNone, binary "<=:" (\x y -> LOp LBLe [x, y]) AssocNone, binary ">=:" (\x y -> LOp LBGe [x, y]) AssocNone ]] binary name f assoc = Infix (do reservedOp name; return f) assoc pLExp' :: LParser LExp pLExp' = try (do lchar '%'; pCast) <|> try (do lchar '%'; pPrim) <|> try (do tc <- option False (do lchar '%'; reserved "tc"; return True) x <- iName []; lazy <- option False (do lchar '@'; return True) lchar '(' args <- sepBy pLExp (lchar ',') lchar ')' if null args then if lazy then return (LLazyApp x []) else return (LV (Glob x)) else if lazy then return (LLazyApp x args) else return (LApp tc (LV (Glob x)) args)) <|> do lchar '('; e <- pLExp; lchar ')'; return e <|> pLConst <|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp reserved "in"; e <- pLExp return (LLet x v e) <|> do lchar '\\'; xs <- sepBy (iName []) (lchar ',') symbol "=>" e <- pLExp return (LLam xs e) <|> do reserved "foreign"; l <- pLang; t <- pType fname <- strlit lchar '(' fargs <- sepBy (do t' <- pType; e <- pLExp; return (t', e)) (lchar ',') lchar ')' return (LForeign l t fname fargs) <|> pCase <|> do x <- iName [] return (LV (Glob x)) pLang = do reserved "C"; return LANG_C pType = do reserved "Int"; return FInt <|> do reserved "Float"; return FDouble <|> do reserved "String"; return FString <|> do reserved "Unit"; return FUnit <|> do reserved "Ptr"; return FPtr <|> do reserved "Any"; return FAny pCase :: LParser LExp pCase = do reserved "case"; e <- pLExp; reserved "of" lchar '{' alts <- sepBy1 pAlt (lchar '|') lchar '}' return (LCase e alts) pCast :: LParser LExp pCast = do reserved "FloatString"; lchar '('; e <- pLExp; lchar ')' return (LOp LFloatStr [e]) <|> do reserved "StringFloat"; lchar '('; e <- pLExp; lchar ')' return (LOp LStrFloat [e]) <|> do reserved "FloatInt"; lchar '('; e <- pLExp; lchar ')' return (LOp LFloatInt [e]) <|> do reserved "IntFloat"; lchar '('; e <- pLExp; lchar ')' return (LOp LIntFloat [e]) <|> do reserved "StringInt"; lchar '('; e <- pLExp; lchar ')' return (LOp LStrInt [e]) <|> do reserved "IntString"; lchar '('; e <- pLExp; lchar ')' return (LOp LIntStr [e]) <|> do reserved "BigInt"; lchar '('; e <- pLExp; lchar ')' return (LOp LBigInt [e]) <|> do reserved "IntBig"; lchar '('; e <- pLExp; lchar ')' return (LOp LIntBig [e]) <|> do reserved "BigString"; lchar '('; e <- pLExp; lchar ')' return (LOp LBigStr [e]) <|> do reserved "StringBig"; lchar '('; e <- pLExp; lchar ')' return (LOp LStrBig [e]) pPrim :: LParser LExp pPrim = do reserved "StrEq"; lchar '('; e <- pLExp; lchar ','; e' <- pLExp; lchar ')'; return (LOp LStrEq [e, e']) <|> do reserved "StrLt"; lchar '(' e <- pLExp; lchar ','; e' <- pLExp; lchar ')' return (LOp LStrLt [e, e']) <|> do reserved "StrLen"; lchar '('; e <- pLExp; lchar ')'; return (LOp LStrLen [e]) <|> do reserved "ReadString"; lchar '('; e <- pLExp; lchar ')'; return (LOp LReadStr [e]) <|> do reserved "WriteString"; lchar '('; e <- pLExp; lchar ')' return (LOp LPrintStr [e]) <|> do reserved "WriteInt"; lchar '('; e <- pLExp; lchar ')'; return (LOp LPrintNum [e]) <|> do reserved "lazy"; lchar '('; e <- pLExp; lchar ')'; return (LLazyExp e) <|> do reserved "StrHead"; lchar '('; e <- pLExp; lchar ')'; return (LOp LStrHead [e]) <|> do reserved "StrTail"; lchar '('; e <- pLExp; lchar ')'; return (LOp LStrTail [e]) <|> do reserved "StrRev"; lchar '('; e <- pLExp; lchar ')'; return (LOp LStrRev [e]) <|> do reserved "StrCons"; lchar '('; x <- pLExp; lchar ','; xs <- pLExp; lchar ')'; return (LOp LStrCons [x, xs]) <|> do reserved "StrIndex"; lchar '('; x <- pLExp; lchar ','; i <- pLExp; lchar ')'; return (LOp LStrIndex [x, i]) pAlt :: LParser LAlt pAlt = try (do x <- iName [] lchar '('; args <- sepBy1 (iName []) (lchar ','); lchar ')' symbol "=>" rhs <- pLExp return (LConCase (-1) x args rhs)) <|> do x <- iName []; symbol "=>" rhs <- pLExp return (LConCase (-1) x [] rhs) <|> do c <- natural symbol "=>" rhs <- pLExp return (LConstCase (I (fromInteger c)) rhs) <|> do symbol "_" symbol "=>" rhs <- pLExp return (LDefaultCase rhs) pLConst :: LParser LExp pLConst = try (do f <- float; return $ LConst (Fl f)) <|> try (do i <- natural; lchar ':'; return $ LConst (BI i)) <|> try (do i <- natural; return $ LConst (I (fromInteger i))) <|> try (do s <- strlit; return $ LConst (Str s)) <|> try (do c <- chlit; return $ LConst (Ch c))