src/Idris/ElabTerm.hs · Idris-dev

git.iko.soy/Idris-dev

on 7afa310 help sign in

Idris-dev/src/Idris/ElabTerm.hs

2213 lines 101 kB history raw

1{-# LANGUAGE PatternGuards #-}

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 qualified Util.Pretty as U

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

24import Control.Monad

25import Control.Monad.State.Strict

26import Data.List

27import qualified Data.Map as M

28import Data.Maybe (mapMaybe, fromMaybe)

29import qualified Data.Set as S

30import qualified Data.Text as T

31import Data.Vector.Unboxed (Vector)

32import qualified Data.Vector.Unboxed as V

34import Debug.Trace

36data ElabMode = ETyDecl | ELHS | ERHS

37 deriving Eq

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

40-- elaborated, typechecked term.

41--

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

43-- holes to pattern bindings.

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

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

48 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

49build ist info emode opts fn tm

50 = do elab ist info emode opts fn tm

51 let tmIn = tm

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

53 [TIPartial] -> True

54 _ -> False

55 ivs <- get_instances

56 hs <- get_holes

57 ptm <- get_term

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

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

60 when (not pattern) $

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

62 do focus n

63 g <- goal

64 try (resolveTC True 7 g fn ist)

65 (movelast n)) ivs

66 ivs <- get_instances

67 hs <- get_holes

68 when (not pattern) $

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

70 do focus n

71 g <- goal

72 resolveTC True 7 g fn ist) ivs

73 tm <- get_term

74 ctxt <- get_context

75 probs <- get_probs

76 u <- getUnifyLog

77 hs <- get_holes

79 when (not pattern) $

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

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

82 do unify_all; matchProblems True; unifyProblems

84 probs <- get_probs

85 case probs of

86 [] -> return ()

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

88 if inf then return ()

89 else lift (Error e)

91 when tydecl (do update_term orderPats

92 mkPat)

93-- update_term liftPats)

94 is <- getAux

95 tt <- get_term

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

97 log <- getLog

98 if (log /= "") then trace log $ return (tm, ds, is)

99 else return (tm, ds, is)

100 where pattern = emode == ELHS

101 tydecl = emode == ETyDecl

102

103 mkPat = do hs <- get_holes

104 tm <- get_term

105 case hs of

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

107 [] -> return ()

108

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

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

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

112

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

114 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

115buildTC ist info emode opts fn tm

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

117 let ns = allNamesIn tm

118 let tmIn = tm

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

120 [TIPartial] -> True

121 _ -> False

122 initNextNameFrom ns

123 elab ist info emode opts fn tm

124 probs <- get_probs

125 tm <- get_term

126 case probs of

127 [] -> return ()

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

129 else lift (Error e)

130 is <- getAux

131 tt <- get_term

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

133 log <- getLog

134 if (log /= "") then trace log $ return (tm, ds, is)

135 else return (tm, ds, is)

136 where pattern = emode == ELHS

137

138-- Returns the set of declarations we need to add to complete the definition

139-- (most likely case blocks to elaborate)

140

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

142 ElabD ()

143elab ist info emode opts fn tm

144 = do let loglvl = opt_logLevel (idris_options ist)

145 when (loglvl > 5) $ unifyLog True

146 compute -- expand type synonyms, etc

147 elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)

148 end_unify

149 ptm <- get_term

150 when pattern -- convert remaining holes to pattern vars

151 (do update_term orderPats

152 unify_all

153 matchProblems False -- only the ones we matched earlier

154 unifyProblems

155 mkPat)

156 where

157 pattern = emode == ELHS

158 bindfree = emode == ETyDecl || emode == ELHS

159

160 tcgen = Dictionary `elem` opts

161 reflection = Reflection `elem` opts

162

163 isph arg = case getTm arg of

164 Placeholder -> (True, priority arg)

165 tm -> (False, priority arg)

166

167 toElab ina arg = case getTm arg of

168 Placeholder -> Nothing

169 v -> Just (priority arg, elabE ina v)

170

171 toElab' ina arg = case getTm arg of

172 Placeholder -> Nothing

173 v -> Just (elabE ina v)

174

175 mkPat = do hs <- get_holes

176 tm <- get_term

177 case hs of

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

179 [] -> return ()

180

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

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

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

184 -- typically

185 elabE :: (Bool, Bool, Bool, Bool) -> PTerm -> ElabD ()

186 elabE ina t =

187 --do g <- goal

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

189 do ct <- insertCoerce ina t

190 t' <- insertLazy ct

191 g <- goal

192 tm <- get_term

193 ps <- get_probs

194 hs <- get_holes

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

196 -- ++ "\n" ++ show tm

197 -- ++ "\nholes " ++ show hs

198 -- ++ "\nproblems " ++ show ps

199 -- ++ "\n-----------\n") $

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

201 let fc = fileFC "Force"

202 env <- get_env

203 handleError (forceErr env)

204 (elab' ina t')

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

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

207 pimp (sUN "a") Placeholder True,

208 pexp ct])) True

209

210 forceErr env (CantUnify _ t t' _ _ _)

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

212 ht == txt "Lazy'" = True

213 forceErr env (CantUnify _ t t' _ _ _)

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

215 ht == txt "Lazy'" = True

216 forceErr env (InfiniteUnify _ t _)

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

218 ht == txt "Lazy'" = True

219 forceErr env (Elaborating _ _ t) = forceErr env t

220 forceErr env (ElaboratingArg _ _ _ t) = forceErr env t

221 forceErr env (At _ t) = forceErr env t

222 forceErr env t = False

223

224 local f = do e <- get_env

225 return (f `elem` map fst e)

226

227 -- | Is a constant a type?

228 constType :: Const -> Bool

229 constType (AType _) = True

230 constType StrType = True

231 constType PtrType = True

232 constType VoidType = True

233 constType _ = False

234

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

236

237 elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)

238 -> PTerm -- ^ The term to elaborate

239 -> ElabD ()

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

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

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

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

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

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

246 elab' ina (PConstant c) = do apply (RConstant c) []; solve

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

248 elab' ina (PTrue fc _) =

249 do hnf_compute

250 g <- goal

251 case g of

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

253 _ -> elab' ina (PRef fc unitCon)

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

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

256 elab' ina (PResolveTC fc)

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

258 instanceArg c

259 elab' ina (PRefl fc t)

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

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

262 elab' ina (PEq fc Placeholder Placeholder l r)

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

264 claim tyn RType

265 movelast tyn

266 elab' ina (PApp fc (PRef fc eqTy)

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

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

269 pexp l, pexp r]))

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

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

272 claim atyn RType

273 movelast atyn

274 claim btyn RType

275 movelast btyn

276 elab' ina (PApp fc (PRef fc eqTy)

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

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

279 pexp l, pexp r]))

280

281 elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)

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

283 pimp (sUN "B") rt False,

284 pexp l, pexp r])

285 elab' ina@(_, a, inty, qq) (PPair fc _ l r)

286 = do hnf_compute

287 g <- goal

288 case g of

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

290 [pexp l,pexp r])

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

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

293 pimp (sUN "B") Placeholder False,

294 pexp l, pexp r])

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

296 = case t of

297 Placeholder ->

298 do hnf_compute

299 g <- goal

300 case g of

301 TType _ -> asType

302 _ -> asValue

303 _ -> asType

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

305 [pexp t,

306 pexp (PLam n Placeholder r)])

307 asValue = elab' ina (PApp fc (PRef fc existsCon)

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

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

310 pexp l, pexp r])

311 elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon)

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

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

314 pexp l, pexp r])

315 elab' ina (PAlternative True as)

316 = do hnf_compute

317 ty <- goal

318 ctxt <- get_context

319 let (tc, _) = unApply ty

320 env <- get_env

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

322-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

323 tryAll (zip (map (elab' ina) as') (map showHd as'))

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

325 showHd (PRef _ n) = n

326 showHd (PApp _ h _) = showHd h

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

328 elab' ina (PAlternative False as)

329 = trySeq as

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

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

332 try' e1 (trySeq' e1 xs) True

333 trySeq' deferr [] = proofFail deferr

334 trySeq' deferr (x : xs)

335 = try' (elab' ina x) (trySeq' deferr xs) True

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

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

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

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

340 elab' (ina, guarded, inty, qq) (PRef fc n)

341 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq

342 = do ctxt <- get_context

343 let defined = case lookupTy n ctxt of

344 [] -> False

345 _ -> True

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

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

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

349 else if (defined && not guarded)

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

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

352 (do patvar n; ) -- update_term liftPats)

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

354 [] -> False

355 _ -> True

356 bindable (NS _ _) = False

357 bindable (UN xs) = True

358 bindable n = implicitable n

359 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

360 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

361 elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)

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

363 ctxt <- get_context

364 when (isTConName n ctxt) $

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

366 checkPiGoal n

367 attack; intro (Just n);

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

369 elabE (True, a, inty, qq) sc; solve

370 elab' ina@(_, a, inty, qq) (PLam n ty sc)

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

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

373 ctxt <- get_context

374 when (isTConName n ctxt) $

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

376 checkPiGoal n

377 claim tyn RType

378 explicit tyn

379 attack

380 ptm <- get_term

381 hs <- get_holes

382 introTy (Var tyn) (Just n)

383 focus tyn

384 elabE (True, a, True, qq) ty

385 elabE (True, a, inty, qq) sc

386 solve

387 elab' ina@(_, a, _, qq) (PPi _ n Placeholder sc)

388 = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) sc; solve

389 elab' ina@(_, a, _, qq) (PPi _ n ty sc)

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

391 claim tyn RType

392 n' <- case n of

393 MN _ _ -> unique_hole n

394 _ -> return n

395 forall n' (Var tyn)

396 focus tyn

397 elabE (True, a, True, qq) ty

398 elabE (True, a, True, qq) sc

399 solve

400 elab' ina@(_, a, inty, qq) (PLet n ty val sc)

401 = do attack

402 ivs <- get_instances

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

404 claim tyn RType

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

406 claim valn (Var tyn)

407 explicit valn

408 letbind n (Var tyn) (Var valn)

409 case ty of

410 Placeholder -> return ()

411 _ -> do focus tyn

412 explicit tyn

413 elabE (True, a, True, qq) ty

414 focus valn

415 elabE (True, a, True, qq) val

416 ivs' <- get_instances

417 env <- get_env

418 elabE (True, a, inty, qq) sc

419 when (not pattern) $

420 mapM_ (\n -> do focus n

421 g <- goal

422 hs <- get_holes

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

424 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

425 then try (resolveTC True 7 g fn ist)

426 (movelast n)

427 else movelast n)

428 (ivs' \\ ivs)

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

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

431 expandLet n (case lookup n env of

432 Just (Let t v) -> v)

433 solve

434 elab' ina@(_, a, inty, qq) (PGoal fc r n sc) = do

435 rty <- goal

436 attack

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

438 claim tyn RType

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

440 claim valn (Var tyn)

441 letbind n (Var tyn) (Var valn)

442 focus valn

443 elabE (True, a, True, qq) (PApp fc r [pexp (delab ist rty)])

444 env <- get_env

445 computeLet n

446 elabE (True, a, inty, qq) sc

447 solve

448-- elab' ina (PLet n Placeholder

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

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

451 rty <- goal

452 ds <- get_deferred

453 ctxt <- get_context

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

455 -- new function name

456 env <- get_env

457 argTys <- claimArgTys env args

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

459 let fty = fnTy argTys rty

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

461 -- build and defer the function application

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

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

464 -- be explicit.

465 mapM_ elabIArg (zip argTys args)

466 where claimArgTys env [] = return []

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

468 = do nty <- get_type (Var n)

469 ans <- claimArgTys env xs

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

471 claimArgTys env (_ : xs)

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

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

474 claim an RType

475 claim aval (Var an)

476 ans <- claimArgTys env xs

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

478 fnTy [] ret = forget ret

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

480

481 localVar env (PRef _ x)

482 = case lookup x env of

483 Just _ -> Just x

484 _ -> Nothing

485 localVar env _ = Nothing

486

487 elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)

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

489

490 mkN n@(NS _ _) = n

491 mkN n@(SN _) = n

492 mkN n = case namespace info of

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

494 _ -> n

495

496 elab' ina (PMatchApp fc fn)

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

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

499 _ -> lift $ tfail (NoSuchVariable fn)

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

501 solve

502 elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')

503 | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

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

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

506 elab' (ina, g, inty, qq) tm@(PApp fc (PRef _ f) args)

507 = do env <- get_env

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

509 then -- simple app, as below

510 do simple_app (elabE (ina, g, inty, qq) (PRef fc f))

511 (elabE (True, g, inty, qq) (getTm (head args)))

512 (show tm)

513 solve

514 else

515 do ivs <- get_instances

516 ps <- get_probs

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

518 -- function or default definition.

519 let isinf = f == inferCon || tcname f

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

521 -- we can unify with them

522 case lookupCtxt f (idris_classes ist) of

523 [] -> return ()

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

525 -- maybe more things are solvable now

526 unifyProblems

527 ctxt <- get_context

528 let guarded = isConName f ctxt

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

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

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

532 -- mark any type class arguments as injective

533 mapM_ checkIfInjective (map snd ns)

534 unifyProblems -- try again with the new information,

535 -- to help with disambiguation

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

