84019b6 · Idris-dev · git.iko.soy

999 = do -- First extract the unquoted subterms, replacing them with fresh

1000 -- names in the quasiquoted term. Claim their reflections to be

1001 -- an inferred type (to support polytypic quasiquotes).

1002− qty <- goal

1002+ finalTy <- goal

1003 (t, unq) <- extractUnquotes 0 t

1004 let unquoteNames = map fst unq

1005− mapM_ (\uqn -> claim uqn (forget qty)) unquoteNames

1005+ mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames

1006

1007 -- Save the old state - we need a fresh proof state to avoid

1008 -- capturing lexically available variables in the quoted term.

1052 env <- get_env

1053 loadState

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

1055−

1055+ isRaw = case unApply (normaliseAll ctxt env finalTy) of

1056+ (P _ n _, []) | n == reflm "Raw" -> True

1057+ _ -> False

1056 case quoted of

1058 case quoted of

1057 Just q -> do ctxt <- get_context

1059 Just q -> do ctxt <- get_context

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

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

1059 if pattern

1061 if pattern

1062+ then if isRaw

1063+ then reflectRawQuotePattern unquoteNames (forget q')

1060− then do try' (reflectTTQuotePattern unquoteNames q')

1064+ else reflectTTQuotePattern unquoteNames q'

1061− (reflectRawQuotePattern unquoteNames (forget q'))

1065+ else do if isRaw

1062− True

1063− else do try' (fill $ reflectTTQuote unquoteNames q')

1064− -- we forget q' instead of using q to ensure rechecking

1066+ then -- we forget q' instead of using q to ensure rechecking

1065− (fill $ reflectRawQuote unquoteNames (forget q'))

1067+ fill $ reflectRawQuote unquoteNames (forget q')

1066− True -- ignore errors like proof search does

1068+ else fill $ reflectTTQuote unquoteNames q'

1067 solve

1069 solve

1068

1070

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

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

2463reflectTTQuote unq (V n)

2465reflectTTQuote unq (V n)

2464 = reflCall "V" [RConstant (I n)]

2466 = reflCall "V" [RConstant (I n)]

2465reflectTTQuote unq (Bind n b x)

2467reflectTTQuote unq (Bind n b x)

2466− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]

2468+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

2467reflectTTQuote unq (App f x)

2469reflectTTQuote unq (App f x)

2468 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2470 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2469reflectTTQuote unq (Constant c)

2471reflectTTQuote unq (Constant c)

2480 | n `elem` unq = Var n

2482 | n `elem` unq = Var n

2481 | otherwise = reflCall "Var" [reflectName n]

2483 | otherwise = reflCall "Var" [reflectName n]

2482reflectRawQuote unq (RBind n b r) =

2484reflectRawQuote unq (RBind n b r) =

2483− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]

2485+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]

2484reflectRawQuote unq (RApp f x) =

2486reflectRawQuote unq (RApp f x) =

2485 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2487 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2486reflectRawQuote unq RType = Var (reflm "RType")

2488reflectRawQuote unq RType = Var (reflm "RType")

2538 solve

2540 solve

2539

2541

2540reflectBinder :: Binder Term -> Raw

2542reflectBinder :: Binder Term -> Raw

2541−reflectBinder = reflectBinderQuote reflectTTQuote []

2543+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2542−

2544+

2543−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw

2545+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2544−reflectBinderQuote q unq (Lam t)

2546+reflectBinderQuote q ty unq (Lam t)

2545− = reflCall "Lam" [Var (reflm "TT"), q unq t]

2547+ = reflCall "Lam" [Var ty, q unq t]

2546−reflectBinderQuote q unq (Pi _ t k)

2548+reflectBinderQuote q ty unq (Pi _ t k)

2547− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]

2549+ = reflCall "Pi" [Var ty, q unq t, q unq k]

2548−reflectBinderQuote q unq (Let x y)

2550+reflectBinderQuote q ty unq (Let x y)

2549− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]

2551+ = reflCall "Let" [Var ty, q unq x, q unq y]

2550−reflectBinderQuote q unq (NLet x y)

2552+reflectBinderQuote q ty unq (NLet x y)

2551− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]

2553+ = reflCall "NLet" [Var ty, q unq x, q unq y]

2552−reflectBinderQuote q unq (Hole t)

2554+reflectBinderQuote q ty unq (Hole t)

2553− = reflCall "Hole" [Var (reflm "TT"), q unq t]

2555+ = reflCall "Hole" [Var ty, q unq t]

2554−reflectBinderQuote q unq (GHole _ t)

2556+reflectBinderQuote q ty unq (GHole _ t)

2555− = reflCall "GHole" [Var (reflm "TT"), q unq t]

2557+ = reflCall "GHole" [Var ty, q unq t]

2556−reflectBinderQuote q unq (Guess x y)

2558+reflectBinderQuote q ty unq (Guess x y)

2557− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]

2559+ = reflCall "Guess" [Var ty, q unq x, q unq y]

2558−reflectBinderQuote q unq (PVar t)

2560+reflectBinderQuote q ty unq (PVar t)

2559− = reflCall "PVar" [Var (reflm "TT"), q unq t]

2561+ = reflCall "PVar" [Var ty, q unq t]

2560−reflectBinderQuote q unq (PVTy t)

2562+reflectBinderQuote q ty unq (PVTy t)

2561− = reflCall "PVTy" [Var (reflm "TT"), q unq t]

2563+ = reflCall "PVTy" [Var ty, q unq t]

2562

2564

2563mkList :: Raw -> [Raw] -> Raw

2565mkList :: Raw -> [Raw] -> Raw

2564mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

2566mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty