src/Idris/Parser.hs · Idris-dev

git.iko.soy/Idris-dev

on 7ea4422 help sign in

Idris-dev/src/Idris/Parser.hs

419 lines 15 kB history raw

1module Idris.Parser where

3import Idris.AbsSyntax

4import Idris.Imports

5import Paths_miniidris

6import Idris.ElabDecls

8import Core.CoreParser

9import Core.TT

11import Text.ParserCombinators.Parsec

12import Text.ParserCombinators.Parsec.Expr

13import Text.ParserCombinators.Parsec.Language

14import qualified Text.ParserCombinators.Parsec.Token as PTok

16import Data.List

17import Control.Monad.State

18import Debug.Trace

20type TokenParser a = PTok.TokenParser a

22type IParser = GenParser Char IState

24lexer :: TokenParser IState

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

38integer = PTok.integer lexer

39float = PTok.float lexer

40strlit = PTok.stringLiteral lexer

41chlit = PTok.charLiteral lexer

42lchar = lexeme.char

44-- Loading modules

46loadModule :: FilePath -> Idris ()

47loadModule f = do datadir <- lift $ getDataDir

48 fp <- lift $ findImport [".", datadir] f

49 i <- getIState

50 if (f `elem` imported i)

51 then iLOG $ "Already read " ++ f

52 else do putIState (i { imported = f : imported i })

53 case fp of

54 IDR fn -> loadSource fn

55 IBC fn -> error "Not implemented"

57loadSource :: FilePath -> Idris ()

58loadSource f = do iLOG ("Reading " ++ f)

59 file <- lift $ readFile f

60 (modules, rest, pos) <- parseImports f file

61 mapM_ loadModule modules

62 ds <- parseProg defaultSyntax f rest pos

63 logLvl 3 (dumpDecls ds)

64 i <- getIState

65 logLvl 3 (show (idris_infixes i))

66 -- Now add all the declarations to the context

67 mapM_ (elabDecl toplevel) ds

68 iLOG ("Finished " ++ f)

69 return ()

71parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

73parseImports :: FilePath -> String -> Idris ([String], String, SourcePos)

74parseImports fname input

75 = do i <- get

76 case (runParser (do ps <- many pImport

77 rest <- getInput

78 pos <- getPosition

79 return ((ps, rest, pos), i)) i fname input) of

80 Left err -> fail (show err)

81 Right (x, i) -> do put i

82 return x

84pImport :: IParser String

85pImport = do reserved "import"

86 f <- identifier

87 lchar ';'

88 return f

90parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]

91parseProg syn fname input pos

92 = do i <- get

