@@ -28,9 +28,10 @@ import qualified Util.Pretty as U
28import Control.Applicative ((<$>))
28import Control.Applicative ((<$>))
29import Control.Monad
29import Control.Monad
30import Control.Monad.State.Strict
30import Control.Monad.State.Strict
31+import Data.Foldable (for_)
31import Data.List
32import Data.List
32import qualified Data.Map as M
33import qualified Data.Map as M
33−import Data.Maybe (mapMaybe, fromMaybe, catMaybes)
34+import Data.Maybe (mapMaybe, fromMaybe, catMaybes, maybeToList)
34import qualified Data.Set as S
35import qualified Data.Set as S
35import qualified Data.Text as T
36import qualified Data.Text as T
@@ -90,7 +91,7 @@ build ist info emode opts fn tm
91 ptm <- get_term
92 ptm <- get_term
92 resolveTC' True True 10 g fn ist) ivs
93 resolveTC' True True 10 g fn ist) ivs
94 when (not pattern) $ solveAutos ist fn False
95 when (not pattern) $ solveAutos ist fn False
96 tm <- get_term
97 tm <- get_term
@@ -137,15 +138,16 @@ build ist info emode opts fn tm
137-- (Separate, so we don't go overboard resolving things that we don't
138-- (Separate, so we don't go overboard resolving things that we don't
138-- know about yet on the LHS of a pattern def)
139-- know about yet on the LHS of a pattern def)
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
141 ElabD ElabResult
144 ElabD ElabResult
142−buildTC ist info emode opts fn tm
145+buildTC ist info emode opts fn ns tm
143− = do -- set name supply to begin after highest index in tm
144− let ns = allNamesIn tm
145− let tmIn = tm
146+ = do let tmIn = tm
146 let inf = case lookupCtxt fn (idris_tyinfodata ist) of
147 let inf = case lookupCtxt fn (idris_tyinfodata ist) of
147 [TIPartial] -> True
148 [TIPartial] -> True
148 _ -> False
149 _ -> False
150+ -- set name supply to begin after highest index in tm
149 initNextNameFrom ns
151 initNextNameFrom ns
150 elab ist info emode opts fn tm
152 elab ist info emode opts fn tm
151 probs <- get_probs
153 probs <- get_probs
@@ -169,7 +171,7 @@ buildTC ist info emode opts fn tm
169 else return (ElabResult tm ds (map snd is) ctxt impls highlights)
171 else return (ElabResult tm ds (map snd is) ctxt impls highlights)
170 where pattern = emode == ELHS
172 where pattern = emode == ELHS
172−-- return whether arguments of the given constructor name can be
174+-- return whether arguments of the given constructor name can be
173-- matched on. If they're polymorphic, no, unless the type has beed made
175-- matched on. If they're polymorphic, no, unless the type has beed made
174-- concrete by the time we get around to elaborating the argument.
176-- concrete by the time we get around to elaborating the argument.
175getUnmatchable :: Context -> Name -> [Bool]
177getUnmatchable :: Context -> Name -> [Bool]
@@ -178,11 +180,11 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
178 Nothing -> []
180 Nothing -> []
179 Just ty -> checkArgs [] [] ty
181 Just ty -> checkArgs [] [] ty
180 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
182 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
181− checkArgs env ns (Bind n (Pi _ t _) sc)
183+ checkArgs env ns (Bind n (Pi _ t _) sc)
182 = let env' = case t of
184 = let env' = case t of
183 TType _ -> n : env
185 TType _ -> n : env
184 _ -> env in
186 _ -> env in
185− checkArgs env' (intersect env (refsIn t) : ns)
187+ checkArgs env' (intersect env (refsIn t) : ns)
186 (instantiate (P Bound n t) sc)
188 (instantiate (P Bound n t) sc)
187 checkArgs env ns t
189 checkArgs env ns t
188 = map (not . null) (reverse ns)
190 = map (not . null) (reverse ns)
@@ -191,7 +193,7 @@ getUnmatchable ctxt n = []
192data ElabCtxt = ElabCtxt { e_inarg :: Bool,
194data ElabCtxt = ElabCtxt { e_inarg :: Bool,
193 e_isfn :: Bool, -- ^ Function part of application
195 e_isfn :: Bool, -- ^ Function part of application
194− e_guarded :: Bool,
196+ e_guarded :: Bool,
195 e_intype :: Bool,
197 e_intype :: Bool,
196 e_qq :: Bool,
198 e_qq :: Bool,
197 e_nomatching :: Bool -- ^ can't pattern match
199 e_nomatching :: Bool -- ^ can't pattern match
@@ -265,17 +267,17 @@ elab ist info emode opts fn tm
265 -- normally correct to call elabE - the ones that don't are desugarings
267 -- normally correct to call elabE - the ones that don't are desugarings
266 -- typically
268 -- typically
267 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
269 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
268− elabE ina fc' t =
270+ elabE ina fc' t =
269 do solved <- get_recents
271 do solved <- get_recents
270 as <- get_autos
272 as <- get_autos
271 hs <- get_holes
273 hs <- get_holes
272 -- If any of the autos use variables which have recently been solved,
274 -- If any of the autos use variables which have recently been solved,
273 -- have another go at solving them now.
275 -- have another go at solving them now.
274− mapM_ (\(a, (failc, ns)) ->
276+ mapM_ (\(a, (failc, ns)) ->
275 if any (\n -> n `elem` solved) ns && head hs /= a
277 if any (\n -> n `elem` solved) ns && head hs /= a
276 then solveAuto ist fn False (a, failc)
278 then solveAuto ist fn False (a, failc)
277 else return ()) as
279 else return ()) as
279 itm <- if not pattern then insertImpLam ina t else return t
281 itm <- if not pattern then insertImpLam ina t else return t
280 ct <- insertCoerce ina itm
282 ct <- insertCoerce ina itm
281 t' <- insertLazy ct
283 t' <- insertLazy ct
@@ -308,7 +310,7 @@ elab ist info emode opts fn tm
308 forceErr orig env (InfiniteUnify _ t _)
310 forceErr orig env (InfiniteUnify _ t _)
309 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
311 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
310 ht == txt "Lazy'" = notDelay orig
312 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
312 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
314 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
313 forceErr orig env (At _ t) = forceErr orig env t
315 forceErr orig env (At _ t) = forceErr orig env t
314 forceErr orig env t = False
316 forceErr orig env t = False
@@ -341,7 +343,7 @@ elab ist info emode opts fn tm
341-- elab' (_,_,inty) (PConstant c)
343-- elab' (_,_,inty) (PConstant c)
342-- | constType c && pattern && not reflection && not inty
344-- | constType c && pattern && not reflection && not inty
343-- = lift $ tfail (Msg "Typecase is not allowed")
345-- = lift $ tfail (Msg "Typecase is not allowed")
344− elab' ina fc tm@(PConstant fc' c)
346+ elab' ina fc tm@(PConstant fc' c)
345 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
347 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
346 && isTypeConst c
348 && isTypeConst c
347 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
349 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
@@ -361,7 +363,7 @@ elab ist info emode opts fn tm
361 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
363 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
362 = do g <- goal; resolveTC' False False 5 g fn ist
364 = do g <- goal; resolveTC' False False 5 g fn ist
363 elab' ina fc (PResolveTC fc')
365 elab' ina fc (PResolveTC fc')
364− = do c <- getNameFrom (sMN 0 "class")
366+ = do c <- getNameFrom (sMN 0 "__class")
365 instanceArg c
367 instanceArg c
366 -- Elaborate the equality type first homogeneously, then
368 -- Elaborate the equality type first homogeneously, then
367 -- heterogeneously as a fallback
369 -- heterogeneously as a fallback
@@ -395,7 +397,7 @@ elab ist info emode opts fn tm
395 UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)
397 UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)
396 [pexp l,pexp r])
398 [pexp l,pexp r])
397 _ -> case tc of
399 _ -> case tc of
398− P _ n _ | n == upairTy
400+ P _ n _ | n == upairTy
399 -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)
401 -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)
400 [pimp (sUN "A") Placeholder False,
402 [pimp (sUN "A") Placeholder False,
401 pimp (sUN "B") Placeholder False,
403 pimp (sUN "B") Placeholder False,
@@ -442,16 +444,17 @@ elab ist info emode opts fn tm
442 uns <- get_usedns
444 uns <- get_usedns
443 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
445 let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
444 (h : hs) <- get_holes
446 (h : hs) <- get_holes
445−-- trace (show (map showHd as')) $
446 ty <- goal
447 ty <- goal
447 case as' of
448 case as' of
449+ [] -> do hds <- mapM showHd as
448− [] -> lift $ tfail $ NoValidAlts (map showHd as)
450+ lift $ tfail $ NoValidAlts hds
449 [x] -> elab' ina fc x
451 [x] -> elab' ina fc x
450 -- If there's options, try now, and if that fails, postpone
452 -- If there's options, try now, and if that fails, postpone
451 -- to later.
453 -- to later.
452 _ -> handleError isAmbiguous
454 _ -> handleError isAmbiguous
455+ (do hds <- mapM showHd as'
453− (tryAll (zip (map (elab' ina fc) as')
456+ tryAll (zip (map (elab' ina fc) as')
454− (map showHd as')))
457+ hds))
455 (do movelast h
458 (do movelast h
456 delayElab 5 $ do
459 delayElab 5 $ do
457 hs <- get_holes
460 hs <- get_holes
@@ -460,16 +463,17 @@ elab ist info emode opts fn tm
460 as'' <- doPrune as'
463 as'' <- doPrune as'
461 case as'' of
464 case as'' of
462 [x] -> elab' ina fc x
465 [x] -> elab' ina fc x
466+ _ -> do hds <- mapM showHd as''
463− _ -> tryAll (zip (map (elab' ina fc) as'')
467+ tryAll (zip (map (elab' ina fc) as'')
464− (map showHd as'')))
468+ hds))
465 where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])
469 where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])
466 | l == txt "Delay" = showHd (getTm arg)
470 | l == txt "Delay" = showHd (getTm arg)
467− showHd (PApp _ (PRef _ _ n) _) = n
471+ showHd (PApp _ (PRef _ _ n) _) = return n
468− showHd (PRef _ _ n) = n
472+ showHd (PRef _ _ n) = return n
469 showHd (PApp _ h _) = showHd h
473 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
472− doPrune as =
476+ doPrune as =
473 do compute
477 do compute
474 ty <- goal
478 ty <- goal
475 let (tc, _) = unApply (unDelay ty)
479 let (tc, _) = unApply (unDelay ty)
@@ -479,10 +483,9 @@ elab ist info emode opts fn tm
479 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
483 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
480 l == txt "Lazy'" = unDelay arg
484 l == txt "Lazy'" = unDelay arg
481 | otherwise = t
485 | otherwise = t
484 isAmbiguous (CantResolveAlts _) = delayok
487 isAmbiguous (CantResolveAlts _) = delayok
485− isAmbiguous (Elaborating _ _ e) = isAmbiguous e
488+ isAmbiguous (Elaborating _ _ _ e) = isAmbiguous e
486 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e
489 isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e
487 isAmbiguous (At _ e) = isAmbiguous e
490 isAmbiguous (At _ e) = isAmbiguous e
488 isAmbiguous _ = False
491 isAmbiguous _ = False
@@ -506,7 +509,7 @@ elab ist info emode opts fn tm
506 ty <- goal
509 ty <- goal
507 let doelab = elab' ina fc orig
510 let doelab = elab' ina fc orig
508 tryCatch doelab
511 tryCatch doelab
509− (\err ->
512+ (\err ->
510 if recoverableErr err
513 if recoverableErr err
511 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++
514 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++
512 -- show alts ++ "\n" ++
515 -- show alts ++ "\n" ++
@@ -544,7 +547,7 @@ elab ist info emode opts fn tm
544 pruneAlts err alts _ = filter isLend alts
547 pruneAlts err alts _ = filter isLend alts
546 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'
549 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) _)
548 = case lookupTyExact a (tt_ctxt ist) of
551 = case lookupTyExact a (tt_ctxt ist) of
549 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in
552 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in
550 any (fnIs n) args
553 any (fnIs n) args
@@ -659,7 +662,7 @@ elab ist info emode opts fn tm
659 introTy (Var tyn) (Just n)
662 introTy (Var tyn) (Just n)
660 addPSname n -- okay for proof search
663 addPSname n -- okay for proof search
661 focus tyn
664 focus tyn
663 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
666 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
664 elabE (ec { e_inarg = True }) (Just fc) sc
667 elabE (ec { e_inarg = True }) (Just fc) sc
@@ -698,10 +701,10 @@ elab ist info emode opts fn tm
698 Placeholder -> return ()
701 Placeholder -> return ()
699 _ -> do focus tyn
702 _ -> do focus tyn
700 explicit tyn
703 explicit tyn
701− elabE (ina { e_inarg = True, e_intype = True })
704+ elabE (ina { e_inarg = True, e_intype = True })
702 (Just fc) ty
705 (Just fc) ty
703 focus valn
706 focus valn
704− elabE (ina { e_inarg = True, e_intype = True })
707+ elabE (ina { e_inarg = True, e_intype = True })
705 (Just fc) val
708 (Just fc) val
706 ivs' <- get_instances
709 ivs' <- get_instances
707 env <- get_env
710 env <- get_env
@@ -711,8 +714,9 @@ elab ist info emode opts fn tm
711 g <- goal
714 g <- goal
712 hs <- get_holes
715 hs <- get_holes
713 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
716 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
717+ then handleError (tcRecoverable emode)
714− then try (resolveTC' True False 10 g fn ist)
718+ (resolveTC' True False 10 g fn ist)
715− (movelast n)
719+ (movelast n)
716 else movelast n)
720 else movelast n)
717 (ivs' \\ ivs)
721 (ivs' \\ ivs)
718 -- HACK: If the name leaks into its type, it may leak out of
722 -- HACK: If the name leaks into its type, it may leak out of
@@ -804,14 +808,14 @@ elab ist info emode opts fn tm
804 annot <- findHighlight f
808 annot <- findHighlight f
805 mapM_ checkKnownImplicit args_in
809 mapM_ checkKnownImplicit args_in
806 let args = insertScopedImps fc (normalise ctxt env fty) args_in
810 let args = insertScopedImps fc (normalise ctxt env fty) args_in
807− let unmatchableArgs = if pattern
811+ let unmatchableArgs = if pattern
808 then getUnmatchable (tt_ctxt ist) f
812 then getUnmatchable (tt_ctxt ist) f
810−-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
814+-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
811 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
815 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
812 && isTConName f (tt_ctxt ist)) $
816 && isTConName f (tt_ctxt ist)) $
813 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
817 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)) $
815 if (f `elem` map fst env && length args == 1 && length args_in == 1)
819 if (f `elem` map fst env && length args == 1 && length args_in == 1)
816 then -- simple app, as below
820 then -- simple app, as below
817 do simple_app False
821 do simple_app False
@@ -849,7 +853,7 @@ elab ist info emode opts fn tm
849 mapM (uncurry highlightSource) $
853 mapM (uncurry highlightSource) $
850 (ffc, annot) : map (\f -> (f, annot)) hls
854 (ffc, annot) : map (\f -> (f, annot)) hls
852− elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
856+ elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
853 [] fc False f
857 [] fc False f
854 (zip ns (unmatchableArgs ++ repeat False))
858 (zip ns (unmatchableArgs ++ repeat False))
855 (f == sUN "Force")
859 (f == sUN "Force")
@@ -876,26 +880,27 @@ elab ist info emode opts fn tm
876 ivs' <- get_instances
880 ivs' <- get_instances
877 -- Attempt to resolve any type classes which have 'complete' types,
881 -- Attempt to resolve any type classes which have 'complete' types,
878 -- i.e. no holes in them
882 -- i.e. no holes in them
879− when (not pattern || (e_inarg ina && not tcgen &&
883+ when (not pattern || (e_inarg ina && not tcgen &&
880 not (e_guarded ina))) $
884 not (e_guarded ina))) $
881 mapM_ (\n -> do focus n
885 mapM_ (\n -> do focus n
882 g <- goal
886 g <- goal
883 env <- get_env
887 env <- get_env
884 hs <- get_holes
888 hs <- get_holes
885 if all (\n -> not (n `elem` hs)) (freeNames g)
889 if all (\n -> not (n `elem` hs)) (freeNames g)
890+ then handleError (tcRecoverable emode)
886− then try (resolveTC' False False 10 g fn ist)
891+ (resolveTC' False False 10 g fn ist)
887 (movelast n)
892 (movelast n)
888 else movelast n)
893 else movelast n)
889 (ivs' \\ ivs)
894 (ivs' \\ ivs)
890 return []
895 return []
892 -- Run the elaborator, which returns how many implicit
897 -- Run the elaborator, which returns how many implicit
893 -- args were needed, then run it again with those args. We need
898 -- args were needed, then run it again with those args. We need
894 -- this because we have to elaborate the whole application to
899 -- this because we have to elaborate the whole application to
895 -- find out whether any computations have caused more implicits
900 -- find out whether any computations have caused more implicits
896 -- to be needed.
901 -- to be needed.
897 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
902 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
898− implicitApp elab
903+ implicitApp elab
899 | pattern || intransform = do elab; return ()
904 | pattern || intransform = do elab; return ()
900 | otherwise
905 | otherwise
901 = do s <- get
906 = do s <- get
@@ -904,7 +909,7 @@ elab ist info emode opts fn tm
904 [] -> return ()
909 [] -> return ()
905 es -> do put s
910 es -> do put s
906 elab' ina topfc (PAppImpl tm es)
911 elab' ina topfc (PAppImpl tm es)
908 checkKnownImplicit imp
913 checkKnownImplicit imp
909 | UnknownImp `elem` argopts imp
914 | UnknownImp `elem` argopts imp
910 = lift $ tfail $ UnknownImplicit (pname imp) f
915 = lift $ tfail $ UnknownImplicit (pname imp) f
@@ -961,7 +966,7 @@ elab ist info emode opts fn tm
961 headRef (PAlternative _ _ as) = all headRef as
966 headRef (PAlternative _ _ as) = all headRef as
962 headRef _ = False
967 headRef _ = False
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...
966 where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits
971 where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits
967 appImpl (e : es) = simple_app False
972 appImpl (e : es) = simple_app False
@@ -1023,12 +1028,22 @@ elab ist info emode opts fn tm
1024 elab' ina _ c@(PCase fc scr opts)
1029 elab' ina _ c@(PCase fc scr opts)
1025 = do attack
1030 = do attack
1026 tyn <- getNameFrom (sMN 0 "scty")
1032 tyn <- getNameFrom (sMN 0 "scty")
1027 claim tyn RType
1033 claim tyn RType
1028 valn <- getNameFrom (sMN 0 "scval")
1034 valn <- getNameFrom (sMN 0 "scval")
1029 scvn <- getNameFrom (sMN 0 "scvar")
1035 scvn <- getNameFrom (sMN 0 "scvar")
1030 claim valn (Var tyn)
1036 claim valn (Var tyn)
1031 letbind scvn (Var tyn) (Var valn)
1037 letbind scvn (Var tyn) (Var valn)
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)
1043+ Nothing -> return ()
1044+ Just ty -> do focus tyn
1045+ elabE ina (Just fc) ty
1032 focus valn
1047 focus valn
1033 elabE (ina { e_inarg = True }) (Just fc) scr
1048 elabE (ina { e_inarg = True }) (Just fc) scr
1034 -- Solve any remaining implicits - we need to solve as many
1049 -- Solve any remaining implicits - we need to solve as many
@@ -1041,7 +1056,7 @@ elab ist info emode opts fn tm
1042 -- Drop the unique arguments used in the term already
1057 -- Drop the unique arguments used in the term already
1043 -- and in the scrutinee (since it's
1058 -- and in the scrutinee (since it's
1044− -- not valid to use them again anyway)
1059+ -- not valid to use them again anyway)
1046 -- Also drop unique arguments which don't appear explicitly
1061 -- Also drop unique arguments which don't appear explicitly
1047 -- in either case branch so they don't count as used
1062 -- in either case branch so they don't count as used
@@ -1050,14 +1065,14 @@ elab ist info emode opts fn tm
1050 ptm <- get_term
1065 ptm <- get_term
1051 let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
1066 let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
1053− let argsDropped = filter (isUnique envU)
1068+ let argsDropped = filter (isUnique envU)
1054 (nub $ allNamesIn scr ++ inApp ptm ++
1069 (nub $ allNamesIn scr ++ inApp ptm ++
1057 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
1072 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
1060− cname' <- defer argsDropped (mkN (mkCaseName fn))
1075+ cname' <- defer argsDropped (mkN (mkCaseName fc fn))
1063 -- if the scrutinee is one of the 'args' in env, we should
1078 -- if the scrutinee is one of the 'args' in env, we should
@@ -1070,8 +1085,8 @@ elab ist info emode opts fn tm
1070 -- if we haven't got the type yet, hopefully we'll get it later!
1085 -- if we haven't got the type yet, hopefully we'll get it later!
1071 movelast tyn
1086 movelast tyn
1073− where mkCaseName (NS n ns) = NS (mkCaseName n) ns
1088+ where mkCaseName fc (NS n ns) = NS (mkCaseName fc n) ns
1074− mkCaseName n = SN (CaseN n)
1089+ mkCaseName fc n = SN (CaseN (FC' fc) n)
1075-- mkCaseName (UN x) = UN (x ++ "_case")
1090-- mkCaseName (UN x) = UN (x ++ "_case")
1076-- mkCaseName (MN i x) = MN i (x ++ "_case")
1091-- mkCaseName (MN i x) = MN i (x ++ "_case")
1077 mkN n@(NS _ _) = n
1092 mkN n@(NS _ _) = n
@@ -1079,6 +1094,21 @@ elab ist info emode opts fn tm
1079 Just xs@(_:_) -> sNS n xs
1094 Just xs@(_:_) -> sNS n xs
1097+ getScrType [] = Nothing
1098+ getScrType (f : os) = maybe (getScrType os) Just (getAppType f)
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)))
1108+ _ -> Nothing -- ambiguity is no help to us!
1109+ getAppType (PApp _ t as) = getAppType t
1110+ getAppType _ = Nothing
1082 inApp (P _ n _) = [n]
1112 inApp (P _ n _) = [n]
1083 inApp (App _ f a) = inApp f ++ inApp a
1113 inApp (App _ f a) = inApp f ++ inApp a
1084 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
1114 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
@@ -1220,12 +1250,12 @@ elab ist info emode opts fn tm
1220 [] -> lift . tfail . NoSuchVariable $ n
1250 [] -> lift . tfail . NoSuchVariable $ n
1221 more -> lift . tfail . CantResolveAlts $ map fst more
1251 more -> lift . tfail . CantResolveAlts $ map fst more
1222 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
1252 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)
1224 | reflection = elab' ina fc t
1254 | reflection = elab' ina fc t
1225 | otherwise
1255 | otherwise
1226 = do (h : hs) <- get_holes
1256 = do (h : hs) <- get_holes
1227 -- Dotting a hole means that either the hole or any outer
1257 -- 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)
1229 -- must be solvable by unification as well as being filled
1259 -- must be solvable by unification as well as being filled
1230 -- in directly.
1260 -- in directly.
1231 -- Delay dotted things to the end, then when we elaborate them
1261 -- Delay dotted things to the end, then when we elaborate them
@@ -1237,17 +1267,18 @@ elab ist info emode opts fn tm
1237 elab' ina fc (PRunElab fc' tm ns) =
1267 elab' ina fc (PRunElab fc' tm ns) =
1238 do attack
1268 do attack
1239 n <- getNameFrom (sMN 0 "tacticScript")
1269 n <- getNameFrom (sMN 0 "tacticScript")
1240− n' <- getNameFrom (sMN 0 "tacticExpr")
1241 let scriptTy = RApp (Var (sNS (sUN "Elab")
1270 let scriptTy = RApp (Var (sNS (sUN "Elab")
1242 ["Elab", "Reflection", "Language"]))
1271 ["Elab", "Reflection", "Language"]))
1243 (Var unitTy)
1272 (Var unitTy)
1244 claim n scriptTy
1273 claim n scriptTy
1246− letbind n' scriptTy (Var n)
1275+ attack -- to get an extra hole
1248 elab' ina (Just fc') tm
1276 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
1249 env <- get_env
1280 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
1252 elab' ina fc (PConstSugar constFC tm) =
1283 elab' ina fc (PConstSugar constFC tm) =
1253 -- Here we elaborate the contained term, then calculate
1284 -- Here we elaborate the contained term, then calculate
@@ -1292,7 +1323,7 @@ elab ist info emode opts fn tm
1292 -- The delayed things with lower numbered priority will be elaborated
1323 -- The delayed things with lower numbered priority will be elaborated
1293 -- first. (In practice, this means delayed alternatives, then PHidden
1324 -- first. (In practice, this means delayed alternatives, then PHidden
1294 -- things.)
1325 -- things.)
1295− delayElab pri t
1326+ delayElab pri t
1296 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })
1327 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })
1298 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
1329 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
@@ -1360,6 +1391,19 @@ elab ist info emode opts fn tm
1360 getFC d (PAlternative _ _ (x:_)) = getFC d x
1391 getFC d (PAlternative _ _ (x:_)) = getFC d x
1361 getFC d x = d
1392 getFC d x = d
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 ()
1363 insertLazy :: PTerm -> ElabD PTerm
1407 insertLazy :: PTerm -> ElabD PTerm
1364 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
1408 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
1365 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
1409 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
@@ -1396,9 +1440,9 @@ elab ist info emode opts fn tm
1396 notImplicitable _ = False
1440 notImplicitable _ = False
1398 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
1442 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
1399− | tcinstance i
1443+ | tcinstance i && not (toplevel_imp i)
1400 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
1444 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
1401− | otherwise
1445+ | not (toplevel_imp i)
1402 = pimp n Placeholder True : insertScopedImps fc sc xs
1446 = pimp n Placeholder True : insertScopedImps fc sc xs
1403 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
1447 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
1404 = x : insertScopedImps fc sc xs
1448 = x : insertScopedImps fc sc xs
@@ -1432,7 +1476,7 @@ elab ist info emode opts fn tm
1432 let t' = case (t, cs) of
1476 let t' = case (t, cs) of
1433 (PCoerced tm, _) -> tm
1477 (PCoerced tm, _) -> tm
1434 (_, []) -> t
1478 (_, []) -> t
1435− (_, cs) -> PAlternative [] TryImplicit
1479+ (_, cs) -> PAlternative [] TryImplicit
1436 (t : map (mkCoerce env t) cs)
1480 (t : map (mkCoerce env t) cs)
1437 return t'
1481 return t'
@@ -1554,7 +1598,7 @@ pruneByType env (P _ n _) ist as
1554 [] -> asV
1598 [] -> asV
1555 _ -> as'
1599 _ -> as'
1557− ctxt = tt_ctxt ist
1601+ ctxt = tt_ctxt ist
1559 headIs var f (PRef _ _ f') = typeHead var f f'
1603 headIs var f (PRef _ _ f') = typeHead var f f'
1560 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
1604 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
@@ -1573,7 +1617,7 @@ pruneByType env (P _ n _) ist as
1573 _ -> let ty' = normalise ctxt [] ty in
1617 _ -> let ty' = normalise ctxt [] ty in
1574 case unApply (getRetTy ty') of
1618 case unApply (getRetTy ty') of
1575 (P _ ftyn _, _) -> ftyn == f
1619 (P _ ftyn _, _) -> ftyn == f
1576− (V _, _) ->
1620+ (V _, _) ->
1577 -- keep, variable
1621 -- keep, variable
1578-- trace ("Keeping " ++ show (f', ty')
1622-- trace ("Keeping " ++ show (f', ty')
1579-- ++ " for " ++ show n) $
1623-- ++ " for " ++ show n) $
@@ -1590,22 +1634,22 @@ pruneByType _ t _ as = as
1590-- (FIXME: This isn't complete, but I'm leaving it here and coming back
1634-- (FIXME: This isn't complete, but I'm leaving it here and coming back
1591-- to it later - just returns 'var' for now. EB)
1635-- to it later - just returns 'var' for now. EB)
1592isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
1636isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
1593−isPlausible ist var env n ty
1637+isPlausible ist var env n ty
1594 = let (hvar, classes) = collectConstraints [] [] ty in
1638 = let (hvar, classes) = collectConstraints [] [] ty in
1595 case hvar of
1639 case hvar of
1596 Nothing -> True
1640 Nothing -> True
1597 Just rth -> var -- trace (show (rth, classes)) var
1641 Just rth -> var -- trace (show (rth, classes)) var
1599− collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
1643+ collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
1600 (Maybe Name, [(Term, [Name])])
1644 (Maybe Name, [(Term, [Name])])
1601 collectConstraints env tcs (Bind n (Pi _ ty _) sc)
1645 collectConstraints env tcs (Bind n (Pi _ ty _) sc)
1602 = let tcs' = case unApply ty of
1646 = let tcs' = case unApply ty of
1603− (P _ c _, _) ->
1647+ (P _ c _, _) ->
1604 case lookupCtxtExact c (idris_classes ist) of
1648 case lookupCtxtExact c (idris_classes ist) of
1605− Just tc -> ((ty, map fst (class_instances tc))
1649+ Just tc -> ((ty, map fst (class_instances tc))
1606− : tcs)
1650+ : tcs)
1607 Nothing -> tcs
1651 Nothing -> tcs
1608− _ -> tcs
1652+ _ -> tcs
1610 collectConstraints (n : env) tcs' sc
1654 collectConstraints (n : env) tcs' sc
1611 collectConstraints env tcs t
1655 collectConstraints env tcs t
@@ -1625,7 +1669,7 @@ findHighlight n = do ctxt <- get_context
1626-- Try again to solve auto implicits
1670-- Try again to solve auto implicits
1627solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()
1671solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()
1628−solveAuto ist fn ambigok (n, failc)
1672+solveAuto ist fn ambigok (n, failc)
1629 = do hs <- get_holes
1673 = do hs <- get_holes
1630 when (not (null hs)) $ do
1674 when (not (null hs)) $ do
1631 env <- get_env
1675 env <- get_env
@@ -1638,15 +1682,15 @@ solveAuto ist fn ambigok (n, failc)
1638 (lift $ Error (addLoc failc
1682 (lift $ Error (addLoc failc
1639 (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))
1683 (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))
1640 return ()
1684 return ()
1641− where addLoc (FailContext fc f x : prev) err
1685+ where addLoc (FailContext fc f x : prev) err
1642− = At fc (ElaboratingArg f x
1686+ = At fc (ElaboratingArg f x
1643 (map (\(FailContext _ f' x') -> (f', x')) prev) err)
1687 (map (\(FailContext _ f' x') -> (f', x')) prev) err)
1644 addLoc _ err = err
1688 addLoc _ err = err
1646 cantsolve (CantSolveGoal _ _) = True
1690 cantsolve (CantSolveGoal _ _) = True
1647 cantsolve (InternalMsg _) = True
1691 cantsolve (InternalMsg _) = True
1648 cantsolve (At _ e) = cantsolve e
1692 cantsolve (At _ e) = cantsolve e
1649− cantsolve (Elaborating _ _ e) = cantsolve e
1693+ cantsolve (Elaborating _ _ _ e) = cantsolve e
1650 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e
1694 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e
1651 cantsolve _ = False
1695 cantsolve _ = False
@@ -1655,6 +1699,15 @@ solveAutos ist fn ambigok
1655 = do autos <- get_autos
1699 = do autos <- get_autos
1656 mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
1700 mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
1702+-- Return true if the given error suggests a type class failure is
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
1658trivial' ist
1711trivial' ist
1659 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
1712 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
1660trivialHoles' psn h ist
1713trivialHoles' psn h ist
@@ -1668,38 +1721,25 @@ resolveTC' di mv depth tm n ist
1669collectDeferred :: Maybe Name -> [Name] -> Context ->
1722collectDeferred :: Maybe Name -> [Name] -> Context ->
1670 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
1723 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
1671−collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =
1724+collectDeferred top casenames ctxt tm = cd [] tm
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
1677− -- Evaluate the top level functions in arguments, if possible, and if it's
1726+ cd env (Bind n (GHole i psns t) app) =
1678− -- not a name we're immediately going to define in a case block, so that
1727+ do ds <- get
1679− -- any immediate specialisation of the function applied to constructors
1728+ t' <- collectDeferred top casenames ctxt t
1680− -- can be done
1729+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])
1681− tidyArg env (Bind n b@(Pi im t k) sc)
1731+ cd env (Bind n b t)
1682− = Bind n (Pi im (tidy ctxt env t) k)
1732+ = do b' <- cdb b
1683− (tidyArg ((n, b) : env) sc)
1733+ t' <- cd ((n, b) : env) t
1684− tidyArg env t = tidy ctxt env t
1686− tidy ctxt env t = normalise ctxt env t
1688− getFn (Bind n (Lam _) t) = getFn t
1689− getFn t | (f, a) <- unApply t = f
1691−collectDeferred top ns ctxt (Bind n b t)
1693− t' <- collectDeferred top ns ctxt t
1694− return (Bind n b' t')
1734+ return (Bind n b' t')
1696− cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1736+ cdb (Let t v) = liftM2 Let (cd env t) (cd env v)
1697− cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1737+ cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)
1698− cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)
1738+ cdb b = do ty' <- cd env (binderTy b)
1699− return (b { binderTy = ty' })
1739+ return (b { binderTy = ty' })
1700−collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f)
1740+ cd env (App s f a) = liftM2 (App s) (cd env f)
1701− (collectDeferred top ns ctxt a)
1741+ (cd env a)
1702−collectDeferred top ns ctxt t = return t
1742+ cd env t = return t
1704case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
1744case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
1705case_ ind autoSolve ist fn tm = do
1745case_ ind autoSolve ist fn tm = do
@@ -1735,14 +1775,33 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1736 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
1776 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
1738− patvars :: [Name] -> Term -> ([Name], Term)
1778+ patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)
1739− patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)
1779+ patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
1740 patvars ns tm = (ns, tm)
1780 patvars ns tm = (ns, tm)
1742− pullVars :: (Term, Term) -> ([Name], Term, Term)
1782+ pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
1743 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
1783 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
1785+ requireError :: Err -> ElabD a -> ElabD ()
1786+ requireError orErr elab =
1788+ case runStateT elab state of
1789+ OK (_, state') -> lift (tfail orErr)
1790+ Error e -> return ()
1792+ -- create a fake TT term for the LHS of an impossible case
1793+ fakeTT :: Raw -> Term
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
1745− defineFunction :: RFunDefn -> ElabD ()
1804+ defineFunction :: RFunDefn Raw -> ElabD ()
1746 defineFunction (RDefineFun n clauses) =
1805 defineFunction (RDefineFun n clauses) =
1747 do ctxt <- get_context
1806 do ctxt <- get_context
1748 ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
1807 ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
@@ -1754,22 +1813,24 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1754 lift $ converts ctxt [] lty rty
1813 lift $ converts ctxt [] lty rty
1755 return $ Right (lhs', rhs')
1814 return $ Right (lhs', rhs')
1756 RMkImpossibleClause lhs ->
1815 RMkImpossibleClause lhs ->
1816+ do requireError (Msg "Not an impossible case") . lift $
1757− do lhs' <- fmap fst . lift $ check ctxt [] lhs
1817+ check ctxt [] lhs
1758− return $ Left lhs')
1818+ return $ Left (fakeTT lhs))
1759 let clauses'' = map (\case Right c -> pullVars c
1819 let clauses'' = map (\case Right c -> pullVars c
1760− Left lhs -> let (ns, lhs') = patvars [] lhs'
1820+ Left lhs -> let (ns, lhs') = patvars [] lhs
1761 in (ns, lhs', Impossible))
1821 in (ns, lhs', Impossible))
1762 clauses'
1822 clauses'
1823+ let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''
1763 ctxt'<- lift $
1824 ctxt'<- lift $
1764 addCasedef n (const [])
1825 addCasedef n (const [])
1765 info False (STerm Erased)
1826 info False (STerm Erased)
1766 True False -- TODO what are these?
1827 True False -- TODO what are these?
1767 (map snd $ getArgTys ty) [] -- TODO inaccessible types
1828 (map snd $ getArgTys ty) [] -- TODO inaccessible types
1768 clauses'
1829 clauses'
1769− clauses''
1830+ clauses'''
1770− clauses''
1831+ clauses'''
1771− clauses''
1832+ clauses'''
1772− clauses''
1833+ clauses'''
1775 set_context ctxt'
1836 set_context ctxt'
@@ -1785,10 +1846,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1785 -- step, the output is the (reflected) term returned.
1846 -- step, the output is the (reflected) term returned.
1786 runTacTm :: Term -> ElabD Term
1847 runTacTm :: Term -> ElabD Term
1787 runTacTm (unApply -> tac@(P _ n _, args))
1848 runTacTm (unApply -> tac@(P _ n _, args))
1788− | n == tacN "prim__Solve", [] <- args
1849+ | n == tacN "Prim__Solve", [] <- args
1789 = do solve
1850 = do solve
1790 returnUnit
1851 returnUnit
1791− | n == tacN "prim__Goal", [] <- args
1852+ | n == tacN "Prim__Goal", [] <- args
1792 = do hs <- get_holes
1853 = do hs <- get_holes
1793 case hs of
1854 case hs of
1794 (h : _) -> do t <- goal
1855 (h : _) -> do t <- goal
@@ -1798,27 +1859,19 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1798 [] -> lift . tfail . Msg $
1859 [] -> lift . tfail . Msg $
1799 "Elaboration is complete. There are no goals."
1860 "Elaboration is complete. There are no goals."
1801− | n == tacN "prim__Holes", [] <- args
1862+ | n == tacN "Prim__Holes", [] <- args
1802 = do hs <- get_holes
1863 = do hs <- get_holes
1803 fmap fst . checkClosed $
1864 fmap fst . checkClosed $
1804 mkList (Var $ reflm "TTName") (map reflectName hs)
1865 mkList (Var $ reflm "TTName") (map reflectName hs)
1805− | n == tacN "prim__Guess", [] <- args
1866+ | n == tacN "Prim__Guess", [] <- args
1806− = do ok <- is_guess
1808− then do guess <- fmap forget get_guess
1867+ = do g <- get_guess
1809− fmap fst . get_type_val $
1810− RApp (RApp (Var (sNS (sUN "Just") ["Maybe", "Prelude"]))
1811− (Var (reflm "TT")))
1813− else fmap fst . checkClosed $
1868+ fmap fst . checkClosed $ reflect g
1814− RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1816− | n == tacN "prim__LookupTy", [n] <- args
1869+ | n == tacN "Prim__LookupTy", [n] <- args
1817 = do n' <- reifyTTName n
1870 = do n' <- reifyTTName n
1818 ctxt <- get_context
1871 ctxt <- get_context
1819− let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
1872+ let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
1820− TyDecl nt ty -> (nt, ty)
1873+ TyDecl nt ty -> (nt, ty)
1821− Operator ty _ _ -> (Ref, ty)
1874+ Operator ty _ _ -> (Ref, ty)
1822 CaseOp _ ty _ _ _ _ -> (Ref, ty)
1875 CaseOp _ ty _ _ _ _ -> (Ref, ty)
1823 -- Idris tuples nest to the right
1876 -- Idris tuples nest to the right
1824 reflectTriple (x, y, z) =
1877 reflectTriple (x, y, z) =
@@ -1835,46 +1888,75 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1835 , raw_apply (Var pairTy) [ Var (reflm "NameType")
1888 , raw_apply (Var pairTy) [ Var (reflm "NameType")
1836 , Var (reflm "TT")]])
1889 , Var (reflm "TT")]])
1838− | n == tacN "prim__LookupDatatype", [name] <- args
1891+ | n == tacN "Prim__LookupDatatype", [name] <- args
1839 = do n' <- reifyTTName name
1892 = do n' <- reifyTTName name
1840 datatypes <- get_datatypes
1893 datatypes <- get_datatypes
1841 ctxt <- get_context
1894 ctxt <- get_context
1842 fmap fst . checkClosed $
1895 fmap fst . checkClosed $
1843 rawList (Var (tacN "Datatype"))
1896 rawList (Var (tacN "Datatype"))
1844 (map reflectDatatype (buildDatatypes ist n'))
1897 (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")]
1912+ , raw_apply (Var pairCon) [listFunArg, Var (reflm "Raw")
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))
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")]])
1927+ | n == tacN "Prim__SourceLocation", [] <- args
1846 = fmap fst . checkClosed $
1928 = fmap fst . checkClosed $
1847 reflectFC fc
1929 reflectFC fc
1848− | n == tacN "prim__Namespace", [] <- args
1930+ | n == tacN "Prim__Namespace", [] <- args
1849 = fmap fst . checkClosed $
1931 = fmap fst . checkClosed $
1850 rawList (RConstant StrType) (map (RConstant . Str) ns)
1932 rawList (RConstant StrType) (map (RConstant . Str) ns)
1851− | n == tacN "prim__Env", [] <- args
1933+ | n == tacN "Prim__Env", [] <- args
1852 = do env <- get_env
1934 = do env <- get_env
1853 fmap fst . checkClosed $ reflectEnv env
1935 fmap fst . checkClosed $ reflectEnv env
1854− | n == tacN "prim__Fail", [_a, errs] <- args
1936+ | n == tacN "Prim__Fail", [_a, errs] <- args
1855 = do errs' <- eval errs
1937 = do errs' <- eval errs
1856 parts <- reifyReportParts errs'
1938 parts <- reifyReportParts errs'
1857 lift . tfail $ ReflectionError [parts] (Msg "")
1939 lift . tfail $ ReflectionError [parts] (Msg "")
1858− | n == tacN "prim__PureElab", [_a, tm] <- args
1940+ | n == tacN "Prim__PureElab", [_a, tm] <- args
1859 = return tm
1941 = return tm
1860− | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
1942+ | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
1861 = do first' <- eval first
1943 = do first' <- eval first
1862 res <- eval =<< runTacTm first'
1944 res <- eval =<< runTacTm first'
1863 next <- eval (App Complete andThen res)
1945 next <- eval (App Complete andThen res)
1864 runTacTm next
1946 runTacTm next
1865− | n == tacN "prim__Try", [_a, first, alt] <- args
1947+ | n == tacN "Prim__Try", [_a, first, alt] <- args
1866 = do first' <- eval first
1948 = do first' <- eval first
1867 alt' <- eval alt
1949 alt' <- eval alt
1868 try' (runTacTm first') (runTacTm alt') True
1950 try' (runTacTm first') (runTacTm alt') True
1869− | n == tacN "prim__Fill", [raw] <- args
1951+ | n == tacN "Prim__Fill", [raw] <- args
1870 = do raw' <- reifyRaw =<< eval raw
1952 = do raw' <- reifyRaw =<< eval raw
1871− fill raw'
1953+ apply raw' []
1872 returnUnit
1954 returnUnit
1873− | n == tacN "prim__Apply" || n == tacN "prim__MatchApply"
1955+ | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
1874 , [raw, argSpec] <- args
1956 , [raw, argSpec] <- args
1875 = do raw' <- reifyRaw =<< eval raw
1957 = do raw' <- reifyRaw =<< eval raw
1876− argSpec' <- reifyList (reifyPair reifyBool reifyInt) argSpec
1958+ argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
1877− let op = if n == tacN "prim__Apply"
1959+ let op = if n == tacN "Prim__Apply"
1878 then apply
1960 then apply
1879 else match_apply
1961 else match_apply
1880 ns <- op raw' argSpec'
1962 ns <- op raw' argSpec'
@@ -1884,91 +1966,88 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1884 (reflectName n1, reflectName n2)
1966 (reflectName n1, reflectName n2)
1885 | (n1, n2) <- ns
1967 | (n1, n2) <- ns
1887− | n == tacN "prim__Gensym", [hint] <- args
1969+ | n == tacN "Prim__Gensym", [hint] <- args
1888 = do hintStr <- eval hint
1970 = do hintStr <- eval hint
1889 case hintStr of
1971 case hintStr of
1890 Constant (Str h) -> do
1972 Constant (Str h) -> do
1891 n <- getNameFrom (sMN 0 h)
1973 n <- getNameFrom (sMN 0 h)
1892 fmap fst $ get_type_val (reflectName n)
1974 fmap fst $ get_type_val (reflectName n)
1893 _ -> fail "no hint"
1975 _ -> fail "no hint"
1894− | n == tacN "prim__Claim", [n, ty] <- args
1976+ | n == tacN "Prim__Claim", [n, ty] <- args
1895 = do n' <- reifyTTName n
1977 = do n' <- reifyTTName n
1896 ty' <- reifyRaw ty
1978 ty' <- reifyRaw ty
1897 claim n' ty'
1979 claim n' ty'
1898 returnUnit
1980 returnUnit
1899− | n == tacN "prim__Check", [raw] <- args
1981+ | n == tacN "Prim__Check", [env', raw] <- args
1982+ = do env <- reifyEnv env'
1900− = do raw' <- reifyRaw =<< eval raw
1983+ raw' <- reifyRaw =<< eval raw
1901 ctxt <- get_context
1984 ctxt <- get_context
1903 (tm, ty) <- lift $ check ctxt env raw'
1985 (tm, ty) <- lift $ check ctxt env raw'
1904 fmap fst . checkClosed $
1986 fmap fst . checkClosed $
1905 rawPair (Var (reflm "TT"), Var (reflm "TT"))
1987 rawPair (Var (reflm "TT"), Var (reflm "TT"))
1906 (reflect tm, reflect ty)
1988 (reflect tm, reflect ty)
1907− | n == tacN "prim__Forget", [tt] <- args
1989+ | n == tacN "Prim__Attack", [] <- args
1908− = do tt' <- reifyTT tt
1909− fmap fst . checkClosed . reflectRaw $ forget tt'
1910− | n == tacN "prim__Attack", [] <- args
1911 = do attack
1990 = do attack
1912 returnUnit
1991 returnUnit
1913− | n == tacN "prim__Rewrite", [rule] <- args
1992+ | n == tacN "Prim__Rewrite", [rule] <- args
1914 = do r <- reifyRaw rule
1993 = do r <- reifyRaw rule
1915 rewrite r
1994 rewrite r
1916 returnUnit
1995 returnUnit
1917− | n == tacN "prim__Focus", [what] <- args
1996+ | n == tacN "Prim__Focus", [what] <- args
1918 = do n' <- reifyTTName what
1997 = do n' <- reifyTTName what
1919 hs <- get_holes
1998 hs <- get_holes
1920 if elem n' hs
1999 if elem n' hs
1921 then focus n' >> returnUnit
2000 then focus n' >> returnUnit
1922 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
2001 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
1924 = do n' <- reifyTTName what
2003 = do n' <- reifyTTName what
1925 movelast n'
2004 movelast n'
1926 returnUnit
2005 returnUnit
1927− | n == tacN "prim__Intro", [mn] <- args
2006+ | n == tacN "Prim__Intro", [mn] <- args
1928 = do n <- case fromTTMaybe mn of
2007 = do n <- case fromTTMaybe mn of
1929 Nothing -> return Nothing
2008 Nothing -> return Nothing
1930 Just name -> fmap Just $ reifyTTName name
2009 Just name -> fmap Just $ reifyTTName name
1932 returnUnit
2011 returnUnit
1933− | n == tacN "prim__Forall", [n, ty] <- args
2012+ | n == tacN "Prim__Forall", [n, ty] <- args
1934 = do n' <- reifyTTName n
2013 = do n' <- reifyTTName n
1935 ty' <- reifyRaw ty
2014 ty' <- reifyRaw ty
1936 forall n' Nothing ty'
2015 forall n' Nothing ty'
1937 returnUnit
2016 returnUnit
1938− | n == tacN "prim__PatVar", [n] <- args
2017+ | n == tacN "Prim__PatVar", [n] <- args
1939 = do n' <- reifyTTName n
2018 = do n' <- reifyTTName n
1940 patvar' n'
2019 patvar' n'
1941 returnUnit
2020 returnUnit
1942− | n == tacN "prim__PatBind", [n] <- args
2021+ | n == tacN "Prim__PatBind", [n] <- args
1943 = do n' <- reifyTTName n
2022 = do n' <- reifyTTName n
1944 patbind n'
2023 patbind n'
1945 returnUnit
2024 returnUnit
1946− | n == tacN "prim__LetBind", [n, ty, tm] <- args
2025+ | n == tacN "Prim__LetBind", [n, ty, tm] <- args
1947 = do n' <- reifyTTName n
2026 = do n' <- reifyTTName n
1948 ty' <- reifyRaw ty
2027 ty' <- reifyRaw ty
1949 tm' <- reifyRaw tm
2028 tm' <- reifyRaw tm
1950 letbind n' ty' tm'
2029 letbind n' ty' tm'
1951 returnUnit
2030 returnUnit
1952− | n == tacN "prim__Compute", [] <- args
2031+ | n == tacN "Prim__Compute", [] <- args
1953 = do compute ; returnUnit
2032 = do compute ; returnUnit
1954− | n == tacN "prim__Normalise", [env, tm] <- args
2033+ | n == tacN "Prim__Normalise", [env, tm] <- args
1955 = do env' <- reifyEnv env
2034 = do env' <- reifyEnv env
1956 tm' <- reifyTT tm
2035 tm' <- reifyTT tm
1957 ctxt <- get_context
2036 ctxt <- get_context
1958 let out = normaliseAll ctxt env' (finalise tm')
2037 let out = normaliseAll ctxt env' (finalise tm')
1959 fmap fst . checkClosed $ reflect out
2038 fmap fst . checkClosed $ reflect out
1960− | n == tacN "prim__Whnf", [tm] <- args
2039+ | n == tacN "Prim__Whnf", [tm] <- args
1961 = do tm' <- reifyTT tm
2040 = do tm' <- reifyTT tm
1962 ctxt <- get_context
2041 ctxt <- get_context
1963 fmap fst . checkClosed . reflect $ whnf ctxt tm'
2042 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
1965 = do env' <- reifyEnv env
2044 = do env' <- reifyEnv env
1966 tm1' <- reifyTT tm1
2045 tm1' <- reifyTT tm1
1967 tm2' <- reifyTT tm2
2046 tm2' <- reifyTT tm2
1968 ctxt <- get_context
2047 ctxt <- get_context
1969 lift $ converts ctxt env' tm1' tm2'
2048 lift $ converts ctxt env' tm1' tm2'
1970 returnUnit
2049 returnUnit
1971− | n == tacN "prim__DeclareType", [decl] <- args
2050+ | n == tacN "Prim__DeclareType", [decl] <- args
1972 = do (RDeclare n args res) <- reifyTyDecl decl
2051 = do (RDeclare n args res) <- reifyTyDecl decl
1973 ctxt <- get_context
2052 ctxt <- get_context
1974 let mkPi arg res = RBind (argName arg)
2053 let mkPi arg res = RBind (argName arg)
@@ -1990,24 +2069,28 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1990 set_context ctxt'
2069 set_context ctxt'
1991 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
2070 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
1992 new_tyDecls e }
2071 new_tyDecls e }
1994 returnUnit
2072 returnUnit
1995− | n == tacN "prim__DefineFunction", [decl] <- args
2073+ | n == tacN "Prim__DefineFunction", [decl] <- args
1996 = do defn <- reifyFunDefn decl
2074 = do defn <- reifyFunDefn decl
1997 defineFunction defn
2075 defineFunction defn
1998 returnUnit
2076 returnUnit
1999− | n == tacN "prim__AddInstance", [cls, inst] <- args
2077+ | n == tacN "Prim__AddInstance", [cls, inst] <- args
2000 = do className <- reifyTTName cls
2078 = do className <- reifyTTName cls
2001 instName <- reifyTTName inst
2079 instName <- reifyTTName inst
2002 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2080 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2003 new_tyDecls e}
2081 new_tyDecls e}
2004 returnUnit
2082 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
2006 = do g <- goal
2089 = do g <- goal
2007 fn <- reifyTTName fn
2090 fn <- reifyTTName fn
2008 resolveTC' False True 100 g fn ist
2091 resolveTC' False True 100 g fn ist
2009 returnUnit
2092 returnUnit
2010− | n == tacN "prim__Search", [depth, hints] <- args
2093+ | n == tacN "Prim__Search", [depth, hints] <- args
2011 = do d <- eval depth
2094 = do d <- eval depth
2012 hints' <- eval hints
2095 hints' <- eval hints
2013 case (d, unList hints') of
2096 case (d, unList hints') of
@@ -2020,7 +2103,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2020 (Constant (I _), Nothing ) ->
2103 (Constant (I _), Nothing ) ->
2021 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
2104 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
2022 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
2105 (_, _) -> 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
2024 = do goal' <- reifyRaw goal
2107 = do goal' <- reifyRaw goal
2025 ctxt <- get_context
2108 ctxt <- get_context
2026 script <- eval script
2109 script <- eval script
@@ -2030,22 +2113,28 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2030 aux <- getAux
2113 aux <- getAux
2031 datatypes <- get_datatypes
2114 datatypes <- get_datatypes
2032 env <- get_env
2115 env <- get_env
2033− (_, ES (p, aux') _ _) <-
2117+ (ctxt', ES (p, aux') _ _) <-
2034 do (ES (current_p, _) _ _) <- get
2118 do (ES (current_p, _) _ _) <- get
2035− lift $ runElab aux (runElabAction ist fc [] script ns)
2120+ (do runElabAction ist fc [] script ns
2121+ ctxt' <- get_context
2036− ((newProof recH ctxt datatypes goalTT)
2123+ ((newProof recH ctxt datatypes goalTT)
2037− { nextname = nextname current_p})
2124+ { nextname = nextname current_p })
2038 let tm_out = getProofTerm (pterm p)
2127 let tm_out = getProofTerm (pterm p)
2039 do (ES (prf, _) s e) <- get
2128 do (ES (prf, _) s e) <- get
2040 let p' = prf { nextname = nextname p }
2129 let p' = prf { nextname = nextname p }
2041 put (ES (p', aux') s e)
2130 put (ES (p', aux') s e)
2042 env' <- get_env
2131 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
2044 let (tm', ty') = (reflect tm, reflect ty)
2133 let (tm', ty') = (reflect tm, reflect ty)
2045 fmap fst . checkClosed $
2134 fmap fst . checkClosed $
2046 rawPair (Var $ reflm "TT", Var $ reflm "TT")
2135 rawPair (Var $ reflm "TT", Var $ reflm "TT")
2047 (tm', ty')
2136 (tm', ty')
2048− | n == tacN "prim__Metavar", [n] <- args
2137+ | n == tacN "Prim__Metavar", [n] <- args
2049 = do n' <- reifyTTName n
2138 = do n' <- reifyTTName n
2050 ctxt <- get_context
2139 ctxt <- get_context
2051 ptm <- get_term
2140 ptm <- get_term
@@ -2056,10 +2145,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2056 defer unique_used mvn
2145 defer unique_used mvn
2058 returnUnit
2147 returnUnit
2059− | n == tacN "prim__Fixity", [op'] <- args
2148+ | n == tacN "Prim__Fixity", [op'] <- args
2060 = do opTm <- eval op'
2149 = do opTm <- eval op'
2061 case opTm of
2150 case opTm of
2062− Constant (Str op) ->
2151+ Constant (Str op) ->
2063 let opChars = ":!#$%&*+./<=>?@\\^|-~"
2152 let opChars = ":!#$%&*+./<=>?@\\^|-~"
2064 invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
2153 invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
2065 fixities = idris_infixes ist
2154 fixities = idris_infixes ist
@@ -2070,7 +2159,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2070 [f] -> fmap fst . checkClosed $ reflectFixity f
2159 [f] -> fmap fst . checkClosed $ reflectFixity f
2071 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
2160 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
2072 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
2161 _ -> 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
2074 = do msg' <- eval msg
2163 = do msg' <- eval msg
2075 parts <- reifyReportParts msg
2164 parts <- reifyReportParts msg
2076 debugElaborator parts
2165 debugElaborator parts
@@ -2096,7 +2185,7 @@ runTac autoSolve ist perhapsFC fn tac
2096 bname _ = Nothing
2185 bname _ = Nothing
2097 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
2186 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
2098 runT Intros = do g <- goal
2187 runT Intros = do g <- goal
2099− attack;
2188+ attack;
2100 intro (bname g)
2189 intro (bname g)
2101 try' (runT Intros)
2190 try' (runT Intros)
2102 (return ()) True
2191 (return ()) True
@@ -2341,18 +2430,18 @@ elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
2341withErrorReflection :: Idris a -> Idris a
2430withErrorReflection :: Idris a -> Idris a
2342withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2431withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2343 where handle :: Err -> Idris Err
2432 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"
2345 return e -- Don't do meta-reflection of errors
2434 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"
2347 return e
2436 return e
2348 -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
2437 -- 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"
2350 err' <- handle err
2439 err' <- handle err
2351 return (At fc err')
2440 return (At fc err')
2352− handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
2441+ handle e@(Elaborating what n ty err) = do logElab 3 "Reflecting body of Elaborating"
2353− err' <- handle err
2442+ err' <- handle err
2354− return (Elaborating what n err')
2443+ return (Elaborating what n ty err')
2355− handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
2444+ handle e@(ElaboratingArg f a prev err) = do logElab 3 "Reflecting body of ElaboratingArg"
2356 hs <- getFnHandlers f a
2445 hs <- getFnHandlers f a
2357 err' <- if null hs
2446 err' <- if null hs
2358 then handle err
2447 then handle err
@@ -2362,8 +2451,8 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2362 handle (ProofSearchFail e) = handle e
2451 handle (ProofSearchFail e) = handle e
2363 -- TODO: argument-specific error handlers go here for ElaboratingArg
2452 -- TODO: argument-specific error handlers go here for ElaboratingArg
2364 handle e = do ist <- getIState
2453 handle e = do ist <- getIState
2365− logLvl 2 "Starting error reflection"
2454+ logElab 2 "Starting error reflection"
2366− logLvl 5 (show e)
2455+ logElab 5 (show e)
2367 let handlers = idris_errorhandlers ist
2456 let handlers = idris_errorhandlers ist
2368 applyHandlers e handlers
2457 applyHandlers e handlers
2369 getFnHandlers :: Name -> Name -> Idris [Name]
2458 getFnHandlers :: Name -> Name -> Idris [Name]
@@ -2377,7 +2466,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2377 applyHandlers e handlers =
2466 applyHandlers e handlers =
2378 do ist <- getIState
2467 do ist <- getIState
2379 let err = fmap (errReverse ist) e
2468 let err = fmap (errReverse ist) e
2380− logLvl 3 $ "Using reflection handlers " ++
2469+ logElab 3 $ "Using reflection handlers " ++
2381 concat (intersperse ", " (map show handlers))
2470 concat (intersperse ", " (map show handlers))
2382 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
2471 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
@@ -2389,7 +2478,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2389 -- Normalize error handler terms to produce the new messages
2478 -- Normalize error handler terms to produce the new messages
2390 ctxt <- getContext
2479 ctxt <- getContext
2391 let results = map (normalise ctxt []) (map fst handlers)
2480 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))
2394 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
2483 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
2395 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
2484 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
@@ -2410,8 +2499,8 @@ processTacticDecls info steps =
2410 -- establish metavars that later function bodies resolve.
2499 -- establish metavars that later function bodies resolve.
2411 forM_ (reverse steps) $ \case
2500 forM_ (reverse steps) $ \case
2412 RTyDeclInstrs n fc impls ty ->
2501 RTyDeclInstrs n fc impls ty ->
2413− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
2502+ do logElab 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
2414− logLvl 3 $ " It has impls " ++ show impls
2503+ logElab 3 $ " It has impls " ++ show impls
2415 updateIState $ \i -> i { idris_implicits =
2504 updateIState $ \i -> i { idris_implicits =
2416 addDef n impls (idris_implicits i) }
2505 addDef n impls (idris_implicits i) }
2417 addIBC (IBCImp n)
2506 addIBC (IBCImp n)
@@ -2428,13 +2517,13 @@ processTacticDecls info steps =
2428 in addDeferred ds'
2517 in addDeferred ds'
2429 _ -> return ()
2518 _ -> return ()
2430 RAddInstance className instName ->
2519 RAddInstance className instName ->
2431− do -- The type class resolution machinery relies on a special
2520+ do -- The type class resolution machinery relies on a special
2432− logLvl 2 $ "Adding elab script instance " ++ show instName ++
2521+ logElab 2 $ "Adding elab script instance " ++ show instName ++
2433 " for " ++ show className
2522 " for " ++ show className
2434 addInstance False True className instName
2523 addInstance False True className instName
2435 addIBC (IBCInstance False True className instName)
2524 addIBC (IBCInstance False True className instName)
2436 RClausesInstrs n cs ->
2525 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
2438 solveDeferred n
2527 solveDeferred n
2439 let lhss = map (\(_, lhs, _) -> lhs) cs
2528 let lhss = map (\(_, lhs, _) -> lhs) cs
2440 let fc = fileFC "elab_reflected"
2529 let fc = fileFC "elab_reflected"
@@ -2464,7 +2553,7 @@ processTacticDecls info steps =
2464 calls = findCalls sc' scargs
2553 calls = findCalls sc' scargs
2465 used = findUsedArgs sc' scargs'
2554 used = findUsedArgs sc' scargs'
2466 cg = CGInfo scargs' calls [] used []
2555 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
2468 addToCG n cg
2557 addToCG n cg
2469 addToCalledG n (nub (map fst calls))
2558 addToCalledG n (nub (map fst calls))
2470 addIBC $ IBCCG n
2559 addIBC $ IBCCG n
@@ -2493,7 +2582,8 @@ processTacticDecls info steps =
2493 let fc = fileFC "elab_reflected_totality"
2582 let fc = fileFC "elab_reflected_totality"
2494 let tcgen = False -- TODO: later we may support dictionary generation
2583 let tcgen = False -- TODO: later we may support dictionary generation
2495 case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState
2584 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)
2497 OK (ElabResult lhs' _ _ _ _ _, _) ->
2587 OK (ElabResult lhs' _ _ _ _ _, _) ->
2498 do -- not recursively calling here, because we don't
2588 do -- not recursively calling here, because we don't
2499 -- want to run infinitely many times
2589 -- want to run infinitely many times