4b1109e · Idris-dev · git.iko.soy

37lexer :: TokenParser IState

38lexer = PTok.makeTokenParser idrisDef

39

40−whiteSpace= PTok.whiteSpace lexer

40+whiteSpace = PTok.whiteSpace lexer

41−lexeme = PTok.lexeme lexer

41+lexeme = PTok.lexeme lexer

42−symbol = PTok.symbol lexer

42+symbol = PTok.symbol lexer

43−natural = PTok.natural lexer

43+natural = PTok.natural lexer

44−parens = PTok.parens lexer

44+parens = PTok.parens lexer

45−semi = PTok.semi lexer

45+semi = PTok.semi lexer

46−comma = PTok.comma lexer

46+comma = PTok.comma lexer

47−identifier= PTok.identifier lexer

47+identifier = PTok.identifier lexer

48−reserved = PTok.reserved lexer

48+reserved = PTok.reserved lexer

49−operator = PTok.operator lexer

49+operator = PTok.operator lexer

50−reservedOp= PTok.reservedOp lexer

50+reservedOp = PTok.reservedOp lexer

51−integer = PTok.integer lexer

51+integer = PTok.integer lexer

52−float = PTok.float lexer

52+float = PTok.float lexer

53−strlit = PTok.stringLiteral lexer

53+strlit = PTok.stringLiteral lexer

54−chlit = PTok.charLiteral lexer

54+chlit = PTok.charLiteral lexer

55−lchar = lexeme.char

55+lchar = lexeme.char

56

57-- Loading modules

58

62 ibcsd <- valIBCSubDir i

63 ids <- allImportDirs i

64 fp <- liftIO $ findImport ids ibcsd f

65− if (f `elem` imported i)

65+ if f `elem` imported i

66 then iLOG $ "Already read " ++ f

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

68 case fp of

91 putIState (i { default_access = Hidden })

92 mapM_ loadModule modules

93 clearIBC -- start a new .ibc file

94− mapM_ (\m -> addIBC (IBCImport m)) modules

94+ mapM_ (addIBC . IBCImport) modules

95 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })

96 f rest pos

97 let ds = namespaces mname ds'

126addHides xs = do i <- getIState

127 let defh = default_access i

128 let (hs, as) = partition isNothing xs

129− if null as then return ()

129+ unless (null as) $

130− else mapM_ doHide

130+ mapM_ doHide

131− (map (\ (n, _) -> (n, defh)) hs ++

131+ (map (\ (n, _) -> (n, defh)) hs ++

132− map (\ (n, Just a) -> (n, a)) as)

132+ map (\ (n, Just a) -> (n, a)) as)

133 where isNothing (_, Nothing) = True

134 isNothing _ = False

135

141 eof

142 return t) i "(proof)"

143

144+iShowError fname err = let ln = sourceLine (errorPos err)

145+ clm = sourceColumn (errorPos err)

146+ msg = map messageString (errorMessages err) in

147+ fname ++ ":" ++ show ln ++ ":parse error"

148+ ++ " at column " ++ show clm -- ++ " with error:\n\t" ++ show msg

149+

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

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

145parseImports fname input

151parseImports fname input

146 = do i <- get

152 = do i <- get

147− case (runParser (do whiteSpace

153+ case runParser (do whiteSpace

148− mname <- pHeader

154+ mname <- pHeader

149− ps <- many pImport

155+ ps <- many pImport

150− rest <- getInput

156+ rest <- getInput

151− pos <- getPosition

157+ pos <- getPosition

152− return ((mname, ps, rest, pos), i)) i fname input) of

158+ return ((mname, ps, rest, pos), i)) i fname input of

153− Left err -> fail (show err)

159+ Left err -> fail (iShowError fname err)

154− Right (x, i) -> do put i

160+ Right (x, i) -> do put i

155− return x

161+ return x

156− where ishow err = let ln = sourceLine (errorPos err) in

157− fname ++ ":" ++ show ln ++ ":parse error"

158−-- ++ show (map messageString (errorMessages err))

159

162

160pHeader :: IParser [String]

163pHeader :: IParser [String]

161pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')

164pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')

162 return (parseName i))

165 return (parseName i))

163 <|> return []

166 <|> return []

164 where parseName x = case span (/='.') x of

167 where parseName x = case span (/='.') x of

165− (x, "") -> [x]

168+ (x, "") -> [x]

166− (x, '.':y) -> x : parseName y

169+ (x, '.':y) -> x : parseName y

167

170

168−push_indent :: IParser ()

171+pushIndent :: IParser ()

169−push_indent = do pos <- getPosition

172+pushIndent = do pos <- getPosition

170− ist <- getState

173+ ist <- getState

171− setState (ist { indent_stack = sourceColumn pos :

174+ setState (ist { indent_stack = sourceColumn pos :

172 indent_stack ist })

175 indent_stack ist })

173

176

174−last_indent :: IParser Int

177+lastIndent :: IParser Int

175−last_indent = do ist <- getState

178+lastIndent = do ist <- getState

176− case indent_stack ist of

179+ case indent_stack ist of

177− (x : xs) -> return x

180+ (x : xs) -> return x

178− _ -> return 1

181+ _ -> return 1

179

182

180indent :: IParser Int

183indent :: IParser Int

181−indent = do pos <- getPosition

184+indent = liftM sourceColumn getPosition

182− return (sourceColumn pos)

183

185

184−pop_indent :: IParser ()

186+popIndent :: IParser ()

185−pop_indent = do ist <- getState

187+popIndent = do ist <- getState

186− let (x : xs) = indent_stack ist

188+ let (x : xs) = indent_stack ist

187− setState (ist { indent_stack = xs })

189+ setState (ist { indent_stack = xs })

188

190

189−open_block :: IParser ()

191+openBlock :: IParser ()

190−open_block = do lchar '{'

192+openBlock = do lchar '{'

191− ist <- getState

193+ ist <- getState

192− setState (ist { brace_stack = Nothing : brace_stack ist })

194+ setState (ist { brace_stack = Nothing : brace_stack ist })

193 <|> do ist <- getState

195 <|> do ist <- getState

194 lvl <- indent

196 lvl <- indent

195 setState (ist { brace_stack = Just lvl : brace_stack ist })

197 setState (ist { brace_stack = Just lvl : brace_stack ist })

196

198

197−close_block :: IParser ()

199+closeBlock :: IParser ()

198−close_block = do ist <- getState

200+closeBlock = do ist <- getState

199− bs <- case brace_stack ist of

201+ bs <- case brace_stack ist of

200− Nothing : xs -> do lchar '}'

202+ Nothing : xs -> do lchar '}'

201− return xs

203+ return xs

202− Just lvl : xs -> do i <- indent

204+ Just lvl : xs -> do i <- indent

203− inp <- getInput

205+ inp <- getInput

204-- trace (show (take 10 inp, i, lvl)) $

206-- trace (show (take 10 inp, i, lvl)) $

205− if (i >= lvl && take 1 inp /= ")")

207+ if i >= lvl && take 1 inp /= ")"

206− then fail "Not end of block"

208+ then fail "Not end of block"

207− else return xs

209+ else return xs

208− setState (ist { brace_stack = bs })

210+ setState (ist { brace_stack = bs })

209−

211+

210−pTerminator = do lchar ';'; pop_indent

212+pTerminator = do lchar ';'; popIndent

211− <|> do c <- indent; l <- last_indent

213+ <|> do c <- indent; l <- lastIndent

212− if (c <= l) then pop_indent

214+ if c <= l

215+ then popIndent

213− else fail "Not a terminator"

216+ else fail "Not a terminator"

214− <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent

217+ <|> do i <- getInput

218+ if "}" `isPrefixOf` i || ")" `isPrefixOf` i

219+ then popIndent

215− else fail "Not a terminator"

220+ else fail "Not a terminator"

216 <|> lookAhead eof

221 <|> lookAhead eof

217

222

218pBarTerminator

223pBarTerminator

219 = do lchar '|'; return ()

224 = do lchar '|'; return ()

220− <|> do c <- indent; l <- last_indent

225+ <|> do c <- indent; l <- lastIndent

221− if (c <= l) then return ()

222− else fail "Not a terminator"

226+ unless (c <= l) $ fail "Not a terminator"

223 <|> lookAhead eof

227 <|> lookAhead eof

224

228

225pKeepTerminator

229pKeepTerminator

226 = do lchar ';'; return ()

230 = do lchar ';'; return ()

227− <|> do c <- indent; l <- last_indent

231+ <|> do c <- indent; l <- lastIndent

228− if (c <= l) then return ()

229− else fail "Not a terminator"

232+ unless (c <= l) $ fail "Not a terminator"

230− <|> do i <- getInput; let h = take 1 i

233+ <|> do i <- getInput

231− if (h == "}" || h == ")" || h == "|") then return ()

234+ let h = take 1 i

232− else fail "Not a terminator"

235+ unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"

233 <|> lookAhead eof

236 <|> lookAhead eof

234

237

235−notEndApp = do c <- indent; l <- last_indent

238+notEndApp = do c <- indent; l <- lastIndent

236 i <- getInput

239 i <- getInput

237− if (c <= l) then fail "Terminator"

240+ when (c <= l) $ fail "Terminator"

238− else return ()

239

241

240notEndBlock = do ist <- getState

242notEndBlock = do ist <- getState

241 case brace_stack ist of

243 case brace_stack ist of

242− Just lvl : xs -> do i <- indent

244+ Just lvl : xs -> do i <- indent

243 inp <- getInput

245 inp <- getInput

244− if (i < lvl || take 1 inp == ")")

245− then fail "End of block"

246+ when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"

246− else return ()

247− _ -> return ()

247+ _ -> return ()

248

249pfc :: IParser FC

250pfc = do s <- getPosition

251 let (dir, file) = splitFileName (sourceName s)

252 let f = case dir of

253− "./" -> file

253+ "./" -> file

254− _ -> sourceName s

254+ _ -> sourceName s

255 return $ FC f (sourceLine s)

256

257pImport :: IParser String

258−pImport = do reserved "import"

258+pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')

259− f <- identifier

260− option ';' (lchar ';')

261 return (map dot f)

259 return (map dot f)

262 where dot '.' = '/'

260 where dot '.' = '/'

263 dot c = c

261 dot c = c

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

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

266parseProg syn fname input pos

264parseProg syn fname input pos

267 = do i <- get

265 = do i <- get

268− case (runParser (do setPosition pos

266+ case runParser (do setPosition pos

269− whiteSpace

267+ whiteSpace

270− ps <- many (pDecl syn)

268+ ps <- many (pDecl syn)

271− eof

269+ eof

272− i' <- getState

270+ i' <- getState

273− return (concat ps, i')) i fname input) of

271+ return (concat ps, i')) i fname input of

274− Left err -> fail (ishow err)

272+ Left err -> fail (iShowError fname err)

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

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

276 return (collect x)

274 return (collect x)

277− where ishow err = let ln = sourceLine (errorPos err) in

278− fname ++ ":" ++ show ln ++ ":parse error"

279− ++ " at column " ++ show (sourceColumn (errorPos err))

280−-- show (map messageString (errorMessages err))

281

275

282-- Collect PClauses with the same function name

276-- Collect PClauses with the same function name

283

277

323 <|> pInstance syn

317 <|> pInstance syn

324 <|> do d <- pDSL syn; return [d]

318 <|> do d <- pDSL syn; return [d]

325 <|> pDirective

319 <|> pDirective

326− <|> try (do reserved "import"

320+ <|> try (do reserved "import"; fp <- identifier

327− fp <- identifier

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

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

329

322

330pFunDecl :: SyntaxInfo -> IParser [PDecl]

323pFunDecl :: SyntaxInfo -> IParser [PDecl]

366

359

367pSyntaxRule :: SyntaxInfo -> IParser Syntax

360pSyntaxRule :: SyntaxInfo -> IParser Syntax

368pSyntaxRule syn

361pSyntaxRule syn

369− = do push_indent

362+ = do pushIndent

370 sty <- option AnySyntax (do reserved "term"; return TermSyntax

363 sty <- option AnySyntax (do reserved "term"; return TermSyntax

371 <|> do reserved "pattern"; return PatternSyntax)

364 <|> do reserved "pattern"; return PatternSyntax)

372 reserved "syntax"

365 reserved "syntax"

406 return (Symbol sym)

399 return (Symbol sym)

407

400

408pFunDecl' :: SyntaxInfo -> IParser PDecl

401pFunDecl' :: SyntaxInfo -> IParser PDecl

409−pFunDecl' syn = try (do push_indent

402+pFunDecl' syn = try (do pushIndent

410 opts <- pFnOpts

403 opts <- pFnOpts

411 acc <- pAccessibility

404 acc <- pAccessibility

412 opts' <- pFnOpts

405 opts' <- pFnOpts

422

415

423pUsing :: SyntaxInfo -> IParser [PDecl]

416pUsing :: SyntaxInfo -> IParser [PDecl]

424pUsing syn =

417pUsing syn =

425− do reserved "using";

418+ do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')'

426− lchar '('

419+ openBlock

427− ns <- tyDeclList syn

428− lchar ')'

429− open_block

430 let uvars = using syn

420 let uvars = using syn

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

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

432− close_block

422+ closeBlock

433 return (concat ds)

423 return (concat ds)

434

424

435pParams :: SyntaxInfo -> IParser [PDecl]

425pParams :: SyntaxInfo -> IParser [PDecl]

436pParams syn =

426pParams syn =

437− do reserved "params";

427+ do reserved "params"; lchar '('; ns <- tyDeclList syn; lchar ')'

438− lchar '('

439− ns <- tyDeclList syn

440− lchar ')'

441 lchar '{'

428 lchar '{'

442 let pvars = syn_params syn

429 let pvars = syn_params syn

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

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

447

434

448pNamespace :: SyntaxInfo -> IParser [PDecl]

435pNamespace :: SyntaxInfo -> IParser [PDecl]

449pNamespace syn =

436pNamespace syn =

450− do reserved "namespace";

437+ do reserved "namespace"; n <- identifier;

451− n <- identifier

438+ openBlock

452− open_block

453 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })

439 ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })

454− close_block

440+ closeBlock

455 return [PNamespace n (concat ds)]

441 return [PNamespace n (concat ds)]

456

442

457--------- Fixity ---------

443--------- Fixity ---------

458

444

459pFixity :: IParser PDecl

445pFixity :: IParser PDecl

460−pFixity = do push_indent

446+pFixity = do pushIndent

461 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

447 f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

462 pTerminator

448 pTerminator

463 let prec = fromInteger i

449 let prec = fromInteger i

479

465

480pClass :: SyntaxInfo -> IParser [PDecl]

466pClass :: SyntaxInfo -> IParser [PDecl]

481pClass syn = do acc <- pAccessibility

467pClass syn = do acc <- pAccessibility

482− reserved "class"

483− fc <- pfc

484− cons <- pConstList syn

468+ reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName

485− n_in <- pName; let n = expandNS syn n_in

469+ let n = expandNS syn n_in

486 cs <- many1 carg

470 cs <- many1 carg

487− reserved "where"; open_block

471+ reserved "where"; openBlock

488 ds <- many $ pFunDecl syn

472 ds <- many $ pFunDecl syn

489− close_block

473+ closeBlock

490 let allDs = concat ds

474 let allDs = concat ds

491 accData acc n (concatMap declared allDs)

475 accData acc n (concatMap declared allDs)

492 return [PClass syn fc cons n cs allDs]

476 return [PClass syn fc cons n cs allDs]

497 return (i, PSet)

481 return (i, PSet)

498

482

499pInstance :: SyntaxInfo -> IParser [PDecl]

483pInstance :: SyntaxInfo -> IParser [PDecl]

500−pInstance syn = do reserved "instance"

484+pInstance syn = do reserved "instance"; fc <- pfc

501− fc <- pfc

502 en <- option Nothing

485 en <- option Nothing

503 (do lchar '['; n_in <- pfName; lchar ']'

486 (do lchar '['; n_in <- pfName; lchar ']'

504 let n = expandNS syn n_in

487 let n = expandNS syn n_in

508 args <- many1 (pSimpleExpr syn)

491 args <- many1 (pSimpleExpr syn)

509 let sc = PApp fc (PRef fc cn) (map pexp args)

492 let sc = PApp fc (PRef fc cn) (map pexp args)

510 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc

493 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc

511− reserved "where"; open_block

494+ reserved "where"; openBlock

512 ds <- many $ pFunDecl syn

495 ds <- many $ pFunDecl syn

513− close_block

496+ closeBlock

514 return [PInstance syn fc cs cn args t en (concat ds)]

497 return [PInstance syn fc cs cn args t en (concat ds)]

515

498

516--------- Expressions ---------

499--------- Expressions ---------

535 simple (Rule (SimpleExpr x:xs) _ _) = False

518 simple (Rule (SimpleExpr x:xs) _ _) = False

536 simple (Rule [Keyword _] _ _) = True

519 simple (Rule [Keyword _] _ _) = True

537 simple (Rule [Symbol _] _ _) = True

520 simple (Rule [Symbol _] _ _) = True

538− simple (Rule (_:xs) _ _) = case (last xs) of

521+ simple (Rule (_:xs) _ _) = case last xs of

539 Keyword _ -> True

522 Keyword _ -> True

540 Symbol _ -> True

523 Symbol _ -> True

541 _ -> False

524 _ -> False

552 <|> pComprehension syn

535 <|> pComprehension syn

553

536

554pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

537pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

555−pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))

538+pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))

556 where

539 where

557 valid (Rule _ _ AnySyntax) = True

540 valid (Rule _ _ AnySyntax) = True

558 valid (Rule _ _ PatternSyntax) = inPattern syn

541 valid (Rule _ _ PatternSyntax) = inPattern syn

649addAcc n a = do i <- getState

632addAcc n a = do i <- getState

650 setState (i { hide_list = (n, a) : hide_list i })

633 setState (i { hide_list = (n, a) : hide_list i })

651

634

635+pCaseExpr syn = do

636+ reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";

637+ openBlock

638+ pushIndent

639+ opts <- many1 (do notEndBlock

640+ x <- pCaseOpt syn

641+ pKeepTerminator

642+ return x) -- sepBy1 (pCaseOpt syn) (lchar '|')

643+ popIndent

644+ closeBlock

645+ return (PCase fc scr opts)

646+

647+pProofExpr syn = do

648+ reserved "proof"; lchar '{'

649+ ts <- endBy (pTactic syn) (lchar ';')

650+ lchar '}'

651+ return (PProof ts)

652+

653+pTacticsExpr syn = do

654+ reserved "tactics"; lchar '{'

655+ ts <- endBy (pTactic syn) (lchar ';')

656+ lchar '}'

657+ return (PTactics ts)

658+

652pSimpleExpr syn =

659pSimpleExpr syn =

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

660+ try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)

