c271f58 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Support interfaces in mutual blocks

c271f58Edwin Brady10 years ago

docs/tutorial/interfaces.rst+10

compare with master

unifiedsplit

@@ -153,6 +153,16 @@ separated list, for example:

153 sortAndShow : (Ord a, Show a) => List a -> String

154 sortAndShow xs = show (sort xs)

155

156+Note: Interfaces and ``mutual`` blocks

157+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

158+

159+Idris is strictly "define before use", except in ``mutual`` blocks.

160+In a ``mutual`` block, Idris elaborates in two passes: types on the first

161+pass and definitions on the second. When the mutual block contains an

162+interface declaration, it elaborates the interface header but none of the

163+method types on the first pass, and elaborates the method types and any

164+default definitions on the second pass.

165+

156Functors and Applicatives

166Functors and Applicatives

157=========================

167=========================

158

168

src/Idris/Elab/Interface.hs+94−89

@@ -61,6 +61,7 @@ data MArgTy = IA Name | EA Name | CA deriving Show

61elabInterface :: ElabInfo

62 -> SyntaxInfo

63 -> Docstring (Either Err PTerm)

64+ -> ElabWhat

64 -> FC

65 -> FC

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

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

66 -> Name

67 -> Name

@@ -72,7 +73,7 @@ elabInterface :: ElabInfo

72 -> Maybe (Name, FC) -- ^ implementation ctor name and location

73 -> Maybe (Name, FC) -- ^ implementation ctor name and location

73 -> Docstring (Either Err PTerm) -- ^ implementation ctor docs

74 -> Docstring (Either Err PTerm) -- ^ implementation ctor docs

74 -> Idris ()

75 -> Idris ()

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

76+elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn cd

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

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

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

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

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

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

@@ -109,94 +110,98 @@ elabInterface info_in syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

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

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

110

111

111 let pre_ddecl = PLaterdecl tn NoFC tty

112 let pre_ddecl = PLaterdecl tn NoFC tty

112− -- Elaborate the interface header

113+ -- Elaborate the interface header, as long as we haven't done it

114+ -- in an earlier pass

115+ when (what /= EDefns) $

113− elabData info (syn { no_imp = no_imp syn ++ mnames,

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

114− imp_methods = mnames }) doc pDocs fc [] pre_ddecl

117+ imp_methods = mnames }) doc pDocs fc [] pre_ddecl

118+ -- Continue only if we're not in the first pass of a mutual block

119+ when (what /= ETypes) $ do

115− dets <- findDets tn (map fst fds)

120+ dets <- findDets tn (map fst fds)

116−

121+

117− logElab 3 $ "Building methods " ++ show fullmnames

122+ logElab 3 $ "Building methods " ++ show fullmnames

118− ims <- mapM (tdecl impps mnames) mdecls

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

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

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

120− (filter clause ds)

125+ (filter clause ds)

121− let (methods, imethods)

126+ let (methods, imethods)

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

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

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

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

124−

129+

125− addInterface tn (CI cn (map nodoc imethods) defaults idecls

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

126− (map (\(n, _, _) -> n) impps)

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

127− (map (\(n, _, _) -> n) ps)

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

128− (map snd constraints)

133+ (map snd constraints)

129− [] dets)

134+ [] dets)

130−

135+

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

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

132− -- elaborate types now, bodies later (after we've done the constructor

137+ -- elaborate types now, bodies later (after we've done the constructor

133− -- of the interface)

138+ -- of the interface)

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

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

135− let (cfnTyDecls, cfnDefs) = unzip cfns

140+ let (cfnTyDecls, cfnDefs) = unzip cfns

136− mapM_ (rec_elabDecl info EAll info) cfnTyDecls

141+ mapM_ (rec_elabDecl info EAll info) cfnTyDecls

137−

142+

138− -- for each method, build a top level function

143+ -- for each method, build a top level function

139− -- 'tfun' builds appropriate implicits for the constructor

144+ -- 'tfun' builds appropriate implicits for the constructor

140− -- declaration

145+ -- declaration

141− fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })

146+ fns <- mapM (tfun cn constraint (syn { imp_methods = mnames }) -- mnames })

142− (map fst imethods)) imethods

147+ (map fst imethods)) imethods

143− let (fnTyDecls, fnDefs) = unzip fns

148+ let (fnTyDecls, fnDefs) = unzip fns

144− mapM_ (rec_elabDecl info EAll info) fnTyDecls

149+ mapM_ (rec_elabDecl info EAll info) fnTyDecls

145−

150+

146− elabMethTys <- mapM getElabMethTy fullmnames

151+ elabMethTys <- mapM getElabMethTy fullmnames

147−

152+

148− logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)

153+ logElab 3 $ "Method types:\n" ++ showSep "\n" (map showTmImpls elabMethTys)

149−

154+

150− let cpos = map (\ (n, ty) -> (n, findConstraint ty))

155+ let cpos = map (\ (n, ty) -> (n, findConstraint ty))

151− (zip fullmnames elabMethTys)

156+ (zip fullmnames elabMethTys)

152− logElab 5 $ "Constraint pos: " ++ show cpos

157+ logElab 5 $ "Constraint pos: " ++ show cpos

153−

158+

154− -- Method types to store in the IState, taken from the elaborated

159+ -- Method types to store in the IState, taken from the elaborated

155− -- types with the parameter removed

160+ -- types with the parameter removed

156− let storemeths = map (mkMethTy True cpos) (zip fullmnames elabMethTys)

