3971cb9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

More partial evaluation improvements

Propagate staticness into where blocks, make constraints on instances static, and generalise over functions in types to make the partially evaluated version as general as possible.

commit3971cb9b407470c05256046661e04b4268d10a89 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 19 Oct 2014, 21:47 (12 years ago) parentfde21b7

5 files changed+77−22

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+19−11 src/Idris/Elab/Instance.hs+1−1 src/Idris/Elab/Utils.hs+17 src/Idris/PartialEval.hs+36−9 src/Idris/Transforms.hs+4−1

src/Idris/Elab/Clause.hs+19−11

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

149149

150150 case specNames opts of

151151 Just _ ->

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

153− logLvl 2 $ "Transformed:\n" ++ show pats_transformed

152+ do logLvl 3 $ "Partially evaluated:\n" ++ show pats_pe

154153 _ -> return ()

154+ logLvl 3 $ "Transformed:\n" ++ show pats_transformed

155155

156156 erInfo <- getErasureInfo <$> getIState

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

@@ -333,8 +333,14 @@ elabPE info fc caller r =

333333 idrisCatch

334334 (if (undef && all (concreteArg ist) (snd specapp)) then do

335335 cgns <- getAllNames n

336− let cgns' = filter (/= n) cgns

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

336+ -- on the RHS of the new definition, we should reduce

337+ -- everything that's not itself static (because we'll

338+ -- want to be a PE version of those next)

339+ let cgns' = filter (\x -> x /= n &&

340+ notStatic ist x) cgns

341+ let opts = [Specialise ((if pe_simple specdecl

342+ then map (\x -> (x, Nothing)) cgns'

343+ else []) ++

338344 (n, Just 65536) :

339345 mapMaybe (specName (pe_simple specdecl))

340346 (snd specapp))]

@@ -347,7 +353,7 @@ elabPE info fc caller r =

347353 logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++

348354 showSep "\n"

349355 (map (\ (lhs, rhs) ->

350− (showTmImpls lhs ++ " = " ++

356+ (show lhs ++ " = " ++

351357 showTmImpls rhs)) (pe_clauses specdecl))

352358

353359 logLvl 2 $ show n ++ " transformation rule: " ++

@@ -373,6 +379,10 @@ elabPE info fc caller r =

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

374380 specName simpl _ = Nothing

375381

382+ notStatic ist n = case lookupCtxtExact n (idris_statics ist) of

383+ Just s -> not (or s)

384+ _ -> True

385+

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

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

378388 concreteArg ist _ = True

@@ -554,6 +564,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

554564

555565 let lhs_tm = orderPats (getInferTerm lhs')

556566 let lhs_ty = getInferType lhs'

567+ let static_names = getStaticNames i lhs_tm

568+

557569 logLvl 3 ("Elaborated: " ++ show lhs_tm)

558570 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

559571 logLvl 5 ("Injective: " ++ show fname ++ " " ++ show inj)

@@ -596,7 +608,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

596608 let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all

597609

598610 let winfo = pinfo info newargs defs windex

599− let wb = map (expandParamsD False ist decorate newargs defs) whereblock

611+ let wb = map (mkStatic static_names) $

612+ map (expandParamsD False ist decorate newargs defs) whereblock

600613

601614 -- Split the where block into declarations with a type, and those

602615 -- without

@@ -875,11 +888,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

875888 getImps (Bind n (Pi _ _) t) = pexp Placeholder : getImps t

876889 getImps _ = []

877890

878− getStatics ns (Bind n (Pi _ _) t)

879− | n `elem` ns = True : getStatics ns t

880− | otherwise = False : getStatics ns t

881− getStatics _ _ = []

882−

883891 mkAuxC wname lhs ns ns' (PClauses fc o n cs)

884892 | True = do cs' <- mapM (mkAux wname lhs ns ns') cs

885893 return $ PClauses fc o wname cs'

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

@@ -223,7 +223,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

223223

224224 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

225225

226− conbind (ty : ns) x = PPi (constraint { pstatic = Dynamic })

226+ conbind (ty : ns) x = PPi (constraint) -- { pstatic = Dynamic })

227227 (sMN 0 "class") ty (conbind ns x)

228228 conbind [] x = x

229229

src/Idris/Elab/Utils.hs+17

@@ -251,5 +251,22 @@ getStaticNames ist tm

251251 getStatics _ _ = []

252252getStaticNames _ _ = []

253253

254+getStatics :: [Name] -> Term -> [Bool]

255+getStatics ns (Bind n (Pi _ _) t)

256+ | n `elem` ns = True : getStatics ns t

257+ | otherwise = False : getStatics ns t

258+getStatics _ _ = []

259+

260+mkStatic :: [Name] -> PDecl -> PDecl

261+mkStatic ns (PTy doc argdocs syn fc o n ty)

262+ = PTy doc argdocs syn fc o n (mkStaticTy ns ty)

263+mkStatic ns t = t

264+

265+mkStaticTy :: [Name] -> PTerm -> PTerm