537 let (ns', eargs) = unzip $

538 sortBy cmpArg (zip ns args)

539 ulog <- getUnifyLog

540 elabArgs ist (ina || not isinf, guarded, inty, qq)

541 [] fc False f ns'

542 (f == sUN "Force")

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

544 solve

545 ivs' <- get_instances

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

547 -- i.e. no holes in them

548 when (not pattern || (ina && not tcgen && not guarded)) $

549 mapM_ (\n -> do focus n

550 g <- goal

551 env <- get_env

552 hs <- get_holes

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

554 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

555 then try (resolveTC False 7 g fn ist)

556 (movelast n)

557 else movelast n)

558 (ivs' \\ ivs)

559 where -- normal < alternatives < lambdas < rewrites < tactic < default tactic

560 -- reason for lambdas after alternatives is that having

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

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

563 -- as possible about the type.

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

565 -- retried after more information is in.

566 cmpArg (_, x) (_, y)

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

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

569 | otherwise

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

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

572 where alt t = case getTm t of

573 PAlternative False _ -> 5

574 PAlternative True _ -> 2

575 PTactics _ -> 150

576 PLam _ _ _ -> 3

577 PRewrite _ _ _ _ -> 4

578 PResolveTC _ -> 0

579 _ -> 1

580

581 constraint (PConstraint _ _ _ _) = True

582 constraint _ = False

583

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

585 -- function (so higher score --> done later)

586 -- Only relevant when on lhs

587 conDepth d t | not pattern = 0

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

589 | otherwise = max (100 - d) 1

590 conDepth d (PApp _ f as)

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

592 conDepth d (PPatvar _ _) = 0

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

594 conDepth d Placeholder = 0

595 conDepth d (PResolveTC _) = 0

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

597

598 checkIfInjective n = do

599 env <- get_env

600 case lookup n env of

601 Nothing -> return ()

602 Just b ->

603 case unApply (binderTy b) of

604 (P _ c _, args) ->

605 case lookupCtxt c (idris_classes ist) of

606 [] -> return ()

607 _ -> -- type class, set as injective

608 do mapM_ setinjArg args

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

610 ulog <- getUnifyLog

611 probs <- get_probs

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

613 unifyProblems

614 probs <- get_probs

615 traceWhen ulog (qshow probs) $ return ()

616 _ -> return ()

617

618 setinjArg (P _ n _) = setinj n

619 setinjArg _ = return ()

620

621 tacTm (PTactics _) = True

622 tacTm (PProof _) = True

623 tacTm _ = False

624

625 setInjective (PRef _ n) = setinj n

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

627 setInjective _ = return ()

628

629 elab' ina@(_, a, inty, qq) tm@(PApp fc f [arg])

630 = erun fc $

631 do simple_app (elabE ina f) (elabE (True, a, inty, qq) (getTm arg))

632 (show tm)

633 solve

634 elab' ina Placeholder = do (h : hs) <- get_holes

635 movelast h

636 elab' ina (PMetavar n) =

637 do ptm <- get_term

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

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

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

641 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

642 let n' = mkN n

643 attack

644 defer unique_used n'

645 solve

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

647 mkN n = case namespace info of

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

649 _ -> n

650 elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts

651 elab' ina (PTactics ts)

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

653 | otherwise = elab' ina Placeholder

654 elab' ina (PElabError e) = fail (pshow ist e)

655 elab' ina (PRewrite fc r sc newg)

656 = do attack

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

658 claim tyn RType

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

660 claim valn (Var tyn)

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

662 letbind letn (Var tyn) (Var valn)

663 focus valn

664 elab' ina r

665 compute

666 g <- goal

667 rewrite (Var letn)

668 g' <- goal

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

670 case newg of

671 Nothing -> elab' ina sc

672 Just t -> doEquiv t sc

673 solve

674 where doEquiv t sc =

675 do attack

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

677 claim tyn RType

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

679 claim valn (Var tyn)

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

681 letbind letn (Var tyn) (Var valn)

682 focus tyn

683 elab' ina t

684 focus valn

685 elab' ina sc

686 elab' ina (PRef fc letn)

687 solve

688 elab' ina@(_, a, inty, qq) c@(PCase fc scr opts)

689 = do attack

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

691 claim tyn RType

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

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

694 claim valn (Var tyn)

695 letbind scvn (Var tyn) (Var valn)

696 focus valn

697 elabE (True, a, inty, qq) scr

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

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

700 unifyProblems

701 matchProblems True

702 args <- get_env

703 envU <- mapM (getKind args) args

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

705

706 -- Drop the unique arguments used in the scrutinee (since it's

707 -- not valid to use them again anyway)

708 let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr)

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

710

711 cname <- unique_hole' True (mkCaseName fn)

712 let cname' = mkN cname

713-- elab' ina (PMetavar cname')

714 attack; defer argsDropped cname'; solve

715

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

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

718 let newdef = PClauses fc [] cname'

719 (caseBlock fc cname'

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

721 -- elaborate case

722 updateAux (newdef : )

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

724 movelast tyn

725 solve

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

727 mkCaseName n = SN (CaseN n)

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

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

730 mkN n@(NS _ _) = n

731 mkN n = case namespace info of

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

733 _ -> n

734

735 isUnique envk n = case lookup n envk of

736 Just u -> u

737 _ -> False

738

739 getKind env (n, _)

740 = case lookup n env of

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

742 Just b ->

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

744 case ty of

745 UType UniqueType -> return (n, True)

746 UType AllTypes -> return (n, True)

747 _ -> return (n, False)

748

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

750 = case lookupCtxt n (idris_classes ist) of

751 [_] -> True

752 _ -> False

753 tcName _ = False

754

755 usedIn ns (n, b)

756 = n `elem` ns

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

758

759 -- FIXME: This probably doesn't help us here, but leaving

760 -- it in temporarily... if this comment is still here in master,

761 -- please delete the code!

762 chaseDeps env acc [] = filter (\(n, _) -> n `elem` acc) env

763 chaseDeps env acc ((n,b) : args)

764 = let ns = allTTNames (binderTy b) in

765 extendAcc ns acc args

766 where

767 extendAcc [] acc args = chaseDeps env acc args

768 extendAcc (n:ns) acc args

769 | elem n acc = extendAcc ns acc args

770 | otherwise = case lookup n env of

771 Just b -> extendAcc ns (n : acc)

772 ((n,b) : args)

773 Nothing -> extendAcc ns acc args

774

775 elab' ina (PUnifyLog t) = do unifyLog True

776 elab' ina t

777 unifyLog False

778 elab' (ina, g, inty, qq) (PQuasiquote t goal) -- TODO: goal type

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

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

781 -- of type TT.

782 (t, unq) <- extractUnquotes 0 t

783 let unquoteNames = map fst unq

784 mapM_ (flip claim (Var tt)) unquoteNames

785

786

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

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

789 ctxt <- get_context

790 saveState

791 updatePS (const .

792 newProof (sMN 0 "q") ctxt $

793 P Ref tt Erased)

794

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

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

797 -- of their reflection.

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

799 claim ty RType

800 movelast ty

801 claim n (Var ty)

802 movelast n)

803 unquoteNames

804

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

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

807 -- quasiquoted

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

809 claim qTy RType

810 movelast qTy

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

812 claim qTm (Var qTy)

813

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

815 -- the hole doesn't disappear

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

817 letbind nTm (Var qTy) (Var qTm)

818

819 -- Fill out the goal type, if relevant

820 case goal of

821 Nothing -> return ()

822 Just gTy -> do focus qTy

823 elabE (ina, g, inty, True) gTy

824

825 -- Elaborate the quasiquoted term into the hole

826 focus qTm

827 elabE (ina, g, inty, True) t

828 end_unify

829

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

831 -- original goal in the original proof state.

832 env <- get_env

833 loadState

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

835

836 case quoted of

837 Just q -> do ctxt <- get_context

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

839 if pattern

840 then reflectQuotePattern unquoteNames q'

841 else do fill $ reflectQuote unquoteNames q'

842 solve

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

844

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

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

847 -- the main quotation.

848 mapM_ elabUnquote unq

849 where tt = sNS (sUN "TT") ["Reflection", "Language"]

850

851 elabUnquote (n, tm)

852 = do focus n

853 elabE (ina, g, inty, False) tm

854

855

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

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

858

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

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

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

862

863 caseBlock :: FC -> Name ->

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

865 caseBlock fc n env opts

866 = let args' = findScr env

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

868 map (mkClause args) opts

869

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

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

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

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

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

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

876 findScr (x : xs) = x : findScr xs

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

878

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

880 -- it at the end of the environment

881 scrName n [] = []

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

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

884

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

886

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

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

889 -- old ones with an _

890 mkClause args (l, r)

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

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

893 (map (mkLHSarg l) args') in

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

895

896 mkLHSarg l (tm, True) = pexp l

897 mkLHSarg l (tm, False) = pexp tm

898

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

900 shadowed new t = t

901

902 getFC d (PApp fc _ _) = fc

903 getFC d (PRef fc _) = fc

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

905 getFC d x = d

906

907 insertLazy :: PTerm -> ElabD PTerm

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

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

910 insertLazy (PCoerced t) = return t

911 insertLazy t =

912 do ty <- goal

913 env <- get_env

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

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

916 case tyh of

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

918 -> return (PAlternative False tries)

919 _ -> return t

920 where

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

922 mkDelay env t

923 = let fc = fileFC "Delay" in

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

925 [pexp t])

926

927

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

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

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

931 notImplicitable (PApp _ f _) = notImplicitable f

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

933 notImplicitable (PRef _ n)

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

935 = NoImplicit `elem` opts

936 notImplicitable (PAlternative True as) = any notImplicitable as

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

938 -- they can go in the branches separately.

939 notImplicitable (PCase _ _ _) = True

940 notImplicitable _ = False

941

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

943 insertCoerce ina t | notImplicitable t = return t

944 insertCoerce ina t =

945 do ty <- goal

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

947 -- and add them as 'alternatives'

948 env <- get_env

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

950 let cs = getCoercionsTo ist ty'

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

952 (PCoerced tm, _) -> tm

953 (_, []) -> t

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

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

956 return t'

957 where

958 mkCoerce env t n = let fc = fileFC "Coercion" in -- line never appears!

959 addImplBound ist (map fst env)

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

961

962 -- | Elaborate the arguments to a function

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

964 -> (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a qquote)

965 -> [Bool]

966 -> FC -- ^ Source location

967 -> Bool

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

969 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

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

971 -> [PTerm] -- ^ (Laziness, argument)

972 -> ElabD ()

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

974 elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)

975 = elabArgs ist ina failed fc r f ns force args

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

977 = elabArg argName holeName t

978 where elabArg argName holeName t =

979 do now_elaborating fc f argName

980 wrapErr f argName $ do

981 hs <- get_holes

982 tm <- get_term

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

984 -- recursively!)

985 let elab = if force then elab' else elabE

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

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

988 case holeName `elem` hs of

989 True -> do focus holeName;

990 g <- goal

991 ulog <- getUnifyLog

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

993 elab ina t; return failed

994 False -> return failed

995 done_elaborating_arg f argName

996 elabArgs ist ina failed fc r f ns force args

997 wrapErr f argName action =

998 do elabState <- get

999 while <- elaborating_app

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

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

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

1003 Error e -> do done_elaborating_arg f argName

