src/Idris/Parser/Expr.hs · Idris-dev

git.iko.soy/Idris-dev

on 449089d help sign in

Idris-dev/src/Idris/Parser/Expr.hs

1552 lines 53 kB history raw

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, TupleSections #-}

2module Idris.Parser.Expr where

4import Prelude hiding (pi)

6import Text.Trifecta.Delta

7import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

8import Text.Parser.LookAhead

9import Text.Parser.Expression

10import qualified Text.Parser.Token as Tok

11import qualified Text.Parser.Char as Chr

12import qualified Text.Parser.Token.Highlight as Hi

14import Idris.AbsSyntax

15import Idris.Parser.Helpers

16import Idris.Parser.Ops

17import Idris.DSL

19import Idris.Core.TT

21import Control.Applicative

22import Control.Monad

23import Control.Monad.State.Strict

25import Data.Function (on)

26import Data.Maybe

27import qualified Data.List.Split as Spl

28import Data.List

29import Data.Monoid

30import Data.Char

31import qualified Data.HashSet as HS

32import qualified Data.Text as T

33import qualified Data.ByteString.UTF8 as UTF8

35import Debug.Trace

37-- | Allow implicit type declarations

38allowImp :: SyntaxInfo -> SyntaxInfo

39allowImp syn = syn { implicitAllowed = True }

41-- | Disallow implicit type declarations

42disallowImp :: SyntaxInfo -> SyntaxInfo

43disallowImp syn = syn { implicitAllowed = False }

45{-| Parses an expression as a whole

46@

47 FullExpr ::= Expr EOF_t;

48@

49 -}

50fullExpr :: SyntaxInfo -> IdrisParser PTerm

51fullExpr syn = do x <- expr syn

52 eof

53 i <- get

54 return $ debindApp syn (desugar syn i x)

56tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

57tryFullExpr syn st input =

58 case runparser (fullExpr syn) st "" input of

59 Success tm -> Right tm

60 Failure e -> Left (Msg (show e))

62{- | Parses an expression

63@

64 Expr ::= Pi

65@

66 -}

67expr :: SyntaxInfo -> IdrisParser PTerm

68expr = pi

70{- | Parses an expression with possible operator applied

71@

72 OpExpr ::= {- Expression Parser with Operators based on Expr' -};

73@

74-}

75opExpr :: SyntaxInfo -> IdrisParser PTerm

76opExpr syn = do i <- get

77 buildExpressionParser (table (idris_infixes i)) (expr' syn)

79{- | Parses either an internally defined expression or

80 a user-defined one

81@

82Expr' ::= "External (User-defined) Syntax"

83 | InternalExpr;

84@

85 -}

86expr' :: SyntaxInfo -> IdrisParser PTerm

87expr' syn = try (externalExpr syn)

88 <|> internalExpr syn

89 <?> "expression"

91{- | Parses a user-defined expression -}

92externalExpr :: SyntaxInfo -> IdrisParser PTerm

93externalExpr syn = do i <- get

94 (FC fn start _) <- getFC

95 expr <- extensions syn (syntaxRulesList $ syntax_rules i)

96 (FC _ _ end) <- getFC

97 let outerFC = FC fn start end

98 return (mapPTermFC (fixFC outerFC) (fixFCH fn outerFC) expr)

99 <?> "user-defined expression"

100 where -- Fix non-highlighting FCs by approximating with the span of the syntax application

101 fixFC outer inner | inner `fcIn` outer = inner

102 | otherwise = outer

103 -- Fix highlighting FCs by making them useless, to avoid spurious highlights

104 fixFCH fn outer inner | inner `fcIn` outer = inner

105 | otherwise = FileFC fn

106

107{- | Parses a simple user-defined expression -}

108simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

109simpleExternalExpr syn = do i <- get

110 extensions syn (filter isSimple (syntaxRulesList $ syntax_rules i))

111 where

112 isSimple (Rule (Expr x:xs) _ _) = False

113 isSimple (Rule (SimpleExpr x:xs) _ _) = False

114 isSimple (Rule [Keyword _] _ _) = True

115 isSimple (Rule [Symbol _] _ _) = True

116 isSimple (Rule (_:xs) _ _) = case last xs of

117 Keyword _ -> True

118 Symbol _ -> True

119 _ -> False

120 isSimple _ = False

121

122{- | Tries to parse a user-defined expression given a list of syntactic extensions -}

123extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm

124extensions syn rules = extension syn [] (filter isValid rules)

125 <?> "user-defined expression"

126 where

127 isValid :: Syntax -> Bool

128 isValid (Rule _ _ AnySyntax) = True

129 isValid (Rule _ _ PatternSyntax) = inPattern syn

130 isValid (Rule _ _ TermSyntax) = not (inPattern syn)

131 isValid (DeclRule _ _) = False

132

133data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information

134 deriving Show

135

136extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

137extension syn ns rules =

138 choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

139 case head rs of -- can never be []

140 Rule (symb:_) _ _ -> try $ do

141 n <- extensionSymbol symb

142 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

143 -- If we have more than one Rule in this bucket, our grammar is

144 -- nondeterministic.

145 Rule [] ptm _ -> return (flatten (updateSynMatch (mapMaybe id ns) ptm))

146 where

147 ruleGroup [] [] = True

148 ruleGroup (s1:_) (s2:_) = s1 == s2

149 ruleGroup _ _ = False

150

151 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

152 extensionSymbol (Keyword n) = do fc <- reservedFC (show n)

153 highlightP fc AnnKeyword

154 return Nothing

155 extensionSymbol (Expr n) = do tm <- expr syn

156 return $ Just (n, SynTm tm)

157 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn

158 return $ Just (n, SynTm tm)

159 extensionSymbol (Binding n) = do (b, fc) <- name

160 return $ Just (n, SynBind fc b)

161 extensionSymbol (Symbol s) = do fc <- symbolFC s

162 highlightP fc AnnKeyword

163 return Nothing

164

165 flatten :: PTerm -> PTerm -- flatten application

166 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

167 flatten t = t

168

169updateSynMatch = update

170 where

171 updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)

172 updateB ns (n, fc) = case lookup n ns of

173 Just (SynBind tfc t) -> (t, tfc)

174 _ -> (n, fc)

175

176 update :: [(Name, SynMatch)] -> PTerm -> PTerm

177 update ns (PRef fc hls n) = case lookup n ns of

178 Just (SynTm t) -> t

179 _ -> PRef fc hls n

180 update ns (PPatvar fc n) = uncurry (flip PPatvar) $ updateB ns (n, fc)

181 update ns (PLam fc n nfc ty sc)

182 = let (n', nfc') = updateB ns (n, nfc)

183 in PLam fc n' nfc' (update ns ty) (update (dropn n ns) sc)

184 update ns (PPi p n fc ty sc)

185 = let (n', nfc') = updateB ns (n, fc)

186 in PPi (updTacImp ns p) n' nfc'

187 (update ns ty) (update (dropn n ns) sc)

188 update ns (PLet fc n nfc ty val sc)

189 = let (n', nfc') = updateB ns (n, nfc)

190 in PLet fc n' nfc' (update ns ty)

191 (update ns val) (update (dropn n ns) sc)

192 update ns (PApp fc t args)

193 = PApp fc (update ns t) (map (fmap (update ns)) args)

194 update ns (PAppBind fc t args)

195 = PAppBind fc (update ns t) (map (fmap (update ns)) args)

196 update ns (PMatchApp fc n) = let (n', nfc') = updateB ns (n, fc)

197 in PMatchApp nfc' n'

198 update ns (PIfThenElse fc c t f)

199 = PIfThenElse fc (update ns c) (update ns t) (update ns f)

200 update ns (PCase fc c opts)

201 = PCase fc (update ns c) (map (pmap (update ns)) opts)

202 update ns (PRewrite fc eq tm mty)

203 = PRewrite fc (update ns eq) (update ns tm) (fmap (update ns) mty)

204 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)

