174395b · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -289,6 +289,9 @@ Extra-source-files:

289 test/reg058/run

290 test/reg058/*.idr

291 test/reg058/expected

292+ test/reg059/run

293+ test/reg059/*.idr

294+ test/reg059/expected

292

295

293 test/basic001/run

296 test/basic001/run

294 test/basic001/*.idr

297 test/basic001/*.idr

src/Idris/AbsSyntax.hs+28−18

@@ -1475,31 +1475,34 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1475

1476-- Add implicit arguments in function calls

1477addImplPat :: IState -> PTerm -> PTerm

1478−addImplPat = addImpl' True [] []

1478+addImplPat = addImpl' True [] [] []

1479

1480addImplBound :: IState -> [Name] -> PTerm -> PTerm

1481−addImplBound ist ns = addImpl' False ns [] ist

1481+addImplBound ist ns = addImpl' False ns [] [] ist

1482

1483addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm

1484−addImplBoundInf ist ns inf = addImpl' False ns inf ist

1484+addImplBoundInf ist ns inf = addImpl' False ns inf [] ist

1485

1486-- | Add the implicit arguments to applications in the term

1487+-- [Name] gives the names to always expend, even when under a binder of

1488+-- that name (this is to expand methods with implicit arguments in dependent

1489+-- type classes).

1487−addImpl :: IState -> PTerm -> PTerm

1490+addImpl :: [Name] -> IState -> PTerm -> PTerm

1488addImpl = addImpl' False [] []

1491addImpl = addImpl' False [] []

1489

1492

1490-- TODO: in patterns, don't add implicits to function names guarded by constructors

1493-- TODO: in patterns, don't add implicits to function names guarded by constructors

1491-- and *not* inside a PHidden

1494-- and *not* inside a PHidden

1492

1495

1493−addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1496+addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1494−addImpl' inpat env infns ist ptm

1497+addImpl' inpat env infns imp_meths ist ptm

1495 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)

1498 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)

1496 where

1499 where

1497 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1500 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1498 ai qq env ds (PRef fc f)

1501 ai qq env ds (PRef fc f)

1499 | f `elem` infns = PInferRef fc f

1502 | f `elem` infns = PInferRef fc f

1500− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1503+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []

1501 ai qq env ds (PHidden (PRef fc f))

1504 ai qq env ds (PHidden (PRef fc f))

1502− | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])

1505+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])

1503 ai qq env ds (PEq fc lt rt l r)

1506 ai qq env ds (PEq fc lt rt l r)

1504 = let lt' = ai qq env ds lt

1507 = let lt' = ai qq env ds lt

1505 rt' = ai qq env ds rt

1508 rt' = ai qq env ds rt

@@ -1535,7 +1538,7 @@ addImpl' inpat env infns ist ptm

1535 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)

1538 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)

1536 | not (f `elem` map fst env)

1539 | not (f `elem` map fst env)

1537 = let as' = map (fmap (ai qq env ds)) as in

1540 = let as' = map (fmap (ai qq env ds)) as in

1538− handleErr $ aiFn inpat False qq ist fc f ds as'

1541+ handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'

1539 | Just (Just ty) <- lookup f env =

1542 | Just (Just ty) <- lookup f env =

1540 let as' = map (fmap (ai qq env ds)) as

1543 let as' = map (fmap (ai qq env ds)) as

1541 arity = getPArity ty in

1544 arity = getPArity ty in

@@ -1570,7 +1573,9 @@ addImpl' inpat env infns ist ptm

1570 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])

1573 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])

1571 ai qq env ds (PPi p n ty sc)

1574 ai qq env ds (PPi p n ty sc)

1572 = let ty' = ai qq env ds ty

1575 = let ty' = ai qq env ds ty

1576+ env' = if n `elem` imp_meths then env

1573− sc' = ai qq ((n, Just ty):env) ds sc in

1577+ else ((n, Just ty) : env)

1578+ sc' = ai qq env' ds sc in

1574 PPi p n ty' sc'

1579 PPi p n ty' sc'

1575 ai qq env ds (PGoal fc r n sc)

1580 ai qq env ds (PGoal fc r n sc)

1576 = let r' = ai qq env ds r

1581 = let r' = ai qq env ds r

@@ -1594,8 +1599,8 @@ addImpl' inpat env infns ist ptm

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

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

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

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

1596

1601

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

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

1598−aiFn inpat True qq ist fc f ds []

1603+aiFn inpat True qq imp_meths ist fc f ds []

1599 = case lookupDef f (tt_ctxt ist) of

1604 = case lookupDef f (tt_ctxt ist) of

1600 [] -> Right $ PPatvar fc f

1605 [] -> Right $ PPatvar fc f

1601 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

1606 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1603,7 +1608,7 @@ aiFn inpat True qq ist fc f ds []

1603 if (not (vname f) || tcname f

1608 if (not (vname f) || tcname f

1604 || any (conCaf (tt_ctxt ist)) ialts)

1609 || any (conCaf (tt_ctxt ist)) ialts)

1605-- any constructor alts || any allImp ialts))

1610-- any constructor alts || any allImp ialts))

1606− then aiFn inpat False qq ist fc f ds [] -- use it as a constructor

1611+ then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor

1607 else Right $ PPatvar fc f

1612 else Right $ PPatvar fc f

1608 where imp (PExp _ _ _ _) = False

1613 where imp (PExp _ _ _ _) = False

1609 imp _ = True

1614 imp _ = True

@@ -1617,9 +1622,9 @@ aiFn inpat True qq ist fc f ds []

1617 vname (UN n) = True -- non qualified

1622 vname (UN n) = True -- non qualified

1618 vname _ = False

1623 vname _ = False

1619

1624

1620−aiFn inpat expat qq ist fc f ds as

1625+aiFn inpat expat qq imp_meths ist fc f ds as

1621 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1626 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1622−aiFn inpat expat qq ist fc f ds as

1627+aiFn inpat expat qq imp_meths ist fc f ds as

1623 -- This is where namespaces get resolved by adding PAlternative

1628 -- This is where namespaces get resolved by adding PAlternative

1624 = do let ns = lookupCtxtName f (idris_implicits ist)

1629 = do let ns = lookupCtxtName f (idris_implicits ist)

1625 let nh = filter (\(n, _) -> notHidden n) ns

1630 let nh = filter (\(n, _) -> notHidden n) ns

@@ -1627,15 +1632,20 @@ aiFn inpat expat qq ist fc f ds as

1627 [] -> nh

1632 [] -> nh

1628 x -> x

1633 x -> x

1629 case ns' of

1634 case ns' of

1630− [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1635+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)

1631 [] -> if f `elem` (map fst (idris_metavars ist))

1636 [] -> if f `elem` (map fst (idris_metavars ist))

1632 then Right $ PApp fc (PRef fc f) as

1637 then Right $ PApp fc (PRef fc f) as

1633 else Right $ mkPApp fc (length as) (PRef fc f) as

1638 else Right $ mkPApp fc (length as) (PRef fc f) as

1634 alts -> Right $

1639 alts -> Right $

1635 PAlternative True $

1640 PAlternative True $

1636− map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1641+ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))

1637 (insertImpl ns as)) alts

1642 (insertImpl ns as)) alts

1638 where

1643 where

1644+ -- if the name is in imp_meths, we should actually refer to the bound

1645+ -- name rather than the global one after expanding implicits

1646+ isImpName f f' | f `elem` imp_meths = f

1647+ | otherwise = f'

1648+

1639 trimAlts [] alts = alts

1649 trimAlts [] alts = alts

1640 trimAlts ns alts

1650 trimAlts ns alts

1641 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

1651 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

@@ -1679,7 +1689,7 @@ aiFn inpat expat qq ist fc f ds as

1679 PImp p True l n Placeholder :

1689 PImp p True l n Placeholder :

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

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

1681 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

1691 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

1682− let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1692+ let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in

1683 case find n imps [] of

1693 case find n imps [] of

1684 Just (tm, imps') ->

1694 Just (tm, imps') ->

1685 PTacImplicit p l n sc tm :

1695 PTacImplicit p l n sc tm :

src/Idris/AbsSyntaxTree.hs+4−1

@@ -1201,6 +1201,9 @@ data SyntaxInfo = Syn { using :: [Using],

1201 syn_params :: [(Name, PTerm)],

1202 syn_namespace :: [String],

1203 no_imp :: [Name],

1204+ imp_methods :: [Name], -- class methods. When expanding

1205+ -- implicits, these should be expanded even under

1206+ -- binders

1204 decoration :: Name -> Name,

1207 decoration :: Name -> Name,

1205 inPattern :: Bool,

1208 inPattern :: Bool,

1206 implicitAllowed :: Bool,

1209 implicitAllowed :: Bool,

@@ -1214,7 +1217,7 @@ deriving instance NFData SyntaxInfo

1214deriving instance Binary SyntaxInfo

1217deriving instance Binary SyntaxInfo

1215!-}

1218!-}

1216

1219

1217−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0

1220+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0

1218

1221

1219expandNS :: SyntaxInfo -> Name -> Name

1222expandNS :: SyntaxInfo -> Name -> Name

1220expandNS syn n@(NS _ _) = n

1223expandNS syn n@(NS _ _) = n

src/Idris/Coverage.hs+1−1

@@ -24,7 +24,7 @@ import Control.Monad.State.Strict

24-- provided explicitly from new clause generation.

25mkPatTm :: PTerm -> Idris Term

26mkPatTm t = do i <- getIState

27− let timp = addImpl' True [] [] i t

27+ let timp = addImpl' True [] [] [] i t

28 evalStateT (toTT (mapPT deNS timp)) 0

29 where

30 toTT (PRef _ n) = do i <- lift getIState

src/Idris/DeepSeq.hs+2−2

@@ -353,10 +353,10 @@ instance NFData Using where

353 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

354

355instance NFData SyntaxInfo where

356− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

356+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

357 = rnf x1 `seq`

358 rnf x2 `seq`

359 rnf x3 `seq`

360 rnf x4 `seq`

361 rnf x5 `seq`

362− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

362+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

src/Idris/Elab/Class.hs+11−11

@@ -77,28 +77,28 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

77 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

78 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

79 -- build instance constructor type

80− -- decorate names of functions to ensure they can't be referred

81− -- to elsewhere in the class declaration

82 let cty = impbind ps $ conbind constraints

80 let cty = impbind ps $ conbind constraints

83 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

81 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

84 constraint

82 constraint

85 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

83 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

86 let ddecl = PDatadecl tn tty cons

84 let ddecl = PDatadecl tn tty cons

87 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

85 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

86+ -- Elaborate the data declaration

88− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

87+ elabData info (syn { no_imp = no_imp syn ++ mnames,

89−

88+ imp_methods = mnames }) doc pDocs fc [] ddecl

90 dets <- findDets cn fds

89 dets <- findDets cn fds

91 addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)

90 addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)

91+

92 -- for each constraint, build a top level function to chase it

93− logLvl 5 $ "Building functions"

94−-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

95−-- ++ using syn }

96− fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

93+ cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

97− mapM_ (rec_elabDecl info EAll info) (concat fns)

94+ mapM_ (rec_elabDecl info EAll info) (concat cfns)

95+

98 -- for each method, build a top level function

96 -- for each method, build a top level function

99 fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

97 fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

100 logLvl 5 $ "Functions " ++ show fns

98 logLvl 5 $ "Functions " ++ show fns

99+ -- Elaborate the the top level methods

101 mapM_ (rec_elabDecl info EAll info) (concat fns)

100 mapM_ (rec_elabDecl info EAll info) (concat fns)

101+

102 -- add the default definitions

103 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

104 addIBC (IBCClass tn)

@@ -134,8 +134,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

134

135 getMName (PTy _ _ _ _ _ n _) = nsroot n

136 tdecl allmeths (PTy doc _ syn _ o n t)

137− = do t' <- implicit' info syn allmeths n t

137+ = do t' <- implicit' info syn (map fst ps ++ allmeths) n t

138− logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

138+ logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

139 return ( (n, (toExp (map fst ps) Exp t')),

140 (n, (doc, o, (toExp (map fst ps)

141 (\ l s p -> Imp l s p Nothing) t'))),

src/Idris/Elab/Clause.hs+1−1

@@ -548,7 +548,7 @@ elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

548elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

549 = do let tcgen = Dictionary `elem` opts

550 i <- get

551− let lhs = addImpl i lhs_in

551+ let lhs = addImpl [] i lhs_in

552 b <- checkPossible info fc tcgen fname lhs_in

553 case b of

554 True -> tclift $ tfail (At fc

src/Idris/Elab/Data.hs+2−1

@@ -215,6 +215,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

215 Idris (Name, Type)

216elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

217 = do checkUndefined fc n

218+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

218 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

219 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

219 ctxt <- getContext

220 ctxt <- getContext

220 let cty' = normalise ctxt [] cty

221 let cty' = normalise ctxt [] cty

@@ -223,7 +224,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

223 -- Check that the constructor type is, in fact, a part of the family being defined

224 -- Check that the constructor type is, in fact, a part of the family being defined

224 tyIs n cty'

225 tyIs n cty'

225

226

226− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

227+ logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

227 logLvl 5 $ "Inaccessible args: " ++ show inacc

228 logLvl 5 $ "Inaccessible args: " ++ show inacc

228 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

229 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

229

230

src/Idris/Elab/Instance.hs+1−1

@@ -167,7 +167,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

167 = do ty' <- addUsingConstraints syn fc t

168 -- TODO think: something more in info?

169 ty' <- implicit info syn iname ty'

170− let ty = addImpl i ty'

170+ let ty = addImpl [] i ty'

171 ctxt <- getContext

172 (ElabResult tyT _ _ ctxt' newDecls, _) <-

173 tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

src/Idris/Elab/Type.hs+4−4

@@ -57,13 +57,13 @@ buildType info syn fc opts n ty' = do

57 ctxt <- getContext

58 i <- getIState

59

60− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

60+ logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)

61 ty' <- addUsingConstraints syn fc ty'

62 ty' <- addUsingImpls syn n fc ty'

63− let ty = addImpl i ty'

63+ let ty = addImpl (imp_methods syn) i ty'

64

65− logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

65+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66− logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

66+ logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

67

68 (ElabResult tyT' defer is ctxt' newDecls, log) <-

69 tclift $ elaborate ctxt n (TType (UVal 0)) initEState

src/Idris/Elab/Value.hs+1−1

@@ -56,7 +56,7 @@ elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Nam

56elabValBind info aspat norm tm_in

57 = do ctxt <- getContext

58 i <- getIState

59− let tm = addImpl i tm_in

59+ let tm = addImpl [] i tm_in

60 logLvl 10 (showTmImpls tm)

61 -- try:

62 -- * ordinary elaboration

src/Idris/IBC.hs+2−2

@@ -1420,7 +1420,7 @@ instance Binary Using where

1420 _ -> error "Corrupted binary data for Using"

1421

1422instance Binary SyntaxInfo where

1423− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1423+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

1424 = do put x1

1425 put x2

1426 put x3

@@ -1436,7 +1436,7 @@ instance Binary SyntaxInfo where

1436 x5 <- get

1437 x6 <- get

1438 x7 <- get

1439− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)

1439+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)

1440

1441instance (Binary t) => Binary (PClause' t) where

1442 put x

src/Idris/TypeSearch.hs+1−1

@@ -46,7 +46,7 @@ searchByType pkgs pterm = do

46 mapM_ loadPkgIndex pkgs

47 pterm' <- addUsingConstraints syn emptyFC pterm

48 pterm'' <- implicit toplevel syn name pterm'

49− let pterm''' = addImpl i pterm''

49+ let pterm''' = addImpl [] i pterm''

50 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

51 let names = searchUsing searchPred i ty

52 let names' = take numLimit names

test/reg059/expectednew file

No changes to the content.

test/reg059/reg059.idrnew file+8

@@ -0,0 +1,8 @@

1+class Monad m => ContainerMonad (m : Type -> Type) where

2+ Elem : a -> m a -> Type

3+ tagElem : (mx : m a) -> m (x : a ** Elem x mx)

4+

5+class Monad m => ContainerMonad2 a (m : Type -> Type) where

6+ Elem2 : a -> m a -> Type

7+ tagElem2 : (mx : m a) -> m (x : a ** Elem2 x mx)

8+

test/reg059/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg059.idr --check

3+rm -f *.ibc