@@ -983,7 +983,7 @@ elab ist info emode opts fn tm
983983 saveState
984984 updatePS (const .
985985 newProof (sMN 0 "q") ctxt $
986− P Ref tt Erased)
986+ P Ref (reflm "TT") Erased)
987987
988988 -- Re-add the unquotes, letting Idris infer the (fictional)
989989 -- types. Here, they represent the real type rather than the type
@@ -1030,8 +1030,9 @@ elab ist info emode opts fn tm
10301030 Just q -> do ctxt <- get_context
10311031 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
10321032 if pattern
1033− then reflectTTQuotePattern unquoteNames q'
1034− -- TODO: support quasiquote patterns of Raw terms
1033+ then do try' (reflectTTQuotePattern unquoteNames q')
1034+ (reflectRawQuotePattern unquoteNames (forget q'))
1035+ True
10351036 else do try' (fill $ reflectTTQuote unquoteNames q')
10361037 -- we forget q' instead of using q to ensure rechecking
10371038 (fill $ reflectRawQuote unquoteNames (forget q'))
@@ -1044,9 +1045,7 @@ elab ist info emode opts fn tm
10441045 -- happens last so that their holes still exist while elaborating
10451046 -- the main quotation.
10461047 mapM_ elabUnquote unq
1047− where tt = sNS (sUN "TT") ["Reflection", "Language"]
1048−
1049− elabUnquote (n, tm)
1048+ where elabUnquote (n, tm)
10501049 = do focus n
10511050 elabE (ina { e_qq = False }) fc tm
10521051
@@ -2175,62 +2174,7 @@ reflectTTQuotePattern unq (Bind n b x)
21752174 Var x']
21762175 solve
21772176 focus x'; reflectTTQuotePattern unq x
2178− focus b'; reflectBinderQuotePattern unq b
2179−
2180− where
2181− reflectBinderQuotePattern :: [Name] -> Binder Term -> ElabD ()
2182− reflectBinderQuotePattern unq (Lam t)
2183− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2184− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2185− solve
2186− focus t'; reflectTTQuotePattern unq t
2187− reflectBinderQuotePattern unq (Pi _ t k)
2188− = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2189− k' <- claimTT (sMN 0 "k"); movelast k';
2190− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2191− solve
2192− focus t'; reflectTTQuotePattern unq t
2193− reflectBinderQuotePattern unq (Let x y)
2194− = do x' <- claimTT (sMN 0 "ty"); movelast x';
2195− y' <- claimTT (sMN 0 "v"); movelast y';
2196− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2197− solve
2198− focus x'; reflectTTQuotePattern unq x
2199− focus y'; reflectTTQuotePattern unq y
2200− reflectBinderQuotePattern unq (NLet x y)
2201− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2202− y' <- claimTT (sMN 0 "v"); movelast y'
2203− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2204− solve
2205− focus x'; reflectTTQuotePattern unq x
2206− focus y'; reflectTTQuotePattern unq y
2207− reflectBinderQuotePattern unq (Hole t)
2208− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2209− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2210− solve
2211− focus t'; reflectTTQuotePattern unq t
2212− reflectBinderQuotePattern unq (GHole _ t)
2213− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2214− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2215− solve
2216− focus t'; reflectTTQuotePattern unq t
2217− reflectBinderQuotePattern unq (Guess x y)
2218− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2219− y' <- claimTT (sMN 0 "v"); movelast y'
2220− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2221− solve
2222− focus x'; reflectTTQuotePattern unq x
2223− focus y'; reflectTTQuotePattern unq y
2224− reflectBinderQuotePattern unq (PVar t)
2225− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2226− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2227− solve
2228− focus t'; reflectTTQuotePattern unq t
2229− reflectBinderQuotePattern unq (PVTy t)
2230− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2231− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2232− solve
2233− focus t'; reflectTTQuotePattern unq t
2177+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
22342178reflectTTQuotePattern unq (App f x)
22352179 = do f' <- claimTT (sMN 0 "f"); movelast f'
22362180 x' <- claimTT (sMN 0 "x"); movelast x'
@@ -2273,6 +2217,131 @@ reflectTTQuotePattern unq (UType u)
22732217 AllTypes -> "AllTypes")))
22742218 solve
22752219
2220+reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
2221+reflectRawQuotePattern unq (Var n)
2222+ -- the unquoted names already have types, just use them
2223+ | n `elem` unq = do fill (Var n); solve
2224+ | otherwise = do fill (reflCall "Var" [reflectName n]); solve
2225+reflectRawQuotePattern unq (RBind n b sc) =
2226+ do scH <- getNameFrom (sMN 0 "sc")
2227+ claim scH (Var (reflm "Raw"))
2228+ movelast scH
2229+ bH <- getNameFrom (sMN 0 "binder")
2230+ claim bH (RApp (Var (reflm "Binder"))
2231+ (Var (reflm "Raw")))
2232+ if n `elem` freeNamesR sc
2233+ then do fill $ reflCall "RBind" [reflectName n,
2234+ Var bH,
2235+ Var scH]
2236+ solve
2237+ else do any <- getNameFrom (sMN 0 "anyName")
2238+ claim any (Var (reflm "TTName"))
2239+ movelast any
2240+ fill $ reflCall "RBind" [Var any, Var bH, Var scH]
2241+ solve
2242+ focus scH; reflectRawQuotePattern unq sc
2243+ focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
2244+ where freeNamesR (Var n) = [n]
2245+ freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
2246+ freeNamesR body \\ [n],
2247+ freeNamesR t]
2248+ freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
2249+ (freeNamesR body \\ [n])
2250+ freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
2251+ freeNamesR RType = []
2252+ freeNamesR (RUType _) = []
2253+ freeNamesR (RForce r) = freeNamesR r
2254+ freeNamesR (RConstant _) = []
2255+reflectRawQuotePattern unq (RApp f x) =
2256+ do fH <- getNameFrom (sMN 0 "f")
2257+ claim fH (Var (reflm "Raw"))
2258+ movelast fH
2259+ xH <- getNameFrom (sMN 0 "x")
2260+ claim xH (Var (reflm "Raw"))
2261+ movelast xH
2262+ fill $ reflCall "RApp" [Var fH, Var xH]
2263+ solve
2264+ focus fH; reflectRawQuotePattern unq f
2265+ focus xH; reflectRawQuotePattern unq x
2266+reflectRawQuotePattern unq RType =
2267+ do fill (Var (reflm "RType"))
2268+ solve
2269+reflectRawQuotePattern unq (RUType univ) =
2270+ do uH <- getNameFrom (sMN 0 "universe")
2271+ claim uH (Var (reflm "Universe"))
2272+ movelast uH
2273+ fill $ reflCall "RUType" [Var uH]
2274+ solve
2275+ focus uH; fill (reflectUniverse univ); solve
2276+reflectRawQuotePattern unq (RForce r) =
2277+ do rH <- getNameFrom (sMN 0 "raw")
2278+ claim rH (Var (reflm "Raw"))
2279+ movelast rH
2280+ fill $ reflCall "RForce" [Var rH]
2281+ solve
2282+ focus rH; reflectRawQuotePattern unq r
2283+reflectRawQuotePattern unq (RConstant c) =
2284+ do cH <- getNameFrom (sMN 0 "const")
2285+ claim cH (Var (reflm "Constant"))
2286+ movelast cH
2287+ fill (reflCall "RConstant" [Var cH]); solve
2288+ focus cH
2289+ fill (reflectConstant c); solve
2290+
2291+reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
2292+reflectBinderQuotePattern q unq (Lam t)
2293+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2294+ fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2295+ solve
2296+ focus t'; q unq t
2297+reflectBinderQuotePattern q unq (Pi _ t k)
2298+ = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2299+ k' <- claimTT (sMN 0 "k"); movelast k';
2300+ fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2301+ solve
2302+ focus t'; q unq t
2303+reflectBinderQuotePattern q unq (Let x y)
2304+ = do x' <- claimTT (sMN 0 "ty"); movelast x';
2305+ y' <- claimTT (sMN 0 "v"); movelast y';
2306+ fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2307+ solve
2308+ focus x'; q unq x
2309+ focus y'; q unq y
2310+reflectBinderQuotePattern q unq (NLet x y)
2311+ = do x' <- claimTT (sMN 0 "ty"); movelast x'
2312+ y' <- claimTT (sMN 0 "v"); movelast y'
2313+ fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2314+ solve
2315+ focus x'; q unq x
2316+ focus y'; q unq y
2317+reflectBinderQuotePattern q unq (Hole t)
2318+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2319+ fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2320+ solve
2321+ focus t'; q unq t
2322+reflectBinderQuotePattern q unq (GHole _ t)
2323+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2324+ fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2325+ solve
2326+ focus t'; q unq t
2327+reflectBinderQuotePattern q unq (Guess x y)
2328+ = do x' <- claimTT (sMN 0 "ty"); movelast x'
2329+ y' <- claimTT (sMN 0 "v"); movelast y'
2330+ fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2331+ solve
2332+ focus x'; q unq x
2333+ focus y'; q unq y
2334+reflectBinderQuotePattern q unq (PVar t)
2335+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2336+ fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2337+ solve
2338+ focus t'; q unq t
2339+reflectBinderQuotePattern q unq (PVTy t)
2340+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2341+ fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2342+ solve
2343+ focus t'; q unq t
2344+
22762345reflectUniverse :: Universe -> Raw
22772346reflectUniverse u =
22782347 (Var (reflm (case u of