161+ let storemeths = map (mkMethTy True cpos) (zip fullmnames elabMethTys)

157− updateIMethods tn storemeths

162+ updateIMethods tn storemeths

158−

163+

159− -- build implementation constructor type

164+ -- build implementation constructor type

160− let cty = impbind [(pn, pt) | (pn, _, pt) <- impps ++ ps] $

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

161− conbind constraints $

166+ conbind constraints $

162− pibind (map (mkMethTy False cpos) (zip fullmnames elabMethTys))

167+ pibind (map (mkMethTy False cpos) (zip fullmnames elabMethTys))

163− constraint

168+ constraint

164− logElab 3 $ "Constraint constructor type: " ++ showTmImpls cty

169+ logElab 3 $ "Constraint constructor type: " ++ showTmImpls cty

165−

170+

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

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

167− let ddecl = PDatadecl tn NoFC tty cons

172+ let ddecl = PDatadecl tn NoFC tty cons

168−

173+

169− logElab 10 $ "Interface " ++ show (showDImp verbosePPOption ddecl)

174+ logElab 10 $ "Interface " ++ show (showDImp verbosePPOption ddecl)

170−

175+

171−

176+

172− -- Elaborate the data declaration

177+ -- Elaborate the data declaration

173− elabData info (syn { no_imp = no_imp syn ++ mnames,

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

174− imp_methods = [] }) doc pDocs fc [] ddecl

179+ imp_methods = [] }) doc pDocs fc [] ddecl

175−

180+

176−

181+

177− logElab 5 $ "Function types " ++ show fnTyDecls

182+ logElab 5 $ "Function types " ++ show fnTyDecls

178− logElab 5 $ "Method types now: " ++ show imethods

183+ logElab 5 $ "Method types now: " ++ show imethods

179−

184+

180− -- Elaborate the the top level constraint chasers

185+ -- Elaborate the the top level constraint chasers

181− -- (Types elaborated earlier)

186+ -- (Types elaborated earlier)

182− mapM_ (rec_elabDecl info EAll info) cfnDefs

187+ mapM_ (rec_elabDecl info EAll info) cfnDefs

183− -- Elaborate the the top level method bodies

188+ -- Elaborate the the top level method bodies

184− mapM_ (rec_elabDecl info EAll info) fnDefs

189+ mapM_ (rec_elabDecl info EAll info) fnDefs

185−

190+

186− -- Flag all the top level data declarations as injective

191+ -- Flag all the top level data declarations as injective

187− mapM_ (\n -> do setInjectivity n True

192+ mapM_ (\n -> do setInjectivity n True

188− addIBC (IBCInjective n True))

193+ addIBC (IBCInjective n True))

189− (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))

194+ (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))

190−

195+

191− -- add the default definitions

196+ -- add the default definitions

192− mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)

197+ mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)

193− addIBC (IBCInterface tn)

198+ addIBC (IBCInterface tn)

194−

199+

195− sendHighlighting $

200+ sendHighlighting $

196− [(tnfc, AnnName tn Nothing Nothing Nothing)] ++

201+ [(tnfc, AnnName tn Nothing Nothing Nothing)] ++

197− [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

202+ [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

198− [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

203+ [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

199− maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

204+ maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

200

205

201 where

206 where

202 info = info_in { noCaseLift = tn : noCaseLift info_in }

207 info = info_in { noCaseLift = tn : noCaseLift info_in }

src/Idris/ElabDecls.hs+1−2

@@ -291,9 +291,8 @@ elabDecl' what info (PNamespace n nfc ps) =

291 ninfo = info { namespace = newNS }

292

293elabDecl' what info (PInterface doc s f cs n nfc ps pdocs fds ds cn cd)

294− | what /= EDefns

295 = do logElab 1 $ "Elaborating interface " ++ show n

294 = do logElab 1 $ "Elaborating interface " ++ show n

296− elabInterface info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd

295+ elabInterface info (s { syn_params = [] }) doc what f cs n nfc ps pdocs fds ds cn cd

297elabDecl' what info (PImplementation doc argDocs s f cs pnames acc fnopts n nfc ps pextra t expn ds)

296elabDecl' what info (PImplementation doc argDocs s f cs pnames acc fnopts n nfc ps pextra t expn ds)

298 = do logElab 1 $ "Elaborating implementation " ++ show n

297 = do logElab 1 $ "Elaborating implementation " ++ show n

299 elabImplementation info s doc argDocs what f cs pnames acc fnopts n nfc ps pextra t expn ds

298 elabImplementation info s doc argDocs what f cs pnames acc fnopts n nfc ps pextra t expn ds

test/dsl001/run+2−2

@@ -1,5 +1,5 @@

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ test001.idr -o test001

2+${IDRIS:-idris} $@ test001.idr -o test001 --partial-eval

3./test001

4−${IDRIS:-idris} $@ test001.idr --quiet --port none < input

4+${IDRIS:-idris} $@ test001.idr --partial-eval --quiet --port none < input

5rm -f test001 test001.ibc

test/regression001/reg002.idrnew file+8

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

1+mutual

2+ interface MyInterface a where

3+ foo : a -> b

4+ foo = bar

6+ bar : MyInterface a => a -> b

7+ bar = ?bar_rhs

test/regression001/run+1−1

@@ -1,6 +1,6 @@

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ --check \

3− reg001.idr reg036.idr reg037.idr reg038.idr reg046.idr \

3+ reg001.idr reg002.idr reg036.idr reg037.idr reg038.idr reg046.idr \

4 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \

5 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \

6 reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \