@@ -1,5 +1,5 @@
1−{-# LANGUAGE PatternGuards #-}
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
@@ -164,13 +164,14 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
164getUnmatchable ctxt n = []
164getUnmatchable ctxt n = []
166data ElabCtxt = ElabCtxt { e_inarg :: Bool,
166data ElabCtxt = ElabCtxt { e_inarg :: Bool,
167+ e_isfn :: Bool, -- ^ Function part of application
167 e_guarded :: Bool,
168 e_guarded :: Bool,
168 e_intype :: Bool,
169 e_intype :: Bool,
169 e_qq :: Bool,
170 e_qq :: Bool,
170 e_nomatching :: Bool -- ^ can't pattern match
171 e_nomatching :: Bool -- ^ can't pattern match
173−initElabCtxt = ElabCtxt False False False False False
174+initElabCtxt = ElabCtxt False False False False False False
175goal_polymorphic :: ElabD Bool
176goal_polymorphic :: ElabD Bool
176goal_polymorphic =
177goal_polymorphic =
@@ -244,7 +245,7 @@ elab ist info emode opts fn tm
244 then solveAuto ist fn False a
245 then solveAuto ist fn False a
245 else return ()) as
246 else return ()) as
247− itm <- if not pattern then insertImpLam t else return t
248+ itm <- if not pattern then insertImpLam ina t else return t
248 ct <- insertCoerce ina itm
249 ct <- insertCoerce ina itm
249 t' <- insertLazy ct
250 t' <- insertLazy ct
250 g <- goal
251 g <- goal
@@ -308,7 +309,7 @@ elab ist info emode opts fn tm
308 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
309 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
309 && isTypeConst c
310 && isTypeConst c
310 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
311 = 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
312 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
313 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
313 | otherwise = do apply (RConstant c) []; solve
314 | otherwise = do apply (RConstant c) []; solve
314 elab' ina fc (PQuote r) = do fill r; solve
315 elab' ina fc (PQuote r) = do fill r; solve
@@ -317,6 +318,7 @@ elab ist info emode opts fn tm
317 g <- goal
318 g <- goal
318 case g of
319 case g of
319 TType _ -> elab' ina (Just fc) (PRef fc unitTy)
320 TType _ -> elab' ina (Just fc) (PRef fc unitTy)
321+ UType _ -> elab' ina (Just fc) (PRef fc unitTy)
320 _ -> elab' ina (Just fc) (PRef fc unitCon)
322 _ -> elab' ina (Just fc) (PRef fc unitCon)
321 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
322 = do g <- goal; resolveTC False 5 g fn ist
324 = do g <- goal; resolveTC False 5 g fn ist
@@ -352,13 +354,32 @@ elab ist info emode opts fn tm
352 elab' ina _ (PPair fc _ l r)
354 elab' ina _ (PPair fc _ l r)
353 = do hnf_compute
355 = do hnf_compute
354 g <- goal
356 g <- goal
357+ let (tc, _) = unApply g
355 case g of
358 case g of
356 TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
359 TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
357 [pexp l,pexp r])
360 [pexp l,pexp r])
361+ UType _ -> elab' ina (Just fc) (PApp fc (PRef fc upairTy)
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,
358− _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
369+ _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
359 [pimp (sUN "A") Placeholder False,
370 [pimp (sUN "A") Placeholder False,
360 pimp (sUN "B") Placeholder False,
371 pimp (sUN "B") Placeholder False,
361 pexp l, pexp r])
372 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,
377+-- (elab' ina (Just fc) (PApp fc (PRef fc upairCon)
378+-- [pimp (sUN "A") Placeholder False,
379+-- pimp (sUN "B") Placeholder False,
362 elab' ina _ (PDPair fc p l@(PRef _ n) t r)
383 elab' ina _ (PDPair fc p l@(PRef _ n) t r)
363 = case t of
384 = case t of
364 Placeholder ->
385 Placeholder ->
@@ -399,6 +420,7 @@ elab ist info emode opts fn tm
399 where -- if none work, take the error from the first
420 where -- if none work, take the error from the first
400 trySeq (x : xs) = let e1 = elab' ina fc x in
421 trySeq (x : xs) = let e1 = elab' ina fc x in
401 try' e1 (trySeq' e1 xs) True
422 try' e1 (trySeq' e1 xs) True
423+ trySeq [] = fail "Nothing to try in sequence"
402 trySeq' deferr [] = proofFail deferr
424 trySeq' deferr [] = proofFail deferr
403 trySeq' deferr (x : xs)
425 trySeq' deferr (x : xs)
404 = try' (do elab' ina fc x
426 = try' (do elab' ina fc x
@@ -411,7 +433,7 @@ elab ist info emode opts fn tm
411 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
433 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
412 && isTConName n (tt_ctxt ist)
434 && isTConName n (tt_ctxt ist)
413 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
435 = 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
415 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
437 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
416 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
438 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
417 = do let ina = e_inarg ec
439 = do let ina = e_inarg ec
@@ -439,7 +461,7 @@ elab ist info emode opts fn tm
439 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
461 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
440 && isTConName n (tt_ctxt ist)
462 && isTConName n (tt_ctxt ist)
441 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
463 = 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
443 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
465 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
444 | otherwise =
466 | otherwise =
445 do fty <- get_type (Var n) -- check for implicits
467 do fty <- get_type (Var n) -- check for implicits
@@ -525,7 +547,8 @@ elab ist info emode opts fn tm
525 -- HACK: If the name leaks into its type, it may leak out of
547 -- HACK: If the name leaks into its type, it may leak out of
526 -- scope outside, so substitute in the outer scope.
548 -- scope outside, so substitute in the outer scope.
527 expandLet n (case lookup n env of
549 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))
530 elab' ina _ (PGoal fc r n sc) = do
553 elab' ina _ (PGoal fc r n sc) = do
531 rty <- goal
554 rty <- goal
@@ -596,17 +619,13 @@ elab ist info emode opts fn tm
596 _ -> lift $ tfail (NoSuchVariable fn)
619 _ -> lift $ tfail (NoSuchVariable fn)
597 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
620 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
599− -- This isn't a sound way of checking for Typecase - we need a
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")
604 -- if f is local, just do a simple_app
622 -- if f is local, just do a simple_app
623+ -- FIXME: Anyone feel like refactoring this mess? - EB
605− elab' ina _ tm@(PApp fc (PRef _ f) args_in)
624+ elab' ina topfc tm@(PApp fc (PRef _ f) args_in)
606− | pattern && not reflection && e_nomatching ina
625+ | pattern && not reflection && not (e_qq ina) && e_nomatching ina
607 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
626 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
608− | otherwise
627+ | otherwise = implicitApp $
609− = do env <- get_env
628+ do env <- get_env
610 ty <- goal
629 ty <- goal
611 fty <- get_type (Var f)
630 fty <- get_type (Var f)
612 ctxt <- get_context
631 ctxt <- get_context
@@ -614,18 +633,18 @@ elab ist info emode opts fn tm
614 let unmatchableArgs = if pattern
633 let unmatchableArgs = if pattern
615 then getUnmatchable (tt_ctxt ist) f
634 then getUnmatchable (tt_ctxt ist) f
617− -- Dot it if we're in a pattern and it isn't a constructor
636+-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
618−-- when (pattern && not (isDConName f ctxt) && f /= fn) $ dotterm
620 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
637 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
621 && isTConName f (tt_ctxt ist)) $
638 && isTConName f (tt_ctxt ist)) $
622 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
639 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
623 if (f `elem` map fst env && length args == 1 && length args_in == 1)
640 if (f `elem` map fst env && length args == 1 && length args_in == 1)
624 then -- simple app, as below
641 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))
626 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
644 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
627 (show tm)
645 (show tm)
630 do ivs <- get_instances
649 do ivs <- get_instances
631 ps <- get_probs
650 ps <- get_probs
@@ -656,22 +675,58 @@ elab ist info emode opts fn tm
656 (zip ns' (unmatchableArgs ++ repeat False))
675 (zip ns' (unmatchableArgs ++ repeat False))
657 (f == sUN "Force")
676 (f == sUN "Force")
658 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
677 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
678+ imp <- if (e_isfn ina) then
679+ do guess <- get_guess
680+ gty <- get_type (forget guess)
682+ let ty_n = normalise ctxt env gty
683+ return $ getReqImps ty_n
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...)
690+ rs@(_:_) | not pattern -> return rs -- quit, try again
659− solve
691+ _ -> do solve
660− ivs' <- get_instances
693+ ivs' <- get_instances
661− -- Attempt to resolve any type classes which have 'complete' types,
694+ -- Attempt to resolve any type classes which have 'complete' types,
662− -- i.e. no holes in them
695+ -- i.e. no holes in them
663− when (not pattern || (e_inarg ina && not tcgen &&
696+ when (not pattern || (e_inarg ina && not tcgen &&
664− not (e_guarded ina))) $
697+ not (e_guarded ina))) $
665− mapM_ (\n -> do focus n
698+ mapM_ (\n -> do focus n
666− g <- goal
699+ g <- goal
667− env <- get_env
700+ env <- get_env
668− hs <- get_holes
701+ hs <- get_holes
669− if all (\n -> not (n `elem` hs)) (freeNames g)
702+ if all (\n -> not (n `elem` hs)) (freeNames g)
670− then try (resolveTC False 7 g fn ist)
703+ then try (resolveTC False 7 g fn ist)
671− (movelast n)
704+ (movelast n)
672− else movelast n)
705+ else movelast n)
673− (ivs' \\ ivs)
706+ (ivs' \\ ivs)
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
714+ implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
716+ | pattern = do elab; return ()
723+ elab' ina topfc (PAppImpl tm es)
725+ getReqImps (Bind x (Pi (Just i) ty _) sc)
674− where -- normal < alternatives < lambdas < rewrites < tactic < default tactic
729+ -- normal < alternatives < lambdas < rewrites < tactic < default tactic
675 -- reason for lambdas after alternatives is that having
730 -- reason for lambdas after alternatives is that having
676 -- the alternative resolved can help with typechecking the lambda
731 -- the alternative resolved can help with typechecking the lambda
677 -- or the rewrite. Rewrites/tactics need as much information
732 -- or the rewrite. Rewrites/tactics need as much information
@@ -744,15 +799,24 @@ elab ist info emode opts fn tm
744 setInjective (PApp _ (PRef _ n) _) = setinj n
799 setInjective (PApp _ (PRef _ n) _) = setinj n
745 setInjective _ = return ()
800 setInjective _ = return ()
747− elab' ina _ tm@(PApp fc f [arg])
802+ elab' ina _ tm@(PApp fc f [arg]) =
748− = erun fc $
803+ erun fc $
749 do simple_app (not $ headRef f)
804 do simple_app (not $ headRef f)
805+ (elabE (ina { e_isfn = True }) (Just fc) f)
750− (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
806+ (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
751 (show tm)
807 (show tm)
753 where headRef (PRef _ _) = True
809 where headRef (PRef _ _) = True
754 headRef (PApp _ f _) = headRef f
810 headRef (PApp _ f _) = headRef f
755 headRef _ = False
811 headRef _ = False
813+ elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...
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
818+ (elab' ina fc Placeholder)
756 elab' ina fc Placeholder
820 elab' ina fc Placeholder
757 = do (h : hs) <- get_holes
821 = do (h : hs) <- get_holes
758 movelast h
822 movelast h
@@ -826,9 +890,21 @@ elab ist info emode opts fn tm
826 envU <- mapM (getKind args) args
890 envU <- mapM (getKind args) args
827 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
891 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
829− -- Drop the unique arguments used in the scrutinee (since it's
893+ -- Drop the unique arguments used in the term already
894+ -- and in the scrutinee (since it's
830− -- not valid to use them again anyway)
895+ -- not valid to use them again anyway)
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)
902+ let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
831− let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr)
904+ let argsDropped = filter (isUnique envU)
905+ (nub $ allNamesIn scr ++ inApp ptm ++
832 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
908 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
834 cname <- unique_hole' True (mkCaseName fn)
910 cname <- unique_hole' True (mkCaseName fn)
@@ -855,6 +931,13 @@ elab ist info emode opts fn tm
855 Just xs@(_:_) -> sNS n xs
931 Just xs@(_:_) -> sNS n xs
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
858 isUnique envk n = case lookup n envk of
941 isUnique envk n = case lookup n envk of
859 Just u -> u
942 Just u -> u
860 _ -> False
943 _ -> False
@@ -882,13 +965,16 @@ elab ist info emode opts fn tm
882 elab' ina fc (PUnifyLog t) = do unifyLog True
965 elab' ina fc (PUnifyLog t) = do unifyLog True
883 elab' ina fc t
966 elab' ina fc t
884 unifyLog False
967 unifyLog False
885− elab' ina fc (PQuasiquote t goal) -- TODO: goal type
968+ elab' ina fc (PQuasiquote t goal)
886 = do -- First extract the unquoted subterms, replacing them with fresh
969 = do -- First extract the unquoted subterms, replacing them with fresh
887 -- names in the quasiquoted term. Claim their reflections to be
970 -- names in the quasiquoted term. Claim their reflections to be
888− -- of type TT.
971+ -- an inferred type (to support polytypic quasiquotes).
889 (t, unq) <- extractUnquotes 0 t
972 (t, unq) <- extractUnquotes 0 t
890 let unquoteNames = map fst unq
973 let unquoteNames = map fst unq
974+ mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")
891− mapM_ (flip claim (Var tt)) unquoteNames
977+ claim uqn (Var uqh)) unquoteNames
894 -- Save the old state - we need a fresh proof state to avoid
980 -- Save the old state - we need a fresh proof state to avoid
@@ -897,7 +983,7 @@ elab ist info emode opts fn tm
897 saveState
983 saveState
898 updatePS (const .
984 updatePS (const .
899 newProof (sMN 0 "q") ctxt $
985 newProof (sMN 0 "q") ctxt $
900− P Ref tt Erased)
986+ P Ref (reflm "TT") Erased)
902 -- Re-add the unquotes, letting Idris infer the (fictional)
988 -- Re-add the unquotes, letting Idris infer the (fictional)
903 -- types. Here, they represent the real type rather than the type
989 -- types. Here, they represent the real type rather than the type
@@ -944,18 +1030,22 @@ elab ist info emode opts fn tm
944 Just q -> do ctxt <- get_context
1030 Just q -> do ctxt <- get_context
945 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
1031 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
946 if pattern
1032 if pattern
947− then reflectQuotePattern unquoteNames q'
1033+ then do try' (reflectTTQuotePattern unquoteNames q')
1034+ (reflectRawQuotePattern unquoteNames (forget q'))
1036+ else do try' (fill $ reflectTTQuote unquoteNames q')
1037+ -- we forget q' instead of using q to ensure rechecking
948− else do fill $ reflectQuote unquoteNames q'
1038+ (fill $ reflectRawQuote unquoteNames (forget q'))
1039+ True -- ignore errors like proof search does
950 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
1042 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
952 -- Finally fill in the terms or patterns from the unquotes. This
1044 -- Finally fill in the terms or patterns from the unquotes. This
953 -- happens last so that their holes still exist while elaborating
1045 -- happens last so that their holes still exist while elaborating
954 -- the main quotation.
1046 -- the main quotation.
955 mapM_ elabUnquote unq
1047 mapM_ elabUnquote unq
956− where tt = sNS (sUN "TT") ["Reflection", "Language"]
958− elabUnquote (n, tm)
1048+ where elabUnquote (n, tm)
959 = do focus n
1049 = do focus n
960 elabE (ina { e_qq = False }) fc tm
1050 elabE (ina { e_qq = False }) fc tm
@@ -976,6 +1066,20 @@ elab ist info emode opts fn tm
976 delayElab $ do focus h
1066 delayElab $ do focus h
978 elab' ina fc t
1068 elab' ina fc t
1069+ elab' ina _ (PRunTactics fc tm) =
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)
1076+ letbind n' scriptTy (Var n)
1078+ elab' ina (Just fc) tm
1080+ ctxt <- get_context
1081+ runTactical fc ctxt env (P Bound n' Erased)
979 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
981 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
1085 delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
@@ -999,6 +1103,7 @@ elab ist info emode opts fn tm
999 findScr [(n, (_, t))] = [(n, (True, t))]
1103 findScr [(n, (_, t))] = [(n, (True, t))]
1000 findScr (x : xs) = x : findScr xs
1104 findScr (x : xs) = x : findScr xs
1001 -- [] can't happen since scrutinee is in the environment!
1105 -- [] can't happen since scrutinee is in the environment!
1106+ findScr [] = error "The impossible happened - the scrutinee was not in the environment"
1003 -- To make sure top level pattern name remains in scope, put
1108 -- To make sure top level pattern name remains in scope, put
1004 -- it at the end of the environment
1109 -- it at the end of the environment
@@ -1072,16 +1177,20 @@ elab ist info emode opts fn tm
1072 = x : insertScopedImps fc sc xs
1177 = x : insertScopedImps fc sc xs
1073 insertScopedImps _ _ xs = xs
1178 insertScopedImps _ _ xs = xs
1075− insertImpLam t =
1180+ insertImpLam ina t =
1076 do ty <- goal
1181 do ty <- goal
1077 env <- get_env
1182 env <- get_env
1078 let ty' = normalise (tt_ctxt ist) env ty
1183 let ty' = normalise (tt_ctxt ist) env ty
1079 addLam ty' t
1184 addLam ty' t
1081 -- just one level at a time
1186 -- just one level at a time
1082− addLam (Bind n (Pi (Just _) _ _) sc) t
1187+ addLam (Bind n (Pi (Just _) _ _) sc) t =
1083− = do impn <- unique_hole (sMN 0 "imp")
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])
1084− return (PLam emptyFC impn Placeholder t)
1193+ else return (PLam emptyFC impn Placeholder t)
1085 addLam _ t = return t
1194 addLam _ t = return t
1087 insertCoerce ina t@(PCase _ _ _) = return t
1196 insertCoerce ina t@(PCase _ _ _) = return t
@@ -1156,7 +1265,8 @@ elab ist info emode opts fn tm
1156 lift (tfail (elaboratingArgErr while' e))
1265 lift (tfail (elaboratingArgErr while' e))
1157 put newState
1266 put newState
1158 return result
1267 return result
1159−
1268+ elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
1269+ fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
1161-- For every alternative, look at the function at the head. Automatically resolve
1271-- For every alternative, look at the function at the head. Automatically resolve
1162-- any nested alternatives where that function is also at the head
1272-- any nested alternatives where that function is also at the head
@@ -1334,6 +1444,7 @@ resTC' tcs defaultOn depth topg fn ist
1334 let imps = case lookupCtxtName n (idris_implicits ist) of
1444 let imps = case lookupCtxtName n (idris_implicits ist) of
1335 [] -> []
1445 [] -> []
1336 [args] -> map isImp (snd args) -- won't be overloaded!
1446 [args] -> map isImp (snd args) -- won't be overloaded!
1447+ xs -> error "The impossible happened - overloading is not expected here!"
1337 ps <- get_probs
1448 ps <- get_probs
1338 tm <- get_term
1449 tm <- get_term
1339 args <- map snd <$> try' (apply (Var n) imps)
1450 args <- map snd <$> try' (apply (Var n) imps)
@@ -1394,6 +1505,86 @@ case_ ind autoSolve ist fn tm = do
1394 else casetac (forget val)
1505 else casetac (forget val)
1395 when autoSolve solveAll
1506 when autoSolve solveAll
1508+runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1509+runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1511+ eval = normaliseAll ctxt env
1512+ tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1513+ returnUnit = fmap fst $ get_type_val (Var unitCon)
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
1522+ | n == tacN "prim__Goal", [] <- args
1523+ = do (h:_) <- get_holes
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
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")))
1540+ else fmap fst . get_type_val $
1541+ RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
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
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)
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
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
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
1578+ | n == tacN "prim__Focus", [what] <- args
1579+ = do n' <- reifyTTName what
1582+ | n == tacN "prim__Unfocus", [what] <- args
1583+ = do n' <- reifyTTName what
1586+ runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1397-- Running tactics directly
1588-- Running tactics directly
1398-- if a tactic adds unification problems, return an error
1589-- if a tactic adds unification problems, return an error
@@ -1460,6 +1651,12 @@ runTac autoSolve ist perhapsFC fn tac
1460 when autoSolve solveAll
1651 when autoSolve solveAll
1461 runT DoUnify = do unify_all
1652 runT DoUnify = do unify_all
1462 when autoSolve solveAll
1653 when autoSolve solveAll
1654+ runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal")
1656+ claim n (Var tmHole)
1658+ elab ist toplevel ERHS [] (sMN 0 "tac") tm
1463 runT (Equiv tm) -- let bind tm, then
1660 runT (Equiv tm) -- let bind tm, then
1464 = do attack
1661 = do attack
1465 tyn <- getNameFrom (sMN 0 "ety")
1662 tyn <- getNameFrom (sMN 0 "ety")
@@ -1520,6 +1717,10 @@ runTac autoSolve ist perhapsFC fn tac
1520 = do proofSearch' ist rec False depth prover top fn hints
1717 = do proofSearch' ist rec False depth prover top fn hints
1521 when autoSolve solveAll
1718 when autoSolve solveAll
1522 runT (Focus n) = focus n
1719 runT (Focus n) = focus n
1720+ runT Unfocus = do hs <- get_holes
1723+ (h : _) -> movelast h
1523 runT Solve = solve
1724 runT Solve = solve
1524 runT (Try l r) = do try' (runT l) (runT r) True
1725 runT (Try l r) = do try' (runT l) (runT r) True
1525 runT (TSeq l r) = do runT l; runT r
1726 runT (TSeq l r) = do runT l; runT r
@@ -1664,6 +1865,7 @@ reify _ (P _ n _) | n == reflm "Solve" = return Solve
1664reify _ (P _ n _) | n == reflm "Compute" = return Compute
1865reify _ (P _ n _) | n == reflm "Compute" = return Compute
1665reify _ (P _ n _) | n == reflm "Skip" = return Skip
1866reify _ (P _ n _) | n == reflm "Skip" = return Skip
1666reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
1867reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
1868+reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
1667reify ist t@(App _ _)
1869reify ist t@(App _ _)
1668 | (P _ f _, args) <- unApply t = reifyApp ist f args
1870 | (P _ f _, args) <- unApply t = reifyApp ist f args
1669reify _ t = fail ("Unknown tactic " ++ show t)
1871reify _ t = fail ("Unknown tactic " ++ show t)
@@ -1675,6 +1877,9 @@ reifyApp _ t [Constant (I i)]
1675reifyApp _ t [x]
1877reifyApp _ t [x]
1676 | t == reflm "Refine" = do n <- reifyTTName x
1878 | t == reflm "Refine" = do n <- reifyTTName x
1677 return $ Refine n []
1879 return $ Refine n []
1880+reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
1882+ return $ Claim n' (delab ist goal)
1678reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
1883reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
1679reifyApp ist t [Constant (Str n), x]
1884reifyApp ist t [Constant (Str n), x]
1680 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
1885 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
@@ -1705,16 +1910,20 @@ reifyApp ist t [n, tt', t']
1705 t'' <- reifyTT t'
1910 t'' <- reifyTT t'
1706 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
1911 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
1707reifyApp ist t [errs]
1912reifyApp ist t [errs]
1708− | t == reflm "Fail" = case unList errs of
1913+ | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
1709− Nothing -> fail "Failed to reify errors"
1711− let parts = mapM reifyReportPart errs' in
1713− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1715− return $ TFail errs''
1716reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
1914reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
1916+reifyReportParts :: Term -> ElabD [ErrorReportPart]
1917+reifyReportParts errs =
1918+ case unList errs of
1919+ Nothing -> fail "Failed to reify errors"
1921+ let parts = mapM reifyReportPart errs' in
1923+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1718-- | Reify terms from their reflected representation
1927-- | Reify terms from their reflected representation
1719reifyTT :: Term -> ElabD Term
1928reifyTT :: Term -> ElabD Term
1720reifyTT t@(App _ _)
1929reifyTT t@(App _ _)
@@ -1894,6 +2103,7 @@ reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
1894reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
2103reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
1895reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
2104reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
1896 (reifyNativeTy nt)
2105 (reifyNativeTy nt)
2106+reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
1898reifyTTUExp :: Term -> ElabD UExp
2108reifyTTUExp :: Term -> ElabD UExp
1899reifyTTUExp t@(App _ _)
2109reifyTTUExp t@(App _ _)
@@ -1910,7 +2120,11 @@ reflCall funName args
1911-- | Lift a term into its Language.Reflection.TT representation
2121-- | Lift a term into its Language.Reflection.TT representation
1912reflect :: Term -> Raw
2122reflect :: Term -> Raw
1913−reflect = reflectQuote []
2123+reflect = reflectTTQuote []
2125+-- | Lift a term into its Language.Reflection.Raw representation
2126+reflectRaw :: Raw -> Raw
2127+reflectRaw = reflectRawQuote []
1915claimTT :: Name -> ElabD Name
2129claimTT :: Name -> ElabD Name
1916claimTT n = do n' <- getNameFrom n
2130claimTT n = do n' <- getNameFrom n
@@ -1921,8 +2135,8 @@ claimTT n = do n' <- getNameFrom n
1921-- In particular, the less-interesting bits are elaborated to _ patterns. This
2135-- In particular, the less-interesting bits are elaborated to _ patterns. This
1922-- happens to NameTypes, universe levels, names that are bound but not used,
2136-- happens to NameTypes, universe levels, names that are bound but not used,
1923-- and the type annotation field of the P constructor.
2137-- and the type annotation field of the P constructor.
1924−reflectQuotePattern :: [Name] -> Term -> ElabD ()
2138+reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
1925−reflectQuotePattern unq (P _ n _)
2139+reflectTTQuotePattern unq (P _ n _)
1926 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
2140 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
1927 do fill (Var n) ; solve
2141 do fill (Var n) ; solve
1928 | otherwise =
2142 | otherwise =
@@ -1936,10 +2150,10 @@ reflectQuotePattern unq (P _ n _)
1936 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
2150 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
1938 focus n'; reflectNameQuotePattern n
2152 focus n'; reflectNameQuotePattern n
1939−reflectQuotePattern unq (V n)
2153+reflectTTQuotePattern unq (V n)
1940 = do fill $ reflCall "V" [RConstant (I n)]
2154 = do fill $ reflCall "V" [RConstant (I n)]
1942−reflectQuotePattern unq (Bind n b x)
2156+reflectTTQuotePattern unq (Bind n b x)
1943 = do x' <- claimTT (sMN 0 "sc")
2157 = do x' <- claimTT (sMN 0 "sc")
1944 movelast x'
2158 movelast x'
1945 b' <- getNameFrom (sMN 0 "binder")
2159 b' <- getNameFrom (sMN 0 "binder")
@@ -1959,111 +2173,215 @@ reflectQuotePattern unq (Bind n b x)
1962− focus x'; reflectQuotePattern unq x
2176+ focus x'; reflectTTQuotePattern unq x
1963− focus b'; reflectBinderQuotePattern unq b
2177+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
1964−
2178+reflectTTQuotePattern unq (App f x)
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']
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']
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']
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']
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']
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']
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']
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']
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']
2018− focus t'; reflectQuotePattern unq t
2019−reflectQuotePattern unq (App f x)
2020 = do f' <- claimTT (sMN 0 "f"); movelast f'
2179 = do f' <- claimTT (sMN 0 "f"); movelast f'
2021 x' <- claimTT (sMN 0 "x"); movelast x'
2180 x' <- claimTT (sMN 0 "x"); movelast x'
2022 fill $ reflCall "App" [Var f', Var x']
2181 fill $ reflCall "App" [Var f', Var x']
2024− focus f'; reflectQuotePattern unq f
2183+ focus f'; reflectTTQuotePattern unq f
2025− focus x'; reflectQuotePattern unq x
2184+ focus x'; reflectTTQuotePattern unq x
2026−reflectQuotePattern unq (Constant c)
2185+reflectTTQuotePattern unq (Constant c)
2027 = do fill $ reflCall "TConst" [reflectConstant c]
2186 = do fill $ reflCall "TConst" [reflectConstant c]
2029−reflectQuotePattern unq (Proj t i)
2188+reflectTTQuotePattern unq (Proj t i)
2030 = do t' <- claimTT (sMN 0 "t"); movelast t'
2189 = do t' <- claimTT (sMN 0 "t"); movelast t'
2031 fill $ reflCall "Proj" [Var t', RConstant (I i)]
2190 fill $ reflCall "Proj" [Var t', RConstant (I i)]
2033− focus t'; reflectQuotePattern unq t
2192+ focus t'; reflectTTQuotePattern unq t
2034−reflectQuotePattern unq (Erased)
2193+reflectTTQuotePattern unq (Erased)
2035 = do erased <- claimTT (sMN 0 "erased")
2194 = do erased <- claimTT (sMN 0 "erased")
2036 movelast erased
2195 movelast erased
2037 fill $ (Var erased)
2196 fill $ (Var erased)
2039−reflectQuotePattern unq (Impossible)
2198+reflectTTQuotePattern unq (Impossible)
2040 = do fill $ Var (reflm "Impossible")
2199 = do fill $ Var (reflm "Impossible")
2042−reflectQuotePattern unq (TType exp)
2201+reflectTTQuotePattern unq (TType exp)
2043 = do ue <- getNameFrom (sMN 0 "uexp")
2202 = do ue <- getNameFrom (sMN 0 "uexp")
2044 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2203 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2045 movelast ue
2204 movelast ue
2046 fill $ reflCall "TType" [Var ue]
2205 fill $ reflCall "TType" [Var ue]
2207+reflectTTQuotePattern unq (UType u)
2208+ = do uH <- getNameFrom (sMN 0 "someUniv")
2209+ claim uH (Var (reflm "Universe"))
2211+ fill $ reflCall "UType" [Var uH]
2214+ fill (Var (reflm (case u of
2215+ NullType -> "NullType"
2216+ UniqueType -> "UniqueType"
2217+ AllTypes -> "AllTypes")))
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"))
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,
2237+ else do any <- getNameFrom (sMN 0 "anyName")
2238+ claim any (Var (reflm "TTName"))
2240+ fill $ reflCall "RBind" [Var any, Var bH, Var scH]
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],
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"))
2259+ xH <- getNameFrom (sMN 0 "x")
2260+ claim xH (Var (reflm "Raw"))
2262+ fill $ reflCall "RApp" [Var fH, Var xH]
2264+ focus fH; reflectRawQuotePattern unq f
2265+ focus xH; reflectRawQuotePattern unq x
2266+reflectRawQuotePattern unq RType =
2267+ do fill (Var (reflm "RType"))
2269+reflectRawQuotePattern unq (RUType univ) =
2270+ do uH <- getNameFrom (sMN 0 "universe")
2271+ claim uH (Var (reflm "Universe"))
2273+ fill $ reflCall "RUType" [Var uH]
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"))
2280+ fill $ reflCall "RForce" [Var rH]
2282+ focus rH; reflectRawQuotePattern unq r
2283+reflectRawQuotePattern unq (RConstant c) =
2284+ do cH <- getNameFrom (sMN 0 "const")
2285+ claim cH (Var (reflm "Constant"))
2287+ fill (reflCall "RConstant" [Var cH]); solve
2289+ fill (reflectConstant c); solve
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']
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']
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']
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']
2317+reflectBinderQuotePattern q unq (Hole t)
2318+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2319+ fill $ reflCall "Hole" [Var (reflm "TT"), Var 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']
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']
2334+reflectBinderQuotePattern q unq (PVar t)
2335+ = do t' <- claimTT (sMN 0 "ty"); movelast t'
2336+ fill $ reflCall "PVar" [Var (reflm "TT"), Var 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']
2345+reflectUniverse :: Universe -> Raw
2347+ (Var (reflm (case u of
2348+ NullType -> "NullType"
2349+ UniqueType -> "UniqueType"
2350+ AllTypes -> "AllTypes")))
2049−-- | Create a reflected term, but leave refs to the provided name intact
2352+-- | Create a reflected TT term, but leave refs to the provided name intact
2050−reflectQuote :: [Name] -> Term -> Raw
2353+reflectTTQuote :: [Name] -> Term -> Raw
2051−reflectQuote unq (P nt n t)
2354+reflectTTQuote unq (P nt n t)
2052 | n `elem` unq = Var n
2355 | n `elem` unq = Var n
2053− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
2356+ | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2054−reflectQuote unq (V n)
2357+reflectTTQuote unq (V n)
2055 = reflCall "V" [RConstant (I n)]
2358 = reflCall "V" [RConstant (I n)]
2056−reflectQuote unq (Bind n b x)
2359+reflectTTQuote unq (Bind n b x)
2057− = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]
2360+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]
2058−reflectQuote unq (App f x)
2361+reflectTTQuote unq (App f x)
2059− = reflCall "App" [reflectQuote unq f, reflectQuote unq x]
2362+ = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2060−reflectQuote unq (Constant c)
2363+reflectTTQuote unq (Constant c)
2061 = reflCall "TConst" [reflectConstant c]
2364 = reflCall "TConst" [reflectConstant c]
2062−reflectQuote unq (Proj t i)
2365+reflectTTQuote unq (Proj t i)
2063− = reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
2366+ = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2064−reflectQuote unq (Erased) = Var (reflm "Erased")
2367+reflectTTQuote unq (Erased) = Var (reflm "Erased")
2065−reflectQuote unq (Impossible) = Var (reflm "Impossible")
2368+reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2066−reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2369+reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2370+reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
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]
2068reflectNameType :: NameType -> Raw
2386reflectNameType :: NameType -> Raw
2069reflectNameType (Bound) = Var (reflm "Bound")
2387reflectNameType (Bound) = Var (reflm "Bound")
@@ -2114,27 +2432,27 @@ reflectNameQuotePattern _ -- for all other names, match any
2116reflectBinder :: Binder Term -> Raw
2434reflectBinder :: Binder Term -> Raw
2117−reflectBinder = reflectBinderQuote []
2435+reflectBinder = reflectBinderQuote reflectTTQuote []
2119−reflectBinderQuote :: [Name] -> Binder Term -> Raw
2437+reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw
2120−reflectBinderQuote unq (Lam t)
2438+reflectBinderQuote q unq (Lam t)
2121− = reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
2439+ = reflCall "Lam" [Var (reflm "TT"), q unq t]
2122−reflectBinderQuote unq (Pi _ t k)
2440+reflectBinderQuote q unq (Pi _ t k)
2123− = reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]
2441+ = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]
2124−reflectBinderQuote unq (Let x y)
2442+reflectBinderQuote q unq (Let x y)
2125− = reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2443+ = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]
2126−reflectBinderQuote unq (NLet x y)
2444+reflectBinderQuote q unq (NLet x y)
2127− = reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2445+ = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]
2128−reflectBinderQuote unq (Hole t)
2446+reflectBinderQuote q unq (Hole t)
2129− = reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
2447+ = reflCall "Hole" [Var (reflm "TT"), q unq t]
2130−reflectBinderQuote unq (GHole _ t)
2448+reflectBinderQuote q unq (GHole _ t)
2131− = reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
2449+ = reflCall "GHole" [Var (reflm "TT"), q unq t]
2132−reflectBinderQuote unq (Guess x y)
2450+reflectBinderQuote q unq (Guess x y)
2133− = reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
2451+ = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]
2134−reflectBinderQuote unq (PVar t)
2452+reflectBinderQuote q unq (PVar t)
2135− = reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
2453+ = reflCall "PVar" [Var (reflm "TT"), q unq t]
2136−reflectBinderQuote unq (PVTy t)
2454+reflectBinderQuote q unq (PVTy t)
2137− = reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
2455+ = reflCall "PVTy" [Var (reflm "TT"), q unq t]
2139mkList :: Raw -> [Raw] -> Raw
2457mkList :: Raw -> [Raw] -> Raw
2140mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
2458mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
@@ -2174,7 +2492,8 @@ reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")
2174reflectConstant BufferType = Var (reflm "BufferType")
2492reflectConstant BufferType = Var (reflm "BufferType")
2175reflectConstant VoidType = Var (reflm "VoidType")
2493reflectConstant VoidType = Var (reflm "VoidType")
2176reflectConstant Forgot = Var (reflm "Forgot")
2494reflectConstant Forgot = Var (reflm "Forgot")
2177−
2495+reflectConstant WorldType = Var (reflm "WorldType")
2496+reflectConstant TheWorld = Var (reflm "TheWorld")
2179reflectUExp :: UExp -> Raw
2498reflectUExp :: UExp -> Raw
2180reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
2499reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]