@@ -637,22 +637,25 @@ elab ist info pattern opts fn tm
637 elab' ina t
637 elab' ina t
638 unifyLog False
638 unifyLog False
639 elab' (ina, g, inty, qq) (PQuasiquote t)
639 elab' (ina, g, inty, qq) (PQuasiquote t)
640− = do -- First elaborate the unquoted subterms, replacing them with
640+ = do -- First extract the unquoted subterms, replacing them with fresh
641− -- fresh names in the quasiquoted term
641+ -- names in the quasiquoted term. Claim their reflections to be
642 (t, unq) <- extractUnquotes t
643 (t, unq) <- extractUnquotes t
643 let unquoteNames = map fst unq
644 let unquoteNames = map fst unq
644 mapM_ (flip claim (Var tt)) unquoteNames
645 mapM_ (flip claim (Var tt)) unquoteNames
647− -- Save the old state - we need a fresh proof state for this to
648+ -- Save the old state - we need a fresh proof state to avoid
648− -- avoid capture
649+ -- capturing lexically available variables in the quoted term.
649 ctxt <- get_context
650 ctxt <- get_context
650 saveState
651 saveState
651 updatePS (const .
652 updatePS (const .
652 newProof (sMN 0 "q") ctxt $
653 newProof (sMN 0 "q") ctxt $
653 P Ref tt Erased)
654 P Ref tt Erased)
655− -- Re-add the unquotes, letting Idris infer the (fictional) types
656+ -- Re-add the unquotes, letting Idris infer the (fictional)
657+ -- types. Here, they represent the real type rather than the type
658+ -- of their reflection.
656 mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
659 mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
657 claim ty RType
660 claim ty RType
658 movelast ty
661 movelast ty
@@ -670,16 +673,17 @@ elab ist info pattern opts fn tm
670 -- the hole doesn't disappear
673 -- the hole doesn't disappear
671 nTm <- getNameFrom (sMN 0 "quotedTerm")
674 nTm <- getNameFrom (sMN 0 "quotedTerm")
672 letbind nTm (Var qTy) (Var qTm)
675 letbind nTm (Var qTy) (Var qTm)
674 -- We must solve the type later through unification
676 -- We must solve the type later through unification
675 movelast qTy
677 movelast qTy
676 -- Elaborate the quasiquoted term into the hole
680 -- Elaborate the quasiquoted term into the hole
677 focus qTm
681 focus qTm
678 elabE (ina, g, inty, True) t
682 elabE (ina, g, inty, True) t
679 end_unify
683 end_unify
681 -- We now have an elaborated term. Reflect it and solve the
685 -- We now have an elaborated term. Reflect it and solve the
682− -- original goal
686+ -- original goal in the original proof state.
683 env <- get_env
687 env <- get_env
684 loadState
688 loadState
685 case fmap (explicitNames . binderVal) $ lookup nTm env of
689 case fmap (explicitNames . binderVal) $ lookup nTm env of
@@ -688,6 +692,10 @@ elab ist info pattern opts fn tm
688 | otherwise -> do fill $ reflectQuote unquoteNames q
692 | otherwise -> do fill $ reflectQuote unquoteNames q
690 Nothing -> fail "Broken elaboration of quasiquote"
694 Nothing -> fail "Broken elaboration of quasiquote"
696+ -- Finally fill in the terms or patterns from the unquotes. This
697+ -- happens last so that their holes still exist while elaborating
698+ -- the main quotation.
691 mapM_ elabUnquote unq
699 mapM_ elabUnquote unq
692 where tt = sNS (sUN "TT") ["Reflection", "Language"]
700 where tt = sNS (sUN "TT") ["Reflection", "Language"]