205 update ns (PDPair fc hls p l t r)

206 = PDPair fc hls p (update ns l) (update ns t) (update ns r)

207 update ns (PAs fc n t) = PAs fc (fst $ updateB ns (n, NoFC)) (update ns t)

208 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)

209 update ns (PHidden t) = PHidden (update ns t)

210 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

211 update ns (PDoBlock ds) = PDoBlock $ map (upd ns) ds

212 where upd :: [(Name, SynMatch)] -> PDo -> PDo

213 upd ns (DoExp fc t) = DoExp fc (update ns t)

214 upd ns (DoBind fc n nfc t) = DoBind fc n nfc (update ns t)

215 upd ns (DoLet fc n nfc ty t) = DoLet fc n nfc (update ns ty) (update ns t)

216 upd ns (DoBindP fc i t ts)

217 = DoBindP fc (update ns i) (update ns t)

218 (map (\(l,r) -> (update ns l, update ns r)) ts)

219 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)

220 update ns (PIdiom fc t) = PIdiom fc $ update ns t

221 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)

222 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs

223 update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs

224 update ns (PDisamb nsps t) = PDisamb nsps $ update ns t

225 update ns (PUnifyLog t) = PUnifyLog $ update ns t

226 update ns (PNoImplicits t) = PNoImplicits $ update ns t

227 update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)

228 update ns (PUnquote t) = PUnquote $ update ns t

229 update ns (PQuoteName n res fc) = let (n', fc') = (updateB ns (n, fc))

230 in PQuoteName n' res fc'

231 update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp

232 update ns (PConstSugar fc t) = PConstSugar fc $ update ns t

233 -- PConstSugar probably can't contain anything substitutable, but it's hard to track

234 update ns t = t

235

236 updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic

237 -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms

238 updTactic ns (Intro ns') = Intro $ map (fst . updateB ns . (, NoFC)) ns'

239 updTactic ns (Focus n) = Focus . fst $ updateB ns (n, NoFC)

240 updTactic ns (Refine n bs) = Refine (fst $ updateB ns (n, NoFC)) bs

241 updTactic ns (Claim n t) = Claim (fst $ updateB ns (n, NoFC)) (update ns t)

242 updTactic ns (MatchRefine n) = MatchRefine (fst $ updateB ns (n, NoFC))

243 updTactic ns (LetTac n t) = LetTac (fst $ updateB ns (n, NoFC)) (update ns t)

244 updTactic ns (LetTacTy n ty tm) = LetTacTy (fst $ updateB ns (n, NoFC)) (update ns ty) (update ns tm)

245 updTactic ns (ProofSearch rec prover depth top psns hints) = ProofSearch rec prover depth

246 (fmap (fst . updateB ns . (, NoFC)) top) (map (fst . updateB ns . (, NoFC)) psns) (map (fst . updateB ns . (, NoFC)) hints)

247 updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)

248 updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)

249 updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac

250 updTactic ns (TDocStr (Left n)) = TDocStr . Left . fst $ updateB ns (n, NoFC)

251 updTactic ns t = fmap (update ns) t

252

253 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

254 updTacImp _ x = x

255

256 dropn :: Name -> [(Name, a)] -> [(Name, a)]

257 dropn n [] = []

258 dropn n ((x,t) : xs) | n == x = xs

259 | otherwise = (x,t):dropn n xs

260

261

262{- | Parses a (normal) built-in expression

263@

264InternalExpr ::=

265 UnifyLog

266 | RecordType

267 | SimpleExpr

268 | Lambda

269 | QuoteGoal

270 | Let

271 | If

272 | RewriteTerm

273 | CaseExpr

274 | DoBlock

275 | App

276 ;

277@

278-}

279internalExpr :: SyntaxInfo -> IdrisParser PTerm

280internalExpr syn =

281 unifyLog syn

282 <|> runElab syn

283 <|> disamb syn

284 <|> noImplicits syn

285 <|> recordType syn

286 <|> if_ syn

287 <|> lambda syn

288 <|> quoteGoal syn

289 <|> let_ syn

290 <|> rewriteTerm syn

291 <|> doBlock syn

292 <|> caseExpr syn

293 <|> app syn

294 <?> "expression"

295

296{- | Parses the "impossible" keyword

297@

298Impossible ::= 'impossible'

299@

300-}

301impossible :: IdrisParser PTerm

302impossible = do fc <- reservedFC "impossible"

303 highlightP fc AnnKeyword

304 return PImpossible

305

306{- | Parses a case expression

307@

308CaseExpr ::=

309 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;

310@

311-}

312caseExpr :: SyntaxInfo -> IdrisParser PTerm

313caseExpr syn = do kw1 <- reservedFC "case"; fc <- getFC

314 scr <- expr syn; kw2 <- reservedFC "of";

315 opts <- indentedBlock1 (caseOption syn)

316 highlightP kw1 AnnKeyword

317 highlightP kw2 AnnKeyword

318 return (PCase fc scr opts)

319 <?> "case expression"

320

321{- | Parses a case in a case expression

322@

323CaseOption ::=

324 Expr (Impossible | '=>' Expr) Terminator

325 ;

326@

327-}

328caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

329caseOption syn = do lhs <- expr (syn { inPattern = True })

330 r <- impossible <|> symbol "=>" *> expr syn

331 return (lhs, r)

332 <?> "case option"

333

334warnTacticDeprecation :: FC -> IdrisParser ()

335warnTacticDeprecation fc =

336 parserWarning fc (Just NoOldTacticDeprecationWarnings) (Msg "This style of tactic proof is deprecated. See %runElab for the replacement.")

337

338{- | Parses a proof block

339@

340ProofExpr ::=

341 'proof' OpenBlock Tactic'* CloseBlock

342 ;

343@

344-}

345proofExpr :: SyntaxInfo -> IdrisParser PTerm

346proofExpr syn = do kw <- reservedFC "proof"

347 ts <- indentedBlock1 (tactic syn)

348 highlightP kw AnnKeyword

349 warnTacticDeprecation kw

350 return $ PProof ts

