1054d7d · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Utils.idr+1

compare with master

unifiedsplit

@@ -291,6 +291,7 @@ instance Show Err where

291 show UniverseError = "UniverseError"

292 show ProgramLineComment = "ProgramLineComment"

293 show (Inaccessible n) = "Inaccessible " ++ show n

294+ show (UnknownImplicit n f) = "UnknownImplicit " ++ show n ++ " " ++ show f

294 show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n

295 show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n

295 show (AlreadyDefined n) = "AlreadyDefined " ++ show n

296 show (AlreadyDefined n) = "AlreadyDefined " ++ show n

296 show (ProofSearchFail err) = "ProofSearchFail " ++ show err

297 show (ProofSearchFail err) = "ProofSearchFail " ++ show err

libs/prelude/Language/Reflection/Errors.idr+1

@@ -36,6 +36,7 @@ data Err = Msg String

36 | UniverseError

37 | ProgramLineComment

38 | Inaccessible TTName

39+ | UnknownImplicit TTName TTName

39 | NonCollapsiblePostulate TTName

40 | NonCollapsiblePostulate TTName

40 | AlreadyDefined TTName

41 | AlreadyDefined TTName

41 | ProofSearchFail Err

42 | ProofSearchFail Err

src/Idris/AbsSyntax.hs+24−7

@@ -1622,7 +1622,13 @@ addImpl' inpat env infns imp_meths ist ptm

1622-- if in a pattern, and there are no arguments, and there's no possible

1623-- names with zero explicit arguments, don't add implicits.

1624

1625−aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> FC -> [[T.Text]] -> [PArg] -> Either Err PTerm

1625+aiFn :: Bool -> Bool -> Bool

1626+ -> [Name]

1627+ -> IState -> FC

1628+ -> Name -- ^ function being applied

1629+ -> FC -> [[T.Text]]

1630+ -> [PArg] -> -- ^ initial arguments

1631+ Either Err PTerm

1626aiFn inpat True qq imp_meths ist fc f ffc ds []

1632aiFn inpat True qq imp_meths ist fc f ffc ds []

1627 = case lookupDef f (tt_ctxt ist) of

1633 = case lookupDef f (tt_ctxt ist) of

1628 [] -> Right $ PPatvar ffc f

1634 [] -> Right $ PPatvar ffc f

@@ -1685,8 +1691,20 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

1685 Just (n,t) -> t

1691 Just (n,t) -> t

1686 _ -> Public

1692 _ -> Public

1687

1693

1688− insertImpl :: [PArg] -> [PArg] -> [PArg]

1694+ insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)

1695+ -> [PArg] -- ^ given arguments

1696+ -> [PArg]

1697+ insertImpl ps as

1698+ = let (as', badimpls) = partition (impIn ps) as in

1699+ map addUnknownImp badimpls ++

1689− insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not . exp) as)

1700+ insImpAcc M.empty ps (filter exp as') (filter (not . exp) as')

1701+

1702+ -- return True if the second argument is an implicit argument which is

1703+ -- expected in the implicits, or if it's not an implicit

1704+ impIn :: [PArg] -> PArg -> Bool

1705+ impIn ps (PExp _ _ _ _) = True

1706+ impIn ps (PConstraint _ _ _ _) = True

1707+ impIn ps arg = any (\p -> pname arg == pname p) ps

1690

1708

1691 exp (PExp _ _ _ _) = True

1709 exp (PExp _ _ _ _) = True

1692 exp (PConstraint _ _ _ _) = True

1710 exp (PConstraint _ _ _ _) = True

@@ -1723,12 +1741,11 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

1723 insImpAcc (M.insert n Placeholder pnas) ps given imps

1741 insImpAcc (M.insert n Placeholder pnas) ps given imps

1724 else PTacImplicit p l n sc sc :

1742 else PTacImplicit p l n sc sc :

1725 insImpAcc (M.insert n sc pnas) ps given imps

1743 insImpAcc (M.insert n sc pnas) ps given imps

1726− insImpAcc _ expected [] imps = imps -- so that unused implicits give error

1744+ insImpAcc _ expected [] imps = map addUnknownImp imps -- so that unused implicits give error

1727− -- TODO: report here, and prune alternatives

1728− -- Issue #1740 in the Issue Tracker

1729−-- https://github.com/idris-lang/Idris-dev/issues/1740

1730 insImpAcc _ _ given imps = given ++ imps

1745 insImpAcc _ _ given imps = given ++ imps

1731

1746

1747+ addUnknownImp arg = arg { argopts = UnknownImp : argopts arg }

1748+

1732 find n [] acc = Nothing

1749 find n [] acc = Nothing

1733 find n (PImp _ _ _ n' t : gs) acc

1750 find n (PImp _ _ _ n' t : gs) acc

1734 | n == n' = Just (t, reverse acc ++ gs)

1751 | n == n' = Just (t, reverse acc ++ gs)

src/Idris/AbsSyntaxTree.hs+3−2

@@ -987,7 +987,8 @@ type PDo = PDo' PTerm

987data PArg' t = PImp { priority :: Int,

988 machine_inf :: Bool, -- true if the machine inferred it

989 argopts :: [ArgOpt],

990− pname :: Name, getTm :: t }

990+ pname :: Name,

991+ getTm :: t }

991 | PExp { priority :: Int,

992 | PExp { priority :: Int,

992 argopts :: [ArgOpt],

993 argopts :: [ArgOpt],

993 pname :: Name,

994 pname :: Name,

@@ -1003,7 +1004,7 @@ data PArg' t = PImp { priority :: Int,

1003 getTm :: t }

1004 getTm :: t }

1004 deriving (Show, Eq, Functor, Data, Typeable)

1005 deriving (Show, Eq, Functor, Data, Typeable)

1005

1006

1006−data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg

1007+data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp

1007 deriving (Show, Eq, Data, Typeable)

1008 deriving (Show, Eq, Data, Typeable)

1008

1009

1009instance Sized a => Sized (PArg' a) where

1010instance Sized a => Sized (PArg' a) where

src/Idris/Core/Binary.hs+5

@@ -179,6 +179,9 @@ instance Binary a => Binary (Err' a) where

179 put t

180 put (ElabScriptStuck x1) = do putWord8 39

181 put x1

182+ put (UnknownImplicit n f) = do putWord8 40

183+ put n

184+ put f

182

185

183 get = do i <- getWord8

186 get = do i <- getWord8

184 case i of

187 case i of

@@ -246,6 +249,8 @@ instance Binary a => Binary (Err' a) where

246 return (InvalidTCArg x1 x2)

249 return (InvalidTCArg x1 x2)

247 39 -> do x1 <- get

250 39 -> do x1 <- get

248 return (ElabScriptStuck x1)

251 return (ElabScriptStuck x1)

252+ 40 -> do x <- get ; y <- get

253+ return $ UnknownImplicit x y

249 _ -> error "Corrupted binary data for Err'"

254 _ -> error "Corrupted binary data for Err'"

250----- Generated by 'derive'

255----- Generated by 'derive'

251

256

src/Idris/Core/DeepSeq.hs+1

@@ -98,6 +98,7 @@ instance NFData Err where

98 rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

99 rnf ProgramLineComment = ()

100 rnf (Inaccessible x1) = rnf x1 `seq` ()

101+ rnf (UnknownImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

101 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

102 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

102 rnf (AlreadyDefined x1) = rnf x1 `seq` ()

103 rnf (AlreadyDefined x1) = rnf x1 `seq` ()

103 rnf (ProofSearchFail x1) = rnf x1 `seq` ()

104 rnf (ProofSearchFail x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+2

@@ -231,6 +231,7 @@ data Err' t

231 | UniqueKindError Universe Name

232 | ProgramLineComment

233 | Inaccessible Name

234+ | UnknownImplicit Name Name

234 | CantMatch t

235 | CantMatch t

235 | NonCollapsiblePostulate Name

236 | NonCollapsiblePostulate Name

236 | AlreadyDefined Name

237 | AlreadyDefined Name

@@ -332,6 +333,7 @@ instance Show Err where

332 show e ++ " in " ++ show sc ++ " " ++ show i

333 show e ++ " in " ++ show sc ++ " " ++ show i

333 show (CantSolveGoal g _) = "CantSolve " ++ show g

334 show (CantSolveGoal g _) = "CantSolve " ++ show g

334 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

335 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

336+ show (UnknownImplicit n f) = show n ++ " is not an implicit argument of " ++ show f

335 show (ProviderError msg) = "Type provider error: " ++ msg

337 show (ProviderError msg) = "Type provider error: " ++ msg

336 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

338 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

337 show ProgramLineComment = "Program line next to comment"

339 show ProgramLineComment = "Program line next to comment"

src/Idris/Delaborate.hs+1

@@ -338,6 +338,7 @@ pprintErr' i (UniqueKindError k n) = text "Constructor" <+> annName' n (showbasi

338 <+> text "but the data type does not"

339pprintErr' i ProgramLineComment = text "Program line next to comment"

340pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

341+pprintErr' i (UnknownImplicit n f) = annName n <+> text "is not an implicit argument of" <+> annName f

341pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

342pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

342 annName n <+> text "is not collapsible"

343 annName n <+> text "is not collapsible"

343pprintErr' i (AlreadyDefined n) = annName n<+>

344pprintErr' i (AlreadyDefined n) = annName n<+>

src/Idris/Elab/Term.hs+8−1

@@ -708,6 +708,7 @@ elab ist info emode opts fn tm

708 ctxt <- get_context

709 annot <- findHighlight f

710 let args = insertScopedImps fc (normalise ctxt env fty) args_in

711+ mapM_ checkKnownImplicit args

711 let unmatchableArgs = if pattern

712 let unmatchableArgs = if pattern

712 then getUnmatchable (tt_ctxt ist) f

713 then getUnmatchable (tt_ctxt ist) f

713 else []

714 else []

@@ -715,6 +716,7 @@ elab ist info emode opts fn tm

715 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

716 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

716 && isTConName f (tt_ctxt ist)) $

717 && isTConName f (tt_ctxt ist)) $

717 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

718 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

719+-- trace (show (f, args_in, args)) $

718 if (f `elem` map fst env && length args == 1 && length args_in == 1)

720 if (f `elem` map fst env && length args == 1 && length args_in == 1)

719 then -- simple app, as below

721 then -- simple app, as below

720 do simple_app False

722 do simple_app False

@@ -805,7 +807,12 @@ elab ist info emode opts fn tm

805 [] -> return ()

807 [] -> return ()

806 es -> do put s

808 es -> do put s

807 elab' ina topfc (PAppImpl tm es)

809 elab' ina topfc (PAppImpl tm es)

808−

810+

811+ checkKnownImplicit imp

812+ | UnknownImp `elem` argopts imp

813+ = lift $ tfail $ UnknownImplicit (pname imp) f

814+ checkKnownImplicit _ = return ()

815+

809 getReqImps (Bind x (Pi (Just i) ty _) sc)

816 getReqImps (Bind x (Pi (Just i) ty _) sc)

810 = i : getReqImps sc

817 = i : getReqImps sc

811 getReqImps _ = []

818 getReqImps _ = []

src/Idris/IBC.hs+2

@@ -1071,12 +1071,14 @@ instance Binary ArgOpt where

1071 HideDisplay -> putWord8 0

1072 InaccessibleArg -> putWord8 1

1073 AlwaysShow -> putWord8 2

1074+ UnknownImp -> putWord8 3

1074 get

1075 get

1075 = do i <- getWord8

1076 = do i <- getWord8

1076 case i of

1077 case i of

1077 0 -> return HideDisplay

1078 0 -> return HideDisplay

1078 1 -> return InaccessibleArg

1079 1 -> return InaccessibleArg

1079 2 -> return AlwaysShow

1080 2 -> return AlwaysShow

1081+ 3 -> return UnknownImp

1080 _ -> error "Corrupted binary data for Static"

1082 _ -> error "Corrupted binary data for Static"

1081

1083

1082instance Binary Static where

1084instance Binary Static where

src/Idris/Reflection.hs+1

@@ -853,6 +853,7 @@ reflectErr (UniverseError fc ue old new tys) =

853 Var $ reflErrName "UniverseError"

854reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

855reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

856+reflectErr (UnknownImplicit n f) = raw_apply (Var $ reflErrName "UnknownImplicit") [reflectName n, reflectName f]

856reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

857reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

857reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

858reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]

858reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

859reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]