@@ -387,10 +387,10 @@ reflect = reflectTTQuote []
387387reflectRaw :: Raw -> Raw
388388reflectRaw = reflectRawQuote []
389389
390−claimTT :: Name -> ElabD Name
391−claimTT n = do n' <- getNameFrom n
392− claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
393− return n'
390+claimTy :: Name -> Raw -> ElabD Name
391+claimTy n ty = do n' <- getNameFrom n
392+ claim n' ty
393+ return n'
394394
395395-- | Convert a reflected term to a more suitable form for pattern-matching.
396396-- In particular, the less-interesting bits are elaborated to _ patterns. This
@@ -401,7 +401,7 @@ reflectTTQuotePattern unq (P _ n _)
401401 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
402402 do fill (Var n) ; solve
403403 | otherwise =
404− do tyannot <- claimTT (sMN 0 "pTyAnnot")
404+ do tyannot <- claimTy (sMN 0 "pTyAnnot") (Var (reflm "TT"))
405405 movelast tyannot -- use a _ pattern here
406406 nt <- getNameFrom (sMN 0 "nt")
407407 claim nt (Var (reflm "NameType"))
@@ -415,7 +415,7 @@ reflectTTQuotePattern unq (V n)
415415 = do fill $ reflCall "V" [RConstant (I n)]
416416 solve
417417reflectTTQuotePattern unq (Bind n b x)
418− = do x' <- claimTT (sMN 0 "sc")
418+ = do x' <- claimTy (sMN 0 "sc") (Var (reflm "TT"))
419419 movelast x'
420420 b' <- getNameFrom (sMN 0 "binder")
421421 claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
@@ -435,10 +435,10 @@ reflectTTQuotePattern unq (Bind n b x)
435435 Var x']
436436 solve
437437 focus x'; reflectTTQuotePattern unq x
438− focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
438+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern (Var $ reflm "TT") unq b
439439reflectTTQuotePattern unq (App _ f x)
440− = do f' <- claimTT (sMN 0 "f"); movelast f'
441− x' <- claimTT (sMN 0 "x"); movelast x'
440+ = do f' <- claimTy (sMN 0 "f") (Var (reflm "TT")) ; movelast f'
441+ x' <- claimTy (sMN 0 "x") (Var (reflm "TT")) ; movelast x'
442442 fill $ reflCall "App" [Var f', Var x']
443443 solve
444444 focus f'; reflectTTQuotePattern unq f
@@ -447,12 +447,12 @@ reflectTTQuotePattern unq (Constant c)
447447 = do fill $ reflCall "TConst" [reflectConstant c]
448448 solve
449449reflectTTQuotePattern 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'
451451 fill $ reflCall "Proj" [Var t', RConstant (I i)]
452452 solve
453453 focus t'; reflectTTQuotePattern unq t
454454reflectTTQuotePattern unq (Erased)
455− = do erased <- claimTT (sMN 0 "erased")
455+ = do erased <- claimTy (sMN 0 "erased") (Var (reflm "TT"))
456456 movelast erased
457457 fill $ (Var erased)
458458 solve
@@ -501,7 +501,7 @@ reflectRawQuotePattern unq (RBind n b sc) =
501501 fill $ reflCall "RBind" [Var any, Var bH, Var scH]
502502 solve
503503 focus scH; reflectRawQuotePattern unq sc
504− focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
504+ focus bH; reflectBinderQuotePattern reflectRawQuotePattern (Var $ reflm "Raw") unq b
505505 where freeNamesR (Var n) = [n]
506506 freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
507507 freeNamesR body \\ [n],
@@ -549,57 +549,57 @@ reflectRawQuotePattern unq (RConstant c) =
549549 focus cH
550550 fill (reflectConstant c); solve
551551
552−reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
553−reflectBinderQuotePattern q unq (Lam t)
554− = do t' <- claimTT (sMN 0 "ty"); movelast t'
555− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
552+reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
553+reflectBinderQuotePattern q ty unq (Lam t)
554+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
555+ fill $ reflCall "Lam" [ty, Var t']
556556 solve
557557 focus t'; q unq t
558−reflectBinderQuotePattern q unq (Pi _ t k)
559− = do t' <- claimTT (sMN 0 "ty") ; movelast t'
560− k' <- claimTT (sMN 0 "k"); movelast k';
561− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
558+reflectBinderQuotePattern q ty unq (Pi _ t k)
559+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
560+ k' <- claimTy (sMN 0 "k") ty; movelast k';
561+ fill $ reflCall "Pi" [ty, Var t', Var k']
562562 solve
563563 focus t'; q unq t
564−reflectBinderQuotePattern q unq (Let x y)
565− = do x' <- claimTT (sMN 0 "ty"); movelast x';
566− y' <- claimTT (sMN 0 "v"); movelast y';
567− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
564+reflectBinderQuotePattern q ty unq (Let x y)
565+ = do x' <- claimTy (sMN 0 "ty") ty; movelast x';
566+ y' <- claimTy (sMN 0 "v")ty; movelast y';
567+ fill $ reflCall "Let" [ty, Var x', Var y']
568568 solve
569569 focus x'; q unq x
570570 focus y'; q unq y
571−reflectBinderQuotePattern q unq (NLet x y)
572− = do x' <- claimTT (sMN 0 "ty"); movelast x'
573− y' <- claimTT (sMN 0 "v"); movelast y'
574− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
571+reflectBinderQuotePattern q ty unq (NLet x y)
572+ = do x' <- claimTy (sMN 0 "ty") ty; movelast x'
573+ y' <- claimTy (sMN 0 "v") ty; movelast y'
574+ fill $ reflCall "NLet" [ty, Var x', Var y']
575575 solve
576576 focus x'; q unq x
577577 focus y'; q unq y
578−reflectBinderQuotePattern q unq (Hole t)
579− = do t' <- claimTT (sMN 0 "ty"); movelast t'
580− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
578+reflectBinderQuotePattern q ty unq (Hole t)
579+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
580+ fill $ reflCall "Hole" [ty, Var t']
581581 solve
582582 focus t'; q unq t
583−reflectBinderQuotePattern q unq (GHole _ t)
584− = do t' <- claimTT (sMN 0 "ty"); movelast t'
585− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
583+reflectBinderQuotePattern q ty unq (GHole _ t)
584+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
585+ fill $ reflCall "GHole" [ty, Var t']
586586 solve
587587 focus t'; q unq t
588−reflectBinderQuotePattern q unq (Guess x y)
589− = do x' <- claimTT (sMN 0 "ty"); movelast x'
590− y' <- claimTT (sMN 0 "v"); movelast y'
591− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
588+reflectBinderQuotePattern q ty unq (Guess x y)
589+ = do x' <- claimTy (sMN 0 "ty") ty; movelast x'
590+ y' <- claimTy (sMN 0 "v") ty; movelast y'
591+ fill $ reflCall "Guess" [ty, Var x', Var y']
592592 solve
593593 focus x'; q unq x
594594 focus y'; q unq y
595−reflectBinderQuotePattern q unq (PVar t)
596− = do t' <- claimTT (sMN 0 "ty"); movelast t'
597− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
595+reflectBinderQuotePattern q ty unq (PVar t)
596+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
597+ fill $ reflCall "PVar" [ty, Var t']
598598 solve
599599 focus t'; q unq t
600−reflectBinderQuotePattern q unq (PVTy t)
601− = do t' <- claimTT (sMN 0 "ty"); movelast t'
602− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
600+reflectBinderQuotePattern q ty unq (PVTy t)
601+ = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
602+ fill $ reflCall "PVTy" [ty, Var t']
603603 solve
604604 focus t'; q unq t
605605