@@ -133,7 +133,7 @@ elab ist info pattern opts fn tm
135 tcgen = Dictionary `elem` opts
135 tcgen = Dictionary `elem` opts
136− reflect = Reflection `elem` opts
136+ reflection = Reflection `elem` opts
138 isph arg = case getTm arg of
138 isph arg = case getTm arg of
139 Placeholder -> (True, priority arg)
139 Placeholder -> (True, priority arg)
@@ -209,7 +209,7 @@ elab ist info pattern opts fn tm
209 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
209 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
210 elab' ina PType = do apply RType []; solve
210 elab' ina PType = do apply RType []; solve
211-- elab' (_,_,inty) (PConstant c)
211-- elab' (_,_,inty) (PConstant c)
212−-- | constType c && pattern && not reflect && not inty
212+-- | constType c && pattern && not reflection && not inty
213-- = lift $ tfail (Msg "Typecase is not allowed")
213-- = lift $ tfail (Msg "Typecase is not allowed")
214 elab' ina (PConstant c) = do apply (RConstant c) []; solve
214 elab' ina (PConstant c) = do apply (RConstant c) []; solve
215 elab' ina (PQuote r) = do fill r; solve
215 elab' ina (PQuote r) = do fill r; solve
@@ -285,7 +285,7 @@ elab ist info pattern opts fn tm
285 = try' (elab' ina x) (trySeq' deferr xs) True
285 = try' (elab' ina x) (trySeq' deferr xs) True
286 elab' ina (PPatvar fc n) | pattern = patvar n
286 elab' ina (PPatvar fc n) | pattern = patvar n
287-- elab' (_, _, inty) (PRef fc f)
287-- elab' (_, _, inty) (PRef fc f)
288−-- | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
288+-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
289-- = lift $ tfail (Msg "Typecase is not allowed")
289-- = lift $ tfail (Msg "Typecase is not allowed")
290 elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
290 elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
291 = do ctxt <- get_context
291 = do ctxt <- get_context
@@ -434,7 +434,7 @@ elab ist info pattern opts fn tm
434 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
434 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
436 elab' (_, _, inty) (PApp fc (PRef _ f) args')
436 elab' (_, _, inty) (PApp fc (PRef _ f) args')
437− | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
437+ | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
438 = lift $ tfail (Msg "Typecase is not allowed")
438 = lift $ tfail (Msg "Typecase is not allowed")
439 -- if f is local, just do a simple_app
439 -- if f is local, just do a simple_app
440 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)
440 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)
@@ -629,6 +629,28 @@ elab ist info pattern opts fn tm
629 elab' ina (PUnifyLog t) = do unifyLog True
629 elab' ina (PUnifyLog t) = do unifyLog True
630 elab' ina t
630 elab' ina t
631 unifyLog False
631 unifyLog False
632+ elab' ina (PQuasiquote t)
633+ = do -- Establish holes for the type and value of the term to be quasiquoted
634+ qTy <- getNameFrom (sMN 0 "qquoteTy")
636+ qTm <- getNameFrom (sMN 0 "qquoteTm")
638+ -- Let-bind the result of elaborating the contained term, so that
639+ -- the hole doesn't disappear
640+ nTm <- getNameFrom (sMN 0 "quotedTerm")
641+ letbind nTm (Var qTy) (Var qTm)
642+ -- We must solve the type later through unification
644+ -- Elaborate the quasiquoted term into the hole that was
647+ -- We now have an elaborated term. Reflect it and solve the original goal
650+ let qTerm = normalise ctxt env (P Bound nTm Erased)
651+ fill $ reflect qTerm
653+ elab' ina (PUnquote t) = fail "Elaboration of unquotes not yet implemented"
632 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
654 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
634 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
656 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))