351 <?> "proof block"

352

353{- | Parses a tactics block

354@

355TacticsExpr :=

356 'tactics' OpenBlock Tactic'* CloseBlock

357;

358@

359-}

360tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

361tacticsExpr syn = do kw <- reservedFC "tactics"

362 ts <- indentedBlock1 (tactic syn)

363 highlightP kw AnnKeyword

364 warnTacticDeprecation kw

365 return $ PTactics ts

366 <?> "tactics block"

367

368{- | Parses a simple expression

369@

370SimpleExpr ::=

371 {- External (User-defined) Simple Expression -}

372 | '?' Name

373 | % 'instance'

374 | 'Refl' ('{' Expr '}')?

375 | ProofExpr

376 | TacticsExpr

377 | FnName

378 | Idiom

379 | List

380 | Alt

381 | Bracketed

382 | Constant

383 | Type

384 | 'Void'

385 | Quasiquote

386 | NameQuote

387 | Unquote

388 | '_'

389 ;

390@

391-}

392simpleExpr :: SyntaxInfo -> IdrisParser PTerm

393simpleExpr syn =

394 try (simpleExternalExpr syn)

395 <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

396 return (PMetavar (FC f (l, c-1) end) x)

397 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

398 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

399 <|> proofExpr syn

400 <|> tacticsExpr syn

401 <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

402 <|> do reserved "AnyType"; return $ PUniverse AllTypes

403 <|> PType <$> reservedFC "Type"

404 <|> do reserved "UniqueType"; return $ PUniverse UniqueType

405 <|> do reserved "NullType"; return $ PUniverse NullType

406 <|> do (c, cfc) <- constant

407 fc <- getFC

408 return (modifyConst syn fc (PConstant cfc c))

409 <|> do symbol "'"; fc <- getFC; str <- fst <$> name

410 return (PApp fc (PRef fc [] (sUN "Symbol_"))

411 [pexp (PConstant NoFC (Str (show str)))])

412 <|> do (x, fc) <- fnName

413 if inPattern syn

414 then option (PRef fc [fc] x)

415 (do reservedOp "@"

416 s <- simpleExpr syn

417 fcIn <- getFC

418 return (PAs fcIn x s))

419 else return (PRef fc [fc] x)

420 <|> idiom syn

421 <|> listExpr syn

422 <|> alt syn

423 <|> do reservedOp "!"

424 s <- simpleExpr syn

425 fc <- getFC

426 return (PAppBind fc s [])

427 <|> bracketed (disallowImp syn)

428 <|> quasiquote syn

429 <|> namequote syn

430 <|> unquote syn

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

432 <?> "expression"

433

434{- |Parses an expression in braces

435@

436Bracketed ::= '(' Bracketed'

437@

438 -}

439bracketed :: SyntaxInfo -> IdrisParser PTerm

440bracketed syn = do (FC fn (sl, sc) _) <- getFC

441 lchar '(' <?> "parenthesized expression"

442 bracketed' (FC fn (sl, sc) (sl, sc+1)) syn

443{- |Parses the rest of an expression in braces

444@

445Bracketed' ::=

446 ')'

447 | Expr ')'

448 | ExprList ')'

449 | Expr '**' Expr ')'

450 | Operator Expr ')'

451 | Expr Operator ')'

452 | Name ':' Expr '**' Expr ')'

453 ;

454@

455-}

456bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm

457bracketed' open syn =

458 do (FC f start (l, c)) <- getFC

459 lchar ')'

460 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

461 <|> try (do (ln, lnfc) <- name

462 colonFC <- lcharFC ':'

463 lty <- expr syn

464 starsFC <- reservedOpFC "**"

465 fc <- getFC

466 r <- expr syn

467 close <- lcharFC ')'

468 return (PDPair fc [open, colonFC, starsFC, close] TypeOrTerm (PRef lnfc [] ln) lty r))

469 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

470 -- No prefix operators! (bit of a hack here...)

471 if (o == "-" || o == "!")

472 then fail "minus not allowed in section"

473 else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

474 (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),

475 pexp e]))

