@@ -28,9 +28,10 @@ import qualified Util.Pretty as U
2828import Control.Applicative ((<$>))
2929import Control.Monad
3030import Control.Monad.State.Strict
31+import Data.Foldable (for_)
3132import Data.List
3233import qualified Data.Map as M
33−import Data.Maybe (mapMaybe, fromMaybe, catMaybes)
34+import Data.Maybe (mapMaybe, fromMaybe, catMaybes, maybeToList)
3435import qualified Data.Set as S
3536import qualified Data.Text as T
3637
@@ -90,7 +91,7 @@ build ist info emode opts fn tm
9091 g <- goal
9192 ptm <- get_term
9293 resolveTC' True True 10 g fn ist) ivs
93−
94+
9495 when (not pattern) $ solveAutos ist fn False
9596
9697 tm <- get_term
@@ -137,15 +138,16 @@ build ist info emode opts fn tm
137138-- (Separate, so we don't go overboard resolving things that we don't
138139-- know about yet on the LHS of a pattern def)
139140
140−buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
141+buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->
142+ [Name] -> -- Cached names in the PTerm, before adding PAlternatives
143+ PTerm ->
141144 ElabD ElabResult
142−buildTC ist info emode opts fn tm
143− = do -- set name supply to begin after highest index in tm
144− let ns = allNamesIn tm
145− let tmIn = tm
145+buildTC ist info emode opts fn ns tm
146+ = do let tmIn = tm
146147 let inf = case lookupCtxt fn (idris_tyinfodata ist) of
147148 [TIPartial] -> True
148149 _ -> False
150+ -- set name supply to begin after highest index in tm
149151 initNextNameFrom ns
150152 elab ist info emode opts fn tm
151153 probs <- get_probs
@@ -169,7 +171,7 @@ buildTC ist info emode opts fn tm
169171 else return (ElabResult tm ds (map snd is) ctxt impls highlights)
170172 where pattern = emode == ELHS
171173
172−-- return whether arguments of the given constructor name can be
174+-- return whether arguments of the given constructor name can be
173175-- matched on. If they're polymorphic, no, unless the type has beed made
174176-- concrete by the time we get around to elaborating the argument.
175177getUnmatchable :: Context -> Name -> [Bool]
@@ -178,11 +180,11 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
178180 Nothing -> []
179181 Just ty -> checkArgs [] [] ty
180182 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
181− checkArgs env ns (Bind n (Pi _ t _) sc)
183+ checkArgs env ns (Bind n (Pi _ t _) sc)
182184 = let env' = case t of
183185 TType _ -> n : env
184186 _ -> env in
185− checkArgs env' (intersect env (refsIn t) : ns)
187+ checkArgs env' (intersect env (refsIn t) : ns)
186188 (instantiate (P Bound n t) sc)
187189 checkArgs env ns t
188190 = map (not . null) (reverse ns)
@@ -191,7 +193,7 @@ getUnmatchable ctxt n = []
191193
192194data ElabCtxt = ElabCtxt { e_inarg :: Bool,
193195 e_isfn :: Bool, -- ^ Function part of application
194− e_guarded :: Bool,
196+ e_guarded :: Bool,
195197 e_intype :: Bool,
196198 e_qq :: Bool,
197199 e_nomatching :: Bool -- ^ can't pattern match
@@ -265,17 +267,17 @@ elab ist info emode opts fn tm
265267 -- normally correct to call elabE - the ones that don't are desugarings
266268 -- typically
267269 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
268− elabE ina fc' t =
270+ elabE ina fc' t =
269271 do solved <- get_recents
270272 as <- get_autos
271273 hs <- get_holes
272274 -- If any of the autos use variables which have recently been solved,
273275 -- have another go at solving them now.
274− mapM_ (\(a, (failc, ns)) ->
276+ mapM_ (\(a, (failc, ns)) ->
275277 if any (\n -> n `elem` solved) ns && head hs /= a
276278 then solveAuto ist fn False (a, failc)
277279 else return ()) as
278−
280+
279281 itm <- if not pattern then insertImpLam ina t else return t
280282 ct <- insertCoerce ina itm
281283 t' <- insertLazy ct
@@ -308,7 +310,7 @@ elab ist info emode opts fn tm
308310 forceErr orig env (InfiniteUnify _ t _)
309311 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
310312 ht == txt "Lazy'" = notDelay orig
311− forceErr orig env (Elaborating _ _ t) = forceErr orig env t
313+ forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t
312314 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
313315 forceErr orig env (At _ t) = forceErr orig env t
314316 forceErr orig env t = False
@@ -341,7 +343,7 @@ elab ist info emode opts fn tm
341343-- elab' (_,_,inty) (PConstant c)
342344-- | constType c && pattern && not reflection && not inty
343345-- = lift $ tfail (Msg "Typecase is not allowed")
344− elab' ina fc tm@(PConstant fc' c)
346+ elab' ina fc tm@(PConstant fc' c)
345347 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
346348 && isTypeConst c
347349 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
@@ -361,7 +363,7 @@ elab ist info emode opts fn tm
361363 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
362364 = do g <- goal; resolveTC' False False 5 g fn ist
363365 elab' ina fc (PResolveTC fc')
364− = do c <- getNameFrom (sMN 0 "class")
366+ = do c <- getNameFrom (sMN 0 "__class")
365367 instanceArg c
366368 -- Elaborate the equality type first homogeneously, then
367369 -- heterogeneously as a fallback
@@ -395,7 +397,7 @@ elab ist info emode opts fn tm
395397 UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)
396398 [pexp l,pexp r])
397399 _ -> case tc of
398− P _ n _ | n == upairTy
400+ P _ n _ | n == upairTy
399401 -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)
400402 [pimp (sUN "A") Placeholder False,
401403 pimp (sUN "B") Placeholder False,
@@ -442,16 +444,17 @@ elab ist info emode opts fn tm
442444 uns <- get_usedns
443445 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
444446 (h : hs) <- get_holes
445−-- trace (show (map showHd as')) $
446447 ty <- goal
447448 case as' of
448− [] -> lift $ tfail $ NoValidAlts (map showHd as)
449+ [] -> do hds <- mapM showHd as
450+ lift $ tfail $ NoValidAlts hds
449451 [x] -> elab' ina fc x
450452 -- If there's options, try now, and if that fails, postpone
451453 -- to later.
452454 _ -> handleError isAmbiguous
453− (tryAll (zip (map (elab' ina fc) as')
454− (map showHd as')))
455+ (do hds <- mapM showHd as'
456+ tryAll (zip (map (elab' ina fc) as')
457+ hds))
455458 (do movelast h
456459 delayElab 5 $ do
457460 hs <- get_holes
@@ -460,16 +463,17 @@ elab ist info emode opts fn tm
460463 as'' <- doPrune as'
461464 case as'' of
462465 [x] -> elab' ina fc x
463− _ -> tryAll (zip (map (elab' ina fc) as'')
464− (map showHd as'')))
466+ _ -> do hds <- mapM showHd as''
467+ tryAll (zip (map (elab' ina fc) as'')
468+ hds))
465469 where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])
466470 | l == txt "Delay" = showHd (getTm arg)
467− showHd (PApp _ (PRef _ _ n) _) = n
468− showHd (PRef _ _ n) = n
471+ showHd (PApp _ (PRef _ _ n) _) = return n
472+ showHd (PRef _ _ n) = return n
469473 showHd (PApp _ h _) = showHd h
470− showHd x = NErased -- We probably should do something better than this here
474+ showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
471475
472− doPrune as =
476+ doPrune as =
473477 do compute
474478 ty <- goal
475479 let (tc, _) = unApply (unDelay ty)
@@ -479,10 +483,9 @@ elab ist info emode opts fn tm
479483 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
480484 l == txt "Lazy'" = unDelay arg
481485 | otherwise = t
482−
483486
484487 isAmbiguous (CantResolveAlts _) = delayok
485− isAmbiguous (Elaborating _ _ e) = isAmbiguous e
488+ isAmbiguous (Elaborating _ _ _ e) = isAmbiguous e
486489 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e
487490 isAmbiguous (At _ e) = isAmbiguous e
488491 isAmbiguous _ = False
@@ -506,7 +509,7 @@ elab ist info emode opts fn tm
506509 ty <- goal
507510 let doelab = elab' ina fc orig
508511 tryCatch doelab
509− (\err ->
512+ (\err ->
510513 if recoverableErr err
511514 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++
512515 -- show alts ++ "\n" ++
@@ -544,7 +547,7 @@ elab ist info emode opts fn tm
544547 pruneAlts err alts _ = filter isLend alts
545548
546549 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'
547− hasArg n env (PApp _ (PRef _ _ a) _)
550+ hasArg n env (PApp _ (PRef _ _ a) _)
548551 = case lookupTyExact a (tt_ctxt ist) of
549552 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in
550553 any (fnIs n) args
@@ -659,7 +662,7 @@ elab ist info emode opts fn tm
659662 introTy (Var tyn) (Just n)
660663 addPSname n -- okay for proof search
661664 focus tyn
662−
665+
663666 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
664667 elabE (ec { e_inarg = True }) (Just fc) sc
665668 solve
@@ -698,10 +701,10 @@ elab ist info emode opts fn tm
698701 Placeholder -> return ()
699702 _ -> do focus tyn
700703 explicit tyn
701− elabE (ina { e_inarg = True, e_intype = True })
704+ elabE (ina { e_inarg = True, e_intype = True })
702705 (Just fc) ty
703706 focus valn
704− elabE (ina { e_inarg = True, e_intype = True })
707+ elabE (ina { e_inarg = True, e_intype = True })
705708 (Just fc) val
706709 ivs' <- get_instances
707710 env <- get_env
@@ -711,8 +714,9 @@ elab ist info emode opts fn tm
711714 g <- goal
712715 hs <- get_holes
713716 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
714− then try (resolveTC' True False 10 g fn ist)
715− (movelast n)
717+ then handleError (tcRecoverable emode)
718+ (resolveTC' True False 10 g fn ist)
719+ (movelast n)
716720 else movelast n)
717721 (ivs' \\ ivs)
718722 -- HACK: If the name leaks into its type, it may leak out of
@@ -804,14 +808,14 @@ elab ist info emode opts fn tm
804808 annot <- findHighlight f
805809 mapM_ checkKnownImplicit args_in
806810 let args = insertScopedImps fc (normalise ctxt env fty) args_in
807− let unmatchableArgs = if pattern
811+ let unmatchableArgs = if pattern
808812 then getUnmatchable (tt_ctxt ist) f
809813 else []
810−-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
814+-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
811815 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
812816 && isTConName f (tt_ctxt ist)) $
813817 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
814−-- trace (show (f, args_in, args)) $
818+-- trace (show (f, args_in, args)) $
815819 if (f `elem` map fst env && length args == 1 && length args_in == 1)
816820 then -- simple app, as below
817821 do simple_app False
@@ -849,7 +853,7 @@ elab ist info emode opts fn tm
849853 mapM (uncurry highlightSource) $
850854 (ffc, annot) : map (\f -> (f, annot)) hls
851855
852− elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
856+ elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
853857 [] fc False f
854858 (zip ns (unmatchableArgs ++ repeat False))
855859 (f == sUN "Force")
@@ -876,26 +880,27 @@ elab ist info emode opts fn tm
876880 ivs' <- get_instances
877881 -- Attempt to resolve any type classes which have 'complete' types,
878882 -- i.e. no holes in them
879− when (not pattern || (e_inarg ina && not tcgen &&
883+ when (not pattern || (e_inarg ina && not tcgen &&
880884 not (e_guarded ina))) $
881885 mapM_ (\n -> do focus n
882886 g <- goal
883887 env <- get_env
884888 hs <- get_holes
885889 if all (\n -> not (n `elem` hs)) (freeNames g)
886− then try (resolveTC' False False 10 g fn ist)
890+ then handleError (tcRecoverable emode)
891+ (resolveTC' False False 10 g fn ist)
887892 (movelast n)
888893 else movelast n)
889894 (ivs' \\ ivs)
890895 return []
891− where
896+ where
892897 -- Run the elaborator, which returns how many implicit
893898 -- args were needed, then run it again with those args. We need
894899 -- this because we have to elaborate the whole application to
895900 -- find out whether any computations have caused more implicits
896901 -- to be needed.
897902 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
898− implicitApp elab
903+ implicitApp elab
899904 | pattern || intransform = do elab; return ()
900905 | otherwise
901906 = do s <- get
@@ -904,7 +909,7 @@ elab ist info emode opts fn tm
904909 [] -> return ()
905910 es -> do put s
906911 elab' ina topfc (PAppImpl tm es)
907−
912+
908913 checkKnownImplicit imp
909914 | UnknownImp `elem` argopts imp
910915 = lift $ tfail $ UnknownImplicit (pname imp) f
@@ -961,7 +966,7 @@ elab ist info emode opts fn tm
961966 headRef (PAlternative _ _ as) = all headRef as
962967 headRef _ = False
963968
964− elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...
969+ elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...
965970 solve
966971 where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits
967972 appImpl (e : es) = simple_app False
@@ -1023,12 +1028,22 @@ elab ist info emode opts fn tm
10231028 solve
10241029 elab' ina _ c@(PCase fc scr opts)
10251030 = do attack
1031+
10261032 tyn <- getNameFrom (sMN 0 "scty")
10271033 claim tyn RType
10281034 valn <- getNameFrom (sMN 0 "scval")
10291035 scvn <- getNameFrom (sMN 0 "scvar")
10301036 claim valn (Var tyn)
10311037 letbind scvn (Var tyn) (Var valn)
1038+
1039+ -- Start filling in the scrutinee type, if we can work one
1040+ -- out from the case options
1041+ let scrTy = getScrType (map fst opts)
1042+ case scrTy of
1043+ Nothing -> return ()
1044+ Just ty -> do focus tyn
1045+ elabE ina (Just fc) ty
1046+
10321047 focus valn
10331048 elabE (ina { e_inarg = True }) (Just fc) scr
10341049 -- Solve any remaining implicits - we need to solve as many
@@ -1041,7 +1056,7 @@ elab ist info emode opts fn tm
10411056
10421057 -- Drop the unique arguments used in the term already
10431058 -- and in the scrutinee (since it's
1044− -- not valid to use them again anyway)
1059+ -- not valid to use them again anyway)
10451060 --
10461061 -- Also drop unique arguments which don't appear explicitly
10471062 -- in either case branch so they don't count as used
@@ -1050,14 +1065,14 @@ elab ist info emode opts fn tm
10501065 ptm <- get_term
10511066 let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
10521067
1053− let argsDropped = filter (isUnique envU)
1068+ let argsDropped = filter (isUnique envU)
10541069 (nub $ allNamesIn scr ++ inApp ptm ++
10551070 inOpts)
10561071
10571072 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
10581073
10591074 attack
1060− cname' <- defer argsDropped (mkN (mkCaseName fn))
1075+ cname' <- defer argsDropped (mkN (mkCaseName fc fn))
10611076 solve
10621077
10631078 -- if the scrutinee is one of the 'args' in env, we should
@@ -1070,8 +1085,8 @@ elab ist info emode opts fn tm
10701085 -- if we haven't got the type yet, hopefully we'll get it later!
10711086 movelast tyn
10721087 solve
1073− where mkCaseName (NS n ns) = NS (mkCaseName n) ns
1074− mkCaseName n = SN (CaseN n)
1088+ where mkCaseName fc (NS n ns) = NS (mkCaseName fc n) ns
1089+ mkCaseName fc n = SN (CaseN (FC' fc) n)
10751090-- mkCaseName (UN x) = UN (x ++ "_case")
10761091-- mkCaseName (MN i x) = MN i (x ++ "_case")
10771092 mkN n@(NS _ _) = n
@@ -1079,6 +1094,21 @@ elab ist info emode opts fn tm
10791094 Just xs@(_:_) -> sNS n xs
10801095 _ -> n
10811096
1097+ getScrType [] = Nothing
1098+ getScrType (f : os) = maybe (getScrType os) Just (getAppType f)
1099+
1100+ getAppType (PRef _ _ n) =
1101+ case lookupTyName n (tt_ctxt ist) of
1102+ [(n', ty)] | isDConName n' (tt_ctxt ist) ->
1103+ case unApply (getRetTy ty) of
1104+ (P _ tyn _, args) ->
1105+ Just (PApp fc (PRef fc [] tyn)
1106+ (map pexp (map (const Placeholder) args)))
1107+ _ -> Nothing
1108+ _ -> Nothing -- ambiguity is no help to us!
1109+ getAppType (PApp _ t as) = getAppType t
1110+ getAppType _ = Nothing
1111+
10821112 inApp (P _ n _) = [n]
10831113 inApp (App _ f a) = inApp f ++ inApp a
10841114 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
@@ -1220,12 +1250,12 @@ elab ist info emode opts fn tm
12201250 [] -> lift . tfail . NoSuchVariable $ n
12211251 more -> lift . tfail . CantResolveAlts $ map fst more
12221252 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
1223− elab' ina fc (PHidden t)
1253+ elab' ina fc (PHidden t)
12241254 | reflection = elab' ina fc t
12251255 | otherwise
12261256 = do (h : hs) <- get_holes
12271257 -- Dotting a hole means that either the hole or any outer
1228− -- hole (a hole outside any occurrence of it)
1258+ -- hole (a hole outside any occurrence of it)
12291259 -- must be solvable by unification as well as being filled
12301260 -- in directly.
12311261 -- Delay dotted things to the end, then when we elaborate them
@@ -1237,17 +1267,18 @@ elab ist info emode opts fn tm
12371267 elab' ina fc (PRunElab fc' tm ns) =
12381268 do attack
12391269 n <- getNameFrom (sMN 0 "tacticScript")
1240− n' <- getNameFrom (sMN 0 "tacticExpr")
12411270 let scriptTy = RApp (Var (sNS (sUN "Elab")
12421271 ["Elab", "Reflection", "Language"]))
12431272 (Var unitTy)
12441273 claim n scriptTy
1245− movelast n
1246− letbind n' scriptTy (Var n)
12471274 focus n
1275+ attack -- to get an extra hole
12481276 elab' ina (Just fc') tm
1277+ script <- get_guess
1278+ fullyElaborated script
1279+ solve -- eliminate the hole. Becuase there are no references, the script is only in the binding
12491280 env <- get_env
1250− runElabAction ist (maybe fc' id fc) env (P Bound n' Erased) ns
1281+ runElabAction ist (maybe fc' id fc) env script ns
12511282 solve
12521283 elab' ina fc (PConstSugar constFC tm) =
12531284 -- Here we elaborate the contained term, then calculate
@@ -1292,7 +1323,7 @@ elab ist info emode opts fn tm
12921323 -- The delayed things with lower numbered priority will be elaborated
12931324 -- first. (In practice, this means delayed alternatives, then PHidden
12941325 -- things.)
1295− delayElab pri t
1326+ delayElab pri t
12961327 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })
12971328
12981329 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
@@ -1360,6 +1391,19 @@ elab ist info emode opts fn tm
13601391 getFC d (PAlternative _ _ (x:_)) = getFC d x
13611392 getFC d x = d
13621393
1394+ -- Fail if a term is not yet fully elaborated (e.g. if it contains
1395+ -- case block functions that don't yet exist)
1396+ fullyElaborated :: Term -> ElabD ()
1397+ fullyElaborated (P _ n _) =
1398+ do EState cases _ _ _ <- getAux
1399+ case lookup n cases of
1400+ Nothing -> return ()
1401+ Just _ -> lift . tfail $ ElabScriptStaging n
1402+ fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated
1403+ fullyElaborated (App _ l r) = fullyElaborated l >> fullyElaborated r
1404+ fullyElaborated (Proj t _) = fullyElaborated t
1405+ fullyElaborated _ = return ()
1406+
13631407 insertLazy :: PTerm -> ElabD PTerm
13641408 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
13651409 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
@@ -1396,9 +1440,9 @@ elab ist info emode opts fn tm
13961440 notImplicitable _ = False
13971441
13981442 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
1399− | tcinstance i
1443+ | tcinstance i && not (toplevel_imp i)
14001444 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
1401− | otherwise
1445+ | not (toplevel_imp i)
14021446 = pimp n Placeholder True : insertScopedImps fc sc xs
14031447 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
14041448 = x : insertScopedImps fc sc xs
@@ -1432,7 +1476,7 @@ elab ist info emode opts fn tm
14321476 let t' = case (t, cs) of
14331477 (PCoerced tm, _) -> tm
14341478 (_, []) -> t
1435− (_, cs) -> PAlternative [] TryImplicit
1479+ (_, cs) -> PAlternative [] TryImplicit
14361480 (t : map (mkCoerce env t) cs)
14371481 return t'
14381482 where
@@ -1554,7 +1598,7 @@ pruneByType env (P _ n _) ist as
15541598 [] -> asV
15551599 _ -> as'
15561600 where
1557− ctxt = tt_ctxt ist
1601+ ctxt = tt_ctxt ist
15581602
15591603 headIs var f (PRef _ _ f') = typeHead var f f'
15601604 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
@@ -1573,7 +1617,7 @@ pruneByType env (P _ n _) ist as
15731617 _ -> let ty' = normalise ctxt [] ty in
15741618 case unApply (getRetTy ty') of
15751619 (P _ ftyn _, _) -> ftyn == f
1576− (V _, _) ->
1620+ (V _, _) ->
15771621 -- keep, variable
15781622-- trace ("Keeping " ++ show (f', ty')
15791623-- ++ " for " ++ show n) $
@@ -1590,22 +1634,22 @@ pruneByType _ t _ as = as
15901634-- (FIXME: This isn't complete, but I'm leaving it here and coming back
15911635-- to it later - just returns 'var' for now. EB)
15921636isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
1593−isPlausible ist var env n ty
1637+isPlausible ist var env n ty
15941638 = let (hvar, classes) = collectConstraints [] [] ty in
15951639 case hvar of
15961640 Nothing -> True
15971641 Just rth -> var -- trace (show (rth, classes)) var
15981642 where
1599− collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
1643+ collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
16001644 (Maybe Name, [(Term, [Name])])
16011645 collectConstraints env tcs (Bind n (Pi _ ty _) sc)
16021646 = let tcs' = case unApply ty of
1603− (P _ c _, _) ->
1647+ (P _ c _, _) ->
16041648 case lookupCtxtExact c (idris_classes ist) of
1605− Just tc -> ((ty, map fst (class_instances tc))
1606− : tcs)
1649+ Just tc -> ((ty, map fst (class_instances tc))
1650+ : tcs)
16071651 Nothing -> tcs
1608− _ -> tcs
1652+ _ -> tcs
16091653 in
16101654 collectConstraints (n : env) tcs' sc
16111655 collectConstraints env tcs t
@@ -1625,7 +1669,7 @@ findHighlight n = do ctxt <- get_context
16251669
16261670-- Try again to solve auto implicits
16271671solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()
1628−solveAuto ist fn ambigok (n, failc)
1672+solveAuto ist fn ambigok (n, failc)
16291673 = do hs <- get_holes
16301674 when (not (null hs)) $ do
16311675 env <- get_env
@@ -1638,15 +1682,15 @@ solveAuto ist fn ambigok (n, failc)
16381682 (lift $ Error (addLoc failc
16391683 (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))
16401684 return ()
1641− where addLoc (FailContext fc f x : prev) err
1642− = At fc (ElaboratingArg f x
1685+ where addLoc (FailContext fc f x : prev) err
1686+ = At fc (ElaboratingArg f x
16431687 (map (\(FailContext _ f' x') -> (f', x')) prev) err)
16441688 addLoc _ err = err
16451689
16461690 cantsolve (CantSolveGoal _ _) = True
16471691 cantsolve (InternalMsg _) = True
16481692 cantsolve (At _ e) = cantsolve e
1649− cantsolve (Elaborating _ _ e) = cantsolve e
1693+ cantsolve (Elaborating _ _ _ e) = cantsolve e
16501694 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e
16511695 cantsolve _ = False
16521696
@@ -1655,6 +1699,15 @@ solveAutos ist fn ambigok
16551699 = do autos <- get_autos
16561700 mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
16571701
1702+-- Return true if the given error suggests a type class failure is
1703+-- recoverable
1704+tcRecoverable :: ElabMode -> Err -> Bool
1705+tcRecoverable ERHS (CantResolve f g) = f
1706+tcRecoverable ETyDecl (CantResolve f g) = f
1707+tcRecoverable e (ElaboratingArg _ _ _ err) = tcRecoverable e err
1708+tcRecoverable e (At _ err) = tcRecoverable e err
1709+tcRecoverable _ _ = True
1710+
16581711trivial' ist
16591712 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
16601713trivialHoles' psn h ist
@@ -1668,38 +1721,25 @@ resolveTC' di mv depth tm n ist
16681721
16691722collectDeferred :: Maybe Name -> [Name] -> Context ->
16701723 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
1671−collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =
1672− do ds <- get
1673− t' <- collectDeferred top casenames ctxt t
1674− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])
1675− collectDeferred top casenames ctxt app
1724+collectDeferred top casenames ctxt tm = cd [] tm
16761725 where
1677− -- Evaluate the top level functions in arguments, if possible, and if it's
1678− -- not a name we're immediately going to define in a case block, so that
1679− -- any immediate specialisation of the function applied to constructors
1680− -- can be done
1681− tidyArg env (Bind n b@(Pi im t k) sc)
1682− = Bind n (Pi im (tidy ctxt env t) k)
1683− (tidyArg ((n, b) : env) sc)
1684− tidyArg env t = tidy ctxt env t
1685−
1686− tidy ctxt env t = normalise ctxt env t
1687−
1688− getFn (Bind n (Lam _) t) = getFn t
1689− getFn t | (f, a) <- unApply t = f
1690−
1691−collectDeferred top ns ctxt (Bind n b t)
1692− = do b' <- cdb b
1693− t' <- collectDeferred top ns ctxt t
1694− return (Bind n b' t')
1695− where
1696− cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1697− cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1698− cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)
1699− return (b { binderTy = ty' })
1700−collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f)
1701− (collectDeferred top ns ctxt a)
1702−collectDeferred top ns ctxt t = return t
1726+ cd env (Bind n (GHole i psns t) app) =
1727+ do ds <- get
1728+ t' <- collectDeferred top casenames ctxt t
1729+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])
1730+ cd env app
1731+ cd env (Bind n b t)
1732+ = do b' <- cdb b
1733+ t' <- cd ((n, b) : env) t
1734+ return (Bind n b' t')
1735+ where
1736+ cdb (Let t v) = liftM2 Let (cd env t) (cd env v)
1737+ cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)
1738+ cdb b = do ty' <- cd env (binderTy b)
1739+ return (b { binderTy = ty' })
1740+ cd env (App s f a) = liftM2 (App s) (cd env f)
1741+ (cd env a)
1742+ cd env t = return t
17031743
17041744case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
17051745case_ ind autoSolve ist fn tm = do
@@ -1735,14 +1775,33 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
17351775
17361776 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
17371777
1738− patvars :: [Name] -> Term -> ([Name], Term)
1739− patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)
1778+ patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)
1779+ patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
17401780 patvars ns tm = (ns, tm)
17411781
1742− pullVars :: (Term, Term) -> ([Name], Term, Term)
1782+ pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
17431783 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
17441784
1745− defineFunction :: RFunDefn -> ElabD ()
1785+ requireError :: Err -> ElabD a -> ElabD ()
1786+ requireError orErr elab =
1787+ do state <- get
1788+ case runStateT elab state of
1789+ OK (_, state') -> lift (tfail orErr)
1790+ Error e -> return ()
1791+
1792+ -- create a fake TT term for the LHS of an impossible case
1793+ fakeTT :: Raw -> Term
1794+ fakeTT (Var n) =
1795+ case lookupNameDef n (tt_ctxt ist) of
1796+ [(n', TyDecl nt _)] -> P nt n' Erased
1797+ _ -> P Ref n Erased
1798+ fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)
1799+ fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)
1800+ fakeTT RType = TType (UVar (-1))
1801+ fakeTT (RUType u) = UType u
1802+ fakeTT (RConstant c) = Constant c
1803+
1804+ defineFunction :: RFunDefn Raw -> ElabD ()
17461805 defineFunction (RDefineFun n clauses) =
17471806 do ctxt <- get_context
17481807 ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
@@ -1754,22 +1813,24 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
17541813 lift $ converts ctxt [] lty rty
17551814 return $ Right (lhs', rhs')
17561815 RMkImpossibleClause lhs ->
1757− do lhs' <- fmap fst . lift $ check ctxt [] lhs
1758− return $ Left lhs')
1816+ do requireError (Msg "Not an impossible case") . lift $
1817+ check ctxt [] lhs
1818+ return $ Left (fakeTT lhs))
17591819 let clauses'' = map (\case Right c -> pullVars c
1760− Left lhs -> let (ns, lhs') = patvars [] lhs'
1820+ Left lhs -> let (ns, lhs') = patvars [] lhs
17611821 in (ns, lhs', Impossible))
17621822 clauses'
1823+ let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''
17631824 ctxt'<- lift $
17641825 addCasedef n (const [])
17651826 info False (STerm Erased)
17661827 True False -- TODO what are these?
17671828 (map snd $ getArgTys ty) [] -- TODO inaccessible types
17681829 clauses'
1769− clauses''
1770− clauses''
1771− clauses''
1772− clauses''
1830+ clauses'''
1831+ clauses'''
1832+ clauses'''
1833+ clauses'''
17731834 ty
17741835 ctxt
17751836 set_context ctxt'
@@ -1785,10 +1846,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
17851846 -- step, the output is the (reflected) term returned.
17861847 runTacTm :: Term -> ElabD Term
17871848 runTacTm (unApply -> tac@(P _ n _, args))
1788− | n == tacN "prim__Solve", [] <- args
1849+ | n == tacN "Prim__Solve", [] <- args
17891850 = do solve
17901851 returnUnit
1791− | n == tacN "prim__Goal", [] <- args
1852+ | n == tacN "Prim__Goal", [] <- args
17921853 = do hs <- get_holes
17931854 case hs of
17941855 (h : _) -> do t <- goal
@@ -1798,27 +1859,19 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
17981859 [] -> lift . tfail . Msg $
17991860 "Elaboration is complete. There are no goals."
18001861
1801− | n == tacN "prim__Holes", [] <- args
1862+ | n == tacN "Prim__Holes", [] <- args
18021863 = do hs <- get_holes
18031864 fmap fst . checkClosed $
18041865 mkList (Var $ reflm "TTName") (map reflectName hs)
1805− | n == tacN "prim__Guess", [] <- args
1806− = do ok <- is_guess
1807− if ok
1808− then do guess <- fmap forget get_guess
1809− fmap fst . get_type_val $
1810− RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1811− (Var (reflm "TT")))
1812− guess
1813− else fmap fst . checkClosed $
1814− RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1815− (Var (reflm "TT"))
1816− | n == tacN "prim__LookupTy", [n] <- args
1866+ | n == tacN "Prim__Guess", [] <- args
1867+ = do g <- get_guess
1868+ fmap fst . checkClosed $ reflect g
1869+ | n == tacN "Prim__LookupTy", [n] <- args
18171870 = do n' <- reifyTTName n
18181871 ctxt <- get_context
1819− let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
1820− TyDecl nt ty -> (nt, ty)
1821− Operator ty _ _ -> (Ref, ty)
1872+ let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
1873+ TyDecl nt ty -> (nt, ty)
1874+ Operator ty _ _ -> (Ref, ty)
18221875 CaseOp _ ty _ _ _ _ -> (Ref, ty)
18231876 -- Idris tuples nest to the right
18241877 reflectTriple (x, y, z) =
@@ -1835,46 +1888,75 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
18351888 , raw_apply (Var pairTy) [ Var (reflm "NameType")
18361889 , Var (reflm "TT")]])
18371890 defs
1838− | n == tacN "prim__LookupDatatype", [name] <- args
1891+ | n == tacN "Prim__LookupDatatype", [name] <- args
18391892 = do n' <- reifyTTName name
18401893 datatypes <- get_datatypes
18411894 ctxt <- get_context
18421895 fmap fst . checkClosed $
18431896 rawList (Var (tacN "Datatype"))
18441897 (map reflectDatatype (buildDatatypes ist n'))
1845− | n == tacN "prim__SourceLocation", [] <- args
1898+ | n == tacN "Prim__LookupFunDefn", [name] <- args
1899+ = do n' <- reifyTTName name
1900+ fmap fst . checkClosed $
1901+ rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
1902+ (map reflectFunDefn (buildFunDefns ist n'))
1903+ | n == tacN "Prim__LookupArgs", [name] <- args
1904+ = do n' <- reifyTTName name
1905+ let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
1906+ listFunArg = RApp listTy (Var (tacN "FunArg"))
1907+ -- Idris tuples nest to the right
1908+ let reflectTriple (x, y, z) =
1909+ raw_apply (Var pairCon) [ Var (reflm "TTName")
1910+ , raw_apply (Var pairTy) [listFunArg, Var (reflm "Raw")]
1911+ , x
1912+ , raw_apply (Var pairCon) [listFunArg, Var (reflm "Raw")
1913+ , y, z]]
1914+ let out =
1915+ [ reflectTriple (reflectName fn, reflectList (Var (tacN "FunArg")) (map reflectArg args), reflectRaw res)
1916+ | (fn, pargs) <- lookupCtxtName n' (idris_implicits ist)
1917+ , (args, res) <- getArgs pargs . forget <$>
1918+ maybeToList (lookupTyExact fn (tt_ctxt ist))
1919+ ]
1920+
1921+ fmap fst . checkClosed $
1922+ rawList (raw_apply (Var pairTy) [Var (reflm "TTName")
1923+ , raw_apply (Var pairTy) [ RApp listTy
1924+ (Var (tacN "FunArg"))
1925+ , Var (reflm "Raw")]])
1926+ out
1927+ | n == tacN "Prim__SourceLocation", [] <- args
18461928 = fmap fst . checkClosed $
18471929 reflectFC fc
1848− | n == tacN "prim__Namespace", [] <- args
1930+ | n == tacN "Prim__Namespace", [] <- args
18491931 = fmap fst . checkClosed $
18501932 rawList (RConstant StrType) (map (RConstant . Str) ns)
1851− | n == tacN "prim__Env", [] <- args
1933+ | n == tacN "Prim__Env", [] <- args
18521934 = do env <- get_env
18531935 fmap fst . checkClosed $ reflectEnv env
1854− | n == tacN "prim__Fail", [_a, errs] <- args
1936+ | n == tacN "Prim__Fail", [_a, errs] <- args
18551937 = do errs' <- eval errs
18561938 parts <- reifyReportParts errs'
18571939 lift . tfail $ ReflectionError [parts] (Msg "")
1858− | n == tacN "prim__PureElab", [_a, tm] <- args
1940+ | n == tacN "Prim__PureElab", [_a, tm] <- args
18591941 = return tm
1860− | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
1942+ | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
18611943 = do first' <- eval first
18621944 res <- eval =<< runTacTm first'
18631945 next <- eval (App Complete andThen res)
18641946 runTacTm next
1865− | n == tacN "prim__Try", [_a, first, alt] <- args
1947+ | n == tacN "Prim__Try", [_a, first, alt] <- args
18661948 = do first' <- eval first
18671949 alt' <- eval alt
18681950 try' (runTacTm first') (runTacTm alt') True
1869− | n == tacN "prim__Fill", [raw] <- args
1951+ | n == tacN "Prim__Fill", [raw] <- args
18701952 = do raw' <- reifyRaw =<< eval raw
1871− fill raw'
1953+ apply raw' []
18721954 returnUnit
1873− | n == tacN "prim__Apply" || n == tacN "prim__MatchApply"
1955+ | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
18741956 , [raw, argSpec] <- args
18751957 = do raw' <- reifyRaw =<< eval raw
1876− argSpec' <- reifyList (reifyPair reifyBool reifyInt) argSpec
1877− let op = if n == tacN "prim__Apply"
1958+ argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
1959+ let op = if n == tacN "Prim__Apply"
18781960 then apply
18791961 else match_apply
18801962 ns <- op raw' argSpec'
@@ -1884,91 +1966,88 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
18841966 (reflectName n1, reflectName n2)
18851967 | (n1, n2) <- ns
18861968 ]
1887− | n == tacN "prim__Gensym", [hint] <- args
1969+ | n == tacN "Prim__Gensym", [hint] <- args
18881970 = do hintStr <- eval hint
18891971 case hintStr of
18901972 Constant (Str h) -> do
18911973 n <- getNameFrom (sMN 0 h)
18921974 fmap fst $ get_type_val (reflectName n)
18931975 _ -> fail "no hint"
1894− | n == tacN "prim__Claim", [n, ty] <- args
1976+ | n == tacN "Prim__Claim", [n, ty] <- args
18951977 = do n' <- reifyTTName n
18961978 ty' <- reifyRaw ty
18971979 claim n' ty'
18981980 returnUnit
1899− | n == tacN "prim__Check", [raw] <- args
1900− = do raw' <- reifyRaw =<< eval raw
1981+ | n == tacN "Prim__Check", [env', raw] <- args
1982+ = do env <- reifyEnv env'
1983+ raw' <- reifyRaw =<< eval raw
19011984 ctxt <- get_context
1902− env <- get_env
19031985 (tm, ty) <- lift $ check ctxt env raw'
19041986 fmap fst . checkClosed $
19051987 rawPair (Var (reflm "TT"), Var (reflm "TT"))
19061988 (reflect tm, reflect ty)
1907− | n == tacN "prim__Forget", [tt] <- args
1908− = do tt' <- reifyTT tt
1909− fmap fst . checkClosed . reflectRaw $ forget tt'
1910− | n == tacN "prim__Attack", [] <- args
1989+ | n == tacN "Prim__Attack", [] <- args
19111990 = do attack
19121991 returnUnit
1913− | n == tacN "prim__Rewrite", [rule] <- args
1992+ | n == tacN "Prim__Rewrite", [rule] <- args
19141993 = do r <- reifyRaw rule
19151994 rewrite r
19161995 returnUnit
1917− | n == tacN "prim__Focus", [what] <- args
1996+ | n == tacN "Prim__Focus", [what] <- args
19181997 = do n' <- reifyTTName what
19191998 hs <- get_holes
19201999 if elem n' hs
19212000 then focus n' >> returnUnit
19222001 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
1923− | n == tacN "prim__Unfocus", [what] <- args
2002+ | n == tacN "Prim__Unfocus", [what] <- args
19242003 = do n' <- reifyTTName what
19252004 movelast n'
19262005 returnUnit
1927− | n == tacN "prim__Intro", [mn] <- args
2006+ | n == tacN "Prim__Intro", [mn] <- args
19282007 = do n <- case fromTTMaybe mn of
19292008 Nothing -> return Nothing
19302009 Just name -> fmap Just $ reifyTTName name
19312010 intro n
19322011 returnUnit
1933− | n == tacN "prim__Forall", [n, ty] <- args
2012+ | n == tacN "Prim__Forall", [n, ty] <- args
19342013 = do n' <- reifyTTName n
19352014 ty' <- reifyRaw ty
19362015 forall n' Nothing ty'
19372016 returnUnit
1938− | n == tacN "prim__PatVar", [n] <- args
2017+ | n == tacN "Prim__PatVar", [n] <- args
19392018 = do n' <- reifyTTName n
19402019 patvar' n'
19412020 returnUnit
1942− | n == tacN "prim__PatBind", [n] <- args
2021+ | n == tacN "Prim__PatBind", [n] <- args
19432022 = do n' <- reifyTTName n
19442023 patbind n'
19452024 returnUnit
1946− | n == tacN "prim__LetBind", [n, ty, tm] <- args
2025+ | n == tacN "Prim__LetBind", [n, ty, tm] <- args
19472026 = do n' <- reifyTTName n
19482027 ty' <- reifyRaw ty
19492028 tm' <- reifyRaw tm
19502029 letbind n' ty' tm'
19512030 returnUnit
1952− | n == tacN "prim__Compute", [] <- args
2031+ | n == tacN "Prim__Compute", [] <- args
19532032 = do compute ; returnUnit
1954− | n == tacN "prim__Normalise", [env, tm] <- args
2033+ | n == tacN "Prim__Normalise", [env, tm] <- args
19552034 = do env' <- reifyEnv env
19562035 tm' <- reifyTT tm
19572036 ctxt <- get_context
19582037 let out = normaliseAll ctxt env' (finalise tm')
19592038 fmap fst . checkClosed $ reflect out
1960− | n == tacN "prim__Whnf", [tm] <- args
2039+ | n == tacN "Prim__Whnf", [tm] <- args
19612040 = do tm' <- reifyTT tm
19622041 ctxt <- get_context
19632042 fmap fst . checkClosed . reflect $ whnf ctxt tm'
1964− | n == tacN "prim__Converts", [env, tm1, tm2] <- args
2043+ | n == tacN "Prim__Converts", [env, tm1, tm2] <- args
19652044 = do env' <- reifyEnv env
19662045 tm1' <- reifyTT tm1
19672046 tm2' <- reifyTT tm2
19682047 ctxt <- get_context
19692048 lift $ converts ctxt env' tm1' tm2'
19702049 returnUnit
1971− | n == tacN "prim__DeclareType", [decl] <- args
2050+ | n == tacN "Prim__DeclareType", [decl] <- args
19722051 = do (RDeclare n args res) <- reifyTyDecl decl
19732052 ctxt <- get_context
19742053 let mkPi arg res = RBind (argName arg)
@@ -1990,24 +2069,28 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
19902069 set_context ctxt'
19912070 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
19922071 new_tyDecls e }
1993− aux <- getAux
19942072 returnUnit
1995− | n == tacN "prim__DefineFunction", [decl] <- args
2073+ | n == tacN "Prim__DefineFunction", [decl] <- args
19962074 = do defn <- reifyFunDefn decl
19972075 defineFunction defn
19982076 returnUnit
1999− | n == tacN "prim__AddInstance", [cls, inst] <- args
2077+ | n == tacN "Prim__AddInstance", [cls, inst] <- args
20002078 = do className <- reifyTTName cls
20012079 instName <- reifyTTName inst
20022080 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
20032081 new_tyDecls e}
20042082 returnUnit
2005− | n == tacN "prim__ResolveTC", [fn] <- args
2083+ | n == tacN "Prim__IsTCName", [n] <- args
2084+ = do n' <- reifyTTName n
2085+ case lookupCtxtExact n' (idris_classes ist) of
2086+ Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
2087+ Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2088+ | n == tacN "Prim__ResolveTC", [fn] <- args
20062089 = do g <- goal
20072090 fn <- reifyTTName fn
20082091 resolveTC' False True 100 g fn ist
20092092 returnUnit
2010− | n == tacN "prim__Search", [depth, hints] <- args
2093+ | n == tacN "Prim__Search", [depth, hints] <- args
20112094 = do d <- eval depth
20122095 hints' <- eval hints
20132096 case (d, unList hints') of
@@ -2020,7 +2103,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20202103 (Constant (I _), Nothing ) ->
20212104 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
20222105 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
2023− | n == tacN "prim__RecursiveElab", [goal, script] <- args
2106+ | n == tacN "Prim__RecursiveElab", [goal, script] <- args
20242107 = do goal' <- reifyRaw goal
20252108 ctxt <- get_context
20262109 script <- eval script
@@ -2030,22 +2113,28 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20302113 aux <- getAux
20312114 datatypes <- get_datatypes
20322115 env <- get_env
2033− (_, ES (p, aux') _ _) <-
2116+
2117+ (ctxt', ES (p, aux') _ _) <-
20342118 do (ES (current_p, _) _ _) <- get
2035− lift $ runElab aux (runElabAction ist fc [] script ns)
2036− ((newProof recH ctxt datatypes goalTT)
2037− { nextname = nextname current_p})
2119+ lift $ runElab aux
2120+ (do runElabAction ist fc [] script ns
2121+ ctxt' <- get_context
2122+ return ctxt')
2123+ ((newProof recH ctxt datatypes goalTT)
2124+ { nextname = nextname current_p })
2125+ set_context ctxt'
2126+
20382127 let tm_out = getProofTerm (pterm p)
20392128 do (ES (prf, _) s e) <- get
20402129 let p' = prf { nextname = nextname p }
20412130 put (ES (p', aux') s e)
20422131 env' <- get_env
2043− (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
2132+ (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out
20442133 let (tm', ty') = (reflect tm, reflect ty)
20452134 fmap fst . checkClosed $
20462135 rawPair (Var $ reflm "TT", Var $ reflm "TT")
20472136 (tm', ty')
2048− | n == tacN "prim__Metavar", [n] <- args
2137+ | n == tacN "Prim__Metavar", [n] <- args
20492138 = do n' <- reifyTTName n
20502139 ctxt <- get_context
20512140 ptm <- get_term
@@ -2056,10 +2145,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20562145 defer unique_used mvn
20572146 solve
20582147 returnUnit
2059− | n == tacN "prim__Fixity", [op'] <- args
2148+ | n == tacN "Prim__Fixity", [op'] <- args
20602149 = do opTm <- eval op'
20612150 case opTm of
2062− Constant (Str op) ->
2151+ Constant (Str op) ->
20632152 let opChars = ":!#$%&*+./<=>?@\\^|-~"
20642153 invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
20652154 fixities = idris_infixes ist
@@ -2070,7 +2159,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20702159 [f] -> fmap fst . checkClosed $ reflectFixity f
20712160 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
20722161 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
2073− | n == tacN "prim__Debug", [ty, msg] <- args
2162+ | n == tacN "Prim__Debug", [ty, msg] <- args
20742163 = do msg' <- eval msg
20752164 parts <- reifyReportParts msg
20762165 debugElaborator parts
@@ -2096,7 +2185,7 @@ runTac autoSolve ist perhapsFC fn tac
20962185 bname _ = Nothing
20972186 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
20982187 runT Intros = do g <- goal
2099− attack;
2188+ attack;
21002189 intro (bname g)
21012190 try' (runT Intros)
21022191 (return ()) True
@@ -2341,18 +2430,18 @@ elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
23412430withErrorReflection :: Idris a -> Idris a
23422431withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
23432432 where handle :: Err -> Idris Err
2344− handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"
2433+ handle e@(ReflectionError _ _) = do logElab 3 "Skipping reflection of error reflection result"
23452434 return e -- Don't do meta-reflection of errors
2346− handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
2435+ handle e@(ReflectionFailed _ _) = do logElab 3 "Skipping reflection of reflection failure"
23472436 return e
23482437 -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
2349− handle e@(At fc err) = do logLvl 3 "Reflecting body of At"
2438+ handle e@(At fc err) = do logElab 3 "Reflecting body of At"
23502439 err' <- handle err
23512440 return (At fc err')
2352− handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
2353− err' <- handle err
2354− return (Elaborating what n err')
2355− handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
2441+ handle e@(Elaborating what n ty err) = do logElab 3 "Reflecting body of Elaborating"
2442+ err' <- handle err
2443+ return (Elaborating what n ty err')
2444+ handle e@(ElaboratingArg f a prev err) = do logElab 3 "Reflecting body of ElaboratingArg"
23562445 hs <- getFnHandlers f a
23572446 err' <- if null hs
23582447 then handle err
@@ -2362,8 +2451,8 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
23622451 handle (ProofSearchFail e) = handle e
23632452 -- TODO: argument-specific error handlers go here for ElaboratingArg
23642453 handle e = do ist <- getIState
2365− logLvl 2 "Starting error reflection"
2366− logLvl 5 (show e)
2454+ logElab 2 "Starting error reflection"
2455+ logElab 5 (show e)
23672456 let handlers = idris_errorhandlers ist
23682457 applyHandlers e handlers
23692458 getFnHandlers :: Name -> Name -> Idris [Name]
@@ -2377,7 +2466,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
23772466 applyHandlers e handlers =
23782467 do ist <- getIState
23792468 let err = fmap (errReverse ist) e
2380− logLvl 3 $ "Using reflection handlers " ++
2469+ logElab 3 $ "Using reflection handlers " ++
23812470 concat (intersperse ", " (map show handlers))
23822471 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
23832472
@@ -2389,7 +2478,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
23892478 -- Normalize error handler terms to produce the new messages
23902479 ctxt <- getContext
23912480 let results = map (normalise ctxt []) (map fst handlers)
2392− logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
2481+ logElab 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
23932482
23942483 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
23952484 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
@@ -2410,8 +2499,8 @@ processTacticDecls info steps =
24102499 -- establish metavars that later function bodies resolve.
24112500 forM_ (reverse steps) $ \case
24122501 RTyDeclInstrs n fc impls ty ->
2413− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
2414− logLvl 3 $ " It has impls " ++ show impls
2502+ do logElab 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
2503+ logElab 3 $ " It has impls " ++ show impls
24152504 updateIState $ \i -> i { idris_implicits =
24162505 addDef n impls (idris_implicits i) }
24172506 addIBC (IBCImp n)
@@ -2428,13 +2517,13 @@ processTacticDecls info steps =
24282517 in addDeferred ds'
24292518 _ -> return ()
24302519 RAddInstance className instName ->
2431− do -- The type class resolution machinery relies on a special
2432− logLvl 2 $ "Adding elab script instance " ++ show instName ++
2520+ do -- The type class resolution machinery relies on a special
2521+ logElab 2 $ "Adding elab script instance " ++ show instName ++
24332522 " for " ++ show className
24342523 addInstance False True className instName
24352524 addIBC (IBCInstance False True className instName)
24362525 RClausesInstrs n cs ->
2437− do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n
2526+ do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n
24382527 solveDeferred n
24392528 let lhss = map (\(_, lhs, _) -> lhs) cs
24402529 let fc = fileFC "elab_reflected"
@@ -2464,7 +2553,7 @@ processTacticDecls info steps =
24642553 calls = findCalls sc' scargs
24652554 used = findUsedArgs sc' scargs'
24662555 cg = CGInfo scargs' calls [] used []
2467− in do logLvl 2 $ "Called names in reflected elab: " ++ show cg
2556+ in do logElab 2 $ "Called names in reflected elab: " ++ show cg
24682557 addToCG n cg
24692558 addToCalledG n (nub (map fst calls))
24702559 addIBC $ IBCCG n
@@ -2493,7 +2582,8 @@ processTacticDecls info steps =
24932582 let fc = fileFC "elab_reflected_totality"
24942583 let tcgen = False -- TODO: later we may support dictionary generation
24952584 case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState
2496− (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of
2585+ (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)
2586+ (infTerm lhs))) of
24972587 OK (ElabResult lhs' _ _ _ _ _, _) ->
24982588 do -- not recursively calling here, because we don't
24992589 -- want to run infinitely many times