@@ -124,7 +124,7 @@ elab ist info pattern opts fn tm
124124 = do let loglvl = opt_logLevel (idris_options ist)
125125 when (loglvl > 5) $ unifyLog True
126126 compute -- expand type synonyms, etc
127− elabE (False, False, False) tm -- (in argument, guarded, in type)
127+ elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)
128128 end_unify
129129 when pattern -- convert remaining holes to pattern vars
130130 (do update_term orderPats
@@ -158,7 +158,7 @@ elab ist info pattern opts fn tm
158158 -- and forces/delays. If you make a recursive call in elab', it is
159159 -- normally correct to call elabE - the ones that don't are desugarings
160160 -- typically
161− elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
161+ elabE :: (Bool, Bool, Bool, Bool) -> PTerm -> ElabD ()
162162 elabE ina t =
163163 --do g <- goal
164164 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
@@ -210,7 +210,7 @@ elab ist info pattern opts fn tm
210210
211211 -- "guarded" means immediately under a constructor, to help find patvars
212212
213− elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
213+ elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)
214214 -> PTerm -- ^ The term to elaborate
215215 -> ElabD ()
216216 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
@@ -239,16 +239,16 @@ elab ist info pattern opts fn tm
239239 [pimp (sMN 0 "A") Placeholder True,
240240 pimp (sMN 0 "B") Placeholder False,
241241 pexp l, pexp r])
242− elab' ina@(_, a, inty) (PPair fc _ l r)
242+ elab' ina@(_, a, inty, qq) (PPair fc _ l r)
243243 = do hnf_compute
244244 g <- goal
245245 case g of
246− TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
247− [pexp l,pexp r])
248− _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
249− [pimp (sMN 0 "A") Placeholder True,
250− pimp (sMN 0 "B") Placeholder True,
251− pexp l, pexp r])
246+ TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
247+ [pexp l,pexp r])
248+ _ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
249+ [pimp (sMN 0 "A") Placeholder True,
250+ pimp (sMN 0 "B") Placeholder True,
251+ pexp l, pexp r])
252252 elab' ina (PDPair fc p l@(PRef _ n) t r)
253253 = case t of
254254 Placeholder ->
@@ -294,7 +294,7 @@ elab ist info pattern opts fn tm
294294-- elab' (_, _, inty) (PRef fc f)
295295-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
296296-- = lift $ tfail (Msg "Typecase is not allowed")
297− elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
297+ elab' (ina, guarded, inty, qq) (PRef fc n) | pattern && not (inparamBlock n)
298298 = do ctxt <- get_context
299299 let defined = case lookupTy n ctxt of
300300 [] -> False
@@ -311,7 +311,7 @@ elab ist info pattern opts fn tm
311311 _ -> True
312312 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
313313 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
314− elab' ina@(_, a, inty) (PLam n Placeholder sc)
314+ elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)
315315 = do -- if n is a type constructor name, this makes no sense...
316316 ctxt <- get_context
317317 when (isTConName n ctxt) $
@@ -319,8 +319,8 @@ elab ist info pattern opts fn tm
319319 checkPiGoal n
320320 attack; intro (Just n);
321321 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
322− elabE (True, a, inty) sc; solve
323− elab' ina@(_, a, inty) (PLam n ty sc)
322+ elabE (True, a, inty, qq) sc; solve
323+ elab' ina@(_, a, inty, qq) (PLam n ty sc)
324324 = do tyn <- getNameFrom (sMN 0 "lamty")
325325 -- if n is a type constructor name, this makes no sense...
326326 ctxt <- get_context
@@ -334,12 +334,12 @@ elab ist info pattern opts fn tm
334334 hs <- get_holes
335335 introTy (Var tyn) (Just n)
336336 focus tyn
337− elabE (True, a, True) ty
338− elabE (True, a, inty) sc
337+ elabE (True, a, True, qq) ty
338+ elabE (True, a, inty, qq) sc
339339 solve
340− elab' ina@(_, a, _) (PPi _ n Placeholder sc)
341− = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve
342− elab' ina@(_, a, _) (PPi _ n ty sc)
340+ elab' ina@(_, a, _, qq) (PPi _ n Placeholder sc)
341+ = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) sc; solve
342+ elab' ina@(_, a, _, qq) (PPi _ n ty sc)
343343 = do attack; tyn <- getNameFrom (sMN 0 "ty")
344344 claim tyn RType
345345 n' <- case n of
@@ -347,10 +347,10 @@ elab ist info pattern opts fn tm
347347 _ -> return n
348348 forall n' (Var tyn)
349349 focus tyn
350− elabE (True, a, True) ty
351− elabE (True, a, True) sc
350+ elabE (True, a, True, qq) ty
351+ elabE (True, a, True, qq) sc
352352 solve
353− elab' ina@(_, a, inty) (PLet n ty val sc)
353+ elab' ina@(_, a, inty, qq) (PLet n ty val sc)
354354 = do attack;
355355 tyn <- getNameFrom (sMN 0 "letty")
356356 claim tyn RType
@@ -362,17 +362,17 @@ elab ist info pattern opts fn tm
362362 Placeholder -> return ()
363363 _ -> do focus tyn
364364 explicit tyn
365− elabE (True, a, True) ty
365+ elabE (True, a, True, qq) ty
366366 focus valn
367− elabE (True, a, True) val
367+ elabE (True, a, True, qq) val
368368 env <- get_env
369− elabE (True, a, inty) sc
369+ elabE (True, a, inty, qq) sc
370370 -- HACK: If the name leaks into its type, it may leak out of
371371 -- scope outside, so substitute in the outer scope.
372372 expandLet n (case lookup n env of
373373 Just (Let t v) -> v)
374374 solve
375− elab' ina@(_, a, inty) (PGoal fc r n sc) = do
375+ elab' ina@(_, a, inty, qq) (PGoal fc r n sc) = do
376376 rty <- goal
377377 attack
378378 tyn <- getNameFrom (sMN 0 "letty")
@@ -381,10 +381,10 @@ elab ist info pattern opts fn tm
381381 claim valn (Var tyn)
382382 letbind n (Var tyn) (Var valn)
383383 focus valn
384− elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])
384+ elabE (True, a, True, qq) (PApp fc r [pexp (delab ist rty)])
385385 env <- get_env
386386 computeLet n
387− elabE (True, a, inty) sc
387+ elabE (True, a, inty, qq) sc
388388 solve
389389-- elab' ina (PLet n Placeholder
390390-- (PApp fc r [pexp (delab ist rty)]) sc)
@@ -440,16 +440,16 @@ elab ist info pattern opts fn tm
440440 _ -> lift $ tfail (NoSuchVariable fn)
441441 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
442442 solve
443− elab' (_, _, inty) (PApp fc (PRef _ f) args')
444− | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
443+ elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')
444+ | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq
445445 = lift $ tfail (Msg "Typecase is not allowed")
446446 -- if f is local, just do a simple_app
447− elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)
447+ elab' (ina, g, inty, qq) tm@(PApp fc (PRef _ f) args)
448448 = do env <- get_env
449449 if (f `elem` map fst env && length args == 1)
450450 then -- simple app, as below
451− do simple_app (elabE (ina, g, inty) (PRef fc f))
452− (elabE (True, g, inty) (getTm (head args)))
451+ do simple_app (elabE (ina, g, inty, qq) (PRef fc f))
452+ (elabE (True, g, inty, qq) (getTm (head args)))
453453 (show tm)
454454 solve
455455 else
@@ -475,7 +475,7 @@ elab ist info pattern opts fn tm
475475 -- Sort so that the implicit tactics and alternatives go last
476476 let (ns', eargs) = unzip $
477477 sortBy cmpArg (zip ns args)
478− elabArgs ist (ina || not isinf, guarded, inty)
478+ elabArgs ist (ina || not isinf, guarded, inty, qq)
479479 [] fc False f ns'
480480 (f == sUN "Force")
481481 (map (\x -> (False, getTm x)) eargs) -- TODO: remove this False arg
@@ -549,9 +549,9 @@ elab ist info pattern opts fn tm
549549 setInjective (PApp _ (PRef _ n) _) = setinj n
550550 setInjective _ = return ()
551551
552− elab' ina@(_, a, inty) tm@(PApp fc f [arg])
552+ elab' ina@(_, a, inty, qq) tm@(PApp fc f [arg])
553553 = erun fc $
554− do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg))
554+ do simple_app (elabE ina f) (elabE (True, a, inty, qq) (getTm arg))
555555 (show tm)
556556 solve
557557 elab' ina Placeholder = do (h : hs) <- get_holes
@@ -600,7 +600,7 @@ elab ist info pattern opts fn tm
600600 elab' ina sc
601601 elab' ina (PRef fc letn)
602602 solve
603− elab' ina@(_, a, inty) c@(PCase fc scr opts)
603+ elab' ina@(_, a, inty, qq) c@(PCase fc scr opts)
604604 = do attack
605605 tyn <- getNameFrom (sMN 0 "scty")
606606 claim tyn RType
@@ -609,7 +609,7 @@ elab ist info pattern opts fn tm
609609 claim valn (Var tyn)
610610 letbind scvn (Var tyn) (Var valn)
611611 focus valn
612− elabE (True, a, inty) scr
612+ elabE (True, a, inty, qq) scr
613613 args <- get_env
614614 cname <- unique_hole' True (mkCaseName fn)
615615 let cname' = mkN cname
@@ -636,7 +636,7 @@ elab ist info pattern opts fn tm
636636 elab' ina (PUnifyLog t) = do unifyLog True
637637 elab' ina t
638638 unifyLog False
639− elab' ina (PQuasiquote t)
639+ elab' (ina, g, inty, qq) (PQuasiquote t)
640640 = do -- First elaborate the unquoted subterms, replacing them with
641641 -- fresh names in the quasiquoted term
642642 (t, unq) <- extractUnquotes t
@@ -651,7 +651,7 @@ elab ist info pattern opts fn tm
651651 newProof (sMN 0 "q") ctxt $
652652 P Ref tt Erased)
653653
654− -- Re-add the unquotes, letting Idris infer the types
654+ -- Re-add the unquotes, letting Idris infer the (fictional) types
655655 mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
656656 claim ty RType
657657 movelast ty
@@ -674,7 +674,7 @@ elab ist info pattern opts fn tm
674674 movelast qTy
675675 -- Elaborate the quasiquoted term into the hole
676676 focus qTm
677− elabE ina t
677+ elabE (ina, g, inty, True) t
678678 end_unify
679679 -- We now have an elaborated term. Reflect it and solve the
680680 -- original goal
@@ -691,7 +691,7 @@ elab ist info pattern opts fn tm
691691
692692 elabUnquote (n, tm)
693693 = do focus n
694− elabE ina tm
694+ elabE (ina, g, inty, False) tm
695695
696696
697697 elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
@@ -786,7 +786,7 @@ elab ist info pattern opts fn tm
786786
787787 -- | Elaborate the arguments to a function
788788 elabArgs :: IState -- ^ The current Idris state
789− -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
789+ -> (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a qquote)
790790 -> [Bool]
791791 -> FC -- ^ Source location
792792 -> Bool