476 <|> try (do l <- simpleExpr syn

477 op <- option Nothing (do o <- operator

478 lchar ')'

479 return (Just o))

480 fc0 <- getFC

481 case op of

482 Nothing -> bracketedExpr syn open l

483 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder

484 (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,

485 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

486 <|> do l <- expr syn

487 bracketedExpr syn open l

488

489-- | Parse the contents of parentheses, after an expression has been parsed.

490bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm

491bracketedExpr syn openParenFC e =

492 do lchar ')'; return e

493 <|> do exprs <- many (do comma <- lcharFC ','

494 r <- expr syn

495 return (r, comma))

496 closeParenFC <- lcharFC ')'

497 let hilite = [openParenFC, closeParenFC] ++ map snd exprs

498 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)

499 <|> do starsFC <- reservedOpFC "**"

500 r <- expr syn

501 closeParenFC <- lcharFC ')'

502 return (PDPair starsFC [openParenFC, starsFC, closeParenFC] TypeOrTerm e Placeholder r)

503 <?> "end of bracketed expression"

504 where mergePairs :: [(PTerm, FC)] -> PTerm

505 mergePairs [(t, fc)] = t

506 mergePairs ((t, fc):rs) = PPair fc [] TypeOrTerm t (mergePairs rs)

507

508-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a

509-- big integer, otherwise try fromInteger and the constants as alternatives.

510-- a better solution would be to fix fromInteger to work with Integer, as the

511-- name suggests, rather than Int

512{-| Finds optimal type for integer constant -}

513modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

514modifyConst syn fc (PConstant inFC (BI x))

515 | not (inPattern syn)

516 = PConstSugar inFC $ -- wrap in original location for highlighting

517 PAlternative [] FirstSuccess

518 (PApp fc (PRef fc [] (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

519 : consts)

520 | otherwise = PConstSugar inFC $

521 PAlternative [] FirstSuccess consts

522 where

523 consts = [ PConstant inFC (BI x)

524 , PConstant inFC (I (fromInteger x))

525 , PConstant inFC (B8 (fromInteger x))

526 , PConstant inFC (B16 (fromInteger x))

527 , PConstant inFC (B32 (fromInteger x))

528 , PConstant inFC (B64 (fromInteger x))

529 ]

530modifyConst syn fc x = x

531

532{- | Parses an alternative expression

533@

534 Alt ::= '(|' Expr_List '|)';

535

536 Expr_List ::=

537 Expr'

538 | Expr' ',' Expr_List

539 ;

540@

541-}

542alt :: SyntaxInfo -> IdrisParser PTerm

543alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"

544 return (PAlternative [] FirstSuccess alts)

545

546{- | Parses a possibly hidden simple expression

547@

548HSimpleExpr ::=

549 '.' SimpleExpr

550 | SimpleExpr

551 ;

552@

553-}

554hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

555hsimpleExpr syn =

556 do lchar '.'

557 e <- simpleExpr syn

558 return $ PHidden e

559 <|> simpleExpr syn

560 <?> "expression"

561

562{- | Parses a unification log expression

563UnifyLog ::=

564 '%' 'unifyLog' SimpleExpr

565 ;

566-}

567unifyLog :: SyntaxInfo -> IdrisParser PTerm

568unifyLog syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "unifyLog")

569 tm <- simpleExpr syn

570 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

571 return (PUnifyLog tm)

572 <?> "unification log expression"

573

574{- | Parses a new-style tactics expression

575RunTactics ::=

576 '%' 'runElab' SimpleExpr

577 ;

578-}

579runElab :: SyntaxInfo -> IdrisParser PTerm

580runElab syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "runElab")

581 fc <- getFC

582 tm <- simpleExpr syn

583 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

584 return $ PRunElab fc tm (syn_namespace syn)

585 <?> "new-style tactics expression"

586

587{- | Parses a disambiguation expression

588Disamb ::=

589 'with' NameList Expr

590 ;

591-}

592disamb :: SyntaxInfo -> IdrisParser PTerm

593disamb syn = do kw <- reservedFC "with"

594 ns <- sepBy1 (fst <$> name) (lchar ',')

595 tm <- expr' syn

596 highlightP kw AnnKeyword

597 return (PDisamb (map tons ns) tm)

598 <?> "namespace disambiguation expression"

599 where tons (NS n s) = txt (show n) : s

600 tons n = [txt (show n)]

601{- | Parses a no implicits expression

602@

603NoImplicits ::=

604 '%' 'noImplicits' SimpleExpr

605 ;

606@

607-}

608noImplicits :: SyntaxInfo -> IdrisParser PTerm

609noImplicits syn = do try (lchar '%' *> reserved "noImplicits")

610 tm <- simpleExpr syn

611 return (PNoImplicits tm)

612 <?> "no implicits expression"

613

614{- | Parses a function application expression

615@

616App ::=

617 'mkForeign' Arg Arg*

618 | MatchApp

619 | SimpleExpr Arg*

620 ;

621MatchApp ::=

622 SimpleExpr '<==' FnName

623 ;

624@

625-}

626app :: SyntaxInfo -> IdrisParser PTerm

627app syn = do f <- simpleExpr syn

628 (do try $ reservedOp "<=="

629 fc <- getFC

630 ff <- fst <$> fnName

631 return (PLet fc (sMN 0 "match") NoFC

632 f

633 (PMatchApp fc ff)

634 (PRef fc [] (sMN 0 "match")))

635 <?> "matching application expression") <|> (do

636 fc <- getFC

637 i <- get

638 args <- many (do notEndApp; arg syn)

639 case args of

640 [] -> return f

641 _ -> return (flattenFromInt fc f args))

642 <?> "function application"

643 where

644 -- bit of a hack to deal with the situation where we're applying a

645 -- literal to an argument, which we may want for obscure applications

646 -- of fromInteger, and this will help disambiguate better.

647 -- We know, at least, it won't be one of the constants!

648 flattenFromInt fc (PAlternative _ x alts) args

649 | Just i <- getFromInt alts

650 = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)

651 flattenFromInt fc f args = PApp fc f args

652

653 getFromInt ((PApp _ (PRef _ _ n) [a]) : _) | n == sUN "fromInteger" = Just a

654 getFromInt (_ : xs) = getFromInt xs

655 getFromInt _ = Nothing

656

657{-| Parses a function argument

658@

659Arg ::=

660 ImplicitArg

661 | ConstraintArg

662 | SimpleExpr

663 ;

664@

665-}

666arg :: SyntaxInfo -> IdrisParser PArg

667arg syn = implicitArg syn

668 <|> constraintArg syn

669 <|> do e <- simpleExpr syn

670 return (pexp e)

671 <?> "function argument"

672

673{-| Parses an implicit function argument

674@

675ImplicitArg ::=

676 '{' Name ('=' Expr)? '}'

677 ;

678@

679-}

680implicitArg :: SyntaxInfo -> IdrisParser PArg

681implicitArg syn = do lchar '{'

682 (n, nfc) <- name

683 fc <- getFC

684 v <- option (PRef nfc [nfc] n) (do lchar '='

685 expr syn)

686 lchar '}'

687 return (pimp n v True)

688 <?> "implicit function argument"

689

690{-| Parses a constraint argument (for selecting a named type class instance)

691

692> ConstraintArg ::=

693> '@{' Expr '}'

694> ;

695

696-}

697constraintArg :: SyntaxInfo -> IdrisParser PArg

698constraintArg syn = do symbol "@{"

699 e <- expr syn

700 symbol "}"

701 return (pconst e)

702 <?> "constraint argument"

703

704{-| Parses a quasiquote expression (for building reflected terms using the elaborator)

705

706> Quasiquote ::= '`(' Expr ')'

707

708-}

709quasiquote :: SyntaxInfo -> IdrisParser PTerm

710quasiquote syn = do startFC <- symbolFC "`("

711 e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,

712 inPattern = False }

713 g <- optional $

714 do fc <- symbolFC ":"

715 ty <- expr syn { inPattern = False } -- don't allow antiquotes

716 return (ty, fc)

717 endFC <- symbolFC ")"

718 mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword), (spanFC startFC endFC, AnnQuasiquote)]

719 case g of

720 Just (_, fc) -> highlightP fc AnnKeyword

721 _ -> return ()

722 return $ PQuasiquote e (fst <$> g)

723 <?> "quasiquotation"

724

725{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

726

727> Unquote ::= ',' Expr

728

729-}

730unquote :: SyntaxInfo -> IdrisParser PTerm

731unquote syn = do guard (syn_in_quasiquote syn > 0)

732 startFC <- symbolFC "~"

733 e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }

734 endFC <- getFC

735 highlightP startFC AnnKeyword

736 highlightP (spanFC startFC endFC) AnnAntiquote

737 return $ PUnquote e

738 <?> "unquotation"

739

740{-| Parses a quotation of a name (for using the elaborator to resolve boring details)

741

742> NameQuote ::= '`{' Name '}'

743

744-}

745namequote :: SyntaxInfo -> IdrisParser PTerm

746namequote syn = do (startFC, res) <-

747 try (do fc <- symbolFC "`{{"

748 return (fc, False)) <|>

749 (do fc <- symbolFC "`{"

750 return (fc, True))

751 (n, nfc) <- fnName

752 endFC <- if res then symbolFC "}" else symbolFC "}}"

753 mapM_ (uncurry highlightP)

754 [ (startFC, AnnKeyword)

755 , (endFC, AnnKeyword)

756 , (spanFC startFC endFC, AnnQuasiquote)

757 ]

758 return $ PQuoteName n res nfc

759 <?> "quoted name"

760

761

762{-| Parses a record field setter expression

763@

764RecordType ::=

765 'record' '{' FieldTypeList '}';

766@

767@

768FieldTypeList ::=

769 FieldType

770 | FieldType ',' FieldTypeList

771 ;

772@

773@

774FieldType ::=

775 FnName '=' Expr

776 ;

777@

778-}

779recordType :: SyntaxInfo -> IdrisParser PTerm

780recordType syn =

781 do kw <- reservedFC "record"

782 lchar '{'

783 fgs <- fieldGetOrSet

784 lchar '}'

785 fc <- getFC

786 rec <- optional (simpleExpr syn)

787 highlightP kw AnnKeyword

788 case fgs of

789 Left fields ->

790 case rec of

791 Nothing ->

792 return (PLam fc (sMN 0 "fldx") NoFC Placeholder

793 (applyAll fc fields (PRef fc [] (sMN 0 "fldx"))))

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

795 Right fields ->

796 case rec of

797 Nothing ->

798 return (PLam fc (sMN 0 "fldx") NoFC Placeholder

799 (getAll fc (reverse fields)

800 (PRef fc [] (sMN 0 "fldx"))))

801 Just v -> return (getAll fc (reverse fields) v)

802

803 <?> "record setting expression"

804 where fieldSet :: IdrisParser ([Name], PTerm)

805 fieldSet = do ns <- fieldGet

806 lchar '='

807 e <- expr syn

808 return (ns, e)

809 <?> "field setter"

810

811 fieldGet :: IdrisParser [Name]

812 fieldGet = sepBy1 (fst <$> fnName) (symbol "->")

813

814 fieldGetOrSet :: IdrisParser (Either [([Name], PTerm)] [Name])

815 fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',')

816 return (Left fs))

817 <|> do f <- fieldGet

818 return (Right f)

819

820 applyAll :: FC -> [([Name], PTerm)] -> PTerm -> PTerm

821 applyAll fc [] x = x

822 applyAll fc ((ns, e) : es) x

823 = applyAll fc es (doUpdate fc ns e x)

824

825 doUpdate fc [n] e get

826 = PApp fc (PRef fc [] (mkType n)) [pexp e, pexp get]

827 doUpdate fc (n : ns) e get

828 = PApp fc (PRef fc [] (mkType n))

829 [pexp (doUpdate fc ns e (PApp fc (PRef fc [] n) [pexp get])),

830 pexp get]

831

832 getAll :: FC -> [Name] -> PTerm -> PTerm

833 getAll fc [n] e = PApp fc (PRef fc [] n) [pexp e]

834 getAll fc (n:ns) e = PApp fc (PRef fc [] n) [pexp (getAll fc ns e)]

835

836

837-- | Creates setters for record types on necessary functions

838mkType :: Name -> Name

839mkType (UN n) = sUN ("set_" ++ str n)

840mkType (MN 0 n) = sMN 0 ("set_" ++ str n)

841mkType (NS n s) = NS (mkType n) s

842

843{- | Parses a type signature

844@

845TypeSig ::=

846 ':' Expr

847 ;

848@

849@

850TypeExpr ::= ConstraintList? Expr;

851@

852 -}

853typeExpr :: SyntaxInfo -> IdrisParser PTerm

854typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

855 sc <- expr syn

856 return (bindList (PPi constraint) cs sc)

857 <?> "type signature"

858

859{- | Parses a lambda expression

860@

861Lambda ::=

862 '\\' TypeOptDeclList LambdaTail

863 | '\\' SimpleExprList LambdaTail

864 ;

865@

866@

867SimpleExprList ::=

868 SimpleExpr

869 | SimpleExpr ',' SimpleExprList

870 ;

871@

872@

873LambdaTail ::=

874 Impossible

875 | '=>' Expr

876@

877-}

878lambda :: SyntaxInfo -> IdrisParser PTerm

879lambda syn = do lchar '\\' <?> "lambda expression"

880 ((do xt <- try $ tyOptDeclList syn

881 fc <- getFC

882 sc <- lambdaTail

883 return (bindList (PLam fc) xt sc))

884 <|>

885 (do ps <- sepBy (do fc <- getFC

886 e <- simpleExpr (syn { inPattern = True })

887 return (fc, e))

888 (lchar ',')

889 sc <- lambdaTail

890 return (pmList (zip [0..] ps) sc)))

891 <?> "lambda expression"

892 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

893 pmList [] sc = sc

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

895 = PLam fc (sMN i "lamp") NoFC Placeholder

896 (PCase fc (PRef fc [] (sMN i "lamp"))

897 [(x, pmList xs sc)])

898 lambdaTail :: IdrisParser PTerm

899 lambdaTail = impossible <|> symbol "=>" *> expr syn

900

901{- | Parses a term rewrite expression

902@

903RewriteTerm ::=

904 'rewrite' Expr ('==>' Expr)? 'in' Expr

905 ;

906@

907-}

908rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

909rewriteTerm syn = do kw <- reservedFC "rewrite"

910 fc <- getFC

911 prf <- expr syn

