@@ -17,14 +17,6 @@ import Debug.Trace
1717
1818type TokenParser a = PTok.TokenParser a
1919
20−idrisDef = haskellDef {
21− reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>"],
22− reservedNames = ["let", "in", "data", "Set", "if", "then", "else",
23− "do", "dsl", "import", "infix", "infixl", "infixr",
24− "where", "forall", "syntax",
25− "using", "params", "namespace"]
26− }
27−
2820type IParser = Parsec String IState
2921
3022lexer :: TokenParser IState
@@ -61,22 +53,32 @@ pFullExpr = do x <- pExpr; eof; return x
6153pDecl :: IParser PDecl
6254pDecl = do d <- pDecl'; lchar ';'; return d
6355
56+--------- Top Level Declarations ---------
57+
6458pDecl' :: IParser PDecl
65−pDecl' = try (do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
66− let prec = fromInteger i
67− istate <- getState
68− let fs = map (Fix (f prec)) ops
69− setState (istate {
70− idris_infixes = sort (fs ++ idris_infixes istate) })
71− return (PFix (f prec) ops))
72− <|> try (do n <- iName; ty <- pTSig
59+pDecl' = try pFixity
60+ <|> try (do n <- pfName; ty <- pTSig
7361 return (PTy n ty))
62+ <|> try pData
63+
64+-------- Fixity --------
65+
66+pFixity :: IParser PDecl
67+pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
68+ let prec = fromInteger i
69+ istate <- getState
70+ let fs = map (Fix (f prec)) ops
71+ setState (istate {
72+ idris_infixes = sort (fs ++ idris_infixes istate) })
73+ return (PFix (f prec) ops)
7474
7575fixity :: IParser (Int -> Fixity)
7676fixity = try (do reserved "infixl"; return Infixl)
7777 <|> try (do reserved "infixr"; return Infixr)
7878 <|> try (do reserved "infix"; return InfixN)
7979
80+--------- Expressions ---------
81+
8082pExpr = do i <- getState
8183 buildExpressionParser (table (idris_infixes i)) pExpr'
8284
@@ -86,13 +88,16 @@ pExpr' = try pApp
8688 <|> try pLambda
8789 <|> try pPi
8890
91+pfName = try iName
92+ <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])
93+
8994pSimpleExpr =
9095 try (do symbol "!["; t <- pTerm; lchar ']'
9196 return $ PQuote t)
92− <|> try (do x <- iName; return (PRef x))
97+ <|> try (do x <- pfName; return (PRef x))
9398 <|> try (do lchar '_'; return Placeholder)
94− <|> try (do lchar '('; o <- operator; lchar ')'; return (PRef (UN [o])))
9599 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
100+ <|> try (do reserved "Set"; return PSet)
96101
97102pApp = do f <- pSimpleExpr
98103 args <- many1 pSimpleExpr
@@ -130,3 +135,37 @@ toTable fs = map (map toBin)
130135
131136binary name f assoc = Infix (do { reservedOp name; return f }) assoc
132137
138+--------- Data declarations ---------
139+
140+pData :: IParser PDecl
141+pData = try (do reserved "data"; tyn <- pfName; ty <- pTSig
142+ reserved "where"
143+ cons <- sepBy1 pConstructor (lchar '|')
144+ return $ PData (PDatadecl tyn ty cons))
145+ <|> do reserved "data"; tyn <- pfName; args <- many iName
146+ lchar '='
147+ cons <- sepBy1 pSimpleCon (lchar '|')
148+ let conty = mkPApp (PRef tyn) (map PRef args)
149+ return $ PData (PDatadecl tyn (bindArgs (map (\a -> PSet) args) PSet)
150+ (map (\ (x, cargs) ->
151+ (x, bindArgs cargs conty)) cons))
152+
153+mkPApp t [] = t
154+mkPApp t xs = PApp t [] xs
155+
156+bindArgs :: [PTerm] -> PTerm -> PTerm
157+bindArgs [] t = t
158+bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)
159+
160+pConstructor :: IParser (Name, PTerm)
161+pConstructor
162+ = do cn <- pfName; ty <- pTSig
163+ return (cn, ty)
164+
165+pSimpleCon :: IParser (Name, [PTerm])
166+pSimpleCon = do cn <- pfName
167+ args <- many pSimpleExpr
168+ return (cn, args)
169+
170+--------- Pattern match clauses ---------
171+