src/Idris/Elab/Term.hs · Idris-dev

git.iko.soy/Idris-dev

on master help sign in

Idris-dev/src/Idris/Elab/Term.hs

2788 lines 130 kB history raw

1{-|

2Module : Idris.Elab.Term

3Description : Code to elaborate terms.

5License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}

9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10module Idris.Elab.Term where

12import Idris.AbsSyntax

13import Idris.Core.CaseTree (SC'(STerm), findCalls)

14import Idris.Core.Elaborate hiding (Tactic(..))

15import Idris.Core.Evaluate

16import Idris.Core.ProofTerm (getProofTerm)

17import Idris.Core.TT

18import Idris.Core.Typecheck (check, converts, isType, recheck)

19import Idris.Core.Unify

20import Idris.Core.WHNF (whnf)

21import Idris.Coverage (genClauses, recoverableCoverage)

22import Idris.Delaborate

23import Idris.Elab.Quasiquote (extractUnquotes)

24import Idris.Elab.Rewrite

25import Idris.Elab.Utils

26import Idris.Error

27import Idris.ErrReverse (errReverse)

28import Idris.Options

29import Idris.ProofSearch

30import Idris.Reflection

31import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)

33import Control.Applicative ((<$>))

34import Control.Monad

35import Control.Monad.State.Strict

36import Data.Foldable (for_)

37import Data.List

38import qualified Data.Map as M

39import Data.Maybe (fromMaybe, mapMaybe, maybeToList)

40import qualified Data.Set as S

41import Debug.Trace

43data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS

44 deriving Eq

47data ElabResult = ElabResult {

48 -- | The term resulting from elaboration

49 resultTerm :: Term

50 -- | Information about new metavariables

51 , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]

52 -- | Deferred declarations as the meaning of case blocks

53 , resultCaseDecls :: [PDecl]

54 -- | The potentially extended context from new definitions

55 , resultContext :: Context

56 -- | Meta-info about the new type declarations

57 , resultTyDecls :: [RDeclInstructions]

58 -- | Saved highlights from elaboration

59 , resultHighlighting :: S.Set (FC', OutputAnnotation)

60 -- | The new global name counter

61 , resultName :: Int

62 }

66-- | Using the elaborator, convert a term in raw syntax to a fully

67-- elaborated, typechecked term.

68--

69-- If building a pattern match, we convert undeclared variables from

70-- holes to pattern bindings.

71--

72-- Also find deferred names in the term and their types

73build :: IState

74 -> ElabInfo

75 -> ElabMode

76 -> FnOpts

77 -> Name

78 -> PTerm

79 -> ElabD ElabResult

80build ist info emode opts fn tm

81 = do elab ist info emode opts fn tm

82 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

83 [TIPartial] -> True

84 _ -> False

86 hs <- get_holes

87 ivs <- get_implementations

88 ptm <- get_term

89 -- Resolve remaining interfaces. Two passes - first to get the

90 -- default Num implementations, second to clean up the rest

91 when (not pattern) $

92 mapM_ (\n -> when (n `elem` hs) $

93 do focus n

94 g <- goal

95 try (resolveTC' True True 10 g fn ist)

96 (movelast n)) ivs

97 ivs <- get_implementations

98 hs <- get_holes

99 when (not pattern) $

100 mapM_ (\n -> when (n `elem` hs) $

101 do focus n

102 g <- goal

103 ptm <- get_term

104 resolveTC' True True 10 g fn ist) ivs

105

106 when (not pattern) $ solveAutos ist fn False

107

108 tm <- get_term

109 ctxt <- get_context

110 probs <- get_probs

111 u <- getUnifyLog

112 hs <- get_holes

113

114 when (not pattern) $

115 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++

116 "Remaining problems:\n" ++ qshow probs) $

117 do unify_all; matchProblems True; unifyProblems

118

119 when (not pattern) $ solveAutos ist fn True

120

121 probs <- get_probs

122 case probs of

123 [] -> return ()

124 ((_,_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ qshow probs ++ "\nin\n" ++ show tm) $

125 if inf then return ()

126 else lift (Error e)

127

128 when tydecl (do mkPat

129 update_term liftPats

130 update_term orderPats)

131 EState is _ impls highlights _ _ <- getAux

132 tt <- get_term

133 ctxt <- get_context

134 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

135 log <- getLog

136 g_nextname <- get_global_nextname

137 if log /= ""

138 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

139 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

140 where pattern = emode == ELHS || emode == EImpossible

141 tydecl = emode == ETyDecl

142

143 mkPat = do hs <- get_holes

144 tm <- get_term

145 case hs of

146 (h: hs) -> do patvar h; mkPat

147 [] -> return ()

148

149-- | Build a term autogenerated as an interface method definition.

150--

151-- (Separate, so we don't go overboard resolving things that we don't

152-- know about yet on the LHS of a pattern def)

153

154buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

155 [Name] -> -- Cached names in the PTerm, before adding PAlternatives

156 PTerm ->

157 ElabD ElabResult

158buildTC ist info emode opts fn ns tm

159 = do let inf = case lookupCtxt fn (idris_tyinfodata ist) of

160 [TIPartial] -> True

161 _ -> False

162 -- set name supply to begin after highest index in tm

163 initNextNameFrom ns

164 elab ist info emode opts fn tm

165 probs <- get_probs

166 tm <- get_term

167 case probs of

168 [] -> return ()

169 ((_,_,_,_,e,_,_):es) -> if inf then return ()

170 else lift (Error e)

171 dots <- get_dotterm

172 -- 'dots' are the PHidden things which have not been solved by

173 -- unification

174 when (not (null dots)) $

175 lift (Error (CantMatch (getInferTerm tm)))

176 EState is _ impls highlights _ _ <- getAux

177 tt <- get_term

178 ctxt <- get_context

179 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

180 log <- getLog

181 g_nextname <- get_global_nextname

182 if (log /= "")

183 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

184 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

185

186-- | return whether arguments of the given constructor name can be

187-- matched on. If they're polymorphic, no, unless the type has beed

188-- made concrete by the time we get around to elaborating the

189-- argument.

190getUnmatchable :: Context -> Name -> [Bool]

191getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

192 = case lookupTyExact n ctxt of

193 Nothing -> []

194 Just ty -> checkArgs [] [] ty

195 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]

196 checkArgs env ns (Bind n (Pi _ _ t _) sc)

197 = let env' = case t of

198 TType _ -> n : env

199 _ -> env in

200 checkArgs env' (intersect env (refsIn t) : ns)

201 (instantiate (P Bound n t) sc)

202 checkArgs env ns t

203 = map (not . null) (reverse ns)

204

205getUnmatchable ctxt n = []

206

207data ElabCtxt = ElabCtxt { e_inarg :: Bool,

208 e_isfn :: Bool, -- ^ Function part of application

209 e_guarded :: Bool,

210 e_intype :: Bool,

211 e_qq :: Bool,

212 e_nomatching :: Bool -- ^ can't pattern match

213 }

214

215initElabCtxt = ElabCtxt False False False False False False

216

217goal_polymorphic :: ElabD Bool

218goal_polymorphic =

219 do ty <- goal

220 case ty of

221 P _ n _ -> do env <- get_env

222 case lookupBinder n env of

223 Nothing -> return False

224 _ -> return True

225 _ -> return False

226

227-- | Returns the set of declarations we need to add to complete the

228-- definition (most likely case blocks to elaborate) as well as

229-- declarations resulting from user tactic scripts (%runElab)

230elab :: IState

231 -> ElabInfo

232 -> ElabMode

233 -> FnOpts

234 -> Name

235 -> PTerm

236 -> ElabD ()

237elab ist info emode opts fn tm

238 = do let loglvl = opt_logLevel (idris_options ist)

239 when (loglvl > 5) $ unifyLog True

240 compute -- expand type synonyms, etc

241 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

242 est <- getAux

243 sequence_ (get_delayed_elab est)

244 end_unify

245 when (pattern || intransform) $

246 -- convert remaining holes to pattern vars

247 do unify_all

248 matchProblems False -- only the ones we matched earlier

249 unifyProblems

250 mkPat

251 update_term liftPats

252 ptm <- get_term

253 when pattern $

254 -- Look for Rig1 (linear) pattern bindings

255 do let pnms = findLinear Rig1 ist [] ptm

256 update_term (setLinear pnms)

257 where

258 pattern = emode == ELHS || emode == EImpossible

259 eimpossible = emode == EImpossible

260 intransform = emode == ETransLHS

261 bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS

262 || emode == EImpossible

263 autoimpls = opt_autoimpls (idris_options ist)

264

265 get_delayed_elab est =

266 let ds = delayed_elab est in

267 map snd $ sortBy (\(p1, _) (p2, _) -> compare p1 p2) ds

268

269 tcgen = Dictionary `elem` opts

270 reflection = Reflection `elem` opts

271

272 isph arg = case getTm arg of

273 Placeholder -> (True, priority arg)

274 tm -> (False, priority arg)

275

276 mkPat = do hs <- get_holes

277 tm <- get_term

278 case hs of

279 (h: hs) -> do patvar h; mkPat

280 [] -> return ()

281

282 elabRec = elabE initElabCtxt Nothing

283

284 -- | elabE elaborates an expression, possibly wrapping implicit coercions

285 -- and forces/delays. If you make a recursive call in elab', it is

286 -- normally correct to call elabE - the ones that don't are `desugarings

287 -- typically

288 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()

289 elabE ina fc' t =

290 do solved <- get_recents

291 as <- get_autos

292 hs <- get_holes

293 -- If any of the autos use variables which have recently been solved,

294 -- have another go at solving them now.

295 mapM_ (\(a, (failc, ns)) ->

296 if any (\n -> n `elem` solved) ns && head hs /= a

297 then solveAuto ist fn False (a, failc)

298 else return ()) as

299

300 apt <- expandToArity t

301 itm <- if not pattern then insertImpLam ina apt else return apt

302 ct <- insertCoerce ina itm

303 t' <- insertLazy ina ct

304 g <- goal

305 tm <- get_term

306 ps <- get_probs

307 hs <- get_holes

308

309 --trace ("Elaborating " ++ show t' ++ " in " ++ show g

310 -- ++ "\n" ++ show tm

311 -- ++ "\nholes " ++ show hs

312 -- ++ "\nproblems " ++ show ps

313 -- ++ "\n-----------\n") $

314 --trace ("ELAB " ++ show t') $

315 env <- get_env

316 let fc = fileFC "Force"

317 handleError (forceErr t' env)

318 (elab' ina fc' t')

319 (elab' ina fc' (PApp fc (PRef fc [] (sUN "Force"))

320 [pimp (sUN "t") Placeholder True,

321 pimp (sUN "a") Placeholder True,

322 pexp ct]))

323

324 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

325 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

326 ht == txt "Delayed" = notDelay orig

327 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

328 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

329 ht == txt "Delayed" = notDelay orig

330 forceErr orig env (InfiniteUnify _ t _)

331 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

332 ht == txt "Delayed" = notDelay orig

333 forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t

334 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t

335 forceErr orig env (At _ t) = forceErr orig env t

336 forceErr orig env t = False

337

338 notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

339 notDelay _ = True

340

341 elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)

342 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

343 -> PTerm -- ^ The term to elaborate

344 -> ElabD ()

345 elab' ina fc (PNoImplicits t) = elab' ina fc t -- skip elabE step

346 elab' ina fc (PType fc') =

347 do apply RType []

348 solve

349 highlightSource fc' (AnnType "Type" "The type of types")

350 elab' ina fc (PUniverse fc' u) =

351 do unless (UniquenessTypes `elem` idris_language_extensions ist

352 || e_qq ina) $

353 lift $ tfail $ At fc' (Msg "You must turn on the UniquenessTypes extension to use UniqueType or AnyType")

354 apply (RUType u) []

355 solve

356 highlightSource fc' (AnnType (show u) "The type of unique types")

357-- elab' (_,_,inty) (PConstant c)

358-- | constType c && pattern && not reflection && not inty

359-- = lift $ tfail (Msg "Typecase is not allowed")

360 elab' ina fc tm@(PConstant fc' c)

361 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

362 && isTypeConst c

363 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

364 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

365 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

366 | otherwise = do apply (RConstant c) []

367 solve

368 highlightSource fc' (AnnConst c)

369 elab' ina fc (PQuote r) = do fill r; solve

370 elab' ina _ (PTrue fc _) =

371 do compute

372 g <- goal

373 case g of

374 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

375 UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

376 _ -> elab' ina (Just fc) (PRef fc [] unitCon)

377 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent interfaces

378 = do g <- goal; resolveTC False False 5 g fn elabRec ist

379 elab' ina fc (PResolveTC fc')

380 = do c <- getNameFrom (sMN 0 "__interface")

381 implementationArg c

382 -- Elaborate the equality type first homogeneously, then

383 -- heterogeneously as a fallback

384 elab' ina _ (PApp fc (PRef _ _ n) args)

385 | n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args

386 = try (do tyn <- getNameFrom (sMN 0 "aqty")

387 claim tyn RType

388 movelast tyn

389 elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)

390 [pimp (sUN "A") (PRef NoFC [] tyn) True,

391 pimp (sUN "B") (PRef NoFC [] tyn) False,

392 pexp l, pexp r]))

393 (do atyn <- getNameFrom (sMN 0 "aqty")

394 btyn <- getNameFrom (sMN 0 "bqty")

395 claim atyn RType

396 movelast atyn

397 claim btyn RType

398 movelast btyn

399 elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)

400 [pimp (sUN "A") (PRef NoFC [] atyn) True,

401 pimp (sUN "B") (PRef NoFC [] btyn) False,

402 pexp l, pexp r]))

403

404 elab' ina _ (PPair fc hls _ l r)

405 = do compute

406 g <- goal

407 let (tc, _) = unApply g

408 case g of

409 TType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairTy)

410 [pexp l,pexp r])

411 UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)

412 [pexp l,pexp r])

413 _ -> case tc of

414 P _ n _ | n == upairTy

