git.iko.soy/Idris-dev
on master help sign in
Deal with ambiguity in impossible clauses

Some things were getting past totality checking because we weren't generating clauses when there was ambiguity on a non-checkable lhs. Now take a type-directed approach to building the term for the case tree which, even though it can't be checked, at least has the right unambiguous names. If we can't resolve the ambiguity, it's an error. In some (probably rare) cases this might need the programmer to disambiguate explicitly. I think this is a price worth paying for soundness... Fixes #3269

commit183f5332eb25bdff2fea1e2038f62505f1309f5f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 17 Mar 2017, 15:36 (10 years ago) parentc5be396
6 files changed+237−185
compare with master
unifiedsplit
src/Idris/Coverage.hs+56−22 src/Idris/Elab/Term.hs+2−163 src/Idris/Elab/Utils.hs+162 test/totality021/expected+4 test/totality021/run+1 test/totality021/totality021a.idr+12
src/Idris/Coverage.hs+56−22
@@ -14,6 +14,7 @@ import Idris.Core.CaseTree
1414import Idris.Core.Evaluate
1515import Idris.Core.TT
1616import Idris.Delaborate
17+import Idris.Elab.Utils
1718import Idris.Error
1819import Idris.Output (iWarn, iputStrLn)
1920
@@ -28,33 +29,64 @@ import Debug.Trace
2829--
2930-- We need this to eliminate the pattern clauses which have been
3031-- provided explicitly from new clause generation.
32+--
33+-- This takes a type directed approach to disambiguating names. If we
34+-- can't immediately disambiguate by looking at the expected type, it's an
35+-- error (we can't do this the usual way of trying it to see what type checks
36+-- since the whole point of an impossible case is that it won't type check!)
3137mkPatTm :: PTerm -> Idris Term
3238mkPatTm t = do i <- getIState
3339 let timp = addImpl' True [] [] [] i t
34− evalStateT (toTT (mapPT deNS timp)) 0
40+ evalStateT (toTT Nothing timp) 0
3541 where
36− toTT (PRef _ _ n) = do i <- lift getIState
37− case lookupNameDef n (tt_ctxt i) of
38− [(n', TyDecl nt _)] -> return $ P nt n' Erased
39− _ -> return $ P Ref n Erased
40− toTT (PApp _ t args) = do t' <- toTT t
41− args' <- mapM (toTT . getTm) args
42− return $ mkApp t' args'
43− toTT (PDPair _ _ _ l _ r) = do l' <- toTT l
44− r' <- toTT r
45− return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
46− toTT (PPair _ _ _ l r) = do l' <- toTT l
47− r' <- toTT r
48− return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
42+ toTT :: Maybe Type -> PTerm -> StateT Int Idris Term
43+ toTT ty (PRef _ _ n)
44+ = do i <- lift getIState
45+ case lookupDefExact n (tt_ctxt i) of
46+ Just (TyDecl nt _) -> return $ P nt n Erased
47+ _ -> return $ P Ref n Erased
48+ toTT ty (PApp _ t@(PRef _ _ n) args)
49+ = do i <- lift getIState
50+ let aTys = case lookupTyExact n (tt_ctxt i) of
51+ Just nty -> map (Just . snd) (getArgTys nty)
52+ Nothing -> map (const Nothing) args
53+ args' <- zipWithM toTT aTys (map getTm args)
54+ t' <- toTT Nothing t
55+ return $ mkApp t' args'
56+ toTT ty (PApp _ t args)
57+ = do t' <- toTT Nothing t
58+ args' <- mapM (toTT Nothing . getTm) args
59+ return $ mkApp t' args'
60+ toTT ty (PDPair _ _ _ l _ r)
61+ = do l' <- toTT Nothing l
62+ r' <- toTT Nothing r
63+ return $ mkApp (P Ref sigmaCon Erased) [Erased, Erased, l', r']
64+ toTT ty (PPair _ _ _ l r)
65+ = do l' <- toTT Nothing l
66+ r' <- toTT Nothing r
67+ return $ mkApp (P Ref pairCon Erased) [Erased, Erased, l', r']
4968 -- For alternatives, pick the first and drop the namespaces. It doesn't
5069 -- really matter which is taken since matching will ignore the namespace.
51− toTT (PAlternative _ _ (a : as)) = toTT a
52− toTT _ = do v <- get
53− put (v + 1)
54− return (P Bound (sMN v "imp") Erased)
55−
56− deNS (PRef f hl (NS n _)) = PRef f hl n
57− deNS t = t
70+ toTT (Just ty) (PAlternative _ _ as)
71+ | (hd, _) <- unApply ty
72+ = do i <- lift getIState
73+ case pruneByType True [] hd ty i as of
74+ [a] -> toTT (Just ty) a
75+ _ -> lift $ ierror $ CantResolveAlts (map getAltName as)
76+ toTT Nothing (PAlternative _ _ as)
77+ = lift $ ierror $ CantResolveAlts (map getAltName as)
78+ toTT ty _
79+ = do v <- get
80+ put (v + 1)
81+ return (P Bound (sMN v "imp") Erased)
82+
83+ getAltName (PApp _ (PRef _ _ (UN l)) [_, _, arg])
84+ | l == txt "Delay" = getAltName (getTm arg)
85+ getAltName (PApp _ (PRef _ _ n) _) = n
86+ getAltName (PRef _ _ n) = n
87+ getAltName (PApp _ h _) = getAltName h
88+ getAltName (PHidden h) = getAltName h
89+ getAltName x = sUN "_" -- should never happen here
5890
5991-- | Given a list of LHSs, generate a extra clauses which cover the remaining
6092-- cases. The ones which haven't been provided are marked 'absurd' so
@@ -74,7 +106,9 @@ genClauses fc n lhs_tms given
74106 let lhs_given = zipWith removePlaceholders lhs_tms
75107 (map (stripUnmatchable i) (map flattenArgs given))
76108
77− logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map show (lhs_given))
109+ logCoverage 5 $ "Building coverage tree for:\n" ++ showSep "\n" (map showTmImpls given)
110+ logCoverage 10 $ "Building coverage tree for:\n" ++ showSep "\n" (map show lhs_given)
111+ logCoverage 10 $ "From terms:\n" ++ showSep "\n" (map show lhs_tms)
78112 let givenpos = mergePos (map getGivenPos given)
79113
80114 (cns, ctree_in) <-
src/Idris/Elab/Term.hs+2−163
@@ -1522,7 +1522,7 @@ elab ist info emode opts fn tm
15221522 (arg, x : rest)
15231523
15241524 insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]
1525− insertScopedImps fc f knowns ty xs =
1525+ insertScopedImps fc f knowns ty xs =
15261526 do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs
15271527 doInsert ty xs
15281528 where
@@ -1538,7 +1538,7 @@ elab ist info emode opts fn tm
15381538 = liftM (x :) (doInsert sc xs)
15391539 doInsert ty xs = return xs
15401540
1541− -- Any implicit in the application needs to have the name of a
1541+ -- Any implicit in the application needs to have the name of a
15421542 -- scoped implicit or a top level implicit, otherwise report an error
15431543 checkKnownImplicit ns imp@(PImp{})
15441544 | pname imp `elem` ns = return ()
@@ -1698,167 +1698,6 @@ pruneAlt xs = map prune xs
16981698 headIs f (PApp _ f' _) = headIs f f'
16991699 headIs f _ = True -- keep if it's not an application
17001700
1701−-- Rule out alternatives that don't return the same type as the head of the goal
1702−-- (If there are none left as a result, do nothing)
1703−pruneByType :: Bool -> Env -> Term -> -- head of the goal
1704− Type -> -- goal
1705− IState -> [PTerm] -> [PTerm]
1706−-- if an alternative has a locally bound name at the head, take it
1707−pruneByType imp env t goalty c as
1708− | Just a <- locallyBound as = [a]
1709− where
1710− locallyBound [] = Nothing
1711− locallyBound (t:ts)
1712− | Just n <- getName t,
1713− n `elem` map fstEnv env = Just t
1714− | otherwise = locallyBound ts
1715− getName (PRef _ _ n) = Just n
1716− getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays
1717− | l == txt "Delay" = getName (getTm arg)
1718− getName (PApp _ f _) = getName f
1719− getName (PHidden t) = getName t
1720− getName _ = Nothing
1721−
1722−-- 'n' is the name at the head of the goal type
1723−pruneByType imp env (P _ n _) goalty ist as
1724−-- if the goal type is polymorphic, keep everything
1725− | Nothing <- lookupTyExact n ctxt = as
1726−-- if the goal type is a ?metavariable, keep everything
1727− | Just _ <- lookup n (idris_metavars ist) = as
1728− | otherwise
1729− = let asV = filter (headIs True n) as
1730− as' = filter (headIs False n) as in
1731− case as' of
1732− [] -> asV
1733− _ -> as'
1734− where
1735− ctxt = tt_ctxt ist
1736−
1737− -- Get the function at the head of the alternative and see if it's
1738− -- a plausible match against the goal type. Keep if so. Also keep if
1739− -- there is a possible coercion to the goal type.
1740− headIs var f (PRef _ _ f') = typeHead var f f'
1741− headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
1742− | l == txt "Delay" = headIs var f (getTm arg)
1743− headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'
1744− headIs var f (PApp _ f' _) = headIs var f f'
1745− headIs var f (PPi _ _ _ _ sc) = headIs var f sc
1746− headIs var f (PHidden t) = headIs var f t
1747− headIs var f t = True -- keep if it's not an application
1748−
1749− typeHead var f f'
1750− = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
1751− case lookupTyExact f' ctxt of
1752− Just ty -> case unApply (getRetTy ty) of
1753− (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
1754− -> False
1755− _ -> let ty' = normalise ctxt [] ty in
1756−-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty
1757−-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $
1758− case unApply (getRetTy ty') of
1759− (V _, _) ->
1760− isPlausible ist var env n ty
1761− _ -> matchingTypes imp (getRetTy ty') goalty
1762− || isCoercion (getRetTy ty') goalty
1763−-- May be useful to keep for debugging purposes for a bit:
1764−-- let res = matching (getRetTy ty') goalty in
1765−-- traceWhen (not res)
1766−-- ("Rejecting " ++ show (getRetTy ty', goalty)) res
1767− _ -> False
1768−
1769− matchingTypes True = matchingHead
1770− matchingTypes False = matching
1771−
1772− -- If the goal is a constructor, it must match the suggested function type
1773− matching (P _ ctyn _) (P _ n' _)
1774− | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'
1775− | otherwise = True
1776− -- Variables match anything
1777− matching (V _) _ = True
1778− matching _ (V _) = True
1779− matching _ (P _ n _) = not (isTConName n ctxt)
1780− matching (P _ n _) _ = not (isTConName n ctxt)
1781− -- Binders are a plausible match, so keep them
1782− matching (Bind n _ sc) _ = True
1783− matching _ (Bind n _ sc) = True
1784− -- If we hit a function name, it's a plausible match
1785− matching apl@(App _ _ _) apr@(App _ _ _)
1786− | (P _ fl _, argsl) <- unApply apl,
1787− (P _ fr _, argsr) <- unApply apr
1788− = fl == fr && and (zipWith matching argsl argsr)
1789− || (not (isConName fl ctxt && isConName fr ctxt))
1790− -- If the application structures aren't easily comparable, it's a
1791− -- plausible match
1792− matching (App _ f a) (App _ f' a') = True
1793− matching (TType _) (TType _) = True
1794− matching (UType _) (UType _) = True
1795− matching l r = l == r
1796−
1797− -- In impossible-case mode, only look at the heads (this is to account for
1798− -- the non type-directed case with 'impossible' - we'd be ruling out
1799− -- too much and wouldn't find the mismatch we're looking for)
1800− matchingHead apl@(App _ _ _) apr@(App _ _ _)
1801− | (P _ fl _, argsl) <- unApply apl,
1802− (P _ fr _, argsr) <- unApply apr,
1803− isConName fl ctxt && isConName fr ctxt
1804− = fl == fr
1805− matchingHead _ _ = True
1806−
1807− -- Return whether there is a possible coercion between the return type
1808− -- of an alternative and the goal type
1809− isCoercion rty gty | (P _ r _, _) <- unApply rty
1810− = not (null (getCoercionsBetween r gty))
1811− isCoercion _ _ = False
1812−
1813− getCoercionsBetween :: Name -> Type -> [Name]
1814− getCoercionsBetween r goal
1815− = let cs = getCoercionsTo ist goal in
1816− findCoercions r cs
1817− where findCoercions t [] = []
1818− findCoercions t (n : ns) =
1819− let ps = case lookupTy n (tt_ctxt ist) of
1820− [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in
1821− [n | any useR as]
1822− _ -> [] in
1823− ps ++ findCoercions t ns
1824−
1825− useR ty =
1826− case unApply (getRetTy ty) of
1827− (P _ t _, _) -> t == r
1828− _ -> False
1829−
1830−
1831−pruneByType _ _ t _ _ as = as
1832−
1833−-- Could the name feasibly be the return type?
1834−-- If there is an interface constraint on the return type, and no implementation
1835−-- in the environment or globally for that name, then no
1836−-- Otherwise, yes
1837−-- (FIXME: This isn't complete, but I'm leaving it here and coming back
1838−-- to it later - just returns 'var' for now. EB)
1839−isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
1840−isPlausible ist var env n ty
1841− = let (hvar, interfaces) = collectConstraints [] [] ty in
1842− case hvar of
1843− Nothing -> True
1844− Just rth -> var -- trace (show (rth, interfaces)) var
1845− where
1846− collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
1847− (Maybe Name, [(Term, [Name])])
1848− collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)
1849− = let tcs' = case unApply ty of
1850− (P _ c _, _) ->
1851− case lookupCtxtExact c (idris_interfaces ist) of
1852− Just tc -> ((ty, map fst (interface_implementations tc))
1853− : tcs)
1854− Nothing -> tcs
1855− _ -> tcs
1856− in
1857− collectConstraints (n : env) tcs' sc
1858− collectConstraints env tcs t
1859− | (V i, _) <- unApply t = (Just (env !! i), tcs)
1860− | otherwise = (Nothing, tcs)
1861−
18621701-- | Use the local elab context to work out the highlighting for a name
18631702findHighlight :: Name -> ElabD OutputAnnotation
18641703findHighlight n = do ctxt <- get_context
src/Idris/Elab/Utils.hs+162
@@ -606,4 +606,166 @@ linearArg (Bind n (Pi Rig1 _ _ _) sc) = True
606606linearArg (Bind n (Pi _ _ _ _) sc) = linearArg sc
607607linearArg _ = False
608608
609+-- Rule out alternatives that don't return the same type as the head of the goal
610+-- (If there are none left as a result, do nothing)
611+pruneByType :: Bool -> -- In an impossible clause
612+ Env -> Term -> -- head of the goal
613+ Type -> -- goal
614+ IState -> [PTerm] -> [PTerm]
615+-- if an alternative has a locally bound name at the head, take it
616+pruneByType imp env t goalty c as
617+ | Just a <- locallyBound as = [a]
618+ where
619+ locallyBound [] = Nothing
620+ locallyBound (t:ts)
621+ | Just n <- getName t,
622+ n `elem` map fstEnv env = Just t
623+ | otherwise = locallyBound ts
624+ getName (PRef _ _ n) = Just n
625+ getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays
626+ | l == txt "Delay" = getName (getTm arg)
627+ getName (PApp _ f _) = getName f
628+ getName (PHidden t) = getName t
629+ getName _ = Nothing
630+
631+-- 'n' is the name at the head of the goal type
632+pruneByType imp env (P _ n _) goalty ist as
633+-- if the goal type is polymorphic, keep everything
634+ | Nothing <- lookupTyExact n ctxt = as
635+-- if the goal type is a ?metavariable, keep everything
636+ | Just _ <- lookup n (idris_metavars ist) = as
637+ | otherwise
638+ = let asV = filter (headIs True n) as
639+ as' = filter (headIs False n) as in
640+ case as' of
641+ [] -> asV
642+ _ -> as'
643+ where
644+ ctxt = tt_ctxt ist
645+
646+ -- Get the function at the head of the alternative and see if it's
647+ -- a plausible match against the goal type. Keep if so. Also keep if
648+ -- there is a possible coercion to the goal type.
649+ headIs var f (PRef _ _ f') = typeHead var f f'
650+ headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
651+ | l == txt "Delay" = headIs var f (getTm arg)
652+ headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'
653+ headIs var f (PApp _ f' _) = headIs var f f'
654+ headIs var f (PPi _ _ _ _ sc) = headIs var f sc
655+ headIs var f (PHidden t) = headIs var f t
656+ headIs var f t = True -- keep if it's not an application
657+
658+ typeHead var f f'
659+ = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
660+ case lookupTyExact f' ctxt of
661+ Just ty -> case unApply (getRetTy ty) of
662+ (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
663+ -> False
664+ _ -> let ty' = normalise ctxt [] ty in
665+-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty
666+-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $
667+ case unApply (getRetTy ty') of
668+ (V _, _) ->
669+ isPlausible ist var env n ty
670+ _ -> matchingTypes imp (getRetTy ty') goalty
671+ || isCoercion (getRetTy ty') goalty
672+-- May be useful to keep for debugging purposes for a bit:
673+-- let res = matching (getRetTy ty') goalty in
674+-- traceWhen (not res)
675+-- ("Rejecting " ++ show (getRetTy ty', goalty)) res
676+ _ -> False
677+
678+ matchingTypes True = matchingHead
679+ matchingTypes False = matching
680+
681+ -- If the goal is a constructor, it must match the suggested function type
682+ matching (P _ ctyn _) (P _ n' _)
683+ | isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'
684+ | otherwise = True
685+ -- Variables match anything
686+ matching (V _) _ = True
687+ matching _ (V _) = True
688+ matching _ (P _ n _) = not (isTConName n ctxt)
689+ matching (P _ n _) _ = not (isTConName n ctxt)
690+ -- Binders are a plausible match, so keep them
691+ matching (Bind n _ sc) _ = True
692+ matching _ (Bind n _ sc) = True
693+ -- If we hit a function name, it's a plausible match
694+ matching apl@(App _ _ _) apr@(App _ _ _)
695+ | (P _ fl _, argsl) <- unApply apl,
696+ (P _ fr _, argsr) <- unApply apr
697+ = fl == fr && and (zipWith matching argsl argsr)
698+ || (not (isConName fl ctxt && isConName fr ctxt))
699+ -- If the application structures aren't easily comparable, it's a
700+ -- plausible match
701+ matching (App _ f a) (App _ f' a') = True
702+ matching (TType _) (TType _) = True
703+ matching (UType _) (UType _) = True
704+ matching l r = l == r
705+
706+ -- In impossible-case mode, only look at the heads (this is to account for
707+ -- the non type-directed case with 'impossible' - we'd be ruling out
708+ -- too much and wouldn't find the mismatch we're looking for)
709+ matchingHead apl@(App _ _ _) apr@(App _ _ _)
710+ | (P _ fl _, argsl) <- unApply apl,
711+ (P _ fr _, argsr) <- unApply apr,
712+ isConName fl ctxt && isConName fr ctxt
713+ = fl == fr
714+ matchingHead _ _ = True
715+
716+ -- Return whether there is a possible coercion between the return type
717+ -- of an alternative and the goal type
718+ isCoercion rty gty | (P _ r _, _) <- unApply rty
719+ = not (null (getCoercionsBetween r gty))
720+ isCoercion _ _ = False
721+
722+ getCoercionsBetween :: Name -> Type -> [Name]
723+ getCoercionsBetween r goal
724+ = let cs = getCoercionsTo ist goal in
725+ findCoercions r cs
726+ where findCoercions t [] = []
727+ findCoercions t (n : ns) =
728+ let ps = case lookupTy n (tt_ctxt ist) of
729+ [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in
730+ [n | any useR as]
731+ _ -> [] in
732+ ps ++ findCoercions t ns
733+
734+ useR ty =
735+ case unApply (getRetTy ty) of
736+ (P _ t _, _) -> t == r
737+ _ -> False
738+
739+
740+pruneByType _ _ t _ _ as = as
741+
742+-- Could the name feasibly be the return type?
743+-- If there is an interface constraint on the return type, and no implementation
744+-- in the environment or globally for that name, then no
745+-- Otherwise, yes
746+-- (FIXME: This isn't complete, but I'm leaving it here and coming back
747+-- to it later - just returns 'var' for now. EB)
748+isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
749+isPlausible ist var env n ty
750+ = let (hvar, interfaces) = collectConstraints [] [] ty in
751+ case hvar of
752+ Nothing -> True
753+ Just rth -> var -- trace (show (rth, interfaces)) var
754+ where
755+ collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
756+ (Maybe Name, [(Term, [Name])])
757+ collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)
758+ = let tcs' = case unApply ty of
759+ (P _ c _, _) ->
760+ case lookupCtxtExact c (idris_interfaces ist) of
761+ Just tc -> ((ty, map fst (interface_implementations tc))
762+ : tcs)
763+ Nothing -> tcs
764+ _ -> tcs
765+ in
766+ collectConstraints (n : env) tcs' sc
767+ collectConstraints env tcs t
768+ | (V i, _) <- unApply t = (Just (env !! i), tcs)
769+ | otherwise = (Nothing, tcs)
770+
609771
test/totality021/expected+4
@@ -3,3 +3,7 @@ Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNot
33totality021.idr:12:1:
44Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'
55totality021.idr:18:1:Main.v is possibly not total due to: Main.sLevelNotSLevel
6+totality021a.idr:9:1:
7+Main.noNonEmptyPointInt is not total as there are missing cases
8+totality021a.idr:12:1:
9+Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt
test/totality021/run+1
@@ -1,3 +1,4 @@
11#!/usr/bin/env bash
22${IDRIS:-idris} $@ totality021.idr --check
3+${IDRIS:-idris} $@ totality021a.idr --check
34rm -f *.ibc
test/totality021/totality021a.idrnew file+12
@@ -0,0 +1,12 @@
1+%default total
2+
3+-- Testing that overloaded names are properly spotted in impossible cases
4+data Point : Nat -> t -> Type where
5+ Nil : Point Z t
6+ (::) : Num t => t -> Point n t -> Point (S n) t
7+
8+noNonEmptyPointInt : (Point (S n) Int) -> Void
9+noNonEmptyPointInt {n} Nil impossible
10+
11+myVoid : Void
12+myVoid = noNonEmptyPointInt [2]