src/Idris/ElabTerm.hs · Idris-dev

git.iko.soy/Idris-dev

on bf4e535 help sign in

Idris-dev/src/Idris/ElabTerm.hs

2882 lines 131 kB history raw

1{-# LANGUAGE PatternGuards, ViewPatterns #-}

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

3module Idris.ElabTerm where

5import Idris.AbsSyntax

6import Idris.AbsSyntaxTree

7import Idris.DSL

8import Idris.Delaborate

9import Idris.Error

10import Idris.ProofSearch

11import Idris.Output (pshow)

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

14import Idris.Core.TT

15import Idris.Core.Evaluate

16import Idris.Core.Unify

17import Idris.Core.Typecheck (check, recheck)

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20import Idris.Elab.Utils

21import Idris.Reflection

22import qualified Util.Pretty as U

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

25import Control.Monad

26import Control.Monad.State.Strict

27import Data.List

28import qualified Data.Map as M

29import Data.Maybe (mapMaybe, fromMaybe)

30import qualified Data.Set as S

31import qualified Data.Text as T

33import Debug.Trace

35data ElabMode = ETyDecl | ELHS | ERHS

36 deriving Eq

38data ElabResult =

39 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

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

41 -- ^ Information about new metavariables

42 , resultCaseDecls :: [PDecl]

43 -- ^ Deferred declarations as the meaning of case blocks

44 , resultContext :: Context

45 -- ^ The potentially extended context from new definitions

46 , resultTyDecls :: [(Name, FC, [PArg], Type)]

47 -- ^ Meta-info about the new type declarations

48 }

50processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()

51processTacticDecls info =

52 forM_ info $ \(n, fc, impls, ty) ->

53 do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

54 logLvl 3 $ " It has impls " ++ show impls

55 updateIState $ \i -> i { idris_implicits =

56 addDef n impls (idris_implicits i) }

57 addIBC (IBCImp n)

58 ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]

59 addIBC (IBCDef n)

60 let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

61 addDeferred ds'

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

65-- elaborated, typechecked term.

66--

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

68-- holes to pattern bindings.

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

72build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

73 ElabD ElabResult

74build ist info emode opts fn tm

75 = do elab ist info emode opts fn tm

76 let tmIn = tm

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

78 [TIPartial] -> True

79 _ -> False

81 when (not pattern) $ solveAutos ist fn True

83 hs <- get_holes

84 ivs <- get_instances

85 ptm <- get_term

86 -- Resolve remaining type classes. Two passes - first to get the

87 -- default Num instances, second to clean up the rest

88 when (not pattern) $

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

90 do focus n

91 g <- goal

92 try (resolveTC True False 7 g fn ist)

93 (movelast n)) ivs

94 ivs <- get_instances

95 hs <- get_holes

96 when (not pattern) $

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

98 do focus n

99 g <- goal

100 ptm <- get_term

101 resolveTC True True 7 g fn ist) ivs

102 tm <- get_term

103 ctxt <- get_context

104 probs <- get_probs

105 u <- getUnifyLog

106 hs <- get_holes

107

108 when (not pattern) $

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

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

111 do unify_all; matchProblems True; unifyProblems

112

113 probs <- get_probs

114 case probs of

115 [] -> return ()

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

117 if inf then return ()

118 else lift (Error e)

119

120 when tydecl (do mkPat

121 update_term liftPats

122 update_term orderPats)

123 EState is _ impls <- getAux

124 tt <- get_term

125 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

126 log <- getLog

127 ctxt <- get_context

128 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

129 else return (ElabResult tm ds is ctxt impls)

130 where pattern = emode == ELHS

131 tydecl = emode == ETyDecl

132

133 mkPat = do hs <- get_holes

134 tm <- get_term

135 case hs of

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

137 [] -> return ()

138

139-- Build a term autogenerated as a typeclass method definition

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

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

142

143buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

144 ElabD ElabResult

145buildTC ist info emode opts fn tm

146 = do -- set name supply to begin after highest index in tm

147 let ns = allNamesIn tm

148 let tmIn = tm

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

150 [TIPartial] -> True

151 _ -> False

152 initNextNameFrom ns

153 elab ist info emode opts fn tm

154 probs <- get_probs

155 tm <- get_term

156 case probs of

157 [] -> return ()

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

159 else lift (Error e)

160 dots <- get_dotterm

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

162 -- unification

163 when (not (null dots)) $

164 lift (Error (CantMatch (getInferTerm tm)))

165 EState is _ impls <- getAux

166 tt <- get_term

167 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

168 log <- getLog

169 ctxt <- get_context

170 if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

171 else return (ElabResult tm ds is ctxt impls)

172 where pattern = emode == ELHS

173

174-- return whether arguments of the given constructor name can be

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

176-- concrete by the time we get around to elaborating the argument.

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

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

179 = case lookupTyExact n ctxt of

180 Nothing -> []

181 Just ty -> checkArgs [] [] ty

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

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

184 = let env' = case t of

185 TType _ -> n : env

186 _ -> env in

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

188 (instantiate (P Bound n t) sc)

189 checkArgs env ns t

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

191

192getUnmatchable ctxt n = []

193

194data ElabCtxt = ElabCtxt { e_inarg :: Bool,

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

196 e_guarded :: Bool,

197 e_intype :: Bool,

198 e_qq :: Bool,

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

200 }

201

202initElabCtxt = ElabCtxt False False False False False False

203

204goal_polymorphic :: ElabD Bool

205goal_polymorphic =

206 do ty <- goal

207 case ty of

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

209 case lookup n env of

210 Nothing -> return False

211 _ -> return True

212 _ -> return False

213

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

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

216-- declarations resulting from user tactic scripts (%runTactics)

217elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

218 ElabD ()

219elab ist info emode opts fn tm

220 = do let loglvl = opt_logLevel (idris_options ist)

221 when (loglvl > 5) $ unifyLog True

222 compute -- expand type synonyms, etc

223 let fc = maybe "(unknown)"

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

225 est <- getAux

226 sequence_ (delayed_elab est)

227 end_unify

228 ptm <- get_term

229 when pattern -- convert remaining holes to pattern vars

230 (do update_term orderPats

231 unify_all

232 matchProblems False -- only the ones we matched earlier

233 unifyProblems

234 mkPat)

235 where

236 pattern = emode == ELHS

237 bindfree = emode == ETyDecl || emode == ELHS

238

239 tcgen = Dictionary `elem` opts

240 reflection = Reflection `elem` opts

241

242 isph arg = case getTm arg of

243 Placeholder -> (True, priority arg)

244 tm -> (False, priority arg)

245

246 toElab ina arg = case getTm arg of

247 Placeholder -> Nothing

248 v -> Just (priority arg, elabE ina (elabFC info) v)

249

250 toElab' ina arg = case getTm arg of

251 Placeholder -> Nothing

252 v -> Just (elabE ina (elabFC info) v)

253

254 mkPat = do hs <- get_holes

255 tm <- get_term

256 case hs of

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

258 [] -> return ()

259

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

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

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

263 -- typically

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

265 elabE ina fc' t =

266 --do g <- goal

267 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

268 do solved <- get_recents

269 as <- get_autos

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

271 -- have another go at solving them now.

272 mapM_ (\(a, ns) -> if any (\n -> n `elem` solved) ns

273 then solveAuto ist fn False a

274 else return ()) as

275

276 itm <- if not pattern then insertImpLam ina t else return t

277 ct <- insertCoerce ina itm

278 t' <- insertLazy ct

279 g <- goal

280 tm <- get_term

281 ps <- get_probs

282 hs <- get_holes

283

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

285 -- ++ "\n" ++ show tm

286 -- ++ "\nholes " ++ show hs

287 -- ++ "\nproblems " ++ show ps

288 -- ++ "\n-----------\n") $

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

290 let fc = fileFC "Force"

291 env <- get_env

292 handleError (forceErr t' env)

293 (elab' ina fc' t')

294 (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

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

296 pimp (sUN "a") Placeholder True,

297 pexp ct])) True

298

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

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

301 ht == txt "Lazy'" = notDelay orig

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

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

304 ht == txt "Lazy'" = notDelay orig

305 forceErr orig env (InfiniteUnify _ t _)

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

307 ht == txt "Lazy'" = notDelay orig

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

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

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

311 forceErr orig env t = False

312

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

314 notDelay _ = True

315

316 local f = do e <- get_env

317 return (f `elem` map fst e)

318

319 -- | Is a constant a type?

320 constType :: Const -> Bool

321 constType (AType _) = True

322 constType StrType = True

323 constType VoidType = True

324 constType _ = False

325

326 -- "guarded" means immediately under a constructor, to help find patvars

327

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

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

330 -> PTerm -- ^ The term to elaborate

331 -> ElabD ()

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

333 elab' ina fc PType = do apply RType []; solve

334 elab' ina fc (PUniverse u) = do apply (RUType u) []; solve

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

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

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

338 elab' ina fc tm@(PConstant c)

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

340 && isTypeConst c

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

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

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

344 | otherwise = do apply (RConstant c) []; solve

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

346 elab' ina _ (PTrue fc _) =

347 do hnf_compute

348 g <- goal

349 case g of

350 TType _ -> elab' ina (Just fc) (PRef fc unitTy)

351 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

352 _ -> elab' ina (Just fc) (PRef fc unitCon)

353 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

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

355 elab' ina fc (PResolveTC fc')

356 = do c <- getNameFrom (sMN 0 "class")

357 instanceArg c

358 elab' ina _ (PRefl fc t)

359 = elab' ina (Just fc) (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

360 pimp (sMN 0 "x") t False])

361 elab' ina _ (PEq fc Placeholder Placeholder l r)

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

363 claim tyn RType

364 movelast tyn

365 elab' ina (Just fc) (PApp fc (PRef fc eqTy)

366 [pimp (sUN "A") (PRef fc tyn) True,

367 pimp (sUN "B") (PRef fc tyn) False,

368 pexp l, pexp r]))

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

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

371 claim atyn RType

372 movelast atyn

373 claim btyn RType

374 movelast btyn

375 elab' ina (Just fc) (PApp fc (PRef fc eqTy)

376 [pimp (sUN "A") (PRef fc atyn) True,

377 pimp (sUN "B") (PRef fc btyn) False,

378 pexp l, pexp r]))

379

380 elab' ina _ (PEq fc lt rt l r) = elab' ina (Just fc) (PApp fc (PRef fc eqTy)

381 [pimp (sUN "A") lt True,

382 pimp (sUN "B") rt False,

383 pexp l, pexp r])

384 elab' ina _ (PPair fc _ l r)

385 = do hnf_compute

386 g <- goal

387 let (tc, _) = unApply g

388 case g of

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

390 [pexp l,pexp r])

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

392 [pexp l,pexp r])

393 _ -> case tc of

394 P _ n _ | n == upairTy

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

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

397 pimp (sUN "B") Placeholder False,

398 pexp l, pexp r])

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

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

401 pimp (sUN "B") Placeholder False,

402 pexp l, pexp r])

403-- _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon)

404-- [pimp (sUN "A") Placeholder False,

405-- pimp (sUN "B") Placeholder False,

406-- pexp l, pexp r]))

407-- (elab' ina (Just fc) (PApp fc (PRef fc upairCon)

408-- [pimp (sUN "A") Placeholder False,

409-- pimp (sUN "B") Placeholder False,

410-- pexp l, pexp r]))

411-- True

412

413 elab' ina _ (PDPair fc p l@(PRef _ n) t r)

414 = case t of

415 Placeholder ->

416 do hnf_compute

417 g <- goal

418 case g of

419 TType _ -> asType

420 _ -> asValue

421 _ -> asType

422 where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)

423 [pexp t,

424 pexp (PLam fc n Placeholder r)])

425 asValue = elab' ina (Just fc) (PApp fc (PRef fc existsCon)

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

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

428 pexp l, pexp r])

429 elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc existsCon)

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

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

432 pexp l, pexp r])

433 elab' ina fc (PAlternative True as)

434 = do hnf_compute

435 ty <- goal

436 ctxt <- get_context

437 let (tc, _) = unApply ty

438 env <- get_env

439 let as' = pruneByType (map fst env) tc ctxt as

440-- trace (-- show tc ++ " " ++ show as ++ "\n ==> " ++

441-- show (length as') ++ "\n" ++

442-- showSep ", " (map showTmImpls as') ++ "\nEND") $

443 tryAll (zip (map (elab' ina fc) as') (map showHd as'))

444 where showHd (PApp _ (PRef _ n) _) = n

445 showHd (PRef _ n) = n

446 showHd (PApp _ h _) = showHd h

447 showHd x = NErased -- We probably should do something better than this here

448 elab' ina fc (PAlternative False as)

449 = trySeq as

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

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

452 try' e1 (trySeq' e1 xs) True

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

454 trySeq' deferr [] = proofFail deferr

455 trySeq' deferr (x : xs)

456 = try' (do elab' ina fc x

457 solveAutos ist fn False) (trySeq' deferr xs) True

458 elab' ina _ (PPatvar fc n) | bindfree = do patvar n; update_term liftPats

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

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

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

462 elab' ec _ tm@(PRef fc n)

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

464 && isTConName n (tt_ctxt ist)

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

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

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

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

469 = do let ina = e_inarg ec

470 guarded = e_guarded ec

471 inty = e_intype ec

472 ctxt <- get_context

473 let defined = case lookupTy n ctxt of

474 [] -> False

475 _ -> True

476 -- this is to stop us resolve type classes recursively

477 -- trace (show (n, guarded)) $

478 if (tcname n && ina) then erun fc $ do patvar n; update_term liftPats

479 else if (defined && not guarded)

480 then do apply (Var n) []; solve

481 else try (do apply (Var n) []; solve)

482 (do patvar n; update_term liftPats)

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

484 [] -> False

485 _ -> True

486 bindable (NS _ _) = False

487 bindable (UN xs) = True

488 bindable n = implicitable n

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

490 elab' ina fc' tm@(PRef fc n)

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

492 && isTConName n (tt_ctxt ist)

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

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

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

496 | otherwise =

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

498 ctxt <- get_context

499 env <- get_env

500 let a' = insertScopedImps fc (normalise ctxt env fty) []

501 if null a'

502 then erun fc $ do apply (Var n) []; solve

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

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

505 elab' ina _ (PLam fc n Placeholder sc)

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

507 ctxt <- get_context

508 when (isTConName n ctxt) $

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

510 checkPiGoal n

511 attack; intro (Just n);

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

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

514 elab' ec _ (PLam fc n ty sc)

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

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

517 ctxt <- get_context

518 when (isTConName n ctxt) $

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

520 checkPiGoal n

521 claim tyn RType

522 explicit tyn

523 attack

524 ptm <- get_term

525 hs <- get_holes

526 introTy (Var tyn) (Just n)

527 focus tyn

528

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

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

531 solve

532 elab' ina fc (PPi p n Placeholder sc)

533 = do attack; arg n (is_scoped p) (sMN 0 "ty")

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

535 solve

536 elab' ina fc (PPi p n ty sc)

537 = do attack; tyn <- getNameFrom (sMN 0 "ty")

538 claim tyn RType

539 n' <- case n of

540 MN _ _ -> unique_hole n

541 _ -> return n

542 forall n' (is_scoped p) (Var tyn)

543 focus tyn

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

545 elabE ec' fc ty

546 elabE ec' fc sc

547 solve

548 elab' ina _ (PLet fc n ty val sc)

549 = do attack

550 ivs <- get_instances

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

552 claim tyn RType

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

554 claim valn (Var tyn)

555 explicit valn

556 letbind n (Var tyn) (Var valn)

557 case ty of

558 Placeholder -> return ()

559 _ -> do focus tyn

560 explicit tyn

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

562 (Just fc) ty

563 focus valn

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

565 (Just fc) val

566 ivs' <- get_instances

567 env <- get_env

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

569 when (not pattern) $

570 mapM_ (\n -> do focus n

571 g <- goal

572 hs <- get_holes

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

574 then try (resolveTC True False 7 g fn ist)

575 (movelast n)

576 else movelast n)

577 (ivs' \\ ivs)

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

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

580 expandLet n (case lookup n env of

581 Just (Let t v) -> v

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

583 solve

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

585 rty <- goal

586 attack

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

588 claim tyn RType

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

590 claim valn (Var tyn)

591 letbind n (Var tyn) (Var valn)

592 focus valn

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

594 env <- get_env

595 computeLet n

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

597 solve

598-- elab' ina fc (PLet n Placeholder

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

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

601 rty <- goal

602 ds <- get_deferred

603 ctxt <- get_context

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

605 -- new function name

606 env <- get_env

607 argTys <- claimArgTys env args

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

609 let fty = fnTy argTys rty

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

611 -- build and defer the function application

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

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

614 -- be explicit.

615 mapM_ elabIArg (zip argTys args)

616 where claimArgTys env [] = return []

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

618 = do nty <- get_type (Var n)

619 ans <- claimArgTys env xs

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

621 claimArgTys env (_ : xs)

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

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

624 claim an RType

625 claim aval (Var an)

626 ans <- claimArgTys env xs

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

628 fnTy [] ret = forget ret

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

630

631 localVar env (PRef _ x)

632 = case lookup x env of

633 Just _ -> Just x

634 _ -> Nothing

635 localVar env _ = Nothing

636

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

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

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

640

641 mkN n@(NS _ _) = n

642 mkN n@(SN _) = n

643 mkN n = case namespace info of

644 Just xs@(_:_) -> sNS n xs

645 _ -> n

646

647 elab' ina _ (PMatchApp fc fn)

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

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

650 _ -> lift $ tfail (NoSuchVariable fn)

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

652 solve

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

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

655 elab' ina topfc tm@(PApp fc (PRef _ f) args_in)

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

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

658 | otherwise = implicitApp $

659 do env <- get_env

660 ty <- goal

661 fty <- get_type (Var f)

662 ctxt <- get_context

663 let args = insertScopedImps fc (normalise ctxt env fty) args_in

664 let unmatchableArgs = if pattern

665 then getUnmatchable (tt_ctxt ist) f

666 else []

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

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

669 && isTConName f (tt_ctxt ist)) $

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

671 if (f `elem` map fst env && length args == 1 && length args_in == 1)

672 then -- simple app, as below

673 do simple_app False

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

675 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

676 (show tm)

677 solve

678 return []

679 else

680 do ivs <- get_instances

681 ps <- get_probs

682 -- HACK: we shouldn't resolve type classes if we're defining an instance

683 -- function or default definition.

684 let isinf = f == inferCon || tcname f

685 -- if f is a type class, we need to know its arguments so that

686 -- we can unify with them

687 case lookupCtxt f (idris_classes ist) of

688 [] -> return ()

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

690 -- maybe more things are solvable now

691 unifyProblems

692 let guarded = isConName f ctxt

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

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

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

696 -- mark any type class arguments as injective

697 mapM_ checkIfInjective (map snd ns)

698 unifyProblems -- try again with the new information,

699 -- to help with disambiguation

700 -- Sort so that the implicit tactics and alternatives go last

701 let (ns', eargs) = unzip $

702 sortBy cmpArg (zip ns args)

703 ulog <- getUnifyLog

704 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

705 [] fc False f

706 (zip ns' (unmatchableArgs ++ repeat False))

707 (f == sUN "Force")

708 (map (\x -> getTm x) eargs) -- TODO: remove this False arg

709 imp <- if (e_isfn ina) then

710 do guess <- get_guess

711 gty <- get_type (forget guess)

712 env <- get_env

713 let ty_n = normalise ctxt env gty

714 return $ getReqImps ty_n

715 else return []

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

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

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

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

720 case imp of

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

722 _ -> do solve

723 hs <- get_holes

724 ivs' <- get_instances

725 -- Attempt to resolve any type classes which have 'complete' types,

726 -- i.e. no holes in them

727 when (not pattern || (e_inarg ina && not tcgen &&

728 not (e_guarded ina))) $

729 mapM_ (\n -> do focus n

730 g <- goal

731 env <- get_env

732 hs <- get_holes

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

734 then try (resolveTC False False 7 g fn ist)

735 (movelast n)

736 else movelast n)

737 (ivs' \\ ivs)

738 return []

739 where

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

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

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

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

744 -- to be needed.

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

746 implicitApp elab

747 | pattern = do elab; return ()

748 | otherwise

749 = do s <- get

750 imps <- elab

751 case imps of

752 [] -> return ()

753 es -> do put s

754 elab' ina topfc (PAppImpl tm es)

755

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

757 = i : getReqImps sc

758 getReqImps _ = []

759

760 -- normal < alternatives < lambdas < rewrites < tactic < default tactic

761 -- reason for lambdas after alternatives is that having

762 -- the alternative resolved can help with typechecking the lambda

763 -- or the rewrite. Rewrites/tactics need as much information

764 -- as possible about the type.

765 -- FIXME: Better would be to allow alternative resolution to be

766 -- retried after more information is in.

767 cmpArg (_, x) (_, y)

768 | constraint x && not (constraint y) = LT

769 | constraint y && not (constraint x) = GT

770 | otherwise

771 = compare (conDepth 0 (getTm x) + priority x + alt x)

772 (conDepth 0 (getTm y) + priority y + alt y)

773 where alt t = case getTm t of

774 PAlternative False _ -> 5

775 PAlternative True _ -> 2

776 PTactics _ -> 150

777 PLam _ _ _ _ -> 3

778 PRewrite _ _ _ _ -> 4

779 PResolveTC _ -> 0

780 PHidden _ -> 150

781 _ -> 1

782

783 constraint (PConstraint _ _ _ _) = True

784 constraint _ = False

785

786 -- Score a point for every level where there is a non-constructor

787 -- function (so higher score --> done later), and lots of points

788 -- if there is a PHidden since this should be unifiable.

789 -- Only relevant when on lhs

790 conDepth d t | not pattern = 0

791 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0

792 | otherwise = max (100 - d) 1

793 conDepth d (PApp _ f as)

794 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))

795 conDepth d (PPatvar _ _) = 0

796 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

797 conDepth d (PHidden _) = 150

798 conDepth d Placeholder = 0

799 conDepth d (PResolveTC _) = 0

800 conDepth d t = max (100 - d) 1

801

802 checkIfInjective n = do

803 env <- get_env

804 case lookup n env of

805 Nothing -> return ()

806 Just b ->

807 case unApply (binderTy b) of

808 (P _ c _, args) ->

809 case lookupCtxtExact c (idris_classes ist) of

810 Nothing -> return ()

811 Just ci -> -- type class, set as injective

812 do mapM_ setinjArg (getDets 0 (class_determiners ci) args)

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

814 ulog <- getUnifyLog

815 probs <- get_probs

816 traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $

817 unifyProblems

818 probs <- get_probs

819 traceWhen ulog (qshow probs) $ return ()

820 _ -> return ()

821

822 setinjArg (P _ n _) = setinj n

823 setinjArg _ = return ()

824

825 getDets i ds [] = []

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

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

828

829 tacTm (PTactics _) = True

830 tacTm (PProof _) = True

831 tacTm _ = False

832

833 setInjective (PRef _ n) = setinj n

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

835 setInjective _ = return ()

836

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

838 erun fc $

839 do simple_app (not $ headRef f)

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

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

842 (show tm)

843 solve

844 where headRef (PRef _ _) = True

845 headRef (PApp _ f _) = headRef f

846 headRef _ = False

847

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

849 solve

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

851 appImpl (e : es) = simple_app False

852 (appImpl es)

853 (elab' ina fc Placeholder)

854 (show f)

855 elab' ina fc Placeholder

856 = do (h : hs) <- get_holes

857 movelast h

858 elab' ina fc (PMetavar n) =

859 do ptm <- get_term

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

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

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

863 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

864 let n' = mkN n

865 attack

866 defer unique_used n'

867 solve

868 where mkN n@(NS _ _) = n

869 mkN n = case namespace info of

870 Just xs@(_:_) -> sNS n xs

871 _ -> n

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

873 elab' ina fc (PTactics ts)

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

875 | otherwise = elab' ina fc Placeholder

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

877 elab' ina _ (PRewrite fc r sc newg)

878 = do attack

879 tyn <- getNameFrom (sMN 0 "rty")

880 claim tyn RType

881 valn <- getNameFrom (sMN 0 "rval")

882 claim valn (Var tyn)

883 letn <- getNameFrom (sMN 0 "_rewrite_rule")

884 letbind letn (Var tyn) (Var valn)

885 focus valn

886 elab' ina (Just fc) r

887 compute

888 g <- goal

889 rewrite (Var letn)

890 g' <- goal

891 when (g == g') $ lift $ tfail (NoRewriting g)

892 case newg of

893 Nothing -> elab' ina (Just fc) sc

894 Just t -> doEquiv t sc

895 solve

896 where doEquiv t sc =

897 do attack

898 tyn <- getNameFrom (sMN 0 "ety")

899 claim tyn RType

900 valn <- getNameFrom (sMN 0 "eqval")

901 claim valn (Var tyn)

902 letn <- getNameFrom (sMN 0 "equiv_val")

903 letbind letn (Var tyn) (Var valn)

904 focus tyn

905 elab' ina (Just fc) t

906 focus valn

907 elab' ina (Just fc) sc

908 elab' ina (Just fc) (PRef fc letn)

909 solve

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

911 = do attack

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

913 claim tyn RType

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

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

916 claim valn (Var tyn)

917 letbind scvn (Var tyn) (Var valn)

918 focus valn

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

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

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

922 unifyProblems

923 matchProblems True

924 args <- get_env

925 envU <- mapM (getKind args) args

926 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts

927

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

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

930 -- not valid to use them again anyway)

931 --

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

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

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

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

936 ptm <- get_term

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

938

939 let argsDropped = filter (isUnique envU)

940 (nub $ allNamesIn scr ++ inApp ptm ++

941 inOpts)

942

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

944

945 cname <- unique_hole' True (mkCaseName fn)

946 let cname' = mkN cname

947-- elab' ina fc (PMetavar cname')

948 attack; defer argsDropped cname'; solve

949

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

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

952 let newdef = PClauses fc [] cname'

953 (caseBlock fc cname'

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

955 -- elaborate case

956 updateAux (\e -> e { case_decls = newdef : case_decls e } )

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

958 movelast tyn

959 solve

960 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

961 mkCaseName n = SN (CaseN n)

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

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

964 mkN n@(NS _ _) = n

965 mkN n = case namespace info of

966 Just xs@(_:_) -> sNS n xs

967 _ -> n

968

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

970 inApp (App f a) = inApp f ++ inApp a

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

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

973 inApp (Bind n b sc) = inApp sc

974 inApp _ = []

975

976 isUnique envk n = case lookup n envk of

977 Just u -> u

978 _ -> False

979

980 getKind env (n, _)

981 = case lookup n env of

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

983 Just b ->

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

985 case ty of

986 UType UniqueType -> return (n, True)

987 UType AllTypes -> return (n, True)

988 _ -> return (n, False)

989

990 tcName tm | (P _ n _, _) <- unApply tm

991 = case lookupCtxt n (idris_classes ist) of

992 [_] -> True

993 _ -> False

994 tcName _ = False

995

996 usedIn ns (n, b)

997 = n `elem` ns

998 || any (\x -> x `elem` ns) (allTTNames (binderTy b))

999

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

1001 elab' ina fc t

1002 unifyLog False

1003 elab' ina fc (PQuasiquote t goalt)

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

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

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

1007 finalTy <- goal

1008 (t, unq) <- extractUnquotes 0 t

1009 let unquoteNames = map fst unq

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

1011

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

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

1014 ctxt <- get_context

1015 saveState

1016 updatePS (const .

1017 newProof (sMN 0 "q") ctxt $

1018 P Ref (reflm "TT") Erased)

1019

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

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

1022 -- of their reflection.

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

1024 claim ty RType

1025 movelast ty

1026 claim n (Var ty)

1027 movelast n)

1028 unquoteNames

1029

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

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

1032 -- quasiquoted

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

1034 claim qTy RType

1035 movelast qTy

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

1037 claim qTm (Var qTy)

1038

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

1040 -- the hole doesn't disappear

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

1042 letbind nTm (Var qTy) (Var qTm)

1043

1044 -- Fill out the goal type, if relevant

1045 case goalt of

1046 Nothing -> return ()

1047 Just gTy -> do focus qTy

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

1049

1050 -- Elaborate the quasiquoted term into the hole

1051 focus qTm

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

1053 end_unify

1054

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

1056 -- original goal in the original proof state.

1057 env <- get_env

1058 loadState

1059 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

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

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

1062 _ -> False

1063 case quoted of

1064 Just q -> do ctxt <- get_context

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

1066 if pattern

1067 then if isRaw

1068 then reflectRawQuotePattern unquoteNames (forget q')

1069 else reflectTTQuotePattern unquoteNames q'

1070 else do if isRaw

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

1072 fill $ reflectRawQuote unquoteNames (forget q')

1073 else fill $ reflectTTQuote unquoteNames q'

1074 solve

1075

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

1077

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

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

1080 -- the main quotation.

1081 mapM_ elabUnquote unq

1082 where elabUnquote (n, tm)

1083 = do focus n

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

1085

1086

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

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

1089 elab' ina fc (PHidden t)

1090 | reflection = elab' ina fc t

1091 | otherwise

1092 = do (h : hs) <- get_holes

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

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

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

1096 -- in directly.

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

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

1099 movelast h

1100 delayElab $ do focus h

1101 dotterm

1102 elab' ina fc t

1103 elab' ina fc (PRunTactics fc' tm) =

1104 do attack

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

1106 n' <- getNameFrom (sMN 0 "tacticExpr")

1107 let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)

1108 claim n scriptTy

1109 movelast n

1110 letbind n' scriptTy (Var n)

1111 focus n

1112 elab' ina (Just fc') tm

1113 env <- get_env

1114 runTactical (maybe fc' id fc) env (P Bound n' Erased)

1115 EState _ _ todo <- getAux

1116 solve

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

1118

1119 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })

1120

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

1122 isScr (PRef _ n) (n', b) = (n', (n == n', b))

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

1124

1125 caseBlock :: FC -> Name ->

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

1127 caseBlock fc n env opts

1128 = let args' = findScr env

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

1130 map (mkClause args) opts

1131

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

1133 -- 'True'. If the scrutinee is in the environment, match on that

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

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

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

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

1138 findScr (x : xs) = x : findScr xs

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

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

1141

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

1143 -- it at the end of the environment

1144 scrName n [] = []

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

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

1147

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

1149

1150 mkarg (n, s) = (PRef fc n, s)

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

1152 -- old ones with an _

1153 mkClause args (l, r)

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

1155 lhs = PApp (getFC fc l) (PRef (getFC fc l) n)

1156 (map (mkLHSarg l) args') in

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

1158

1159 mkLHSarg l (tm, True) = pexp l

1160 mkLHSarg l (tm, False) = pexp tm

1161

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

1163 shadowed new t = t

1164

1165 getFC d (PApp fc _ _) = fc

1166 getFC d (PRef fc _) = fc

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

1168 getFC d x = d

1169

1170 insertLazy :: PTerm -> ElabD PTerm

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

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

1173 insertLazy (PCoerced t) = return t

1174 insertLazy t =

1175 do ty <- goal

1176 env <- get_env

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

1178 let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]

1179 case tyh of

1180 P _ (UN l) _ | l == txt "Lazy'"

1181 -> return (PAlternative False tries)

1182 _ -> return t

1183 where

1184 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)

1185 mkDelay env t

1186 = let fc = fileFC "Delay" in

1187 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

1188 [pexp t])

1189

1190

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

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

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

1194 notImplicitable (PApp _ f _) = notImplicitable f

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

1196 notImplicitable (PRef _ n)

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

1198 = NoImplicit `elem` opts

1199 notImplicitable (PAlternative True as) = any notImplicitable as

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

1201 -- they can go in the branches separately.

1202 notImplicitable (PCase _ _ _) = True

1203 notImplicitable _ = False

1204

1205 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1206 | tcinstance i

1207 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1208 | otherwise

1209 = pimp n Placeholder True : insertScopedImps fc sc xs

1210 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)

1211 = x : insertScopedImps fc sc xs

1212 insertScopedImps _ _ xs = xs

1213

1214 insertImpLam ina t =

1215 do ty <- goal

1216 env <- get_env

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

1218 addLam ty' t

1219 where

1220 -- just one level at a time

1221 addLam (Bind n (Pi (Just _) _ _) sc) t =

1222 do impn <- unique_hole (sMN 0 "imp")

1223 if e_isfn ina -- apply to an implicit immediately

1224 then return (PApp emptyFC

1225 (PLam emptyFC impn Placeholder t)

1226 [pexp Placeholder])

1227 else return (PLam emptyFC impn Placeholder t)

1228 addLam _ t = return t

1229

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

1231 insertCoerce ina t | notImplicitable t = return t

1232 insertCoerce ina t =

1233 do ty <- goal

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

1235 -- and add them as 'alternatives'

1236 env <- get_env

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

1238 let cs = getCoercionsTo ist ty'

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

1240 (PCoerced tm, _) -> tm

1241 (_, []) -> t

1242 (_, cs) -> PAlternative False [t ,

1243 PAlternative True (map (mkCoerce env t) cs)]

1244 return t'

1245 where

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

1247 addImplBound ist (map fst env)

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

1249

1250 -- | Elaborate the arguments to a function

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

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

1253 -> [Bool]

1254 -> FC -- ^ Source location

1255 -> Bool

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

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

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

1259 -> [PTerm] -- ^ argument

1260 -> ElabD ()

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

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

1263 = do hs <- get_holes

1264 if holeName `elem` hs then

1265 do focus holeName

1266 case t of

1267 Placeholder -> do movelast holeName

1268 elabArgs ist ina failed fc r f ns force args

1269 _ -> elabArg t

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

1271 where elabArg t =

1272 do -- solveAutos ist fn False

1273 now_elaborating fc f argName

1274 wrapErr f argName $ do

1275 hs <- get_holes

1276 tm <- get_term

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

1278 -- recursively!)

1279 let elab = if force then elab' else elabE

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

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

1282 do focus holeName;

1283 g <- goal

1284 -- Can't pattern match on polymorphic goals

1285 poly <- goal_polymorphic

1286 ulog <- getUnifyLog

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

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

1289 return failed

1290 done_elaborating_arg f argName

1291 elabArgs ist ina failed fc r f ns force args

1292 wrapErr f argName action =

1293 do elabState <- get

1294 while <- elaborating_app

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

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

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

1298 Error e -> do done_elaborating_arg f argName

1299 lift (tfail (elaboratingArgErr while' e))

1300 put newState

1301 return result

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

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

1304

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

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

1307

1308pruneAlt :: [PTerm] -> [PTerm]

1309pruneAlt xs = map prune xs

1310 where

1311 prune (PApp fc1 (PRef fc2 f) as)

1312 = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

1313 prune t = t

1314

1315 choose f (PAlternative a as)

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

1317 fs = filter (headIs f) as' in

1318 case fs of

1319 [a] -> a

1320 _ -> PAlternative a as'

1321

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

1323 choose f t = t

1324

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

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

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

1328

1329-- Rule out alternatives that don't return the same type as the head of the goal

1330-- (If there are none left as a result, do nothing)

1331pruneByType :: [Name] -> Term -> -- head of the goal

1332 Context -> [PTerm] -> [PTerm]

1333-- if an alternative has a locally bound name at the head, take it

1334pruneByType env t c as

1335 | Just a <- locallyBound as = [a]

1336 where

1337 locallyBound [] = Nothing

1338 locallyBound (t:ts)

1339 | Just n <- getName t,

1340 n `elem` env = Just t

1341 | otherwise = locallyBound ts

1342 getName (PRef _ n) = Just n

1343 getName (PApp _ f _) = getName f

1344 getName (PHidden t) = getName t

1345 getName _ = Nothing

1346

1347pruneByType env (P _ n _) ctxt as

1348-- if the goal type is polymorphic, keep e

1349 | [] <- lookupTy n ctxt = as

1350 | otherwise

1351 = let asV = filter (headIs True n) as

1352 as' = filter (headIs False n) as in

1353 case as' of

1354 [] -> case asV of

1355 [] -> as

1356 _ -> asV

1357 _ -> as'

1358 where

1359 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1360 headIs var f (PApp _ f' _) = headIs var f f'

1361 headIs var f (PPi _ _ _ sc) = headIs var f sc

1362 headIs var f (PHidden t) = headIs var f t

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

1364

1365 typeHead var f f'

1366 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $

1367 case lookupTy f' ctxt of

1368 [ty] -> case unApply (getRetTy ty) of

1369 (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f

1370 _ -> let ty' = normalise ctxt [] ty in

1371 case unApply (getRetTy ty') of

1372 (P _ ftyn _, _) -> ftyn == f

1373 (V _, _) -> var -- keep, variable

1374 _ -> False

1375 _ -> False

1376

1377pruneByType _ t _ as = as

1378

1379findInstances :: IState -> Term -> [Name]

1380findInstances ist t

1381 | (P _ n _, _) <- unApply t

1382 = case lookupCtxt n (idris_classes ist) of

1383 [CI _ _ _ _ _ ins _] -> filter accessible ins

1384 _ -> []

1385 | otherwise = []

1386 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

1387 Just (_, Hidden) -> False

1388 _ -> True

1389

1390-- Try again to solve auto implicits

1391solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

1392solveAuto ist fn ambigok n

1393 = do hs <- get_holes

1394 when (n `elem` hs) $ do

1395 focus n

1396 g <- goal

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

1398 when (not isg) $

1399 proofSearch' ist True ambigok 100 True Nothing fn []

1400

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

1402solveAutos ist fn ambigok

1403 = do autos <- get_autos

1404 mapM_ (solveAuto ist fn ambigok) (map fst autos)

1405

1406trivial' ist

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

1408proofSearch' ist rec ambigok depth prv top n hints

1409 = do unifyProblems

1410 proofSearch rec prv ambigok (not prv) depth

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

1412

1413-- Resolve type classes. This will only pick up 'normal' instances, never

1414-- named instances (hence using 'tcname' to check it's a generated instance

1415-- name).

1416resolveTC :: Bool -- using default Int

1417 -> Bool -- allow metavariables in the goal

1418 -> Int -- depth

1419 -> Term -- top level goal

1420 -> Name -- top level function name

1421 -> IState -> ElabD ()

1422resolveTC def mvok depth top fn ist

1423 = do hs <- get_holes

1424 resTC' [] def hs depth top fn ist

1425

1426resTC' tcs def topholes 0 topg fn ist = fail $ "Can't resolve type class"

1427resTC' tcs def topholes 1 topg fn ist = try' (trivial' ist) (resolveTC def False 0 topg fn ist) True

1428resTC' tcs defaultOn topholes depth topg fn ist

1429 = do compute

1430 g <- goal

1431 let argsok = tcArgsOK g topholes

1432-- trace (show (g,hs,argsok,topholes)) $

1433 if not argsok -- && not mvok)

1434 then lift $ tfail $ CantResolve True topg

1435 else do

1436 ptm <- get_term

1437 ulog <- getUnifyLog

1438 hs <- get_holes

1439 traceWhen ulog ("Resolving class " ++ show g) $

1440 try' (trivial' ist)

1441 (do t <- goal

1442 let (tc, ttypes) = unApply t

1443 scopeOnly <- needsDefault t tc ttypes

1444 let stk = elab_stack ist

1445 let insts_in = findInstances ist t

1446 let insts = if scopeOnly then filter chaser insts_in

1447 else insts_in

1448 tm <- get_term

1449 let depth' = if scopeOnly then 2 else depth

1450 blunderbuss t depth' stk (stk ++ insts)) True

1451 where

1452 tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1453 = True

1454 tcArgsOK ty hs -- if any arguments are metavariables, postpone

1455 = let (f, as) = unApply ty in

1456 case f of

1457 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

1458 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

1459 Nothing -> not $ any (isMeta hs) as

1460 _ -> not $ any (isMeta hs) as

1461

1462 tcDetArgsOK i ds hs (x : xs)

1463 | i `elem` ds = not (isMeta hs x) && tcDetArgsOK (i + 1) ds hs xs

1464 | otherwise = tcDetArgsOK (i + 1) ds hs xs

1465 tcDetArgsOK _ _ _ [] = True

1466

1467 isMeta :: [Name] -> Term -> Bool

1468 isMeta ns (P _ n _) = n `elem` ns

1469 isMeta _ _ = False

1470

1471 notHole hs (P _ n _, c)

1472 | (P _ cn _, _) <- unApply c,

1473 n `elem` hs && isConName cn (tt_ctxt ist) = False

1474 | Constant _ <- c = not (n `elem` hs)

1475 notHole _ _ = True

1476

1477 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1478 | otherwise = (fail "Can't resolve", show n)

1479

1480 -- HACK! Rather than giving a special name, better to have some kind

1481 -- of flag in ClassInfo structure

1482 chaser (UN nm)

1483 | ('@':'@':_) <- str nm = True -- old way

1484 chaser (SN (ParentN _ _)) = True

1485 chaser (NS n _) = chaser n

1486 chaser _ = False

1487

1488 numclass = sNS (sUN "Num") ["Classes","Prelude"]

1489

1490 needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

1491 = do focus a

1492 fill (RConstant (AType (ATInt ITBig))) -- default Integer

1493 solve

1494 return False

1495 needsDefault t f as

1496 | all boundVar as = return True -- fail $ "Can't resolve " ++ show t

1497 needsDefault t f a = return False -- trace (show t) $ return ()

1498

1499 boundVar (P Bound _ _) = True

1500 boundVar _ = False

1501

1502 blunderbuss t d stk [] = do -- c <- get_env

1503 -- ps <- get_probs

1504 lift $ tfail $ CantResolve False topg

1505 blunderbuss t d stk (n:ns)

1506 | n /= fn && (n `elem` stk || tcname n)

1507 = tryCatch (resolve n d)

1508 (\e -> case e of

1509 CantResolve True _ -> lift $ tfail e

1510 _ -> blunderbuss t d stk ns)

1511 | otherwise = blunderbuss t d stk ns

1512

1513 resolve n depth

1514 | depth == 0 = fail $ "Can't resolve type class"

1515 | otherwise

1516 = do t <- goal

1517 let (tc, ttypes) = unApply t

1518-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

1519-- else do

1520 -- if there's a hole in the goal, don't even try

1521 let imps = case lookupCtxtName n (idris_implicits ist) of

1522 [] -> []

1523 [args] -> map isImp (snd args) -- won't be overloaded!

1524 xs -> error "The impossible happened - overloading is not expected here!"

1525 ps <- get_probs

1526 tm <- get_term

1527 args <- map snd <$> try' (apply (Var n) imps)

1528 (match_apply (Var n) imps) True

1529 ps' <- get_probs

1530 when (length ps < length ps' || unrecoverable ps') $

1531 fail "Can't apply type class"

1532-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

1533 mapM_ (\ (_,n) -> do focus n

1534 t' <- goal

1535 let (tc', ttype) = unApply t'

1536 let got = fst (unApply t)

1537 let depth' = if tc' `elem` tcs

1538 then depth - 1 else depth

1539 resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

1540 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

1541 -- if there's any arguments left, we've failed to resolve

1542 hs <- get_holes

1543 ulog <- getUnifyLog

1544 solve

1545 traceWhen ulog ("Got " ++ show n) $ return ()

1546 where isImp (PImp p _ _ _ _) = (True, p)

1547 isImp arg = (False, priority arg)

1548

1549collectDeferred :: Maybe Name ->

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

1551collectDeferred top (Bind n (GHole i t) app) =

1552 do ds <- get

1553 t' <- collectDeferred top t

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

1555 collectDeferred top app

1556collectDeferred top (Bind n b t) = do b' <- cdb b

1557 t' <- collectDeferred top t

1558 return (Bind n b' t')

1559 where

1560 cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)

1561 cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)

1562 cdb b = do ty' <- collectDeferred top (binderTy b)

1563 return (b { binderTy = ty' })

1564collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)

1565collectDeferred top t = return t

1566

1567case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

1568case_ ind autoSolve ist fn tm = do

1569 attack

1570 tyn <- getNameFrom (sMN 0 "ity")

1571 claim tyn RType

1572 valn <- getNameFrom (sMN 0 "ival")

1573 claim valn (Var tyn)

1574 letn <- getNameFrom (sMN 0 "irule")

1575 letbind letn (Var tyn) (Var valn)

1576 focus valn

1577 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1578 env <- get_env

1579 let (Just binding) = lookup letn env

1580 let val = binderVal binding

1581 if ind then induction (forget val)

1582 else casetac (forget val)

1583 when autoSolve solveAll

1584

1585tacN :: String -> Name

1586tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1587

1588runTactical :: FC -> Env -> Term -> ElabD ()

1589runTactical fc env tm = do tm' <- eval tm

1590 runTacTm tm'

1591 return ()

1592 where

1593 eval tm = do ctxt <- get_context

1594 return $ normaliseAll ctxt env (finalise tm)

1595

1596 returnUnit = fmap fst $ get_type_val (Var unitCon)

1597

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

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

1600 runTacTm :: Term -> ElabD Term

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

1602 | n == tacN "prim__Solve", [] <- args

1603 = do solve

1604 returnUnit

1605 | n == tacN "prim__Goal", [] <- args

1606 = do (h:_) <- get_holes

1607 t <- goal

1608 fmap fst . get_type_val $

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

1610 (reflectName h, reflect t)

1611 | n == tacN "prim__Holes", [] <- args

1612 = do hs <- get_holes

1613 fmap fst . get_type_val $

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

1615 | n == tacN "prim__Guess", [] <- args

1616 = do ok <- is_guess

1617 if ok

1618 then do guess <- fmap forget get_guess

1619 fmap fst . get_type_val $

1620 RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))

1621 (Var (reflm "TT")))

1622 guess

1623 else fmap fst . get_type_val $

1624 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))

1625 (Var (reflm "TT"))

1626 | n == tacN "prim__SourceLocation", [] <- args

1627 = fmap fst . get_type_val $

1628 reflectFC fc

1629 | n == tacN "prim__Env", [] <- args

1630 = do env <- get_env

1631 fmap fst . get_type_val $ reflectEnv env

1632 | n == tacN "prim__Fail", [_a, errs] <- args

1633 = do errs' <- eval errs

1634 parts <- reifyReportParts errs'

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

1636 | n == tacN "prim__PureTactical", [_a, tm] <- args

1637 = return tm

1638 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1639 = do first' <- eval first

1640 res <- runTacTm first'

1641 next <- eval (App andThen res)

1642 runTacTm next

1643 | n == tacN "prim__Try", [_a, first, alt] <- args

1644 = do first' <- eval first

1645 alt' <- eval alt

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

1647 | n == tacN "prim__Fill", [raw] <- args

1648 = do raw' <- reifyRaw raw

1649 apply raw' []

1650 returnUnit

1651 | n == tacN "prim__Gensym", [hint] <- args

1652 = do hintStr <- eval hint

1653 case hintStr of

1654 Constant (Str h) -> do

1655 n <- getNameFrom (sMN 0 h)

1656 fmap fst $ get_type_val (reflectName n)

1657 _ -> fail "no hint"

1658 | n == tacN "prim__Claim", [n, ty] <- args

1659 = do n' <- reifyTTName n

1660 ty' <- reifyRaw ty

1661 claim n' ty'

1662 returnUnit

1663 | n == tacN "prim__Forget", [tt] <- args

1664 = do tt' <- reifyTT tt

1665 fmap fst . get_type_val $ reflect tt'

1666 | n == tacN "prim__Attack", [] <- args

1667 = do attack

1668 returnUnit

1669 | n == tacN "prim__Rewrite", [rule] <- args

1670 = do r <- reifyRaw rule

1671 rewrite r

1672 returnUnit

1673 | n == tacN "prim__Focus", [what] <- args

1674 = do n' <- reifyTTName what

1675 focus n'

1676 returnUnit

1677 | n == tacN "prim__Unfocus", [what] <- args

1678 = do n' <- reifyTTName what

1679 movelast n'

1680 returnUnit

1681 | n == tacN "prim__Intro", [mn] <- args

1682 = do n <- case fromTTMaybe mn of

1683 Nothing -> return Nothing

1684 Just name -> fmap Just $ reifyTTName name

1685 intro n

1686 returnUnit

1687 | n == tacN "prim__DeclareType", [decl] <- args

1688 = do (RDeclare n args res) <- reifyTyDecl decl

1689 ctxt <- get_context

1690 let mkPi arg res = RBind (argName arg)

1691 (Pi Nothing (argTy arg) (RUType AllTypes))

1692 res

1693 rty = foldr mkPi res args

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

1695 case normaliseAll ctxt [] (finalise ty') of

1696 TType _ -> lift . tfail . InternalMsg $

1697 show checked ++ " is not a type: it's " ++ show ty'

1698 _ -> return ()

1699 case lookupDefExact n ctxt of

1700 Just _ -> lift . tfail . InternalMsg $

1701 show n ++ " is already defined."

1702 Nothing -> return ()

1703 let decl = TyDecl Ref checked

1704 ctxt' = addCtxtDef n decl ctxt

1705 set_context ctxt'

1706 updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :

1707 new_tyDecls e }

1708 aux <- getAux

1709 returnUnit

1710 | n == tacN "prim__Debug", [ty, msg] <- args

1711 = do let msg' = fromTTMaybe msg

1712 case msg' of

1713 Nothing -> debugElaborator Nothing

1714 Just (Constant (Str m)) -> debugElaborator (Just m)

1715 Just x -> lift . tfail . InternalMsg $ "Can't reify message for debugging: " ++ show x

1716 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

1717

1718-- Running tactics directly

1719-- if a tactic adds unification problems, return an error

1720

1721runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()

1722runTac autoSolve ist perhapsFC fn tac

1723 = do env <- get_env

1724 g <- goal

1725 let tac' = fmap (addImplBound ist (map fst env)) tac

1726 if autoSolve

1727 then runT tac'

1728 else no_errors (runT tac')

1729 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

1730 where

1731 runT (Intro []) = do g <- goal

1732 attack; intro (bname g)

1733 where

1734 bname (Bind n _ _) = Just n

1735 bname _ = Nothing

1736 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

1737 runT Intros = do g <- goal

1738 attack;

1739 intro (bname g)

1740 try' (runT Intros)

1741 (return ()) True

1742 where

1743 bname (Bind n _ _) = Just n

1744 bname _ = Nothing

1745 runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm

1746 when autoSolve solveAll

1747 runT (MatchRefine fn)

1748 = do fnimps <-

1749 case lookupCtxtName fn (idris_implicits ist) of

1750 [] -> do a <- envArgs fn

1751 return [(fn, a)]

1752 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)

1753 let tacs = map (\ (fn', imps) ->

1754 (match_apply (Var fn') (map (\x -> (x, 0)) imps),

1755 fn')) fnimps

1756 tryAll tacs

1757 when autoSolve solveAll

1758 where envArgs n = do e <- get_env

1759 case lookup n e of

1760 Just t -> return $ map (const False)

1761 (getArgTys (binderTy t))

1762 _ -> return []

1763 runT (Refine fn [])

1764 = do fnimps <-

1765 case lookupCtxtName fn (idris_implicits ist) of

1766 [] -> do a <- envArgs fn

1767 return [(fn, a)]

1768 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)

1769 let tacs = map (\ (fn', imps) ->

1770 (apply (Var fn') (map (\x -> (x, 0)) imps),

1771 fn')) fnimps

1772 tryAll tacs

1773 when autoSolve solveAll

1774 where isImp (PImp _ _ _ _ _) = True

1775 isImp _ = False

1776 envArgs n = do e <- get_env

1777 case lookup n e of

1778 Just t -> return $ map (const False)

1779 (getArgTys (binderTy t))

1780 _ -> return []

1781 runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)

1782 when autoSolve solveAll

1783 runT DoUnify = do unify_all

1784 when autoSolve solveAll

1785 runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal")

1786 claim tmHole RType

1787 claim n (Var tmHole)

1788 focus tmHole

1789 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1790 focus n

1791 runT (Equiv tm) -- let bind tm, then

1792 = do attack

1793 tyn <- getNameFrom (sMN 0 "ety")

1794 claim tyn RType

1795 valn <- getNameFrom (sMN 0 "eqval")

1796 claim valn (Var tyn)

1797 letn <- getNameFrom (sMN 0 "equiv_val")

1798 letbind letn (Var tyn) (Var valn)

1799 focus tyn

1800 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1801 focus valn

1802 when autoSolve solveAll

1803 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

1804 = do attack; -- (h:_) <- get_holes

1805 tyn <- getNameFrom (sMN 0 "rty")

1806 -- start_unify h

1807 claim tyn RType

1808 valn <- getNameFrom (sMN 0 "rval")

1809 claim valn (Var tyn)

1810 letn <- getNameFrom (sMN 0 "rewrite_rule")

1811 letbind letn (Var tyn) (Var valn)

1812 focus valn

1813 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1814 rewrite (Var letn)

1815 when autoSolve solveAll

1816 runT (Induction tm) -- let bind tm, similar to the others

1817 = case_ True autoSolve ist fn tm

1818 runT (CaseTac tm)

1819 = case_ False autoSolve ist fn tm

1820 runT (LetTac n tm)

1821 = do attack

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

1823 claim tyn RType

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

1825 claim valn (Var tyn)

1826 letn <- unique_hole n

1827 letbind letn (Var tyn) (Var valn)

1828 focus valn

1829 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1830 when autoSolve solveAll

1831 runT (LetTacTy n ty tm)

1832 = do attack

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

1834 claim tyn RType

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

1836 claim valn (Var tyn)

1837 letn <- unique_hole n

1838 letbind letn (Var tyn) (Var valn)

1839 focus tyn

1840 elab ist toplevel ERHS [] (sMN 0 "tac") ty

1841 focus valn

1842 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1843 when autoSolve solveAll

1844 runT Compute = compute

1845 runT Trivial = do trivial' ist; when autoSolve solveAll

1846 runT TCInstance = runT (Exact (PResolveTC emptyFC))

1847 runT (ProofSearch rec prover depth top hints)

1848 = do proofSearch' ist rec False depth prover top fn hints

1849 when autoSolve solveAll

1850 runT (Focus n) = focus n

1851 runT Unfocus = do hs <- get_holes

1852 case hs of

1853 [] -> return ()

1854 (h : _) -> movelast h

1855 runT Solve = solve

1856 runT (Try l r) = do try' (runT l) (runT r) True

1857 runT (TSeq l r) = do runT l; runT r

1858 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment

1859 tgoal <- goal -- store the goal

1860 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...

1861 script <- getNameFrom (sMN 0 "script")

1862 claim script scriptTy

1863 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

1864 letbind scriptvar scriptTy (Var script)

1865 focus script

1866 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1867 (script', _) <- get_type_val (Var scriptvar)

1868 -- now that we have the script apply

1869 -- it to the reflected goal and context

1870 restac <- getNameFrom (sMN 0 "restac")

1871 claim restac tacticTy

1872 focus restac

1873 fill (raw_apply (forget script')

1874 [reflectEnv tenv, reflect tgoal])

1875 restac' <- get_guess

1876 solve

1877 -- normalise the result in order to

1878 -- reify it

1879 ctxt <- get_context

1880 env <- get_env

1881 let tactic = normalise ctxt env restac'

1882 runReflected tactic

1883 where tacticTy = Var (reflm "Tactic")

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

1885 scriptTy = (RBind (sMN 0 "__pi_arg")

1886 (Pi Nothing (RApp listTy envTupleType) RType)

1887 (RBind (sMN 1 "__pi_arg")

1888 (Pi Nothing (Var $ reflm "TT") RType) tacticTy))

1889 runT (ByReflection tm) -- run the reflection function 'tm' on the

1890 -- goal, then apply the resulting reflected Tactic

1891 = do tgoal <- goal

1892 attack

1893 script <- getNameFrom (sMN 0 "script")

1894 claim script scriptTy

1895 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

1896 letbind scriptvar scriptTy (Var script)

1897 focus script

1898 ptm <- get_term

1899 elab ist toplevel ERHS [] (sMN 0 "tac")

1900 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

1901 (script', _) <- get_type_val (Var scriptvar)

1902 -- now that we have the script apply

1903 -- it to the reflected goal

1904 restac <- getNameFrom (sMN 0 "restac")

1905 claim restac tacticTy

1906 focus restac

1907 fill (forget script')

1908 restac' <- get_guess

1909 solve

1910 -- normalise the result in order to

1911 -- reify it

1912 ctxt <- get_context

1913 env <- get_env

1914 let tactic = normalise ctxt env restac'

1915 runReflected tactic

1916 where tacticTy = Var (reflm "Tactic")

1917 scriptTy = tacticTy

1918

1919 runT (Reflect v) = do attack -- let x = reflect v in ...

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

1921 claim tyn RType

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

1923 claim valn (Var tyn)

1924 letn <- getNameFrom (sMN 0 "letvar")

1925 letbind letn (Var tyn) (Var valn)

1926 focus valn

1927 elab ist toplevel ERHS [] (sMN 0 "tac") v

1928 (value, _) <- get_type_val (Var letn)

1929 ctxt <- get_context

1930 env <- get_env

1931 let value' = hnf ctxt env value

1932 runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))

1933 runT (Fill v) = do attack -- let x = fill x in ...

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

1935 claim tyn RType

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

1937 claim valn (Var tyn)

1938 letn <- getNameFrom (sMN 0 "letvar")

1939 letbind letn (Var tyn) (Var valn)

1940 focus valn

1941 elab ist toplevel ERHS [] (sMN 0 "tac") v

1942 (value, _) <- get_type_val (Var letn)

1943 ctxt <- get_context

1944 env <- get_env

1945 let value' = normalise ctxt env value

1946 rawValue <- reifyRaw value'

1947 runTac autoSolve ist perhapsFC fn (Exact $ PQuote rawValue)

1948 runT (GoalType n tac) = do g <- goal

1949 case unApply g of

1950 (P _ n' _, _) ->

1951 if nsroot n' == sUN n

1952 then runT tac

1953 else fail "Wrong goal type"

1954 _ -> fail "Wrong goal type"

1955 runT ProofState = do g <- goal

1956 return ()

1957 runT Skip = return ()

1958 runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")

1959 runT SourceFC =

1960 case perhapsFC of

1961 Nothing -> lift . tfail $ Msg "There is no source location available."

1962 Just fc ->

1963 do fill $ reflectFC fc

1964 solve

1965 runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"

1966 runT x = fail $ "Not implemented " ++ show x

1967

1968 runReflected t = do t' <- reify ist t

1969 runTac autoSolve ist perhapsFC fn t'

1970

1971-- | Prefix a name with the "Language.Reflection" namespace

1972reflm :: String -> Name

1973reflm n = sNS (sUN n) ["Reflection", "Language"]

1974

1975

1976-- | Reify tactics from their reflected representation

1977reify :: IState -> Term -> ElabD PTactic

1978reify _ (P _ n _) | n == reflm "Intros" = return Intros

1979reify _ (P _ n _) | n == reflm "Trivial" = return Trivial

1980reify _ (P _ n _) | n == reflm "Instance" = return TCInstance

1981reify _ (P _ n _) | n == reflm "Solve" = return Solve

1982reify _ (P _ n _) | n == reflm "Compute" = return Compute

1983reify _ (P _ n _) | n == reflm "Skip" = return Skip

1984reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

1985reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus

1986reify ist t@(App _ _)

1987 | (P _ f _, args) <- unApply t = reifyApp ist f args

1988reify _ t = fail ("Unknown tactic " ++ show t)

1989

1990reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

1991reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)

1992reifyApp _ t [Constant (I i)]

1993 | t == reflm "Search" = return (ProofSearch True True i Nothing [])

1994reifyApp _ t [x]

1995 | t == reflm "Refine" = do n <- reifyTTName x

1996 return $ Refine n []

1997reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n

1998 goal <- reifyTT ty

1999 return $ Claim n' (delab ist goal)

2000reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)

2001reifyApp ist t [Constant (Str n), x]

2002 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

2003reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)

2004reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')

2005reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')

2006reifyApp ist t [t']

2007 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

2008reifyApp ist t [t']

2009 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')

2010reifyApp ist t [t']

2011 | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')

2012reifyApp _ t [t']

2013 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')

2014reifyApp ist t [t']

2015 | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')

2016reifyApp ist t [x]

2017 | t == reflm "Focus" = liftM Focus (reifyTTName x)

2018reifyApp ist t [t']

2019 | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')

2020reifyApp ist t [n, t']

2021 | t == reflm "LetTac" = do n' <- reifyTTName n

2022 t'' <- reifyTT t'

2023 return $ LetTac n' (delab ist t')

2024reifyApp ist t [n, tt', t']

2025 | t == reflm "LetTacTy" = do n' <- reifyTTName n

2026 tt'' <- reifyTT tt'

2027 t'' <- reifyTT t'

2028 return $ LetTacTy n' (delab ist tt'') (delab ist t'')

2029reifyApp ist t [errs]

2030 | t == reflm "Fail" = fmap TFail (reifyReportParts errs)

2031reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

2032

2033reifyReportParts :: Term -> ElabD [ErrorReportPart]

2034reifyReportParts errs =

2035 case unList errs of

2036 Nothing -> fail "Failed to reify errors"

2037 Just errs' ->

2038 let parts = mapM reifyReportPart errs' in

2039 case parts of

2040 Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err

2041 Right errs'' ->

2042 return errs''

2043

2044-- | Reify terms from their reflected representation

2045reifyTT :: Term -> ElabD Term

2046reifyTT t@(App _ _)

2047 | (P _ f _, args) <- unApply t = reifyTTApp f args

2048reifyTT t@(P _ n _)

2049 | n == reflm "Erased" = return $ Erased

2050reifyTT t@(P _ n _)

2051 | n == reflm "Impossible" = return $ Impossible

2052reifyTT t = fail ("Unknown reflection term: " ++ show t)

2053

2054reifyTTApp :: Name -> [Term] -> ElabD Term

2055reifyTTApp t [nt, n, x]

2056 | t == reflm "P" = do nt' <- reifyTTNameType nt

2057 n' <- reifyTTName n

2058 x' <- reifyTT x

2059 return $ P nt' n' x'

2060reifyTTApp t [Constant (I i)]

2061 | t == reflm "V" = return $ V i

2062reifyTTApp t [n, b, x]

2063 | t == reflm "Bind" = do n' <- reifyTTName n

2064 b' <- reifyTTBinder reifyTT (reflm "TT") b

2065 x' <- reifyTT x

2066 return $ Bind n' b' x'

2067reifyTTApp t [f, x]

2068 | t == reflm "App" = do f' <- reifyTT f

2069 x' <- reifyTT x

2070 return $ App f' x'

2071reifyTTApp t [c]

2072 | t == reflm "TConst" = liftM Constant (reifyTTConst c)

2073reifyTTApp t [t', Constant (I i)]

2074 | t == reflm "Proj" = do t'' <- reifyTT t'

2075 return $ Proj t'' i

2076reifyTTApp t [tt]

2077 | t == reflm "TType" = liftM TType (reifyTTUExp tt)

2078reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

2079

2080-- | Reify raw terms from their reflected representation

2081reifyRaw :: Term -> ElabD Raw

2082reifyRaw t@(App _ _)

2083 | (P _ f _, args) <- unApply t = reifyRawApp f args

2084reifyRaw t@(P _ n _)

2085 | n == reflm "RType" = return $ RType

2086reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)

2087

2088reifyRawApp :: Name -> [Term] -> ElabD Raw

2089reifyRawApp t [n]

2090 | t == reflm "Var" = liftM Var (reifyTTName n)

2091reifyRawApp t [n, b, x]

2092 | t == reflm "RBind" = do n' <- reifyTTName n

2093 b' <- reifyTTBinder reifyRaw (reflm "Raw") b

2094 x' <- reifyRaw x

2095 return $ RBind n' b' x'

2096reifyRawApp t [f, x]

2097 | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)

2098reifyRawApp t [t']

2099 | t == reflm "RForce" = liftM RForce (reifyRaw t')

2100reifyRawApp t [c]

2101 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)

2102reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))

2103

2104reifyTTName :: Term -> ElabD Name

2105reifyTTName t

2106 | (P _ f _, args) <- unApply t = reifyTTNameApp f args

2107reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

2108

2109reifyTTNameApp :: Name -> [Term] -> ElabD Name

2110reifyTTNameApp t [Constant (Str n)]

2111 | t == reflm "UN" = return $ sUN n

2112reifyTTNameApp t [n, ns]

2113 | t == reflm "NS" = do n' <- reifyTTName n

2114 ns' <- reifyTTNamespace ns

2115 return $ sNS n' ns'

2116reifyTTNameApp t [Constant (I i), Constant (Str n)]

2117 | t == reflm "MN" = return $ sMN i n

2118reifyTTNameApp t []

2119 | t == reflm "NErased" = return NErased

2120reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

2121

2122reifyTTNamespace :: Term -> ElabD [String]

2123reifyTTNamespace t@(App _ _)

2124 = case unApply t of

2125 (P _ f _, [Constant StrType])

2126 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []

2127 (P _ f _, [Constant StrType, Constant (Str n), ns])

2128 | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)

2129 _ -> fail ("Unknown reflection namespace arg: " ++ show t)

2130reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

2131

2132reifyTTNameType :: Term -> ElabD NameType

2133reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound

2134reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

2135reifyTTNameType t@(App _ _)

2136 = case unApply t of

2137 (P _ f _, [Constant (I tag), Constant (I num)])

2138 | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!

2139 | f == reflm "TCon" -> return $ TCon tag num

2140 _ -> fail ("Unknown reflection name type: " ++ show t)

2141reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

2142

2143reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

2144reifyTTBinder reificator binderType t@(App _ _)

2145 = case unApply t of

2146 (P _ f _, bt:args) | forget bt == Var binderType

2147 -> reifyTTBinderApp reificator f args

2148 _ -> fail ("Mismatching binder reflection: " ++ show t)

2149reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)

2150

2151reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

2152reifyTTBinderApp reif f [t]

2153 | f == reflm "Lam" = liftM Lam (reif t)

2154reifyTTBinderApp reif f [t, k]

2155 | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)

2156reifyTTBinderApp reif f [x, y]

2157 | f == reflm "Let" = liftM2 Let (reif x) (reif y)

2158reifyTTBinderApp reif f [x, y]

2159 | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)

2160reifyTTBinderApp reif f [t]

2161 | f == reflm "Hole" = liftM Hole (reif t)

2162reifyTTBinderApp reif f [t]

2163 | f == reflm "GHole" = liftM (GHole 0) (reif t)

2164reifyTTBinderApp reif f [x, y]

2165 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)

2166reifyTTBinderApp reif f [t]

2167 | f == reflm "PVar" = liftM PVar (reif t)

2168reifyTTBinderApp reif f [t]

2169 | f == reflm "PVTy" = liftM PVTy (reif t)

2170reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

2171

2172reifyTTConst :: Term -> ElabD Const

2173reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

2174reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

2175reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

2176reifyTTConst t@(App _ _)

2177 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

2178reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

2179

2180reifyTTConstApp :: Name -> Term -> ElabD Const

2181reifyTTConstApp f aty

2182 | f == reflm "AType" = fmap AType (reifyArithTy aty)

2183reifyTTConstApp f (Constant c@(I _))

2184 | f == reflm "I" = return $ c

2185reifyTTConstApp f (Constant c@(BI _))

2186 | f == reflm "BI" = return $ c

2187reifyTTConstApp f (Constant c@(Fl _))

2188 | f == reflm "Fl" = return $ c

2189reifyTTConstApp f (Constant c@(I _))

2190 | f == reflm "Ch" = return $ c

2191reifyTTConstApp f (Constant c@(Str _))

2192 | f == reflm "Str" = return $ c

2193reifyTTConstApp f (Constant c@(B8 _))

2194 | f == reflm "B8" = return $ c

2195reifyTTConstApp f (Constant c@(B16 _))

2196 | f == reflm "B16" = return $ c

2197reifyTTConstApp f (Constant c@(B32 _))

2198 | f == reflm "B32" = return $ c

2199reifyTTConstApp f (Constant c@(B64 _))

2200 | f == reflm "B64" = return $ c

2201reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

2202

2203reifyArithTy :: Term -> ElabD ArithTy

2204reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

2205reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

2206reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

2207

2208reifyNativeTy :: Term -> ElabD NativeTy

2209reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2210reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2211reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2212reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

2213reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x

2214

2215reifyIntTy :: Term -> ElabD IntTy

2216reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)

2217reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative

2218reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig

2219reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

2220reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

2221

2222reifyTTUExp :: Term -> ElabD UExp

2223reifyTTUExp t@(App _ _)

2224 = case unApply t of

2225 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

2226 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

2227 _ -> fail ("Unknown reflection type universe expression: " ++ show t)

2228reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

2229

2230-- | Create a reflected call to a named function/constructor

2231reflCall :: String -> [Raw] -> Raw

2232reflCall funName args

2233 = raw_apply (Var (reflm funName)) args

2234

2235-- | Lift a term into its Language.Reflection.TT representation

2236reflect :: Term -> Raw

2237reflect = reflectTTQuote []

2238

2239-- | Lift a term into its Language.Reflection.Raw representation

2240reflectRaw :: Raw -> Raw

2241reflectRaw = reflectRawQuote []

2242

2243claimTT :: Name -> ElabD Name

2244claimTT n = do n' <- getNameFrom n

2245 claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))

2246 return n'

2247

2248-- | Convert a reflected term to a more suitable form for pattern-matching.

2249-- In particular, the less-interesting bits are elaborated to _ patterns. This

2250-- happens to NameTypes, universe levels, names that are bound but not used,

2251-- and the type annotation field of the P constructor.

2252reflectTTQuotePattern :: [Name] -> Term -> ElabD ()

2253reflectTTQuotePattern unq (P _ n _)

2254 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them

2255 do fill (Var n) ; solve

2256 | otherwise =

2257 do tyannot <- claimTT (sMN 0 "pTyAnnot")

2258 movelast tyannot -- use a _ pattern here

2259 nt <- getNameFrom (sMN 0 "nt")

2260 claim nt (Var (reflm "NameType"))

2261 movelast nt -- use a _ pattern here

2262 n' <- getNameFrom (sMN 0 "n")

2263 claim n' (Var (reflm "TTName"))

2264 fill $ reflCall "P" [Var nt, Var n', Var tyannot]

2265 solve

2266 focus n'; reflectNameQuotePattern n

2267reflectTTQuotePattern unq (V n)

2268 = do fill $ reflCall "V" [RConstant (I n)]

2269 solve

2270reflectTTQuotePattern unq (Bind n b x)

2271 = do x' <- claimTT (sMN 0 "sc")

2272 movelast x'

2273 b' <- getNameFrom (sMN 0 "binder")

2274 claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))

2275 (Var (sNS (sUN "TT") ["Reflection", "Language"])))

2276 if n `elem` freeNames x

2277 then do fill $ reflCall "Bind"

2278 [reflectName n,

2279 Var b',

2280 Var x']

2281 solve

2282 else do any <- getNameFrom (sMN 0 "anyName")

2283 claim any (Var (reflm "TTName"))

2284 movelast any

2285 fill $ reflCall "Bind"

2286 [Var any,

2287 Var b',

2288 Var x']

2289 solve

2290 focus x'; reflectTTQuotePattern unq x

2291 focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

2292reflectTTQuotePattern unq (App f x)

2293 = do f' <- claimTT (sMN 0 "f"); movelast f'

2294 x' <- claimTT (sMN 0 "x"); movelast x'

2295 fill $ reflCall "App" [Var f', Var x']

2296 solve

2297 focus f'; reflectTTQuotePattern unq f

2298 focus x'; reflectTTQuotePattern unq x

2299reflectTTQuotePattern unq (Constant c)

2300 = do fill $ reflCall "TConst" [reflectConstant c]

2301 solve

2302reflectTTQuotePattern unq (Proj t i)

2303 = do t' <- claimTT (sMN 0 "t"); movelast t'

2304 fill $ reflCall "Proj" [Var t', RConstant (I i)]

2305 solve

2306 focus t'; reflectTTQuotePattern unq t

2307reflectTTQuotePattern unq (Erased)

2308 = do erased <- claimTT (sMN 0 "erased")

2309 movelast erased

2310 fill $ (Var erased)

2311 solve

2312reflectTTQuotePattern unq (Impossible)

2313 = do fill $ Var (reflm "Impossible")

2314 solve

2315reflectTTQuotePattern unq (TType exp)

2316 = do ue <- getNameFrom (sMN 0 "uexp")

2317 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

2318 movelast ue

2319 fill $ reflCall "TType" [Var ue]

2320 solve

2321reflectTTQuotePattern unq (UType u)

2322 = do uH <- getNameFrom (sMN 0 "someUniv")

2323 claim uH (Var (reflm "Universe"))

2324 movelast uH

2325 fill $ reflCall "UType" [Var uH]

2326 solve

2327 focus uH

2328 fill (Var (reflm (case u of

2329 NullType -> "NullType"

2330 UniqueType -> "UniqueType"

2331 AllTypes -> "AllTypes")))

2332 solve

2333

2334reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()

2335reflectRawQuotePattern unq (Var n)

2336 -- the unquoted names already have types, just use them

2337 | n `elem` unq = do fill (Var n); solve

2338 | otherwise = do fill (reflCall "Var" [reflectName n]); solve

2339reflectRawQuotePattern unq (RBind n b sc) =

2340 do scH <- getNameFrom (sMN 0 "sc")

2341 claim scH (Var (reflm "Raw"))

2342 movelast scH

2343 bH <- getNameFrom (sMN 0 "binder")

2344 claim bH (RApp (Var (reflm "Binder"))

2345 (Var (reflm "Raw")))

2346 if n `elem` freeNamesR sc

2347 then do fill $ reflCall "RBind" [reflectName n,

2348 Var bH,

2349 Var scH]

2350 solve

2351 else do any <- getNameFrom (sMN 0 "anyName")

2352 claim any (Var (reflm "TTName"))

2353 movelast any

2354 fill $ reflCall "RBind" [Var any, Var bH, Var scH]

2355 solve

2356 focus scH; reflectRawQuotePattern unq sc

2357 focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b

2358 where freeNamesR (Var n) = [n]

2359 freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,

2360 freeNamesR body \\ [n],

2361 freeNamesR t]

2362 freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++

2363 (freeNamesR body \\ [n])

2364 freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x

2365 freeNamesR RType = []

2366 freeNamesR (RUType _) = []

2367 freeNamesR (RForce r) = freeNamesR r

2368 freeNamesR (RConstant _) = []

2369reflectRawQuotePattern unq (RApp f x) =

2370 do fH <- getNameFrom (sMN 0 "f")

2371 claim fH (Var (reflm "Raw"))

2372 movelast fH

2373 xH <- getNameFrom (sMN 0 "x")

2374 claim xH (Var (reflm "Raw"))

2375 movelast xH

2376 fill $ reflCall "RApp" [Var fH, Var xH]

2377 solve

2378 focus fH; reflectRawQuotePattern unq f

2379 focus xH; reflectRawQuotePattern unq x

2380reflectRawQuotePattern unq RType =

2381 do fill (Var (reflm "RType"))

2382 solve

2383reflectRawQuotePattern unq (RUType univ) =

2384 do uH <- getNameFrom (sMN 0 "universe")

2385 claim uH (Var (reflm "Universe"))

2386 movelast uH

2387 fill $ reflCall "RUType" [Var uH]

2388 solve

2389 focus uH; fill (reflectUniverse univ); solve

2390reflectRawQuotePattern unq (RForce r) =

2391 do rH <- getNameFrom (sMN 0 "raw")

2392 claim rH (Var (reflm "Raw"))

2393 movelast rH

2394 fill $ reflCall "RForce" [Var rH]

2395 solve

2396 focus rH; reflectRawQuotePattern unq r

2397reflectRawQuotePattern unq (RConstant c) =

2398 do cH <- getNameFrom (sMN 0 "const")

2399 claim cH (Var (reflm "Constant"))

2400 movelast cH

2401 fill (reflCall "RConstant" [Var cH]); solve

2402 focus cH

2403 fill (reflectConstant c); solve

2404

2405reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()

2406reflectBinderQuotePattern q unq (Lam t)

2407 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2408 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

2409 solve

2410 focus t'; q unq t

2411reflectBinderQuotePattern q unq (Pi _ t k)

2412 = do t' <- claimTT (sMN 0 "ty") ; movelast t'

2413 k' <- claimTT (sMN 0 "k"); movelast k';

2414 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

2415 solve

2416 focus t'; q unq t

2417reflectBinderQuotePattern q unq (Let x y)

2418 = do x' <- claimTT (sMN 0 "ty"); movelast x';

2419 y' <- claimTT (sMN 0 "v"); movelast y';

2420 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']

2421 solve

2422 focus x'; q unq x

2423 focus y'; q unq y

2424reflectBinderQuotePattern q unq (NLet x y)

2425 = do x' <- claimTT (sMN 0 "ty"); movelast x'

2426 y' <- claimTT (sMN 0 "v"); movelast y'

2427 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']

2428 solve

2429 focus x'; q unq x

2430 focus y'; q unq y

2431reflectBinderQuotePattern q unq (Hole t)

2432 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2433 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']

2434 solve

2435 focus t'; q unq t

2436reflectBinderQuotePattern q unq (GHole _ t)

2437 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2438 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']

2439 solve

2440 focus t'; q unq t

2441reflectBinderQuotePattern q unq (Guess x y)

2442 = do x' <- claimTT (sMN 0 "ty"); movelast x'

2443 y' <- claimTT (sMN 0 "v"); movelast y'

2444 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']

2445 solve

2446 focus x'; q unq x

2447 focus y'; q unq y

2448reflectBinderQuotePattern q unq (PVar t)

2449 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2450 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']

2451 solve

2452 focus t'; q unq t

2453reflectBinderQuotePattern q unq (PVTy t)

2454 = do t' <- claimTT (sMN 0 "ty"); movelast t'

2455 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']

2456 solve

2457 focus t'; q unq t

2458

2459reflectUniverse :: Universe -> Raw

2460reflectUniverse u =

2461 (Var (reflm (case u of

2462 NullType -> "NullType"

2463 UniqueType -> "UniqueType"

2464 AllTypes -> "AllTypes")))

2465

2466-- | Create a reflected TT term, but leave refs to the provided name intact

2467reflectTTQuote :: [Name] -> Term -> Raw

2468reflectTTQuote unq (P nt n t)

2469 | n `elem` unq = Var n

2470 | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]

2471reflectTTQuote unq (V n)

2472 = reflCall "V" [RConstant (I n)]

2473reflectTTQuote unq (Bind n b x)

2474 = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

2475reflectTTQuote unq (App f x)

2476 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2477reflectTTQuote unq (Constant c)

2478 = reflCall "TConst" [reflectConstant c]

2479reflectTTQuote unq (Proj t i)

2480 = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]

2481reflectTTQuote unq (Erased) = Var (reflm "Erased")

2482reflectTTQuote unq (Impossible) = Var (reflm "Impossible")

2483reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

2484reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]

2485

2486reflectRawQuote :: [Name] -> Raw -> Raw

2487reflectRawQuote unq (Var n)

2488 | n `elem` unq = Var n

2489 | otherwise = reflCall "Var" [reflectName n]

2490reflectRawQuote unq (RBind n b r) =

2491 reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]

2492reflectRawQuote unq (RApp f x) =

2493 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2494reflectRawQuote unq RType = Var (reflm "RType")

2495reflectRawQuote unq (RUType u) =

2496 reflCall "RUType" [reflectUniverse u]

2497reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]

