@@ -18,7 +18,7 @@ import Idris.Core.ProofTerm (getProofTerm)
18import Idris.Core.TT
18import Idris.Core.TT
19import Idris.Core.Typecheck (check, converts, isType, recheck)
19import Idris.Core.Typecheck (check, converts, isType, recheck)
20import Idris.Core.Unify
20import Idris.Core.Unify
21−import Idris.Core.WHNF (whnf)
21+import Idris.Core.WHNF (whnf,whnfArgs)
22import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)
22import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)
23import Idris.Delaborate
23import Idris.Delaborate
24import Idris.DSL
24import Idris.DSL
@@ -45,7 +45,7 @@ import qualified Data.Set as S
45import qualified Data.Text as T
45import qualified Data.Text as T
46import Debug.Trace
46import Debug.Trace
48−data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS
48+data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS
49 deriving Eq
49 deriving Eq
@@ -143,7 +143,7 @@ build ist info emode opts fn tm
143 if log /= ""
143 if log /= ""
144 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
144 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
145 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
145 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
146− where pattern = emode == ELHS
146+ where pattern = emode == ELHS || emode == EImpossible
147 tydecl = emode == ETyDecl
147 tydecl = emode == ETyDecl
149 mkPat = do hs <- get_holes
149 mkPat = do hs <- get_holes
@@ -189,7 +189,7 @@ buildTC ist info emode opts fn ns tm
189 if (log /= "")
189 if (log /= "")
190 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
190 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
191 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
191 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
192− where pattern = emode == ELHS
192+ where pattern = emode == ELHS || emode == EImpossible
194-- | return whether arguments of the given constructor name can be
194-- | return whether arguments of the given constructor name can be
195-- matched on. If they're polymorphic, no, unless the type has beed
195-- matched on. If they're polymorphic, no, unless the type has beed
@@ -201,7 +201,7 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
201 Nothing -> []
201 Nothing -> []
202 Just ty -> checkArgs [] [] ty
202 Just ty -> checkArgs [] [] ty
203 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
203 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
204− checkArgs env ns (Bind n (Pi _ t _) sc)
204+ checkArgs env ns (Bind n (Pi _ _ t _) sc)
205 = let env' = case t of
205 = let env' = case t of
206 TType _ -> n : env
206 TType _ -> n : env
207 _ -> env in
207 _ -> env in
@@ -227,7 +227,7 @@ goal_polymorphic =
227 do ty <- goal
227 do ty <- goal
228 case ty of
228 case ty of
229 P _ n _ -> do env <- get_env
229 P _ n _ -> do env <- get_env
230− case lookup n env of
230+ case lookupBinder n env of
231 Nothing -> return False
231 Nothing -> return False
232 _ -> return True
232 _ -> return True
233 _ -> return False
233 _ -> return False
@@ -245,23 +245,30 @@ elab :: IState
245elab ist info emode opts fn tm
245elab ist info emode opts fn tm
246 = do let loglvl = opt_logLevel (idris_options ist)
246 = do let loglvl = opt_logLevel (idris_options ist)
247 when (loglvl > 5) $ unifyLog True
247 when (loglvl > 5) $ unifyLog True
248− compute -- expand type synonyms, etc
248+ whnf_compute_args -- expand type synonyms, etc
249 let fc = maybe "(unknown)"
249 let fc = maybe "(unknown)"
250 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
250 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
251 est <- getAux
251 est <- getAux
252 sequence_ (get_delayed_elab est)
252 sequence_ (get_delayed_elab est)
253 end_unify
253 end_unify
254+ when (pattern || intransform) $
255+ -- convert remaining holes to pattern vars
257+ matchProblems False -- only the ones we matched earlier
260+ update_term liftPats
254 ptm <- get_term
261 ptm <- get_term
255− when (pattern || intransform) -- convert remaining holes to pattern vars
262+ when pattern $
256− (do unify_all
263+ -- Look for Rig1 (linear) pattern bindings
257− matchProblems False -- only the ones we matched earlier
264+ do let pnms = findLinear ist [] ptm
258− unifyProblems
265+ update_term (setLinear pnms)
260− update_term liftPats)
262− pattern = emode == ELHS
267+ pattern = emode == ELHS || emode == EImpossible
268+ eimpossible = emode == EImpossible
263 intransform = emode == ETransLHS
269 intransform = emode == ETransLHS
264 bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS
270 bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS
271+ || emode == EImpossible
265 autoimpls = opt_autoimpls (idris_options ist)
272 autoimpls = opt_autoimpls (idris_options ist)
267 get_delayed_elab est =
274 get_delayed_elab est =
@@ -293,7 +300,7 @@ elab ist info emode opts fn tm
294 -- | elabE elaborates an expression, possibly wrapping implicit coercions
301 -- | elabE elaborates an expression, possibly wrapping implicit coercions
295 -- and forces/delays. If you make a recursive call in elab', it is
302 -- and forces/delays. If you make a recursive call in elab', it is
296− -- normally correct to call elabE - the ones that don't are desugarings
303+ -- normally correct to call elabE - the ones that don't are `desugarings
297 -- typically
304 -- typically
298 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
305 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
299 elabE ina fc' t =
306 elabE ina fc' t =
@@ -332,13 +339,13 @@ elab ist info emode opts fn tm
332 pexp ct]))
339 pexp ct]))
334 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
341 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
335− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
342+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t),
336 ht == txt "Delayed" = notDelay orig
343 ht == txt "Delayed" = notDelay orig
337 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
344 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
338− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
345+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t'),
339 ht == txt "Delayed" = notDelay orig
346 ht == txt "Delayed" = notDelay orig
340 forceErr orig env (InfiniteUnify _ t _)
347 forceErr orig env (InfiniteUnify _ t _)
341− | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
348+ | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t),
342 ht == txt "Delayed" = notDelay orig
349 ht == txt "Delayed" = notDelay orig
343 forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t
350 forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t
344 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
351 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
@@ -349,7 +356,7 @@ elab ist info emode opts fn tm
349 notDelay _ = True
356 notDelay _ = True
351 local f = do e <- get_env
358 local f = do e <- get_env
352− return (f `elem` map fst e)
359+ return (f `elem` map fstEnv e)
354 -- | Is a constant a type?
361 -- | Is a constant a type?
355 constType :: Const -> Bool
362 constType :: Const -> Bool
@@ -370,7 +377,10 @@ elab ist info emode opts fn tm
371 highlightSource fc' (AnnType "Type" "The type of types")
378 highlightSource fc' (AnnType "Type" "The type of types")
372 elab' ina fc (PUniverse fc' u) =
379 elab' ina fc (PUniverse fc' u) =
373− do apply (RUType u) []
380+ do unless (UniquenessTypes `elem` idris_language_extensions ist
382+ lift $ tfail $ At fc' (Msg "You must turn on the UniquenessTypes extension to use UniqueType or AnyType")
375 highlightSource fc' (AnnType (show u) "The type of unique types")
385 highlightSource fc' (AnnType (show u) "The type of unique types")
376-- elab' (_,_,inty) (PConstant c)
386-- elab' (_,_,inty) (PConstant c)
@@ -387,7 +397,7 @@ elab ist info emode opts fn tm
387 highlightSource fc' (AnnConst c)
397 highlightSource fc' (AnnConst c)
388 elab' ina fc (PQuote r) = do fill r; solve
398 elab' ina fc (PQuote r) = do fill r; solve
389 elab' ina _ (PTrue fc _) =
399 elab' ina _ (PTrue fc _) =
390− do compute
400+ do whnf_compute
391 g <- goal
401 g <- goal
392 case g of
402 case g of
393 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
403 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
@@ -421,7 +431,7 @@ elab ist info emode opts fn tm
421 pexp l, pexp r]))
431 pexp l, pexp r]))
423 elab' ina _ (PPair fc hls _ l r)
433 elab' ina _ (PPair fc hls _ l r)
424− = do compute
434+ = do whnf_compute
425 g <- goal
435 g <- goal
426 let (tc, _) = unApply g
436 let (tc, _) = unApply g
427 case g of
437 case g of
@@ -444,7 +454,7 @@ elab ist info emode opts fn tm
444 IsType -> asType
454 IsType -> asType
445 IsTerm -> asValue
455 IsTerm -> asValue
446 TypeOrTerm ->
456 TypeOrTerm ->
447− do compute
457+ do whnf_compute
448 g <- goal
458 g <- goal
449 case g of
459 case g of
450 TType _ -> asType
460 TType _ -> asType
@@ -498,11 +508,13 @@ elab ist info emode opts fn tm
498 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
508 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
500 doPrune as =
510 doPrune as =
501− do compute
511+ do compute -- to get 'Delayed' if it's there
502 ty <- goal
512 ty <- goal
503− let (tc, _) = unApply (unDelay ty)
513+ ctxt <- get_context
504 env <- get_env
514 env <- get_env
505− return $ pruneByType env tc (unDelay ty) ist as
515+ let ty' = unDelay ty
516+ let (tc, _) = unApply ty'
517+ return $ pruneByType eimpossible env tc ty' ist as
507 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
519 unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
508 l == txt "Delayed" = unDelay arg
520 l == txt "Delayed" = unDelay arg
@@ -532,7 +544,7 @@ elab ist info emode opts fn tm
532 (trySeq' deferr xs) True
544 (trySeq' deferr xs) True
533 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do
545 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do
534 env <- get_env
546 env <- get_env
535− compute
547+ whnf_compute
536 ty <- goal
548 ty <- goal
537 let doelab = elab' ina fc orig
549 let doelab = elab' ina fc orig
538 tryCatch doelab
550 tryCatch doelab
@@ -564,7 +576,7 @@ elab ist info emode opts fn tm
564 recoverableErr _ = True
576 recoverableErr _ = True
566 pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env
578 pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env
567− = case unApply (normalise (tt_ctxt ist) env inc) of
579+ = case unApply (whnf (tt_ctxt ist) env inc) of
568 (P (TCon _ _) n _, _) -> filter (hasArg n env) alts
580 (P (TCon _ _) n _, _) -> filter (hasArg n env) alts
569 (Constant _, _) -> alts
581 (Constant _, _) -> alts
570 _ -> filter isLend alts -- special case hack for 'Borrowed'
582 _ -> filter isLend alts -- special case hack for 'Borrowed'
@@ -656,7 +668,7 @@ elab ist info emode opts fn tm
656 do fty <- get_type (Var n) -- check for implicits
668 do fty <- get_type (Var n) -- check for implicits
657 ctxt <- get_context
669 ctxt <- get_context
658 env <- get_env
670 env <- get_env
659− let a' = insertScopedImps fc (normalise ctxt env fty) []
671+ let a' = insertScopedImps fc (whnfArgs ctxt env fty) []
660 if null a'
672 if null a'
661 then erun fc $
673 then erun fc $
662 do apply (Var n) []
674 do apply (Var n) []
@@ -698,19 +710,30 @@ elab ist info emode opts fn tm
699 highlightSource nfc (AnnBoundName n False)
711 highlightSource nfc (AnnBoundName n False)
700 elab' ina fc (PPi p n nfc Placeholder sc)
712 elab' ina fc (PPi p n nfc Placeholder sc)
701− = do attack; arg n (is_scoped p) (sMN 0 "ty")
713+ = do attack;
716+ _ -> unless (LinearTypes `elem` idris_language_extensions ist
718+ lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a count")
719+ arg n (pcount p) (is_scoped p) (sMN 0 "phTy")
702 addAutoBind p n
720 addAutoBind p n
703 addPSname n -- okay for proof search
721 addPSname n -- okay for proof search
704 elabE (ina { e_inarg = True, e_intype = True }) fc sc
722 elabE (ina { e_inarg = True, e_intype = True }) fc sc
706 highlightSource nfc (AnnBoundName n False)
724 highlightSource nfc (AnnBoundName n False)
707 elab' ina fc (PPi p n nfc ty sc)
725 elab' ina fc (PPi p n nfc ty sc)
708− = do attack; tyn <- getNameFrom (sMN 0 "ty")
726+ = do attack; tyn <- getNameFrom (sMN 0 "piTy")
709 claim tyn RType
727 claim tyn RType
710 n' <- case n of
728 n' <- case n of
711 MN _ _ -> unique_hole n
729 MN _ _ -> unique_hole n
712 _ -> return n
730 _ -> return n
713− forall n' (is_scoped p) (Var tyn)
731+ case pcount p of
733+ _ -> unless (LinearTypes `elem` idris_language_extensions ist
735+ lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a linear argument")
736+ forall n' (pcount p) (is_scoped p) (Var tyn)
714 addAutoBind p n'
737 addAutoBind p n'
715 addPSname n' -- okay for proof search
738 addPSname n' -- okay for proof search
716 focus tyn
739 focus tyn
@@ -753,7 +776,7 @@ elab ist info emode opts fn tm
753 (ivs' \\ ivs)
776 (ivs' \\ ivs)
754 -- HACK: If the name leaks into its type, it may leak out of
777 -- HACK: If the name leaks into its type, it may leak out of
755 -- scope outside, so substitute in the outer scope.
778 -- scope outside, so substitute in the outer scope.
756− expandLet n (case lookup n env of
779+ expandLet n (case lookupBinder n env of
757 Just (Let t v) -> v
780 Just (Let t v) -> v
758 other -> error ("Value not a let binding: " ++ show other))
781 other -> error ("Value not a let binding: " ++ show other))
@@ -803,10 +826,10 @@ elab ist info emode opts fn tm
803 ans <- claimArgTys env xs
826 ans <- claimArgTys env xs
804 return ((aval, (True, (Var an))) : ans)
827 return ((aval, (True, (Var an))) : ans)
805 fnTy [] ret = forget ret
828 fnTy [] ret = forget ret
806− fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)
829+ fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi RigW Nothing xt RType) (fnTy xs ret)
808 localVar env (PRef _ _ x)
831 localVar env (PRef _ _ x)
809− = case lookup x env of
832+ = case lookupBinder x env of
810 Just _ -> Just x
833 Just _ -> Just x
811 _ -> Nothing
834 _ -> Nothing
812 localVar env _ = Nothing
835 localVar env _ = Nothing
@@ -840,7 +863,7 @@ elab ist info emode opts fn tm
840 let dataCon = isDConName f ctxt
863 let dataCon = isDConName f ctxt
841 annot <- findHighlight f
864 annot <- findHighlight f
842 mapM_ checkKnownImplicit args_in
865 mapM_ checkKnownImplicit args_in
843− let args = insertScopedImps fc (normalise ctxt env fty) args_in
866+ let args = insertScopedImps fc (whnfArgs ctxt env fty) args_in
844 let unmatchableArgs = if pattern
867 let unmatchableArgs = if pattern
845 then getUnmatchable (tt_ctxt ist) f
868 then getUnmatchable (tt_ctxt ist) f
@@ -849,7 +872,7 @@ elab ist info emode opts fn tm
849 && isTConName f (tt_ctxt ist)) $
872 && isTConName f (tt_ctxt ist)) $
850 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
873 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
851-- trace (show (f, args_in, args)) $
874-- trace (show (f, args_in, args)) $
852− if (f `elem` map fst env && length args == 1 && length args_in == 1)
875+ if (f `elem` map fstEnv env && length args == 1 && length args_in == 1)
853 then -- simple app, as below
876 then -- simple app, as below
854 do simple_app False
877 do simple_app False
855 (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))
878 (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))
@@ -897,12 +920,12 @@ elab ist info emode opts fn tm
897 imp <- if (e_isfn ina) then
920 imp <- if (e_isfn ina) then
898 do guess <- get_guess
921 do guess <- get_guess
899 env <- get_env
922 env <- get_env
900− case safeForgetEnv (map fst env) guess of
923+ case safeForgetEnv (map fstEnv env) guess of
901 Nothing ->
924 Nothing ->
902 return []
925 return []
903 Just rguess -> do
926 Just rguess -> do
904 gty <- get_type rguess
927 gty <- get_type rguess
905− let ty_n = normalise ctxt env gty
928+ let ty_n = whnf ctxt env gty
906 return $ getReqImps ty_n
929 return $ getReqImps ty_n
907 else return []
930 else return []
908 -- Now we find out how many implicits we needed at the
931 -- Now we find out how many implicits we needed at the
@@ -950,16 +973,16 @@ elab ist info emode opts fn tm
950 = lift $ tfail $ UnknownImplicit (pname imp) f
973 = lift $ tfail $ UnknownImplicit (pname imp) f
951 checkKnownImplicit _ = return ()
974 checkKnownImplicit _ = return ()
953− getReqImps (Bind x (Pi (Just i) ty _) sc)
976+ getReqImps (Bind x (Pi _ (Just i) ty _) sc)
954 = i : getReqImps sc
977 = i : getReqImps sc
955 getReqImps _ = []
978 getReqImps _ = []
957 checkIfInjective n = do
980 checkIfInjective n = do
958 env <- get_env
981 env <- get_env
959− case lookup n env of
982+ case lookupBinder n env of
960 Nothing -> return ()
983 Nothing -> return ()
961 Just b ->
984 Just b ->
962− case unApply (normalise (tt_ctxt ist) env (binderTy b)) of
985+ case unApply (whnf (tt_ctxt ist) env (binderTy b)) of
963 (P _ c _, args) ->
986 (P _ c _, args) ->
964 case lookupCtxtExact c (idris_interfaces ist) of
987 case lookupCtxtExact c (idris_interfaces ist) of
965 Nothing -> return ()
988 Nothing -> return ()
@@ -1032,6 +1055,9 @@ elab ist info emode opts fn tm
1032 elab' ina fc (PElabError e) = lift $ tfail e
1055 elab' ina fc (PElabError e) = lift $ tfail e
1033 elab' ina mfc (PRewrite fc substfn rule sc newg)
1056 elab' ina mfc (PRewrite fc substfn rule sc newg)
1034 = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg
1057 = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg
1058+ -- A common error case if trying to typecheck an autogenerated case block
1059+ elab' ina _ c@(PCase fc Placeholder opts)
1060+ = lift $ tfail (Msg "No expression for the case to inspect.\nYou need to replace the _ with an expression.")
1035 elab' ina _ c@(PCase fc scr opts)
1061 elab' ina _ c@(PCase fc scr opts)
1036 = do attack
1062 = do attack
@@ -1069,13 +1095,13 @@ elab ist info emode opts fn tm
1069 -- unnecessarily (can only do this for unique things, since we
1095 -- unnecessarily (can only do this for unique things, since we
1070 -- assume they don't appear implicitly in types)
1096 -- assume they don't appear implicitly in types)
1071 ptm <- get_term
1097 ptm <- get_term
1072− let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
1098+ let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
1074 let argsDropped = filter (isUnique envU)
1100 let argsDropped = filter (isUnique envU)
1075 (nub $ allNamesIn scr ++ inApp ptm ++
1101 (nub $ allNamesIn scr ++ inApp ptm ++
1078− let args' = filter (\(n, _) -> n `notElem` argsDropped) args
1104+ let args' = filter (\(n, _, _) -> n `notElem` argsDropped) args
1081 cname' <- defer argsDropped (mkN (mkCaseName fc fn))
1107 cname' <- defer argsDropped (mkN (mkCaseName fc fn))
@@ -1126,8 +1152,8 @@ elab ist info emode opts fn tm
1126 Just u -> u
1152 Just u -> u
1127 _ -> False
1153 _ -> False
1129− getKind env (n, _)
1155+ getKind env (n, _, _)
1130− = case lookup n env of
1156+ = case lookupBinder n env of
1131 Nothing -> return (n, False) -- can't happen, actually...
1157 Nothing -> return (n, False) -- can't happen, actually...
1132 Just b ->
1158 Just b ->
1133 do ty <- get_type (forget (binderTy b))
1159 do ty <- get_type (forget (binderTy b))
@@ -1210,13 +1236,13 @@ elab ist info emode opts fn tm
1210 loadState
1236 loadState
1211 updateAux (\aux -> aux { highlighting = hs })
1237 updateAux (\aux -> aux { highlighting = hs })
1213− let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
1239+ let quoted = fmap (explicitNames . binderVal) $ lookupBinder nTm env
1214 isRaw = case unApply (normaliseAll ctxt env finalTy) of
1240 isRaw = case unApply (normaliseAll ctxt env finalTy) of
1215 (P _ n _, []) | n == reflm "Raw" -> True
1241 (P _ n _, []) | n == reflm "Raw" -> True
1216 _ -> False
1242 _ -> False
1217 case quoted of
1243 case quoted of
1218 Just q -> do ctxt <- get_context
1244 Just q -> do ctxt <- get_context
1219− (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
1245+ (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, RigW, Lam RigW Erased) | uq <- unquoteNames] (forget q) q
1220 if pattern
1246 if pattern
1221 then if isRaw
1247 then if isRaw
1222 then reflectRawQuotePattern unquoteNames (forget q')
1248 then reflectRawQuotePattern unquoteNames (forget q')
@@ -1245,7 +1271,7 @@ elab ist info emode opts fn tm
1245 elab' ina fc (PQuoteName n True nfc) =
1271 elab' ina fc (PQuoteName n True nfc) =
1246 do ctxt <- get_context
1272 do ctxt <- get_context
1247 env <- get_env
1273 env <- get_env
1248− case lookup n env of
1274+ case lookupBinder n env of
1249 Just _ -> do fill $ reflectName n
1275 Just _ -> do fill $ reflectName n
1251 highlightSource nfc (AnnBoundName n False)
1277 highlightSource nfc (AnnBoundName n False)
@@ -1274,7 +1300,9 @@ elab ist info emode opts fn tm
1275 elab' ina fc t
1301 elab' ina fc t
1276 elab' ina fc (PRunElab fc' tm ns) =
1302 elab' ina fc (PRunElab fc' tm ns) =
1277− do attack
1303+ do unless (ElabReflection `elem` idris_language_extensions ist) $
1304+ lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")
1278 n <- getNameFrom (sMN 0 "tacticScript")
1306 n <- getNameFrom (sMN 0 "tacticScript")
1279 let scriptTy = RApp (Var (sNS (sUN "Elab")
1307 let scriptTy = RApp (Var (sNS (sUN "Elab")
1280 ["Elab", "Reflection", "Language"]))
1308 ["Elab", "Reflection", "Language"]))
@@ -1312,7 +1340,7 @@ elab ist info emode opts fn tm
1312 env <- get_env
1340 env <- get_env
1313 ctxt <- get_context
1341 ctxt <- get_context
1314 let v = fmap (normaliseAll ctxt env . finalise . binderVal)
1342 let v = fmap (normaliseAll ctxt env . finalise . binderVal)
1315− (lookup n env)
1343+ (lookupBinder n env)
1316 loadState -- we have the highlighting - re-elaborate the value
1344 loadState -- we have the highlighting - re-elaborate the value
1317 elab' ina fc tm
1345 elab' ina fc tm
1318 case v of
1346 case v of
@@ -1335,9 +1363,9 @@ elab ist info emode opts fn tm
1335 delayElab pri t
1363 delayElab pri t
1336 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })
1364 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })
1338− isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
1366+ isScr :: PTerm -> (Name, RigCount, Binder Term) -> (Name, (Bool, Binder Term))
1339− isScr (PRef _ _ n) (n', b) = (n', (n == n', b))
1367+ isScr (PRef _ _ n) (n', _, b) = (n', (n == n', b))
1340− isScr _ (n', b) = (n', (False, b))
1368+ isScr _ (n', _, b) = (n', (False, b))
1342 caseBlock :: FC -> Name
1370 caseBlock :: FC -> Name
1343 -> PTerm -- original scrutinee
1371 -> PTerm -- original scrutinee
@@ -1437,8 +1465,8 @@ elab ist info emode opts fn tm
1437 mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)
1465 mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)
1438 mkDelay env t
1466 mkDelay env t
1439 = let fc = fileFC "Delay" in
1467 = let fc = fileFC "Delay" in
1440− addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay"))
1468+ addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] (sUN "Delay"))
1441− [pexp t])
1469+ [pexp t])
1444 -- Don't put implicit coercions around applications which are marked
1472 -- Don't put implicit coercions around applications which are marked
@@ -1463,7 +1491,7 @@ elab ist info emode opts fn tm
1463 case fullApp tm of
1491 case fullApp tm of
1464 -- if f is global, leave it alone because we've already
1492 -- if f is global, leave it alone because we've already
1465 -- expanded it to the right arity
1493 -- expanded it to the right arity
1466− PApp fc ftm@(PRef _ _ f) args | Just aty <- lookup f env ->
1494+ PApp fc ftm@(PRef _ _ f) args | Just aty <- lookupBinder f env ->
1467 do let a = length (getArgTys (normalise (tt_ctxt ist) env (binderTy aty)))
1495 do let a = length (getArgTys (normalise (tt_ctxt ist) env (binderTy aty)))
1468 return (mkPApp fc a ftm args)
1496 return (mkPApp fc a ftm args)
1469 _ -> return tm
1497 _ -> return tm
@@ -1472,12 +1500,12 @@ elab ist info emode opts fn tm
1472 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1500 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1473 fullApp x = x
1501 fullApp x = x
1475− insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
1503+ insertScopedImps fc (Bind n (Pi _ im@(Just i) _ _) sc) xs
1476 | tcimplementation i && not (toplevel_imp i)
1504 | tcimplementation i && not (toplevel_imp i)
1477 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
1505 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
1478 | not (toplevel_imp i)
1506 | not (toplevel_imp i)
1479 = pimp n Placeholder True : insertScopedImps fc sc xs
1507 = pimp n Placeholder True : insertScopedImps fc sc xs
1480− insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
1508+ insertScopedImps fc (Bind n (Pi _ _ _ _) sc) (x : xs)
1481 = x : insertScopedImps fc sc xs
1509 = x : insertScopedImps fc sc xs
1482 insertScopedImps _ _ xs = xs
1510 insertScopedImps _ _ xs = xs
@@ -1488,7 +1516,7 @@ elab ist info emode opts fn tm
1488 addLam ty' t
1516 addLam ty' t
1490 -- just one level at a time
1518 -- just one level at a time
1491− addLam (Bind n (Pi (Just _) _ _) sc) t =
1519+ addLam (Bind n (Pi _ (Just _) _ _) sc) t =
1492 do impn <- unique_hole n -- (sMN 0 "scoped_imp")
1520 do impn <- unique_hole n -- (sMN 0 "scoped_imp")
1493 if e_isfn ina -- apply to an implicit immediately
1521 if e_isfn ina -- apply to an implicit immediately
1494 then return (PApp emptyFC
1522 then return (PApp emptyFC
@@ -1516,7 +1544,7 @@ elab ist info emode opts fn tm
1516 mkCoerce env (PAlternative ms aty tms) n
1544 mkCoerce env (PAlternative ms aty tms) n
1517 = PAlternative ms aty (map (\t -> mkCoerce env t n) tms)
1545 = PAlternative ms aty (map (\t -> mkCoerce env t n) tms)
1518 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in
1546 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in
1519− addImplBound ist (map fst env)
1547+ addImplBound ist (map fstEnv env)
1520 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])
1548 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])
1522 -- | Elaborate the arguments to a function
1550 -- | Elaborate the arguments to a function
@@ -1575,7 +1603,7 @@ elab ist info emode opts fn tm
1575 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
1603 fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
1577 addAutoBind :: Plicity -> Name -> ElabD ()
1605 addAutoBind :: Plicity -> Name -> ElabD ()
1578− addAutoBind (Imp _ _ _ _ False) n
1606+ addAutoBind (Imp _ _ _ _ False _) n
1579 = updateAux (\est -> est { auto_binds = n : auto_binds est })
1607 = updateAux (\est -> est { auto_binds = n : auto_binds est })
1580 addAutoBind _ _ = return ()
1608 addAutoBind _ _ = return ()
@@ -1625,17 +1653,17 @@ pruneAlt xs = map prune xs
1626-- Rule out alternatives that don't return the same type as the head of the goal
1654-- Rule out alternatives that don't return the same type as the head of the goal
1627-- (If there are none left as a result, do nothing)
1655-- (If there are none left as a result, do nothing)
1628−pruneByType :: Env -> Term -> -- head of the goal
1656+pruneByType :: Bool -> Env -> Term -> -- head of the goal
1629 Type -> -- goal
1657 Type -> -- goal
1630 IState -> [PTerm] -> [PTerm]
1658 IState -> [PTerm] -> [PTerm]
1631-- if an alternative has a locally bound name at the head, take it
1659-- if an alternative has a locally bound name at the head, take it
1632−pruneByType env t goalty c as
1660+pruneByType imp env t goalty c as
1633 | Just a <- locallyBound as = [a]
1661 | Just a <- locallyBound as = [a]
1635 locallyBound [] = Nothing
1663 locallyBound [] = Nothing
1636 locallyBound (t:ts)
1664 locallyBound (t:ts)
1637 | Just n <- getName t,
1665 | Just n <- getName t,
1638− n `elem` map fst env = Just t
1666+ n `elem` map fstEnv env = Just t
1639 | otherwise = locallyBound ts
1667 | otherwise = locallyBound ts
1640 getName (PRef _ _ n) = Just n
1668 getName (PRef _ _ n) = Just n
1641 getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays
1669 getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays
@@ -1645,7 +1673,7 @@ pruneByType env t goalty c as
1645 getName _ = Nothing
1673 getName _ = Nothing
1647-- 'n' is the name at the head of the goal type
1675-- 'n' is the name at the head of the goal type
1648−pruneByType env (P _ n _) goalty ist as
1676+pruneByType imp env (P _ n _) goalty ist as
1649-- if the goal type is polymorphic, keep everything
1677-- if the goal type is polymorphic, keep everything
1650 | Nothing <- lookupTyExact n ctxt = as
1678 | Nothing <- lookupTyExact n ctxt = as
1651-- if the goal type is a ?metavariable, keep everything
1679-- if the goal type is a ?metavariable, keep everything
@@ -1677,12 +1705,13 @@ pruneByType env (P _ n _) goalty ist as
1677 Just ty -> case unApply (getRetTy ty) of
1705 Just ty -> case unApply (getRetTy ty) of
1678 (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
1706 (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
1679 -> False
1707 -> False
1680− _ -> let ty' = normalise ctxt [] ty in
1708+ _ -> let ty' = whnf ctxt [] ty in
1681−-- trace ("Trying " ++ show (getRetTy ty') ++ " for " ++ show goalty) $
1709+-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty
1710+-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $
1682 case unApply (getRetTy ty') of
1711 case unApply (getRetTy ty') of
1683 (V _, _) ->
1712 (V _, _) ->
1684 isPlausible ist var env n ty
1713 isPlausible ist var env n ty
1685− _ -> matching (getRetTy ty') goalty
1714+ _ -> matchingTypes imp (getRetTy ty') goalty
1686 || isCoercion (getRetTy ty') goalty
1715 || isCoercion (getRetTy ty') goalty
1687-- May be useful to keep for debugging purposes for a bit:
1716-- May be useful to keep for debugging purposes for a bit:
1688-- let res = matching (getRetTy ty') goalty in
1717-- let res = matching (getRetTy ty') goalty in
@@ -1690,9 +1719,12 @@ pruneByType env (P _ n _) goalty ist as
1690-- ("Rejecting " ++ show (getRetTy ty', goalty)) res
1719-- ("Rejecting " ++ show (getRetTy ty', goalty)) res
1691 _ -> False
1720 _ -> False
1722+ matchingTypes True = matchingHead
1723+ matchingTypes False = matching
1693 -- If the goal is a constructor, it must match the suggested function type
1725 -- If the goal is a constructor, it must match the suggested function type
1694 matching (P _ ctyn _) (P _ n' _)
1726 matching (P _ ctyn _) (P _ n' _)
1695− | isTConName n' ctxt = ctyn == n'
1727+ | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'
1696 | otherwise = True
1728 | otherwise = True
1697 -- Variables match anything
1729 -- Variables match anything
1698 matching (V _) _ = True
1730 matching (V _) _ = True
@@ -1703,14 +1735,28 @@ pruneByType env (P _ n _) goalty ist as
1703 matching (Bind n _ sc) _ = True
1735 matching (Bind n _ sc) _ = True
1704 matching _ (Bind n _ sc) = True
1736 matching _ (Bind n _ sc) = True
1705 -- If we hit a function name, it's a plausible match
1737 -- If we hit a function name, it's a plausible match
1706− matching (App _ (P _ f _) _) _ | not (isConName f ctxt) = True
1738+ matching apl@(App _ _ _) apr@(App _ _ _)
1707− matching _ (App _ (P _ f _) _) | not (isConName f ctxt) = True
1739+ | (P _ fl _, argsl) <- unApply apl,
1708− -- Otherwise, match the rest of the structure
1740+ (P _ fr _, argsr) <- unApply apr
1709− matching (App _ f a) (App _ f' a') = matching f f' && matching a a'
1741+ = fl == fr && and (zipWith matching argsl argsr)
1742+ || (not (isConName fl ctxt && isConName fr ctxt))
1743+ -- If the application structures aren't easily comparable, it's a
1745+ matching (App _ f a) (App _ f' a') = True
1710 matching (TType _) (TType _) = True
1746 matching (TType _) (TType _) = True
1711 matching (UType _) (UType _) = True
1747 matching (UType _) (UType _) = True
1712 matching l r = l == r
1748 matching l r = l == r
1750+ -- In impossible-case mode, only look at the heads (this is to account for
1751+ -- the non type-directed case with 'impossible' - we'd be ruling out
1752+ -- too much and wouldn't find the mismatch we're looking for)
1753+ matchingHead apl@(App _ _ _) apr@(App _ _ _)
1754+ | (P _ fl _, argsl) <- unApply apl,
1755+ (P _ fr _, argsr) <- unApply apr,
1756+ isConName fl ctxt && isConName fr ctxt
1758+ matchingHead _ _ = True
1714 -- Return whether there is a possible coercion between the return type
1760 -- Return whether there is a possible coercion between the return type
1715 -- of an alternative and the goal type
1761 -- of an alternative and the goal type
1716 isCoercion rty gty | (P _ r _, _) <- unApply rty
1762 isCoercion rty gty | (P _ r _, _) <- unApply rty
@@ -1735,7 +1781,7 @@ pruneByType env (P _ n _) goalty ist as
1735 _ -> False
1781 _ -> False
1738−pruneByType _ t _ _ as = as
1784+pruneByType _ _ t _ _ as = as
1740-- Could the name feasibly be the return type?
1786-- Could the name feasibly be the return type?
1741-- If there is an interface constraint on the return type, and no implementation
1787-- If there is an interface constraint on the return type, and no implementation
@@ -1752,7 +1798,7 @@ isPlausible ist var env n ty
1753 collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
1799 collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
1754 (Maybe Name, [(Term, [Name])])
1800 (Maybe Name, [(Term, [Name])])
1755− collectConstraints env tcs (Bind n (Pi _ ty _) sc)
1801+ collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)
1756 = let tcs' = case unApply ty of
1802 = let tcs' = case unApply ty of
1757 (P _ c _, _) ->
1803 (P _ c _, _) ->
1758 case lookupCtxtExact c (idris_interfaces ist) of
1804 case lookupCtxtExact c (idris_interfaces ist) of
@@ -1770,7 +1816,7 @@ isPlausible ist var env n ty
1770findHighlight :: Name -> ElabD OutputAnnotation
1816findHighlight :: Name -> ElabD OutputAnnotation
1771findHighlight n = do ctxt <- get_context
1817findHighlight n = do ctxt <- get_context
1772 env <- get_env
1818 env <- get_env
1773− case lookup n env of
1819+ case lookupBinder n env of
1774 Just _ -> return $ AnnBoundName n False
1820 Just _ -> return $ AnnBoundName n False
1775 Nothing -> case lookupTyExact n ctxt of
1821 Nothing -> case lookupTyExact n ctxt of
1776 Just _ -> return $ AnnName n Nothing Nothing Nothing
1822 Just _ -> return $ AnnName n Nothing Nothing Nothing
@@ -1790,7 +1836,7 @@ solveAuto ist fn ambigok (n, failc)
1790 when (not isg) $
1836 when (not isg) $
1791 proofSearch' ist True ambigok 100 True Nothing fn [] [])
1837 proofSearch' ist True ambigok 100 True Nothing fn [] [])
1792 (lift $ Error (addLoc failc
1838 (lift $ Error (addLoc failc
1793− (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))
1839+ (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env))))
1794 return ()
1840 return ()
1795 where addLoc (FailContext fc f x : prev) err
1841 where addLoc (FailContext fc f x : prev) err
1796 = At fc (ElaboratingArg f x
1842 = At fc (ElaboratingArg f x
@@ -1863,7 +1909,7 @@ case_ ind autoSolve ist fn tm = do
1863 focus valn
1909 focus valn
1864 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1910 elab ist toplevel ERHS [] (sMN 0 "tac") tm
1865 env <- get_env
1911 env <- get_env
1866− let (Just binding) = lookup letn env
1912+ let (Just binding) = lookupBinder letn env
1867 let val = binderVal binding
1913 let val = binderVal binding
1868 if ind then induction (forget val)
1914 if ind then induction (forget val)
1869 else casetac (forget val)
1915 else casetac (forget val)
@@ -1886,7 +1932,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
1886 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
1932 returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
1888 patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)
1934 patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)
1889− patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
1935+ patvars ns (Bind n (PVar _ t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
1890 patvars ns tm = (ns, tm)
1936 patvars ns tm = (ns, tm)
1892 pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
1938 pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
@@ -1955,7 +2001,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
1956 -- | Add another argument to a Pi
2002 -- | Add another argument to a Pi
1957 mkPi :: RFunArg -> Raw -> Raw
2003 mkPi :: RFunArg -> Raw -> Raw
1958− mkPi arg rTy = RBind (argName arg) (Pi Nothing (argTy arg) (RUType AllTypes)) rTy
2004+ mkPi arg rTy = RBind (argName arg) (Pi RigW Nothing (argTy arg) (RUType AllTypes)) rTy
1960 mustBeType ctxt tm ty =
2006 mustBeType ctxt tm ty =
1961 case normaliseAll ctxt [] (finalise ty) of
2007 case normaliseAll ctxt [] (finalise ty) of
@@ -2012,7 +2058,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2014 getRetTy :: Type -> Type
2060 getRetTy :: Type -> Type
2015− getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
2061+ getRetTy (Bind _ (Pi _ _ _ _) sc) = getRetTy sc
2016 getRetTy ty = ty
2062 getRetTy ty = ty
2018 elabScriptStuck :: Term -> ElabD a
2064 elabScriptStuck :: Term -> ElabD a
@@ -2220,7 +2266,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2220 = do ~[n, ty] <- tacTmArgs 2 tac args
2266 = do ~[n, ty] <- tacTmArgs 2 tac args
2221 n' <- reifyTTName n
2267 n' <- reifyTTName n
2222 ty' <- reifyRaw ty
2268 ty' <- reifyRaw ty
2223− forall n' Nothing ty'
2269+ forall n' RigW Nothing ty'
2224 returnUnit
2270 returnUnit
2225 | n == tacN "Prim__PatVar"
2271 | n == tacN "Prim__PatVar"
2226 = do ~[n] <- tacTmArgs 1 tac args
2272 = do ~[n] <- tacTmArgs 1 tac args
@@ -2230,7 +2276,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2230 | n == tacN "Prim__PatBind"
2276 | n == tacN "Prim__PatBind"
2231 = do ~[n] <- tacTmArgs 1 tac args
2277 = do ~[n] <- tacTmArgs 1 tac args
2232 n' <- reifyTTName n
2278 n' <- reifyTTName n
2233− patbind n'
2279+ patbind n' RigW
2234 returnUnit
2280 returnUnit
2235 | n == tacN "Prim__LetBind"
2281 | n == tacN "Prim__LetBind"
2236 = do ~[n, ty, tm] <- tacTmArgs 3 tac args
2282 = do ~[n, ty, tm] <- tacTmArgs 3 tac args
@@ -2252,7 +2298,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2252 = do ~[tm] <- tacTmArgs 1 tac args
2298 = do ~[tm] <- tacTmArgs 1 tac args
2253 tm' <- reifyTT tm
2299 tm' <- reifyTT tm
2254 ctxt <- get_context
2300 ctxt <- get_context
2255− fmap fst . checkClosed . reflect $ whnf ctxt tm'
2301+ fmap fst . checkClosed . reflect $ whnf ctxt [] tm'
2256 | n == tacN "Prim__Converts"
2302 | n == tacN "Prim__Converts"
2257 = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
2303 = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
2258 env' <- reifyEnv env
2304 env' <- reifyEnv env
@@ -2426,11 +2472,11 @@ runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
2426runTac autoSolve ist perhapsFC fn tac
2472runTac autoSolve ist perhapsFC fn tac
2427 = do env <- get_env
2473 = do env <- get_env
2428 g <- goal
2474 g <- goal
2429− let tac' = fmap (addImplBound ist (map fst env)) tac
2475+ let tac' = fmap (addImplBound ist (map fstEnv env)) tac
2430 if autoSolve
2476 if autoSolve
2431 then runT tac'
2477 then runT tac'
2432 else no_errors (runT tac')
2478 else no_errors (runT tac')
2433− (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
2479+ (Just (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env)))
2435 runT (Intro []) = do g <- goal
2481 runT (Intro []) = do g <- goal
2436 attack; intro (bname g)
2482 attack; intro (bname g)
@@ -2460,7 +2506,7 @@ runTac autoSolve ist perhapsFC fn tac
2460 tryAll tacs
2506 tryAll tacs
2461 when autoSolve solveAll
2507 when autoSolve solveAll
2462 where envArgs n = do e <- get_env
2508 where envArgs n = do e <- get_env
2463− case lookup n e of
2509+ case lookupBinder n e of
2464 Just t -> return $ map (const False)
2510 Just t -> return $ map (const False)
2465 (getArgTys (binderTy t))
2511 (getArgTys (binderTy t))
2466 _ -> return []
2512 _ -> return []
@@ -2478,7 +2524,7 @@ runTac autoSolve ist perhapsFC fn tac
2478 where isImp (PImp _ _ _ _ _) = True
2524 where isImp (PImp _ _ _ _ _) = True
2479 isImp _ = False
2525 isImp _ = False
2480 envArgs n = do e <- get_env
2526 envArgs n = do e <- get_env
2481− case lookup n e of
2527+ case lookupBinder n e of
2482 Just t -> return $ map (const False)
2528 Just t -> return $ map (const False)
2483 (getArgTys (binderTy t))
2529 (getArgTys (binderTy t))
2484 _ -> return []
2530 _ -> return []
@@ -2587,9 +2633,9 @@ runTac autoSolve ist perhapsFC fn tac
2587 where tacticTy = Var (reflm "Tactic")
2633 where tacticTy = Var (reflm "Tactic")
2588 listTy = Var (sNS (sUN "List") ["List", "Prelude"])
2634 listTy = Var (sNS (sUN "List") ["List", "Prelude"])
2589 scriptTy = (RBind (sMN 0 "__pi_arg")
2635 scriptTy = (RBind (sMN 0 "__pi_arg")
2590− (Pi Nothing (RApp listTy envTupleType) RType)
2636+ (Pi RigW Nothing (RApp listTy envTupleType) RType)
2591 (RBind (sMN 1 "__pi_arg")
2637 (RBind (sMN 1 "__pi_arg")
2592− (Pi Nothing (Var $ reflm "TT") RType) tacticTy))
2638+ (Pi RigW Nothing (Var $ reflm "TT") RType) tacticTy))
2593 runT (ByReflection tm) -- run the reflection function 'tm' on the
2639 runT (ByReflection tm) -- run the reflection function 'tm' on the
2594 -- goal, then apply the resulting reflected Tactic
2640 -- goal, then apply the resulting reflected Tactic
2595 = do tgoal <- goal
2641 = do tgoal <- goal
@@ -2785,7 +2831,7 @@ processTacticDecls info steps =
2785 mapM_ (addIBC . IBCDef . cn) ctors
2831 mapM_ (addIBC . IBCDef . cn) ctors
2786 ctxt <- getContext
2832 ctxt <- getContext
2787 let params = findParams tyn (normalise ctxt [] tyconTy) (map cty ctors)
2833 let params = findParams tyn (normalise ctxt [] tyconTy) (map cty ctors)
2788− let typeInfo = TI (map cn ctors) False [] params []
2834+ let typeInfo = TI (map cn ctors) False [] params [] False
2789 -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.
2835 -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.
2790 -- otherwise writing the IBC just fails silently!
2836 -- otherwise writing the IBC just fails silently!
2791 updateIState $ \i -> i { idris_datatypes =
2837 updateIState $ \i -> i { idris_datatypes =
@@ -2826,15 +2872,16 @@ processTacticDecls info steps =
2826 RClausesInstrs n cs ->
2872 RClausesInstrs n cs ->
2827 do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n
2873 do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n
2828 solveDeferred emptyFC n
2874 solveDeferred emptyFC n
2829− let lhss = map (\(_, lhs, _) -> lhs) cs
2875+ let lhss = map (\(ns, lhs, _) -> (map fst ns, lhs)) cs
2830 let fc = fileFC "elab_reflected"
2876 let fc = fileFC "elab_reflected"
2831 pmissing <-
2877 pmissing <-
2832 do ist <- getIState
2878 do ist <- getIState
2833 possible <- genClauses fc n lhss
2879 possible <- genClauses fc n lhss
2834− (map (\lhs ->
2880+ (map (\ (ns, lhs) ->
2835 delab' ist lhs True True) lhss)
2881 delab' ist lhs True True) lhss)
2836 missing <- filterM (checkPossible n) possible
2882 missing <- filterM (checkPossible n) possible
2837− return (filter (noMatch ist lhss) missing)
2883+ let undef = filter (noMatch ist (map snd lhss)) missing
2838 let tot = if null pmissing
2885 let tot = if null pmissing
2839 then Unchecked -- still need to check recursive calls
2886 then Unchecked -- still need to check recursive calls
2840 else Partial NotCovering -- missing cases implies not total
2887 else Partial NotCovering -- missing cases implies not total
@@ -2871,16 +2918,16 @@ processTacticDecls info steps =
2872 -- TODO: see if the code duplication with Idris.Elab.Clause can be
2919 -- TODO: see if the code duplication with Idris.Elab.Clause can be
2873 -- reduced or eliminated.
2920 -- reduced or eliminated.
2921+ -- These are always cases generated by genClauses
2874 checkPossible :: Name -> PTerm -> Idris Bool
2922 checkPossible :: Name -> PTerm -> Idris Bool
2875 checkPossible fname lhs_in =
2923 checkPossible fname lhs_in =
2876 do ctxt <- getContext
2924 do ctxt <- getContext
2877 ist <- getIState
2925 ist <- getIState
2878 let lhs = addImplPat ist lhs_in
2926 let lhs = addImplPat ist lhs_in
2879 let fc = fileFC "elab_reflected_totality"
2927 let fc = fileFC "elab_reflected_totality"
2880− let tcgen = False -- TODO: later we may support dictionary generation
2881 case elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState
2928 case elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState
2882− (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)
2929+ (erun fc (buildTC ist info EImpossible [] fname (allNamesIn lhs_in)
2883− (infTerm lhs))) of
2930+ (infTerm lhs))) of
2884 OK (ElabResult lhs' _ _ _ _ _ name', _) ->
2931 OK (ElabResult lhs' _ _ _ _ _ name', _) ->
2885 do -- not recursively calling here, because we don't
2932 do -- not recursively calling here, because we don't
2886 -- want to run infinitely many times
2933 -- want to run infinitely many times
@@ -2890,9 +2937,7 @@ processTacticDecls info steps =
2890 OK _ -> return True
2937 OK _ -> return True
2891 err -> return False
2938 err -> return False
2892 -- if it's a recoverable error, the case may become possible
2939 -- if it's a recoverable error, the case may become possible
2893− Error err -> if tcgen then return (recoverableCoverage ctxt err)
2940+ Error err -> return (recoverableCoverage ctxt err)
2894− else return (validCoverageCase ctxt err ||
2895− recoverableCoverage ctxt err)
2898 -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause
2943 -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause