git.iko.soy/Idris-dev
on 2050102 help sign in
Idris-dev/src/Core/CoreParser.hs
129 lines 4.2 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef) where
5import Core.TT
7import Text.ParserCombinators.Parsec
8import Text.ParserCombinators.Parsec.Expr
9import Text.ParserCombinators.Parsec.Language
10import qualified Text.ParserCombinators.Parsec.Token as PTok
12import Debug.Trace
14type TokenParser a = PTok.TokenParser a
16idrisDef = haskellDef {
17 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>"],
18 reservedNames = ["let", "in", "data", "Set", "if", "then", "else",
19 "do", "dsl", "import", "infix", "infixl", "infixr",
20 "where", "forall", "syntax",
21 "using", "params", "namespace"]
22 }
24lexer :: TokenParser a
25lexer = PTok.makeTokenParser idrisDef
27whiteSpace= PTok.whiteSpace lexer
28lexeme = PTok.lexeme lexer
29symbol = PTok.symbol lexer
30natural = PTok.natural lexer
31parens = PTok.parens lexer
32semi = PTok.semi lexer
33comma = PTok.comma lexer
34identifier= PTok.identifier lexer
35reserved = PTok.reserved lexer
36operator = PTok.operator lexer
37reservedOp= PTok.reservedOp lexer
38lchar = lexeme.char
40type CParser a = GenParser Char a
42parseFile = runParser pTestFile () "(input)"
43parseDef = runParser pDef () "(input)"
44parseTerm = runParser pTerm () "(input)"
46pTestFile :: CParser a RProgram
47pTestFile = do p <- many1 pDef ; eof
48 return p
50iName :: CParser a Name
51iName = do x <- identifier
52 return (UN [x])
54pDef :: CParser a (Name, RDef)
55pDef = try (do x <- iName; lchar ':'; ty <- pTerm
56 lchar '='
57 tm <- pTerm
58 lchar ';'
59 return (x, RFunction (RawFun ty tm)))
60 <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'
61 return (x, RConst ty)
62 <|> do (x, d) <- pData; lchar ';'
63 return (x, RData d)
65app :: CParser a (Raw -> Raw -> Raw)
66app = do whiteSpace ; return RApp
68arrow :: CParser a (Raw -> Raw -> Raw)
69arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
71pTerm :: CParser a Raw
72pTerm = try (do chainl1 pNoApp app)
73 <|> pNoApp
75pNoApp :: CParser a Raw
76pNoApp = try (chainr1 pExp arrow)
77 <|> pExp
78pExp :: CParser a Raw
79pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
80 symbol "=>";
81 sc <- pTerm
82 return (RBind x (Lam ty) sc)
83 <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm
84 lchar '.';
85 sc <- pTerm
86 return (RBind x (Hole ty) sc))
87 <|> try (do lchar '(';
88 x <- iName; lchar ':'; ty <- pTerm
89 lchar ')';
90 symbol "->";
91 sc <- pTerm
92 return (RBind x (Pi ty) sc))
93 <|> try (do lchar '(';
94 t <- pTerm
95 lchar ')'
96 return t)
97 <|> try (do symbol "??";
98 x <- iName; lchar ':'; ty <- pTerm
99 lchar '=';
100 val <- pTerm
101 sc <- pTerm
102 return (RBind x (Guess ty val) sc))
103 <|> try (do reserved "let";
104 x <- iName; lchar ':'; ty <- pTerm
105 lchar '=';
106 val <- pTerm
107 reserved "in";
108 sc <- pTerm
109 return (RBind x (Let ty val) sc))
110 <|> try (do lchar '_';
111 x <- iName; lchar ':'; ty <- pTerm
112 lchar '.';
113 sc <- pTerm
114 return (RBind x (PVar ty) sc))
115 <|> try (do reserved "Set"; i <- option 0 natural
116 return (RSet (fromInteger i)))
117 <|> try (do x <- iName
118 return (Var x))
120pData :: CParser a (Name, RawDatatype)
121pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"
122 cs <- many pConstructor
123 return (x, RDatatype x ty cs)
125pConstructor :: CParser a (Name, Raw)
126pConstructor = do lchar '|'
127 c <- iName; lchar ':'; ty <- pTerm
128 return (c, ty)