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

git.iko.soy/Idris-dev

Partially evaluate type class dictionaries

All constraints are assumed to be 'static' so functions with type class constraints will now be monomorphised, ultimately. (I should add a flag to turn partial evaluation off, shortly, in case this is not wanted, or too slow...)

commit03f6913b495c26eaadc54d86b2e1e5c7c84db456 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Oct 2014, 18:53 (12 years ago) parent466a2e7

6 files changed+68−39

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+22−6 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Elab/Class.hs+1−1 src/Idris/Elab/Clause.hs+32−23 src/Idris/PartialEval.hs+8−5 src/Idris/Transforms.hs+4−3

src/Idris/AbsSyntax.hs+22−6

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

10591059addStatics n tm ptm =

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

10611061 ist <- getIState

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

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

1064− _ -> []

1062+ let paramnames

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

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

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

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

10651067

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

10681070 \\ paramnames

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

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

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

10741076 let stpos = staticList statics' tm

10751077 i <- getIState

10761078 when (not (null statics)) $

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

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

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

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

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

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

10791083 ++ "\n" ++ show stpos

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

10811085 addIBC (IBCStatic n)

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

10911095 else (static, dynamic)

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

10931097

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+

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

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

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

src/Idris/AbsSyntaxTree.hs+1−1

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

485485impl = Imp [] Dynamic False

486486expl = Exp [] Dynamic False

487487expl_param = Exp [] Dynamic True

488−constraint = Constraint [] Dynamic

488+constraint = Constraint [] Static

489489tacimpl t = TacImp [] Dynamic t

490490

491491data 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

220220

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

222222 = PPi p n ty (insertConstraint c sc)

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

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

224224 (sMN 0 "class") c sc

225225

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

7474 let atys = map snd (getArgTys fty)

7575 cs_elab <- mapM (elabClause info opts)

7676 (zip [0..] cs)

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

78+ -- no simplification or PE

7779 let (pats_in, cs_full) = unzip cs_elab

78−

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

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

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

8082

8183 solveDeferred n

8284

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

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

9597 -- RHS

9698 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

98100

99101 let tcase = opt_typecase (idris_options ist)

100102

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

103105 -- for partially evaluated definitions

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

105107 Left _ -> return []

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

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

107109

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

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

110112 -- used in place of the general one

111113 ist <- getIState

112− let pats_transformed = transformPats ist pats

114+ let pats_transformed = transformPats ist pats_pe

113115

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

115117 --

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

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

119121

120122 -- 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− let pdef = map debind pats_transformed

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

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

124128

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

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

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

127131

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

137141

138142 case specNames opts of

139143 Just _ ->

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

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

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

142146 _ -> return ()

143147

144148 erInfo <- getErasureInfo <$> getIState

145149 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

147151 cov <- coverage

148152 pmissing <-

149153 if cov && not (hasDefault cs)

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

164168 else return []

165169 let pcover = null pmissing

166170

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

168− pdef_in' <- applyOpts pdef

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

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

173+ pdef_in' <- applyOpts pdef_pe

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

170175

171176 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

197202 ctxt <- getContext

198203 ist <- getIState

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

201206 (idris_patdefs ist) })

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

203208 case lookupTy n ctxt of

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

207212 (AssertTotal `elem` opts)

208213 atys

209214 inacc

210− pats

211− pdef pdef pdef_inl pdef' ty)

215+ pats_pe

216+ pdef

217+ pdef -- compile time

218+ pdef_inl -- inlined

219+ pdef' ty)

212220 addIBC (IBCDef n)

213221 setTotality n tot

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

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

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

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

322330 (n, Just 65536) :

323− mapMaybe specName (snd specapp))]

331+ mapMaybe (specName (pe_simple specdecl))

332+ (snd specapp))]

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

325334 ++ " in " ++ show caller ++

326335 " with " ++ show opts

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

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

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

349358 -- lifted out).

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

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

351360 return [])

352361

353− specName (ImplicitS, tm)

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

355− specName (ExplicitS, tm)

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

357− specName _ = Nothing

362+ specName simpl (ImplicitS, tm)

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

364+ specName simpl (ExplicitS, tm)

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

366+ specName simpl _ = Nothing

358367

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

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

src/Idris/PartialEval.hs+8−5

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

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

44 mkPE_TyDecl, mkPE_TermDecl, PEArgType(..),

5− pe_app, pe_def, pe_clauses) where

5+ pe_app, pe_def, pe_clauses, pe_simple) where

77import Idris.AbsSyntax

88import Idris.Delaborate

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

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

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

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

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

2931 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

3134 }

3235

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

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

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

154157-- in this case

155158mkNewPats 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

157160 where dynVar ap = case unApply ap of

158161 (_, args) -> dynArgs ns args

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

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

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

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

168171mkNewPats ist d ns newname sname lhs rhs =

169− PEDecl lhs rhs (map mkClause d)

172+ PEDecl lhs rhs (map mkClause d) False

170173 where

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

172175 mkClause (oldlhs, oldrhs)

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

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

216219 patdef = lookupCtxtExact sname (idris_patdefs ist)

217220 newpats = case patdef of

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

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

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

220223 newname sname lhs rhs in

221224 newpats where

src/Idris/Transforms.hs+4−3

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

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

4444 = let rules = case lookupCtxtExact fn ts of

4545 Just r -> extra ++ r

46− Nothing -> extra in

46+ Nothing -> extra

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

4748 case rules of

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

49− rs -> case applyFnRules rs ap of

49+ [] -> ap'

50+ rs -> case applyFnRules rs ap' of

5051 Just tm' -> tm'

5152 _ -> App (applyAll extra ts f)

5253 (applyAll extra ts a)