93 case (runParser (do setPosition pos

94 whiteSpace

95 ps <- many1 (pDecl syn)

96 eof

97 i' <- getState

98 return (concat ps, i')) i fname input) of

99 Left err -> fail (show err)

100 Right (x, i) -> do put i

101 return (collect x)

102

103-- Collect PClauses with the same function name

104collect :: [PDecl] -> [PDecl]

105collect (c@(PClauses _ [PClause n l r w]) : ds) = clauses n [] (c:ds)

106 where clauses n acc (PClauses _ [PClause n' l r w] : ds)

107 | n == n' = clauses n (PClause n' l r (collect w) : acc) ds

108 clauses n acc xs = PClauses n (reverse acc) : collect xs

109collect (PParams ns ps : ds) = PParams ns (collect ps) : (collect ds)

110collect (d : ds) = d : collect ds

111collect [] = []

112

113pFullExpr :: SyntaxInfo -> IParser PTerm

114pFullExpr syn

115 = do x <- pExpr syn; eof;

116 i <- getState

117 return $ desugar syn i x

118

119pDecl :: SyntaxInfo -> IParser [PDecl]

120pDecl syn

121 = do d <- pDecl' syn

122 i <- getState

123 let d' = fmap (desugar syn i) d

124 return [d']

125 <|> try (pUsing syn)

126 <|> try (pParams syn)

127 <|> try (do reserved "import"

128 fp <- identifier

129 lchar ';'

130 fail "imports must be at the top of file")

131

132pFunDecl :: SyntaxInfo -> IParser [PDecl]

133pFunDecl syn

134 = try (do d <- pFunDecl' syn

135 i <- getState

136 let d' = fmap (desugar syn i) d

137 return [d'])

138

139--------- Top Level Declarations ---------

140

141pDecl' :: SyntaxInfo -> IParser PDecl

142pDecl' syn

143 = try pFixity

144 <|> pFunDecl' syn

145 <|> try (pData syn)

146

147pFunDecl' :: SyntaxInfo -> IParser PDecl

148pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

149 lchar ';'

150 ty' <- implicit syn n ty

151 return (PTy n ty'))

152 <|> try (pPattern syn)

153

154pUsing :: SyntaxInfo -> IParser [PDecl]

155pUsing syn =

156 do reserved "using";

157 lchar '('

158 ns <- tyDeclList syn

159 lchar ')'

160 lchar '{'

161 let uvars = using syn

162 ds <- many1 (pDecl (syn { using = uvars ++ ns }))

163 lchar '}'

164 return (concat ds)

165

166pParams :: SyntaxInfo -> IParser [PDecl]

167pParams syn =

168 do reserved "params";

169 lchar '('

170 ns <- tyDeclList syn

171 lchar ')'

172 lchar '{'

173 let pvars = syn_params syn

174 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })

175 lchar '}'

176 return [PParams ns (concat ds)]

177

178--------- Fixity ---------

179

180pFixity :: IParser PDecl

181pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

182 lchar ';'

183 let prec = fromInteger i

184 istate <- getState

185 let fs = map (Fix (f prec)) ops

186 setState (istate {

187 idris_infixes = sort (fs ++ idris_infixes istate) })

188 return (PFix (f prec) ops)

189

190fixity :: IParser (Int -> Fixity)

191fixity = try (do reserved "infixl"; return Infixl)

192 <|> try (do reserved "infixr"; return Infixr)

193 <|> try (do reserved "infix"; return InfixN)

194 <|> try (do reserved "prefix"; return PrefixN)

195

196--------- Expressions ---------

197

198pExpr syn = do i <- getState

199 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)

200

201pExpr' :: SyntaxInfo -> IParser PTerm

202pExpr' syn

203 = try (pApp syn)

204 <|> pSimpleExpr syn

205 <|> try (pLambda syn)

206 <|> try (pPi syn)

207 <|> try (pDoBlock syn)

208

209pfName = try iName

210 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

211

212pSimpleExpr syn =

213 try (do symbol "!["; t <- pTerm; lchar ']'

214 return $ PQuote t)

215 <|> try (do reserved "return"; return PReturn)

216 <|> try (do x <- pfName; return (PRef x))

217 <|> try (do lchar '('; l <- pExpr syn; lchar ','; r <- pExpr syn; lchar ')';

218 return (PPair l r))

219 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

220 <|> try (do c <- pConstant; return (PConstant c))

221 <|> try (do reserved "Set"; return PSet)

222 <|> try (do symbol "()"; return PTrue)

223 <|> try (do symbol "_|_"; return PFalse)

224 <|> try (do lchar '_'; return Placeholder)

225

226pHSimpleExpr syn

227 = try (pSimpleExpr syn)

228 <|> do lchar '.'

229 e <- pSimpleExpr syn

230 return $ PHidden e

231

232pApp syn = do f <- pSimpleExpr syn

233 args <- many1 (pArg syn)

234 return (PApp f args)

235

236pArg :: SyntaxInfo -> IParser PArg

237pArg syn = pImplicitArg syn

238 <|> do e <- pSimpleExpr syn

239 return (PExp e)

240

241pImplicitArg syn = do lchar '{'; n <- iName

242 v <- option (PRef n) (do lchar '='; pExpr syn)

243 lchar '}'

244 return (PImp n v)

245

246pTSig syn = do lchar ':'

247 pExpr syn

248

249pLambda syn = do lchar '\\';

250 xt <- tyOptDeclList syn

251 symbol "=>"

252 sc <- pExpr syn

253 return (bindList PLam xt sc)

254

255pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'

256 symbol "->"

257 sc <- pExpr syn

258 return (bindList (PPi Exp) xt sc)

259 <|> do lchar '{'; xt <- tyDeclList syn; lchar '}'

260 symbol "->"

261 sc <- pExpr syn

262 return (bindList (PPi Imp) xt sc)

263

264tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

265 (lchar ',')

266

267tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (pTSig syn)

268 return (x,t))

269 (lchar ',')

270

271bindList b [] sc = sc

272bindList b ((n, t):bs) sc = b n t (bindList b bs sc)

273

274pDoBlock syn

275 = do reserved "do"; lchar '{'

276 ds <- endBy1 (pDo syn) (lchar ';')

277 lchar '}'

278 return (PDoBlock ds)

279

280pDo syn

281 = try (do i <- iName; symbol "<-"; e <- pExpr syn;

282 return (DoBind i e))

283 <|> try (do reserved "let"; i <- iName; reservedOp "="; e <- pExpr syn

284 return (DoLet i e))

285 <|> try (do e <- pExpr syn; return (DoExp e))

286

287pConstant :: IParser Const

288pConstant = do reserved "Int"; return IType

289 <|> do reserved "Char"; return ChType

290 <|> do reserved "Float"; return FlType

291 <|> do reserved "String"; return StrType

292 <|> do reserved "Ptr"; return PtrType

293 <|> try (do f <- float; return $ Fl f)

294 <|> try (do i <- natural; return $ I (fromInteger i))

295 <|> try (do s <- strlit; return $ Str s)

296 <|> try (do c <- chlit; return $ Ch c)

297

298table fixes

299 = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]

300 ++ toTable (reverse fixes) ++

301 [[binary "=" (\x y -> PApp (PRef (UN ["="])) [PExp x,PExp y]) AssocLeft],

302 [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]

303

304toTable fs = map (map toBin)

305 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

306 where toBin (Fix (PrefixN _) op) = prefix op

307 (\x -> PApp (PRef (UN [op])) [PExp x])

308 toBin (Fix f op) = binary op

309 (\x y -> PApp (PRef (UN [op])) [PExp x,PExp y]) (assoc f)

310 assoc (Infixl _) = AssocLeft

311 assoc (Infixr _) = AssocRight

312 assoc (InfixN _) = AssocNone

313

314binary name f assoc = Infix (do { reservedOp name; return f }) assoc

315prefix name f = Prefix (do { reservedOp name; return f })

316

317--------- Data declarations ---------

318

319pData :: SyntaxInfo -> IParser PDecl

320pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn

321 reserved "where"

322 ty' <- implicit syn tyn ty

323 cons <- sepBy (pConstructor syn) (lchar '|')

324 lchar ';'

325 return $ PData (PDatadecl tyn ty' cons))

326 <|> do reserved "data"; tyn <- pfName; args <- many iName

327 lchar '='

328 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

329 lchar ';'

330 let conty = mkPApp (PRef tyn) (map PRef args)

331 let ty = bindArgs (map (\a -> PSet) args) PSet

332 ty' <- implicit syn tyn ty

333 cons' <- mapM (\ (x, cargs) -> do let cty = bindArgs cargs conty

334 cty' <- implicit syn x cty

335 return (x, cty')) cons

336 return $ PData (PDatadecl tyn ty' cons')

337

338mkPApp t [] = t

339mkPApp t xs = PApp t (map PExp xs)

340

341bindArgs :: [PTerm] -> PTerm -> PTerm

342bindArgs [] t = t

343bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)

344

345pConstructor :: SyntaxInfo -> IParser (Name, PTerm)

346pConstructor syn

347 = do cn <- pfName; ty <- pTSig syn

348 ty' <- implicit syn cn ty

349 return (cn, ty')

350

351pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm])

352pSimpleCon syn

353 = do cn <- pfName

354 args <- many (pSimpleExpr syn)

355 return (cn, args)

356

357--------- Pattern match clauses ---------

358

359pPattern :: SyntaxInfo -> IParser PDecl

360pPattern syn = do clause <- pClause syn

361 return (PClauses (MN 2 "_") [clause]) -- collect together later

362

363pClause :: SyntaxInfo -> IParser PClause

364pClause syn

365 = try (do n <- pfName

366 iargs <- many (pImplicitArg syn)

367 args <- many (pHSimpleExpr syn)

368 lchar '='

369 rhs <- pExpr syn

370 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

371 return $ PClause n (PApp (PRef n) (iargs ++ map PExp args)) rhs wheres)

372 <|> do l <- pSimpleExpr syn

373 op <- operator

374 let n = UN [op]

375 r <- pSimpleExpr syn

376 lchar '='

377 rhs <- pExpr syn

378 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

379 return $ PClause n (PApp (PRef n) [PExp l,PExp r]) rhs wheres

380

381pWhereblock :: SyntaxInfo -> IParser [PDecl]

382pWhereblock syn = do reserved "where"; lchar '{'

383 ds <- many1 $ pFunDecl syn;

384 lchar '}';

385 return $ concat ds

386

387-- Dealing with implicit arguments

388

389implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm

390implicit syn n ptm

391 = do i <- getState

392 let (tm', impdata) = implicitise syn i ptm

393 setState (i { idris_implicits = addDef n impdata (idris_implicits i) })

394 return tm'

395

396desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

397desugar syn i t = let t' = expandDo (dsl_info syn) t in

398 addImpl i t'

399

400expandDo :: DSL -> PTerm -> PTerm

401expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

402expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

403expandDo dsl (PApp t args) = PApp (expandDo dsl t)

404 (map (fmap (expandDo dsl)) args)

405expandDo dsl (PPair l r) = PPair (expandDo dsl l) (expandDo dsl r)

406expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

407expandDo dsl PReturn = PRef (dsl_return dsl)

408expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

409 where

410 block b [DoExp tm] = tm

411 block b [a] = PElabError "Last statement in do block must be an expression"

412 block b (DoBind n tm : rest)

413 = PApp (PRef b) [PExp tm, PExp (PLam n Placeholder (block b rest))]

414 block b (DoExp tm : rest)

415 = PApp (PRef b) [PExp tm, PExp (PLam (MN 0 "bindx") Placeholder (block b rest))]

416expandDo dsl t = t

417

418

419