88faa10 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Reorganise interface elaboration

88faa10Edwin Brady10 years ago

src/Idris/AbsSyntax.hs+12−4

compare with master

unifiedsplit

@@ -502,9 +502,10 @@ addInterface :: Name -> InterfaceInfo -> Idris ()

502addInterface n i

503 = do ist <- getIState

504 let i' = case lookupCtxt n (idris_interfaces ist) of

505− [c] -> c { interface_implementations = interface_implementations i }

505+ [c] -> i { interface_implementations = interface_implementations c ++

506+ interface_implementations i }

506 _ -> i

507 _ -> i

507− putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }

508+ putIState $ ist { idris_interfaces = addDef n i (idris_interfaces ist) }

508

509

509addRecord :: Name -> RecordInfo -> Idris ()

510addRecord :: Name -> RecordInfo -> Idris ()

510addRecord n ri = do ist <- getIState

511addRecord n ri = do ist <- getIState

@@ -1927,7 +1928,8 @@ addImpl' inpat env infns imp_meths ist ptm

1927 ai inpat qq env ds (PPi p n nfc ty sc)

1928 ai inpat qq env ds (PPi p n nfc ty sc)

1928 = let ty' = ai inpat qq env ds ty

1929 = let ty' = ai inpat qq env ds ty

1929 env' = if n `elem` imp_meths then env

1930 env' = if n `elem` imp_meths then env

1931+ else

1930− else ((n, Just ty) : env)

1932+ ((n, Just ty) : env)

1931 sc' = ai inpat qq env' ds sc in

1933 sc' = ai inpat qq env' ds sc in

1932 PPi p n nfc ty' sc'

1934 PPi p n nfc ty' sc'

1933 ai inpat qq env ds (PGoal fc r n sc)

1935 ai inpat qq env ds (PGoal fc r n sc)

@@ -2168,8 +2170,12 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

2168 -- check will not necessarily fully resolve constructor names,

2170 -- check will not necessarily fully resolve constructor names,

2169 -- and these bare names will otherwise get in the way of

2171 -- and these bare names will otherwise get in the way of

2170 -- impossbility checking.

2172 -- impossbility checking.

2173+ | -- Just fn <- getFn f,

2171− | canBeDConName fn ctxt

2174+ canBeDConName fn ctxt

2172 = PApp fc f (fmap (fmap su) args)

2175 = PApp fc f (fmap (fmap su) args)

2176+ where getFn (PRef _ _ fn) = Just fn

2177+ getFn (PApp _ f args) = getFn f

2178+ getFn _ = Nothing

2173 su (PApp fc f args)

2179 su (PApp fc f args)

2174 = PHidden (PApp fc f args)

2180 = PHidden (PApp fc f args)

2175 su (PAlternative ms b alts)

2181 su (PAlternative ms b alts)

@@ -2379,6 +2385,8 @@ substMatchesShadow nmap shs t = sm shs t where

2379 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))

2385 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))

2380 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))

2386 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))

2381 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)

2387 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)

2388+ sm xs (PLet fc x xfc val t sc)

2389+ = PLet fc x xfc (sm xs val) (sm xs t) (sm xs sc)

2382 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

2390 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

2383 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

2391 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

2384 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

2392 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

src/Idris/Elab/Interface.hs+50−23

@@ -106,6 +106,12 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

106 concatMap (namesIn [] ist) (map snd constraints)

107

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

109+

110+ let pre_ddecl = PLaterdecl tn NoFC tty

111+ -- Elaborate the interface header

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

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

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

109

115

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

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

111 ims <- mapM (tdecl impps mnames) mdecls

117 ims <- mapM (tdecl impps mnames) mdecls

@@ -114,7 +120,20 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

114 let (methods, imethods)

120 let (methods, imethods)

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

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

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

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

117−

123+

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

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

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

127+ (map snd constraints)

128+ [] dets)

129+

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

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

132+ -- of the interface)

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

134+ let (cfnTyDecls, cfnDefs) = unzip cfns

135+ mapM_ (rec_elabDecl info EAll info) cfnTyDecls

136+

118 -- build implementation constructor type

137 -- build implementation constructor type

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

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

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

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

@@ -125,26 +144,27 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

125

144

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

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

127

146

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

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

149+ -- declaration

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

151+ (map fst imethods)) imethods

152+ let (fnTyDecls, fnDefs) = unzip fns

153+

128 -- Elaborate the data declaration

154 -- Elaborate the data declaration

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

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

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

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

131− dets <- findDets cn (map fst fds)

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

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

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

135− (map snd constraints)

136− [] dets)

137

157

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

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

140− mapM_ (rec_elabDecl info EAll info) (concat cfns)

158+ mapM_ (rec_elabDecl info EAll info) fnTyDecls

141

159

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

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

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

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

144− (map fst imethods)) imethods

162+

145− logElab 5 $ "Functions " ++ show fns

163+ -- Elaborate the the top level constraint chasers

146− -- Elaborate the the top level methods

164+ -- (Types elaborated earlier)

165+ mapM_ (rec_elabDecl info EAll info) cfnDefs

166+ -- Elaborate the the top level method bodies

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

167+ mapM_ (rec_elabDecl info EAll info) fnDefs

148

168

149 -- Flag all the top level data declarations as injective

169 -- Flag all the top level data declarations as injective

150 mapM_ (\n -> do setInjectivity n True

170 mapM_ (\n -> do setInjectivity n True

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

207

227

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

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

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

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

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

230+ logElab 1 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

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

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

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

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

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

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

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

249 clause _ = False

269 clause _ = False

250

270

251 -- Generate a function for chasing a dictionary constraint

271 -- Generate a function for chasing a dictionary constraint

252− cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> (Name, PTerm) -> Idris [PDecl' PTerm]

272+ cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> (Name, PTerm) -> Idris (PDecl, PDecl)

253 cfun cn c syn all (cnm, con)

273 cfun cn c syn all (cnm, con)

254 = do let cfn = SN (ParentN cn (txt (show con)))

274 = do let cfn = SN (ParentN cn (txt (show con)))

255 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

275 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

@@ -269,8 +289,8 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

269 addImplementation False True conn' cfn

289 addImplementation False True conn' cfn

270 addIBC (IBCImplementation False True conn' cfn)

290 addIBC (IBCImplementation False True conn' cfn)

271-- iputStrLn ("Added " ++ show (conn, cfn, ty))

291-- iputStrLn ("Added " ++ show (conn, cfn, ty))

272− return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

292+ return (PTy emptyDocstring [] syn fc [] cfn NoFC ty,

273− PClauses fc [Inlinable, Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

293+ PClauses fc [Inlinable, Dictionary] cfn [PClause fc cfn lhs [] rhs []])

274

294

275 -- | Generate a top level function which looks up a method in a given

295 -- | Generate a top level function which looks up a method in a given

276 -- dictionary (this is inlinable, always)

296 -- dictionary (this is inlinable, always)

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

279 -> SyntaxInfo -> [Name] -- ^ All the method names

299 -> SyntaxInfo -> [Name] -- ^ All the method names

280 -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))

300 -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))

281 -- ^ The present declaration

301 -- ^ The present declaration

282− -> Idris [PDecl]

302+ -> Idris (PDecl, PDecl)

283 tfun cn c syn all (m, (isdata, mfc, doc, o, ty))

303 tfun cn c syn all (m, (isdata, mfc, doc, o, ty))

284 = do let ty' = expandMethNS syn (insertConstraint c all ty)

304 = do let ty' = expandMethNS syn (insertConstraint c all ty)

285 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

305 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

@@ -291,8 +311,15 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

291 logElab 2 ("Top level type: " ++ showTmImpls ty')

311 logElab 2 ("Top level type: " ++ showTmImpls ty')

292 logElab 1 (show (m, ty', capp, margs))

312 logElab 1 (show (m, ty', capp, margs))

293 logElab 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)

313 logElab 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)

294− return [PTy doc [] syn fc o m mfc ty',

314+ return (PTy doc [] syn fc o m mfc ty',

295− PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

315+ PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])

316+

317+ updateIMethod :: [(Name, PTerm)] ->

318+ (Name, (a, b, c, d, PTerm)) ->

319+ (Name, (a, b, c, d, PTerm))

320+ updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))

321+ | Just ty' <- lookup (nsroot n) ns = (n, (isf, mfc, doc, o, ty'))

322+ | otherwise = tm

296

323

297 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

324 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

298 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc

325 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc

src/Idris/Elab/Term.hs+5−1

@@ -1097,7 +1097,7 @@ elab ist info emode opts fn tm

1097 ptm <- get_term

1098 let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

1099

1100− let argsDropped = filter (isUnique envU)

1100+ let argsDropped = filter (\t -> isUnique envU t || isConstraint args t)

1101 (nub $ allNamesIn scr ++ inApp ptm ++

1102 inOpts)

1103

@@ -1168,6 +1168,10 @@ elab ist info emode opts fn tm

1168 _ -> False

1169 tcName _ = False

1170

1171+ isConstraint env n = case lookupBinder n env of

1172+ Just ty -> False -- tcName (binderTy ty)

1173+ _ -> False

1174+

1171 usedIn ns (n, b)

1175 usedIn ns (n, b)

1172 = n `elem` ns

1176 = n `elem` ns

1173 || any (\x -> x `elem` ns) (allTTNames (binderTy b))

1177 || any (\x -> x `elem` ns) (allTTNames (binderTy b))

test/interfaces002/interfaces002.idr+1−4

@@ -1,10 +1,9 @@

1import Data.Vect

3%default total

4−

5interface ArrayM where

6 Array : (n : Nat) -> (a : Type) -> Type

7−

8 create : (n : Nat) -> a -> Array n a

7 create : (n : Nat) -> a -> Array n a

10 lkp : (i : Nat) -> (prf : LTE (S i) n) -> Array n a -> a

9 lkp : (i : Nat) -> (prf : LTE (S i) n) -> Array n a -> a

@@ -37,5 +36,3 @@ testSum = sumArray

38main : IO ()

37main : IO ()

39main = printLn (testSum (upd 11 1 (LTESucc (LTESucc LTEZero)) (create 4 10)))

38main = printLn (testSum (upd 11 1 (LTESucc (LTESucc LTEZero)) (create 4 10)))

40−

41−