@@ -154,8 +154,12 @@ elab ist info pattern opts fn tm
154 (h: hs) -> do patvar h; mkPat
154 (h: hs) -> do patvar h; mkPat
155 [] -> return ()
155 [] -> return ()
157+ -- | elabE elaborates an expression, possibly wrapping implicit coercions
158+ -- and forces/delays. If you make a recursive call in elab', it is
159+ -- normally correct to call elabE - the ones that don't are desugarings
157 elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
161 elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
158− elabE ina t =
162+ elabE ina t =
159 --do g <- goal
163 --do g <- goal
160 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
164 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
161 do ct <- insertCoerce ina t
165 do ct <- insertCoerce ina t
@@ -204,6 +208,8 @@ elab ist info pattern opts fn tm
204 constType VoidType = True
208 constType VoidType = True
205 constType _ = False
209 constType _ = False
211+ -- "guarded" means immediately under a constructor, to help find patvars
207 elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
213 elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
208 -> PTerm -- ^ The term to elaborate
214 -> PTerm -- ^ The term to elaborate
209 -> ElabD ()
215 -> ElabD ()
@@ -634,7 +640,7 @@ elab ist info pattern opts fn tm
634 = do -- First elaborate the unquoted subterms, replacing them with
640 = do -- First elaborate the unquoted subterms, replacing them with
635 -- fresh names in the quasiquoted term
641 -- fresh names in the quasiquoted term
636 (t, unq) <- extractUnquotes t
642 (t, unq) <- extractUnquotes t
637− mapM_ elabUnquote unq
643+ mapM_ (flip claim (Var tt) . fst) unq
638 let unquoteNames = map fst unq
644 let unquoteNames = map fst unq
640 -- Save the old state - we need a fresh proof state for this to
646 -- Save the old state - we need a fresh proof state for this to
@@ -643,10 +649,15 @@ elab ist info pattern opts fn tm
643 saveState
649 saveState
644 updatePS (const .
650 updatePS (const .
645 newProof (sMN 0 "q") ctxt $
651 newProof (sMN 0 "q") ctxt $
646− P Ref (sNS (sUN "TT") ["Reflection", "Language"]) Erased)
652+ P Ref tt Erased)
648− -- Re-add the unquotes
654+ -- Re-add the unquotes, letting Idris infer the types
649− mapM_ (flip claim (Var (sNS (sUN "TT") ["Reflection", "Language"]))) unquoteNames
655+ mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
651 -- Establish holes for the type and value of the term to be
662 -- Establish holes for the type and value of the term to be
652 -- quasiquoted
663 -- quasiquoted
@@ -658,27 +669,31 @@ elab ist info pattern opts fn tm
658 -- the hole doesn't disappear
669 -- the hole doesn't disappear
659 nTm <- getNameFrom (sMN 0 "quotedTerm")
670 nTm <- getNameFrom (sMN 0 "quotedTerm")
660 letbind nTm (Var qTy) (Var qTm)
671 letbind nTm (Var qTy) (Var qTm)
661 -- We must solve the type later through unification
673 -- We must solve the type later through unification
662 movelast qTy
674 movelast qTy
663− -- Elaborate the quasiquoted term into the hole that was
675+ -- Elaborate the quasiquoted term into the hole
664 focus qTm
676 focus qTm
665− elab' ina t
677+ elabE ina t
666 -- We now have an elaborated term. Reflect it and solve the
679 -- We now have an elaborated term. Reflect it and solve the
667 -- original goal
680 -- original goal
668 env <- get_env
681 env <- get_env
669 let qTerm = fmap (reflectQuote unquoteNames . binderVal) $ lookup nTm env
682 let qTerm = fmap (reflectQuote unquoteNames . binderVal) $ lookup nTm env
670 case qTerm of
684 case qTerm of
671 Just q -> do loadState
685 Just q -> do loadState
688+ mapM_ elabUnquote unq
674 Nothing -> fail "Broken elaboration of quasiquote"
689 Nothing -> fail "Broken elaboration of quasiquote"
675− where elabUnquote (n, tm)
676− = do qn <- getNameFrom (sMN 0 "unquotHole")
677− let tt = sNS (sUN "TT") ["Reflection", "Language"]
690+ where tt = sNS (sUN "TT") ["Reflection", "Language"]
678− claim qn (Var tt)
691+
679− letbind n (Var tt) (Var qn)
692+ elabUnquote (n, tm)
680− focus qn
693+ = do focus n
681− elab' ina tm
694+ elabE ina tm
682 elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
697 elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
683 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
698 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x