1004 lift (tfail (elaboratingArgErr while' e))

1005 put newState

1006 return result

1007

1008

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

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

1011

1012pruneAlt :: [PTerm] -> [PTerm]

1013pruneAlt xs = map prune xs

1014 where

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

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

1017 prune t = t

1018

1019 choose f (PAlternative a as)

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

1021 fs = filter (headIs f) as' in

1022 case fs of

1023 [a] -> a

1024 _ -> PAlternative a as'

1025

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

1027 choose f t = t

1028

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

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

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

1032

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

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

1035pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm]

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

1037pruneByType env t c as

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

1039 where

1040 locallyBound [] = Nothing

1041 locallyBound (t:ts)

1042 | Just n <- getName t,

1043 n `elem` env = Just t

1044 | otherwise = locallyBound ts

1045 getName (PRef _ n) = Just n

1046 getName (PApp _ f _) = getName f

1047 getName _ = Nothing

1048

1049pruneByType env (P _ n _) c as

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

1051 | [] <- lookupTy n c = as

1052 | otherwise

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

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

1055 case as' of

1056 [] -> case asV of

1057 [] -> as

1058 _ -> asV

1059 _ -> as'

1060 where

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

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

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

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

1065

1066 typeHead var f f'

1067 = case lookupTy f' c of

1068 [ty] -> let ty' = normalise c [] ty in

1069 case unApply (getRetTy ty') of

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

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

1072 _ -> False

1073 _ -> False

1074

1075pruneByType _ t _ as = as

1076

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

1078findInstances ist t

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

1080 = case lookupCtxt n (idris_classes ist) of

1081 [CI _ _ _ _ _ ins] -> ins

1082 _ -> []

1083 | otherwise = []

1084

1085trivial' ist

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

1087proofSearch' ist rec depth prv top n hints

1088 = do unifyProblems

1089 proofSearch rec prv depth

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

1091

1092resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1093resolveTC = resTC' []

1094

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

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

1097resTC' tcs defaultOn depth topg fn ist

1098 = do hnf_compute

1099 g <- goal

1100 ptm <- get_term

1101 ulog <- getUnifyLog

1102 hs <- get_holes

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

1104 try' (trivial' ist)

1105 (do t <- goal

1106 let (tc, ttypes) = unApply t

1107 scopeOnly <- needsDefault t tc ttypes

1108 let insts_in = findInstances ist t

1109 let insts = if scopeOnly then filter chaser insts_in

1110 else insts_in

1111 tm <- get_term

1112 let depth' = if scopeOnly then 2 else depth

1113 blunderbuss t depth' insts) True

1114 where

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

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

1117

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

1119 -- of flag in ClassInfo structure

1120 chaser (UN nm)

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

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

1123 chaser (NS n _) = chaser n

1124 chaser _ = False

1125

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

1127

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

1129 = do focus a

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

1131 solve

1132 return False

1133 needsDefault t f as

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

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

1136

1137 boundVar (P Bound _ _) = True

1138 boundVar _ = False

1139

1140 blunderbuss t d [] = do -- c <- get_env

1141 -- ps <- get_probs

1142 lift $ tfail $ CantResolve topg

1143 blunderbuss t d (n:ns)

1144 | n /= fn && tcname n = try' (resolve n d)

1145 (blunderbuss t d ns) True

1146 | otherwise = blunderbuss t d ns

1147

1148 resolve n depth

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

1150 | otherwise

1151 = do t <- goal

1152 let (tc, ttypes) = unApply t

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

1154-- else do

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

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

1157 [] -> []

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

1159 ps <- get_probs

1160 tm <- get_term

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

1162 (match_apply (Var n) imps) True

1163 ps' <- get_probs

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

1165 fail "Can't apply type class"

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

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

1168 t' <- goal

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

1170 let got = fst (unApply t)

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

1172 then depth - 1 else depth

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

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

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

1176 hs <- get_holes

1177 ulog <- getUnifyLog

1178 solve

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

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

1181 isImp arg = (False, priority arg)

1182

1183collectDeferred :: Maybe Name ->

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

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

1186 do ds <- get

1187 t' <- collectDeferred top t

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

1189 collectDeferred top app

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

1191 t' <- collectDeferred top t

1192 return (Bind n b' t')

1193 where

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

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

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

1197 return (b { binderTy = ty' })

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

1199collectDeferred top t = return t

1200

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

1202case_ ind autoSolve ist fn tm = do

1203 attack

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

1205 claim tyn RType

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

1207 claim valn (Var tyn)

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

1209 letbind letn (Var tyn) (Var valn)

1210 focus valn

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

1212 env <- get_env

1213 let (Just binding) = lookup letn env

1214 let val = binderVal binding

1215 if ind then induction (forget val)

1216 else casetac (forget val)

1217 when autoSolve solveAll

1218

1219-- Running tactics directly

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

1221

1222runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()

1223runTac autoSolve ist fn tac

1224 = do env <- get_env

1225 g <- goal

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

1227 if autoSolve

1228 then runT tac'

1229 else no_errors (runT tac')

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

1231 where

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

1233 attack; intro (bname g)

1234 where

1235 bname (Bind n _ _) = Just n

1236 bname _ = Nothing

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

1238 runT Intros = do g <- goal

1239 attack; intro (bname g)

1240 try' (runT Intros)

1241 (return ()) True

1242 where

1243 bname (Bind n _ _) = Just n

1244 bname _ = Nothing

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

1246 when autoSolve solveAll

1247 runT (MatchRefine fn)

1248 = do fnimps <-

1249 case lookupCtxtName fn (idris_implicits ist) of

1250 [] -> do a <- envArgs fn

1251 return [(fn, a)]

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

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

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

1255 fn')) fnimps

1256 tryAll tacs

1257 when autoSolve solveAll

1258 where envArgs n = do e <- get_env

1259 case lookup n e of

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

1261 (getArgTys (binderTy t))

1262 _ -> return []

1263 runT (Refine fn [])

1264 = do fnimps <-

1265 case lookupCtxtName fn (idris_implicits ist) of

1266 [] -> do a <- envArgs fn

1267 return [(fn, a)]

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

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

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

1271 fn')) fnimps

1272 tryAll tacs

1273 when autoSolve solveAll

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

1275 isImp _ = False

1276 envArgs n = do e <- get_env

1277 case lookup n e of

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

1279 (getArgTys (binderTy t))

1280 _ -> return []

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

1282 when autoSolve solveAll

1283 runT DoUnify = do unify_all

1284 when autoSolve solveAll

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

1286 = do attack

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

1288 claim tyn RType

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

1290 claim valn (Var tyn)

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

1292 letbind letn (Var tyn) (Var valn)

1293 focus tyn

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

1295 focus valn

1296 when autoSolve solveAll

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

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

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

1300 -- start_unify h

1301 claim tyn RType

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

1303 claim valn (Var tyn)

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

1305 letbind letn (Var tyn) (Var valn)

1306 focus valn

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

1308 rewrite (Var letn)

1309 when autoSolve solveAll

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

1311 = case_ True autoSolve ist fn tm

1312 runT (CaseTac tm)

1313 = case_ False autoSolve ist fn tm

1314 runT (LetTac n tm)

1315 = do attack

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

1317 claim tyn RType

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

1319 claim valn (Var tyn)

1320 letn <- unique_hole n

1321 letbind letn (Var tyn) (Var valn)

1322 focus valn

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

1324 when autoSolve solveAll

1325 runT (LetTacTy n ty tm)

1326 = do attack

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

1328 claim tyn RType

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

1330 claim valn (Var tyn)

1331 letn <- unique_hole n

1332 letbind letn (Var tyn) (Var valn)

1333 focus tyn

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

1335 focus valn

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

1337 when autoSolve solveAll

1338 runT Compute = compute

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

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

1341 runT (ProofSearch rec prover depth top hints)

1342 = do proofSearch' ist rec depth prover top fn hints

1343 when autoSolve solveAll

1344 runT (Focus n) = focus n

1345 runT Solve = solve

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

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

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

1349 tgoal <- goal -- store the goal

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

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

1352 claim script scriptTy

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

1354 letbind scriptvar scriptTy (Var script)

1355 focus script

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

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

1358 -- now that we have the script apply

1359 -- it to the reflected goal and context

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

1361 claim restac tacticTy

1362 focus restac

1363 fill (raw_apply (forget script')

1364 [reflectEnv tenv, reflect tgoal])

1365 restac' <- get_guess

1366 solve

1367 -- normalise the result in order to

1368 -- reify it

1369 ctxt <- get_context

1370 env <- get_env

1371 let tactic = normalise ctxt env restac'

1372 runReflected tactic

1373 where tacticTy = Var (reflm "Tactic")

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

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

1376 (Pi (RApp listTy envTupleType) RType)

1377 (RBind (sMN 1 "__pi_arg")

1378 (Pi (Var $ reflm "TT") RType) tacticTy))

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

1380 -- goal, then apply the resulting reflected Tactic

1381 = do tgoal <- goal

1382 attack

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

1384 claim script scriptTy

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

1386 letbind scriptvar scriptTy (Var script)

1387 focus script

1388 ptm <- get_term

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

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

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

1392 -- now that we have the script apply

1393 -- it to the reflected goal

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

1395 claim restac tacticTy

1396 focus restac

1397 fill (forget script')

1398 restac' <- get_guess

1399 solve

1400 -- normalise the result in order to

1401 -- reify it

1402 ctxt <- get_context

1403 env <- get_env

1404 let tactic = normalise ctxt env restac'

1405 runReflected tactic

1406 where tacticTy = Var (reflm "Tactic")

1407 scriptTy = tacticTy

1408

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

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

1411 claim tyn RType

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

1413 claim valn (Var tyn)

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

1415 letbind letn (Var tyn) (Var valn)

1416 focus valn

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

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

1419 ctxt <- get_context

1420 env <- get_env

1421 let value' = hnf ctxt env value

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

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

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

1425 claim tyn RType

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

1427 claim valn (Var tyn)

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

1429 letbind letn (Var tyn) (Var valn)

1430 focus valn

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

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

1433 ctxt <- get_context

1434 env <- get_env

1435 let value' = normalise ctxt env value

1436 rawValue <- reifyRaw value'

1437 runTac autoSolve ist fn (Exact $ PQuote rawValue)

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

1439 case unApply g of

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

1441 if nsroot n' == sUN n

1442 then runT tac

1443 else fail "Wrong goal type"

1444 _ -> fail "Wrong goal type"

1445 runT ProofState = do g <- goal

1446 return ()

1447 runT Skip = return ()

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

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

1450

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

1452 runTac autoSolve ist fn t'

1453

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

1455reflm :: String -> Name

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

1457

1458

1459-- | Reify tactics from their reflected representation

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

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

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

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

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

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

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

1467reify ist t@(App _ _)

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

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

1470

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

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

1473reifyApp _ t [Constant (I i)]

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

1475reifyApp _ t [x]

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

1477 return $ Refine n []

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

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

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

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

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

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

1484reifyApp ist t [t']

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

1486reifyApp ist t [t']

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

1488reifyApp ist t [t']

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

1490reifyApp _ t [t']

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

1492reifyApp ist t [t']

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

1494reifyApp ist t [x]

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

1496reifyApp ist t [t']

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

1498reifyApp ist t [n, t']

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

1500 t'' <- reifyTT t'

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

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

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

1504 tt'' <- reifyTT tt'

1505 t'' <- reifyTT t'

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

1507reifyApp ist t [errs]

1508 | t == reflm "Fail" = case unList errs of

1509 Nothing -> fail "Failed to reify errors"

1510 Just errs' ->

1511 let parts = mapM reifyReportPart errs' in

1512 case parts of

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

1514 Right errs'' ->

1515 return $ TFail errs''

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

1517

1518-- | Reify terms from their reflected representation

1519reifyTT :: Term -> ElabD Term

1520reifyTT t@(App _ _)

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

1522reifyTT t@(P _ n _)

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

1524reifyTT t@(P _ n _)

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

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

1527

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

1529reifyTTApp t [nt, n, x]

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

1531 n' <- reifyTTName n

1532 x' <- reifyTT x

1533 return $ P nt' n' x'

1534reifyTTApp t [Constant (I i)]

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

1536reifyTTApp t [n, b, x]

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

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

1539 x' <- reifyTT x

1540 return $ Bind n' b' x'

1541reifyTTApp t [f, x]

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

1543 x' <- reifyTT x

1544 return $ App f' x'

1545reifyTTApp t [c]

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

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

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

1549 return $ Proj t'' i

1550reifyTTApp t [tt]

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

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

1553

1554-- | Reify raw terms from their reflected representation

1555reifyRaw :: Term -> ElabD Raw

1556reifyRaw t@(App _ _)

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

1558reifyRaw t@(P _ n _)

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

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

1561

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

1563reifyRawApp t [n]

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

1565reifyRawApp t [n, b, x]

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

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

1568 x' <- reifyRaw x

1569 return $ RBind n' b' x'

1570reifyRawApp t [f, x]

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

1572reifyRawApp t [t']

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

1574reifyRawApp t [c]

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

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

1577

1578reifyTTName :: Term -> ElabD Name

1579reifyTTName t

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

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

1582

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

1584reifyTTNameApp t [Constant (Str n)]

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

1586reifyTTNameApp t [n, ns]

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

1588 ns' <- reifyTTNamespace ns

1589 return $ sNS n' ns'

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

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

1592reifyTTNameApp t []

1593 | t == reflm "NErased" = return NErased

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

1595

1596reifyTTNamespace :: Term -> ElabD [String]

1597reifyTTNamespace t@(App _ _)

1598 = case unApply t of

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

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

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

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

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

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

1605

1606reifyTTNameType :: Term -> ElabD NameType

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

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

1609reifyTTNameType t@(App _ _)

1610 = case unApply t of

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

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

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

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

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

1616

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

1618reifyTTBinder reificator binderType t@(App _ _)

1619 = case unApply t of

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

1621 -> reifyTTBinderApp reificator f args

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

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

1624

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

1626reifyTTBinderApp reif f [t]

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

1628reifyTTBinderApp reif f [t, k]

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

1630reifyTTBinderApp reif f [x, y]

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

1632reifyTTBinderApp reif f [x, y]

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

1634reifyTTBinderApp reif f [t]

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

1636reifyTTBinderApp reif f [t]

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

1638reifyTTBinderApp reif f [x, y]

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

1640reifyTTBinderApp reif f [t]

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

1642reifyTTBinderApp reif f [t]

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

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

1645

1646reifyTTConst :: Term -> ElabD Const

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

1648reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType

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

1650reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

1651reifyTTConst t@(App _ _)

1652 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

1653reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

1654

1655reifyTTConstApp :: Name -> Term -> ElabD Const

1656reifyTTConstApp f aty

1657 | f == reflm "AType" = fmap AType (reifyArithTy aty)

1658reifyTTConstApp f (Constant c@(I _))

1659 | f == reflm "I" = return $ c

1660reifyTTConstApp f (Constant c@(BI _))

1661 | f == reflm "BI" = return $ c

1662reifyTTConstApp f (Constant c@(Fl _))

1663 | f == reflm "Fl" = return $ c

1664reifyTTConstApp f (Constant c@(I _))

1665 | f == reflm "Ch" = return $ c

1666reifyTTConstApp f (Constant c@(Str _))

1667 | f == reflm "Str" = return $ c

1668reifyTTConstApp f (Constant c@(B8 _))

1669 | f == reflm "B8" = return $ c

1670reifyTTConstApp f (Constant c@(B16 _))

1671 | f == reflm "B16" = return $ c

1672reifyTTConstApp f (Constant c@(B32 _))

1673 | f == reflm "B32" = return $ c

1674reifyTTConstApp f (Constant c@(B64 _))

1675 | f == reflm "B64" = return $ c

1676reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

1677

1678reifyArithTy :: Term -> ElabD ArithTy

1679reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)

1680reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat

1681reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

1682

1683reifyNativeTy :: Term -> ElabD NativeTy

1684reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

1685reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

1686reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

1687reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8

1688reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x

1689

1690reifyIntTy :: Term -> ElabD IntTy

1691reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)

1692reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative

1693reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig

1694reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar

1695reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)

1696 (reifyNativeTy nt)

1697

1698reifyTTUExp :: Term -> ElabD UExp

1699reifyTTUExp t@(App _ _)

1700 = case unApply t of

1701 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

1702 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

1703 _ -> fail ("Unknown reflection type universe expression: " ++ show t)

1704reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

1705

1706-- | Create a reflected call to a named function/constructor

1707reflCall :: String -> [Raw] -> Raw

1708reflCall funName args

1709 = raw_apply (Var (reflm funName)) args

1710

1711-- | Lift a term into its Language.Reflection.TT representation

1712reflect :: Term -> Raw

1713reflect = reflectQuote []

1714

1715claimTT :: Name -> ElabD Name

1716claimTT n = do n' <- getNameFrom n

1717 claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))

1718 return n'

1719

1720-- | Convert a reflected term to a more suitable form for pattern-matching.

1721-- In particular, the less-interesting bits are elaborated to _ patterns. This

1722-- happens to NameTypes, universe levels, names that are bound but not used,

1723-- and the type annotation field of the P constructor.

1724reflectQuotePattern :: [Name] -> Term -> ElabD ()

1725reflectQuotePattern unq (P _ n _)

1726 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them

1727 do fill (Var n) ; solve

1728 | otherwise =

1729 do tyannot <- claimTT (sMN 0 "pTyAnnot")

1730 movelast tyannot -- use a _ pattern here

1731 nt <- getNameFrom (sMN 0 "nt")

1732 claim nt (Var (reflm "NameType"))

1733 movelast nt -- use a _ pattern here

1734 n' <- getNameFrom (sMN 0 "n")

1735 claim n' (Var (reflm "TTName"))

1736 fill $ reflCall "P" [Var nt, Var n', Var tyannot]

1737 solve

1738 focus n'; reflectNameQuotePattern n

1739reflectQuotePattern unq (V n)

1740 = do fill $ reflCall "V" [RConstant (I n)]

1741 solve

1742reflectQuotePattern unq (Bind n b x)

1743 = do x' <- claimTT (sMN 0 "sc")

1744 movelast x'

1745 b' <- getNameFrom (sMN 0 "binder")

1746 claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))

1747 (Var (sNS (sUN "TT") ["Reflection", "Language"])))

1748 if n `elem` freeNames x

1749 then do fill $ reflCall "Bind"

1750 [reflectName n,

1751 Var b',

1752 Var x']

1753 solve

1754 else do any <- getNameFrom (sMN 0 "anyName")

1755 claim any (Var (reflm "TTName"))

1756 movelast any

1757 fill $ reflCall "Bind"

1758 [Var any,

1759 Var b',

1760 Var x']

1761 solve

1762 focus x'; reflectQuotePattern unq x

1763 focus b'; reflectBinderQuotePattern unq b

1764

1765 where

1766 reflectBinderQuotePattern :: [Name] -> Binder Term -> ElabD ()

1767 reflectBinderQuotePattern unq (Lam t)

1768 = do t' <- claimTT (sMN 0 "ty"); movelast t'

1769 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

1770 solve

1771 focus t'; reflectQuotePattern unq t

1772 reflectBinderQuotePattern unq (Pi t k)

1773 = do t' <- claimTT (sMN 0 "ty") ; movelast t'

1774 k' <- claimTT (sMN 0 "k"); movelast k';

1775 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

1776 solve

1777 focus t'; reflectQuotePattern unq t

1778 reflectBinderQuotePattern unq (Let x y)

1779 = do x' <- claimTT (sMN 0 "ty"); movelast x';

1780 y' <- claimTT (sMN 0 "v"); movelast y';

1781 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']

1782 solve

1783 focus x'; reflectQuotePattern unq x

1784 focus y'; reflectQuotePattern unq y

1785 reflectBinderQuotePattern unq (NLet x y)

1786 = do x' <- claimTT (sMN 0 "ty"); movelast x'

1787 y' <- claimTT (sMN 0 "v"); movelast y'

1788 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']

1789 solve

1790 focus x'; reflectQuotePattern unq x

1791 focus y'; reflectQuotePattern unq y

1792 reflectBinderQuotePattern unq (Hole t)

1793 = do t' <- claimTT (sMN 0 "ty"); movelast t'

1794 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']

1795 solve

1796 focus t'; reflectQuotePattern unq t

1797 reflectBinderQuotePattern unq (GHole _ t)

1798 = do t' <- claimTT (sMN 0 "ty"); movelast t'

1799 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']

1800 solve

1801 focus t'; reflectQuotePattern unq t

1802 reflectBinderQuotePattern unq (Guess x y)

1803 = do x' <- claimTT (sMN 0 "ty"); movelast x'

1804 y' <- claimTT (sMN 0 "v"); movelast y'

1805 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']

1806 solve

1807 focus x'; reflectQuotePattern unq x

1808 focus y'; reflectQuotePattern unq y

1809 reflectBinderQuotePattern unq (PVar t)

1810 = do t' <- claimTT (sMN 0 "ty"); movelast t'

1811 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']

1812 solve

1813 focus t'; reflectQuotePattern unq t

1814 reflectBinderQuotePattern unq (PVTy t)

1815 = do t' <- claimTT (sMN 0 "ty"); movelast t'

1816 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']

1817 solve

1818 focus t'; reflectQuotePattern unq t

1819reflectQuotePattern unq (App f x)

1820 = do f' <- claimTT (sMN 0 "f"); movelast f'

1821 x' <- claimTT (sMN 0 "x"); movelast x'

1822 fill $ reflCall "App" [Var f', Var x']

1823 solve

1824 focus f'; reflectQuotePattern unq f

1825 focus x'; reflectQuotePattern unq x

1826reflectQuotePattern unq (Constant c)

1827 = do fill $ reflCall "TConst" [reflectConstant c]

1828 solve

1829reflectQuotePattern unq (Proj t i)

1830 = do t' <- claimTT (sMN 0 "t"); movelast t'

1831 fill $ reflCall "Proj" [Var t', RConstant (I i)]

1832 solve

1833 focus t'; reflectQuotePattern unq t

1834reflectQuotePattern unq (Erased)

1835 = do erased <- claimTT (sMN 0 "erased")

1836 movelast erased

1837 fill $ (Var erased)

1838 solve

1839reflectQuotePattern unq (Impossible)

1840 = do fill $ Var (reflm "Impossible")

1841 solve

1842reflectQuotePattern unq (TType exp)

1843 = do ue <- getNameFrom (sMN 0 "uexp")

1844 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

1845 movelast ue

1846 fill $ reflCall "TType" [Var ue]

1847 solve

1848

1849-- | Create a reflected term, but leave refs to the provided name intact

1850reflectQuote :: [Name] -> Term -> Raw

1851reflectQuote unq (P nt n t)

1852 | n `elem` unq = Var n

1853 | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]

1854reflectQuote unq (V n)

1855 = reflCall "V" [RConstant (I n)]

1856reflectQuote unq (Bind n b x)

1857 = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]

1858reflectQuote unq (App f x)

1859 = reflCall "App" [reflectQuote unq f, reflectQuote unq x]

1860reflectQuote unq (Constant c)

1861 = reflCall "TConst" [reflectConstant c]

1862reflectQuote unq (Proj t i)

1863 = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]

1864reflectQuote unq (Erased) = Var (reflm "Erased")

1865reflectQuote unq (Impossible) = Var (reflm "Impossible")

1866reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

1867

1868reflectNameType :: NameType -> Raw

1869reflectNameType (Bound) = Var (reflm "Bound")

1870reflectNameType (Ref) = Var (reflm "Ref")

1871reflectNameType (DCon x y _)

1872 = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!

1873reflectNameType (TCon x y)

1874 = reflCall "TCon" [RConstant (I x), RConstant (I y)]

1875

1876reflectName :: Name -> Raw

1877reflectName (UN s)

1878 = reflCall "UN" [RConstant (Str (str s))]

1879reflectName (NS n ns)

1880 = reflCall "NS" [ reflectName n

1881 , foldr (\ n s ->

1882 raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )

1883 [ RConstant StrType, RConstant (Str n), s ])

1884 ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )

1885 [ RConstant StrType ])

1886 (map str ns)

1887 ]

1888reflectName (MN i n)

1889 = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]

1890reflectName (NErased) = Var (reflm "NErased")

1891reflectName n = Var (reflm "NErased") -- special name, not yet implemented

1892

1893-- | Elaborate a name to a pattern. This means that NS and UN will be intact.

1894-- MNs corresponding to will care about the string but not the number. All

1895-- others become _.

1896reflectNameQuotePattern :: Name -> ElabD ()

1897reflectNameQuotePattern n@(UN s)

1898 = do fill $ reflectName n

1899 solve

1900reflectNameQuotePattern n@(NS _ _)

1901 = do fill $ reflectName n

1902 solve

1903reflectNameQuotePattern (MN _ n)

1904 = do i <- getNameFrom (sMN 0 "mnCounter")

1905 claim i (RConstant (AType (ATInt ITNative)))

1906 movelast i

1907 fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]

1908 solve

1909reflectNameQuotePattern _ -- for all other names, match any

1910 = do nameHole <- getNameFrom (sMN 0 "name")

1911 claim nameHole (Var (reflm "TTName"))

1912 movelast nameHole

1913 fill (Var nameHole)

1914 solve

1915

1916reflectBinder :: Binder Term -> Raw

1917reflectBinder = reflectBinderQuote []

1918

1919reflectBinderQuote :: [Name] -> Binder Term -> Raw

1920reflectBinderQuote unq (Lam t)

1921 = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]

1922reflectBinderQuote unq (Pi t k)

1923 = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]

