@@ -1,5 +1,5 @@
11{-# LANGUAGE PatternGuards, ViewPatterns #-}
2−
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
33module Idris.ElabTerm where
44
55import Idris.AbsSyntax
@@ -400,6 +400,7 @@ elab ist info emode opts fn tm
400400 where -- if none work, take the error from the first
401401 trySeq (x : xs) = let e1 = elab' ina fc x in
402402 try' e1 (trySeq' e1 xs) True
403+ trySeq [] = fail "Nothing to try in sequence"
403404 trySeq' deferr [] = proofFail deferr
404405 trySeq' deferr (x : xs)
405406 = try' (do elab' ina fc x
@@ -526,7 +527,8 @@ elab ist info emode opts fn tm
526527 -- HACK: If the name leaks into its type, it may leak out of
527528 -- scope outside, so substitute in the outer scope.
528529 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))
530532 solve
531533 elab' ina _ (PGoal fc r n sc) = do
532534 rty <- goal
@@ -935,7 +937,7 @@ elab ist info emode opts fn tm
935937 elab' ina fc (PUnifyLog t) = do unifyLog True
936938 elab' ina fc t
937939 unifyLog False
938− elab' ina fc (PQuasiquote t goal) -- TODO: goal type
940+ elab' ina fc (PQuasiquote t goal)
939941 = do -- First extract the unquoted subterms, replacing them with fresh
940942 -- names in the quasiquoted term. Claim their reflections to be
941943 -- of type TT.
@@ -997,9 +999,14 @@ elab ist info emode opts fn tm
997999 Just q -> do ctxt <- get_context
9981000 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
9991001 if pattern
1000− then reflectQuotePattern unquoteNames q'
1001− else do fill $ reflectQuote 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
1006+ (fill $ reflectRawQuote unquoteNames (forget q'))
1007+ True -- ignore errors like proof search does
10021008 solve
1009+
10031010 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
10041011
10051012 -- Finally fill in the terms or patterns from the unquotes. This
@@ -1066,6 +1073,7 @@ elab ist info emode opts fn tm
10661073 findScr [(n, (_, t))] = [(n, (True, t))]
10671074 findScr (x : xs) = x : findScr xs
10681075 -- [] can't happen since scrutinee is in the environment!
1076+ findScr [] = error "The impossible happened - the scrutinee was not in the environment"
10691077
10701078 -- To make sure top level pattern name remains in scope, put
10711079 -- it at the end of the environment
@@ -1227,7 +1235,8 @@ elab ist info emode opts fn tm
12271235 lift (tfail (elaboratingArgErr while' e))
12281236 put newState
12291237 return result
1230−
1238+ elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
1239+ fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
12311240
12321241-- For every alternative, look at the function at the head. Automatically resolve
12331242-- any nested alternatives where that function is also at the head
@@ -1405,6 +1414,7 @@ resTC' tcs defaultOn depth topg fn ist
14051414 let imps = case lookupCtxtName n (idris_implicits ist) of
14061415 [] -> []
14071416 [args] -> map isImp (snd args) -- won't be overloaded!
1417+ xs -> error "The impossible happened - overloading is not expected here!"
14081418 ps <- get_probs
14091419 tm <- get_term
14101420 args <- map snd <$> try' (apply (Var n) imps)
@@ -2063,6 +2073,7 @@ reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
20632073reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
20642074reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
20652075 (reifyNativeTy nt)
2076+reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
20662077
20672078reifyTTUExp :: Term -> ElabD UExp
20682079reifyTTUExp t@(App _ _)
@@ -2079,7 +2090,11 @@ reflCall funName args
20792090
20802091-- | Lift a term into its Language.Reflection.TT representation
20812092reflect :: Term -> Raw
2082−reflect = reflectQuote []
2093+reflect = reflectTTQuote []
2094+
2095+-- | Lift a term into its Language.Reflection.Raw representation
2096+reflectRaw :: Raw -> Raw
2097+reflectRaw = reflectRawQuote []
20832098
20842099claimTT :: Name -> ElabD Name
20852100claimTT n = do n' <- getNameFrom n
@@ -2090,8 +2105,8 @@ claimTT n = do n' <- getNameFrom n
20902105-- In particular, the less-interesting bits are elaborated to _ patterns. This
20912106-- happens to NameTypes, universe levels, names that are bound but not used,
20922107-- and the type annotation field of the P constructor.
2093−reflectQuotePattern :: [Name] -> Term -> ElabD ()
2094−reflectQuotePattern unq (P _ n _)
2108+reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
2109+reflectTTQuotePattern unq (P _ n _)
20952110 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
20962111 do fill (Var n) ; solve
20972112 | otherwise =
@@ -2105,10 +2120,10 @@ reflectQuotePattern unq (P _ n _)
21052120 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
21062121 solve
21072122 focus n'; reflectNameQuotePattern n
2108−reflectQuotePattern unq (V n)
2123+reflectTTQuotePattern unq (V n)
21092124 = do fill $ reflCall "V" [RConstant (I n)]
21102125 solve
2111−reflectQuotePattern unq (Bind n b x)
2126+reflectTTQuotePattern unq (Bind n b x)
21122127 = do x' <- claimTT (sMN 0 "sc")
21132128 movelast x'
21142129 b' <- getNameFrom (sMN 0 "binder")
@@ -2128,7 +2143,7 @@ reflectQuotePattern unq (Bind n b x)
21282143 Var b',
21292144 Var x']
21302145 solve
2131− focus x'; reflectQuotePattern unq x
2146+ focus x'; reflectTTQuotePattern unq x
21322147 focus b'; reflectBinderQuotePattern unq b
21332148
21342149 where
@@ -2137,102 +2152,136 @@ reflectQuotePattern unq (Bind n b x)
21372152 = do t' <- claimTT (sMN 0 "ty"); movelast t'
21382153 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
21392154 solve
2140− focus t'; reflectQuotePattern unq t
2155+ focus t'; reflectTTQuotePattern unq t
21412156 reflectBinderQuotePattern unq (Pi _ t k)
21422157 = do t' <- claimTT (sMN 0 "ty") ; movelast t'
21432158 k' <- claimTT (sMN 0 "k"); movelast k';
21442159 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
21452160 solve
2146− focus t'; reflectQuotePattern unq t
2161+ focus t'; reflectTTQuotePattern unq t
21472162 reflectBinderQuotePattern unq (Let x y)
21482163 = do x' <- claimTT (sMN 0 "ty"); movelast x';
21492164 y' <- claimTT (sMN 0 "v"); movelast y';
21502165 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
21512166 solve
2152− focus x'; reflectQuotePattern unq x
2153− focus y'; reflectQuotePattern unq y
2167+ focus x'; reflectTTQuotePattern unq x
2168+ focus y'; reflectTTQuotePattern unq y
21542169 reflectBinderQuotePattern unq (NLet x y)
21552170 = do x' <- claimTT (sMN 0 "ty"); movelast x'
21562171 y' <- claimTT (sMN 0 "v"); movelast y'
21572172 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
21582173 solve
2159− focus x'; reflectQuotePattern unq x
2160− focus y'; reflectQuotePattern unq y
2174+ focus x'; reflectTTQuotePattern unq x
2175+ focus y'; reflectTTQuotePattern unq y
21612176 reflectBinderQuotePattern unq (Hole t)
21622177 = do t' <- claimTT (sMN 0 "ty"); movelast t'
21632178 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
21642179 solve
2165− focus t'; reflectQuotePattern unq t
2180+ focus t'; reflectTTQuotePattern unq t
21662181 reflectBinderQuotePattern unq (GHole _ t)
21672182 = do t' <- claimTT (sMN 0 "ty"); movelast t'
21682183 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
21692184 solve
2170− focus t'; reflectQuotePattern unq t
2185+ focus t'; reflectTTQuotePattern unq t
21712186 reflectBinderQuotePattern unq (Guess x y)
21722187 = do x' <- claimTT (sMN 0 "ty"); movelast x'
21732188 y' <- claimTT (sMN 0 "v"); movelast y'
21742189 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
21752190 solve
2176− focus x'; reflectQuotePattern unq x
2177− focus y'; reflectQuotePattern unq y
2191+ focus x'; reflectTTQuotePattern unq x
2192+ focus y'; reflectTTQuotePattern unq y
21782193 reflectBinderQuotePattern unq (PVar t)
21792194 = do t' <- claimTT (sMN 0 "ty"); movelast t'
21802195 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
21812196 solve
2182− focus t'; reflectQuotePattern unq t
2197+ focus t'; reflectTTQuotePattern unq t
21832198 reflectBinderQuotePattern unq (PVTy t)
21842199 = do t' <- claimTT (sMN 0 "ty"); movelast t'
21852200 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
21862201 solve
2187− focus t'; reflectQuotePattern unq t
2188−reflectQuotePattern unq (App f x)
2202+ focus t'; reflectTTQuotePattern unq t
2203+reflectTTQuotePattern unq (App f x)
21892204 = do f' <- claimTT (sMN 0 "f"); movelast f'
21902205 x' <- claimTT (sMN 0 "x"); movelast x'
21912206 fill $ reflCall "App" [Var f', Var x']
21922207 solve
2193− focus f'; reflectQuotePattern unq f
2194− focus x'; reflectQuotePattern unq x
2195−reflectQuotePattern unq (Constant c)
2208+ focus f'; reflectTTQuotePattern unq f
2209+ focus x'; reflectTTQuotePattern unq x
2210+reflectTTQuotePattern unq (Constant c)
21962211 = do fill $ reflCall "TConst" [reflectConstant c]
21972212 solve
2198−reflectQuotePattern unq (Proj t i)
2213+reflectTTQuotePattern unq (Proj t i)
21992214 = do t' <- claimTT (sMN 0 "t"); movelast t'
22002215 fill $ reflCall "Proj" [Var t', RConstant (I i)]
22012216 solve
2202− focus t'; reflectQuotePattern unq t
2203−reflectQuotePattern unq (Erased)
2217+ focus t'; reflectTTQuotePattern unq t
2218+reflectTTQuotePattern unq (Erased)
22042219 = do erased <- claimTT (sMN 0 "erased")
22052220 movelast erased
22062221 fill $ (Var erased)
22072222 solve
2208−reflectQuotePattern unq (Impossible)
2223+reflectTTQuotePattern unq (Impossible)
22092224 = do fill $ Var (reflm "Impossible")
22102225 solve
2211−reflectQuotePattern unq (TType exp)
2226+reflectTTQuotePattern unq (TType exp)
22122227 = do ue <- getNameFrom (sMN 0 "uexp")
22132228 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
22142229 movelast ue
22152230 fill $ reflCall "TType" [Var ue]
22162231 solve
2232+reflectTTQuotePattern unq (UType u)
2233+ = do uH <- getNameFrom (sMN 0 "someUniv")
2234+ claim uH (Var (reflm "Universe"))
2235+ movelast uH
2236+ fill $ reflCall "UType" [Var uH]
2237+ solve
2238+ focus uH
2239+ fill (Var (reflm (case u of
2240+ NullType -> "NullType"
2241+ UniqueType -> "UniqueType"
2242+ AllTypes -> "AllTypes")))
2243+ solve
2244+
2245+reflectUniverse :: Universe -> Raw
2246+reflectUniverse u =
2247+ (Var (reflm (case u of
2248+ NullType -> "NullType"
2249+ UniqueType -> "UniqueType"
2250+ AllTypes -> "AllTypes")))
22172251
2218−-- | Create a reflected term, but leave refs to the provided name intact
2219−reflectQuote :: [Name] -> Term -> Raw
2220−reflectQuote unq (P nt n t)
2252+-- | Create a reflected TT term, but leave refs to the provided name intact
2253+reflectTTQuote :: [Name] -> Term -> Raw
2254+reflectTTQuote unq (P nt n t)
22212255 | n `elem` unq = Var n
2222− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
2223−reflectQuote unq (V n)
2256+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2257+reflectTTQuote unq (V n)
22242258 = reflCall "V" [RConstant (I n)]
2225−reflectQuote unq (Bind n b x)
2226− = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]
2227−reflectQuote unq (App f x)
2228− = reflCall "App" [reflectQuote unq f, reflectQuote unq x]
2229−reflectQuote unq (Constant c)
2259+reflectTTQuote unq (Bind n b x)
2260+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]
2261+reflectTTQuote unq (App f x)
2262+ = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2263+reflectTTQuote unq (Constant c)
22302264 = reflCall "TConst" [reflectConstant c]
2231−reflectQuote unq (Proj t i)
2232− = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
2233−reflectQuote unq (Erased) = Var (reflm "Erased")
2234−reflectQuote unq (Impossible) = Var (reflm "Impossible")
2235−reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2265+reflectTTQuote unq (Proj t i)
2266+ = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2267+reflectTTQuote unq (Erased) = Var (reflm "Erased")
2268+reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2269+reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2270+reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
2271+
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]
22362285
22372286reflectNameType :: NameType -> Raw
22382287reflectNameType (Bound) = Var (reflm "Bound")
@@ -2283,27 +2332,27 @@ reflectNameQuotePattern _ -- for all other names, match any
22832332 solve
22842333
22852334reflectBinder :: Binder Term -> Raw
2286−reflectBinder = reflectBinderQuote []
2287−
2288−reflectBinderQuote :: [Name] -> Binder Term -> Raw
2289−reflectBinderQuote unq (Lam t)
2290− = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
2291−reflectBinderQuote unq (Pi _ t k)
2292− = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]
2293−reflectBinderQuote unq (Let x y)
2294− = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2295−reflectBinderQuote unq (NLet x y)
2296− = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2297−reflectBinderQuote unq (Hole t)
2298− = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
2299−reflectBinderQuote unq (GHole _ t)
2300− = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
2301−reflectBinderQuote unq (Guess x y)
2302− = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2303−reflectBinderQuote unq (PVar t)
2304− = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
2305−reflectBinderQuote unq (PVTy t)
2306− = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
2335+reflectBinder = reflectBinderQuote reflectTTQuote []
2336+
2337+reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw
2338+reflectBinderQuote q unq (Lam t)
2339+ = reflCall "Lam" [Var (reflm "TT"), q unq t]
2340+reflectBinderQuote q unq (Pi _ t k)
2341+ = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]
2342+reflectBinderQuote q unq (Let x y)
2343+ = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]
2344+reflectBinderQuote q unq (NLet x y)
2345+ = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]
2346+reflectBinderQuote q unq (Hole t)
2347+ = reflCall "Hole" [Var (reflm "TT"), q unq t]
2348+reflectBinderQuote q unq (GHole _ t)
2349+ = reflCall "GHole" [Var (reflm "TT"), q unq t]
2350+reflectBinderQuote q unq (Guess x y)
2351+ = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]
2352+reflectBinderQuote q unq (PVar t)
2353+ = reflCall "PVar" [Var (reflm "TT"), q unq t]
2354+reflectBinderQuote q unq (PVTy t)
2355+ = reflCall "PVTy" [Var (reflm "TT"), q unq t]
23072356
23082357mkList :: Raw -> [Raw] -> Raw
23092358mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
@@ -2343,7 +2392,8 @@ reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")
23432392reflectConstant BufferType = Var (reflm "BufferType")
23442393reflectConstant VoidType = Var (reflm "VoidType")
23452394reflectConstant Forgot = Var (reflm "Forgot")
2346−
2395+reflectConstant WorldType = Var (reflm "WorldType")
2396+reflectConstant TheWorld = Var (reflm "TheWorld")
23472397
23482398reflectUExp :: UExp -> Raw
23492399reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]