@@ -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
@@ -164,13 +164,14 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
164164getUnmatchable ctxt n = []
165165
166166data ElabCtxt = ElabCtxt { e_inarg :: Bool,
167+ e_isfn :: Bool, -- ^ Function part of application
167168 e_guarded :: Bool,
168169 e_intype :: Bool,
169170 e_qq :: Bool,
170171 e_nomatching :: Bool -- ^ can't pattern match
171172 }
172173
173−initElabCtxt = ElabCtxt False False False False False
174+initElabCtxt = ElabCtxt False False False False False False
174175
175176goal_polymorphic :: ElabD Bool
176177goal_polymorphic =
@@ -244,7 +245,7 @@ elab ist info emode opts fn tm
244245 then solveAuto ist fn False a
245246 else return ()) as
246247
247− itm <- if not pattern then insertImpLam t else return t
248+ itm <- if not pattern then insertImpLam ina t else return t
248249 ct <- insertCoerce ina itm
249250 t' <- insertLazy ct
250251 g <- goal
@@ -308,7 +309,7 @@ elab ist info emode opts fn tm
308309 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
309310 && isTypeConst c
310311 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
311− | pattern && not reflection && e_nomatching ina
312+ | pattern && not reflection && not (e_qq ina) && e_nomatching ina
312313 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
313314 | otherwise = do apply (RConstant c) []; solve
314315 elab' ina fc (PQuote r) = do fill r; solve
@@ -317,6 +318,7 @@ elab ist info emode opts fn tm
317318 g <- goal
318319 case g of
319320 TType _ -> elab' ina (Just fc) (PRef fc unitTy)
321+ UType _ -> elab' ina (Just fc) (PRef fc unitTy)
320322 _ -> elab' ina (Just fc) (PRef fc unitCon)
321323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
322324 = do g <- goal; resolveTC False 5 g fn ist
@@ -352,13 +354,32 @@ elab ist info emode opts fn tm
352354 elab' ina _ (PPair fc _ l r)
353355 = do hnf_compute
354356 g <- goal
357+ let (tc, _) = unApply g
355358 case g of
356359 TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
357360 [pexp l,pexp r])
358− _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
361+ UType _ -> elab' ina (Just fc) (PApp fc (PRef fc upairTy)
362+ [pexp l,pexp r])
363+ _ -> case tc of
364+ P _ n _ | n == upairTy
365+ -> elab' ina (Just fc) (PApp fc (PRef fc upairCon)
366+ [pimp (sUN "A") Placeholder False,
367+ pimp (sUN "B") Placeholder False,
368+ pexp l, pexp r])
369+ _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
359370 [pimp (sUN "A") Placeholder False,
360371 pimp (sUN "B") Placeholder False,
361372 pexp l, pexp r])
373+-- _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon)
374+-- [pimp (sUN "A") Placeholder False,
375+-- pimp (sUN "B") Placeholder False,
376+-- pexp l, pexp r]))
377+-- (elab' ina (Just fc) (PApp fc (PRef fc upairCon)
378+-- [pimp (sUN "A") Placeholder False,
379+-- pimp (sUN "B") Placeholder False,
380+-- pexp l, pexp r]))
381+-- True
382+
362383 elab' ina _ (PDPair fc p l@(PRef _ n) t r)
363384 = case t of
364385 Placeholder ->
@@ -399,6 +420,7 @@ elab ist info emode opts fn tm
399420 where -- if none work, take the error from the first
400421 trySeq (x : xs) = let e1 = elab' ina fc x in
401422 try' e1 (trySeq' e1 xs) True
423+ trySeq [] = fail "Nothing to try in sequence"
402424 trySeq' deferr [] = proofFail deferr
403425 trySeq' deferr (x : xs)
404426 = try' (do elab' ina fc x
@@ -411,7 +433,7 @@ elab ist info emode opts fn tm
411433 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
412434 && isTConName n (tt_ctxt ist)
413435 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
414− | pattern && not reflection && e_nomatching ec
436+ | pattern && not reflection && not (e_qq ec) && e_nomatching ec
415437 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
416438 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
417439 = do let ina = e_inarg ec
@@ -439,7 +461,7 @@ elab ist info emode opts fn tm
439461 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
440462 && isTConName n (tt_ctxt ist)
441463 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
442− | pattern && not reflection && e_nomatching ina
464+ | pattern && not reflection && not (e_qq ina) && e_nomatching ina
443465 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
444466 | otherwise =
445467 do fty <- get_type (Var n) -- check for implicits
@@ -525,7 +547,8 @@ elab ist info emode opts fn tm
525547 -- HACK: If the name leaks into its type, it may leak out of
526548 -- scope outside, so substitute in the outer scope.
527549 expandLet n (case lookup n env of
528− Just (Let t v) -> v)
550+ Just (Let t v) -> v
551+ other -> error ("Value not a let binding: " ++ show other))
529552 solve
530553 elab' ina _ (PGoal fc r n sc) = do
531554 rty <- goal
@@ -596,17 +619,13 @@ elab ist info emode opts fn tm
596619 _ -> lift $ tfail (NoSuchVariable fn)
597620 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
598621 solve
599− -- This isn't a sound way of checking for Typecase - we need a
600− -- better way!
601−-- elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')
602−-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq
603−-- = lift $ tfail (Msg "Typecase is not allowed")
604622 -- if f is local, just do a simple_app
605− elab' ina _ tm@(PApp fc (PRef _ f) args_in)
606− | pattern && not reflection && e_nomatching ina
623+ -- FIXME: Anyone feel like refactoring this mess? - EB
624+ elab' ina topfc tm@(PApp fc (PRef _ f) args_in)
625+ | pattern && not reflection && not (e_qq ina) && e_nomatching ina
607626 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
608− | otherwise
609− = do env <- get_env
627+ | otherwise = implicitApp $
628+ do env <- get_env
610629 ty <- goal
611630 fty <- get_type (Var f)
612631 ctxt <- get_context
@@ -614,18 +633,18 @@ elab ist info emode opts fn tm
614633 let unmatchableArgs = if pattern
615634 then getUnmatchable (tt_ctxt ist) f
616635 else []
617− -- Dot it if we're in a pattern and it isn't a constructor
618−-- when (pattern && not (isDConName f ctxt) && f /= fn) $ dotterm
619−
636+-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
620637 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
621638 && isTConName f (tt_ctxt ist)) $
622639 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
623640 if (f `elem` map fst env && length args == 1 && length args_in == 1)
624641 then -- simple app, as below
625− do simple_app False (elabE ina (Just fc) (PRef fc f))
642+ do simple_app False
643+ (elabE (ina { e_isfn = True }) (Just fc) (PRef fc f))
626644 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
627645 (show tm)
628646 solve
647+ return []
629648 else
630649 do ivs <- get_instances
631650 ps <- get_probs
@@ -656,22 +675,58 @@ elab ist info emode opts fn tm
656675 (zip ns' (unmatchableArgs ++ repeat False))
657676 (f == sUN "Force")
658677 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
659− solve
660− ivs' <- get_instances
661− -- Attempt to resolve any type classes which have 'complete' types,
662− -- i.e. no holes in them
663− when (not pattern || (e_inarg ina && not tcgen &&
664− not (e_guarded ina))) $
665− mapM_ (\n -> do focus n
666− g <- goal
667− env <- get_env
668− hs <- get_holes
669− if all (\n -> not (n `elem` hs)) (freeNames g)
670− then try (resolveTC False 7 g fn ist)
671− (movelast n)
672− else movelast n)
673− (ivs' \\ ivs)
674− where -- normal < alternatives < lambdas < rewrites < tactic < default tactic
678+ imp <- if (e_isfn ina) then
679+ do guess <- get_guess
680+ gty <- get_type (forget guess)
681+ env <- get_env
682+ let ty_n = normalise ctxt env gty
683+ return $ getReqImps ty_n
684+ else return []
685+ -- Now we find out how many implicits we needed at the
686+ -- end of the application by looking at the goal again
687+ -- - Have another go, but this time add the
688+ -- implicits (can't think of a better way than this...)
689+ case imp of
690+ rs@(_:_) | not pattern -> return rs -- quit, try again
691+ _ -> do solve
692+ hs <- get_holes
693+ ivs' <- get_instances
694+ -- Attempt to resolve any type classes which have 'complete' types,
695+ -- i.e. no holes in them
696+ when (not pattern || (e_inarg ina && not tcgen &&
697+ not (e_guarded ina))) $
698+ mapM_ (\n -> do focus n
699+ g <- goal
700+ env <- get_env
701+ hs <- get_holes
702+ if all (\n -> not (n `elem` hs)) (freeNames g)
703+ then try (resolveTC False 7 g fn ist)
704+ (movelast n)
705+ else movelast n)
706+ (ivs' \\ ivs)
707+ return []
708+ where
709+ -- Run the elaborator, which returns how many implicit
710+ -- args were needed, then run it again with those args. We need
711+ -- this because we have to elaborate the whole application to
712+ -- find out whether any computations have caused more implicits
713+ -- to be needed.
714+ implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
715+ implicitApp elab
716+ | pattern = do elab; return ()
717+ | otherwise
718+ = do s <- get
719+ imps <- elab
720+ case imps of
721+ [] -> return ()
722+ es -> do put s
723+ elab' ina topfc (PAppImpl tm es)
724+
725+ getReqImps (Bind x (Pi (Just i) ty _) sc)
726+ = i : getReqImps sc
727+ getReqImps _ = []
728+
729+ -- normal < alternatives < lambdas < rewrites < tactic < default tactic
675730 -- reason for lambdas after alternatives is that having
676731 -- the alternative resolved can help with typechecking the lambda
677732 -- or the rewrite. Rewrites/tactics need as much information
@@ -744,15 +799,24 @@ elab ist info emode opts fn tm
744799 setInjective (PApp _ (PRef _ n) _) = setinj n
745800 setInjective _ = return ()
746801
747− elab' ina _ tm@(PApp fc f [arg])
748− = erun fc $
802+ elab' ina _ tm@(PApp fc f [arg]) =
803+ erun fc $
749804 do simple_app (not $ headRef f)
750− (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
805+ (elabE (ina { e_isfn = True }) (Just fc) f)
806+ (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
751807 (show tm)
752808 solve
753809 where headRef (PRef _ _) = True
754810 headRef (PApp _ f _) = headRef f
755811 headRef _ = False
812+
813+ elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...
814+ solve
815+ where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits
816+ appImpl (e : es) = simple_app False
817+ (appImpl es)
818+ (elab' ina fc Placeholder)
819+ (show f)
756820 elab' ina fc Placeholder
757821 = do (h : hs) <- get_holes
758822 movelast h
@@ -826,9 +890,21 @@ elab ist info emode opts fn tm
826890 envU <- mapM (getKind args) args
827891 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
828892
829− -- Drop the unique arguments used in the scrutinee (since it's
830− -- not valid to use them again anyway)
831− let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr)
893+ -- Drop the unique arguments used in the term already
894+ -- and in the scrutinee (since it's
895+ -- not valid to use them again anyway)
896+ --
897+ -- Also drop unique arguments which don't appear explicitly
898+ -- in either case branch so they don't count as used
899+ -- unnecessarily (can only do this for unique things, since we
900+ -- assume they don't appear implicitly in types)
901+ ptm <- get_term
902+ let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
903+
904+ let argsDropped = filter (isUnique envU)
905+ (nub $ allNamesIn scr ++ inApp ptm ++
906+ inOpts)
907+
832908 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
833909
834910 cname <- unique_hole' True (mkCaseName fn)
@@ -855,6 +931,13 @@ elab ist info emode opts fn tm
855931 Just xs@(_:_) -> sNS n xs
856932 _ -> n
857933
934+ inApp (P _ n _) = [n]
935+ inApp (App f a) = inApp f ++ inApp a
936+ inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
937+ inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc
938+ inApp (Bind n b sc) = inApp sc
939+ inApp _ = []
940+
858941 isUnique envk n = case lookup n envk of
859942 Just u -> u
860943 _ -> False
@@ -882,13 +965,16 @@ elab ist info emode opts fn tm
882965 elab' ina fc (PUnifyLog t) = do unifyLog True
883966 elab' ina fc t
884967 unifyLog False
885− elab' ina fc (PQuasiquote t goal) -- TODO: goal type
968+ elab' ina fc (PQuasiquote t goal)
886969 = do -- First extract the unquoted subterms, replacing them with fresh
887970 -- names in the quasiquoted term. Claim their reflections to be
888− -- of type TT.
971+ -- an inferred type (to support polytypic quasiquotes).
889972 (t, unq) <- extractUnquotes 0 t
890973 let unquoteNames = map fst unq
891− mapM_ (flip claim (Var tt)) unquoteNames
974+ mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")
975+ claim uqh RType
976+ movelast uqh
977+ claim uqn (Var uqh)) unquoteNames
892978
893979
894980 -- Save the old state - we need a fresh proof state to avoid
@@ -897,7 +983,7 @@ elab ist info emode opts fn tm
897983 saveState
898984 updatePS (const .
899985 newProof (sMN 0 "q") ctxt $
900− P Ref tt Erased)
986+ P Ref (reflm "TT") Erased)
901987
902988 -- Re-add the unquotes, letting Idris infer the (fictional)
903989 -- types. Here, they represent the real type rather than the type
@@ -944,18 +1030,22 @@ elab ist info emode opts fn tm
9441030 Just q -> do ctxt <- get_context
9451031 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
9461032 if pattern
947− then reflectQuotePattern unquoteNames q'
948− else do fill $ reflectQuote unquoteNames q'
1033+ then do try' (reflectTTQuotePattern unquoteNames q')
1034+ (reflectRawQuotePattern unquoteNames (forget q'))
1035+ True
1036+ else do try' (fill $ reflectTTQuote unquoteNames q')
1037+ -- we forget q' instead of using q to ensure rechecking
1038+ (fill $ reflectRawQuote unquoteNames (forget q'))
1039+ True -- ignore errors like proof search does
9491040 solve
1041+
9501042 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
9511043
9521044 -- Finally fill in the terms or patterns from the unquotes. This
9531045 -- happens last so that their holes still exist while elaborating
9541046 -- the main quotation.
9551047 mapM_ elabUnquote unq
956− where tt = sNS (sUN "TT") ["Reflection", "Language"]
957−
958− elabUnquote (n, tm)
1048+ where elabUnquote (n, tm)
9591049 = do focus n
9601050 elabE (ina { e_qq = False }) fc tm
9611051
@@ -976,6 +1066,20 @@ elab ist info emode opts fn tm
9761066 delayElab $ do focus h
9771067 dotterm
9781068 elab' ina fc t
1069+ elab' ina _ (PRunTactics fc tm) =
1070+ do attack
1071+ n <- getNameFrom (sMN 0 "tacticScript")
1072+ n' <- getNameFrom (sMN 0 "tacticExpr")
1073+ let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)
1074+ claim n scriptTy
1075+ movelast n
1076+ letbind n' scriptTy (Var n)
1077+ focus n
1078+ elab' ina (Just fc) tm
1079+ env <- get_env
1080+ ctxt <- get_context
1081+ runTactical fc ctxt env (P Bound n' Erased)
1082+ solve
9791083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
9801084
9811085 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
@@ -999,6 +1103,7 @@ elab ist info emode opts fn tm
9991103 findScr [(n, (_, t))] = [(n, (True, t))]
10001104 findScr (x : xs) = x : findScr xs
10011105 -- [] can't happen since scrutinee is in the environment!
1106+ findScr [] = error "The impossible happened - the scrutinee was not in the environment"
10021107
10031108 -- To make sure top level pattern name remains in scope, put
10041109 -- it at the end of the environment
@@ -1072,16 +1177,20 @@ elab ist info emode opts fn tm
10721177 = x : insertScopedImps fc sc xs
10731178 insertScopedImps _ _ xs = xs
10741179
1075− insertImpLam t =
1180+ insertImpLam ina t =
10761181 do ty <- goal
10771182 env <- get_env
10781183 let ty' = normalise (tt_ctxt ist) env ty
10791184 addLam ty' t
10801185 where
10811186 -- just one level at a time
1082− addLam (Bind n (Pi (Just _) _ _) sc) t
1083− = do impn <- unique_hole (sMN 0 "imp")
1084− return (PLam emptyFC impn Placeholder t)
1187+ addLam (Bind n (Pi (Just _) _ _) sc) t =
1188+ do impn <- unique_hole (sMN 0 "imp")
1189+ if e_isfn ina -- apply to an implicit immediately
1190+ then return (PApp emptyFC
1191+ (PLam emptyFC impn Placeholder t)
1192+ [pexp Placeholder])
1193+ else return (PLam emptyFC impn Placeholder t)
10851194 addLam _ t = return t
10861195
10871196 insertCoerce ina t@(PCase _ _ _) = return t
@@ -1156,7 +1265,8 @@ elab ist info emode opts fn tm
11561265 lift (tfail (elaboratingArgErr while' e))
11571266 put newState
11581267 return result
1159−
1268+ elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
1269+ fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
11601270
11611271-- For every alternative, look at the function at the head. Automatically resolve
11621272-- any nested alternatives where that function is also at the head
@@ -1334,6 +1444,7 @@ resTC' tcs defaultOn depth topg fn ist
13341444 let imps = case lookupCtxtName n (idris_implicits ist) of
13351445 [] -> []
13361446 [args] -> map isImp (snd args) -- won't be overloaded!
1447+ xs -> error "The impossible happened - overloading is not expected here!"
13371448 ps <- get_probs
13381449 tm <- get_term
13391450 args <- map snd <$> try' (apply (Var n) imps)
@@ -1394,6 +1505,86 @@ case_ ind autoSolve ist fn tm = do
13941505 else casetac (forget val)
13951506 when autoSolve solveAll
13961507
1508+runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1509+runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1510+ where
1511+ eval = normaliseAll ctxt env
1512+ tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1513+ returnUnit = fmap fst $ get_type_val (Var unitCon)
1514+
1515+ -- | Do a step in the reflected elaborator monad. The input is the
1516+ -- step, the output is the (reflected) term returned.
1517+ runTacTm :: Term -> ElabD Term
1518+ runTacTm (unApply -> tac@(P _ n _, args))
1519+ | n == tacN "prim__Solve", [] <- args
1520+ = do solve
1521+ returnUnit
1522+ | n == tacN "prim__Goal", [] <- args
1523+ = do (h:_) <- get_holes
1524+ t <- goal
1525+ fmap fst . get_type_val $
1526+ rawPair (Var (reflm "TTName"), Var (reflm "TT"))
1527+ (reflectName h, reflect t)
1528+ | n == tacN "prim__Holes", [] <- args
1529+ = do hs <- get_holes
1530+ fmap fst . get_type_val $
1531+ mkList (Var $ reflm "TTName") (map reflectName hs)
1532+ | n == tacN "prim__Guess", [] <- args
1533+ = do ok <- is_guess
1534+ if ok
1535+ then do guess <- fmap forget get_guess
1536+ fmap fst . get_type_val $
1537+ RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1538+ (Var (reflm "TT")))
1539+ guess
1540+ else fmap fst . get_type_val $
1541+ RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1542+ (Var (reflm "TT"))
1543+ | n == tacN "prim__Env", [] <- args
1544+ = do env <- get_env
1545+ fmap fst . get_type_val $ reflectEnv env
1546+ | n == tacN "prim__Fail", [_a, errs] <- args
1547+ = do parts <- reifyReportParts (eval errs)
1548+ lift . tfail $ ReflectionError [parts] (Msg "")
1549+ | n == tacN "prim__PureTactical", [_a, tm] <- args
1550+ = return tm
1551+ | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1552+ = do let first' = eval first
1553+ res <- runTacTm first'
1554+ let next = eval (App andThen res)
1555+ runTacTm next
1556+ | n == tacN "prim__Try", [_a, first, alt] <- args
1557+ = do let first' = eval first
1558+ let alt' = eval alt
1559+ try' (runTacTm first') (runTacTm alt') True
1560+ | n == tacN "prim__Fill", [raw] <- args
1561+ = do raw' <- reifyRaw raw
1562+ apply raw' []
1563+ returnUnit
1564+ | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args
1565+ = do n <- getNameFrom (sMN 0 hint)
1566+ fmap fst $ get_type_val (reflectName n)
1567+ | n == tacN "prim__Claim", [n, ty] <- args
1568+ = do n' <- reifyTTName n
1569+ ty' <- reifyRaw ty
1570+ claim n' ty'
1571+ returnUnit
1572+ | n == tacN "prim__Forget", [tt] <- args
1573+ = do tt' <- reifyTT tt
1574+ fmap fst . get_type_val $ reflect tt'
1575+ | n == tacN "prim__Attack", [] <- args
1576+ = do attack
1577+ returnUnit
1578+ | n == tacN "prim__Focus", [what] <- args
1579+ = do n' <- reifyTTName what
1580+ focus n'
1581+ returnUnit
1582+ | n == tacN "prim__Unfocus", [what] <- args
1583+ = do n' <- reifyTTName what
1584+ movelast n'
1585+ returnUnit
1586+ runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1587+
13971588-- Running tactics directly
13981589-- if a tactic adds unification problems, return an error
13991590
@@ -1460,6 +1651,12 @@ runTac autoSolve ist perhapsFC fn tac
14601651 when autoSolve solveAll
14611652 runT DoUnify = do unify_all
14621653 when autoSolve solveAll
1654+ runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal")
1655+ claim tmHole RType
1656+ claim n (Var tmHole)
1657+ focus tmHole
1658+ elab ist toplevel ERHS [] (sMN 0 "tac") tm
1659+ focus n
14631660 runT (Equiv tm) -- let bind tm, then
14641661 = do attack
14651662 tyn <- getNameFrom (sMN 0 "ety")
@@ -1520,6 +1717,10 @@ runTac autoSolve ist perhapsFC fn tac
15201717 = do proofSearch' ist rec False depth prover top fn hints
15211718 when autoSolve solveAll
15221719 runT (Focus n) = focus n
1720+ runT Unfocus = do hs <- get_holes
1721+ case hs of
1722+ [] -> return ()
1723+ (h : _) -> movelast h
15231724 runT Solve = solve
15241725 runT (Try l r) = do try' (runT l) (runT r) True
15251726 runT (TSeq l r) = do runT l; runT r
@@ -1664,6 +1865,7 @@ reify _ (P _ n _) | n == reflm "Solve" = return Solve
16641865reify _ (P _ n _) | n == reflm "Compute" = return Compute
16651866reify _ (P _ n _) | n == reflm "Skip" = return Skip
16661867reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
1868+reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
16671869reify ist t@(App _ _)
16681870 | (P _ f _, args) <- unApply t = reifyApp ist f args
16691871reify _ t = fail ("Unknown tactic " ++ show t)
@@ -1675,6 +1877,9 @@ reifyApp _ t [Constant (I i)]
16751877reifyApp _ t [x]
16761878 | t == reflm "Refine" = do n <- reifyTTName x
16771879 return $ Refine n []
1880+reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
1881+ goal <- reifyTT ty
1882+ return $ Claim n' (delab ist goal)
16781883reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
16791884reifyApp ist t [Constant (Str n), x]
16801885 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
@@ -1705,16 +1910,20 @@ reifyApp ist t [n, tt', t']
17051910 t'' <- reifyTT t'
17061911 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
17071912reifyApp ist t [errs]
1708− | t == reflm "Fail" = case unList errs of
1709− Nothing -> fail "Failed to reify errors"
1710− Just errs' ->
1711− let parts = mapM reifyReportPart errs' in
1712− case parts of
1713− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1714− Right errs'' ->
1715− return $ TFail errs''
1913+ | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
17161914reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
17171915
1916+reifyReportParts :: Term -> ElabD [ErrorReportPart]
1917+reifyReportParts errs =
1918+ case unList errs of
1919+ Nothing -> fail "Failed to reify errors"
1920+ Just errs' ->
1921+ let parts = mapM reifyReportPart errs' in
1922+ case parts of
1923+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1924+ Right errs'' ->
1925+ return errs''
1926+
17181927-- | Reify terms from their reflected representation
17191928reifyTT :: Term -> ElabD Term
17201929reifyTT t@(App _ _)
@@ -1894,6 +2103,7 @@ reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
18942103reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
18952104reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
18962105 (reifyNativeTy nt)
2106+reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
18972107
18982108reifyTTUExp :: Term -> ElabD UExp
18992109reifyTTUExp t@(App _ _)
@@ -1910,7 +2120,11 @@ reflCall funName args
19102120
19112121-- | Lift a term into its Language.Reflection.TT representation
19122122reflect :: Term -> Raw
1913−reflect = reflectQuote []
2123+reflect = reflectTTQuote []
2124+
2125+-- | Lift a term into its Language.Reflection.Raw representation
2126+reflectRaw :: Raw -> Raw
2127+reflectRaw = reflectRawQuote []
19142128
19152129claimTT :: Name -> ElabD Name
19162130claimTT n = do n' <- getNameFrom n
@@ -1921,8 +2135,8 @@ claimTT n = do n' <- getNameFrom n
19212135-- In particular, the less-interesting bits are elaborated to _ patterns. This
19222136-- happens to NameTypes, universe levels, names that are bound but not used,
19232137-- and the type annotation field of the P constructor.
1924−reflectQuotePattern :: [Name] -> Term -> ElabD ()
1925−reflectQuotePattern unq (P _ n _)
2138+reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
2139+reflectTTQuotePattern unq (P _ n _)
19262140 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
19272141 do fill (Var n) ; solve
19282142 | otherwise =
@@ -1936,10 +2150,10 @@ reflectQuotePattern unq (P _ n _)
19362150 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
19372151 solve
19382152 focus n'; reflectNameQuotePattern n
1939−reflectQuotePattern unq (V n)
2153+reflectTTQuotePattern unq (V n)
19402154 = do fill $ reflCall "V" [RConstant (I n)]
19412155 solve
1942−reflectQuotePattern unq (Bind n b x)
2156+reflectTTQuotePattern unq (Bind n b x)
19432157 = do x' <- claimTT (sMN 0 "sc")
19442158 movelast x'
19452159 b' <- getNameFrom (sMN 0 "binder")
@@ -1959,111 +2173,215 @@ reflectQuotePattern unq (Bind n b x)
19592173 Var b',
19602174 Var x']
19612175 solve
1962− focus x'; reflectQuotePattern unq x
1963− focus b'; reflectBinderQuotePattern unq b
1964−
1965− where
1966− reflectBinderQuotePattern :: [Name] -> Binder Term -> ElabD ()
1967− reflectBinderQuotePattern unq (Lam t)
1968− = do t' <- claimTT (sMN 0 "ty"); movelast t'
1969− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
1970− solve
1971− focus t'; reflectQuotePattern unq t
1972− reflectBinderQuotePattern unq (Pi _ t k)
1973− = do t' <- claimTT (sMN 0 "ty") ; movelast t'
1974− k' <- claimTT (sMN 0 "k"); movelast k';
1975− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
1976− solve
1977− focus t'; reflectQuotePattern unq t
1978− reflectBinderQuotePattern unq (Let x y)
1979− = do x' <- claimTT (sMN 0 "ty"); movelast x';
1980− y' <- claimTT (sMN 0 "v"); movelast y';
1981− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
1982− solve
1983− focus x'; reflectQuotePattern unq x
1984− focus y'; reflectQuotePattern unq y
1985− reflectBinderQuotePattern unq (NLet x y)
1986− = do x' <- claimTT (sMN 0 "ty"); movelast x'
1987− y' <- claimTT (sMN 0 "v"); movelast y'
1988− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
1989− solve
1990− focus x'; reflectQuotePattern unq x
1991− focus y'; reflectQuotePattern unq y
1992− reflectBinderQuotePattern unq (Hole t)
1993− = do t' <- claimTT (sMN 0 "ty"); movelast t'
1994− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
1995− solve
1996− focus t'; reflectQuotePattern unq t
1997− reflectBinderQuotePattern unq (GHole _ t)
1998− = do t' <- claimTT (sMN 0 "ty"); movelast t'
1999− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2000− solve
2001− focus t'; reflectQuotePattern unq t
2002− reflectBinderQuotePattern unq (Guess x y)
2003− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2004− y' <- claimTT (sMN 0 "v"); movelast y'
2005− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2006− solve
2007− focus x'; reflectQuotePattern unq x
2008− focus y'; reflectQuotePattern unq y
2009− reflectBinderQuotePattern unq (PVar t)
2010− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2011− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2012− solve
2013− focus t'; reflectQuotePattern unq t
2014− reflectBinderQuotePattern unq (PVTy t)
2015− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2016− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2017− solve
2018− focus t'; reflectQuotePattern unq t
2019−reflectQuotePattern unq (App f x)
2176+ focus x'; reflectTTQuotePattern unq x
2177+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
2178+reflectTTQuotePattern unq (App f x)
20202179 = do f' <- claimTT (sMN 0 "f"); movelast f'
20212180 x' <- claimTT (sMN 0 "x"); movelast x'
20222181 fill $ reflCall "App" [Var f', Var x']
20232182 solve
2024− focus f'; reflectQuotePattern unq f
2025− focus x'; reflectQuotePattern unq x
2026−reflectQuotePattern unq (Constant c)
2183+ focus f'; reflectTTQuotePattern unq f
2184+ focus x'; reflectTTQuotePattern unq x
2185+reflectTTQuotePattern unq (Constant c)
20272186 = do fill $ reflCall "TConst" [reflectConstant c]
20282187 solve
2029−reflectQuotePattern unq (Proj t i)
2188+reflectTTQuotePattern unq (Proj t i)
20302189 = do t' <- claimTT (sMN 0 "t"); movelast t'
20312190 fill $ reflCall "Proj" [Var t', RConstant (I i)]
20322191 solve
2033− focus t'; reflectQuotePattern unq t
2034−reflectQuotePattern unq (Erased)
2192+ focus t'; reflectTTQuotePattern unq t
2193+reflectTTQuotePattern unq (Erased)
20352194 = do erased <- claimTT (sMN 0 "erased")
20362195 movelast erased
20372196 fill $ (Var erased)
20382197 solve
2039−reflectQuotePattern unq (Impossible)
2198+reflectTTQuotePattern unq (Impossible)
20402199 = do fill $ Var (reflm "Impossible")
20412200 solve
2042−reflectQuotePattern unq (TType exp)
2201+reflectTTQuotePattern unq (TType exp)
20432202 = do ue <- getNameFrom (sMN 0 "uexp")
20442203 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
20452204 movelast ue
20462205 fill $ reflCall "TType" [Var ue]
20472206 solve
2207+reflectTTQuotePattern unq (UType u)
2208+ = do uH <- getNameFrom (sMN 0 "someUniv")
2209+ claim uH (Var (reflm "Universe"))
2210+ movelast uH
2211+ fill $ reflCall "UType" [Var uH]
2212+ solve
2213+ focus uH
2214+ fill (Var (reflm (case u of
2215+ NullType -> "NullType"
2216+ UniqueType -> "UniqueType"
2217+ AllTypes -> "AllTypes")))
2218+ solve
20482219
2049−-- | Create a reflected term, but leave refs to the provided name intact
2050−reflectQuote :: [Name] -> Term -> Raw
2051−reflectQuote unq (P nt n t)
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+
2345+reflectUniverse :: Universe -> Raw
2346+reflectUniverse u =
2347+ (Var (reflm (case u of
2348+ NullType -> "NullType"
2349+ UniqueType -> "UniqueType"
2350+ AllTypes -> "AllTypes")))
2351+
2352+-- | Create a reflected TT term, but leave refs to the provided name intact
2353+reflectTTQuote :: [Name] -> Term -> Raw
2354+reflectTTQuote unq (P nt n t)
20522355 | n `elem` unq = Var n
2053− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
2054−reflectQuote unq (V n)
2356+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2357+reflectTTQuote unq (V n)
20552358 = reflCall "V" [RConstant (I n)]
2056−reflectQuote unq (Bind n b x)
2057− = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]
2058−reflectQuote unq (App f x)
2059− = reflCall "App" [reflectQuote unq f, reflectQuote unq x]
2060−reflectQuote unq (Constant c)
2359+reflectTTQuote unq (Bind n b x)
2360+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]
2361+reflectTTQuote unq (App f x)
2362+ = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2363+reflectTTQuote unq (Constant c)
20612364 = reflCall "TConst" [reflectConstant c]
2062−reflectQuote unq (Proj t i)
2063− = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
2064−reflectQuote unq (Erased) = Var (reflm "Erased")
2065−reflectQuote unq (Impossible) = Var (reflm "Impossible")
2066−reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2365+reflectTTQuote unq (Proj t i)
2366+ = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2367+reflectTTQuote unq (Erased) = Var (reflm "Erased")
2368+reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2369+reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2370+reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
2371+
2372+reflectRawQuote :: [Name] -> Raw -> Raw
2373+reflectRawQuote unq (Var n)
2374+ | n `elem` unq = Var n
2375+ | otherwise = reflCall "Var" [reflectName n]
2376+reflectRawQuote unq (RBind n b r) =
2377+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]
2378+reflectRawQuote unq (RApp f x) =
2379+ reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
2380+reflectRawQuote unq RType = Var (reflm "RType")
2381+reflectRawQuote unq (RUType u) =
2382+ reflCall "RUType" [reflectUniverse u]
2383+reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
2384+reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
20672385
20682386reflectNameType :: NameType -> Raw
20692387reflectNameType (Bound) = Var (reflm "Bound")
@@ -2114,27 +2432,27 @@ reflectNameQuotePattern _ -- for all other names, match any
21142432 solve
21152433
21162434reflectBinder :: Binder Term -> Raw
2117−reflectBinder = reflectBinderQuote []
2118−
2119−reflectBinderQuote :: [Name] -> Binder Term -> Raw
2120−reflectBinderQuote unq (Lam t)
2121− = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
2122−reflectBinderQuote unq (Pi _ t k)
2123− = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]
2124−reflectBinderQuote unq (Let x y)
2125− = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2126−reflectBinderQuote unq (NLet x y)
2127− = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2128−reflectBinderQuote unq (Hole t)
2129− = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
2130−reflectBinderQuote unq (GHole _ t)
2131− = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
2132−reflectBinderQuote unq (Guess x y)
2133− = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2134−reflectBinderQuote unq (PVar t)
2135− = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
2136−reflectBinderQuote unq (PVTy t)
2137− = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
2435+reflectBinder = reflectBinderQuote reflectTTQuote []
2436+
2437+reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw
2438+reflectBinderQuote q unq (Lam t)
2439+ = reflCall "Lam" [Var (reflm "TT"), q unq t]
2440+reflectBinderQuote q unq (Pi _ t k)
2441+ = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]
2442+reflectBinderQuote q unq (Let x y)
2443+ = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]
2444+reflectBinderQuote q unq (NLet x y)
2445+ = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]
2446+reflectBinderQuote q unq (Hole t)
2447+ = reflCall "Hole" [Var (reflm "TT"), q unq t]
2448+reflectBinderQuote q unq (GHole _ t)
2449+ = reflCall "GHole" [Var (reflm "TT"), q unq t]
2450+reflectBinderQuote q unq (Guess x y)
2451+ = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]
2452+reflectBinderQuote q unq (PVar t)
2453+ = reflCall "PVar" [Var (reflm "TT"), q unq t]
2454+reflectBinderQuote q unq (PVTy t)
2455+ = reflCall "PVTy" [Var (reflm "TT"), q unq t]
21382456
21392457mkList :: Raw -> [Raw] -> Raw
21402458mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
@@ -2174,7 +2492,8 @@ reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")
21742492reflectConstant BufferType = Var (reflm "BufferType")
21752493reflectConstant VoidType = Var (reflm "VoidType")
21762494reflectConstant Forgot = Var (reflm "Forgot")
2177−
2495+reflectConstant WorldType = Var (reflm "WorldType")
2496+reflectConstant TheWorld = Var (reflm "TheWorld")
21782497
21792498reflectUExp :: UExp -> Raw
21802499reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]