654− return $ PQuote t)

655 <|> do lchar '?'; x <- pName; return (PMetavar x)

661 <|> do lchar '?'; x <- pName; return (PMetavar x)

656 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)

662 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)

657-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)

663-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)

658− <|> do reserved "proof"; lchar '{';

664+ <|> pProofExpr syn

659− ts <- endBy (pTactic syn) (lchar ';')

665+ <|> pTacticsExpr syn

660− lchar '}'

666+ <|> pCaseExpr syn

661− return (PProof ts)

667+ <|> try (do x <- pfName

662− <|> do reserved "tactics"; lchar '{';

668+ fc <- pfc

663− ts <- endBy (pTactic syn) (lchar ';')

664− lchar '}'

665− return (PTactics ts)

666− <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";

667− open_block

668− push_indent

669− opts <- many1 (do notEndBlock

670− x <- pCaseOpt syn

671− pKeepTerminator

672− return x) -- sepBy1 (pCaseOpt syn) (lchar '|')

673− pop_indent

674− close_block

675− return (PCase fc scr opts)

676− <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

669+ return (PRef fc x))

677 <|> try (pList syn)

670 <|> try (pList syn)

678 <|> try (pAlt syn)

671 <|> try (pAlt syn)

679 <|> try (pIdiom syn)

672 <|> try (pIdiom syn)

673+ <|> try (do lchar '('

680− <|> try (do lchar '('; bracketed (noImp syn))

674+ bracketed (noImp syn))

681− <|> try (do c <- pConstant; fc <- pfc

675+ <|> try (do c <- pConstant

676+ fc <- pfc

682 return (modifyConst syn fc (PConstant c)))

677 return (modifyConst syn fc (PConstant c)))

683 <|> do reserved "Set"; return PSet

678 <|> do reserved "Set"; return PSet

684−-- <|> do symbol "*"; return PSet

679+ <|> try (do symbol "()"

680+ fc <- pfc

685− <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))

681+ return (PTrue fc))

682+ <|> try (do symbol "_|_"

683+ fc <- pfc

686− <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))

684+ return (PFalse fc))

687 <|> do lchar '_'; return Placeholder

685 <|> do lchar '_'; return Placeholder

688 <|> pSimpleExtExpr syn

686 <|> pSimpleExtExpr syn

689

687

703 pexp (PRef fc (MN 0 "x"))]))

701 pexp (PRef fc (MN 0 "x"))]))

704

702

705pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)

703pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)

706−pCaseOpt syn = do lhs <- pExpr syn; symbol "=>";

704+pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn

707− rhs <- pExpr syn

708 return (lhs, rhs)

705 return (lhs, rhs)

709

706

710modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

707modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

714 | otherwise = PConstant (I x)

711 | otherwise = PConstant (I x)

715modifyConst syn fc x = x

712modifyConst syn fc x = x

716

713

717−pList syn = do lchar '['; fc <- pfc

718− xs <- sepBy (pExpr syn) (lchar ','); lchar ']'

714+pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'

719 return (mkList fc xs)

715 return (mkList fc xs)

720 where

716 where

721 mkList fc [] = PRef fc (UN "Nil")

717 mkList fc [] = PRef fc (UN "Nil")

731 <|> try (do x <- ntuple

727 <|> try (do x <- ntuple

732 lchar ')'

728 lchar ')'

733 return x)

729 return x)

734− <|> do ln <- pName; lchar ':'; lty <- pExpr syn;

730+ <|> do ln <- pName; lchar ':'

731+ lty <- pExpr syn

735− reservedOp "**";

732+ reservedOp "**"

736 fc <- pfc

733 fc <- pfc

737− r <- pExpr syn; lchar ')';

734+ r <- pExpr syn

735+ lchar ')'

738 return (PDPair fc (PRef fc ln) lty r)

736 return (PDPair fc (PRef fc ln) lty r)

739 where

737 where

740 restTuple = do lchar ')'; return []

738 restTuple = do lchar ')'; return []

753 r <- pExpr syn

751 r <- pExpr syn

754 return (PPair fc l r))

752 return (PPair fc l r))

755

753

756−pAlt syn = do symbol "(|";

757− alts <- sepBy1 (pExpr' syn) (lchar ',')

754+pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"

758− symbol "|)"

759 return (PAlternative False alts)

755 return (PAlternative False alts)

760

756

761pHSimpleExpr syn

757pHSimpleExpr syn

782 <|> do e <- pSimpleExpr syn

778 <|> do e <- pSimpleExpr syn

783 return (pexp e)

779 return (pexp e)

784

780

785−pImplicitArg syn = do lchar '{'; n <- pName

781+pImplicitArg syn = do lchar '{'

782+ n <- pName

786 fc <- pfc

783 fc <- pfc

787− v <- option (PRef fc n) (do lchar '='; pExpr syn)

784+ v <- option (PRef fc n) (do lchar '='

785+ pExpr syn)

788 lchar '}'

786 lchar '}'

789 return (pimp n v)

787 return (pimp n v)

790

788

791−pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"

789+pConstraintArg syn = do symbol "@{"

790+ e <- pExpr syn

791+ symbol "}"

792 return (pconst e)

793

794pRecordSet syn

797 fields <- sepBy1 pFieldSet (lchar ',')

798 lchar '}'

799 fc <- pfc

800− rec <- option Nothing (do e <- pSimpleExpr syn; return (Just e))

800+ rec <- option Nothing (do e <- pSimpleExpr syn

801+ return (Just e))

801 case rec of

802 case rec of

802 Nothing ->

803 Nothing ->

803 return (PLam (MN 0 "fldx") Placeholder

804 return (PLam (MN 0 "fldx") Placeholder

804 (applyAll fc fields (PRef fc (MN 0 "fldx"))))

805 (applyAll fc fields (PRef fc (MN 0 "fldx"))))

805 Just v -> return (applyAll fc fields v)

806 Just v -> return (applyAll fc fields v)

806− where pFieldSet = do n <- pfName; lchar '='

807+ where pFieldSet = do n <- pfName

808+ lchar '='

807 e <- pExpr syn

809 e <- pExpr syn

808 return (n, e)

810 return (n, e)

809 applyAll fc [] x = x

811 applyAll fc [] x = x

823 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

825 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

824

826

825pLambda syn = do lchar '\\'

827pLambda syn = do lchar '\\'

826− (try (do xt <- tyOptDeclList syn

828+ try (do xt <- tyOptDeclList syn

827− symbol "=>"

829+ symbol "=>"

828− sc <- pExpr syn

830+ sc <- pExpr syn

829− return (bindList PLam xt sc))

831+ return (bindList PLam xt sc)

830 <|> (do ps <- sepBy (do fc <- pfc

832 <|> (do ps <- sepBy (do fc <- pfc

831 e <- pSimpleExpr syn

833 e <- pSimpleExpr syn

832 return (fc, e)) (lchar ',')

834 return (fc, e)) (lchar ',')

837 pmList ((i, (fc, x)) : xs) sc

839 pmList ((i, (fc, x)) : xs) sc

838 = PLam (MN i "lamp") Placeholder

840 = PLam (MN i "lamp") Placeholder

839 (PCase fc (PRef fc (MN i "lamp"))

841 (PCase fc (PRef fc (MN i "lamp"))

840− [(x, (pmList xs sc))])

842+ [(x, pmList xs sc)])

841

843

842pLet syn = try (do reserved "let"; n <- pName;

844pLet syn = try (do reserved "let"; n <- pName;

843 ty <- option Placeholder (do lchar ':'; pExpr' syn)

845 ty <- option Placeholder (do lchar ':'; pExpr' syn)

846+ lchar '='

844− lchar '='; v <- pExpr syn

847+ v <- pExpr syn

845 reserved "in"; sc <- pExpr syn

848 reserved "in"; sc <- pExpr syn

846 return (PLet n ty v sc))

849 return (PLet n ty v sc))

847 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn

850 <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn

856 symbol "->"

859 symbol "->"

857 sc <- pExpr syn

860 sc <- pExpr syn

858 return (bindList (PPi (Exp lazy st)) xt sc))

861 return (bindList (PPi (Exp lazy st)) xt sc))

859− <|> try (if implicitAllowed syn then

862+ <|> try (if implicitAllowed syn

860− do lazy <- option False (do lchar '|'; return True)

863+ then do lazy <- option False (do lchar '|'

864+ return True)

861− st <- pStatic

865+ st <- pStatic

866+ lchar '{'

862− lchar '{'; xt <- tyDeclList syn; lchar '}'

867+ xt <- tyDeclList syn

868+ lchar '}'

863− symbol "->"

869+ symbol "->"

864− sc <- pExpr syn

870+ sc <- pExpr syn

865− return (bindList (PPi (Imp lazy st)) xt sc)

871+ return (bindList (PPi (Imp lazy st)) xt sc)

866 else fail "No implicit arguments allowed here")

872 else fail "No implicit arguments allowed here")

873+ <|> try (do lchar '{'

867− <|> try (do lchar '{'; reserved "auto"

874+ reserved "auto"

868− xt <- tyDeclList syn; lchar '}'

875+ xt <- tyDeclList syn

876+ lchar '}'

869 symbol "->"

877 symbol "->"

870 sc <- pExpr syn

878 sc <- pExpr syn

871 return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))

879 return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc))

880+ <|> try (do lchar '{'

872− <|> try (do lchar '{'; reserved "default"

881+ reserved "default"

873 script <- pSimpleExpr syn

882 script <- pSimpleExpr syn

874− xt <- tyDeclList syn; lchar '}'

883+ xt <- tyDeclList syn

884+ lchar '}'

875 symbol "->"

885 symbol "->"

876 sc <- pExpr syn

886 sc <- pExpr syn

877 return (bindList (PPi (TacImp False Dynamic script)) xt sc))

887 return (bindList (PPi (TacImp False Dynamic script)) xt sc))

878 <|> do --lazy <- option False (do lchar '|'; return True)

888 <|> do --lazy <- option False (do lchar '|'; return True)

889+ lchar '{'

879− lchar '{'; reserved "static"; lchar '}'

890+ reserved "static"

891+ lchar '}'

880 t <- pExpr' syn

892 t <- pExpr' syn

881 symbol "->"

893 symbol "->"

882 sc <- pExpr syn

894 sc <- pExpr syn

893 return [t])

905 return [t])

894 <|> return []

906 <|> return []

895

907

896−tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig (noImp syn); return (x,t))

908+tyDeclList syn = try (sepBy1 (do x <- pfName

909+ t <- pTSig (noImp syn)

910+ return (x,t))

897 (lchar ','))

911 (lchar ','))

898 <|> do ns <- sepBy1 pName (lchar ',')

912 <|> do ns <- sepBy1 pName (lchar ',')

899 t <- pTSig (noImp syn)

913 t <- pTSig (noImp syn)

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

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

910

924

911pComprehension syn

925pComprehension syn

926+ = do lchar '['

927+ fc <- pfc

912− = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|';

