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

git.iko.soy/Idris-dev

Reorganise interface elaboration

Check the interface type, constraint chaser type, then method types before checking bodies, because this will make some imminent changes easier and cleaner.

commit88faa102a923d31f1be2cb6d1b2d9d7739b79453 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 23 Jan 2017, 23:44 (10 years ago) parentdc3d53f

4 files changed+68−32

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+12−4 src/Idris/Elab/Interface.hs+50−23 src/Idris/Elab/Term.hs+5−1 test/interfaces002/interfaces002.idr+1−4

src/Idris/AbsSyntax.hs+12−4

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

502502addInterface n i

503503 = do ist <- getIState

504504 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 }

506507 _ -> i

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

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

508509

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

510511addRecord n ri = do ist <- getIState

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

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

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

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

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

1931+ else

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

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

19321934 PPi p n nfc ty' sc'

19331935 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

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

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

21702172 -- impossbility checking.

2171− | canBeDConName fn ctxt

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

2174+ canBeDConName fn ctxt

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

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

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

2178+ getFn _ = Nothing

21732179 su (PApp fc f args)

21742180 = PHidden (PApp fc f args)

21752181 su (PAlternative ms b alts)

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

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

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

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

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

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

23842392 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

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

107107

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

109115

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

111117 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

114120 let (methods, imethods)

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

116122 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+

118137 -- build implementation constructor type

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

120139 $ 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

125144

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

127146

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+

128154 -- Elaborate the data declaration

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

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

137157

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

141159

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

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

144− (map fst imethods)) imethods

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

146− -- Elaborate the the top level methods

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

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

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

162+

163+ -- Elaborate the the top level constraint chasers

164+ -- (Types elaborated earlier)

165+ mapM_ (rec_elabDecl info EAll info) cfnDefs

166+ -- Elaborate the the top level method bodies

167+ mapM_ (rec_elabDecl info EAll info) fnDefs

148168

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

150170 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

207227

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

209229 = 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'

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

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

213233 (\ 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

249269 clause _ = False

250270

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

253273 cfun cn c syn all (cnm, con)

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

255275 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

269289 addImplementation False True conn' cfn

270290 addIBC (IBCImplementation False True conn' cfn)

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

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

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

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

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

274294

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

276296 -- dictionary (this is inlinable, always)

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

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

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

281301 -- ^ The present declaration

282− -> Idris [PDecl]

302+ -> Idris (PDecl, PDecl)

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

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

285305 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

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

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

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

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

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

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

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

296323

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

298325 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

10971097 ptm <- get_term

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

10991099

1100− let argsDropped = filter (isUnique envU)

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

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

11021102 inOpts)

11031103

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

11681168 _ -> False

11691169 tcName _ = False

11701170

1171+ isConstraint env n = case lookupBinder n env of

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

1173+ _ -> False

1174+

11711175 usedIn ns (n, b)

11721176 = n `elem` ns

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

test/interfaces002/interfaces002.idr+1−4

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

11import Data.Vect

33%default total

4−

55interface ArrayM where

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

7−

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

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

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

3736

3837main : IO ()

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

40−

41−