03f6913 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Partially evaluate type class dictionaries

03f6913Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+22−6

compare with master

unifiedsplit

@@ -1059,12 +1059,14 @@ addStatics :: Name -> Term -> PTerm -> Idris ()

1059addStatics n tm ptm =

1060 do let (statics, dynamics) = initStatics tm ptm

1061 ist <- getIState

1062+ let paramnames

1062− let paramnames = case lookupCtxtExact n (idris_fninfo ist) of

1063+ = nub $ case lookupCtxtExact n (idris_fninfo ist) of

1063− Just p -> getNamesFrom 0 (fn_params p) tm

1064+ Just p -> getNamesFrom 0 (fn_params p) tm ++

1064− _ -> []

1065+ concatMap (getParamNames ist) (map snd statics)

1066+ _ -> concatMap (getParamNames ist) (map snd statics)

1065

1067

1066 let stnames = nub $ concatMap freeArgNames (map snd statics)

1068 let stnames = nub $ concatMap freeArgNames (map snd statics)

1067− let dnames = nub $ concatMap freeArgNames (map snd dynamics)

1069+ let dnames = (nub $ concatMap freeArgNames (map snd dynamics))

1068 \\ paramnames

1070 \\ paramnames

1069 -- also get the arguments which are 'uniquely inferrable' from

1071 -- also get the arguments which are 'uniquely inferrable' from

1070 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")

1072 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")

@@ -1074,8 +1076,10 @@ addStatics n tm ptm =

1074 let stpos = staticList statics' tm

1076 let stpos = staticList statics' tm

1075 i <- getIState

1077 i <- getIState

1076 when (not (null statics)) $

1078 when (not (null statics)) $

1077− logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ " "

1079+ logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"

1080+ ++ showTmImpls ptm ++ "\n"

1078− ++ show statics' ++ "\n" ++ show dynamics

1081+ ++ show statics ++ "\n" ++ show dynamics

1082+ ++ "\n" ++ show paramnames

1079 ++ "\n" ++ show stpos

1083 ++ "\n" ++ show stpos

1080 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

1084 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

1081 addIBC (IBCStatic n)

1085 addIBC (IBCStatic n)

@@ -1091,6 +1095,18 @@ addStatics n tm ptm =

1091 else (static, dynamic)

1095 else (static, dynamic)

1092 initStatics t pt = ([], [])

1096 initStatics t pt = ([], [])

1093

1097

1098+ getParamNames ist tm | (P _ n _ , args) <- unApply tm

1099+ = case lookupCtxtExact n (idris_datatypes ist) of

1100+ Just ti -> getNamePos 0 (param_pos ti) args

1101+ Nothing -> []

1102+ where getNamePos i ps [] = []

1103+ getNamePos i ps (P _ n _ : as)

1104+ | i `elem` ps = n : getNamePos (i + 1) ps as

1105+ getNamePos i ps (_ : as) = getNamePos (i + 1) ps as

1106+ getParamNames ist (Bind t (Pi (P _ n _) _) sc)

1107+ = n : getParamNames ist sc

1108+ getParamNames ist _ = []

1109+

1094 getNamesFrom i ps (Bind n (Pi _ _) sc)

1110 getNamesFrom i ps (Bind n (Pi _ _) sc)

1095 | i `elem` ps = n : getNamesFrom (i + 1) ps sc

1111 | i `elem` ps = n : getNamesFrom (i + 1) ps sc

1096 | otherwise = getNamesFrom (i + 1) ps sc

1112 | otherwise = getNamesFrom (i + 1) ps sc

src/Idris/AbsSyntaxTree.hs+1−1

@@ -485,7 +485,7 @@ deriving instance NFData Plicity

485impl = Imp [] Dynamic False

486expl = Exp [] Dynamic False

487expl_param = Exp [] Dynamic True

488−constraint = Constraint [] Dynamic

488+constraint = Constraint [] Static

489tacimpl t = TacImp [] Dynamic t

490

491data FnOpt = Inlinable -- always evaluate when simplifying

src/Idris/Elab/Class.hs+1−1

@@ -220,7 +220,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

220

221 insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

222 = PPi p n ty (insertConstraint c sc)

223− insertConstraint c sc = PPi (constraint) -- { pstatic = Static })

223+ insertConstraint c sc = PPi (constraint { pstatic = Static })

224 (sMN 0 "class") c sc

225

226 -- make arguments explicit and don't bind class parameters

src/Idris/Elab/Clause.hs+32−23

@@ -74,9 +74,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

74 let atys = map snd (getArgTys fty)

75 cs_elab <- mapM (elabClause info opts)

76 (zip [0..] cs)

77+ -- pats_raw is the version we'll work with at compile time:

78+ -- no simplification or PE

77 let (pats_in, cs_full) = unzip cs_elab

79 let (pats_in, cs_full) = unzip cs_elab

78−

80+ let pats_raw = map (simple_lhs (tt_ctxt ist)) pats_in

79− logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

81+ logLvl 3 $ "Elaborated patterns:\n" ++ show pats_raw

81 solveDeferred n

83 solveDeferred n

@@ -94,7 +96,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

94 -- If the definition is specialisable, this reduces the

96 -- If the definition is specialisable, this reduces the

95 -- RHS

97 -- RHS

96 pe_tm <- doPartialEval ist tpats

98 pe_tm <- doPartialEval ist tpats

97− let pats = map (simple_lhs (tt_ctxt ist)) pe_tm

99+ let pats_pe = map (simple_lhs (tt_ctxt ist)) pe_tm

100

99 let tcase = opt_typecase (idris_options ist)

101 let tcase = opt_typecase (idris_options ist)

100

102

@@ -103,13 +105,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

103 -- for partially evaluated definitions

105 -- for partially evaluated definitions

104 newrules <- mapM (\ e -> case e of

106 newrules <- mapM (\ e -> case e of

105 Left _ -> return []

107 Left _ -> return []

106− Right (l, r) -> elabPE info fc n r) pats

108+ Right (l, r) -> elabPE info fc n r) pats_pe

107

109

108 -- Redo transforms with the newly generated transformations, so

110 -- Redo transforms with the newly generated transformations, so

109 -- that the specialised application we've just made gets

111 -- that the specialised application we've just made gets

110 -- used in place of the general one

112 -- used in place of the general one

111 ist <- getIState

113 ist <- getIState

112− let pats_transformed = transformPats ist pats

114+ let pats_transformed = transformPats ist pats_pe

113

115

114 -- Summary of what's about to happen: Definitions go:

116 -- Summary of what's about to happen: Definitions go:

115 --

117 --

@@ -118,11 +120,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

118 -- addCaseDef builds case trees from <pdef> and <pdef'>

120 -- addCaseDef builds case trees from <pdef> and <pdef'>

119

121

120 -- pdef is the compile-time pattern definition.

122 -- pdef is the compile-time pattern definition.

121− -- This will get further optimised for run-time, and, separately,

122− -- further inlined to help with totality checking.

123+ -- This will get further inlined to help with totality checking.

123− let pdef = map debind pats_transformed

124+ let pdef = map debind pats_raw

125+ -- pdef_pe is the one which will get further optimised

126+ -- for run-time, and, partially evaluated

127+ let pdef_pe = map debind pats_transformed

124

128

125− logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats

129+ logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats_raw

126 logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef

130 logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef

127

131

128 -- NOTE: Need to store original definition so that proofs which

132 -- NOTE: Need to store original definition so that proofs which

@@ -137,13 +141,13 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

137

141

138 case specNames opts of

142 case specNames opts of

139 Just _ ->

143 Just _ ->

140− do logLvl 2 $ "Partially evaluated:\n" ++ show pats

144+ do logLvl 2 $ "Partially evaluated:\n" ++ show pats_pe

141 logLvl 2 $ "Transformed:\n" ++ show pats_transformed

145 logLvl 2 $ "Transformed:\n" ++ show pats_transformed

142 _ -> return ()

146 _ -> return ()

143

147

144 erInfo <- getErasureInfo <$> getIState

148 erInfo <- getErasureInfo <$> getIState

145 tree@(CaseDef scargs sc _) <- tclift $

149 tree@(CaseDef scargs sc _) <- tclift $

146− simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo

150+ simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo

147 cov <- coverage

151 cov <- coverage

148 pmissing <-

152 pmissing <-

149 if cov && not (hasDefault cs)

153 if cov && not (hasDefault cs)

@@ -164,8 +168,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

164 else return []

168 else return []

165 let pcover = null pmissing

169 let pcover = null pmissing

166

170

167− -- pdef' is the version that gets compiled for run-time

171+ -- pdef' is the version that gets compiled for run-time,

172+ -- so we start from the partially evaluated version

168− pdef_in' <- applyOpts pdef

173+ pdef_in' <- applyOpts pdef_pe

169 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

174 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

170

175

171 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

176 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

@@ -197,7 +202,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

197 ctxt <- getContext

202 ctxt <- getContext

198 ist <- getIState

203 ist <- getIState

199 let opt = idris_optimisation ist

204 let opt = idris_optimisation ist

200− putIState (ist { idris_patdefs = addDef n (force pdef, force pmissing)

205+ putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

201 (idris_patdefs ist) })

206 (idris_patdefs ist) })

202 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

207 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

203 case lookupTy n ctxt of

208 case lookupTy n ctxt of

@@ -207,8 +212,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

207 (AssertTotal `elem` opts)

212 (AssertTotal `elem` opts)

208 atys

213 atys

209 inacc

214 inacc

210− pats

215+ pats_pe

216+ pdef

217+ pdef -- compile time

211− pdef pdef pdef_inl pdef' ty)

218+ pdef_inl -- inlined

219+ pdef' ty)

212 addIBC (IBCDef n)

220 addIBC (IBCDef n)

213 setTotality n tot

221 setTotality n tot

214 when (not reflect) $ do totcheck (fc, n)

222 when (not reflect) $ do totcheck (fc, n)

@@ -320,7 +328,8 @@ elabPE info fc caller r =

320 let cgns' = filter (/= n) cgns

328 let cgns' = filter (/= n) cgns

321 let opts = [Specialise (map (\x -> (x, Nothing)) cgns' ++

329 let opts = [Specialise (map (\x -> (x, Nothing)) cgns' ++

322 (n, Just 65536) :

330 (n, Just 65536) :

331+ mapMaybe (specName (pe_simple specdecl))

323− mapMaybe specName (snd specapp))]

332+ (snd specapp))]

324 logLvl 3 $ "Specialising application: " ++ show specapp

333 logLvl 3 $ "Specialising application: " ++ show specapp

325 ++ " in " ++ show caller ++

334 ++ " in " ++ show caller ++

326 " with " ++ show opts

335 " with " ++ show opts

@@ -347,14 +356,14 @@ elabPE info fc caller r =

347 -- if it doesn't work, just don't specialise. Could happen for lots

356 -- if it doesn't work, just don't specialise. Could happen for lots

348 -- of valid reasons (e.g. local variables in scope which can't be

357 -- of valid reasons (e.g. local variables in scope which can't be

349 -- lifted out).

358 -- lifted out).

350− (\e -> do logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e)

359+ (\e -> do logLvl 3 $ "Couldn't specialise: " ++ (pshow ist e)

351 return [])

360 return [])

352

361

353− specName (ImplicitS, tm)

362+ specName simpl (ImplicitS, tm)

354− | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

363+ | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

355− specName (ExplicitS, tm)

364+ specName simpl (ExplicitS, tm)

356− | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

365+ | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))

357− specName _ = Nothing

366+ specName simpl _ = Nothing

358

367

359 concreteArg ist (ImplicitS, tm) = concreteTm ist tm

368 concreteArg ist (ImplicitS, tm) = concreteTm ist tm

360 concreteArg ist (ExplicitS, tm) = concreteTm ist tm

369 concreteArg ist (ExplicitS, tm) = concreteTm ist tm

src/Idris/PartialEval.hs+8−5

@@ -2,7 +2,7 @@

3module Idris.PartialEval(partial_eval, getSpecApps, specType,

4 mkPE_TyDecl, mkPE_TermDecl, PEArgType(..),

5− pe_app, pe_def, pe_clauses) where

5+ pe_app, pe_def, pe_clauses, pe_simple) where

7import Idris.AbsSyntax

8import Idris.Delaborate

@@ -25,9 +25,12 @@ data PEArgType = ImplicitS -- ^ Implicit static argument

25-- | A partially evaluated function. pe_app captures the lhs of the

26-- new definition, pe_def captures the rhs, and pe_clauses is the

27-- specialised implementation.

28+-- pe_simple is set if the result is always reducible, because in such a

29+-- case we'll also need to reduce the static argument

28data PEDecl = PEDecl { pe_app :: PTerm, -- new application

30data PEDecl = PEDecl { pe_app :: PTerm, -- new application

29 pe_def :: PTerm, -- old application

31 pe_def :: PTerm, -- old application

30− pe_clauses :: [(PTerm, PTerm)] -- clauses of new application

32+ pe_clauses :: [(PTerm, PTerm)], -- clauses of new application

33+ pe_simple :: Bool -- if just one reducible clause

31 }

34 }

33-- | Partially evaluates given terms under the given context.

36-- | Partially evaluates given terms under the given context.

@@ -153,7 +156,7 @@ mkNewPats :: IState ->

153-- definition isn't going to block on any of the dynamic arguments

156-- definition isn't going to block on any of the dynamic arguments

154-- in this case

157-- in this case

155mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

158mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

156− = PEDecl lhs rhs [(lhs, rhs)]

159+ = PEDecl lhs rhs [(lhs, rhs)] True

157 where dynVar ap = case unApply ap of

160 where dynVar ap = case unApply ap of

158 (_, args) -> dynArgs ns args

161 (_, args) -> dynArgs ns args

159 dynArgs _ [] = True -- can definitely reduce from here

162 dynArgs _ [] = True -- can definitely reduce from here

@@ -166,7 +169,7 @@ mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)

166 dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as

169 dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as

167 dynArgs _ _ = False -- and now we'll get stuck

170 dynArgs _ _ = False -- and now we'll get stuck

168mkNewPats ist d ns newname sname lhs rhs =

171mkNewPats ist d ns newname sname lhs rhs =

169− PEDecl lhs rhs (map mkClause d)

172+ PEDecl lhs rhs (map mkClause d) False

170 where

173 where

171 mkClause :: (Term, Term) -> (PTerm, PTerm)

174 mkClause :: (Term, Term) -> (PTerm, PTerm)

172 mkClause (oldlhs, oldrhs)

175 mkClause (oldlhs, oldrhs)

@@ -215,7 +218,7 @@ mkPE_TermDecl ist newname sname ns

215 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

218 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

216 patdef = lookupCtxtExact sname (idris_patdefs ist)

219 patdef = lookupCtxtExact sname (idris_patdefs ist)

217 newpats = case patdef of

220 newpats = case patdef of

218− Nothing -> PEDecl lhs rhs [(lhs, rhs)]

221+ Nothing -> PEDecl lhs rhs [(lhs, rhs)] True

219 Just d -> mkNewPats ist (getPats d) ns

222 Just d -> mkNewPats ist (getPats d) ns

220 newname sname lhs rhs in

223 newname sname lhs rhs in

221 newpats where

224 newpats where

src/Idris/Transforms.hs+4−3

@@ -43,10 +43,11 @@ applyAll extra ts ap@(App f a)

43 | (P _ fn ty, args) <- unApply ap

44 = let rules = case lookupCtxtExact fn ts of

45 Just r -> extra ++ r

46− Nothing -> extra in

46+ Nothing -> extra

47+ ap' = App (applyAll extra ts f) (applyAll extra ts a) in

47 case rules of

48 case rules of

48− [] -> App (applyAll extra ts f) (applyAll extra ts a)

49+ [] -> ap'

49− rs -> case applyFnRules rs ap of

50+ rs -> case applyFnRules rs ap' of

50 Just tm' -> tm'

51 Just tm' -> tm'

51 _ -> App (applyAll extra ts f)

52 _ -> App (applyAll extra ts f)

52 (applyAll extra ts a)

53 (applyAll extra ts a)