012b898 · Idris-dev · git.iko.soy

387reflectRaw :: Raw -> Raw

388reflectRaw = reflectRawQuote []

389

390−claimTT :: Name -> ElabD Name

390+claimTy :: Name -> Raw -> ElabD Name

391−claimTT n = do n' <- getNameFrom n

391+claimTy n ty = do n' <- getNameFrom n

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

392+ claim n' ty

393− return n'

393+ return n'

394

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

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

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

402 do fill (Var n) ; solve

403 | otherwise =

404− do tyannot <- claimTT (sMN 0 "pTyAnnot")

404+ do tyannot <- claimTy (sMN 0 "pTyAnnot") (Var (reflm "TT"))

405 movelast tyannot -- use a _ pattern here

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

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

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

416 solve

417reflectTTQuotePattern unq (Bind n b x)

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

418+ = do x' <- claimTy (sMN 0 "sc") (Var (reflm "TT"))

419 movelast x'

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

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

435 Var x']

436 solve

437 focus x'; reflectTTQuotePattern unq x

438− focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

438+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern (Var $ reflm "TT") unq b

439reflectTTQuotePattern unq (App _ f x)

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

440+ = do f' <- claimTy (sMN 0 "f") (Var (reflm "TT")) ; movelast f'

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

441+ x' <- claimTy (sMN 0 "x") (Var (reflm "TT")) ; movelast x'

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

443 solve

444 focus f'; reflectTTQuotePattern unq f

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

448 solve

449reflectTTQuotePattern unq (Proj t i)

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

450+ = do t' <- claimTy (sMN 0 "t") (Var (reflm "TT")) ; movelast t'

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

452 solve

453 focus t'; reflectTTQuotePattern unq t

454reflectTTQuotePattern unq (Erased)

455− = do erased <- claimTT (sMN 0 "erased")

455+ = do erased <- claimTy (sMN 0 "erased") (Var (reflm "TT"))

456 movelast erased

457 fill $ (Var erased)

458 solve

501 fill $ reflCall "RBind" [Var any, Var bH, Var scH]

502 solve

503 focus scH; reflectRawQuotePattern unq sc

504− focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b

504+ focus bH; reflectBinderQuotePattern reflectRawQuotePattern (Var $ reflm "Raw") unq b

505 where freeNamesR (Var n) = [n]

506 freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,

507 freeNamesR body \\ [n],

549 focus cH

550 fill (reflectConstant c); solve

551

552−reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()

552+reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()

553−reflectBinderQuotePattern q unq (Lam t)

553+reflectBinderQuotePattern q ty unq (Lam t)

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

554+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

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

555+ fill $ reflCall "Lam" [ty, Var t']

556 solve

557 focus t'; q unq t

558−reflectBinderQuotePattern q unq (Pi _ t k)

558+reflectBinderQuotePattern q ty unq (Pi _ t k)

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

559+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

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

560+ k' <- claimTy (sMN 0 "k") ty; movelast k';

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

561+ fill $ reflCall "Pi" [ty, Var t', Var k']

562 solve

563 focus t'; q unq t

564−reflectBinderQuotePattern q unq (Let x y)

564+reflectBinderQuotePattern q ty unq (Let x y)

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

565+ = do x' <- claimTy (sMN 0 "ty") ty; movelast x';

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

566+ y' <- claimTy (sMN 0 "v")ty; movelast y';

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

567+ fill $ reflCall "Let" [ty, Var x', Var y']

568 solve

569 focus x'; q unq x

570 focus y'; q unq y

571−reflectBinderQuotePattern q unq (NLet x y)

571+reflectBinderQuotePattern q ty unq (NLet x y)

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

572+ = do x' <- claimTy (sMN 0 "ty") ty; movelast x'

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

573+ y' <- claimTy (sMN 0 "v") ty; movelast y'

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

574+ fill $ reflCall "NLet" [ty, Var x', Var y']

575 solve

576 focus x'; q unq x

577 focus y'; q unq y

578−reflectBinderQuotePattern q unq (Hole t)

578+reflectBinderQuotePattern q ty unq (Hole t)

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

579+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

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

580+ fill $ reflCall "Hole" [ty, Var t']

581 solve

582 focus t'; q unq t

583−reflectBinderQuotePattern q unq (GHole _ t)

583+reflectBinderQuotePattern q ty unq (GHole _ t)

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

584+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

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

585+ fill $ reflCall "GHole" [ty, Var t']

586 solve

587 focus t'; q unq t

588−reflectBinderQuotePattern q unq (Guess x y)

588+reflectBinderQuotePattern q ty unq (Guess x y)

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

589+ = do x' <- claimTy (sMN 0 "ty") ty; movelast x'

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

590+ y' <- claimTy (sMN 0 "v") ty; movelast y'

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

591+ fill $ reflCall "Guess" [ty, Var x', Var y']

592 solve

593 focus x'; q unq x

594 focus y'; q unq y

595−reflectBinderQuotePattern q unq (PVar t)

595+reflectBinderQuotePattern q ty unq (PVar t)

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

596+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

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

597+ fill $ reflCall "PVar" [ty, Var t']

598 solve

599 focus t'; q unq t

600−reflectBinderQuotePattern q unq (PVTy t)

600+reflectBinderQuotePattern q ty unq (PVTy t)

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

601+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

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

602+ fill $ reflCall "PVTy" [ty, Var t']

603 solve

604 focus t'; q unq t

605