git.iko.soy/Idris-dev
on 019faba help sign in
Idris-dev/src/Idris/Parser.hs
236 lines 7.3 kB history raw
1module Idris.Parser where
3import Idris.AbsSyntax
5import Core.CoreParser
6import Core.TT
8import Text.ParserCombinators.Parsec
9import Text.ParserCombinators.Parsec.Expr
10import Text.ParserCombinators.Parsec.Language
11import qualified Text.ParserCombinators.Parsec.Token as PTok
13import Data.List
14import Control.Monad.State
15import Debug.Trace
17type TokenParser a = PTok.TokenParser a
19type IParser = GenParser Char IState
21lexer :: TokenParser IState
22lexer = PTok.makeTokenParser idrisDef
24whiteSpace= PTok.whiteSpace lexer
25lexeme = PTok.lexeme lexer
26symbol = PTok.symbol lexer
27natural = PTok.natural lexer
28parens = PTok.parens lexer
29semi = PTok.semi lexer
30comma = PTok.comma lexer
31identifier= PTok.identifier lexer
32reserved = PTok.reserved lexer
33operator = PTok.operator lexer
34reservedOp= PTok.reservedOp lexer
35lchar = lexeme.char
37parseExpr i = runParser pFullExpr i "(input)"
39parseProg :: String -> Idris [PDecl]
40parseProg fname = do file <- lift $ readFile fname
41 i <- get
42 case (runParser (do ps <- many1 pDecl
43 eof
44 i' <- getState
45 return (ps, i')) i fname file) of
46 Left err -> fail (show err)
47 Right (x, i) -> do put i
48 return (collect x)
50-- Collect PClauses with the same function name
51collect :: [PDecl] -> [PDecl]
52collect (PClauses _ [c@(PClause n l r)] : ds) = clauses n [c] ds
53 where clauses n acc (PClauses _ [c@(PClause n' l r)] : ds)
54 | n == n' = clauses n (c : acc) ds
55 clauses n acc xs = PClauses n (reverse acc) : collect xs
56collect (d : ds) = d : collect ds
57collect [] = []
59pFullExpr :: IParser PTerm
60pFullExpr = do x <- pExpr; eof;
61 i <- getState
62 return (addImpl i x)
64pDecl :: IParser PDecl
65pDecl = do d <- pDecl'
66 lchar ';'
67 i <- getState
68 return (fmap (addImpl i) d)
70--------- Top Level Declarations ---------
72pDecl' :: IParser PDecl
73pDecl' = try pFixity
74 <|> try (do n <- pfName; ty <- pTSig
75 ty' <- implicit n ty
76 return (PTy n ty'))
77 <|> try pData
78 <|> try pPattern
80--------- Fixity ---------
82pFixity :: IParser PDecl
83pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
84 let prec = fromInteger i
85 istate <- getState
86 let fs = map (Fix (f prec)) ops
87 setState (istate {
88 idris_infixes = sort (fs ++ idris_infixes istate) })
89 return (PFix (f prec) ops)
91fixity :: IParser (Int -> Fixity)
92fixity = try (do reserved "infixl"; return Infixl)
93 <|> try (do reserved "infixr"; return Infixr)
94 <|> try (do reserved "infix"; return InfixN)
96--------- Expressions ---------
98pExpr = do i <- getState
99 buildExpressionParser (table (idris_infixes i)) pExpr'
101pExpr' :: IParser PTerm
102pExpr' = try pApp
103 <|> pSimpleExpr
104 <|> try pLambda
105 <|> try pPi
107pfName = try iName
108 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])
110pSimpleExpr =
111 try (do symbol "!["; t <- pTerm; lchar ']'
112 return $ PQuote t)
113 <|> try (do x <- pfName; return (PRef x))
114 <|> try (do lchar '_'; return Placeholder)
115 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
116 <|> try (do reserved "Set"; return PSet)
118pHSimpleExpr = try pSimpleExpr
119 <|> do lchar '.'
120 e <- pSimpleExpr
121 return $ PHidden e
123pApp = do f <- pSimpleExpr
124 iargs <- many pImplicitArg
125 args <- many1 pSimpleExpr
126 return (PApp f iargs args)
128pImplicitArg = do lchar '{'; n <- iName
129 v <- option (PRef n) (do lchar '='; pExpr)
130 lchar '}'
131 return (n, v)
133pTSig = do lchar ':'
134 pExpr
136pLambda = do lchar '\\'; x <- iName; t <- option Placeholder pTSig
137 symbol "=>"
138 sc <- pExpr
139 return (PLam x t sc)
141pPi = do lchar '('; x <- iName; t <- pTSig; lchar ')'
142 symbol "->"
143 sc <- pExpr
144 return (PPi Exp x t sc)
145 <|> do lchar '{'; x <- iName; t <- pTSig; lchar '}'
146 symbol "->"
147 sc <- pExpr
148 return (PPi Imp x t sc)
150table fixes
151 = toTable (reverse fixes) ++
152 [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],
153 [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]
155toTable fs = map (map toBin)
156 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
157 where toBin (Fix f op) = binary op
158 (\x y -> PApp (PRef (UN [op])) [] [x,y]) (assoc f)
159 assoc (Infixl _) = AssocLeft
160 assoc (Infixr _) = AssocRight
161 assoc (InfixN _) = AssocNone
163binary name f assoc = Infix (do { reservedOp name; return f }) assoc
165--------- Data declarations ---------
167pData :: IParser PDecl
168pData = try (do reserved "data"; tyn <- pfName; ty <- pTSig
169 reserved "where"
170 ty' <- implicit tyn ty
171 cons <- sepBy1 pConstructor (lchar '|')
172 return $ PData (PDatadecl tyn ty' cons))
173 <|> do reserved "data"; tyn <- pfName; args <- many iName
174 lchar '='
175 cons <- sepBy1 pSimpleCon (lchar '|')
176 let conty = mkPApp (PRef tyn) (map PRef args)
177 let ty = bindArgs (map (\a -> PSet) args) PSet
178 ty' <- implicit tyn ty
179 cons' <- mapM (\ (x, cargs) -> do let cty = bindArgs cargs conty
180 cty' <- implicit x cty
181 return (x, cty')) cons
182 return $ PData (PDatadecl tyn ty' cons')
184mkPApp t [] = t
185mkPApp t xs = PApp t [] xs
187bindArgs :: [PTerm] -> PTerm -> PTerm
188bindArgs [] t = t
189bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)
191pConstructor :: IParser (Name, PTerm)
192pConstructor
193 = do cn <- pfName; ty <- pTSig
194 ty' <- implicit cn ty
195 return (cn, ty')
197pSimpleCon :: IParser (Name, [PTerm])
198pSimpleCon = do cn <- pfName
199 args <- many pSimpleExpr
200 return (cn, args)
202--------- Pattern match clauses ---------
204pPattern :: IParser PDecl
205pPattern = do clause <- pClause
206 return (PClauses (MN 0 "_") [clause]) -- collect together later
208pClause :: IParser PClause
209pClause = try (do n <- pfName
210 iargs <- many pImplicitArg
211 args <- many pHSimpleExpr
212 lchar '='
213 rhs <- pExpr
214 return $ PClause n (PApp (PRef n) iargs args) rhs)
215 <|> do l <- pSimpleExpr
216 op <- operator
217 let n = UN [op]
218 r <- pSimpleExpr
219 lchar '='
220 rhs <- pExpr
221 return $ PClause n (PApp (PRef n) [] [l,r]) rhs
223-- Dealing with implicit arguments
225implicit :: Name -> PTerm -> IParser PTerm
226implicit n ptm
227 = do i <- getState
228 let (tm', name_arity) = implicitise i ptm
229 setState (i { idris_implicits = addDef n name_arity (idris_implicits i) })
230 return tm'
232addImplicits :: PTerm -> IParser PTerm
233addImplicits tm
234 = do i <- getState
235 return (addImpl i tm)