912 giving <- optional (do symbol "==>"; expr' syn)

913 kw' <- reservedFC "in"; sc <- expr syn

914 highlightP kw AnnKeyword

915 highlightP kw' AnnKeyword

916 return (PRewrite fc

917 (PApp fc (PRef fc [] (sUN "sym")) [pexp prf]) sc

918 giving)

919 <?> "term rewrite expression"

920

921{- |Parses a let binding

922@

923Let ::=

924 'let' Name TypeSig'? '=' Expr 'in' Expr

925| 'let' Expr' '=' Expr' 'in' Expr

926

927TypeSig' ::=

928 ':' Expr'

929 ;

930@

931 -}

932let_ :: SyntaxInfo -> IdrisParser PTerm

933let_ syn = try (do kw <- reservedFC "let"

934 ls <- indentedBlock (let_binding syn)

935 kw' <- reservedFC "in"; sc <- expr syn

936 highlightP kw AnnKeyword; highlightP kw' AnnKeyword

937 return (buildLets ls sc))

938 <?> "let binding"

939 where buildLets [] sc = sc

940 buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc

941 = PLet fc n nfc ty v (buildLets ls sc)

942 buildLets ((fc, pat, ty, v, alts) : ls) sc

943 = PCase fc v ((pat, buildLets ls sc) : alts)

944

945let_binding syn = do fc <- getFC;

946 pat <- expr' (syn { inPattern = True })

947 ty <- option Placeholder (do lchar ':'; expr' syn)

948 lchar '='

949 v <- expr syn

950 ts <- option [] (do lchar '|'

951 sepBy1 (do_alt syn) (lchar '|'))

952 return (fc,pat,ty,v,ts)

953

954{- | Parses a conditional expression

955@

956If ::= 'if' Expr 'then' Expr 'else' Expr

957@

958

959-}

960if_ :: SyntaxInfo -> IdrisParser PTerm

961if_ syn = (do ifFC <- reservedFC "if"

962 fc <- getFC

963 c <- expr syn

964 thenFC <- reservedFC "then"

965 t <- expr syn

966 elseFC <- reservedFC "else"

967 f <- expr syn

968 mapM_ (flip highlightP AnnKeyword) [ifFC, thenFC, elseFC]

969 return (PIfThenElse fc c t f))

970 <?> "conditional expression"

971

972

973{- | Parses a quote goal

974

975@

976QuoteGoal ::=

977 'quoteGoal' Name 'by' Expr 'in' Expr

978 ;

979@

980 -}

981quoteGoal :: SyntaxInfo -> IdrisParser PTerm

982quoteGoal syn = do kw1 <- reservedFC "quoteGoal"; n <- fst <$> name;

983 kw2 <- reservedFC "by"

984 r <- expr syn

985 kw3 <- reservedFC "in"

986 fc <- getFC

987 sc <- expr syn

988 mapM_ (flip highlightP AnnKeyword) [kw1, kw2, kw3]

989 return (PGoal fc r n sc)

990 <?> "quote goal expression"

991

992{- | Parses a dependent type signature

993

994@

995Pi ::= PiOpts Static? Pi'

996@

997

998@

999Pi' ::=

1000 OpExpr ('->' Pi)?

1001 | '(' TypeDeclList ')' '->' Pi

1002 | '{' TypeDeclList '}' '->' Pi

1003 | '{' 'auto' TypeDeclList '}' '->' Pi

1004 | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi

1005 ;

1006@

1007 -}

1008

1009bindsymbol opts st syn

1010 = do symbol "->"

1011 return (Exp opts st False)

1012

1013explicitPi opts st syn

1014 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

1015 binder <- bindsymbol opts st syn

1016 sc <- expr syn

1017 return (bindList (PPi binder) xt sc)

1018

1019autoImplicit opts st syn

1020 = do kw <- reservedFC "auto"

1021 when (st == Static) $ fail "auto implicits can not be static"

1022 xt <- typeDeclList syn

1023 lchar '}'

1024 symbol "->"

1025 sc <- expr syn

1026 highlightP kw AnnKeyword

1027 return (bindList (PPi

1028 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)

1029

1030defaultImplicit opts st syn = do

1031 kw <- reservedFC "default"

1032 when (st == Static) $ fail "default implicits can not be static"

1033 ist <- get

1034 script' <- simpleExpr syn

1035 let script = debindApp syn . desugar syn ist $ script'

1036 xt <- typeDeclList syn

1037 lchar '}'

1038 symbol "->"

1039 sc <- expr syn

1040 highlightP kw AnnKeyword

1041 return (bindList (PPi (TacImp [] Dynamic script)) xt sc)

1042

1043normalImplicit opts st syn = do

1044 xt <- typeDeclList syn <* lchar '}'

1045 symbol "->"

1046 cs <- constraintList syn

1047 sc <- expr syn

1048 let (im,cl)

1049 = if implicitAllowed syn

1050 then (Imp opts st False (Just (Impl False True)),

1051 constraint)

1052 else (Imp opts st False (Just (Impl False False)),

1053 Imp opts st False (Just (Impl True False)))

1054 return (bindList (PPi im) xt

1055 (bindList (PPi cl) cs sc))

1056

1057implicitPi opts st syn =

1058 autoImplicit opts st syn

1059 <|> defaultImplicit opts st syn

1060 <|> normalImplicit opts st syn

1061

1062unboundPi opts st syn = do

1063 x <- opExpr syn

1064 (do binder <- bindsymbol opts st syn

1065 sc <- expr syn

1066 return (PPi binder (sUN "__pi_arg") NoFC x sc))

1067 <|> return x

1068

1069pi :: SyntaxInfo -> IdrisParser PTerm

1070pi syn =

1071 do opts <- piOpts syn

1072 st <- static

1073 explicitPi opts st syn

1074 <|> try (do lchar '{'; implicitPi opts st syn)

1075 <|> unboundPi opts st syn

1076 <?> "dependent type signature"

1077

1078{- | Parses Possible Options for Pi Expressions

1079@

1080 PiOpts ::= '.'?

1081@

1082-}

1083piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

1084piOpts syn | implicitAllowed syn =

1085 lchar '.' *> return [InaccessibleArg]

1086 <|> return []

1087piOpts syn = return []

1088

1089{- | Parses a type constraint list

1090

1091@

1092ConstraintList ::=

1093 '(' Expr_List ')' '=>'

1094 | Expr '=>'

1095 ;

1096@

1097-}

1098constraintList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1099constraintList syn = try (constraintList1 syn)

1100 <|> return []

1101

1102constraintList1 :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1103constraintList1 syn = try (do lchar '('

1104 tys <- sepBy1 nexpr (lchar ',')

1105 lchar ')'

1106 reservedOp "=>"

1107 return tys)

1108 <|> try (do t <- opExpr (disallowImp syn)

1109 reservedOp "=>"

1110 return [(defname, NoFC, t)])

1111 <?> "type constraint list"

1112 where nexpr = try (do (n, fc) <- name; lchar ':'

1113 e <- expr syn

1114 return (n, fc, e))

1115 <|> do e <- expr syn

1116 return (defname, NoFC, e)

1117 defname = sMN 0 "constraint"

1118

1119{- | Parses a type declaration list

1120@

1121TypeDeclList ::=

1122 FunctionSignatureList

1123 | NameList TypeSig

1124 ;

1125@

1126

1127@

1128FunctionSignatureList ::=

1129 Name TypeSig

1130 | Name TypeSig ',' FunctionSignatureList

1131 ;

1132@

1133-}

1134typeDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1135typeDeclList syn = try (sepBy1 (do (x, xfc) <- fnName

1136 lchar ':'

1137 t <- typeExpr (disallowImp syn)

1138 return (x, xfc, t))

1139 (lchar ','))

1140 <|> do ns <- sepBy1 name (lchar ',')

1141 lchar ':'

1142 t <- typeExpr (disallowImp syn)

1143 return (map (\(x, xfc) -> (x, xfc, t)) ns)

1144 <?> "type declaration list"

1145

1146{- | Parses a type declaration list with optional parameters

1147@

1148TypeOptDeclList ::=

1149 NameOrPlaceholder TypeSig?

1150 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList

1151 ;

1152@

1153

1154@

1155NameOrPlaceHolder ::= Name | '_';

1156@

1157-}

1158tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1159tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder

1160 t <- option Placeholder (do lchar ':'

1161 expr syn)

1162 return (x, fc, t))

1163 (lchar ',')

1164 <?> "type declaration list"

1165 where nameOrPlaceholder :: IdrisParser (Name, FC)

1166 nameOrPlaceholder = fnName

1167 <|> do symbol "_"

1168 return (sMN 0 "underscore", NoFC)

1169 <?> "name or placeholder"

1170

1171{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]

1172@

1173ListExpr ::=

1174 '[' ']'

1175 | '[' Expr '|' DoList ']'

1176 | '[' ExprList ']'

1177;

1178@

1179@

1180DoList ::=

1181 Do

1182 | Do ',' DoList

1183 ;

1184@

1185@

1186ExprList ::=

1187 Expr

1188 | Expr ',' ExprList

1189 ;

1190@

1191 -}

1192listExpr :: SyntaxInfo -> IdrisParser PTerm

1193listExpr syn = do (FC f (l, c) _) <- getFC

1194 lchar '['; fc <- getFC;

1195 (try . token $ do (char ']' <?> "end of list expression")

1196 (FC _ _ (l', c')) <- getFC

1197 return (mkNil (FC f (l, c) (l', c'))))

1198 <|> (do x <- expr syn <?> "expression"

1199 (do try (lchar '|') <?> "list comprehension"

1200 qs <- sepBy1 (do_ syn) (lchar ',')

1201 lchar ']'

1202 return (PDoBlock (map addGuard qs ++

1203 [DoExp fc (PApp fc (PRef fc [] (sUN "return"))

1204 [pexp x])]))) <|>

1205 (do xs <- many (do (FC fn (sl, sc) _) <- getFC

1206 lchar ',' <?> "list element"

1207 let commaFC = FC fn (sl, sc) (sl, sc + 1)

1208 elt <- expr syn

1209 return (elt, commaFC))

1210 (FC fn (sl, sc) _) <- getFC

1211 lchar ']' <?> "end of list expression"

1212 let rbrackFC = FC fn (sl, sc) (sl, sc+1)

1213 return (mkList fc rbrackFC ((x, (FC f (l, c) (l, c+1))) : xs))))

1214 <?> "list expression"

1215 where

1216 mkNil :: FC -> PTerm

1217 mkNil fc = PRef fc [fc] (sUN "Nil")

1218 mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm

1219 mkList errFC nilFC [] = PRef nilFC [nilFC] (sUN "Nil")

1220 mkList errFC nilFC ((x, fc) : xs) = PApp errFC (PRef fc [fc] (sUN "::")) [pexp x, pexp (mkList errFC nilFC xs)]

1221 addGuard :: PDo -> PDo

1222 addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc [] (sUN "guard"))