928+ pat <- pExpr syn

929+ lchar '|'

913− qs <- sepBy1 (pDo syn) (lchar ','); lchar ']';

930+ qs <- sepBy1 (pDo syn) (lchar ',')

931+ lchar ']'

914 return (PDoBlock (map addGuard qs ++

932 return (PDoBlock (map addGuard qs ++

915 [DoExp fc (PApp fc (PRef fc (UN "return"))

933 [DoExp fc (PApp fc (PRef fc (UN "return"))

916 [pexp pat])]))

934 [pexp pat])]))

919 addGuard x = x

937 addGuard x = x

920

938

921pDoBlock syn

939pDoBlock syn

922− = do reserved "do"; open_block

940+ = do reserved "do"

923− push_indent

941+ openBlock

942+ pushIndent

924 ds <- many1 (do notEndBlock

943 ds <- many1 (do notEndBlock

944+ x <- pDo syn

925− x <- pDo syn; pKeepTerminator; return x)

945+ pKeepTerminator

926− pop_indent

946+ return x)

927− close_block

947+ popIndent

948+ closeBlock

928 return (PDoBlock ds)

949 return (PDoBlock ds)

929

950

930pDo syn

951pDo syn

931− = try (do reserved "let"; i <- pName;

952+ = try (do reserved "let"

953+ i <- pName;

932− ty <- option Placeholder (do lchar ':'; pExpr' syn)

954+ ty <- option Placeholder (do lchar ':'

955+ pExpr' syn)

933− reservedOp "="; fc <- pfc

956+ reservedOp "="

957+ fc <- pfc

934 e <- pExpr syn

958 e <- pExpr syn

935 return (DoLet fc i ty e))

959 return (DoLet fc i ty e))

936− <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc

960+ <|> try (do reserved "let"

961+ i <- pExpr' syn

962+ reservedOp "="

963+ fc <- pfc

937 sc <- pExpr syn

964 sc <- pExpr syn

938 return (DoLetP fc i sc))

965 return (DoLetP fc i sc))

939− <|> try (do i <- pName; symbol "<-"; fc <- pfc

966+ <|> try (do i <- pName

967+ symbol "<-"

968+ fc <- pfc

940 e <- pExpr syn;

969 e <- pExpr syn;

941 return (DoBind fc i e))

970 return (DoBind fc i e))

942− <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc

971+ <|> try (do i <- pExpr' syn

972+ symbol "<-"

973+ fc <- pfc

943 e <- pExpr syn;

974 e <- pExpr syn;

944 return (DoBindP fc i e))

975 return (DoBindP fc i e))

945− <|> try (do e <- pExpr syn; fc <- pfc

976+ <|> try (do e <- pExpr syn

977+ fc <- pfc

946 return (DoExp fc e))

978 return (DoExp fc e))

947

979

948pIdiom syn

980pIdiom syn

981+ = do symbol "[|"

982+ fc <- pfc

949− = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]"

983+ e <- pExpr syn

984+ symbol "|]"

950 return (PIdiom fc e)

985 return (PIdiom fc e)

951

986

952pConstant :: IParser Const

987pConstant :: IParser Const

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

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

964

999

965pStatic :: IParser Static

1000pStatic :: IParser Static

966−pStatic = do lchar '['; reserved "static"; lchar ']';

1001+pStatic = do lchar '['

1002+ reserved "static"

1003+ lchar ']';

967 return Static

1004 return Static

968 <|> return Dynamic

1005 <|> return Dynamic

969

1006

972 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]

1009 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]

973 ++ toTable (reverse fixes) ++

1010 ++ toTable (reverse fixes) ++

974 [[backtick],

1011 [[backtick],

975− [binary "=" (\fc x y -> PEq fc x y) AssocLeft],

1012+ [binary "=" PEq AssocLeft],

976 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]

1013 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]

977

1014

978toTable fs = map (map toBin)

1015toTable fs = map (map toBin)

985 assoc (Infixr _) = AssocRight

1022 assoc (Infixr _) = AssocRight

986 assoc (InfixN _) = AssocNone

1023 assoc (InfixN _) = AssocNone

987

1024

988−binary name f assoc = Infix (do reservedOp name; fc <- pfc;

1025+binary name f = Infix (do reservedOp name

1026+ fc <- pfc;

989− return (f fc)) assoc

1027+ return (f fc))

990−prefix name f = Prefix (do reservedOp name; fc <- pfc;

1028+prefix name f = Prefix (do reservedOp name

1029+ fc <- pfc;

991 return (f fc))

1030 return (f fc))

992−backtick = Infix (do lchar '`'; n <- pfName; lchar '`'

1031+backtick = Infix (do lchar '`'; n <- pfName

1032+ lchar '`'

993 fc <- pfc

1033 fc <- pfc

994 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

1034 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

995

1035

999accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()

1039accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()

1000accData (Just Frozen) n ns = do addAcc n (Just Frozen)

1040accData (Just Frozen) n ns = do addAcc n (Just Frozen)

1001 mapM_ (\n -> addAcc n (Just Hidden)) ns

1041 mapM_ (\n -> addAcc n (Just Hidden)) ns

1002−accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns

1042+accData a n ns = do addAcc n a

1043+ mapM_ (`addAcc` a) ns

1003

1044

1004pRecord :: SyntaxInfo -> IParser PDecl

1045pRecord :: SyntaxInfo -> IParser PDecl

1005pRecord syn = do acc <- pAccessibility

1046pRecord syn = do acc <- pAccessibility

1006− reserved "record"; fc <- pfc

1047+ reserved "record"

1048+ fc <- pfc

1049+ tyn_in <- pfName

1007− tyn_in <- pfName; ty <- pTSig (impOK syn)

1050+ ty <- pTSig (impOK syn)

1008 let tyn = expandNS syn tyn_in

1051 let tyn = expandNS syn tyn_in

1009 reserved "where"

1052 reserved "where"

1010− open_block

1053+ openBlock

1011− push_indent

1054+ pushIndent

1012 (cn, cty, _) <- pConstructor syn

1055 (cn, cty, _) <- pConstructor syn

1013 pKeepTerminator

1056 pKeepTerminator

1014− pop_indent

1057+ popIndent

1015− close_block

1058+ closeBlock

1016 accData acc tyn [cn]

1059 accData acc tyn [cn]

1017 let rsyn = syn { syn_namespace = show (nsroot tyn) :

1060 let rsyn = syn { syn_namespace = show (nsroot tyn) :

1018 syn_namespace syn }

1061 syn_namespace syn }

1029

1072

1030pData :: SyntaxInfo -> IParser PDecl

1073pData :: SyntaxInfo -> IParser PDecl

1031pData syn = try (do acc <- pAccessibility

1074pData syn = try (do acc <- pAccessibility

1032− reserved "data"; fc <- pfc

1075+ reserved "data"

1076+ fc <- pfc

1077+ tyn_in <- pfName

1033− tyn_in <- pfName; ty <- pTSig (impOK syn)

1078+ ty <- pTSig (impOK syn)

1034 let tyn = expandNS syn tyn_in

1079 let tyn = expandNS syn tyn_in

1035 reserved "where"

1080 reserved "where"

1036− open_block

1081+ openBlock

1037− push_indent

1082+ pushIndent

1038 cons <- many (do notEndBlock

1083 cons <- many (do notEndBlock

1039 c <- pConstructor syn

1084 c <- pConstructor syn

1040 pKeepTerminator

1085 pKeepTerminator

1041 return c) -- (lchar '|')

1086 return c) -- (lchar '|')

1042− pop_indent

1087+ popIndent

1043− close_block

1088+ closeBlock

1044 accData acc tyn (map (\ (n, _, _) -> n) cons)

1089 accData acc tyn (map (\ (n, _, _) -> n) cons)

1045 return $ PData syn fc (PDatadecl tyn ty cons))

1090 return $ PData syn fc (PDatadecl tyn ty cons))

1046− <|> try (do push_indent

1091+ <|> try (do pushIndent

1047 acc <- pAccessibility

1092 acc <- pAccessibility

1048− reserved "data"; fc <- pfc

1093+ reserved "data"

1094+ fc <- pfc

1095+ tyn_in <- pfName

1049− tyn_in <- pfName; args <- many pName

1096+ args <- many pName

1050 let tyn = expandNS syn tyn_in

1097 let tyn = expandNS syn tyn_in

1051 lchar '='

1098 lchar '='

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

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

1053 pTerminator

1100 pTerminator

1054 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

1101 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

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

1102+ let ty = bindArgs (map (const PSet) args) PSet

1056 cons' <- mapM (\ (x, cargs, cfc) ->

1103 cons' <- mapM (\ (x, cargs, cfc) ->

1057 do let cty = bindArgs cargs conty

1104 do let cty = bindArgs cargs conty

1058 return (x, cty, cfc)) cons

1105 return (x, cty, cfc)) cons

1063 mkPApp fc t xs = PApp fc t (map pexp xs)

1110 mkPApp fc t xs = PApp fc t (map pexp xs)

1064

1111

1065bindArgs :: [PTerm] -> PTerm -> PTerm

1112bindArgs :: [PTerm] -> PTerm -> PTerm

1066−bindArgs [] t = t

1113+bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

1067−bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)

1068

1114

1069pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

1115pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

1070pConstructor syn

1116pConstructor syn

1087--------- DSL syntax overloading ---------

1133--------- DSL syntax overloading ---------

1088

1134

1089pDSL :: SyntaxInfo -> IParser PDecl

1135pDSL :: SyntaxInfo -> IParser PDecl

1090−pDSL syn = do reserved "dsl"; n <- pfName

1136+pDSL syn = do reserved "dsl"

1091− open_block; push_indent

1137+ n <- pfName

1138+ openBlock

1139+ pushIndent

1092 bs <- many1 (do notEndBlock

1140 bs <- many1 (do notEndBlock

1093 b <- pOverload syn

1141 b <- pOverload syn

1094 pKeepTerminator

1142 pKeepTerminator

1095 return b)

1143 return b)

1096− pop_indent; close_block

1144+ popIndent; closeBlock

1097 let dsl = mkDSL bs (dsl_info syn)

1145 let dsl = mkDSL bs (dsl_info syn)

1098 checkDSL dsl

1146 checkDSL dsl

1099 i <- getState

1147 i <- getState

1114checkDSL dsl = return ()

1162checkDSL dsl = return ()

1115

1163

1116pOverload :: SyntaxInfo -> IParser (String, PTerm)

1164pOverload :: SyntaxInfo -> IParser (String, PTerm)

1117−pOverload syn = do o <- identifier <|> do reserved "let"; return "let"

1165+pOverload syn = do o <- identifier <|> do reserved "let"

1166+ return "let"

1118− if (not (o `elem` overloadable))

1167+ if o `notElem` overloadable

1119 then fail $ show o ++ " is not an overloading"

1168 then fail $ show o ++ " is not an overloading"

1120 else do

1169 else do

1121 lchar '='

1170 lchar '='

1144

1193

1145pClause :: SyntaxInfo -> IParser PClause

1194pClause :: SyntaxInfo -> IParser PClause

1146pClause syn

1195pClause syn

1147− = try (do push_indent

1196+ = try (do pushIndent

1148 n_in <- pfName; let n = expandNS syn n_in

1197 n_in <- pfName; let n = expandNS syn n_in

1149 cargs <- many (pConstraintArg syn)

1198 cargs <- many (pConstraintArg syn)

1150 iargs <- many (pImplicitArg syn)

1199 iargs <- many (pImplicitArg syn)

1156 let ctxt = tt_ctxt ist

1205 let ctxt = tt_ctxt ist

1157 let wsyn = syn { syn_namespace = [] }

1206 let wsyn = syn { syn_namespace = [] }

1158 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn

1207 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn

1159− pop_indent

1208+ popIndent

1160 return x,

1209 return x,

1161 do pTerminator

1210 do pTerminator

1162 return ([], [])]

1211 return ([], [])]

1165 ist <- getState

1214 ist <- getState

1166 setState (ist { lastParse = Just n })

1215 setState (ist { lastParse = Just n })

1167 return $ PClause fc n capp wargs rhs wheres)

