c271f58 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Support interfaces in mutual blocks

First pass: Elaborate the interface type only Second pass: Elaborate the method types and default definitions Since elaborating the method types involves creating a data declaration, we save this for the second pass, but at least you can use the existence of the interface in later types in the mutual block. Fixes #3168

commitc271f587a09ef88e3e55c47fd3a7a0afa9a4a923 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 5 Mar 2017, 13:27 (10 years ago) parentf40d2f9

6 files changed+116−94

compare with master

unifiedsplit

docs/tutorial/interfaces.rst+10 src/Idris/Elab/Interface.hs+94−89 src/Idris/ElabDecls.hs+1−2 test/dsl001/run+2−2 test/regression001/reg002.idr+8 test/regression001/run+1−1

docs/tutorial/interfaces.rst+10

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

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

154154 sortAndShow xs = show (sort xs)

155155

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+

156166Functors and Applicatives

157167=========================

158168

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

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

6161elabInterface :: ElabInfo

6262 -> SyntaxInfo

6363 -> Docstring (Either Err PTerm)

64+ -> ElabWhat

6465 -> FC

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

6667 -> Name

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

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

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

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

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

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

7879 (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

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

110111

111112 let pre_ddecl = PLaterdecl tn NoFC tty

112− -- Elaborate the interface header

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

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

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

116−

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

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

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

120− (filter clause ds)

121− let (methods, imethods)

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

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

124−

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

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

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

128− (map snd constraints)

129− [] dets)

130−

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

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

133− -- of the interface)

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

135− let (cfnTyDecls, cfnDefs) = unzip cfns

136− mapM_ (rec_elabDecl info EAll info) cfnTyDecls

137−

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

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

140− -- declaration

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

142− (map fst imethods)) imethods

143− let (fnTyDecls, fnDefs) = unzip fns

144− mapM_ (rec_elabDecl info EAll info) fnTyDecls

145−

146− elabMethTys <- mapM getElabMethTy fullmnames

147−

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

149−

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

151− (zip fullmnames elabMethTys)

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

153−

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

155− -- types with the parameter removed

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

157− updateIMethods tn storemeths

158−

159− -- build implementation constructor type

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

161− conbind constraints $

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

163− constraint

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

165−

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

167− let ddecl = PDatadecl tn NoFC tty cons

168−

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

170−

171−

172− -- Elaborate the data declaration

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

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

175−

176−

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

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

179−

180− -- Elaborate the the top level constraint chasers

181− -- (Types elaborated earlier)

182− mapM_ (rec_elabDecl info EAll info) cfnDefs

183− -- Elaborate the the top level method bodies

184− mapM_ (rec_elabDecl info EAll info) fnDefs

185−

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

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

188− addIBC (IBCInjective n True))

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

190−

191− -- add the default definitions

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

193− addIBC (IBCInterface tn)

194−

195− sendHighlighting $

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

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

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

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

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

114+ -- in an earlier pass

115+ when (what /= EDefns) $

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

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

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

121+

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

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

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

125+ (filter clause ds)

126+ let (methods, imethods)

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

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

129+

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

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

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

133+ (map snd constraints)

134+ [] dets)

135+

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

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

138+ -- of the interface)

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

140+ let (cfnTyDecls, cfnDefs) = unzip cfns

141+ mapM_ (rec_elabDecl info EAll info) cfnTyDecls

142+

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

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

145+ -- declaration

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

147+ (map fst imethods)) imethods

148+ let (fnTyDecls, fnDefs) = unzip fns

149+ mapM_ (rec_elabDecl info EAll info) fnTyDecls

150+

151+ elabMethTys <- mapM getElabMethTy fullmnames

152+

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

154+

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

156+ (zip fullmnames elabMethTys)

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

158+

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

160+ -- types with the parameter removed

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

162+ updateIMethods tn storemeths

163+

164+ -- build implementation constructor type

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

166+ conbind constraints $

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

168+ constraint

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

170+

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

172+ let ddecl = PDatadecl tn NoFC tty cons

173+

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

175+

176+

177+ -- Elaborate the data declaration

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

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

180+

181+

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

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

184+

185+ -- Elaborate the the top level constraint chasers

186+ -- (Types elaborated earlier)

187+ mapM_ (rec_elabDecl info EAll info) cfnDefs

188+ -- Elaborate the the top level method bodies

189+ mapM_ (rec_elabDecl info EAll info) fnDefs

190+

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

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

193+ addIBC (IBCInjective n True))

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

195+

196+ -- add the default definitions

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

198+ addIBC (IBCInterface tn)

199+

200+ sendHighlighting $

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

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

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

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

200205

201206 where

202207 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) =

291291 ninfo = info { namespace = newNS }

292292

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

294− | what /= EDefns

295294 = 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

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

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

299298 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 @@

11#!/usr/bin/env bash

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

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

33./test001

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

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

55rm -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 @@

11#!/usr/bin/env bash

22${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 \

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

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

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