415 -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)

416 [pimp (sUN "A") Placeholder False,

417 pimp (sUN "B") Placeholder False,

418 pexp l, pexp r])

419 _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairCon)

420 [pimp (sUN "A") Placeholder False,

421 pimp (sUN "B") Placeholder False,

422 pexp l, pexp r])

423 elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)

424 = case p of

425 IsType -> asType

426 IsTerm -> asValue

427 TypeOrTerm ->

428 do compute

429 g <- goal

430 case g of

431 TType _ -> asType

432 _ -> asValue

433 where asType = elab' ina (Just fc) (PApp fc (PRef NoFC hls sigmaTy)

434 [pexp t,

435 pexp (PLam fc n nfc Placeholder r)])

436 asValue = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)

437 [pimp (sMN 0 "a") t False,

438 pimp (sMN 0 "P") Placeholder True,

439 pexp l, pexp r])

440

441 elab' ina _ (PDPair fc hls p l t r) = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)

442 [pimp (sMN 0 "a") t False,

443 pimp (sMN 0 "P") Placeholder True,

444 pexp l, pexp r])

445 elab' ina fc (PAlternative ms (ExactlyOne delayok) as)

446 = do as_pruned <- doPrune as

447 -- Finish the mkUniqueNames job with the pruned set, rather than

448 -- the full set.

449 uns <- get_usedns

450 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned

451 ~(h : hs) <- get_holes

452 ty <- goal

453 case as' of

454 [] -> do hds <- mapM showHd as

455 lift $ tfail $ NoValidAlts hds

456 [x] -> elab' ina fc x

457 -- If there's options, try now, and if that fails, postpone

458 -- to later.

459 _ -> handleError isAmbiguous

460 (do hds <- mapM showHd as'

461 tryAll (zip (map (elab' ina fc) as')

462 hds))

463 (do movelast h

464 delayElab 5 $ do

465 hs <- get_holes

466 when (h `elem` hs) $ do

467 focus h

468 as'' <- doPrune as'

469 case as'' of

470 [x] -> elab' ina fc x

471 _ -> do hds <- mapM showHd as''

472 tryAll' False (zip (map (elab' ina fc) as'')

473 hds))

474 where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])

475 | l == txt "Delay" = showHd (getTm arg)

476 showHd (PApp _ (PRef _ _ n) _) = return n

477 showHd (PRef _ _ n) = return n

478 showHd (PApp _ h _) = showHd h

479 showHd (PHidden h) = showHd h

480 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here

481

482 doPrune as =

483 do compute -- to get 'Delayed' if it's there

484 ty <- goal

485 ctxt <- get_context

486 env <- get_env

487 let ty' = unDelay ty

488 let (tc, _) = unApply ty'

489 return $ pruneByType eimpossible env tc ty' ist as

490

491 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,

492 l == txt "Delayed" = unDelay arg

493 | otherwise = t

494

495 isAmbiguous (CantResolveAlts _) = delayok

496 isAmbiguous (Elaborating _ _ _ e) = isAmbiguous e

497 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e

498 isAmbiguous (At _ e) = isAmbiguous e

499 isAmbiguous _ = False

500

501 elab' ina fc (PAlternative ms FirstSuccess as_in)

502 = do -- finish the mkUniqueNames job

503 uns <- get_usedns

504 let as = map (mkUniqueNames (uns ++ map snd ms) ms) as_in

505 trySeq as

506 where -- if none work, take the error from the first

507 trySeq (x : xs) = let e1 = elab' ina fc x in

508 try' e1 (trySeq' e1 xs) True

509 trySeq [] = fail "Nothing to try in sequence"

510 trySeq' deferr [] = do deferr; unifyProblems

511 trySeq' deferr (x : xs)

512 = try' (tryCatch (do elab' ina fc x

513 solveAutos ist fn False

514 unifyProblems)

515 (\_ -> trySeq' deferr []))

516 (trySeq' deferr xs) True

517 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

518 env <- get_env

519 compute

520 ty <- goal

521 let doelab = elab' ina fc orig

522 tryCatch doelab

523 (\err ->

524 if recoverableErr err

525 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++

526 -- show alts ++ "\n" ++

527 -- showQuick err) $

528 -- Prune the coercions so that only the ones

529 -- with the right type to fix the error will be tried!

530 case pruneAlts err alts env of

531 [] -> lift $ tfail err

532 alts' -> do

533 try' (elab' ina fc (PAlternative ms (ExactlyOne False) alts'))

534 (lift $ tfail err) -- take error from original if all fail

535 True

536 else lift $ tfail err)

537 where

538 recoverableErr (CantUnify _ _ _ _ _ _) = True

539 recoverableErr (TooManyArguments _) = False

540 recoverableErr (CantSolveGoal _ _) = False

541 recoverableErr (CantResolveAlts _) = False

542 recoverableErr (NoValidAlts _) = True

543 recoverableErr (ProofSearchFail (Msg _)) = True

544 recoverableErr (ProofSearchFail _) = False

545 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

546 recoverableErr (At _ e) = recoverableErr e

547 recoverableErr (ElabScriptDebug _ _ _) = False

548 recoverableErr _ = True

549

550 pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env

551 = case unApply (normalise (tt_ctxt ist) env inc) of

552 (P (TCon _ _) n _, _) -> filter (hasArg n env) alts

553 (Constant _, _) -> alts

554 _ -> filter isLend alts -- special case hack for 'Borrowed'

555 pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env

556 pruneAlts (At _ e) alts env = pruneAlts e alts env

557 pruneAlts (NoValidAlts as) alts env = alts

558 pruneAlts err alts _ = filter isLend alts

559

560 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'

561 hasArg n env (PApp _ (PRef _ _ a) _)

562 = case lookupTyExact a (tt_ctxt ist) of

563 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in

564 any (fnIs n) args

565 Nothing -> False

566 hasArg n env (PAlternative _ _ as) = any (hasArg n env) as

567 hasArg n _ tm = False

568

569 isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"]

570 isLend _ = False

571

572 fnIs n ty = case unApply ty of

573 (P _ n' _, _) -> n == n'

574 _ -> False

575

576 elab' ina _ (PPatvar fc n) | bindfree

577 = do patvar n

578 update_term liftPats

579 highlightSource fc (AnnBoundName n False)

580-- elab' (_, _, inty) (PRef fc f)

581-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

582-- = lift $ tfail (Msg "Typecase is not allowed")

583 elab' ec fc' tm@(PRef fc hls n)

584 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)

585 && isTConName n (tt_ctxt ist)

586 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

587 | pattern && not reflection && not (e_qq ec) && e_nomatching ec

588 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

589 | (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

590 = do ty <- goal

591 testImplicitWarning fc n ty

592 let ina = e_inarg ec

593 ctxt <- get_context

594 env <- get_env

595

596 -- If the name is defined, globally or locally, elaborate it

597 -- as a reference, otherwise it might end up as a pattern var.

598 let defined = case lookupTy n ctxt of

599 [] -> case lookupTyEnv n env of

600 Just _ -> True

601 _ -> False

602 _ -> True

603

604 -- this is to stop us resolving interfaces recursively

605 if (tcname n && ina && not intransform)

606 then erun fc $

607 do patvar n

608 update_term liftPats

609 highlightSource fc (AnnBoundName n False)

610 else if defined -- finally, ordinary PRef elaboration

611 then elabRef ec fc' fc hls n tm

612 else try (do apply (Var n) []

613 annot <- findHighlight n

614 solve

615 highlightSource fc annot)

616 (do patvar n

617 update_term liftPats

618 highlightSource fc (AnnBoundName n False))

619 where inparamBlock n = case lookupCtxtName n (inblock info) of

620 [] -> False

621 _ -> True

622 bindable (NS _ _) = False

623 bindable (MN _ _) = True

624 bindable n = implicitable n && autoimpls

625 elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

626 elab' ina fc' tm@(PRef fc hls n)

627 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

628 && isTConName n (tt_ctxt ist)

629 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

630 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

631 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

632 | otherwise = elabRef ina fc' fc hls n tm

633 elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

634 elab' ina _ (PLam fc n nfc Placeholder sc)

635 = do -- if n is a type constructor name, this makes no sense...

636 ctxt <- get_context

637 when (isTConName n ctxt) $

638 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")

639 checkPiGoal n

640 attack; intro (Just n);

641 addPSname n -- okay for proof search

642 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

643 elabE (ina { e_inarg = True } ) (Just fc) sc; solve

644 highlightSource nfc (AnnBoundName n False)

645 elab' ec _ (PLam fc n nfc ty sc)

646 = do tyn <- getNameFrom (sMN 0 "lamty")

647 -- if n is a type constructor name, this makes no sense...

648 ctxt <- get_context

649 when (isTConName n ctxt) $

650 lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")

651 checkPiGoal n

652 claim tyn RType

653 explicit tyn

654 attack

655 ptm <- get_term

656 hs <- get_holes

657 introTy (Var tyn) (Just n)

658 addPSname n -- okay for proof search

659 focus tyn

660

661 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

662 elabE (ec { e_inarg = True }) (Just fc) sc

663 solve

664 highlightSource nfc (AnnBoundName n False)

665 elab' ina fc (PPi p n nfc Placeholder sc)

666 = do attack;

667 case pcount p of

668 RigW -> return ()

669 _ -> unless (LinearTypes `elem` idris_language_extensions ist

670 || e_qq ina) $

671 lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a count")

672 arg n (pcount p) (is_scoped p) (sMN 0 "phTy")

673 addAutoBind p n

674 addPSname n -- okay for proof search

675 elabE (ina { e_inarg = True, e_intype = True }) fc sc

676 solve

677 highlightSource nfc (AnnBoundName n False)

678 elab' ina fc (PPi p n nfc ty sc)

679 = do attack; tyn <- getNameFrom (sMN 0 "piTy")

680 claim tyn RType

681 n' <- case n of

682 MN _ _ -> unique_hole n

683 _ -> return n

684 case pcount p of

685 RigW -> return ()

686 _ -> unless (LinearTypes `elem` idris_language_extensions ist

687 || e_qq ina) $

688 lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a linear argument")

689 forall n' (pcount p) (is_scoped p) (Var tyn)

690 addAutoBind p n'

691 addPSname n' -- okay for proof search

692 focus tyn

693 let ec' = ina { e_inarg = True, e_intype = True }

694 elabE ec' fc ty

695 elabE ec' fc sc

696 solve

697 highlightSource nfc (AnnBoundName n False)

698 elab' ina _ tm@(PLet fc rig n nfc ty val sc)

699 = do attack

700 ivs <- get_implementations

701 tyn <- getNameFrom (sMN 0 "letty")

702 claim tyn RType

703 valn <- getNameFrom (sMN 0 "letval")

704 claim valn (Var tyn)

705 explicit valn

706 letbind n rig (Var tyn) (Var valn)

707 addPSname n

708 case ty of

709 Placeholder -> return ()

710 _ -> do focus tyn

711 explicit tyn

712 elabE (ina { e_inarg = True, e_intype = True })

713 (Just fc) ty

714 focus valn

715 elabE (ina { e_inarg = True, e_intype = True })

716 (Just fc) val

717 ivs' <- get_implementations

718 env <- get_env

719 elabE (ina { e_inarg = True }) (Just fc) sc

720 when (not (pattern || intransform)) $

721 mapM_ (\n -> do focus n

722 g <- goal

723 hs <- get_holes

724 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

725 then handleError (tcRecoverable emode)

726 (resolveTC True False 10 g fn elabRec ist)

727 (movelast n)

728 else movelast n)

729 (ivs' \\ ivs)

730 -- HACK: If the name leaks into its type, it may leak out of

731 -- scope outside, so substitute in the outer scope.

732 expandLet n (case lookupBinder n env of

733 Just (Let rig t v) -> v

734 other -> error ("Value not a let binding: " ++ show other))

735 solve

736 highlightSource nfc (AnnBoundName n False)

737 elab' ina _ (PGoal fc r n sc) = do

738 rty <- goal

739 attack

740 tyn <- getNameFrom (sMN 0 "letty")

741 claim tyn RType

742 valn <- getNameFrom (sMN 0 "letval")

743 claim valn (Var tyn)

744 letbind n RigW (Var tyn) (Var valn)

745 focus valn

746 elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])

747 env <- get_env

748 computeLet n

749 elabE (ina { e_inarg = True }) (Just fc) sc

750 solve

751-- elab' ina fc (PLet n Placeholder

752-- (PApp fc r [pexp (delab ist rty)]) sc)

753 elab' ina _ tm@(PApp fc (PInferRef _ _ f) args) = do

754 rty <- goal

755 ds <- get_deferred

756 ctxt <- get_context

757 -- make a function type a -> b -> c -> ... -> rty for the

758 -- new function name

759 env <- get_env

760 argTys <- claimArgTys env args

761 fn <- getNameFrom (sMN 0 "inf_fn")

762 let fty = fnTy argTys rty

763-- trace (show (ptm, map fst argTys)) $ focus fn

764 -- build and defer the function application

765 attack; deferType (mkN f) fty (map fst argTys); solve

766 -- elaborate the arguments, to unify their types. They all have to

767 -- be explicit.

768 mapM_ elabIArg (zip argTys args)

769 where claimArgTys env [] = return []

770 claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)

771 = do nty <- get_type (Var n)

772 ans <- claimArgTys env xs

773 return ((n, (False, forget nty)) : ans)

774 claimArgTys env (_ : xs)

775 = do an <- getNameFrom (sMN 0 "inf_argTy")

776 aval <- getNameFrom (sMN 0 "inf_arg")

777 claim an RType

778 claim aval (Var an)

779 ans <- claimArgTys env xs

780 return ((aval, (True, (Var an))) : ans)

781 fnTy [] ret = forget ret

782 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi RigW Nothing xt RType) (fnTy xs ret)

783

784 localVar env (PRef _ _ x)

785 = case lookupBinder x env of

786 Just _ -> Just x

787 _ -> Nothing

788 localVar env _ = Nothing

789

790 elabIArg ((n, (True, ty)), def) =

791 do focus n; elabE ina (Just fc) (getTm def)

792 elabIArg _ = return () -- already done, just a name

793

794 mkN n@(NS _ _) = n

795 mkN n@(SN _) = n

796 mkN n = case namespace info of

797 xs@(_:_) -> sNS n xs

798 _ -> n

799

800 elab' ina _ (PMatchApp fc fn)

801 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

802 [(n, args)] -> return (n, map (const True) args)

803 _ -> lift $ tfail (NoSuchVariable fn)

804 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

805 solve

806 -- if f is local, just do a simple_app

807 -- FIXME: Anyone feel like refactoring this mess? - EB

808 elab' ina topfc tm@(PApp fc (PRef ffc hls f) args_in)

809 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

810 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

811 | otherwise = implicitApp $

812 do env <- get_env

813 ty <- goal

814 fty <- get_type (Var f)

815 ctxt <- get_context

816 let dataCon = isDConName f ctxt

817 annot <- findHighlight f

818 knowns_m <- mapM getKnownImplicit args_in

819 let knowns = mapMaybe id knowns_m

820 args <- insertScopedImps fc f knowns (normalise ctxt env fty) args_in

821

822 let unmatchableArgs = if pattern

823 then getUnmatchable (tt_ctxt ist) f

824 else []

825-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $

826 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

827 && isTConName f (tt_ctxt ist)) $

828 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

829-- trace (show (f, args_in, args)) $

830 if (f `elem` map fstEnv env && length args == 1 && length args_in == 1)

831 then -- simple app, as below

832 do simple_app False

833 (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))

834 (elabE (ina { e_inarg = True,

835 e_guarded = dataCon }) (Just fc) (getTm (head args)))

836 (show tm)

837 solve

838 mapM (uncurry highlightSource) $

839 (ffc, annot) : map (\f -> (f, annot)) hls

840 return []

841 else

842 do ivs <- get_implementations

843 ps <- get_probs

844 -- HACK: we shouldn't resolve interfaces if we're defining an implementation

845 -- function or default definition.

846 let isinf = f == inferCon || tcname f

847 -- if f is an interface, we need to know its arguments so that

848 -- we can unify with them

849 case lookupCtxt f (idris_interfaces ist) of

850 [] -> return ()

851 _ -> do mapM_ setInjective (map getTm args)

852 -- maybe more things are solvable now

853 unifyProblems

854-- trace ("args is " ++ show args) $ return ()

855 ns <- apply (Var f) (map isph args)

856-- trace ("ns is " ++ show ns) $ return ()

857 -- mark any interface arguments as injective

858-- when (not pattern) $

859 mapM_ checkIfInjective (map snd ns)

860 unifyProblems -- try again with the new information,

861 -- to help with disambiguation

862 ulog <- getUnifyLog

863

864 annot <- findHighlight f

865 mapM (uncurry highlightSource) $

866 (ffc, annot) : map (\f -> (f, annot)) hls

867

868 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf,

869 e_guarded = dataCon })

870 [] fc False f

871 (zip ns (unmatchableArgs ++ repeat False))

872 (f == sUN "Force")

873 (map (\x -> getTm x) args) -- TODO: remove this False arg

874 imp <- if (e_isfn ina) then

875 do guess <- get_guess

876 env <- get_env

877 case safeForgetEnv (map fstEnv env) guess of

878 Nothing ->

879 return []

880 Just rguess -> do

881 gty <- get_type rguess

882 let ty_n = normalise ctxt env gty

883 return $ getReqImps ty_n

884 else return []

885 -- Now we find out how many implicits we needed at the

886 -- end of the application by looking at the goal again

887 -- - Have another go, but this time add the

888 -- implicits (can't think of a better way than this...)

889 case imp of

890 rs@(_:_) | not pattern -> return rs -- quit, try again

891 _ -> do solve

892 hs <- get_holes

893 ivs' <- get_implementations

894 -- Attempt to resolve any interfaces which have 'complete' types,

895 -- i.e. no holes in them

896 when (not pattern || (e_inarg ina && not tcgen)) $

897 mapM_ (\n -> do focus n

898 g <- goal

899 env <- get_env

900 hs <- get_holes

901 if all (\n -> not (n `elem` hs)) (freeNames g)

902 then handleError (tcRecoverable emode)

903 (resolveTC False False 10 g fn elabRec ist)

904 (movelast n)

905 else movelast n)

906 (ivs' \\ ivs)

907 return []

908 where

909 -- Run the elaborator, which returns how many implicit

910 -- args were needed, then run it again with those args. We need

911 -- this because we have to elaborate the whole application to

912 -- find out whether any computations have caused more implicits

913 -- to be needed.

914 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

915 implicitApp elab

916 | pattern || intransform = do elab; return ()

917 | otherwise

918 = do s <- get

919 imps <- elab

920 case imps of

921 [] -> return ()

922 es -> do put s

923 elab' ina topfc (PAppImpl tm es)

924

925 getKnownImplicit imp

926 | UnknownImp `elem` argopts imp

927 = return Nothing -- lift $ tfail $ UnknownImplicit (pname imp) f

928 | otherwise = return (Just (pname imp))

929

930 getReqImps (Bind x (Pi _ (Just i) ty _) sc)

931 = i : getReqImps sc

932 getReqImps _ = []

933

934 checkIfInjective n = do

935 env <- get_env

936 case lookupBinder n env of

937 Nothing -> return ()

938 Just b ->

939 case unApply (normalise (tt_ctxt ist) env (binderTy b)) of

940 (P _ c _, args) ->

941 case lookupCtxtExact c (idris_interfaces ist) of

942 Nothing -> return ()

943 Just ci -> -- interface, set as injective

944 do mapM_ setinjArg (getDets 0 (interface_determiners ci) args)

945 -- maybe we can solve more things now...

946 ulog <- getUnifyLog

947 probs <- get_probs

948 inj <- get_inj

949 traceWhen ulog ("Injective now " ++ show args ++ "\nAll: " ++ show inj

950 ++ "\nProblems: " ++ qshow probs) $

951 unifyProblems

952 probs <- get_probs

953 traceWhen ulog (qshow probs) $ return ()

954 _ -> return ()

955

956 setinjArg (P _ n _) = setinj n

957 setinjArg _ = return ()

958

959 getDets i ds [] = []

960 getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as

961 | otherwise = getDets (i + 1) ds as

962

963 setInjective (PRef _ _ n) = setinj n

964 setInjective (PApp _ (PRef _ _ n) _) = setinj n

965 setInjective _ = return ()

966

967 elab' ina _ tm@(PApp fc f [arg]) =

968 erun fc $

969 do simple_app (not $ headRef f)

970 (elabE (ina { e_isfn = True }) (Just fc) f)

971 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

972 (show tm)

973 solve

974 where headRef (PRef _ _ _) = True

975 headRef (PApp _ f _) = headRef f

976 headRef (PAlternative _ _ as) = all headRef as

977 headRef _ = False

978

979 elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...

980 solve

981 where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits

982 appImpl (e : es) = simple_app False

983 (appImpl es)

984 (elab' ina fc Placeholder)

985 (show f)

986 elab' ina fc Placeholder

987 = do ~(h : hs) <- get_holes

988 movelast h

989 elab' ina fc (PMetavar nfc n) =

990 do ptm <- get_term

991 -- When building the metavar application, leave out the unique

992 -- names which have been used elsewhere in the term, since we

993 -- won't be able to use them in the resulting application.

994 env <- get_env

995 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

996 let lin_used = getLinearUsed (tt_ctxt ist) ptm

997 let n' = metavarName (namespace info) n

998 attack

999 psns <- getPSnames

1000 n' <- defer unique_used lin_used n'

1001 solve

1002 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

1003 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

1004 elab' ina fc (PTactics ts)

1005 | not pattern = do mapM_ (runTac False ist fc fn) ts

1006 | otherwise = elab' ina fc Placeholder

1007 elab' ina fc (PElabError e) = lift $ tfail e

1008 elab' ina mfc (PRewrite fc substfn rule sc newg)

1009 = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg

1010 -- A common error case if trying to typecheck an autogenerated case block

1011 elab' ina _ c@(PCase fc Placeholder opts)

1012 = lift $ tfail (Msg "No expression for the case to inspect.\nYou need to replace the _ with an expression.")

1013 elab' ina _ c@(PCase fc scr opts)

1014 = do attack

1015

1016 tyn <- getNameFrom (sMN 0 "scty")

1017 claim tyn RType

1018 valn <- getNameFrom (sMN 0 "scval")

1019 scvn <- getNameFrom (sMN 0 "scvar")

1020 claim valn (Var tyn)

1021 env <- get_env

1022

1023 let scrnames = allNamesIn scr

1024 letbind scvn (letrig scrnames env) (Var tyn) (Var valn)

1025

1026 -- Start filling in the scrutinee type, if we can work one

1027 -- out from the case options

1028 let scrTy = getScrType (map fst opts)

1029 case scrTy of

1030 Nothing -> return ()

1031 Just ty -> do focus tyn

1032 elabE ina (Just fc) ty

1033

1034 focus valn

1035 elabE (ina { e_inarg = True }) (Just fc) scr

1036 -- Solve any remaining implicits - we need to solve as many

1037 -- as possible before making the 'case' type

1038 unifyProblems

1039 matchProblems True

1040 args <- get_env

1041 envU <- mapM (getKind args) args

1042

1043 -- Drop the unique arguments used in the term already

1044 -- and in the scrutinee (since it's

1045 -- not valid to use them again anyway)

1046 --

1047 -- Also drop unique arguments which don't appear explicitly

1048 -- in either case branch so they don't count as used

1049 -- unnecessarily (can only do this for unique things, since we

1050 -- assume they don't appear implicitly in types)

1051 ptm <- get_term

1052 let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

1053

1054 let argsDropped = filter (\t -> isUnique envU t || isNotLift args t)

1055 (nub $ scrnames ++ inApp ptm ++

1056 inOpts)

1057 let lin_used = getLinearUsed (tt_ctxt ist) ptm

1058

1059 let args' = filter (\(n, _, _) -> n `notElem` argsDropped) args

1060

1061 -- trace (show lin_used ++ "\n" ++ show args ++ "\n" ++ show ptm) attack

1062 attack

1063 cname' <- defer argsDropped lin_used (mkN (mkCaseName fc fn))

1064 solve

1065

1066 -- if the scrutinee is one of the 'args' in env, we should

1067 -- inspect it directly, rather than adding it as a new argument

1068 let newdef = PClauses fc [] cname'

1069 (caseBlock fc cname' scr

1070 (map (isScr scr) (reverse args')) opts)

1071 -- elaborate case

1072 updateAux (\e -> e { case_decls = (cname', newdef) : case_decls e } )

1073 -- if we haven't got the type yet, hopefully we'll get it later!

1074 movelast tyn

1075 solve

1076 where mkCaseName fc (NS n ns) = NS (mkCaseName fc n) ns

1077 mkCaseName fc n = SN (CaseN (FC' fc) n)

1078-- mkCaseName (UN x) = UN (x ++ "_case")

1079-- mkCaseName (MN i x) = MN i (x ++ "_case")

1080 mkN n@(NS _ _) = n

1081 mkN n = case namespace info of

1082 xs@(_:_) -> sNS n xs

1083 _ -> n

1084

1085 -- If any variables in the scrutinee are in the environment with

1086 -- multiplicity other than RigW, let bind the scrutinee variable

1087 -- with the smallest multiplicity

1088 letrig ns [] = RigW

1089 letrig ns env = letrig' Rig1 ns env

1090

1091 letrig' def ns [] = def

1092 letrig' def ns ((n, r, _) : env)

1093 | n `elem` ns = letrig' (rigMult def r) ns env

1094 | otherwise = letrig' def ns env

1095

1096 getScrType [] = Nothing

1097 getScrType (f : os) = maybe (getScrType os) Just (getAppType f)

1098

1099 getAppType (PRef _ _ n) =

1100 case lookupTyName n (tt_ctxt ist) of

1101 [(n', ty)] | isDConName n' (tt_ctxt ist) ->

1102 case unApply (getRetTy ty) of

1103 (P _ tyn _, args) ->

1104 Just (PApp fc (PRef fc [] tyn)

1105 (map pexp (map (const Placeholder) args)))

1106 _ -> Nothing

1107 _ -> Nothing -- ambiguity is no help to us!

1108 getAppType (PApp _ t as) = getAppType t

1109 getAppType _ = Nothing

1110

1111 inApp (P _ n _) = [n]

1112 inApp (App _ f a) = inApp f ++ inApp a

1113 inApp (Bind n (Let _ _ v) sc) = inApp v ++ inApp sc

1114 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc

1115 inApp (Bind n b sc) = inApp sc

1116 inApp _ = []

1117

1118 isUnique envk n = case lookup n envk of

1119 Just u -> u

1120 _ -> False

1121

1122 getKind env (n, _, _)

1123 = case lookupBinder n env of

1124 Nothing -> return (n, False) -- can't happen, actually...

1125 Just b ->

1126 do ty <- get_type (forget (binderTy b))

1127 case ty of

1128 UType UniqueType -> return (n, True)

1129 UType AllTypes -> return (n, True)

1130 _ -> return (n, False)

1131

1132 isNotLift env n

1133 = case lookupBinder n env of

1134 Just ty ->

1135 case unApply (binderTy ty) of

1136 (P _ n _, _) -> n `elem` noCaseLift info

1137 _ -> False

1138 _ -> False

1139

1140 elab' ina fc (PUnifyLog t) = do unifyLog True

1141 elab' ina fc t

1142 unifyLog False

1143 elab' ina fc (PQuasiquote t goalt)

1144 = do -- First extract the unquoted subterms, replacing them with fresh

1145 -- names in the quasiquoted term. Claim their reflections to be

1146 -- an inferred type (to support polytypic quasiquotes).

1147 finalTy <- goal

1148 (t, unq) <- extractUnquotes 0 t

1149 let unquoteNames = map fst unq

1150 mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames

1151

1152 -- Save the old state - we need a fresh proof state to avoid

1153 -- capturing lexically available variables in the quoted term.

1154 ctxt <- get_context

1155 datatypes <- get_datatypes

1156 g_nextname <- get_global_nextname

1157 saveState

1158 updatePS (const .

1159 newProof (sMN 0 "q") (constraintNS info) ctxt datatypes g_nextname $

1160 P Ref (reflm "TT") Erased)

1161

1162 -- Re-add the unquotes, letting Idris infer the (fictional)

1163 -- types. Here, they represent the real type rather than the type

1164 -- of their reflection.

1165 mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")

1166 claim ty RType

1167 movelast ty

1168 claim n (Var ty)

1169 movelast n)

1170 unquoteNames

1171

1172 -- Determine whether there's an explicit goal type, and act accordingly

1173 -- Establish holes for the type and value of the term to be

1174 -- quasiquoted

1175 qTy <- getNameFrom (sMN 0 "qquoteTy")

1176 claim qTy RType

1177 movelast qTy

1178 qTm <- getNameFrom (sMN 0 "qquoteTm")

1179 claim qTm (Var qTy)

1180

1181 -- Let-bind the result of elaborating the contained term, so that

1182 -- the hole doesn't disappear

1183 nTm <- getNameFrom (sMN 0 "quotedTerm")

1184 letbind nTm RigW (Var qTy) (Var qTm)

1185

1186 -- Fill out the goal type, if relevant

1187 case goalt of

1188 Nothing -> return ()

1189 Just gTy -> do focus qTy

1190 elabE (ina { e_qq = True }) fc gTy

1191

1192 -- Elaborate the quasiquoted term into the hole

1193 focus qTm

1194 elabE (ina { e_qq = True }) fc t

1195 end_unify

1196

1197 -- We now have an elaborated term. Reflect it and solve the

1198 -- original goal in the original proof state, preserving highlighting

1199 env <- get_env

1200 EState _ _ _ hs _ _ <- getAux

1201 loadState

1202 updateAux (\aux -> aux { highlighting = hs })

1203

1204 let quoted = fmap (explicitNames . binderVal) $ lookupBinder nTm env

1205 isRaw = case unApply (normaliseAll ctxt env finalTy) of

1206 (P _ n _, []) | n == reflm "Raw" -> True

1207 _ -> False

1208 case quoted of

1209 Just q -> do ctxt <- get_context

1210 (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, RigW, Lam RigW Erased) | uq <- unquoteNames] (forget q) q

1211 if pattern

1212 then if isRaw

1213 then reflectRawQuotePattern unquoteNames (forget q')

1214 else reflectTTQuotePattern unquoteNames q'

1215 else do if isRaw

1216 then -- we forget q' instead of using q to ensure rechecking

1217 fill $ reflectRawQuote unquoteNames (forget q')

1218 else fill $ reflectTTQuote unquoteNames q'

1219 solve

1220

1221 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

1222

1223 -- Finally fill in the terms or patterns from the unquotes. This

1224 -- happens last so that their holes still exist while elaborating

1225 -- the main quotation.

1226 mapM_ elabUnquote unq

1227 where elabUnquote (n, tm)

1228 = do focus n

1229 elabE (ina { e_qq = False }) fc tm

1230

1231

1232 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"

1233 elab' ina fc (PQuoteName n False nfc) =

1234 do fill $ reflectName n

1235 solve

1236 elab' ina fc (PQuoteName n True nfc) =

1237 do ctxt <- get_context

1238 env <- get_env

1239 case lookupBinder n env of

1240 Just _ -> do fill $ reflectName n

1241 solve

1242 highlightSource nfc (AnnBoundName n False)

1243 Nothing ->

1244 case lookupNameDef n ctxt of

1245 [(n', _)] -> do fill $ reflectName n'

1246 solve

1247 highlightSource nfc (AnnName n' Nothing Nothing Nothing)

1248 [] -> lift . tfail . NoSuchVariable $ n

1249 more -> lift . tfail . CantResolveAlts $ map fst more

1250 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"

1251 elab' ina fc (PHidden t)

1252 | reflection = elab' ina fc t

1253 | otherwise

1254 = do ~(h : hs) <- get_holes

1255 -- Dotting a hole means that either the hole or any outer

1256 -- hole (a hole outside any occurrence of it)

1257 -- must be solvable by unification as well as being filled

1258 -- in directly.

1259 -- Delay dotted things to the end, then when we elaborate them

1260 -- we can check the result against what was inferred

1261 movelast h

1262 ~(h' : hs) <- get_holes

1263 -- If we're at the end anyway, do it now

1264 if h == h' then elabHidden h

1265 else delayElab 10 $ elabHidden h

1266 where

1267 elabHidden h = do hs <- get_holes

1268 when (h `elem` hs) $ do

1269 focus h

1270 dotterm

1271 elab' ina fc t

1272 elab' ina fc (PRunElab fc' tm ns) =

1273 do unless (ElabReflection `elem` idris_language_extensions ist) $

1274 lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")

1275 attack

1276 let elabName = sNS (sUN "Elab") ["Elab", "Reflection", "Language"]

1277 n <- getNameFrom (sMN 0 "tacticScript")

1278 let scriptTy = RApp (Var elabName) (Var unitTy)

1279 claim n scriptTy

1280 focus n

1281 elabUnit <- goal

1282 attack -- to get an extra hole

1283 elab' ina (Just fc') tm

1284 script <- get_guess

1285 fullyElaborated script

1286 solve -- eliminate the hole. Because there are no references, the script is only in the binding

1287 ctxt <- get_context

1288 env <- get_env

1289 (scriptTm, scriptTy) <- lift $ check ctxt [] (forget script)

1290 lift $ converts ctxt env elabUnit scriptTy

1291 env <- get_env

1292 runElabAction info ist (maybe fc' id fc) env script ns

1293 solve

1294 elab' ina fc (PConstSugar constFC tm) =

1295 -- Here we elaborate the contained term, then calculate

1296 -- highlighting for constFC. The highlighting is the

1297 -- highlighting for the outermost constructor of the result of

1298 -- evaluating the elaborated term, if one exists (it always

1299 -- should, but better to fail gracefully for something silly

1300 -- like highlighting info). This is how implicit applications of

1301 -- fromInteger get highlighted.

1302 do saveState -- so we don't pollute the elaborated term

1303 n <- getNameFrom (sMN 0 "cstI")

1304 n' <- getNameFrom (sMN 0 "cstIhole")

1305 g <- forget <$> goal

1306 claim n' g

1307 movelast n'

1308 -- In order to intercept the elaborated value, we need to

1309 -- let-bind it.

1310 attack

1311 letbind n RigW g (Var n')

1312 focus n'

1313 elab' ina fc tm

1314 env <- get_env

1315 ctxt <- get_context

1316 let v = fmap (normaliseAll ctxt env . finalise . binderVal)

1317 (lookupBinder n env)

1318 loadState -- we have the highlighting - re-elaborate the value

1319 elab' ina fc tm

1320 case v of

1321 Just val -> highlightConst constFC val

1322 Nothing -> return ()

1323 where highlightConst fc (P _ n _) =

1324 highlightSource fc (AnnName n Nothing Nothing Nothing)

1325 highlightConst fc (App _ f _) =

1326 highlightConst fc f

1327 highlightConst fc (Constant c) =

1328 highlightSource fc (AnnConst c)

1329 highlightConst _ _ = return ()

1330 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1331

1332 -- delay elaboration of 't', with priority 'pri' until after everything

1333 -- else is done.

1334 -- The delayed things with lower numbered priority will be elaborated

1335 -- first. (In practice, this means delayed alternatives, then PHidden

1336 -- things.)

1337 delayElab pri t

1338 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

1339

1340 -- If the variable in the environment is the scrutinee of the case,

1341 -- and has multiplicity W, keep it available

1342 isScr :: PTerm -> (Name, RigCount, Binder Term) -> (Name, (Bool, Binder Term))

1343 isScr (PRef _ _ n) (n', RigW, b) = (n', (n == n', b))

1344 isScr _ (n', _, b) = (n', (False, b))

1345

1346 caseBlock :: FC -> Name

1347 -> PTerm -- original scrutinee

1348 -> [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]

1349 caseBlock fc n scr env opts

1350 = let args' = findScr env

1351 args = map mkarg (map getNmScr args') in

1352 map (mkClause args) opts

1353

1354 where -- Find the variable we want as the scrutinee and mark it as

1355 -- 'True'. If the scrutinee is available in the environment,

1356 -- match on that otherwise match on the new argument we're adding.

1357 findScr ((n, (True, t)) : xs)

1358 = (n, (True, t)) : scrName n xs

1359 findScr [(n, (_, t))] = [(n, (True, t))]

1360 findScr (x : xs) = x : findScr xs

1361 -- [] can't happen since scrutinee is in the environment!

1362 findScr [] = error "The impossible happened - the scrutinee was not in the environment"

1363

1364 -- To make sure top level pattern name remains in scope, put

1365 -- it at the end of the environment

1366 scrName n [] = []

1367 scrName n [(_, t)] = [(n, t)]

1368 scrName n (x : xs) = x : scrName n xs

1369

1370 getNmScr (n, (s, _)) = (n, s)

1371

1372 mkarg (n, s) = (PRef fc [] n, s)

1373 -- may be shadowed names in the new pattern - so replace the

1374 -- old ones with an _

1375 -- Also, names which don't appear on the rhs should not be

1376 -- fixed on the lhs, or this restricts the kind of matching

1377 -- we can do to non-dependent types.

1378 mkClause args (l, r)

1379 = let args' = map (shadowed (allNamesIn l)) args

1380 args'' = map (implicitable (allNamesIn r ++

1381 keepscrName scr)) args'

1382 lhs = PApp (getFC fc l) (PRef NoFC [] n)

1383 (map (mkLHSarg l) args'') in

1384 PClause (getFC fc l) n lhs [] r []

1385

1386 -- Keep scrutinee available if it's just a name (this makes

1387 -- the names in scope look better when looking at a hole on

1388 -- the rhs of a case)

1389 keepscrName (PRef _ _ n) = [n]

1390 keepscrName _ = []

1391

1392 mkLHSarg l (tm, True) = pexp l

1393 mkLHSarg l (tm, False) = pexp tm

1394

1395 shadowed new (PRef _ _ n, s) | n `elem` new = (Placeholder, s)

1396 shadowed new t = t

1397

1398 implicitable rhs (PRef _ _ n, s) | n `notElem` rhs = (Placeholder, s)

1399 implicitable rhs t = t

1400

1401

1402 getFC d (PApp fc _ _) = fc

1403 getFC d (PRef fc _ _) = fc

1404 getFC d (PAlternative _ _ (x:_)) = getFC d x

1405 getFC d x = d

1406

1407 -- Fail if a term is not yet fully elaborated (e.g. if it contains

1408 -- case block functions that don't yet exist)

1409 fullyElaborated :: Term -> ElabD ()

1410 fullyElaborated (P _ n _) =

1411 do estate <- getAux

1412 case lookup n (case_decls estate) of

1413 Nothing -> return ()

1414 Just _ -> lift . tfail $ ElabScriptStaging n

1415 fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated

1416 fullyElaborated (App _ l r) = fullyElaborated l >> fullyElaborated r

1417 fullyElaborated (Proj t _) = fullyElaborated t

1418 fullyElaborated _ = return ()

1419

1420 -- If the goal type is a "Lazy", then try elaborating via 'Delay'

1421 -- first. We need to do this brute force approach, rather than anything

1422 -- more precise, since there may be various other ambiguities to resolve

1423 -- first.

1424 insertLazy :: ElabCtxt -> PTerm -> ElabD PTerm

1425 insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1426 insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

1427 insertLazy ina (PCoerced t) = return t

1428 -- Don't add a delay to top level pattern variables, since they

1429 -- can be forced on the rhs if needed

1430 insertLazy ina t@(PPatvar _ _) | pattern && not (e_guarded ina) = return t

1431 insertLazy ina t =

1432 do ty <- goal

1433 env <- get_env

1434 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)

1435 let tries = [mkDelay env t, t]

1436 case tyh of

1437 P _ (UN l) _ | l == txt "Delayed"

1438 -> return (PAlternative [] FirstSuccess tries)

1439 _ -> return t

1440 where

1441 mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)

1442 mkDelay env t

1443 = let fc = fileFC "Delay" in

1444 addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] (sUN "Delay"))

1445 [pexp t])

1446

1447

1448 -- Don't put implicit coercions around applications which are marked

1449 -- as '%noImplicit', or around case blocks, otherwise we get exponential

1450 -- blowup especially where there are errors deep in large expressions.

1451 notImplicitable (PApp _ f _) = notImplicitable f

1452 -- TMP HACK no coercing on bind (make this configurable)

1453 notImplicitable (PRef _ _ n)

1454 | [opts] <- lookupCtxt n (idris_flags ist)

1455 = NoImplicit `elem` opts

1456 notImplicitable (PAlternative _ _ as) = any notImplicitable as

1457 -- case is tricky enough without implicit coercions! If they are needed,

1458 -- they can go in the branches separately.

1459 notImplicitable (PCase _ _ _) = True

1460 notImplicitable _ = False

1461

1462 -- Elaboration works more smoothly if we expand function applications

1463 -- to their full arity and elaborate it all at once (better error messages

1464 -- in particular)

1465 expandToArity tm@(PApp fc f a) = do

1466 env <- get_env

1467 case fullApp tm of

1468 -- if f is global, leave it alone because we've already

1469 -- expanded it to the right arity

1470 PApp fc ftm@(PRef _ _ f) args | Just aty <- lookupBinder f env ->

1471 do let a = length (getArgTys (normalise (tt_ctxt ist) env (binderTy aty)))

1472 return (mkPApp fc a ftm args)

1473 _ -> return tm

1474 expandToArity t = return t

1475

1476 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1477 fullApp x = x

1478

1479 -- See if the name is listed as an implicit. If it is, return it, and

1480 -- drop it from the rest of the list

1481 findImplicit :: Name -> [PArg] -> (Maybe PArg, [PArg])

1482 findImplicit n [] = (Nothing, [])

1483 findImplicit n (i@(PImp _ _ _ n' _) : args)

1484 | n == n' = (Just i, args)

1485 findImplicit n (i@(PTacImplicit _ _ n' _ _) : args)

1486 | n == n' = (Just i, args)

1487 findImplicit n (x : xs) = let (arg, rest) = findImplicit n xs in

1488 (arg, x : rest)

1489

1490 insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]

1491 insertScopedImps fc f knowns ty xs =

1492 do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs

1493 doInsert ty xs

1494 where

1495 doInsert ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs

1496 | (Just arg, xs') <- findImplicit n xs,

1497 not (toplevel_imp i)

1498 = liftM (arg :) (doInsert sc xs')

1499 | tcimplementation i && not (toplevel_imp i)

1500 = liftM (pimp n (PResolveTC fc) True :) (doInsert sc xs)

1501 | not (toplevel_imp i)

1502 = liftM (pimp n Placeholder True :) (doInsert sc xs)

1503 doInsert (Bind n (Pi _ _ _ _) sc) (x : xs)

1504 = liftM (x :) (doInsert sc xs)

1505 doInsert ty xs = return xs

1506

1507 -- Any implicit in the application needs to have the name of a

1508 -- scoped implicit or a top level implicit, otherwise report an error

1509 checkKnownImplicit ns imp@(PImp{})

1510 | pname imp `elem` ns = return ()

1511 | otherwise = lift $ tfail $ At fc $ UnknownImplicit (pname imp) f

1512 checkKnownImplicit ns _ = return ()

1513

1514 insertImpLam ina t =

1515 do ty <- goal

1516 env <- get_env

1517 let ty' = normalise (tt_ctxt ist) env ty

1518 addLam ty' t

1519 where

1520 -- just one level at a time

1521 addLam goal@(Bind n (Pi _ (Just _) _ _) sc) t =

1522 do impn <- unique_hole n -- (sMN 0 "scoped_imp")

1523 return (PLam emptyFC impn NoFC Placeholder t)

1524 addLam _ t = return t

1525

1526 insertCoerce ina t@(PCase _ _ _) = return t

1527 insertCoerce ina t | notImplicitable t = return t

1528 insertCoerce ina t =

1529 do ty <- goal

1530 -- Check for possible coercions to get to the goal

1531 -- and add them as 'alternatives'

1532 env <- get_env

1533 let ty' = normalise (tt_ctxt ist) env ty

1534 let cs = getCoercionsTo ist ty'

1535 let t' = case (t, cs) of

1536 (PCoerced tm, _) -> tm

1537 (_, []) -> t

1538 (_, cs) -> PAlternative [] TryImplicit

1539 (t : map (mkCoerce env t) cs)

1540 return t'

1541 where

1542 mkCoerce env (PAlternative ms aty tms) n

1543 = PAlternative ms aty (map (\t -> mkCoerce env t n) tms)

1544 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1545 addImplBound ist (map fstEnv env)

1546 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

1547

1548 elabRef :: ElabCtxt -> Maybe FC -> FC -> [FC] -> Name -> PTerm -> ElabD ()

1549 elabRef ina fc' fc hls n tm =

1550 do fty <- get_type (Var n) -- check for implicits

1551 ctxt <- get_context

1552 env <- get_env

1553 a' <- insertScopedImps fc n [] (normalise ctxt env fty) []

1554 if null a'

1555 then erun fc $

1556 do apply (Var n) []

1557 hilite <- findHighlight n

1558 solve

1559 mapM_ (uncurry highlightSource) $

1560 (fc, hilite) : map (\f -> (f, hilite)) hls

1561 else elab' ina fc' (PApp fc tm [])

1562

1563 -- | Elaborate the arguments to a function

1564 elabArgs :: IState -- ^ The current Idris state

1565 -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)

1566 -> [Bool]

1567 -> FC -- ^ Source location

1568 -> Bool

1569 -> Name -- ^ Name of the function being applied

1570 -> [((Name, Name), Bool)] -- ^ (Argument Name, Hole Name, unmatchable)

1571 -> Bool -- ^ under a 'force'

1572 -> [PTerm] -- ^ argument

1573 -> ElabD ()

1574 elabArgs ist ina failed fc retry f [] force _ = return ()

1575 elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args)

1576 = do hs <- get_holes

1577 if holeName `elem` hs then

1578 do focus holeName

1579 case t of

1580 Placeholder -> do movelast holeName

1581 elabArgs ist ina failed fc r f ns force args

1582 _ -> elabArg t

1583 else elabArgs ist ina failed fc r f ns force args

1584 where elabArg t =

1585 do -- solveAutos ist fn False

1586 now_elaborating fc f argName

1587 wrapErr f argName $ do

1588 hs <- get_holes

1589 tm <- get_term

1590 -- No coercing under an explicit Force (or it can Force/Delay

1591 -- recursively!)

1592 let elab = if force then elab' else elabE

1593 failed' <- -- trace (show (n, t, hs, tm)) $

1594 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

1595 do focus holeName;

1596 g <- goal

1597 -- Can't pattern match on polymorphic goals

1598 poly <- goal_polymorphic

1599 ulog <- getUnifyLog

1600 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

1601 elab (ina { e_nomatching = unm && poly }) (Just fc) t

1602 return failed

1603 done_elaborating_arg f argName

1604 elabArgs ist ina failed fc r f ns force args

1605 wrapErr f argName action =

1606 do elabState <- get

1607 while <- elaborating_app

1608 let while' = map (\(x, y, z)-> (y, z)) while

1609 (result, newState) <- case runStateT action elabState of

1610 OK (res, newState) -> return (res, newState)

1611 Error e -> do done_elaborating_arg f argName

1612 lift (tfail (elaboratingArgErr while' e))

1613 put newState

1614 return result

1615 elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =

1616 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole

1617

1618 addAutoBind :: Plicity -> Name -> ElabD ()

1619 addAutoBind (Imp _ _ _ _ False _) n

1620 = updateAux (\est -> est { auto_binds = n : auto_binds est })

1621 addAutoBind _ _ = return ()

1622

1623 testImplicitWarning :: FC -> Name -> Type -> ElabD ()

1624 testImplicitWarning fc n goal

1625 | implicitable n && emode == ETyDecl

1626 = do env <- get_env

1627 est <- getAux

1628 when (n `elem` auto_binds est) $

1629 tryUnify env (lookupTyName n (tt_ctxt ist))

1630 | otherwise = return ()

1631 where

1632 tryUnify env [] = return ()

1633 tryUnify env ((nm, ty) : ts)

1634 = do inj <- get_inj

1635 hs <- get_holes

1636 case unify (tt_ctxt ist) env (ty, Nothing) (goal, Nothing)

1637 inj hs [] [] of

1638 OK _ ->

1639 updateAux (\est -> est { implicit_warnings =

1640 (fc, nm) : implicit_warnings est })

1641 _ -> tryUnify env ts

1642

1643-- For every alternative, look at the function at the head. Automatically resolve

1644-- any nested alternatives where that function is also at the head

1645

1646pruneAlt :: [PTerm] -> [PTerm]

1647pruneAlt xs = map prune xs

1648 where

1649 prune (PApp fc1 (PRef fc2 hls f) as)

1650 = PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as)

1651 prune t = t

1652

1653 choose f (PAlternative ms a as)

1654 = let as' = fmap (choose f) as

1655 fs = filter (headIs f) as' in

1656 case fs of

1657 [a] -> a

1658 _ -> PAlternative ms a as'

1659

1660 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

1661 choose f t = t

1662

1663 headIs f (PApp _ (PRef _ _ f') _) = f == f'

1664 headIs f (PApp _ f' _) = headIs f f'

1665 headIs f _ = True -- keep if it's not an application

1666

1667-- | Use the local elab context to work out the highlighting for a name

1668findHighlight :: Name -> ElabD OutputAnnotation

1669findHighlight n = do ctxt <- get_context

1670 env <- get_env

1671 case lookupBinder n env of

1672 Just _ -> return $ AnnBoundName n False

1673 Nothing -> case lookupTyExact n ctxt of

1674 Just _ -> return $ AnnName n Nothing Nothing Nothing

1675 Nothing -> lift . tfail . InternalMsg $

1676 "Can't find name " ++ show n

1677

1678-- Try again to solve auto implicits

1679solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()

1680solveAuto ist fn ambigok (n, failc)

1681 = do hs <- get_holes

1682 when (not (null hs)) $ do

1683 env <- get_env

1684 g <- goal

1685 handleError cantsolve (when (n `elem` hs) $ do

1686 focus n

1687 isg <- is_guess -- if it's a guess, we're working on it recursively, so stop

1688 when (not isg) $

1689 proofSearch' ist True ambigok 100 True Nothing fn [] [])

1690 (lift $ Error (addLoc failc

1691 (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env))))

1692 return ()

1693 where addLoc (FailContext fc f x : prev) err

1694 = At fc (ElaboratingArg f x

1695 (map (\(FailContext _ f' x') -> (f', x')) prev) err)

1696 addLoc _ err = err

1697

1698 cantsolve (CantSolveGoal _ _) = True

1699 cantsolve (InternalMsg _) = True

1700 cantsolve (At _ e) = cantsolve e

1701 cantsolve (Elaborating _ _ _ e) = cantsolve e

1702 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e

1703 cantsolve _ = False

1704

1705solveAutos :: IState -> Name -> Bool -> ElabD ()

1706solveAutos ist fn ambigok

1707 = do autos <- get_autos

1708 mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)

1709

1710-- Return true if the given error suggests an interface failure is

1711-- recoverable

1712tcRecoverable :: ElabMode -> Err -> Bool

1713tcRecoverable ERHS (CantResolve f g _) = f

1714tcRecoverable ETyDecl (CantResolve f g _) = f

1715tcRecoverable e (ElaboratingArg _ _ _ err) = tcRecoverable e err

1716tcRecoverable e (At _ err) = tcRecoverable e err

1717tcRecoverable _ _ = True

1718

1719trivial' ist

1720 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1721trivialHoles' psn h ist

1722 = trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1723proofSearch' ist rec ambigok depth prv top n psns hints

1724 = do unifyProblems

1725 proofSearch rec prv ambigok (not prv) depth

1726 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist

1727resolveTC' di mv depth tm n ist

1728 = resolveTC di mv depth tm n (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1729

1730collectDeferred :: Maybe Name -> [Name] -> Context ->

1731 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

1732collectDeferred top casenames ctxt tm = cd [] tm

1733 where

1734 cd env (Bind n (GHole i psns t) app) =

1735 do ds <- get

1736 t' <- collectDeferred top casenames ctxt t

1737 when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])

1738 cd env app

1739 cd env (Bind n b t)

1740 = do b' <- cdb b

1741 t' <- cd ((n, b) : env) t

1742 return (Bind n b' t')

1743 where

1744 cdb (Let rig t v) = liftM2 (Let rig) (cd env t) (cd env v)

1745 cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

1746 cdb b = do ty' <- cd env (binderTy b)

1747 return (b { binderTy = ty' })

1748 cd env (App s f a) = liftM2 (App s) (cd env f)

1749 (cd env a)

1750 cd env t = return t

1751

1752-- | Compute the appropriate name for a top-level metavariable

1753metavarName :: [String] -> Name -> Name

1754metavarName _ n@(NS _ _) = n

1755metavarName (ns@(_:_)) n = sNS n ns

1756metavarName _ n = n

1757

1758runElabAction :: ElabInfo -> IState -> FC -> Env -> Term -> [String] -> ElabD Term

1759runElabAction info ist fc env tm ns = do tm' <- eval tm

1760 runTacTm tm'

1761

1762 where

1763 eval tm = do ctxt <- get_context

1764 return $ normaliseAll ctxt env (finalise tm)

1765

1766 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)

1767

1768 patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)

1769 patvars ns (Bind n (PVar _ t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)

1770 patvars ns tm = (ns, tm)

1771

1772 pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)

1773 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs

1774

1775 requireError :: Err -> ElabD a -> ElabD ()

1776 requireError orErr elab =

1777 do state <- get

1778 case runStateT elab state of

1779 OK (_, state') -> lift (tfail orErr)

1780 Error e -> return ()

1781

1782 -- create a fake TT term for the LHS of an impossible case

1783 fakeTT :: Raw -> Term

1784 fakeTT (Var n) =

1785 case lookupNameDef n (tt_ctxt ist) of

1786 [(n', TyDecl nt _)] -> P nt n' Erased

1787 _ -> P Ref n Erased

1788 fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)

1789 fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)

1790 fakeTT RType = TType (UVar [] (-1))

1791 fakeTT (RUType u) = UType u

1792 fakeTT (RConstant c) = Constant c

1793

1794 defineFunction :: RFunDefn Raw -> ElabD ()

1795 defineFunction (RDefineFun n clauses) =

1796 do ctxt <- get_context

1797 ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt

1798 let info = CaseInfo True True False -- TODO document and figure out

1799 clauses' <- forM clauses (\case

1800 RMkFunClause lhs rhs ->

1801 do (lhs', lty) <- lift $ check ctxt [] lhs

1802 (rhs', rty) <- lift $ check ctxt [] rhs

1803 lift $ converts ctxt [] lty rty

1804 return $ Right (lhs', rhs')

1805 RMkImpossibleClause lhs ->

1806 do requireError (Msg "Not an impossible case") . lift $

1807 check ctxt [] lhs

1808 return $ Left (fakeTT lhs))

1809 let clauses'' = map (\case Right c -> pullVars c

1810 Left lhs -> let (ns, lhs') = patvars [] lhs

1811 in (ns, lhs', Impossible))

1812 clauses'

1813 let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''

1814 let argtys = map (\x -> (x, isCanonical x ctxt))

1815 (map snd (getArgTys (normalise ctxt [] ty)))

1816 ctxt'<- lift $

1817 addCasedef n (const [])

1818 info False (STerm Erased)

1819 True False -- TODO what are these?

1820 argtys [] -- TODO inaccessible types

1821 clauses'

1822 clauses'''

1823 clauses'''

1824 ty

1825 ctxt

1826 set_context ctxt'

1827 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1828 return ()

1829

1830

1831 checkClosed :: Raw -> Elab' aux (Term, Type)

1832 checkClosed tm = do ctxt <- get_context

1833 (val, ty) <- lift $ check ctxt [] tm

1834 return $! (finalise val, finalise ty)

1835

1836 -- | Add another argument to a Pi

1837 mkPi :: RFunArg -> Raw -> Raw

1838 mkPi arg rTy = RBind (argName arg) (Pi RigW Nothing (argTy arg) (RUType AllTypes)) rTy

1839

1840 mustBeType ctxt tm ty =

1841 case normaliseAll ctxt [] (finalise ty) of

1842 UType _ -> return ()

1843 TType _ -> return ()

1844 ty' -> lift . tfail . InternalMsg $

1845 show tm ++ " is not a type: it's " ++ show ty'

1846

1847 mustNotBeDefined ctxt n =

1848 case lookupDefExact n ctxt of

1849 Just _ -> lift . tfail . InternalMsg $

1850 show n ++ " is already defined."

1851 Nothing -> return ()

1852

1853 -- | Prepare a constructor to be added to a datatype being defined here

1854 prepareConstructor :: Name -> RConstructorDefn -> ElabD (Name, [PArg], Type)

1855 prepareConstructor tyn (RConstructor cn args resTy) =

1856 do ctxt <- get_context

1857 -- ensure the constructor name is not qualified, and

1858 -- construct a qualified one

1859 notQualified cn

1860 let qcn = qualify cn

1861

1862 -- ensure that the constructor name is not defined already

1863 mustNotBeDefined ctxt qcn

1864

1865 -- construct the actual type for the constructor

1866 let cty = foldr mkPi resTy args

1867 (checkedTy, ctyTy) <- lift $ check ctxt [] cty

1868 mustBeType ctxt checkedTy ctyTy

1869

1870 -- ensure that the constructor builds the right family

1871 case unApply (getRetTy (normaliseAll ctxt [] (finalise checkedTy))) of

1872 (P _ n _, _) | n == tyn -> return ()

1873 t -> lift . tfail . Msg $ "The constructor " ++ show cn ++

1874 " doesn't construct " ++ show tyn ++

1875 " (return type is " ++ show t ++ ")"

1876

1877 -- add temporary type declaration for constructor (so it can

1878 -- occur in later constructor types)

1879 set_context (addTyDecl qcn (DCon 0 0 False) checkedTy ctxt)

1880

1881 -- Save the implicits for high-level Idris

1882 let impls = map rFunArgToPArg args

1883

1884 return (qcn, impls, checkedTy)

1885

1886 where

1887 notQualified (NS _ _) = lift . tfail . Msg $ "Constructor names may not be qualified"

1888 notQualified _ = return ()

1889

1890 qualify n = case tyn of

1891 (NS _ ns) -> NS n ns

1892 _ -> n

1893

1894 getRetTy :: Type -> Type

1895 getRetTy (Bind _ (Pi _ _ _ _) sc) = getRetTy sc

1896 getRetTy ty = ty

1897

1898 elabScriptStuck :: Term -> ElabD a

1899 elabScriptStuck x = lift . tfail $ ElabScriptStuck x

1900

1901

1902 -- Should be dependent

1903 tacTmArgs :: Int -> Term -> [Term] -> ElabD [Term]

1904 tacTmArgs l t args | length args == l = return args

1905 | otherwise = elabScriptStuck t -- Probably should be an argument size mismatch internal error

1906

1907

1908 -- | Do a step in the reflected elaborator monad. The input is the

1909 -- step, the output is the (reflected) term returned.

1910 runTacTm :: Term -> ElabD Term

1911 runTacTm tac@(unApply -> (P _ n _, args))

1912 | n == tacN "Prim__Solve"

1913 = do ~[] <- tacTmArgs 0 tac args -- patterns are irrefutable because `tacTmArgs` returns lists of exactly the size given to it as first argument

1914 solve

1915 returnUnit

1916 | n == tacN "Prim__Goal"

1917 = do ~[] <- tacTmArgs 0 tac args

1918 hs <- get_holes

1919 case hs of

1920 (h : _) -> do t <- goal

1921 fmap fst . checkClosed $

1922 rawPair (Var (reflm "TTName"), Var (reflm "TT"))

1923 (reflectName h, reflect t)

1924 [] -> lift . tfail . Msg $

1925 "Elaboration is complete. There are no goals."

1926

1927 | n == tacN "Prim__Holes"

1928 = do ~[] <- tacTmArgs 0 tac args

1929 hs <- get_holes

1930 fmap fst . checkClosed $

1931 mkList (Var $ reflm "TTName") (map reflectName hs)

1932 | n == tacN "Prim__Guess"

1933 = do ~[] <- tacTmArgs 0 tac args

1934 g <- get_guess

1935 fmap fst . checkClosed $ reflect g

1936 | n == tacN "Prim__LookupTy"

1937 = do ~[name] <- tacTmArgs 1 tac args

1938 n' <- reifyTTName name

1939 ctxt <- get_context

1940 let getNameTypeAndType = \case Function ty _ -> (Ref, ty)

1941 TyDecl nt ty -> (nt, ty)

1942 Operator ty _ _ -> (Ref, ty)

1943 CaseOp _ ty _ _ _ _ -> (Ref, ty)

1944 -- Idris tuples nest to the right

1945 reflectTriple (x, y, z) =

1946 raw_apply (Var pairCon) [ Var (reflm "TTName")

1947 , raw_apply (Var pairTy) [Var (reflm "NameType"), Var (reflm "TT")]

1948 , x

1949 , raw_apply (Var pairCon) [ Var (reflm "NameType"), Var (reflm "TT")

1950 , y, z]]

1951 let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)

1952 | (n, def) <- lookupNameDef n' ctxt

1953 , let (nt, ty) = getNameTypeAndType def ]

1954 fmap fst . checkClosed $

1955 rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")

1956 , raw_apply (Var pairTy) [ Var (reflm "NameType")

1957 , Var (reflm "TT")]])

1958 defs

1959 | n == tacN "Prim__LookupDatatype"

1960 = do ~[name] <- tacTmArgs 1 tac args

1961 n' <- reifyTTName name

1962 datatypes <- get_datatypes

1963 ctxt <- get_context

1964 fmap fst . checkClosed $

1965 rawList (Var (tacN "Datatype"))

1966 (map reflectDatatype (buildDatatypes ist n'))

1967 | n == tacN "Prim__LookupFunDefn"

1968 = do ~[name] <- tacTmArgs 1 tac args

1969 n' <- reifyTTName name

1970 fmap fst . checkClosed $

1971 rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))

1972 (map reflectFunDefn (buildFunDefns ist n'))

1973 | n == tacN "Prim__LookupArgs"

1974 = do ~[name] <- tacTmArgs 1 tac args

1975 n' <- reifyTTName name

1976 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1977 listFunArg = RApp listTy (Var (tacN "FunArg"))

1978 -- Idris tuples nest to the right

1979 let reflectTriple (x, y, z) =

1980 raw_apply (Var pairCon) [ Var (reflm "TTName")

1981 , raw_apply (Var pairTy) [listFunArg, Var (reflm "Raw")]

1982 , x

1983 , raw_apply (Var pairCon) [listFunArg, Var (reflm "Raw")

1984 , y, z]]

1985 let out =

1986 [ reflectTriple (reflectName fn, reflectList (Var (tacN "FunArg")) (map reflectArg args), reflectRaw res)

1987 | (fn, pargs) <- lookupCtxtName n' (idris_implicits ist)

1988 , (args, res) <- getArgs pargs . forget <$>

1989 maybeToList (lookupTyExact fn (tt_ctxt ist))

1990 ]

1991

1992 fmap fst . checkClosed $

1993 rawList (raw_apply (Var pairTy) [Var (reflm "TTName")

1994 , raw_apply (Var pairTy) [ RApp listTy

1995 (Var (tacN "FunArg"))

1996 , Var (reflm "Raw")]])

1997 out

1998 | n == tacN "Prim__SourceLocation"

1999 = do ~[] <- tacTmArgs 0 tac args

2000 fmap fst . checkClosed $

2001 reflectFC fc

2002 | n == tacN "Prim__Namespace"

2003 = do ~[] <- tacTmArgs 0 tac args

2004 fmap fst . checkClosed $

2005 rawList (RConstant StrType) (map (RConstant . Str) ns)

2006 | n == tacN "Prim__Env"

2007 = do ~[] <- tacTmArgs 0 tac args

2008 env <- get_env

2009 fmap fst . checkClosed $ reflectEnv env

2010 | n == tacN "Prim__Fail"

2011 = do ~[_a, errs] <- tacTmArgs 2 tac args

2012 errs' <- eval errs

2013 parts <- reifyReportParts errs'

2014 lift . tfail $ ReflectionError [parts] (Msg "")

2015 | n == tacN "Prim__PureElab"

2016 = do ~[_a, tm] <- tacTmArgs 2 tac args

2017 return tm

2018 | n == tacN "Prim__BindElab"

2019 = do ~[_a, _b, first, andThen] <- tacTmArgs 4 tac args

2020 first' <- eval first

2021 res <- eval =<< runTacTm first'

2022 next <- eval (App Complete andThen res)

2023 runTacTm next

2024 | n == tacN "Prim__Try"

2025 = do ~[_a, first, alt] <- tacTmArgs 3 tac args

2026 first' <- eval first

2027 alt' <- eval alt

2028 try' (runTacTm first') (runTacTm alt') True

2029 | n == tacN "Prim__TryCatch"

2030 = do ~[_a, first, f] <- tacTmArgs 3 tac args

2031 first' <- eval first

2032 f' <- eval f

2033 tryCatch (runTacTm first') $ \err ->

2034 do (err', _) <- checkClosed (reflectErr err)

2035 f' <- eval (App Complete f err')

2036 runTacTm f'

2037 | n == tacN "Prim__Fill"

2038 = do ~[raw] <- tacTmArgs 1 tac args

2039 raw' <- reifyRaw =<< eval raw

2040 apply raw' []

2041 returnUnit

2042 | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"

2043 = do ~[raw, argSpec] <- tacTmArgs 2 tac args

2044 raw' <- reifyRaw =<< eval raw

2045 argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec

2046 let op = if n == tacN "Prim__Apply"

2047 then apply

2048 else match_apply

2049 ns <- op raw' argSpec'

2050 fmap fst . checkClosed $

2051 rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TTName"))

2052 [ rawPair (Var $ reflm "TTName", Var $ reflm "TTName")

2053 (reflectName n1, reflectName n2)

2054 | (n1, n2) <- ns

2055 ]

2056 | n == tacN "Prim__Gensym"

2057 = do ~[hint] <- tacTmArgs 1 tac args

2058 hintStr <- eval hint

2059 case hintStr of

2060 Constant (Str h) -> do

2061 n <- getNameFrom (sMN 0 h)

2062 fmap fst $ get_type_val (reflectName n)

2063 _ -> fail "no hint"

2064 | n == tacN "Prim__Claim"

2065 = do ~[n, ty] <- tacTmArgs 2 tac args

2066 n' <- reifyTTName n

2067 ty' <- reifyRaw ty

2068 claim n' ty'

2069 returnUnit

2070 | n == tacN "Prim__Check"

2071 = do ~[env', raw] <- tacTmArgs 2 tac args

2072 env <- reifyEnv env'

2073 raw' <- reifyRaw =<< eval raw

2074 ctxt <- get_context

2075 (tm, ty) <- lift $ check ctxt env raw'

2076 fmap fst . checkClosed $

2077 rawPair (Var (reflm "TT"), Var (reflm "TT"))

2078 (reflect tm, reflect ty)

2079 | n == tacN "Prim__Attack"

2080 = do ~[] <- tacTmArgs 0 tac args

2081 attack

2082 returnUnit

2083 | n == tacN "Prim__Rewrite"

2084 = do ~[rule] <- tacTmArgs 1 tac args

2085 r <- reifyRaw rule

2086 rewrite r

2087 returnUnit

2088 | n == tacN "Prim__Focus"

2089 = do ~[what] <- tacTmArgs 1 tac args

2090 n' <- reifyTTName what

2091 hs <- get_holes

2092 if elem n' hs

2093 then focus n' >> returnUnit

2094 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"

2095 | n == tacN "Prim__Unfocus"

2096 = do ~[what] <- tacTmArgs 1 tac args

2097 n' <- reifyTTName what

2098 movelast n'

2099 returnUnit

2100 | n == tacN "Prim__Intro"

2101 = do ~[mn] <- tacTmArgs 1 tac args

2102 n <- case fromTTMaybe mn of

2103 Nothing -> return Nothing

2104 Just name -> fmap Just $ reifyTTName name

2105 intro n

2106 returnUnit

2107 | n == tacN "Prim__Forall"

2108 = do ~[n, ty] <- tacTmArgs 2 tac args

2109 n' <- reifyTTName n

2110 ty' <- reifyRaw ty

2111 forall n' RigW Nothing ty'

2112 returnUnit

2113 | n == tacN "Prim__PatVar"

2114 = do ~[n] <- tacTmArgs 1 tac args

2115 n' <- reifyTTName n

2116 patvar' n'

2117 returnUnit

2118 | n == tacN "Prim__PatBind"

2119 = do ~[n] <- tacTmArgs 1 tac args

2120 n' <- reifyTTName n

2121 patbind n' RigW

2122 returnUnit

2123 | n == tacN "Prim__LetBind"

2124 = do ~[n, ty, tm] <- tacTmArgs 3 tac args

2125 n' <- reifyTTName n

2126 ty' <- reifyRaw ty

2127 tm' <- reifyRaw tm

2128 letbind n' RigW ty' tm'

2129 returnUnit

2130 | n == tacN "Prim__Compute"

2131 = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit

2132 | n == tacN "Prim__Normalise"

2133 = do ~[env, tm] <- tacTmArgs 2 tac args

2134 env' <- reifyEnv env

2135 tm' <- reifyTT tm

2136 ctxt <- get_context

2137 let out = normaliseAll ctxt env' (finalise tm')

2138 fmap fst . checkClosed $ reflect out

2139 | n == tacN "Prim__Whnf"

2140 = do ~[tm] <- tacTmArgs 1 tac args

2141 tm' <- reifyTT tm

2142 ctxt <- get_context

2143 fmap fst . checkClosed . reflect $ whnf ctxt [] tm'

2144 | n == tacN "Prim__Converts"

2145 = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args

2146 env' <- reifyEnv env

2147 tm1' <- reifyTT tm1

2148 tm2' <- reifyTT tm2

2149 ctxt <- get_context

2150 lift $ converts ctxt env' tm1' tm2'

2151 returnUnit

2152 | n == tacN "Prim__DeclareType"

2153 = do ~[decl] <- tacTmArgs 1 tac args

2154 (RDeclare n args res) <- reifyTyDecl decl

2155 ctxt <- get_context

2156 let rty = foldr mkPi res args

2157 (checked, ty') <- lift $ check ctxt [] rty

2158 mustBeType ctxt checked ty'

2159 mustNotBeDefined ctxt n

2160 let decl = TyDecl Ref checked

2161 ctxt' = addCtxtDef n decl ctxt

2162 set_context ctxt'

2163 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :

2164 new_tyDecls e }

2165 returnUnit

2166 | n == tacN "Prim__DefineFunction"

2167 = do ~[decl] <- tacTmArgs 1 tac args

2168 defn <- reifyFunDefn decl

2169 defineFunction defn

2170 returnUnit

2171 | n == tacN "Prim__DeclareDatatype"

2172 = do ~[decl] <- tacTmArgs 1 tac args

2173 RDeclare n args resTy <- reifyTyDecl decl

2174 ctxt <- get_context

2175 let tcTy = foldr mkPi resTy args

2176 (checked, ty') <- lift $ check ctxt [] tcTy

2177 mustBeType ctxt checked ty'

2178 mustNotBeDefined ctxt n

2179 let ctxt' = addTyDecl n (TCon 0 0) checked ctxt

2180 set_context ctxt'

2181 updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }

2182 returnUnit

2183 | n == tacN "Prim__DefineDatatype"

2184 = do ~[defn] <- tacTmArgs 1 tac args

2185 RDefineDatatype n ctors <- reifyRDataDefn defn

2186 ctxt <- get_context

2187 tyconTy <- case lookupTyExact n ctxt of

2188 Just t -> return t

2189 Nothing -> lift . tfail . Msg $ "Type not previously declared"

2190 datatypes <- get_datatypes

2191 case lookupCtxtName n datatypes of

2192 [] -> return ()

2193 _ -> lift . tfail . Msg $ show n ++ " is already defined as a datatype."

2194 -- Prepare the constructors

2195 ctors' <- mapM (prepareConstructor n) ctors

2196 ttag <- do ES (ps, aux) str prev <- get

2197 let i = global_nextname ps

2198 put $ ES (ps { global_nextname = global_nextname ps + 1 },

2199 aux)

2200 str

2201 prev

2202 return i

2203 let ctxt' = addDatatype (Data n ttag tyconTy False (map (\(cn, _, cty) -> (cn, cty)) ctors')) ctxt

2204 set_context ctxt'

2205 -- the rest happens in a bit

2206 updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }

2207 returnUnit

2208 | n == tacN "Prim__AddImplementation"

2209 = do ~[cls, impl] <- tacTmArgs 2 tac args

2210 interfaceName <- reifyTTName cls

2211 implName <- reifyTTName impl

2212 updateAux $ \e -> e { new_tyDecls = RAddImplementation interfaceName implName :

2213 new_tyDecls e }

2214 returnUnit

2215 | n == tacN "Prim__IsTCName"

2216 = do ~[n] <- tacTmArgs 1 tac args

2217 n' <- reifyTTName n

2218 case lookupCtxtExact n' (idris_interfaces ist) of

2219 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])

2220 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])

2221 | n == tacN "Prim__ResolveTC"

2222 = do ~[fn] <- tacTmArgs 1 tac args

2223 g <- goal

2224 fn <- reifyTTName fn

2225 resolveTC' False True 100 g fn ist

2226 returnUnit

2227 | n == tacN "Prim__Search"

2228 = do ~[depth, hints] <- tacTmArgs 2 tac args

2229 d <- eval depth

2230 hints' <- eval hints

2231 case (d, unList hints') of

2232 (Constant (I i), Just hs) ->

2233 do actualHints <- mapM reifyTTName hs

2234 unifyProblems

2235 let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")

2236 proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist

2237 returnUnit

2238 (Constant (I _), Nothing ) ->

2239 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'

2240 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d

2241 | n == tacN "Prim__RecursiveElab"

2242 = do ~[goal, script] <- tacTmArgs 2 tac args

2243 goal' <- reifyRaw goal

2244 ctxt <- get_context

2245 script <- eval script

2246 (goalTT, goalTy) <- lift $ check ctxt [] goal'

2247 lift $ isType ctxt [] goalTy

2248 recH <- getNameFrom (sMN 0 "recElabHole")

2249 aux <- getAux

2250 datatypes <- get_datatypes

2251 env <- get_env

2252 g_next <- get_global_nextname

2253

2254 (ctxt', ES (p, aux') _ _) <-

2255 do (ES (current_p, _) _ _) <- get

2256 lift $ runElab aux

2257 (do runElabAction info ist fc [] script ns

2258 ctxt' <- get_context

2259 return ctxt')

2260 ((newProof recH (constraintNS info) ctxt datatypes g_next goalTT)

2261 { nextname = nextname current_p })

2262 set_context ctxt'

2263

2264 let tm_out = getProofTerm (pterm p)

2265 do (ES (prf, _) s e) <- get

2266 let p' = prf { nextname = nextname p

2267 , global_nextname = global_nextname p

2268 }

2269 put (ES (p', aux') s e)

2270 env' <- get_env

2271 (tm, ty, _) <- lift $ recheck (constraintNS info) ctxt' env (forget tm_out) tm_out

2272 let (tm', ty') = (reflect tm, reflect ty)

2273 fmap fst . checkClosed $

2274 rawPair (Var $ reflm "TT", Var $ reflm "TT")

2275 (tm', ty')

2276 | n == tacN "Prim__Metavar"

2277 = do ~[n] <- tacTmArgs 1 tac args

2278 n' <- reifyTTName n

2279 ctxt <- get_context

2280 ptm <- get_term

2281 -- See documentation above in the elab case for PMetavar

2282 let unique_used = getUniqueUsed ctxt ptm

2283 let lin_used = getLinearUsed ctxt ptm

2284 let mvn = metavarName ns n'

2285 attack

2286 defer unique_used lin_used mvn

2287 solve

2288 returnUnit

2289 | n == tacN "Prim__Fixity"

2290 = do ~[op'] <- tacTmArgs 1 tac args

2291 opTm <- eval op'

2292 case opTm of

2293 Constant (Str op) ->

2294 let opChars = ":!#$%&*+./<=>?@\\^|-~"

2295 invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]

2296 fixities = idris_infixes ist

2297 in if not (all (flip elem opChars) op) || elem op invalidOperators

2298 then lift . tfail . Msg $ "'" ++ op ++ "' is not a valid operator name."

2299 else case nub [f | Fix f someOp <- fixities, someOp == op] of

2300 [] -> lift . tfail . Msg $ "No fixity found for operator '" ++ op ++ "'."

2301 [f] -> fmap fst . checkClosed $ reflectFixity f

2302 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many

2303 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm

2304 | n == tacN "Prim__Debug"

2305 = do ~[ty, msg] <- tacTmArgs 2 tac args

2306 msg' <- eval msg

2307 parts <- reifyReportParts msg

2308 debugElaborator parts

2309 runTacTm x = elabScriptStuck x

2310

2311-- Running tactics directly

2312-- if a tactic adds unification problems, return an error

2313

2314runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()

2315runTac autoSolve ist perhapsFC fn tac

2316 = do env <- get_env

2317 g <- goal

2318 let tac' = fmap (addImplBound ist (map fstEnv env)) tac

2319 if autoSolve

2320 then runT tac'

2321 else no_errors (runT tac')

2322 (Just (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env)))

2323 where

2324 runT (Intro []) = do g <- goal

2325 attack; intro (bname g)

2326 where

2327 bname (Bind n _ _) = Just n

2328 bname _ = Nothing

2329 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

2330 runT Intros = do g <- goal

2331 attack;

2332 intro (bname g)

2333 try' (runT Intros)

2334 (return ()) True

2335 where

2336 bname (Bind n _ _) = Just n

2337 bname _ = Nothing

2338 runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm

2339 when autoSolve solveAll

2340 runT (MatchRefine fn)

2341 = do fnimps <-

2342 case lookupCtxtName fn (idris_implicits ist) of

2343 [] -> do a <- envArgs fn

2344 return [(fn, a)]

2345 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)

2346 let tacs = map (\ (fn', imps) ->

2347 (match_apply (Var fn') (map (\x -> (x, 0)) imps),

2348 fn')) fnimps

2349 tryAll tacs

2350 when autoSolve solveAll

2351 where envArgs n = do e <- get_env

2352 case lookupBinder n e of

2353 Just t -> return $ map (const False)

2354 (getArgTys (binderTy t))

2355 _ -> return []

2356 runT (Refine fn [])

2357 = do fnimps <-

2358 case lookupCtxtName fn (idris_implicits ist) of

2359 [] -> do a <- envArgs fn

2360 return [(fn, a)]

2361 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)

2362 let tacs = map (\ (fn', imps) ->

2363 (apply (Var fn') (map (\x -> (x, 0)) imps),

2364 fn')) fnimps

2365 tryAll tacs

2366 when autoSolve solveAll

2367 where isImp (PImp _ _ _ _ _) = True

2368 isImp _ = False

2369 envArgs n = do e <- get_env

2370 case lookupBinder n e of

2371 Just t -> return $ map (const False)

2372 (getArgTys (binderTy t))

2373 _ -> return []

2374 runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)

2375 when autoSolve solveAll

2376 runT DoUnify = do unify_all

2377 when autoSolve solveAll

2378 runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal")

2379 claim tmHole RType

2380 claim n (Var tmHole)

2381 focus tmHole

2382 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2383 focus n

2384 runT (Equiv tm) -- let bind tm, then

2385 = do attack

2386 tyn <- getNameFrom (sMN 0 "ety")

2387 claim tyn RType

2388 valn <- getNameFrom (sMN 0 "eqval")

2389 claim valn (Var tyn)

2390 letn <- getNameFrom (sMN 0 "equiv_val")

2391 letbind letn RigW (Var tyn) (Var valn)

2392 focus tyn

2393 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2394 focus valn

2395 when autoSolve solveAll

2396 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

2397 = do attack; -- (h:_) <- get_holes

2398 tyn <- getNameFrom (sMN 0 "rty")

2399 -- start_unify h

2400 claim tyn RType

2401 valn <- getNameFrom (sMN 0 "rval")

2402 claim valn (Var tyn)

2403 letn <- getNameFrom (sMN 0 "rewrite_rule")

2404 letbind letn RigW (Var tyn) (Var valn)

2405 focus valn

2406 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2407 rewrite (Var letn)

2408 when autoSolve solveAll

2409 runT (LetTac n tm)

2410 = do attack

2411 tyn <- getNameFrom (sMN 0 "letty")

2412 claim tyn RType

2413 valn <- getNameFrom (sMN 0 "letval")

2414 claim valn (Var tyn)

2415 letn <- unique_hole n

2416 letbind letn RigW (Var tyn) (Var valn)

2417 focus valn

2418 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2419 when autoSolve solveAll

2420 runT (LetTacTy n ty tm)

2421 = do attack

2422 tyn <- getNameFrom (sMN 0 "letty")

2423 claim tyn RType

2424 valn <- getNameFrom (sMN 0 "letval")

2425 claim valn (Var tyn)

2426 letn <- unique_hole n

2427 letbind letn RigW (Var tyn) (Var valn)

2428 focus tyn

2429 elab ist toplevel ERHS [] (sMN 0 "tac") ty

2430 focus valn

2431 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2432 when autoSolve solveAll

2433 runT Compute = compute

2434 runT Trivial = do trivial' ist; when autoSolve solveAll

2435 runT TCImplementation = runT (Exact (PResolveTC emptyFC))

2436 runT (ProofSearch rec prover depth top psns hints)

2437 = do proofSearch' ist rec False depth prover top fn psns hints

2438 when autoSolve solveAll

2439 runT (Focus n) = focus n

2440 runT Unfocus = do hs <- get_holes

2441 case hs of

2442 [] -> return ()

2443 (h : _) -> movelast h

2444 runT Solve = solve

2445 runT (Try l r) = do try' (runT l) (runT r) True

2446 runT (TSeq l r) = do runT l; runT r

2447 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment

2448 tgoal <- goal -- store the goal

2449 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...

2450 script <- getNameFrom (sMN 0 "script")

2451 claim script scriptTy

2452 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

2453 letbind scriptvar RigW scriptTy (Var script)

2454 focus script

2455 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2456 (script', _) <- get_type_val (Var scriptvar)

2457 -- now that we have the script apply

2458 -- it to the reflected goal and context

2459 restac <- getNameFrom (sMN 0 "restac")

2460 claim restac tacticTy

2461 focus restac

2462 fill (raw_apply (forget script')

2463 [reflectEnv tenv, reflect tgoal])

2464 restac' <- get_guess

2465 solve

2466 -- normalise the result in order to

2467 -- reify it

2468 ctxt <- get_context

2469 env <- get_env

2470 let tactic = normalise ctxt env restac'

2471 runReflected tactic

2472 where tacticTy = Var (reflm "Tactic")

2473 listTy = Var (sNS (sUN "List") ["List", "Prelude"])

2474 scriptTy = (RBind (sMN 0 "__pi_arg")

2475 (Pi RigW Nothing (RApp listTy envTupleType) RType)

2476 (RBind (sMN 1 "__pi_arg")

2477 (Pi RigW Nothing (Var $ reflm "TT") RType) tacticTy))

2478 runT (ByReflection tm) -- run the reflection function 'tm' on the

2479 -- goal, then apply the resulting reflected Tactic

2480 = do tgoal <- goal

2481 attack

2482 script <- getNameFrom (sMN 0 "script")

2483 claim script scriptTy

2484 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

2485 letbind scriptvar RigW scriptTy (Var script)

2486 focus script

2487 ptm <- get_term

2488 env <- get_env

2489 let denv = map (\(n, _, b) -> (n, binderTy b)) env

2490 elab ist toplevel ERHS [] (sMN 0 "tac")

2491 (PApp emptyFC tm [pexp (delabTy' ist [] denv tgoal True True True)])

2492 (script', _) <- get_type_val (Var scriptvar)

2493 -- now that we have the script apply

2494 -- it to the reflected goal

2495 restac <- getNameFrom (sMN 0 "restac")

2496 claim restac tacticTy

2497 focus restac

2498 fill (forget script')

2499 restac' <- get_guess

2500 solve

2501 -- normalise the result in order to

2502 -- reify it

2503 ctxt <- get_context

2504 env <- get_env

2505 let tactic = normalise ctxt env restac'

2506 runReflected tactic

2507 where tacticTy = Var (reflm "Tactic")

2508 scriptTy = tacticTy

2509

2510 runT (Reflect v) = do attack -- let x = reflect v in ...

2511 tyn <- getNameFrom (sMN 0 "letty")

2512 claim tyn RType

2513 valn <- getNameFrom (sMN 0 "letval")

2514 claim valn (Var tyn)

2515 letn <- getNameFrom (sMN 0 "letvar")

2516 letbind letn RigW (Var tyn) (Var valn)

2517 focus valn

2518 elab ist toplevel ERHS [] (sMN 0 "tac") v

2519 (value, _) <- get_type_val (Var letn)

2520 ctxt <- get_context

2521 env <- get_env

2522 let value' = normalise ctxt env value

2523 runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))

2524 runT (Fill v) = do attack -- let x = fill x in ...

2525 tyn <- getNameFrom (sMN 0 "letty")

2526 claim tyn RType

2527 valn <- getNameFrom (sMN 0 "letval")

2528 claim valn (Var tyn)

2529 letn <- getNameFrom (sMN 0 "letvar")

2530 letbind letn RigW (Var tyn) (Var valn)

2531 focus valn

2532 elab ist toplevel ERHS [] (sMN 0 "tac") v

2533 (value, _) <- get_type_val (Var letn)

2534 ctxt <- get_context

2535 env <- get_env

2536 let value' = normalise ctxt env value

2537 rawValue <- reifyRaw value'

2538 runTac autoSolve ist perhapsFC fn (Exact $ PQuote rawValue)

2539 runT (GoalType n tac) = do g <- goal

2540 case unApply g of

2541 (P _ n' _, _) ->

2542 if nsroot n' == sUN n

2543 then runT tac

2544 else fail "Wrong goal type"

2545 _ -> fail "Wrong goal type"

2546 runT ProofState = do g <- goal

2547 return ()

2548 runT Skip = return ()

2549 runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")

2550 runT SourceFC =

2551 case perhapsFC of

2552 Nothing -> lift . tfail $ Msg "There is no source location available."

2553 Just fc ->

2554 do fill $ reflectFC fc

2555 solve

2556 runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"

2557 runT x = fail $ "Not implemented " ++ show x

2558

2559 runReflected t = do t' <- reify ist t

2560 runTac autoSolve ist perhapsFC fn t'

2561

2562elaboratingArgErr :: [(Name, Name)] -> Err -> Err

2563elaboratingArgErr [] err = err

2564elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

2565 where rewrite (ElaboratingArg _ _ _ _) = Nothing

2566 rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)

2567 rewrite (At fc e) = fmap (At fc) (rewrite e)

2568 rewrite err = Just (ElaboratingArg f x during err)

2569

2570

2571withErrorReflection :: Idris a -> Idris a

2572withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2573 where handle :: Err -> Idris Err

2574 handle e@(ReflectionError _ _) = do logElab 3 "Skipping reflection of error reflection result"

2575 return e -- Don't do meta-reflection of errors

2576 handle e@(ReflectionFailed _ _) = do logElab 3 "Skipping reflection of reflection failure"

2577 return e

2578 -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them

2579 handle e@(At fc err) = do logElab 3 "Reflecting body of At"

2580 err' <- handle err

2581 return (At fc err')

2582 handle e@(Elaborating what n ty err) = do logElab 3 "Reflecting body of Elaborating"

2583 err' <- handle err

2584 return (Elaborating what n ty err')

2585 handle e@(ElaboratingArg f a prev err) = do logElab 3 "Reflecting body of ElaboratingArg"

2586 hs <- getFnHandlers f a

2587 err' <- if null hs

2588 then handle err

2589 else applyHandlers err hs

2590 return (ElaboratingArg f a prev err')

2591 -- ProofSearchFail is an internal detail - so don't expose it

2592 handle (ProofSearchFail e) = handle e

2593 -- TODO: argument-specific error handlers go here for ElaboratingArg

2594 handle e = do ist <- getIState

2595 logElab 2 "Starting error reflection"

2596 logElab 5 (show e)

2597 let handlers = idris_errorhandlers ist

2598 applyHandlers e handlers

2599 getFnHandlers :: Name -> Name -> Idris [Name]

2600 getFnHandlers f arg = do ist <- getIState

2601 let funHandlers = maybe M.empty id .

2602 lookupCtxtExact f .

2603 idris_function_errorhandlers $ ist

2604 return . maybe [] S.toList . M.lookup arg $ funHandlers

2605

2606

2607 applyHandlers e handlers =

2608 do ist <- getIState

2609 let err = fmap (errReverse ist) e

2610 logElab 3 $ "Using reflection handlers " ++

2611 concat (intersperse ", " (map show handlers))

2612 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers

2613

2614 -- Typecheck error handlers - if this fails, most

2615 -- likely something which is needed by it has not

2616 -- been imported, so keep the original error.

2617 handlers <- case mapM (check (tt_ctxt ist) []) reports of

2618 Error _ -> return [] -- ierror $ ReflectionFailed "Type error while constructing reflected error" e

2619 OK hs -> return hs

2620

2621 -- Normalize error handler terms to produce the new messages

2622 -- Need to use 'normaliseAll' since we have to reduce private

2623 -- names in error handlers too

2624 ctxt <- getContext

2625 let results = map (normaliseAll ctxt []) (map fst handlers)

2626 logElab 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

2627

2628 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

2629 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

2630 errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

2631 Left err -> ierror err

2632 Right ok -> return ok

2633 return $ case errorparts of

2634 [] -> e

2635 parts -> ReflectionError errorparts e

2636

2637solveAll = try (do solve; solveAll) (return ())

2638

2639-- | Do the left-over work after creating declarations in reflected

2640-- elaborator scripts

2641processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()

2642processTacticDecls info steps =

2643 -- The order of steps is important: type declarations might

2644 -- establish metavars that later function bodies resolve.

2645 forM_ (reverse steps) $ \case

2646 RTyDeclInstrs n fc impls ty ->

2647 do logElab 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

2648 logElab 3 $ " It has impls " ++ show impls

2649 updateIState $ \i -> i { idris_implicits =

2650 addDef n impls (idris_implicits i) }

2651 addIBC (IBCImp n)

2652 ds <- checkDef info fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]

2653 addIBC (IBCDef n)

2654 ctxt <- getContext

2655 case lookupDef n ctxt of

2656 (TyDecl _ _ : _) ->

2657 -- If the function isn't defined at the end of the elab script,

2658 -- then it must be added as a metavariable. This needs guarding

2659 -- to prevent overwriting case defs with a metavar, if the case

2660 -- defs come after the type decl in the same script!

2661 let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) ds

2662 in addDeferred ds'

2663 _ -> return ()

2664 RDatatypeDeclInstrs n impls ->

2665 do addIBC (IBCDef n)

2666 updateIState $ \i -> i { idris_implicits = addDef n impls (idris_implicits i) }

2667 addIBC (IBCImp n)

2668

2669 RDatatypeDefnInstrs tyn tyconTy ctors ->

2670 do let cn (n, _, _) = n

2671 cty (_, _, t) = t

2672 addIBC (IBCDef tyn)

2673 mapM_ (addIBC . IBCDef . cn) ctors

2674 ctxt <- getContext

2675 let params = findParams tyn (normalise ctxt [] tyconTy) (map cty ctors)

2676 let typeInfo = TI (map cn ctors) False [] params [] False

2677 -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.

2678 -- otherwise writing the IBC just fails silently!

2679 updateIState $ \i -> i { idris_datatypes =

2680 addDef tyn typeInfo (idris_datatypes i) }

2681 addIBC (IBCData tyn)

2682

2683

2684 ttag <- getName -- from AbsSyntax.hs, really returns a disambiguating Int

2685

2686 let metainf = DataMI params

2687 addIBC (IBCMetaInformation tyn metainf)

2688 updateContext (setMetaInformation tyn metainf)

2689

2690 for_ ctors $ \(cn, impls, _) ->

2691 do updateIState $ \i -> i { idris_implicits = addDef cn impls (idris_implicits i) }

2692 addIBC (IBCImp cn)

2693

2694 for_ ctors $ \(ctorN, _, _) ->

2695 do totcheck (NoFC, ctorN)

2696 ctxt <- tt_ctxt <$> getIState

2697 case lookupTyExact ctorN ctxt of

2698 Just cty -> do checkPositive (tyn : map cn ctors) (ctorN, cty)

2699 return ()

2700 Nothing -> return ()

2701

2702 case ctors of

2703 [ctor] -> do setDetaggable (cn ctor); setDetaggable tyn

2704 addIBC (IBCOpt (cn ctor)); addIBC (IBCOpt tyn)

2705 _ -> return ()

2706 -- TODO: inaccessible

2707

2708 RAddImplementation interfaceName implName ->

2709 do -- The interface resolution machinery relies on a special

2710 logElab 2 $ "Adding elab script implementation " ++ show implName ++

2711 " for " ++ show interfaceName

2712 addImplementation False True interfaceName implName

2713 addIBC (IBCImplementation False True interfaceName implName)

2714 RClausesInstrs n cs ->

2715 do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n

2716 solveDeferred emptyFC n

2717 let lhss = map (\(ns, lhs, _) -> (map fst ns, lhs)) cs

2718 let fc = fileFC "elab_reflected"

2719 pmissing <-

2720 do ist <- getIState

2721 possible <- genClauses fc n lhss

2722 (map (\ (ns, lhs) ->

2723 delab' ist lhs True True) lhss)

2724 missing <- filterM (checkPossible n) possible

2725 let undef = filter (noMatch ist (map snd lhss)) missing

2726 return undef

2727 let tot = if null pmissing

2728 then Unchecked -- still need to check recursive calls

2729 else Partial NotCovering -- missing cases implies not total

2730 setTotality n tot

2731 updateIState $ \i -> i { idris_patdefs =

2732 addDef n (cs, pmissing) $ idris_patdefs i }

2733 addIBC (IBCDef n)

2734

2735 ctxt <- getContext

2736 case lookupDefExact n ctxt of

2737 Just (CaseOp _ _ _ _ _ cd) ->

2738 -- Here, we populate the call graph with a list of things

2739 -- we refer to, so that if they aren't total, the whole

2740 -- thing won't be.

2741 let (scargs, sc) = cases_compiletime cd

2742 calls = map fst $ findCalls sc scargs

2743 in do logElab 2 $ "Called names in reflected elab: " ++ show calls

2744 addCalls n calls

2745 addIBC $ IBCCG n

2746 Just _ -> return () -- TODO throw internal error

2747 Nothing -> return ()

2748

2749 -- checkDeclTotality requires that the call graph be present

2750 -- before calling it.

2751 -- TODO: reduce code duplication with Idris.Elab.Clause

2752 buildSCG (fc, n)

2753

2754 -- Actually run the totality checker. In the main clause

2755 -- elaborator, this is deferred until after. Here, we run it

2756 -- now to get totality information as early as possible.

2757 tot' <- checkDeclTotality (fc, n)

2758 setTotality n tot'

2759 when (tot' /= Unchecked) $ addIBC (IBCTotal n tot')

2760 where

2761 -- TODO: see if the code duplication with Idris.Elab.Clause can be

2762 -- reduced or eliminated.

2763 -- These are always cases generated by genClauses

2764 checkPossible :: Name -> PTerm -> Idris Bool

2765 checkPossible fname lhs_in =

2766 do ctxt <- getContext

2767 ist <- getIState

2768 let lhs = addImplPat ist lhs_in

2769 let fc = fileFC "elab_reflected_totality"

2770 case elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState

2771 (erun fc (buildTC ist info EImpossible [] fname (allNamesIn lhs_in)

2772 (infTerm lhs))) of

2773 OK (ElabResult lhs' _ _ _ _ _ name', _) ->

2774 do -- not recursively calling here, because we don't

2775 -- want to run infinitely many times

2776 let lhs_tm = orderPats (getInferTerm lhs')

2777 updateIState $ \i -> i { idris_name = name' }

2778 case recheck (constraintNS info) ctxt [] (forget lhs_tm) lhs_tm of

2779 OK _ -> return True

2780 err -> return False

2781 -- if it's a recoverable error, the case may become possible

2782 Error err -> return (recoverableCoverage ctxt err)

2783

2784

2785 -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause

2786 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of

2787 Right _ -> False

2788 Left _ -> True) cs