git.iko.soy/Idris-dev
on 7ea4422 help sign in
Idris-dev/src/Core/CoreParser.hs
137 lines 4.5 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 opStart = iOpStart,
18 opLetter = iOpLetter,
19 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>"],
20 reservedNames = ["let", "in", "data", "Set", "if", "then", "else",
21 "do", "dsl", "import",
22 "infix", "infixl", "infixr", "prefix",
23 "where", "forall", "syntax",
24 "using", "params", "namespace",
25 "Int", "Float", "Char", "String", "Ptr"]
26 }
28iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"
29iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
30 <|> letter
32lexer :: TokenParser a
33lexer = PTok.makeTokenParser idrisDef
35whiteSpace= PTok.whiteSpace lexer
36lexeme = PTok.lexeme lexer
37symbol = PTok.symbol lexer
38natural = PTok.natural lexer
39parens = PTok.parens lexer
40semi = PTok.semi lexer
41comma = PTok.comma lexer
42identifier= PTok.identifier lexer
43reserved = PTok.reserved lexer
44operator = PTok.operator lexer
45reservedOp= PTok.reservedOp lexer
46lchar = lexeme.char
48type CParser a = GenParser Char a
50parseFile = runParser pTestFile () "(input)"
51parseDef = runParser pDef () "(input)"
52parseTerm = runParser pTerm () "(input)"
54pTestFile :: CParser a RProgram
55pTestFile = do p <- many1 pDef ; eof
56 return p
58iName :: CParser a Name
59iName = do x <- identifier
60 return (UN [x])
62pDef :: CParser a (Name, RDef)
63pDef = try (do x <- iName; lchar ':'; ty <- pTerm
64 lchar '='
65 tm <- pTerm
66 lchar ';'
67 return (x, RFunction (RawFun ty tm)))
68 <|> do x <- iName; lchar ':'; ty <- pTerm; lchar ';'
69 return (x, RConst ty)
70 <|> do (x, d) <- pData; lchar ';'
71 return (x, RData d)
73app :: CParser a (Raw -> Raw -> Raw)
74app = do whiteSpace ; return RApp
76arrow :: CParser a (Raw -> Raw -> Raw)
77arrow = do symbol "->" ; return $ \s t -> RBind (MN 0 "X") (Pi s) t
79pTerm :: CParser a Raw
80pTerm = try (do chainl1 pNoApp app)
81 <|> pNoApp
83pNoApp :: CParser a Raw
84pNoApp = try (chainr1 pExp arrow)
85 <|> pExp
86pExp :: CParser a Raw
87pExp = do lchar '\\'; x <- iName; lchar ':'; ty <- pTerm
88 symbol "=>";
89 sc <- pTerm
90 return (RBind x (Lam ty) sc)
91 <|> try (do lchar '?'; x <- iName; lchar ':'; ty <- pTerm
92 lchar '.';
93 sc <- pTerm
94 return (RBind x (Hole ty) sc))
95 <|> try (do lchar '(';
96 x <- iName; lchar ':'; ty <- pTerm
97 lchar ')';
98 symbol "->";
99 sc <- pTerm
100 return (RBind x (Pi ty) sc))
101 <|> try (do lchar '(';
102 t <- pTerm
103 lchar ')'
104 return t)
105 <|> try (do symbol "??";
106 x <- iName; lchar ':'; ty <- pTerm
107 lchar '=';
108 val <- pTerm
109 sc <- pTerm
110 return (RBind x (Guess ty val) sc))
111 <|> try (do reserved "let";
112 x <- iName; lchar ':'; ty <- pTerm
113 lchar '=';
114 val <- pTerm
115 reserved "in";
116 sc <- pTerm
117 return (RBind x (Let ty val) sc))
118 <|> try (do lchar '_';
119 x <- iName; lchar ':'; ty <- pTerm
120 lchar '.';
121 sc <- pTerm
122 return (RBind x (PVar ty) sc))
123 <|> try (do reserved "Set"; i <- option 0 natural
124 return (RSet (fromInteger i)))
125 <|> try (do x <- iName
126 return (Var x))
128pData :: CParser a (Name, RawDatatype)
129pData = do reserved "data"; x <- iName; lchar ':'; ty <- pTerm; reserved "where"
130 cs <- many pConstructor
131 return (x, RDatatype x ty cs)
133pConstructor :: CParser a (Name, Raw)
134pConstructor = do lchar '|'
135 c <- iName; lchar ':'; ty <- pTerm
136 return (c, ty)