Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

258 lines (232 sloc) 9.646 kb
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))
Jump to Line
Something went wrong with that request. Please try again.