1924reflectBinderQuote unq (Let x y)

1925 = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

1926reflectBinderQuote unq (NLet x y)

1927 = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

1928reflectBinderQuote unq (Hole t)

1929 = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]

1930reflectBinderQuote unq (GHole _ t)

1931 = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]

1932reflectBinderQuote unq (Guess x y)

1933 = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]

1934reflectBinderQuote unq (PVar t)

1935 = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]

1936reflectBinderQuote unq (PVTy t)

1937 = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]

1938

1939mkList :: Raw -> [Raw] -> Raw

1940mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

1941mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)

1942 x)

1943 (mkList ty xs)

1944

1945reflectConstant :: Const -> Raw

1946reflectConstant c@(I _) = reflCall "I" [RConstant c]

1947reflectConstant c@(BI _) = reflCall "BI" [RConstant c]

1948reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]

1949reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]

1950reflectConstant c@(Str _) = reflCall "Str" [RConstant c]

1951reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]

1952reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]

1953reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]

1954reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]

1955reflectConstant (B8V ws) = reflCall "B8V" [mkList (Var (sUN "Bits8")) . map (RConstant . B8) . V.toList $ ws]

1956reflectConstant (B16V ws) = reflCall "B8V" [mkList (Var (sUN "Bits16")) . map (RConstant . B16) . V.toList $ ws]