1216 return $ PClause fc n capp wargs rhs wheres)

1168− <|> try (do push_indent

1217+ <|> try (do pushIndent

1169 wargs <- many1 (pWExpr syn)

1218 wargs <- many1 (pWExpr syn)

1170 ist <- getState

1219 ist <- getState

1171 n <- case lastParse ist of

1220 n <- case lastParse ist of

1176 let ctxt = tt_ctxt ist

1225 let ctxt = tt_ctxt ist

1177 let wsyn = syn { syn_namespace = [] }

1226 let wsyn = syn { syn_namespace = [] }

1178 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn

1227 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn

1179− pop_indent

1228+ popIndent

1180 return x,

1229 return x,

1181 do pTerminator

1230 do pTerminator

1182 return ([], [])]

1231 return ([], [])]

1183 return $ PClauseR fc wargs rhs wheres)

1232 return $ PClauseR fc wargs rhs wheres)

1184

1233

1185− <|> try (do push_indent

1234+ <|> try (do pushIndent

1186 n_in <- pfName; let n = expandNS syn n_in

1235 n_in <- pfName; let n = expandNS syn n_in

1187 cargs <- many (pConstraintArg syn)

1236 cargs <- many (pConstraintArg syn)

1188 iargs <- many (pImplicitArg syn)

1237 iargs <- many (pImplicitArg syn)

1195 setState (ist { lastParse = Just n })

1244 setState (ist { lastParse = Just n })

1196 reserved "with"

1245 reserved "with"

1197 wval <- pSimpleExpr syn

1246 wval <- pSimpleExpr syn

1198− open_block

1247+ openBlock

1199 ds <- many1 $ pFunDecl syn

1248 ds <- many1 $ pFunDecl syn

1200 let withs = map (fillLHSD n capp wargs) $ concat ds

1249 let withs = map (fillLHSD n capp wargs) $ concat ds

1201− close_block

1250+ closeBlock

1202− pop_indent

1251+ popIndent

1203 return $ PWith fc n capp wargs wval withs)

1252 return $ PWith fc n capp wargs wval withs)

1204

1253

1205 <|> try (do wargs <- many1 (pWExpr syn)

1254 <|> try (do wargs <- many1 (pWExpr syn)

1206 fc <- pfc

1255 fc <- pfc

1207 reserved "with"

1256 reserved "with"

1208 wval <- pSimpleExpr syn

1257 wval <- pSimpleExpr syn

1209− open_block

1258+ openBlock

1210 ds <- many1 $ pFunDecl syn

1259 ds <- many1 $ pFunDecl syn

1211 let withs = concat ds

1260 let withs = concat ds

1212− close_block

1261+ closeBlock

1213 return $ PWithR fc wargs wval withs)

1262 return $ PWithR fc wargs wval withs)

1214

1263

1215− <|> do push_indent

1264+ <|> do pushIndent

1216 l <- pArgExpr syn

1265 l <- pArgExpr syn

1217 op <- operator

1266 op <- operator

1218 let n = expandNS syn (UN op)

1267 let n = expandNS syn (UN op)

1222 rhs <- pRHS syn n

1271 rhs <- pRHS syn n

1223 let wsyn = syn { syn_namespace = [] }

1272 let wsyn = syn { syn_namespace = [] }

1224 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn

1273 (wheres, nmap) <- choice [do x <- pWhereblock n wsyn

1225− pop_indent

1274+ popIndent

1226 return x,

1275 return x,

1227 do pTerminator

1276 do pTerminator

1228 return ([], [])]

1277 return ([], [])]

1239 wargs <- many (pWExpr syn)

1288 wargs <- many (pWExpr syn)

1240 reserved "with"

1289 reserved "with"

1241 wval <- pSimpleExpr syn

1290 wval <- pSimpleExpr syn

1242− open_block

1291+ openBlock

1243 ds <- many1 $ pFunDecl syn

1292 ds <- many1 $ pFunDecl syn

1244− close_block

1293+ closeBlock

1245 ist <- getState

1294 ist <- getState

1246 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

1295 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

1247 let withs = map (fillLHSD n capp wargs) $ concat ds

1296 let withs = map (fillLHSD n capp wargs) $ concat ds

1259 fillLHSD n c a x = x

1308 fillLHSD n c a x = x

1260

1309

1261pWExpr :: SyntaxInfo -> IParser PTerm

1310pWExpr :: SyntaxInfo -> IParser PTerm

1262−pWExpr syn = do lchar '|'; pExpr' syn

1311+pWExpr syn = do lchar '|'

1312+ pExpr' syn

1263

1313

1264pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])

1314pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])

1265pWhereblock n syn

1315pWhereblock n syn

1266− = do reserved "where"; open_block

1316+ = do reserved "where"; openBlock

1267 ds <- many1 $ pFunDecl syn

1317 ds <- many1 $ pFunDecl syn

1268 let dns = concatMap (concatMap declared) ds

1318 let dns = concatMap (concatMap declared) ds

1269− close_block

1319+ closeBlock

1270 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1320 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1271

1321

1272pDirective :: IParser [PDecl]

1322pDirective :: IParser [PDecl]

1274 return [PDirective (do addLib lib

1324 return [PDirective (do addLib lib

1275 addIBC (IBCLib lib))])

1325 addIBC (IBCLib lib))])

1276 <|> try (do lchar '%'; reserved "link"; obj <- strlit;

1326 <|> try (do lchar '%'; reserved "link"; obj <- strlit;

1277− return [PDirective (do datadir <- liftIO $ getDataDir

1327+ return [PDirective (do datadir <- liftIO getDataDir

1278 o <- liftIO $ findInPath [".", datadir] obj

1328 o <- liftIO $ findInPath [".", datadir] obj

1279 addIBC (IBCObj o)

1329 addIBC (IBCObj o)

1280 addObjectFile o)])

1330 addObjectFile o)])