git.iko.soy/Idris-dev
on master help sign in
Parsing high level data declarations
64b7cfdEdwin Brady
decls.minew file+25
compare with master
unifiedsplit
@@ -0,0 +1,25 @@
1+infixl 5 +, - ;
2+infixl 6 *, / ;
3+
4+infixl 7 :: ;
5+
6+data Nat = O | S Nat;
7+data List a = Nil | Cons a (List a);
8+
9+data Vect : Set -> Nat -> Set where
10+ VNil : Vect a O
11+ | (::) : a -> Vect a k -> Vect a (S k);
12+
13+plus : Nat -> Nat -> Nat;
14+{-
15+plus O y = y;
16+plus (S k) y = S (plus k y);
17+-}
18+
19+app : Vect a n -> Vect a m -> Vect a (plus n m);
20+{-
21+app VNil ys = ys;
22+app (x :: xs) ys = x :: (app xs ys);
23+-}
24+
25+(::) : a -> Vect a k -> Vect a (S k);
src/Core/CoreParser.hs+10−2
@@ -1,6 +1,6 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName) where
3+module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef) where
4
4
5import Core.TT
5import Core.TT
6
6
@@ -14,8 +14,16 @@ import Debug.Trace
14
14
15type TokenParser a = PTok.TokenParser a
15type TokenParser a = PTok.TokenParser a
16
16
17+idrisDef = haskellDef {
18+ reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>"],
19+ reservedNames = ["let", "in", "data", "Set", "if", "then", "else",
20+ "do", "dsl", "import", "infix", "infixl", "infixr",
21+ "where", "forall", "syntax",
22+ "using", "params", "namespace"]
23+ }
24+
17lexer :: TokenParser a
25lexer :: TokenParser a
18−lexer = PTok.makeTokenParser haskellDef
26+lexer = PTok.makeTokenParser idrisDef
19
27
20whiteSpace= PTok.whiteSpace lexer
28whiteSpace= PTok.whiteSpace lexer
21lexeme = PTok.lexeme lexer
29lexeme = PTok.lexeme lexer
src/Idris/AbsSyntax.hs+6
@@ -11,6 +11,11 @@ import Data.List
11data IOption = Logging
11data IOption = Logging
12 deriving (Show, Eq)
12 deriving (Show, Eq)
13
13
14+-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
15+-- without typechecking).
16+-- This will include all the functions and data declarations, plus fixity declarations
17+-- and syntax macros.
18+
14data IState = IState { tt_ctxt :: Context,
19data IState = IState { tt_ctxt :: Context,
15 idris_infixes :: [FixDecl],
20 idris_infixes :: [FixDecl],
16 idris_implicits :: Ctxt [Name],
21 idris_implicits :: Ctxt [Name],
@@ -77,6 +82,7 @@ data PTerm = PQuote Raw
77 | PLam Name PTerm PTerm
82 | PLam Name PTerm PTerm
78 | PPi Plicity Name PTerm PTerm
83 | PPi Plicity Name PTerm PTerm
79 | PApp PTerm [(Name, PTerm)] [PTerm]
84 | PApp PTerm [(Name, PTerm)] [PTerm]
85+ | PSet
80 | Placeholder
86 | Placeholder
81 deriving Show
87 deriving Show
82
88
src/Idris/Parser.hs+57−18
@@ -17,14 +17,6 @@ import Debug.Trace
17
17
18type TokenParser a = PTok.TokenParser a
18type TokenParser a = PTok.TokenParser a
19
19
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−
28type IParser = Parsec String IState
20type IParser = Parsec String IState
29
21
30lexer :: TokenParser IState
22lexer :: TokenParser IState
@@ -61,22 +53,32 @@ pFullExpr = do x <- pExpr; eof; return x
61pDecl :: IParser PDecl
53pDecl :: IParser PDecl
62pDecl = do d <- pDecl'; lchar ';'; return d
54pDecl = do d <- pDecl'; lchar ';'; return d
63
55
56+--------- Top Level Declarations ---------
57+
64pDecl' :: IParser PDecl
58pDecl' :: IParser PDecl
65−pDecl' = try (do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
59+pDecl' = try pFixity
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
60+ <|> try (do n <- pfName; ty <- pTSig
73 return (PTy n ty))
61 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)
74
74
75fixity :: IParser (Int -> Fixity)
75fixity :: IParser (Int -> Fixity)
76fixity = try (do reserved "infixl"; return Infixl)
76fixity = try (do reserved "infixl"; return Infixl)
77 <|> try (do reserved "infixr"; return Infixr)
77 <|> try (do reserved "infixr"; return Infixr)
78 <|> try (do reserved "infix"; return InfixN)
78 <|> try (do reserved "infix"; return InfixN)
79
79
80+--------- Expressions ---------
81+
80pExpr = do i <- getState
82pExpr = do i <- getState
81 buildExpressionParser (table (idris_infixes i)) pExpr'
83 buildExpressionParser (table (idris_infixes i)) pExpr'
82
84
@@ -86,13 +88,16 @@ pExpr' = try pApp
86 <|> try pLambda
88 <|> try pLambda
87 <|> try pPi
89 <|> try pPi
88
90
91+pfName = try iName
92+ <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])
93+
89pSimpleExpr =
94pSimpleExpr =
90 try (do symbol "!["; t <- pTerm; lchar ']'
95 try (do symbol "!["; t <- pTerm; lchar ']'
91 return $ PQuote t)
96 return $ PQuote t)
92− <|> try (do x <- iName; return (PRef x))
97+ <|> try (do x <- pfName; return (PRef x))
93 <|> try (do lchar '_'; return Placeholder)
98 <|> try (do lchar '_'; return Placeholder)
94− <|> try (do lchar '('; o <- operator; lchar ')'; return (PRef (UN [o])))
95 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
99 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
100+ <|> try (do reserved "Set"; return PSet)
96
101
97pApp = do f <- pSimpleExpr
102pApp = do f <- pSimpleExpr
98 args <- many1 pSimpleExpr
103 args <- many1 pSimpleExpr
@@ -130,3 +135,37 @@ toTable fs = map (map toBin)
130
135
131binary name f assoc = Infix (do { reservedOp name; return f }) assoc
136binary name f assoc = Infix (do { reservedOp name; return f }) assoc
132
137
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+