f467346 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Detect implicit parameters to interfaces

f467346Edwin Brady10 years ago

CHANGELOG.md+10

compare with master

unifiedsplit

@@ -21,6 +21,16 @@

21 score->attempted $= (+1) } st

22 ```

24+* Implicit parameter to interfaces are now allowed. For example:

25+

26+ ```

27+ interface Shows (ts : Vect k Type) where

28+ shows : HVect ts -> Vect k String

29+ ```

30+ In this interface, `k` is an implicit parameter, but previously needed to

31+ be explicit

32+

33+

24## Library updates

34## Library updates

26* The File Effect has been updated to take into account changes in

36* The File Effect has been updated to take into account changes in

src/Idris/AbsSyntax.hs+3−3

@@ -444,10 +444,10 @@ addImplementation :: Bool -- ^ whether the name is an Integer implementation

444addImplementation int res n i

445 = do ist <- getIState

446 case lookupCtxt n (idris_interfaces ist) of

447− [CI a b c d e ins fds] ->

447+ [CI a b c d e f ins fds] ->

448− do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_interfaces ist)

448+ do let cs = addDef n (CI a b c d e f (addI i ins) fds) (idris_interfaces ist)

449 putIState $ ist { idris_interfaces = cs }

450− _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_interfaces ist)

450+ _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)

451 putIState $ ist { idris_interfaces = cs }

452 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]

453 addI i ins | int = (i, res) : ins

src/Idris/AbsSyntaxTree.hs+1

@@ -1399,6 +1399,7 @@ data InterfaceInfo = CI {

1399 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method

1400 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl

1401 , interface_default_super_interfaces :: [PDecl]

1402+ , interface_impparams :: [Name]

1402 , interface_params :: [Name]

1403 , interface_params :: [Name]

1403 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded

1404 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded

1404 , interface_determiners :: [Int]

1405 , interface_determiners :: [Int]

src/Idris/Core/TT.hs+9−1

@@ -38,7 +38,7 @@ module Idris.Core.TT(

38 , bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact

39 , discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname

40 , fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv

41− , freeNames, getArgTys, getRetTy, implicitable, instantiate, internalNS

41+ , freeNames, getArgTys, getRetTy, substRetTy, implicitable, instantiate, internalNS

42 , intTyName, isInjective, isTypeConst, lookupCtxt

43 , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth

44 , nextName, noOccurrence, nsroot, occurrences

@@ -1449,6 +1449,14 @@ getRetTy (Bind n (PVTy _) sc) = getRetTy sc

1449getRetTy (Bind n (Pi _ _ _) sc) = getRetTy sc

1450getRetTy sc = sc

1451

1452+-- | As getRetTy but substitutes names for de Bruijn indices

1453+substRetTy :: TT n -> TT n

1454+substRetTy (Bind n (PVar ty) sc) = substRetTy (substV (P Ref n ty) sc)

1455+substRetTy (Bind n (PVTy ty) sc) = substRetTy (substV (P Ref n ty) sc)

1456+substRetTy (Bind n (Pi _ ty _) sc) = substRetTy (substV (P Ref n ty) sc)

1457+substRetTy sc = sc

1458+

1459+

1452uniqueNameFrom :: [Name] -> [Name] -> Name

1460uniqueNameFrom :: [Name] -> [Name] -> Name

1453uniqueNameFrom [] hs = uniqueName (nextName (sUN "x")) hs

1461uniqueNameFrom [] hs = uniqueName (nextName (sUN "x")) hs

1454uniqueNameFrom (s : supply) hs

1462uniqueNameFrom (s : supply) hs

src/Idris/Elab/Implementation.hs+11−3

@@ -129,11 +129,17 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

129 = case lookupTyExact iname (tt_ctxt ist) of

130 Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)

131 _ -> (zip headVars (repeat Placeholder), Erased)

132+

133+ let impps = getImpParams ist (interface_impparams ci)

134+ (snd (unApply (substRetTy ty)))

135+ let iimpps = zip (interface_impparams ci) impps

136+

137+ logElab 5 $ "ImpPS: " ++ show impps ++ " --- " ++ show iimpps

132− logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty

138+ logElab 5 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty

133

139

134 let all_meths = map (nsroot . fst) (interface_methods ci)

140 let all_meths = map (nsroot . fst) (interface_methods ci)

135 let mtys = map (\ (n, (inj, op, t)) ->

141 let mtys = map (\ (n, (inj, op, t)) ->

136− let t_in = substMatchesShadow ips pnames t

142+ let t_in = substMatchesShadow (iimpps ++ ips) pnames t

137 mnamemap =

143 mnamemap =

138 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))

144 map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))

139 (map (toImp fc) headVars)))

145 (map (toImp fc) headVars)))

@@ -142,7 +148,7 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

142 (decorate ns iname n,

148 (decorate ns iname n,

143 op, coninsert cs pextra t', t'))

149 op, coninsert cs pextra t', t'))

144 (interface_methods ci)

150 (interface_methods ci)

145− logElab 3 (show (mtys, ips))

151+ logElab 5 (show (mtys, (iimpps ++ ips)))

146 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci)))

152 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (interface_methods ci)))

147 let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds

153 let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds

148 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")

154 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")

@@ -208,6 +214,8 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

208 addIBC (IBCImplementation intImpl (isNothing expn) n iname)

214 addIBC (IBCImplementation intImpl (isNothing expn) n iname)

209

215

210 where

216 where

217+ getImpParams ist = zipWith (\n tm -> delab ist tm)

218+

211 intImpl = case ps of

219 intImpl = case ps of

212 [PConstant NoFC (AType (ATInt ITNative))] -> True

220 [PConstant NoFC (AType (ATInt ITNative))] -> True

213 _ -> False

221 _ -> False

src/Idris/Elab/Interface.hs+28−12

@@ -62,10 +62,10 @@ elabInterface :: ElabInfo

62 -> SyntaxInfo

63 -> Docstring (Either Err PTerm)

64 -> FC

65− -> [(Name, PTerm)]

65+ -> [(Name, PTerm)] -- ^ Superclass constraints

66 -> Name

67 -> FC

68− -> [(Name, FC, PTerm)]

68+ -> [(Name, FC, PTerm)] -- ^ Parameters

69 -> [(Name, Docstring (Either Err PTerm))]

70 -> [(Name, FC)] -- ^ determining params

71 -> [PDecl] -- ^ interface body

@@ -74,7 +74,6 @@ elabInterface :: ElabInfo

74 -> Idris ()

75elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

76 = do let cn = fromMaybe (SN (ImplementationCtorN tn)) (fst <$> mcn)

77− let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

78 let constraint = PApp fc (PRef fc [] tn)

77 let constraint = PApp fc (PRef fc [] tn)

79 (map (pexp . PRef fc []) (map (\(n, _, _) -> n) ps))

78 (map (pexp . PRef fc []) (map (\(n, _, _) -> n) ps))

@@ -82,6 +81,20 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

82 syn_in { using = addToUsing (using syn_in)

81 syn_in { using = addToUsing (using syn_in)

83 [(pn, pt) | (pn, _, pt) <- ps]

82 [(pn, pt) | (pn, _, pt) <- ps]

84 }

83 }

84+

85+ -- Calculate implicit parameters

86+ ist <- getIState

87+ let impps_ns = nub $ map (\n -> (n, emptyFC, Placeholder)) $

88+ concatMap (implicitNamesIn [] ist)

89+ (map (\ (_,_,x) -> x) ps)

90+ let impps = filter (\ (n, _, _) ->

91+ n `notElem` (map (\ (n, _, _) -> n) ps)) impps_ns

92+

93+ let tty = impbind (map (\(n, _, ty) -> (n, ty)) impps) $

94+ pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

95+

96+ logElab 5 $ "Implicit parameters are " ++ show impps

97+ logElab 5 $ "Interface type is " ++ showTmImpls tty

86 -- build data declaration

99 -- build data declaration

87 let mdecls = filter tydecl ds -- method declarations

100 let mdecls = filter tydecl ds -- method declarations

@@ -95,7 +108,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

95 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames

108 mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames

109

97 logElab 2 $ "Building methods " ++ show mnames

110 logElab 2 $ "Building methods " ++ show mnames

98− ims <- mapM (tdecl mnames) mdecls

111+ ims <- mapM (tdecl impps mnames) mdecls

99 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

112 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

100 (filter clause ds)

113 (filter clause ds)

101 let (methods, imethods)

114 let (methods, imethods)

@@ -103,20 +116,23 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

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

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

104

117

105 -- build implementation constructor type

118 -- build implementation constructor type

106− let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints

119+ let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $ conbind constraints

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

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

108 constraint

121 constraint

109

122

110 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]

123 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]

111 let ddecl = PDatadecl tn NoFC tty cons

124 let ddecl = PDatadecl tn NoFC tty cons

112

125

113− logElab 5 $ "Interface data " ++ show (showDImp verbosePPOption ddecl)

126+ logElab 5 $ "Interface " ++ show (showDImp verbosePPOption ddecl)

114

127

115 -- Elaborate the data declaration

128 -- Elaborate the data declaration

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

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

117 imp_methods = mnames }) doc pDocs fc [] ddecl

130 imp_methods = mnames }) doc pDocs fc [] ddecl

118 dets <- findDets cn (map fst fds)

131 dets <- findDets cn (map fst fds)

119− addInterface tn (CI cn (map nodoc imethods) defaults idecls (map (\(n, _, _) -> n) ps) [] dets)

132+ addInterface tn (CI cn (map nodoc imethods) defaults idecls

133+ (map (\(n, _, _) -> n) impps)

134+ (map (\(n, _, _) -> n) ps)

135+ [] dets)

120

136

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

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

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

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

@@ -188,14 +204,14 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

188 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

204 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

189 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n

205 getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n

190

206

191− tdecl allmeths (PTy doc _ syn _ o n nfc t)

207+ tdecl impps allmeths (PTy doc _ syn _ o n nfc t)

192− = do t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

208+ = do t' <- implicit' info syn (map (\(n, _, _) -> n) (impps ++ ps) ++ allmeths) n t

193 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

209 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

194 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

210 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

195 (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

211 (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

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

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

197 (n, (nfc, syn, o, t) ) )

213 (n, (nfc, syn, o, t) ) )

198− tdecl allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))

214+ tdecl impps allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t))

199 = do let o = []

215 = do let o = []

200 t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

216 t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

201 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'

217 logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'

@@ -203,9 +219,9 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

203 (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

219 (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

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

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

205 (n, (nfc, syn, o, t) ) )

221 (n, (nfc, syn, o, t) ) )

206− tdecl allmeths (PData doc _ syn _ _ _)

222+ tdecl impps allmeths (PData doc _ syn _ _ _)

207 = ierror $ At fc (Msg "Data definitions not allowed in an interface declaration")

223 = ierror $ At fc (Msg "Data definitions not allowed in an interface declaration")

208− tdecl _ _ = ierror $ At fc (Msg "Not allowed in an interface declaration")

224+ tdecl _ _ _ = ierror $ At fc (Msg "Not allowed in an interface declaration")

209

225

210 -- Create default definitions

226 -- Create default definitions

211 defdecl mtys c d@(PClauses fc opts n cs) =

227 defdecl mtys c d@(PClauses fc opts n cs) =

src/Idris/IBC.hs+6−4

@@ -47,7 +47,7 @@ import System.Directory

47import System.FilePath

49ibcVersion :: Word16

50−ibcVersion = 149

50+ibcVersion = 150

52-- | When IBC is being loaded - we'll load different things (and omit

53-- different structures/definitions) depending on which phase we're in.

@@ -551,7 +551,7 @@ processInterfaces ar = do

551 -- Don't lose implementations from previous IBCs, which

552 -- could have loaded in any order

553 let is = case lookupCtxtExact n (idris_interfaces i) of

554− Just (CI _ _ _ _ _ ins _) -> ins

554+ Just ci -> interface_implementations ci

555 _ -> []

556 let c' = c { interface_implementations = interface_implementations c ++ is }

557 putIState (i { idris_interfaces = addDef n c' (idris_interfaces i) })) cs

@@ -2354,13 +2354,14 @@ instance (Binary t) => Binary (PArg' t) where

2354

2355

2356instance Binary InterfaceInfo where

2357− put (CI x1 x2 x3 x4 x5 _ x6)

2357+ put (CI x1 x2 x3 x4 x5 x6 _ x7)

2358 = do put x1

2359 put x2

2360 put x3

2361 put x4

2362 put x5

2363 put x6

2364+ put x7

2364 get

2365 get

2365 = do x1 <- get

2366 = do x1 <- get

2366 x2 <- get

2367 x2 <- get

@@ -2368,7 +2369,8 @@ instance Binary InterfaceInfo where

2368 x4 <- get

2369 x4 <- get

2369 x5 <- get

2370 x5 <- get

2370 x6 <- get

2371 x6 <- get

2372+ x7 <- get

2371− return (CI x1 x2 x3 x4 x5 [] x6)

2373+ return (CI x1 x2 x3 x4 x5 x6 [] x7)

2372

2374

2373instance Binary RecordInfo where

2375instance Binary RecordInfo where

2374 put (RI x1 x2 x3)

2376 put (RI x1 x2 x3)

src/Idris/ProofSearch.hs+2−2

@@ -525,8 +525,8 @@ findImplementations :: IState -> Term -> [Name]

525findImplementations ist t

526 | (P _ n _, _) <- unApply (getRetTy t)

527 = case lookupCtxt n (idris_interfaces ist) of

528− [CI _ _ _ _ _ ins _] ->

528+ [ci] -> let ins = interface_implementations ci in

529− [n | (n, True) <- ins, accessible n]

529+ [n | (n, True) <- ins, accessible n]

530 _ -> []

531 | otherwise = []

532 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of