2498reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]

2499

2500reflectNameType :: NameType -> Raw

2501reflectNameType (Bound) = Var (reflm "Bound")

2502reflectNameType (Ref) = Var (reflm "Ref")

2503reflectNameType (DCon x y _)

2504 = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!

2505reflectNameType (TCon x y)

2506 = reflCall "TCon" [RConstant (I x), RConstant (I y)]

2507

2508reflectName :: Name -> Raw

2509reflectName (UN s)

2510 = reflCall "UN" [RConstant (Str (str s))]

2511reflectName (NS n ns)

2512 = reflCall "NS" [ reflectName n

2513 , foldr (\ n s ->

2514 raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )

2515 [ RConstant StrType, RConstant (Str n), s ])

2516 ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )

2517 [ RConstant StrType ])

2518 (map str ns)

2519 ]

2520reflectName (MN i n)

2521 = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]

2522reflectName (NErased) = Var (reflm "NErased")

2523reflectName n = Var (reflm "NErased") -- special name, not yet implemented

2524

2525-- | Elaborate a name to a pattern. This means that NS and UN will be intact.

2526-- MNs corresponding to will care about the string but not the number. All

2527-- others become _.

2528reflectNameQuotePattern :: Name -> ElabD ()

2529reflectNameQuotePattern n@(UN s)

