f467346 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Detect implicit parameters to interfaces

This allows interfaces parameterised by dependent types to be less noisy, and have less noise in the implementations.

commitf467346791f60d73a3536228b8bad1022bc17274 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 7 Oct 2016, 09:57 (10 years ago) parent8c2a516

8 files changed+70−25

compare with master

unifiedsplit

CHANGELOG.md+10 src/Idris/AbsSyntax.hs+3−3 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/TT.hs+9−1 src/Idris/Elab/Implementation.hs+11−3 src/Idris/Elab/Interface.hs+28−12 src/Idris/IBC.hs+6−4 src/Idris/ProofSearch.hs+2−2

CHANGELOG.md+10

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

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

2222 ```

2323

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+

2434## Library updates

2535

2636* 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

444444addImplementation int res n i

445445 = do ist <- getIState

446446 case lookupCtxt n (idris_interfaces ist) of

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

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

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

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

449449 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)

451451 putIState $ ist { idris_interfaces = cs }

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

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

src/Idris/AbsSyntaxTree.hs+1

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

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

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

14011401 , interface_default_super_interfaces :: [PDecl]

1402+ , interface_impparams :: [Name]

14021403 , interface_params :: [Name]

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

14041405 , interface_determiners :: [Int]

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

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

3838 , bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact

3939 , discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname

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

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

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

4242 , intTyName, isInjective, isTypeConst, lookupCtxt

4343 , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth

4444 , nextName, noOccurrence, nsroot, occurrences

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

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

14501450getRetTy sc = sc

14511451

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+

14521460uniqueNameFrom :: [Name] -> [Name] -> Name

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

14541462uniqueNameFrom (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

129129 = case lookupTyExact iname (tt_ctxt ist) of

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

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

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

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

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

133139

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

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

136− let t_in = substMatchesShadow ips pnames t

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

137143 mnamemap =

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

139145 (map (toImp fc) headVars)))

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

142148 (decorate ns iname n,

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

144150 (interface_methods ci)

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

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

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

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

148154 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

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

209215

210216 where

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

218+

211219 intImpl = case ps of

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

213221 _ -> False

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

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

6262 -> SyntaxInfo

6363 -> Docstring (Either Err PTerm)

6464 -> FC

65− -> [(Name, PTerm)]

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

6666 -> Name

6767 -> FC

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

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

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

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

7171 -> [PDecl] -- ^ interface body

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

7474 -> Idris ()

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

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

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

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

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

8079

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

8281 syn_in { using = addToUsing (using syn_in)

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

8483 }

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

8598

8699 -- build data declaration

87100 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

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

96109

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

98− ims <- mapM (tdecl mnames) mdecls

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

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

100113 (filter clause ds)

101114 let (methods, imethods)

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

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

104117

105118 -- 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

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

108121 constraint

109122

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

111124 let ddecl = PDatadecl tn NoFC tty cons

112125

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

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

114127

115128 -- Elaborate the data declaration

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

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

118131 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)

120136

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

122138 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

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

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

190206

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

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

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

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

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

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

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

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

197213 (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))

199215 = do let o = []

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

201217 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

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

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

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

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

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

207223 = 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")

209225

210226 -- Create default definitions

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

src/Idris/IBC.hs+6−4

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

4747import System.FilePath

4848

4949ibcVersion :: Word16

50−ibcVersion = 149

50+ibcVersion = 150

5151

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

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

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

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

552552 -- could have loaded in any order

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

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

554+ Just ci -> interface_implementations ci

555555 _ -> []

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

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

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

23542354

23552355

23562356instance Binary InterfaceInfo where

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

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

23582358 = do put x1

23592359 put x2

23602360 put x3

23612361 put x4

23622362 put x5

23632363 put x6

2364+ put x7

23642365 get

23652366 = do x1 <- get

23662367 x2 <- get

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

23682369 x4 <- get

23692370 x5 <- get

23702371 x6 <- get

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

2372+ x7 <- get

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

23722374

23732375instance Binary RecordInfo where

23742376 put (RI x1 x2 x3)

src/Idris/ProofSearch.hs+2−2

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

525525findImplementations ist t

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

527527 = case lookupCtxt n (idris_interfaces ist) of

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

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

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

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

530530 _ -> []

531531 | otherwise = []

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