@@ -1,5 +1,5 @@
1−{-# LANGUAGE PatternGuards #-}
2−
1+{-# LANGUAGE PatternGuards, ViewPatterns #-}
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
33module Idris.ElabTerm where
44
55import Idris.AbsSyntax
@@ -420,6 +420,7 @@ elab ist info emode opts fn tm
420420 where -- if none work, take the error from the first
421421 trySeq (x : xs) = let e1 = elab' ina fc x in
422422 try' e1 (trySeq' e1 xs) True
423+ trySeq [] = fail "Nothing to try in sequence"
423424 trySeq' deferr [] = proofFail deferr
424425 trySeq' deferr (x : xs)
425426 = try' (do elab' ina fc x
@@ -546,7 +547,8 @@ elab ist info emode opts fn tm
546547 -- HACK: If the name leaks into its type, it may leak out of
547548 -- scope outside, so substitute in the outer scope.
548549 expandLet n (case lookup n env of
549− Just (Let t v) -> v)
550+ Just (Let t v) -> v
551+ other -> error ("Value not a let binding: " ++ show other))
550552 solve
551553 elab' ina _ (PGoal fc r n sc) = do
552554 rty <- goal
@@ -955,13 +957,16 @@ elab ist info emode opts fn tm
955957 elab' ina fc (PUnifyLog t) = do unifyLog True
956958 elab' ina fc t
957959 unifyLog False
958− elab' ina fc (PQuasiquote t goal) -- TODO: goal type
960+ elab' ina fc (PQuasiquote t goal)
959961 = do -- First extract the unquoted subterms, replacing them with fresh
960962 -- names in the quasiquoted term. Claim their reflections to be
961− -- of type TT.
963+ -- an inferred type (to support polytypic quasiquotes).
962964 (t, unq) <- extractUnquotes 0 t
963965 let unquoteNames = map fst unq
964− mapM_ (flip claim (Var tt)) unquoteNames
966+ mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")
967+ claim uqh RType
968+ movelast uqh
969+ claim uqn (Var uqh)) unquoteNames
965970
966971
967972 -- Save the old state - we need a fresh proof state to avoid
@@ -1017,9 +1022,14 @@ elab ist info emode opts fn tm
10171022 Just q -> do ctxt <- get_context
10181023 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
10191024 if pattern
1020− then reflectQuotePattern unquoteNames q'
1021− else do fill $ reflectQuote unquoteNames q'
1025+ then reflectTTQuotePattern unquoteNames q'
1026+ -- TODO: support quasiquote patterns of Raw terms
1027+ else do try' (fill $ reflectTTQuote unquoteNames q')
1028+ -- we forget q' instead of using q to ensure rechecking
1029+ (fill $ reflectRawQuote unquoteNames (forget q'))
1030+ True -- ignore errors like proof search does
10221031 solve
1032+
10231033 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
10241034
10251035 -- Finally fill in the terms or patterns from the unquotes. This
@@ -1049,6 +1059,20 @@ elab ist info emode opts fn tm
10491059 delayElab $ do focus h
10501060 dotterm
10511061 elab' ina fc t
1062+ elab' ina _ (PRunTactics fc tm) =
1063+ do attack
1064+ n <- getNameFrom (sMN 0 "tacticScript")
1065+ n' <- getNameFrom (sMN 0 "tacticExpr")
1066+ let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)
1067+ claim n scriptTy
1068+ movelast n
1069+ letbind n' scriptTy (Var n)
1070+ focus n
1071+ elab' ina (Just fc) tm
1072+ env <- get_env
1073+ ctxt <- get_context
1074+ runTactical fc ctxt env (P Bound n' Erased)
1075+ solve
10521076 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
10531077
10541078 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
@@ -1072,6 +1096,7 @@ elab ist info emode opts fn tm
10721096 findScr [(n, (_, t))] = [(n, (True, t))]
10731097 findScr (x : xs) = x : findScr xs
10741098 -- [] can't happen since scrutinee is in the environment!
1099+ findScr [] = error "The impossible happened - the scrutinee was not in the environment"
10751100
10761101 -- To make sure top level pattern name remains in scope, put
10771102 -- it at the end of the environment
@@ -1233,7 +1258,8 @@ elab ist info emode opts fn tm
12331258 lift (tfail (elaboratingArgErr while' e))
12341259 put newState
12351260 return result
1236−
1261+ elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
1262+ fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
12371263
12381264-- For every alternative, look at the function at the head. Automatically resolve
12391265-- any nested alternatives where that function is also at the head
@@ -1411,6 +1437,7 @@ resTC' tcs defaultOn depth topg fn ist
14111437 let imps = case lookupCtxtName n (idris_implicits ist) of
14121438 [] -> []
14131439 [args] -> map isImp (snd args) -- won't be overloaded!
1440+ xs -> error "The impossible happened - overloading is not expected here!"
14141441 ps <- get_probs
14151442 tm <- get_term
14161443 args <- map snd <$> try' (apply (Var n) imps)
@@ -1471,6 +1498,86 @@ case_ ind autoSolve ist fn tm = do
14711498 else casetac (forget val)
14721499 when autoSolve solveAll
14731500
1501+runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1502+runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1503+ where
1504+ eval = normaliseAll ctxt env
1505+ tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1506+ returnUnit = fmap fst $ get_type_val (Var unitCon)
1507+
1508+ -- | Do a step in the reflected elaborator monad. The input is the
1509+ -- step, the output is the (reflected) term returned.
1510+ runTacTm :: Term -> ElabD Term
1511+ runTacTm (unApply -> tac@(P _ n _, args))
1512+ | n == tacN "prim__Solve", [] <- args
1513+ = do solve
1514+ returnUnit
1515+ | n == tacN "prim__Goal", [] <- args
1516+ = do (h:_) <- get_holes
1517+ t <- goal
1518+ fmap fst . get_type_val $
1519+ rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1520+ (reflectName h, reflect t)
1521+ | n == tacN "prim__Holes", [] <- args
1522+ = do hs <- get_holes
1523+ fmap fst . get_type_val $
1524+ mkList (Var $ reflm "TTName") (map reflectName hs)
1525+ | n == tacN "prim__Guess", [] <- args
1526+ = do ok <- is_guess
1527+ if ok
1528+ then do guess <- fmap forget get_guess
1529+ fmap fst . get_type_val $
1530+ RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1531+ (Var (reflm "TT")))
1532+ guess
1533+ else fmap fst . get_type_val $
1534+ RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1535+ (Var (reflm "TT"))
1536+ | n == tacN "prim__Env", [] <- args
1537+ = do env <- get_env
1538+ fmap fst . get_type_val $ reflectEnv env
1539+ | n == tacN "prim__Fail", [_a, errs] <- args
1540+ = do parts <- reifyReportParts (eval errs)
1541+ lift . tfail $ ReflectionError [parts] (Msg "")
1542+ | n == tacN "prim__PureTactical", [_a, tm] <- args
1543+ = return tm
1544+ | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1545+ = do let first' = eval first
1546+ res <- runTacTm first'
1547+ let next = eval (App andThen res)
1548+ runTacTm next
1549+ | n == tacN "prim__Try", [_a, first, alt] <- args
1550+ = do let first' = eval first
1551+ let alt' = eval alt
1552+ try' (runTacTm first') (runTacTm alt') True
1553+ | n == tacN "prim__Fill", [raw] <- args
1554+ = do raw' <- reifyRaw raw
1555+ apply raw' []
1556+ returnUnit
1557+ | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args
1558+ = do n <- getNameFrom (sMN 0 hint)
1559+ fmap fst $ get_type_val (reflectName n)
1560+ | n == tacN "prim__Claim", [n, ty] <- args
1561+ = do n' <- reifyTTName n
1562+ ty' <- reifyRaw ty
1563+ claim n' ty'
1564+ returnUnit
1565+ | n == tacN "prim__Forget", [tt] <- args
1566+ = do tt' <- reifyTT tt
1567+ fmap fst . get_type_val $ reflect tt'
1568+ | n == tacN "prim__Attack", [] <- args
1569+ = do attack
1570+ returnUnit
1571+ | n == tacN "prim__Focus", [what] <- args
1572+ = do n' <- reifyTTName what
1573+ focus n'
1574+ returnUnit
1575+ | n == tacN "prim__Unfocus", [what] <- args
1576+ = do n' <- reifyTTName what
1577+ movelast n'
1578+ returnUnit
1579+ runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1580+
14741581-- Running tactics directly
14751582-- if a tactic adds unification problems, return an error
14761583
@@ -1796,16 +1903,20 @@ reifyApp ist t [n, tt', t']
17961903 t'' <- reifyTT t'
17971904 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
17981905reifyApp ist t [errs]
1799− | t == reflm "Fail" = case unList errs of
1800− Nothing -> fail "Failed to reify errors"
1801− Just errs' ->
1802− let parts = mapM reifyReportPart errs' in
1803− case parts of
1804− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1805− Right errs'' ->
1806− return $ TFail errs''
1906+ | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
18071907reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
18081908
1909+reifyReportParts :: Term -> ElabD [ErrorReportPart]
1910+reifyReportParts errs =
1911+ case unList errs of
1912+ Nothing -> fail "Failed to reify errors"
1913+ Just errs' ->
1914+ let parts = mapM reifyReportPart errs' in
1915+ case parts of
1916+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1917+ Right errs'' ->
1918+ return errs''
1919+
18091920-- | Reify terms from their reflected representation
18101921reifyTT :: Term -> ElabD Term
18111922reifyTT t@(App _ _)
@@ -1985,6 +2096,7 @@ reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
19852096reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
19862097reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
19872098 (reifyNativeTy nt)
2099+reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
19882100
19892101reifyTTUExp :: Term -> ElabD UExp
19902102reifyTTUExp t@(App _ _)
@@ -2001,7 +2113,11 @@ reflCall funName args
20012113
20022114-- | Lift a term into its Language.Reflection.TT representation
20032115reflect :: Term -> Raw
2004−reflect = reflectQuote []
2116+reflect = reflectTTQuote []
2117+
2118+-- | Lift a term into its Language.Reflection.Raw representation
2119+reflectRaw :: Raw -> Raw
2120+reflectRaw = reflectRawQuote []
20052121
20062122claimTT :: Name -> ElabD Name
20072123claimTT n = do n' <- getNameFrom n
@@ -2012,8 +2128,8 @@ claimTT n = do n' <- getNameFrom n
20122128-- In particular, the less-interesting bits are elaborated to _ patterns. This
20132129-- happens to NameTypes, universe levels, names that are bound but not used,
20142130-- and the type annotation field of the P constructor.
2015−reflectQuotePattern :: [Name] -> Term -> ElabD ()
2016−reflectQuotePattern unq (P _ n _)
2131+reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
2132+reflectTTQuotePattern unq (P _ n _)
20172133 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
20182134 do fill (Var n) ; solve
20192135 | otherwise =
@@ -2027,10 +2143,10 @@ reflectQuotePattern unq (P _ n _)
20272143 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
20282144 solve
20292145 focus n'; reflectNameQuotePattern n
2030−reflectQuotePattern unq (V n)
2146+reflectTTQuotePattern unq (V n)
20312147 = do fill $ reflCall "V" [RConstant (I n)]
20322148 solve
2033−reflectQuotePattern unq (Bind n b x)
2149+reflectTTQuotePattern unq (Bind n b x)
20342150 = do x' <- claimTT (sMN 0 "sc")
20352151 movelast x'
20362152 b' <- getNameFrom (sMN 0 "binder")
@@ -2050,7 +2166,7 @@ reflectQuotePattern unq (Bind n b x)
20502166 Var b',
20512167 Var x']
20522168 solve
2053− focus x'; reflectQuotePattern unq x
2169+ focus x'; reflectTTQuotePattern unq x
20542170 focus b'; reflectBinderQuotePattern unq b
20552171
20562172 where
@@ -2059,102 +2175,136 @@ reflectQuotePattern unq (Bind n b x)
20592175 = do t' <- claimTT (sMN 0 "ty"); movelast t'
20602176 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
20612177 solve
2062− focus t'; reflectQuotePattern unq t
2178+ focus t'; reflectTTQuotePattern unq t
20632179 reflectBinderQuotePattern unq (Pi _ t k)
20642180 = do t' <- claimTT (sMN 0 "ty") ; movelast t'
20652181 k' <- claimTT (sMN 0 "k"); movelast k';
20662182 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
20672183 solve
2068− focus t'; reflectQuotePattern unq t
2184+ focus t'; reflectTTQuotePattern unq t
20692185 reflectBinderQuotePattern unq (Let x y)
20702186 = do x' <- claimTT (sMN 0 "ty"); movelast x';
20712187 y' <- claimTT (sMN 0 "v"); movelast y';
20722188 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
20732189 solve
2074− focus x'; reflectQuotePattern unq x
2075− focus y'; reflectQuotePattern unq y
2190+ focus x'; reflectTTQuotePattern unq x
2191+ focus y'; reflectTTQuotePattern unq y
20762192 reflectBinderQuotePattern unq (NLet x y)
20772193 = do x' <- claimTT (sMN 0 "ty"); movelast x'
20782194 y' <- claimTT (sMN 0 "v"); movelast y'
20792195 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
20802196 solve
2081− focus x'; reflectQuotePattern unq x
2082− focus y'; reflectQuotePattern unq y
2197+ focus x'; reflectTTQuotePattern unq x
2198+ focus y'; reflectTTQuotePattern unq y
20832199 reflectBinderQuotePattern unq (Hole t)
20842200 = do t' <- claimTT (sMN 0 "ty"); movelast t'
20852201 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
20862202 solve
2087− focus t'; reflectQuotePattern unq t
2203+ focus t'; reflectTTQuotePattern unq t
20882204 reflectBinderQuotePattern unq (GHole _ t)
20892205 = do t' <- claimTT (sMN 0 "ty"); movelast t'
20902206 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
20912207 solve
2092− focus t'; reflectQuotePattern unq t
2208+ focus t'; reflectTTQuotePattern unq t
20932209 reflectBinderQuotePattern unq (Guess x y)
20942210 = do x' <- claimTT (sMN 0 "ty"); movelast x'
20952211 y' <- claimTT (sMN 0 "v"); movelast y'
20962212 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
20972213 solve
2098− focus x'; reflectQuotePattern unq x
2099− focus y'; reflectQuotePattern unq y
2214+ focus x'; reflectTTQuotePattern unq x
2215+ focus y'; reflectTTQuotePattern unq y
21002216 reflectBinderQuotePattern unq (PVar t)
21012217 = do t' <- claimTT (sMN 0 "ty"); movelast t'
21022218 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
21032219 solve
2104− focus t'; reflectQuotePattern unq t
2220+ focus t'; reflectTTQuotePattern unq t
21052221 reflectBinderQuotePattern unq (PVTy t)
21062222 = do t' <- claimTT (sMN 0 "ty"); movelast t'
21072223 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
21082224 solve
2109− focus t'; reflectQuotePattern unq t
2110−reflectQuotePattern unq (App f x)
2225+ focus t'; reflectTTQuotePattern unq t
2226+reflectTTQuotePattern unq (App f x)
21112227 = do f' <- claimTT (sMN 0 "f"); movelast f'
21122228 x' <- claimTT (sMN 0 "x"); movelast x'
21132229 fill $ reflCall "App" [Var f', Var x']
21142230 solve
2115− focus f'; reflectQuotePattern unq f
2116− focus x'; reflectQuotePattern unq x
2117−reflectQuotePattern unq (Constant c)
2231+ focus f'; reflectTTQuotePattern unq f
2232+ focus x'; reflectTTQuotePattern unq x
2233+reflectTTQuotePattern unq (Constant c)
21182234 = do fill $ reflCall "TConst" [reflectConstant c]
21192235 solve
2120−reflectQuotePattern unq (Proj t i)
2236+reflectTTQuotePattern unq (Proj t i)
21212237 = do t' <- claimTT (sMN 0 "t"); movelast t'
21222238 fill $ reflCall "Proj" [Var t', RConstant (I i)]
21232239 solve
2124− focus t'; reflectQuotePattern unq t
2125−reflectQuotePattern unq (Erased)
2240+ focus t'; reflectTTQuotePattern unq t
2241+reflectTTQuotePattern unq (Erased)
21262242 = do erased <- claimTT (sMN 0 "erased")
21272243 movelast erased
21282244 fill $ (Var erased)
21292245 solve
2130−reflectQuotePattern unq (Impossible)
2246+reflectTTQuotePattern unq (Impossible)
21312247 = do fill $ Var (reflm "Impossible")
21322248 solve
2133−reflectQuotePattern unq (TType exp)
2249+reflectTTQuotePattern unq (TType exp)
21342250 = do ue <- getNameFrom (sMN 0 "uexp")
21352251 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
21362252 movelast ue
21372253 fill $ reflCall "TType" [Var ue]
21382254 solve
2255+reflectTTQuotePattern unq (UType u)
2256+ = do uH <- getNameFrom (sMN 0 "someUniv")
2257+ claim uH (Var (reflm "Universe"))
2258+ movelast uH
2259+ fill $ reflCall "UType" [Var uH]
2260+ solve
2261+ focus uH
2262+ fill (Var (reflm (case u of
2263+ NullType -> "NullType"
2264+ UniqueType -> "UniqueType"
2265+ AllTypes -> "AllTypes")))
2266+ solve
21392267
2140−-- | Create a reflected term, but leave refs to the provided name intact
2141−reflectQuote :: [Name] -> Term -> Raw
2142−reflectQuote unq (P nt n t)
2268+reflectUniverse :: Universe -> Raw
2269+reflectUniverse u =
2270+ (Var (reflm (case u of
2271+ NullType -> "NullType"
2272+ UniqueType -> "UniqueType"
2273+ AllTypes -> "AllTypes")))
2274+
2275+-- | Create a reflected TT term, but leave refs to the provided name intact
2276+reflectTTQuote :: [Name] -> Term -> Raw
2277+reflectTTQuote unq (P nt n t)
21432278 | n `elem` unq = Var n
2144− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
2145−reflectQuote unq (V n)
2279+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2280+reflectTTQuote unq (V n)
21462281 = reflCall "V" [RConstant (I n)]
2147−reflectQuote unq (Bind n b x)
2148− = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]
2149−reflectQuote unq (App f x)
2150− = reflCall "App" [reflectQuote unq f, reflectQuote unq x]
2151−reflectQuote unq (Constant c)
2282+reflectTTQuote unq (Bind n b x)
2283+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]
2284+reflectTTQuote unq (App f x)
2285+ = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2286+reflectTTQuote unq (Constant c)
21522287 = reflCall "TConst" [reflectConstant c]
2153−reflectQuote unq (Proj t i)
2154− = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
2155−reflectQuote unq (Erased) = Var (reflm "Erased")
2156−reflectQuote unq (Impossible) = Var (reflm "Impossible")
2157−reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2288+reflectTTQuote unq (Proj t i)
2289+ = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2290+reflectTTQuote unq (Erased) = Var (reflm "Erased")
2291+reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2292+reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2293+reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
2294+
2295+reflectRawQuote :: [Name] -> Raw -> Raw
2296+reflectRawQuote unq (Var n)
2297+ | n `elem` unq = Var n
2298+ | otherwise = reflCall "Var" [reflectName n]
2299+reflectRawQuote unq (RBind n b r) =
2300+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]
2301+reflectRawQuote unq (RApp f x) =
2302+ reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
2303+reflectRawQuote unq RType = Var (reflm "RType")
2304+reflectRawQuote unq (RUType u) =
2305+ reflCall "RUType" [reflectUniverse u]
2306+reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
2307+reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
21582308
21592309reflectNameType :: NameType -> Raw
21602310reflectNameType (Bound) = Var (reflm "Bound")
@@ -2205,27 +2355,27 @@ reflectNameQuotePattern _ -- for all other names, match any
22052355 solve
22062356
22072357reflectBinder :: Binder Term -> Raw
2208−reflectBinder = reflectBinderQuote []
2209−
2210−reflectBinderQuote :: [Name] -> Binder Term -> Raw
2211−reflectBinderQuote unq (Lam t)
2212− = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
2213−reflectBinderQuote unq (Pi _ t k)
2214− = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]
2215−reflectBinderQuote unq (Let x y)
2216− = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2217−reflectBinderQuote unq (NLet x y)
2218− = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2219−reflectBinderQuote unq (Hole t)
2220− = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
2221−reflectBinderQuote unq (GHole _ t)
2222− = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
2223−reflectBinderQuote unq (Guess x y)
2224− = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2225−reflectBinderQuote unq (PVar t)
2226− = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
2227−reflectBinderQuote unq (PVTy t)
2228− = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
2358+reflectBinder = reflectBinderQuote reflectTTQuote []
2359+
2360+reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw
2361+reflectBinderQuote q unq (Lam t)
2362+ = reflCall "Lam" [Var (reflm "TT"), q unq t]
2363+reflectBinderQuote q unq (Pi _ t k)
2364+ = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]
2365+reflectBinderQuote q unq (Let x y)
2366+ = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]
2367+reflectBinderQuote q unq (NLet x y)
2368+ = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]
2369+reflectBinderQuote q unq (Hole t)
2370+ = reflCall "Hole" [Var (reflm "TT"), q unq t]
2371+reflectBinderQuote q unq (GHole _ t)
2372+ = reflCall "GHole" [Var (reflm "TT"), q unq t]
2373+reflectBinderQuote q unq (Guess x y)
2374+ = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]
2375+reflectBinderQuote q unq (PVar t)
2376+ = reflCall "PVar" [Var (reflm "TT"), q unq t]
2377+reflectBinderQuote q unq (PVTy t)
2378+ = reflCall "PVTy" [Var (reflm "TT"), q unq t]
22292379
22302380mkList :: Raw -> [Raw] -> Raw
22312381mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
@@ -2265,7 +2415,8 @@ reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")
22652415reflectConstant BufferType = Var (reflm "BufferType")
22662416reflectConstant VoidType = Var (reflm "VoidType")
22672417reflectConstant Forgot = Var (reflm "Forgot")
2268−
2418+reflectConstant WorldType = Var (reflm "WorldType")
2419+reflectConstant TheWorld = Var (reflm "TheWorld")
22692420
22702421reflectUExp :: UExp -> Raw
22712422reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]