1223 [pexp e])

1224 addGuard x = x

1225

1226{- | Parses a do-block

1227@

1228Do' ::= Do KeepTerminator;

1229@

1230

1231@

1232DoBlock ::=

1233 'do' OpenBlock Do'+ CloseBlock

1234 ;

1235@

1236 -}

1237doBlock :: SyntaxInfo -> IdrisParser PTerm

1238doBlock syn

1239 = do kw <- reservedFC "do"

1240 ds <- indentedBlock1 (do_ syn)

1241 highlightP kw AnnKeyword

1242 return (PDoBlock ds)

1243 <?> "do block"

1244

1245{- | Parses an expression inside a do block

1246@

1247Do ::=

1248 'let' Name TypeSig'? '=' Expr

1249 | 'let' Expr' '=' Expr

1250 | Name '<-' Expr

1251 | Expr' '<-' Expr

1252 | Expr

1253 ;

1254@

1255-}

1256do_ :: SyntaxInfo -> IdrisParser PDo

1257do_ syn

1258 = try (do kw <- reservedFC "let"

1259 (i, ifc) <- name

1260 ty <- option Placeholder (do lchar ':'

1261 expr' syn)

1262 reservedOp "="

1263 fc <- getFC

1264 e <- expr syn

1265 highlightP kw AnnKeyword

1266 return (DoLet fc i ifc ty e))

1267 <|> try (do kw <- reservedFC "let"

1268 i <- expr' syn

1269 reservedOp "="

1270 fc <- getFC

1271 sc <- expr syn

1272 highlightP kw AnnKeyword

1273 return (DoLetP fc i sc))

1274 <|> try (do (i, ifc) <- name

1275 symbol "<-"

1276 fc <- getFC

1277 e <- expr syn;

1278 option (DoBind fc i ifc e)

1279 (do lchar '|'

1280 ts <- sepBy1 (do_alt syn) (lchar '|')

1281 return (DoBindP fc (PRef ifc [ifc] i) e ts)))

1282 <|> try (do i <- expr' syn

1283 symbol "<-"

1284 fc <- getFC

1285 e <- expr syn;

1286 option (DoBindP fc i e [])

1287 (do lchar '|'

1288 ts <- sepBy1 (do_alt syn) (lchar '|')

1289 return (DoBindP fc i e ts)))

1290 <|> do e <- expr syn

1291 fc <- getFC

1292 return (DoExp fc e)

1293 <?> "do block expression"

1294

1295do_alt syn = do l <- expr' syn

1296 option (Placeholder, l)

1297 (do symbol "=>"

1298 r <- expr' syn

1299 return (l, r))

1300

1301{- | Parses an expression in idiom brackets

1302@

1303Idiom ::= '[|' Expr '|]';

1304@

1305-}

1306idiom :: SyntaxInfo -> IdrisParser PTerm

1307idiom syn

1308 = do symbol "[|"

1309 fc <- getFC

1310 e <- expr syn

1311 symbol "|]"

1312 return (PIdiom fc e)

1313 <?> "expression in idiom brackets"

1314

1315{- |Parses a constant or literal expression

1316

1317@

1318Constant ::=

1319 'Integer'

1320 | 'Int'

1321 | 'Char'

1322 | 'Double'

1323 | 'String'

1324 | 'Bits8'

1325 | 'Bits16'

1326 | 'Bits32'

1327 | 'Bits64'

1328 | Float_t

1329 | Natural_t

1330 | VerbatimString_t

1331 | String_t

1332 | Char_t

1333 ;

1334@

1335-}

1336

1337constants :: [(String, Idris.Core.TT.Const)]

1338constants =

1339 [ ("Integer", AType (ATInt ITBig))

1340 , ("Int", AType (ATInt ITNative))

1341 , ("Char", AType (ATInt ITChar))

1342 , ("Double", AType ATFloat)

1343 , ("String", StrType)

1344 , ("prim__WorldType", WorldType)

1345 , ("prim__TheWorld", TheWorld)

1346 , ("Bits8", AType (ATInt (ITFixed IT8)))

1347 , ("Bits16", AType (ATInt (ITFixed IT16)))

1348 , ("Bits32", AType (ATInt (ITFixed IT32)))

1349 , ("Bits64", AType (ATInt (ITFixed IT64)))

1350 ]

1351

1352-- | Parse a constant and its source span

1353constant :: IdrisParser (Idris.Core.TT.Const, FC)

1354constant = choice [ do fc <- reservedFC name; return (ty, fc)

1355 | (name, ty) <- constants

1356 ]

1357 <|> do (f, fc) <- try float; return (Fl f, fc)

1358 <|> do (i, fc) <- natural; return (BI i, fc)

1359 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)

1360 <|> do (s, fc) <- stringLiteral; return (Str s, fc)

1361 <|> do (c, fc) <- try charLiteral; return (Ch c, fc) --Currently ambigous with symbols

1362 <?> "constant or literal"

1363

1364{- | Parses a verbatim multi-line string literal (triple-quoted)

1365

1366@

1367VerbatimString_t ::=

1368 '\"\"\"' ~'\"\"\"' '\"\"\"'

1369;

1370@

1371 -}

1372verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1373verbatimStringLiteral = token $ do (FC f start _) <- getFC

1374 try $ string "\"\"\""

1375 str <- manyTill anyChar $ try (string "\"\"\"")

1376 (FC _ _ end) <- getFC

1377 return (str, FC f start end)

1378

1379{- | Parses a static modifier

1380

1381@

1382Static ::=

1383 '[' static ']'

1384;

1385@

1386-}

1387static :: IdrisParser Static

1388static = do reserved "%static"; return Static

1389 <|> do reserved "[static]"

1390 fc <- getFC

1391 parserWarning fc Nothing (Msg "The use of [static] is deprecated, use %static instead.")

1392 return Static

1393 <|> return Dynamic

1394 <?> "static modifier"

1395

1396{- | Parses a tactic script

1397

1398@

1399Tactic ::= 'intro' NameList?

1400 | 'intros'

1401 | 'refine' Name Imp+

1402 | 'mrefine' Name

1403 | 'rewrite' Expr

1404 | 'induction' Expr

1405 | 'equiv' Expr

1406 | 'let' Name ':' Expr' '=' Expr

1407 | 'let' Name '=' Expr

1408 | 'focus' Name

1409 | 'exact' Expr

1410 | 'applyTactic' Expr

1411 | 'reflect' Expr

1412 | 'fill' Expr

1413 | 'try' Tactic '|' Tactic

1414 | '{' TacticSeq '}'

1415 | 'compute'

1416 | 'trivial'

1417 | 'solve'

1418 | 'attack'

1419 | 'state'

1420 | 'term'

1421 | 'undo'

1422 | 'qed'

1423 | 'abandon'

1424 | ':' 'q'

1425 ;

1426

1427Imp ::= '?' | '_';

1428

1429TacticSeq ::=

1430 Tactic ';' Tactic

1431 | Tactic ';' TacticSeq

1432 ;

1433@

1434-}

1435

1436-- | A specification of the arguments that tactics can take

1437data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

1438 | ExprTArg

1439 | AltsTArg

1440 | StringLitTArg

1441

1442-- The FIXMEs are Issue #1766 in the issue tracker.

1443-- https://github.com/idris-lang/Idris-dev/issues/1766

1444-- | A list of available tactics and their argument requirements

1445tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

1446tactics =

1447 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1448 do ns <- sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)

1449 , noArgs ["intros"] Intros

1450 , noArgs ["unfocus"] Unfocus

1451 , (["refine"], Just ExprTArg, const $

1452 do n <- spaced (fst <$> fnName)

1453 imps <- many imp

1454 return $ Refine n imps)

1455 , (["claim"], Nothing, \syn ->

1456 do n <- indentPropHolds gtProp *> (fst <$> name)

1457 goal <- indentPropHolds gtProp *> expr syn

1458 return $ Claim n goal)

1459 , (["mrefine"], Just ExprTArg, const $

1460 do n <- spaced (fst <$> fnName)

1461 return $ MatchRefine n)

1462 , expressionTactic ["rewrite"] Rewrite

1463 , expressionTactic ["case"] CaseTac

1464 , expressionTactic ["induction"] Induction

1465 , expressionTactic ["equiv"] Equiv

1466 , (["let"], Nothing, \syn -> -- FIXME syntax for let

1467 do n <- (indentPropHolds gtProp *> (fst <$> name))

1468 (do indentPropHolds gtProp *> lchar ':'

1469 ty <- indentPropHolds gtProp *> expr' syn

1470 indentPropHolds gtProp *> lchar '='

1471 t <- indentPropHolds gtProp *> expr syn

1472 i <- get

1473 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))

1474 <|> (do indentPropHolds gtProp *> lchar '='

1475 t <- indentPropHolds gtProp *> expr syn

1476 i <- get

1477 return $ LetTac n (desugar syn i t)))

1478

1479 , (["focus"], Just ExprTArg, const $

1480 do n <- spaced (fst <$> name)

1481 return $ Focus n)

1482 , expressionTactic ["exact"] Exact

1483 , expressionTactic ["applyTactic"] ApplyTactic

1484 , expressionTactic ["byReflection"] ByReflection

1485 , expressionTactic ["reflect"] Reflect

1486 , expressionTactic ["fill"] Fill

1487 , (["try"], Just AltsTArg, \syn ->

1488 do t <- spaced (tactic syn)

1489 lchar '|'

1490 t1 <- spaced (tactic syn)

1491 return $ Try t t1)

1492 , noArgs ["compute"] Compute

1493 , noArgs ["trivial"] Trivial

1494 , noArgs ["unify"] DoUnify

1495 , (["search"], Nothing, const $

1496 do depth <- option 10 $ fst <$> natural

1497 return (ProofSearch True True (fromInteger depth) Nothing [] []))

1498 , noArgs ["instance"] TCInstance

1499 , noArgs ["solve"] Solve

1500 , noArgs ["attack"] Attack

1501 , noArgs ["state", ":state"] ProofState

1502 , noArgs ["term", ":term"] ProofTerm

1503 , noArgs ["undo", ":undo"] Undo

1504 , noArgs ["qed", ":qed"] Qed

1505 , noArgs ["abandon", ":q"] Abandon

1506 , noArgs ["skip"] Skip

1507 , noArgs ["sourceLocation"] SourceFC

1508 , expressionTactic [":e", ":eval"] TEval

1509 , expressionTactic [":t", ":type"] TCheck

1510 , expressionTactic [":search"] TSearch

1511 , (["fail"], Just StringLitTArg, const $

1512 do msg <- fst <$> stringLiteral

1513 return $ TFail [Idris.Core.TT.TextPart msg])

1514 , ([":doc"], Just ExprTArg, const $

1515 do whiteSpace

1516 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1517 eof

1518 return (TDocStr doc))

1519 ]

1520 where

1521 expressionTactic names tactic = (names, Just ExprTArg, \syn ->

1522 do t <- spaced (expr syn)

1523 i <- get

1524 return $ tactic (desugar syn i t))

1525 noArgs names tactic = (names, Nothing, const (return tactic))

1526 spaced parser = indentPropHolds gtProp *> parser

1527 imp :: IdrisParser Bool

1528 imp = do lchar '?'; return False

1529 <|> do lchar '_'; return True

1530

1531

1532tactic :: SyntaxInfo -> IdrisParser PTactic

1533tactic syn = choice [ do choice (map reserved names); parser syn

1534 | (names, _, parser) <- tactics ]

1535 <|> do lchar '{'

1536 t <- tactic syn;

1537 lchar ';';

1538 ts <- sepBy1 (tactic syn) (lchar ';')

1539 lchar '}'

1540 return $ TSeq t (mergeSeq ts)

1541 <|> ((lchar ':' >> empty) <?> "prover command")

1542 <?> "tactic"

1543 where

1544 mergeSeq :: [PTactic] -> PTactic

1545 mergeSeq [t] = t

1546 mergeSeq (t:ts) = TSeq t (mergeSeq ts)

1547

1548-- | Parses a tactic as a whole

1549fullTactic :: SyntaxInfo -> IdrisParser PTactic

1550fullTactic syn = do t <- tactic syn

1551 eof

1552 return t