266+mkStaticTy ns (PPi p n ty sc)

267+ | n `elem` ns = PPi (p { pstatic = Static }) n ty (mkStaticTy ns sc)

268+ | otherwise = PPi p n ty (mkStaticTy ns sc)

269+mkStaticTy ns t = t

270+

254271

255272

src/Idris/PartialEval.hs+36−9

@@ -11,6 +11,7 @@ import Idris.Core.TT

1111import Idris.Core.Evaluate

1212

1313import Control.Monad.State

14+import Control.Applicative

1415import Data.Maybe

1516import Debug.Trace

1617

@@ -44,13 +45,25 @@ partial_eval :: Context ->

4445 [(Name, Maybe Int)] ->

4546 [Either Term (Term, Term)] ->

4647 Maybe [Either Term (Term, Term)]

47−partial_eval ctxt ns tms = mapM peClause tms where

48+partial_eval ctxt ns_in tms = mapM peClause tms where

49+ ns = squash ns_in

50+ squash ((n, Just x) : ns)

51+ | Just (Just y) <- lookup n ns

52+ = squash ((n, Just (x + y)) : drop n ns)

53+ | otherwise = (n, Just x) : squash ns

54+ squash (n : ns) = n : squash ns

55+ squash [] = []

56+

57+ drop n ((m, _) : ns) | n == m = ns

58+ drop n (x : ns) = x : drop n ns

59+ drop n [] = []

60+

4861 -- If the term is not a clause, it is simply kept as is

4962 peClause (Left t) = Just $ Left t

5063 -- If the term is a clause, specialise the right hand side

5164 peClause (Right (lhs, rhs))

5265 = let (rhs', reductions) = specialise ctxt [] (map toLimit ns) rhs in

53− do checkProgress ns reductions

66+ do when (length tms == 1) $ checkProgress ns reductions

5467 return (Right (lhs, rhs'))

5568

5669 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit

@@ -103,23 +116,37 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

103116 put (args ++ (zip xs (repeat (sUN "_"))))

104117 return t

105118

106−-- | Creates an Idris type declaration given current state and a specialised TT function application type.

119+-- | Creates an Idris type declaration given current state and a

120+-- specialised TT function application type.

107121-- Can be used in combination with the output of 'specType'.

122+--

123+-- This should: specialise any static argument position, then generalise

124+-- over any function applications in the result.

108125mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

109126mkPE_TyDecl ist args ty = mkty args ty

110127 where

111128 mkty ((ExplicitD, v) : xs) (Bind n (Pi t k) sc)

112− = PPi expl n (delab ist t) (mkty xs sc)

129+ = PPi expl n (delab ist (generaliseIn t)) (mkty xs sc)

113130 mkty ((ImplicitD, v) : xs) (Bind n (Pi t k) sc)

114131 | concreteClass ist t = mkty xs sc

115132 | classConstraint ist t

116− = PPi constraint n (delab ist t) (mkty xs sc)

117− | otherwise = PPi impl n (delab ist t) (mkty xs sc)

133+ = PPi constraint n (delab ist (generaliseIn t)) (mkty xs sc)

134+ | otherwise = PPi impl n (delab ist (generaliseIn t)) (mkty xs sc)

118135

119136 mkty (_ : xs) t

120137 = mkty xs t

121138 mkty [] t = delab ist t

122139

140+ generaliseIn tm = evalState (gen tm) 0

141+

142+ gen tm | (P _ fn _, args) <- unApply tm,

143+ isFnName fn (tt_ctxt ist)

144+ = do nm <- get

145+ put (nm + 1)

146+ return (P Bound (sMN nm "spec") Erased)

147+ gen (App f a) = App <$> gen f <*> gen a

148+ gen tm = return tm

149+

123150-- | Checks if a given argument is a type class constraint argument

124151classConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool

125152classConstraint ist v

@@ -265,9 +292,9 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

265292 ga env tm@(App f a) | (P _ n _, args) <- unApply tm,

266293 n `notElem` map fst (idris_metavars ist) =

267294 ga env f ++ ga env a ++

268− case (lookupCtxt n (idris_statics ist),

269− lookupCtxt n (idris_implicits ist)) of

270− ([statics], [imps]) ->

295+ case (lookupCtxtExact n (idris_statics ist),

296+ lookupCtxtExact n (idris_implicits ist)) of

297+ (Just statics, Just imps) ->

271298 if (length statics == length args && or statics) then

272299 case buildApp env statics imps args [0..] of

273300 args -> [(n, args)]

src/Idris/Transforms.hs+4−1

@@ -47,7 +47,10 @@ applyAll extra ts ap@(App f a)

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

4848 case rules of

4949 [] -> ap'

50− rs -> case applyFnRules rs ap' of

50+ rs -> case applyFnRules rs ap of

51+ Just tm'@(App f' a') ->

52+ App (applyAll extra ts f')

53+ (applyAll extra ts a')

5154 Just tm' -> tm'

5255 _ -> App (applyAll extra ts f)

5356 (applyAll extra ts a)