d5411e2 · Idris-dev · git.iko.soy

14import Idris.Core.TT

15import Idris.Core.Evaluate

16import Idris.Core.Unify

17−import Idris.Core.Typecheck (check)

17+import Idris.Core.Typecheck (check, recheck)

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20

729 -- original goal in the original proof state.

730 env <- get_env

731 loadState

732− case fmap (explicitNames . binderVal) $ lookup nTm env of

732+ let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

733− Just q

733+

734+ case quoted of

735+ Just q -> do ctxt <- get_context

736+ (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

737+ if pattern

734− | pattern -> reflectQuotePattern unquoteNames q

738+ then reflectQuotePattern unquoteNames q'

735− | otherwise -> do fill $ reflectQuote unquoteNames q

739+ else do fill $ reflectQuote unquoteNames q'

736− solve

740+ solve

737− Nothing -> fail "Broken elaboration of quasiquote"

741+ Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

738

742

739 -- Finally fill in the terms or patterns from the unquotes. This

743 -- Finally fill in the terms or patterns from the unquotes. This

740 -- happens last so that their holes still exist while elaborating

744 -- happens last so that their holes still exist while elaborating

746 = do focus n

750 = do focus n

747 elabE (ina, g, inty, False) tm

751 elabE (ina, g, inty, False) tm

748

752

753+ holesInTerm tm = do hs <- get_holes

754+ return $ intersect (freeNames tm) hs

755+ removeAll xs [] = []

756+ removeAll xs (y:ys) | y `elem` xs = removeAll xs ys

757+ | otherwise = y : removeAll xs ys

749

758

750 elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"

759 elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"

751 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

760 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x