@@ -975,7 +975,7 @@ elab ist info emode opts fn tm
975975 saveState
976976 updatePS (const .
977977 newProof (sMN 0 "q") ctxt $
978− P Ref tt Erased)
978+ P Ref (reflm "TT") Erased)
979979
980980 -- Re-add the unquotes, letting Idris infer the (fictional)
981981 -- types. Here, they represent the real type rather than the type
@@ -1022,8 +1022,9 @@ elab ist info emode opts fn tm
10221022 Just q -> do ctxt <- get_context
10231023 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
10241024 if pattern
1025− then reflectTTQuotePattern unquoteNames q'
1026− -- TODO: support quasiquote patterns of Raw terms
1025+ then do try' (reflectTTQuotePattern unquoteNames q')
1026+ (reflectRawQuotePattern unquoteNames (forget q'))
1027+ True
10271028 else do try' (fill $ reflectTTQuote unquoteNames q')
10281029 -- we forget q' instead of using q to ensure rechecking
10291030 (fill $ reflectRawQuote unquoteNames (forget q'))
@@ -1036,9 +1037,7 @@ elab ist info emode opts fn tm
10361037 -- happens last so that their holes still exist while elaborating
10371038 -- the main quotation.
10381039 mapM_ elabUnquote unq
1039− where tt = sNS (sUN "TT") ["Reflection", "Language"]
1040−
1041− elabUnquote (n, tm)
1040+ where elabUnquote (n, tm)
10421041 = do focus n
10431042 elabE (ina { e_qq = False }) fc tm
10441043
@@ -2167,62 +2166,7 @@ reflectTTQuotePattern unq (Bind n b x)
21672166 Var x']
21682167 solve
21692168 focus x'; reflectTTQuotePattern unq x
2170− focus b'; reflectBinderQuotePattern unq b
2171−
2172− where
2173− reflectBinderQuotePattern :: [Name] -> Binder Term -> ElabD ()
2174− reflectBinderQuotePattern unq (Lam t)
2175− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2176− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2177− solve
2178− focus t'; reflectTTQuotePattern unq t
2179− reflectBinderQuotePattern unq (Pi _ t k)
2180− = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2181− k' <- claimTT (sMN 0 "k"); movelast k';
2182− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2183− solve
2184− focus t'; reflectTTQuotePattern unq t
2185− reflectBinderQuotePattern unq (Let x y)
2186− = do x' <- claimTT (sMN 0 "ty"); movelast x';
2187− y' <- claimTT (sMN 0 "v"); movelast y';
2188− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2189− solve
2190− focus x'; reflectTTQuotePattern unq x
2191− focus y'; reflectTTQuotePattern unq y
2192− reflectBinderQuotePattern unq (NLet x y)
2193− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2194− y' <- claimTT (sMN 0 "v"); movelast y'
2195− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2196− solve
2197− focus x'; reflectTTQuotePattern unq x
2198− focus y'; reflectTTQuotePattern unq y
2199− reflectBinderQuotePattern unq (Hole t)
2200− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2201− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2202− solve
2203− focus t'; reflectTTQuotePattern unq t
2204− reflectBinderQuotePattern unq (GHole _ t)
2205− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2206− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2207− solve
2208− focus t'; reflectTTQuotePattern unq t
2209− reflectBinderQuotePattern unq (Guess x y)
2210− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2211− y' <- claimTT (sMN 0 "v"); movelast y'
2212− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2213− solve
2214− focus x'; reflectTTQuotePattern unq x
2215− focus y'; reflectTTQuotePattern unq y
2216− reflectBinderQuotePattern unq (PVar t)
2217− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2218− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2219− solve
2220− focus t'; reflectTTQuotePattern unq t
2221− reflectBinderQuotePattern unq (PVTy t)
2222− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2223− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2224− solve
2225− focus t'; reflectTTQuotePattern unq t
2169+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
22262170reflectTTQuotePattern unq (App f x)
22272171 = do f' <- claimTT (sMN 0 "f"); movelast f'
22282172 x' <- claimTT (sMN 0 "x"); movelast x'
@@ -2265,6 +2209,131 @@ reflectTTQuotePattern unq (UType u)
22652209 AllTypes -> "AllTypes")))
22662210 solve
22672211
2212+reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
2213+reflectRawQuotePattern unq (Var n)
2214+ -- the unquoted names already have types, just use them
2215+ | n `elem` unq = do fill (Var n); solve
2216+ | otherwise = do fill (reflCall "Var" [reflectName n]); solve
2217+reflectRawQuotePattern unq (RBind n b sc) =
2218+ do scH <- getNameFrom (sMN 0 "sc")
2219+ claim scH (Var (reflm "Raw"))
2220+ movelast scH
2221+ bH <- getNameFrom (sMN 0 "binder")
2222+ claim bH (RApp (Var (reflm "Binder"))
2223+ (Var (reflm "Raw")))
2224+ if n `elem` freeNamesR sc
2225+ then do fill $ reflCall "RBind" [reflectName n,
2226+ Var bH,
2227+ Var scH]
2228+ solve
2229+ else do any <- getNameFrom (sMN 0 "anyName")
2230+ claim any (Var (reflm "TTName"))
2231+ movelast any
2232+ fill $ reflCall "RBind" [Var any, Var bH, Var scH]
2233+ solve
2234+ focus scH; reflectRawQuotePattern unq sc
2235+ focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
2236+ where freeNamesR (Var n) = [n]
2237+ freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
2238+ freeNamesR body \\ [n],
2239+ freeNamesR t]
2240+ freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
2241+ (freeNamesR body \\ [n])
2242+ freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
2243+ freeNamesR RType = []
2244+ freeNamesR (RUType _) = []
2245+ freeNamesR (RForce r) = freeNamesR r
2246+ freeNamesR (RConstant _) = []
2247+reflectRawQuotePattern unq (RApp f x) =
2248+ do fH <- getNameFrom (sMN 0 "f")
2249+ claim fH (Var (reflm "Raw"))
2250+ movelast fH
2251+ xH <- getNameFrom (sMN 0 "x")
2252+ claim xH (Var (reflm "Raw"))
2253+ movelast xH
2254+ fill $ reflCall "RApp" [Var fH, Var xH]
2255+ solve
2256+ focus fH; reflectRawQuotePattern unq f
2257+ focus xH; reflectRawQuotePattern unq x
2258+reflectRawQuotePattern unq RType =
2259+ do fill (Var (reflm "RType"))
2260+ solve
2261+reflectRawQuotePattern unq (RUType univ) =
2262+ do uH <- getNameFrom (sMN 0 "universe")
2263+ claim uH (Var (reflm "Universe"))
2264+ movelast uH
2265+ fill $ reflCall "RUType" [Var uH]
2266+ solve
2267+ focus uH; fill (reflectUniverse univ); solve
2268+reflectRawQuotePattern unq (RForce r) =
2269+ do rH <- getNameFrom (sMN 0 "raw")
2270+ claim rH (Var (reflm "Raw"))
2271+ movelast rH
2272+ fill $ reflCall "RForce" [Var rH]
2273+ solve
2274+ focus rH; reflectRawQuotePattern unq r
2275+reflectRawQuotePattern unq (RConstant c) =
2276+ do cH <- getNameFrom (sMN 0 "const")
2277+ claim cH (Var (reflm "Constant"))
2278+ movelast cH
2279+ fill (reflCall "RConstant" [Var cH]); solve
2280+ focus cH
2281+ fill (reflectConstant c); solve
2282+
2283+reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
2284+reflectBinderQuotePattern q unq (Lam t)
2285+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2286+ fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2287+ solve
2288+ focus t'; q unq t
2289+reflectBinderQuotePattern q unq (Pi _ t k)
2290+ = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2291+ k' <- claimTT (sMN 0 "k"); movelast k';
2292+ fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2293+ solve
2294+ focus t'; q unq t
2295+reflectBinderQuotePattern q unq (Let x y)
2296+ = do x' <- claimTT (sMN 0 "ty"); movelast x';
2297+ y' <- claimTT (sMN 0 "v"); movelast y';
2298+ fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2299+ solve
2300+ focus x'; q unq x
2301+ focus y'; q unq y
2302+reflectBinderQuotePattern q unq (NLet x y)
2303+ = do x' <- claimTT (sMN 0 "ty"); movelast x'
2304+ y' <- claimTT (sMN 0 "v"); movelast y'
2305+ fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2306+ solve
2307+ focus x'; q unq x
2308+ focus y'; q unq y
2309+reflectBinderQuotePattern q unq (Hole t)
2310+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2311+ fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2312+ solve
2313+ focus t'; q unq t
2314+reflectBinderQuotePattern q unq (GHole _ t)
2315+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2316+ fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2317+ solve
2318+ focus t'; q unq t
2319+reflectBinderQuotePattern q unq (Guess x y)
2320+ = do x' <- claimTT (sMN 0 "ty"); movelast x'
2321+ y' <- claimTT (sMN 0 "v"); movelast y'
2322+ fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2323+ solve
2324+ focus x'; q unq x
2325+ focus y'; q unq y
2326+reflectBinderQuotePattern q unq (PVar t)
2327+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2328+ fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2329+ solve
2330+ focus t'; q unq t
2331+reflectBinderQuotePattern q unq (PVTy t)
2332+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2333+ fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2334+ solve
2335+ focus t'; q unq t
2336+
22682337reflectUniverse :: Universe -> Raw
22692338reflectUniverse u =
22702339 (Var (reflm (case u of