@@ -1,5 +1,5 @@
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
2−
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.ElabTerm where
3module Idris.ElabTerm where
5import Idris.AbsSyntax
5import Idris.AbsSyntax
@@ -400,6 +400,7 @@ elab ist info emode opts fn tm
400 where -- if none work, take the error from the first
400 where -- if none work, take the error from the first
401 trySeq (x : xs) = let e1 = elab' ina fc x in
401 trySeq (x : xs) = let e1 = elab' ina fc x in
402 try' e1 (trySeq' e1 xs) True
402 try' e1 (trySeq' e1 xs) True
403+ trySeq [] = fail "Nothing to try in sequence"
403 trySeq' deferr [] = proofFail deferr
404 trySeq' deferr [] = proofFail deferr
404 trySeq' deferr (x : xs)
405 trySeq' deferr (x : xs)
405 = try' (do elab' ina fc x
406 = try' (do elab' ina fc x
@@ -526,7 +527,8 @@ elab ist info emode opts fn tm
526 -- HACK: If the name leaks into its type, it may leak out of
527 -- HACK: If the name leaks into its type, it may leak out of
527 -- scope outside, so substitute in the outer scope.
528 -- scope outside, so substitute in the outer scope.
528 expandLet n (case lookup n env of
529 expandLet n (case lookup n env of
529− Just (Let t v) -> v)
530+ Just (Let t v) -> v
531+ other -> error ("Value not a let binding: " ++ show other))
531 elab' ina _ (PGoal fc r n sc) = do
533 elab' ina _ (PGoal fc r n sc) = do
532 rty <- goal
534 rty <- goal
@@ -935,7 +937,7 @@ elab ist info emode opts fn tm
935 elab' ina fc (PUnifyLog t) = do unifyLog True
937 elab' ina fc (PUnifyLog t) = do unifyLog True
936 elab' ina fc t
938 elab' ina fc t
937 unifyLog False
939 unifyLog False
938− elab' ina fc (PQuasiquote t goal) -- TODO: goal type
940+ elab' ina fc (PQuasiquote t goal)
939 = do -- First extract the unquoted subterms, replacing them with fresh
941 = do -- First extract the unquoted subterms, replacing them with fresh
940 -- names in the quasiquoted term. Claim their reflections to be
942 -- names in the quasiquoted term. Claim their reflections to be
941 -- of type TT.
943 -- of type TT.
@@ -997,9 +999,14 @@ elab ist info emode opts fn tm
997 Just q -> do ctxt <- get_context
999 Just q -> do ctxt <- get_context
998 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
1000 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
999 if pattern
1001 if pattern
1000− then reflectQuotePattern unquoteNames q'
1002+ then reflectTTQuotePattern unquoteNames q'
1003+ -- TODO: support quasiquote patterns of Raw terms
1004+ else do try' (fill $ reflectTTQuote unquoteNames q')
1005+ -- we forget q' instead of using q to ensure rechecking
1001− else do fill $ reflectQuote unquoteNames q'
1006+ (fill $ reflectRawQuote unquoteNames (forget q'))
1007+ True -- ignore errors like proof search does
1003 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
1010 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
1005 -- Finally fill in the terms or patterns from the unquotes. This
1012 -- Finally fill in the terms or patterns from the unquotes. This
@@ -1066,6 +1073,7 @@ elab ist info emode opts fn tm
1066 findScr [(n, (_, t))] = [(n, (True, t))]
1073 findScr [(n, (_, t))] = [(n, (True, t))]
1067 findScr (x : xs) = x : findScr xs
1074 findScr (x : xs) = x : findScr xs
1068 -- [] can't happen since scrutinee is in the environment!
1075 -- [] can't happen since scrutinee is in the environment!
1076+ findScr [] = error "The impossible happened - the scrutinee was not in the environment"
1070 -- To make sure top level pattern name remains in scope, put
1078 -- To make sure top level pattern name remains in scope, put
1071 -- it at the end of the environment
1079 -- it at the end of the environment
@@ -1227,7 +1235,8 @@ elab ist info emode opts fn tm
1227 lift (tfail (elaboratingArgErr while' e))
1235 lift (tfail (elaboratingArgErr while' e))
1228 put newState
1236 put newState
1229 return result
1237 return result
1230−
1238+ elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
1239+ fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
1232-- For every alternative, look at the function at the head. Automatically resolve
1241-- For every alternative, look at the function at the head. Automatically resolve
1233-- any nested alternatives where that function is also at the head
1242-- any nested alternatives where that function is also at the head
@@ -1405,6 +1414,7 @@ resTC' tcs defaultOn depth topg fn ist
1405 let imps = case lookupCtxtName n (idris_implicits ist) of
1414 let imps = case lookupCtxtName n (idris_implicits ist) of
1406 [] -> []
1415 [] -> []
1407 [args] -> map isImp (snd args) -- won't be overloaded!
1416 [args] -> map isImp (snd args) -- won't be overloaded!
1417+ xs -> error "The impossible happened - overloading is not expected here!"
1408 ps <- get_probs
1418 ps <- get_probs
1409 tm <- get_term
1419 tm <- get_term
1410 args <- map snd <$> try' (apply (Var n) imps)
1420 args <- map snd <$> try' (apply (Var n) imps)
@@ -2063,6 +2073,7 @@ reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
2063reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
2073reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
2064reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
2074reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
2065 (reifyNativeTy nt)
2075 (reifyNativeTy nt)
2076+reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
2067reifyTTUExp :: Term -> ElabD UExp
2078reifyTTUExp :: Term -> ElabD UExp
2068reifyTTUExp t@(App _ _)
2079reifyTTUExp t@(App _ _)
@@ -2079,7 +2090,11 @@ reflCall funName args
2080-- | Lift a term into its Language.Reflection.TT representation
2091-- | Lift a term into its Language.Reflection.TT representation
2081reflect :: Term -> Raw
2092reflect :: Term -> Raw
2082−reflect = reflectQuote []
2093+reflect = reflectTTQuote []
2095+-- | Lift a term into its Language.Reflection.Raw representation
2096+reflectRaw :: Raw -> Raw
2097+reflectRaw = reflectRawQuote []
2084claimTT :: Name -> ElabD Name
2099claimTT :: Name -> ElabD Name
2085claimTT n = do n' <- getNameFrom n
2100claimTT n = do n' <- getNameFrom n
@@ -2090,8 +2105,8 @@ claimTT n = do n' <- getNameFrom n
2090-- In particular, the less-interesting bits are elaborated to _ patterns. This
2105-- In particular, the less-interesting bits are elaborated to _ patterns. This
2091-- happens to NameTypes, universe levels, names that are bound but not used,
2106-- happens to NameTypes, universe levels, names that are bound but not used,
2092-- and the type annotation field of the P constructor.
2107-- and the type annotation field of the P constructor.
2093−reflectQuotePattern :: [Name] -> Term -> ElabD ()
2108+reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
2094−reflectQuotePattern unq (P _ n _)
2109+reflectTTQuotePattern unq (P _ n _)
2095 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
2110 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
2096 do fill (Var n) ; solve
2111 do fill (Var n) ; solve
2097 | otherwise =
2112 | otherwise =
@@ -2105,10 +2120,10 @@ reflectQuotePattern unq (P _ n _)
2105 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
2120 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
2107 focus n'; reflectNameQuotePattern n
2122 focus n'; reflectNameQuotePattern n
2108−reflectQuotePattern unq (V n)
2123+reflectTTQuotePattern unq (V n)
2109 = do fill $ reflCall "V" [RConstant (I n)]
2124 = do fill $ reflCall "V" [RConstant (I n)]
2111−reflectQuotePattern unq (Bind n b x)
2126+reflectTTQuotePattern unq (Bind n b x)
2112 = do x' <- claimTT (sMN 0 "sc")
2127 = do x' <- claimTT (sMN 0 "sc")
2113 movelast x'
2128 movelast x'
2114 b' <- getNameFrom (sMN 0 "binder")
2129 b' <- getNameFrom (sMN 0 "binder")
@@ -2128,7 +2143,7 @@ reflectQuotePattern unq (Bind n b x)
2131− focus x'; reflectQuotePattern unq x
2146+ focus x'; reflectTTQuotePattern unq x
2132 focus b'; reflectBinderQuotePattern unq b
2147 focus b'; reflectBinderQuotePattern unq b
@@ -2137,102 +2152,136 @@ reflectQuotePattern unq (Bind n b x)
2137 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2152 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2138 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2153 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2140− focus t'; reflectQuotePattern unq t
2155+ focus t'; reflectTTQuotePattern unq t
2141 reflectBinderQuotePattern unq (Pi _ t k)
2156 reflectBinderQuotePattern unq (Pi _ t k)
2142 = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2157 = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2143 k' <- claimTT (sMN 0 "k"); movelast k';
2158 k' <- claimTT (sMN 0 "k"); movelast k';
2144 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2159 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2146− focus t'; reflectQuotePattern unq t
2161+ focus t'; reflectTTQuotePattern unq t
2147 reflectBinderQuotePattern unq (Let x y)
2162 reflectBinderQuotePattern unq (Let x y)
2148 = do x' <- claimTT (sMN 0 "ty"); movelast x';
2163 = do x' <- claimTT (sMN 0 "ty"); movelast x';
2149 y' <- claimTT (sMN 0 "v"); movelast y';
2164 y' <- claimTT (sMN 0 "v"); movelast y';
2150 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2165 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2152− focus x'; reflectQuotePattern unq x
2167+ focus x'; reflectTTQuotePattern unq x
2153− focus y'; reflectQuotePattern unq y
2168+ focus y'; reflectTTQuotePattern unq y
2154 reflectBinderQuotePattern unq (NLet x y)
2169 reflectBinderQuotePattern unq (NLet x y)
2155 = do x' <- claimTT (sMN 0 "ty"); movelast x'
2170 = do x' <- claimTT (sMN 0 "ty"); movelast x'
2156 y' <- claimTT (sMN 0 "v"); movelast y'
2171 y' <- claimTT (sMN 0 "v"); movelast y'
2157 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2172 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2159− focus x'; reflectQuotePattern unq x
2174+ focus x'; reflectTTQuotePattern unq x
2160− focus y'; reflectQuotePattern unq y
2175+ focus y'; reflectTTQuotePattern unq y
2161 reflectBinderQuotePattern unq (Hole t)
2176 reflectBinderQuotePattern unq (Hole t)
2162 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2177 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2163 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2178 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2165− focus t'; reflectQuotePattern unq t
2180+ focus t'; reflectTTQuotePattern unq t
2166 reflectBinderQuotePattern unq (GHole _ t)
2181 reflectBinderQuotePattern unq (GHole _ t)
2167 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2182 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2168 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2183 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2170− focus t'; reflectQuotePattern unq t
2185+ focus t'; reflectTTQuotePattern unq t
2171 reflectBinderQuotePattern unq (Guess x y)
2186 reflectBinderQuotePattern unq (Guess x y)
2172 = do x' <- claimTT (sMN 0 "ty"); movelast x'
2187 = do x' <- claimTT (sMN 0 "ty"); movelast x'
2173 y' <- claimTT (sMN 0 "v"); movelast y'
2188 y' <- claimTT (sMN 0 "v"); movelast y'
2174 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2189 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2176− focus x'; reflectQuotePattern unq x
2191+ focus x'; reflectTTQuotePattern unq x
2177− focus y'; reflectQuotePattern unq y
2192+ focus y'; reflectTTQuotePattern unq y
2178 reflectBinderQuotePattern unq (PVar t)
2193 reflectBinderQuotePattern unq (PVar t)
2179 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2194 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2180 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2195 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2182− focus t'; reflectQuotePattern unq t
2197+ focus t'; reflectTTQuotePattern unq t
2183 reflectBinderQuotePattern unq (PVTy t)
2198 reflectBinderQuotePattern unq (PVTy t)
2184 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2199 = do t' <- claimTT (sMN 0 "ty"); movelast t'
2185 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2200 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2187− focus t'; reflectQuotePattern unq t
2202+ focus t'; reflectTTQuotePattern unq t
2188−reflectQuotePattern unq (App f x)
2203+reflectTTQuotePattern unq (App f x)
2189 = do f' <- claimTT (sMN 0 "f"); movelast f'
2204 = do f' <- claimTT (sMN 0 "f"); movelast f'
2190 x' <- claimTT (sMN 0 "x"); movelast x'
2205 x' <- claimTT (sMN 0 "x"); movelast x'
2191 fill $ reflCall "App" [Var f', Var x']
2206 fill $ reflCall "App" [Var f', Var x']
2193− focus f'; reflectQuotePattern unq f
2208+ focus f'; reflectTTQuotePattern unq f
2194− focus x'; reflectQuotePattern unq x
2209+ focus x'; reflectTTQuotePattern unq x
2195−reflectQuotePattern unq (Constant c)
2210+reflectTTQuotePattern unq (Constant c)
2196 = do fill $ reflCall "TConst" [reflectConstant c]
2211 = do fill $ reflCall "TConst" [reflectConstant c]
2198−reflectQuotePattern unq (Proj t i)
2213+reflectTTQuotePattern unq (Proj t i)
2199 = do t' <- claimTT (sMN 0 "t"); movelast t'
2214 = do t' <- claimTT (sMN 0 "t"); movelast t'
2200 fill $ reflCall "Proj" [Var t', RConstant (I i)]
2215 fill $ reflCall "Proj" [Var t', RConstant (I i)]
2202− focus t'; reflectQuotePattern unq t
2217+ focus t'; reflectTTQuotePattern unq t
2203−reflectQuotePattern unq (Erased)
2218+reflectTTQuotePattern unq (Erased)
2204 = do erased <- claimTT (sMN 0 "erased")
2219 = do erased <- claimTT (sMN 0 "erased")
2205 movelast erased
2220 movelast erased
2206 fill $ (Var erased)
2221 fill $ (Var erased)
2208−reflectQuotePattern unq (Impossible)
2223+reflectTTQuotePattern unq (Impossible)
2209 = do fill $ Var (reflm "Impossible")
2224 = do fill $ Var (reflm "Impossible")
2211−reflectQuotePattern unq (TType exp)
2226+reflectTTQuotePattern unq (TType exp)
2212 = do ue <- getNameFrom (sMN 0 "uexp")
2227 = do ue <- getNameFrom (sMN 0 "uexp")
2213 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2228 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2214 movelast ue
2229 movelast ue
2215 fill $ reflCall "TType" [Var ue]
2230 fill $ reflCall "TType" [Var ue]
2232+reflectTTQuotePattern unq (UType u)
2233+ = do uH <- getNameFrom (sMN 0 "someUniv")
2234+ claim uH (Var (reflm "Universe"))
2236+ fill $ reflCall "UType" [Var uH]
2239+ fill (Var (reflm (case u of
2240+ NullType -> "NullType"
2241+ UniqueType -> "UniqueType"
2242+ AllTypes -> "AllTypes")))
2245+reflectUniverse :: Universe -> Raw
2247+ (Var (reflm (case u of
2248+ NullType -> "NullType"
2249+ UniqueType -> "UniqueType"
2250+ AllTypes -> "AllTypes")))
2218−-- | Create a reflected term, but leave refs to the provided name intact
2252+-- | Create a reflected TT term, but leave refs to the provided name intact
2219−reflectQuote :: [Name] -> Term -> Raw
2253+reflectTTQuote :: [Name] -> Term -> Raw
2220−reflectQuote unq (P nt n t)
2254+reflectTTQuote unq (P nt n t)
2221 | n `elem` unq = Var n
2255 | n `elem` unq = Var n
2222− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
2256+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2223−reflectQuote unq (V n)
2257+reflectTTQuote unq (V n)
2224 = reflCall "V" [RConstant (I n)]
2258 = reflCall "V" [RConstant (I n)]
2225−reflectQuote unq (Bind n b x)
2259+reflectTTQuote unq (Bind n b x)
2226− = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]
2260+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]
2227−reflectQuote unq (App f x)
2261+reflectTTQuote unq (App f x)
2228− = reflCall "App" [reflectQuote unq f, reflectQuote unq x]
2262+ = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2229−reflectQuote unq (Constant c)
2263+reflectTTQuote unq (Constant c)
2230 = reflCall "TConst" [reflectConstant c]
2264 = reflCall "TConst" [reflectConstant c]
2231−reflectQuote unq (Proj t i)
2265+reflectTTQuote unq (Proj t i)
2232− = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
2266+ = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2233−reflectQuote unq (Erased) = Var (reflm "Erased")
2267+reflectTTQuote unq (Erased) = Var (reflm "Erased")
2234−reflectQuote unq (Impossible) = Var (reflm "Impossible")
2268+reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2235−reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2269+reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2270+reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
2272+reflectRawQuote :: [Name] -> Raw -> Raw
2273+reflectRawQuote unq (Var n)
2274+ | n `elem` unq = Var n
2275+ | otherwise = reflCall "Var" [reflectName n]
2276+reflectRawQuote unq (RBind n b r) =
2277+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]
2278+reflectRawQuote unq (RApp f x) =
2279+ reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
2280+reflectRawQuote unq RType = Var (reflm "RType")
2281+reflectRawQuote unq (RUType u) =
2282+ reflCall "RUType" [reflectUniverse u]
2283+reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
2284+reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
2237reflectNameType :: NameType -> Raw
2286reflectNameType :: NameType -> Raw
2238reflectNameType (Bound) = Var (reflm "Bound")
2287reflectNameType (Bound) = Var (reflm "Bound")
@@ -2283,27 +2332,27 @@ reflectNameQuotePattern _ -- for all other names, match any
2285reflectBinder :: Binder Term -> Raw
2334reflectBinder :: Binder Term -> Raw
2286−reflectBinder = reflectBinderQuote []
2335+reflectBinder = reflectBinderQuote reflectTTQuote []
2288−reflectBinderQuote :: [Name] -> Binder Term -> Raw
2337+reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw
2289−reflectBinderQuote unq (Lam t)
2338+reflectBinderQuote q unq (Lam t)
2290− = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
2339+ = reflCall "Lam" [Var (reflm "TT"), q unq t]
2291−reflectBinderQuote unq (Pi _ t k)
2340+reflectBinderQuote q unq (Pi _ t k)
2292− = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]
2341+ = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]
2293−reflectBinderQuote unq (Let x y)
2342+reflectBinderQuote q unq (Let x y)
2294− = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2343+ = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]
2295−reflectBinderQuote unq (NLet x y)
2344+reflectBinderQuote q unq (NLet x y)
2296− = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2345+ = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]
2297−reflectBinderQuote unq (Hole t)
2346+reflectBinderQuote q unq (Hole t)
2298− = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
2347+ = reflCall "Hole" [Var (reflm "TT"), q unq t]
2299−reflectBinderQuote unq (GHole _ t)
2348+reflectBinderQuote q unq (GHole _ t)
2300− = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
2349+ = reflCall "GHole" [Var (reflm "TT"), q unq t]
2301−reflectBinderQuote unq (Guess x y)
2350+reflectBinderQuote q unq (Guess x y)
2302− = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2351+ = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]
2303−reflectBinderQuote unq (PVar t)
2352+reflectBinderQuote q unq (PVar t)
2304− = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
2353+ = reflCall "PVar" [Var (reflm "TT"), q unq t]
2305−reflectBinderQuote unq (PVTy t)
2354+reflectBinderQuote q unq (PVTy t)
2306− = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
2355+ = reflCall "PVTy" [Var (reflm "TT"), q unq t]
2308mkList :: Raw -> [Raw] -> Raw
2357mkList :: Raw -> [Raw] -> Raw
2309mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
2358mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
@@ -2343,7 +2392,8 @@ reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")
2343reflectConstant BufferType = Var (reflm "BufferType")
2392reflectConstant BufferType = Var (reflm "BufferType")
2344reflectConstant VoidType = Var (reflm "VoidType")
2393reflectConstant VoidType = Var (reflm "VoidType")
2345reflectConstant Forgot = Var (reflm "Forgot")
2394reflectConstant Forgot = Var (reflm "Forgot")
2346−
2395+reflectConstant WorldType = Var (reflm "WorldType")
2396+reflectConstant TheWorld = Var (reflm "TheWorld")
2348reflectUExp :: UExp -> Raw
2398reflectUExp :: UExp -> Raw
2349reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
2399reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]