1957reflectConstant (B32V ws) = reflCall "B8V" [mkList (Var (sUN "Bits32")) . map (RConstant . B32) . V.toList $ ws]

1958reflectConstant (B64V ws) = reflCall "B8V" [mkList (Var (sUN "Bits64")) . map (RConstant . B64) . V.toList $ ws]

1959reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]

1960reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]

1961reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]

1962reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]

1963reflectConstant StrType = Var (reflm "StrType")

1964reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]

1965reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]

1966reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]

1967reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]

1968reflectConstant (AType (ATInt (ITVec IT8 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT8"), RConstant (I c)]]]

1969reflectConstant (AType (ATInt (ITVec IT16 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT16"), RConstant (I c)]]]

1970reflectConstant (AType (ATInt (ITVec IT32 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT32"), RConstant (I c)]]]

1971reflectConstant (AType (ATInt (ITVec IT64 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT64"), RConstant (I c)]]]

1972reflectConstant PtrType = Var (reflm "PtrType")

1973reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")

1974reflectConstant BufferType = Var (reflm "BufferType")

1975reflectConstant VoidType = Var (reflm "VoidType")

1976reflectConstant Forgot = Var (reflm "Forgot")

1977

1978

1979reflectUExp :: UExp -> Raw

1980reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

1981reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

1982

1983-- | Reflect the environment of a proof into a List (TTName, Binder TT)

1984reflectEnv :: Env -> Raw

1985reflectEnv = foldr consToEnvList emptyEnvList

1986 where

1987 consToEnvList :: (Name, Binder Term) -> Raw -> Raw

1988 consToEnvList (n, b) l

1989 = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))

1990 [ envTupleType

1991 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")

1992 , (RApp (Var $ reflm "Binder")

1993 (Var $ reflm "TT"))

1994 , reflectName n

1995 , reflectBinder b

1996 ]

1997 , l

1998 ]

1999

2000 emptyEnvList :: Raw

2001 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

2002 [envTupleType]

2003

2004-- | Reflect an error into the internal datatype of Idris -- TODO

2005rawBool :: Bool -> Raw

2006rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])

2007rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])

2008

2009rawNil :: Raw -> Raw

2010rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]

2011

2012rawCons :: Raw -> Raw -> Raw -> Raw

2013rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]

2014

2015rawList :: Raw -> [Raw] -> Raw

2016rawList ty = foldr (rawCons ty) (rawNil ty)

2017

2018rawPairTy :: Raw -> Raw -> Raw

2019rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]

2020

2021rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

2022rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]

2023

2024reflectCtxt :: [(Name, Type)] -> Raw

2025reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))

2026 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")

2027 (reflectName n, reflect t)))

2028 ctxt)

2029

2030reflectErr :: Err -> Raw

2031reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

2032reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]

2033reflectErr (CantUnify b t1 t2 e ctxt i) =

2034 raw_apply (Var $ reflErrName "CantUnify")

2035 [ rawBool b

2036 , reflect t1

2037 , reflect t2

2038 , reflectErr e

2039 , reflectCtxt ctxt

2040 , RConstant (I i)]

2041reflectErr (InfiniteUnify n tm ctxt) =

2042 raw_apply (Var $ reflErrName "InfiniteUnify")

2043 [ reflectName n

2044 , reflect tm

2045 , reflectCtxt ctxt

2046 ]

2047reflectErr (CantConvert t t' ctxt) =

2048 raw_apply (Var $ reflErrName "CantConvert")

2049 [ reflect t

2050 , reflect t'

2051 , reflectCtxt ctxt

2052 ]

2053reflectErr (CantSolveGoal t ctxt) =

2054 raw_apply (Var $ reflErrName "CantSolveGoal")

2055 [ reflect t

2056 , reflectCtxt ctxt

2057 ]

2058reflectErr (UnifyScope n n' t ctxt) =

2059 raw_apply (Var $ reflErrName "UnifyScope")

2060 [ reflectName n

2061 , reflectName n'

2062 , reflect t

2063 , reflectCtxt ctxt

2064 ]

2065reflectErr (CantInferType str) =

2066 raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]

2067reflectErr (NonFunctionType t t') =

2068 raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']

2069reflectErr (NotEquality t t') =

2070 raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']

2071reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]

2072reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]

2073reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]

2074reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

2075reflectErr (NotInjective t1 t2 t3) =

2076 raw_apply (Var $ reflErrName "NotInjective")

2077 [ reflect t1

2078 , reflect t2

2079 , reflect t3

2080 ]

2081reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2082reflectErr (CantResolveAlts ss) =

2083 raw_apply (Var $ reflErrName "CantResolveAlts")

2084 [rawList (Var $ (sUN "String")) (map Var ss)]

2085reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2086reflectErr UniverseError = Var $ reflErrName "UniverseError"

2087reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2088reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

2089reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

2090reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

2091reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

2092reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]

2093reflectErr (ProviderError str) =

2094 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]

2095reflectErr (LoadingFailed str err) =

2096 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

2097reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

2098

2099elaboratingArgErr :: [(Name, Name)] -> Err -> Err

2100elaboratingArgErr [] err = err

2101elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

2102 where rewrite (ElaboratingArg _ _ _ _) = Nothing

2103 rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)

2104 rewrite (At fc e) = fmap (At fc) (rewrite e)

2105 rewrite err = Just (ElaboratingArg f x during err)

2106

2107

2108withErrorReflection :: Idris a -> Idris a

2109withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2110 where handle :: Err -> Idris Err

2111 handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"

2112 return e -- Don't do meta-reflection of errors

2113 handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"

2114 return e

2115 -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them

2116 handle e@(At fc err) = do logLvl 3 "Reflecting body of At"

2117 err' <- handle err

2118 return (At fc err')

2119 handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"

2120 err' <- handle err

2121 return (Elaborating what n err')

2122 handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"

2123 hs <- getFnHandlers f a

2124 err' <- if null hs

2125 then handle err

2126 else applyHandlers err hs

2127 return (ElaboratingArg f a prev err')

2128 -- ProofSearchFail is an internal detail - so don't expose it

2129 handle (ProofSearchFail e) = handle e

2130 -- TODO: argument-specific error handlers go here for ElaboratingArg

2131 handle e = do ist <- getIState

2132 logLvl 2 "Starting error reflection"

2133 let handlers = idris_errorhandlers ist

2134 applyHandlers e handlers

2135 getFnHandlers :: Name -> Name -> Idris [Name]

2136 getFnHandlers f arg = do ist <- getIState

2137 let funHandlers = maybe M.empty id .

2138 lookupCtxtExact f .

2139 idris_function_errorhandlers $ ist

2140 return . maybe [] S.toList . M.lookup arg $ funHandlers

2141

2142

2143 applyHandlers e handlers =

2144 do ist <- getIState

2145 let err = fmap (errReverse ist) e

2146 logLvl 3 $ "Using reflection handlers " ++

2147 concat (intersperse ", " (map show handlers))

2148 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers

2149

2150 -- Typecheck error handlers - if this fails, then something else was wrong earlier!

2151 handlers <- case mapM (check (tt_ctxt ist) []) reports of

2152 Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e

2153 OK hs -> return hs

2154

2155 -- Normalize error handler terms to produce the new messages

2156 ctxt <- getContext

2157 let results = map (normalise ctxt []) (map fst handlers)

2158 logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

2159

2160 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

2161 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

2162 errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

2163 Left err -> ierror err

2164 Right ok -> return ok

2165 return $ case errorparts of

2166 [] -> e

2167 parts -> ReflectionError errorparts e

2168

2169fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

2170fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

2171 | just == txt "Just" = Just tm

2172fromTTMaybe x = Nothing

2173

2174reflErrName :: String -> Name

2175reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

2176

2177-- | Attempt to reify a report part from TT to the internal

2178-- representation. Not in Idris or ElabD monads because it should be usable

2179-- from either.

2180reifyReportPart :: Term -> Either Err ErrorReportPart

2181reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

2182 Right (TextPart msg)

2183reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2184 | n == reflm "NamePart" =

2185 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2186 Error e -> Left . InternalMsg $

2187 "could not reify name term " ++

2188 show ttn ++

2189 " when reflecting an error:" ++ show e

2190 OK (n', _)-> Right $ NamePart n'

2191reifyReportPart (App (P (DCon _ _ _) n _) tm)

2192 | n == reflm "TermPart" =

2193 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

2194 Error e -> Left . InternalMsg $

2195 "could not reify reflected term " ++

2196 show tm ++

2197 " when reflecting an error:" ++ show e

2198 OK (tm', _) -> Right $ TermPart tm'

2199reifyReportPart (App (P (DCon _ _ _) n _) tm)

2200 | n == reflm "SubReport" =

2201 case unList tm of

2202 Just xs -> do subParts <- mapM reifyReportPart xs

2203 Right (SubReport subParts)

2204 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2205reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2206

2207envTupleType :: Raw

2208envTupleType

2209 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

2210 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

2211 ]

2212

2213solveAll = try (do solve; solveAll) (return ())