2530 = do fill $ reflectName n

2531 solve

2532reflectNameQuotePattern n@(NS _ _)

2533 = do fill $ reflectName n

2534 solve

2535reflectNameQuotePattern (MN _ n)

2536 = do i <- getNameFrom (sMN 0 "mnCounter")

2537 claim i (RConstant (AType (ATInt ITNative)))

2538 movelast i

2539 fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]

2540 solve

2541reflectNameQuotePattern _ -- for all other names, match any

2542 = do nameHole <- getNameFrom (sMN 0 "name")

2543 claim nameHole (Var (reflm "TTName"))

2544 movelast nameHole

2545 fill (Var nameHole)

2546 solve

2547

2548reflectBinder :: Binder Term -> Raw

2549reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2550

2551reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2552reflectBinderQuote q ty unq (Lam t)

2553 = reflCall "Lam" [Var ty, q unq t]

2554reflectBinderQuote q ty unq (Pi _ t k)

2555 = reflCall "Pi" [Var ty, q unq t, q unq k]

2556reflectBinderQuote q ty unq (Let x y)

2557 = reflCall "Let" [Var ty, q unq x, q unq y]

2558reflectBinderQuote q ty unq (NLet x y)

2559 = reflCall "NLet" [Var ty, q unq x, q unq y]

2560reflectBinderQuote q ty unq (Hole t)

2561 = reflCall "Hole" [Var ty, q unq t]

2562reflectBinderQuote q ty unq (GHole _ t)

2563 = reflCall "GHole" [Var ty, q unq t]

2564reflectBinderQuote q ty unq (Guess x y)

2565 = reflCall "Guess" [Var ty, q unq x, q unq y]

2566reflectBinderQuote q ty unq (PVar t)

2567 = reflCall "PVar" [Var ty, q unq t]

2568reflectBinderQuote q ty unq (PVTy t)

2569 = reflCall "PVTy" [Var ty, q unq t]

2570

2571mkList :: Raw -> [Raw] -> Raw

2572mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

2573mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)

2574 x)

2575 (mkList ty xs)

2576

2577reflectConstant :: Const -> Raw

2578reflectConstant c@(I _) = reflCall "I" [RConstant c]

2579reflectConstant c@(BI _) = reflCall "BI" [RConstant c]

2580reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]

2581reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]

2582reflectConstant c@(Str _) = reflCall "Str" [RConstant c]

2583reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]

2584reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]

2585reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]

2586reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]

2587reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]

2588reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]

2589reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]

2590reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]

2591reflectConstant StrType = Var (reflm "StrType")

2592reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]

2593reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]

2594reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]

2595reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]

2596reflectConstant VoidType = Var (reflm "VoidType")

2597reflectConstant Forgot = Var (reflm "Forgot")

2598reflectConstant WorldType = Var (reflm "WorldType")

2599reflectConstant TheWorld = Var (reflm "TheWorld")

2600

2601reflectUExp :: UExp -> Raw

2602reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

2603reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

2604

2605-- | Reflect the environment of a proof into a List (TTName, Binder TT)

2606reflectEnv :: Env -> Raw

2607reflectEnv = foldr consToEnvList emptyEnvList

2608 where

2609 consToEnvList :: (Name, Binder Term) -> Raw -> Raw

2610 consToEnvList (n, b) l

2611 = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))

2612 [ envTupleType

2613 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")

2614 , (RApp (Var $ reflm "Binder")

2615 (Var $ reflm "TT"))

2616 , reflectName n

2617 , reflectBinder b

2618 ]

2619 , l

2620 ]

2621

2622 emptyEnvList :: Raw

2623 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

2624 [envTupleType]

2625

2626-- | Reflect an error into the internal datatype of Idris -- TODO

2627rawBool :: Bool -> Raw

2628rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])

2629rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])

2630

2631rawNil :: Raw -> Raw

2632rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]

2633

2634rawCons :: Raw -> Raw -> Raw -> Raw

2635rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]

2636

2637rawList :: Raw -> [Raw] -> Raw

2638rawList ty = foldr (rawCons ty) (rawNil ty)

2639

2640rawPairTy :: Raw -> Raw -> Raw

2641rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]

2642

2643rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

2644rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]

2645

2646reflectCtxt :: [(Name, Type)] -> Raw

2647reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))

2648 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")

2649 (reflectName n, reflect t)))

2650 ctxt)

2651

2652reflectErr :: Err -> Raw

2653reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

2654reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]

2655reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =

2656 raw_apply (Var $ reflErrName "CantUnify")

2657 [ rawBool b

2658 , reflect t1

2659 , reflect t2

2660 , reflectErr e

2661 , reflectCtxt ctxt

2662 , RConstant (I i)]

2663reflectErr (InfiniteUnify n tm ctxt) =

2664 raw_apply (Var $ reflErrName "InfiniteUnify")

2665 [ reflectName n

2666 , reflect tm

2667 , reflectCtxt ctxt

2668 ]

2669reflectErr (CantConvert t t' ctxt) =

2670 raw_apply (Var $ reflErrName "CantConvert")

2671 [ reflect t

2672 , reflect t'

2673 , reflectCtxt ctxt

2674 ]

2675reflectErr (CantSolveGoal t ctxt) =

2676 raw_apply (Var $ reflErrName "CantSolveGoal")

2677 [ reflect t

2678 , reflectCtxt ctxt

2679 ]

2680reflectErr (UnifyScope n n' t ctxt) =

2681 raw_apply (Var $ reflErrName "UnifyScope")

2682 [ reflectName n

2683 , reflectName n'

2684 , reflect t

2685 , reflectCtxt ctxt

2686 ]

2687reflectErr (CantInferType str) =

2688 raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]

2689reflectErr (NonFunctionType t t') =

2690 raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']

2691reflectErr (NotEquality t t') =

2692 raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']

2693reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]

2694reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]

2695reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]

2696reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]

2697reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]

2698reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

2699reflectErr (NotInjective t1 t2 t3) =

2700 raw_apply (Var $ reflErrName "NotInjective")

2701 [ reflect t1

2702 , reflect t2

2703 , reflect t3

2704 ]

2705reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2706reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]

2707reflectErr (CantResolveAlts ss) =

2708 raw_apply (Var $ reflErrName "CantResolveAlts")

2709 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2710reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2711reflectErr (NoEliminator str t)

2712 = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2713 reflect t]

2714reflectErr UniverseError = Var $ reflErrName "UniverseError"

2715reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2716reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

2717reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

2718reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

2719reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

2720reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]

2721reflectErr (ProviderError str) =

2722 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

2723reflectErr (LoadingFailed str err) =

2724 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

2725reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

2726

2727-- | Reflect a file context

2728reflectFC :: FC -> Raw

2729reflectFC fc = raw_apply (Var (reflm "FileLoc"))

2730 [ RConstant (Str (fc_fname fc))

2731 , raw_apply (Var pairCon) $

2732 [intTy, intTy] ++

2733 map (RConstant . I)

2734 [ fst (fc_start fc)

2735 , snd (fc_start fc)

2736 ]

2737 , raw_apply (Var pairCon) $

2738 [intTy, intTy] ++

2739 map (RConstant . I)

2740 [ fst (fc_end fc)

2741 , snd (fc_end fc)

2742 ]

2743 ]

2744 where intTy = RConstant (AType (ATInt ITNative))

2745

2746elaboratingArgErr :: [(Name, Name)] -> Err -> Err

2747elaboratingArgErr [] err = err

2748elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

2749 where rewrite (ElaboratingArg _ _ _ _) = Nothing

2750 rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)

2751 rewrite (At fc e) = fmap (At fc) (rewrite e)

2752 rewrite err = Just (ElaboratingArg f x during err)

2753

2754

2755withErrorReflection :: Idris a -> Idris a

2756withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2757 where handle :: Err -> Idris Err

2758 handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"

2759 return e -- Don't do meta-reflection of errors

2760 handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"

2761 return e

2762 -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them

2763 handle e@(At fc err) = do logLvl 3 "Reflecting body of At"

2764 err' <- handle err

2765 return (At fc err')

2766 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"

2767 err' <- handle err

2768 return (Elaborating what n err')

2769 handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"

2770 hs <- getFnHandlers f a

2771 err' <- if null hs

2772 then handle err

2773 else applyHandlers err hs

2774 return (ElaboratingArg f a prev err')

2775 -- ProofSearchFail is an internal detail - so don't expose it

2776 handle (ProofSearchFail e) = handle e

2777 -- TODO: argument-specific error handlers go here for ElaboratingArg

2778 handle e = do ist <- getIState

2779 logLvl 2 "Starting error reflection"

2780 let handlers = idris_errorhandlers ist

2781 applyHandlers e handlers

2782 getFnHandlers :: Name -> Name -> Idris [Name]

2783 getFnHandlers f arg = do ist <- getIState

2784 let funHandlers = maybe M.empty id .

2785 lookupCtxtExact f .

2786 idris_function_errorhandlers $ ist

2787 return . maybe [] S.toList . M.lookup arg $ funHandlers

2788

2789

2790 applyHandlers e handlers =

2791 do ist <- getIState

2792 let err = fmap (errReverse ist) e

2793 logLvl 3 $ "Using reflection handlers " ++

2794 concat (intersperse ", " (map show handlers))

2795 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers

2796

2797 -- Typecheck error handlers - if this fails, then something else was wrong earlier!

2798 handlers <- case mapM (check (tt_ctxt ist) []) reports of

2799 Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e

2800 OK hs -> return hs

2801

2802 -- Normalize error handler terms to produce the new messages

2803 ctxt <- getContext

2804 let results = map (normalise ctxt []) (map fst handlers)

2805 logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

2806

2807 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

2808 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

2809 errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

2810 Left err -> ierror err

2811 Right ok -> return ok

2812 return $ case errorparts of

2813 [] -> e

2814 parts -> ReflectionError errorparts e

2815

2816fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

2817fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

2818 | just == txt "Just" = Just tm

2819fromTTMaybe x = Nothing

2820

2821reflErrName :: String -> Name

2822reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

2823

2824-- | Attempt to reify a report part from TT to the internal

2825-- representation. Not in Idris or ElabD monads because it should be usable

2826-- from either.

2827reifyReportPart :: Term -> Either Err ErrorReportPart

2828reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

2829 Right (TextPart msg)

2830reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2831 | n == reflm "NamePart" =

2832 case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2833 Error e -> Left . InternalMsg $

2834 "could not reify name term " ++

2835 show ttn ++

2836 " when reflecting an error:" ++ show e

2837 OK (n', _)-> Right $ NamePart n'

2838reifyReportPart (App (P (DCon _ _ _) n _) tm)

2839 | n == reflm "TermPart" =

2840 case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of

2841 Error e -> Left . InternalMsg $

2842 "could not reify reflected term " ++

2843 show tm ++

2844 " when reflecting an error:" ++ show e

2845 OK (tm', _) -> Right $ TermPart tm'

2846reifyReportPart (App (P (DCon _ _ _) n _) tm)

2847 | n == reflm "SubReport" =

2848 case unList tm of

2849 Just xs -> do subParts <- mapM reifyReportPart xs

2850 Right (SubReport subParts)

2851 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2852reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2853

2854reifyTyDecl :: Term -> ElabD RTyDecl

2855reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

2856 | n == tacN "Declare" =

2857 do tyN' <- reifyTTName tyN

2858 args' <- case unList args of

2859 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

2860 Just xs -> mapM reifyRArg xs

2861 ret' <- reifyRaw ret

2862 return $ RDeclare tyN' args' ret'

2863 where reifyRArg :: Term -> ElabD RArg

2864 reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

2865 | n == tacN "Explicit" = liftM2 RExplicit

2866 (reifyTTName argN)

2867 (reifyRaw argTy)

2868 | n == tacN "Implicit" = liftM2 RImplicit

2869 (reifyTTName argN)

2870 (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

2871 (reifyTTName argN)

2872 (reifyRaw argTy)

2873 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

2874reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

2875

2876envTupleType :: Raw

2877envTupleType

2878 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

2879 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

2880 ]

2881

2882solveAll = try (do solve; solveAll) (return ())