3ade599 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Partial evaluator fixes

Need to identify when a specialisation has made no progress, so we don't treat it as a specialisable application. Also fixes tranform rules. With this it turns out to be safe (if not yet useful) to mark type class dictionaries as 'static', but without further work on the partial evaluator this isn't going to help much yet, so it's not enabled yet.

commit3ade59973af30d5f12bbb10e191d3cd9a27ee799 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 12 Oct 2014, 21:42 (12 years ago) parent6e74e33

8 files changed+129−83

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+8−3 src/Idris/Core/ProofState.hs+2−2 src/Idris/Elab/Clause.hs+60−56 src/Idris/Elab/Transform.hs+2−1 src/Idris/ElabDecls.hs+2−1 src/Idris/Interactive.hs+1−1 src/Idris/PartialEval.hs+17−6 src/Idris/Transforms.hs+37−13

src/Idris/Core/Evaluate.hs+8−3

@@ -89,12 +89,17 @@ normaliseTrace tr ctxt env t

8989 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []

9090 quote 0 val) initEval

9191

92−specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name

92+-- Return a specialised name, and an updated list of reductions available,

93+-- so that the caller can tell how much specialisation was achieved.

94+specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->

95+ (TT Name, [(Name, Int)])

9396specialise ctxt env limits t

94− = evalState (do val <- eval False ctxt []

97+ = let (tm, st) =

98+ runState (do val <- eval False ctxt []

9599 (map finalEntry env) (finalise t)

96100 [Spec]

97− quote 0 val) (initEval { limited = limits })

101+ quote 0 val) (initEval { limited = limits }) in

102+ (tm, limited st)

98103

99104-- | Like normalise, but we only reduce functions that are marked as okay to

100105-- inline (and probably shouldn't reduce lets?)

src/Idris/Core/ProofState.hs+2−2

@@ -651,7 +651,7 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

651651 mapM_ addConsHole (reverse consargs')

652652 let res' = forget $ res

653653 (scv, sct) <- lift $ check ctxt env res'

654− let scv' = specialise ctxt env [] scv

654+ let (scv', _) = specialise ctxt env [] scv

655655 return scv'

656656 [] -> fail $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

657657 xs -> fail $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

@@ -705,7 +705,7 @@ hnf_compute ctxt env t = return t

705705-- reduce let bindings only

706706simplify :: RunTactic

707707simplify ctxt env (Bind x (Hole ty) sc) =

708− do return $ Bind x (Hole (specialise ctxt env [] ty)) sc

708+ do return $ Bind x (Hole (fst (specialise ctxt env [] ty))) sc

709709simplify ctxt env t = return t

710710

711711check_in :: Raw -> RunTactic

src/Idris/Elab/Clause.hs+60−56

@@ -90,22 +90,23 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

9090 Nothing -> transformPats ist pats_in

9191 _ -> pats_in

9292

93− let pats = map (simple_lhs (tt_ctxt ist)) $

94− doPartialEval ist tpats

93+ -- If the definition is specialisable, this reduces the

94+ -- RHS

95+ pe_tm <- doPartialEval ist tpats

96+ let pats = map (simple_lhs (tt_ctxt ist)) pe_tm

9597

96− -- logLvl 3 (showSep "\n" (map (\ (l,r) ->

97− -- show l ++ " = " ++

98− -- show r) pats))

9998 let tcase = opt_typecase (idris_options ist)

10099

101100 -- Look for 'static' names and generate new specialised

102101 -- definitions for them, as well as generating rewrite rules

103102 -- for partially evaluated definitions

104− mapM_ (\ e -> case e of

105− Left _ -> return ()

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

103+ newrules <- mapM (\ e -> case e of

104+ Left _ -> return []

105+ Right (l, r) -> elabPE info fc n r) pats

107106

108− -- Redo transforms with the newly generated transformations

107+ -- Redo transforms with the newly generated transformations, so

108+ -- that the specialised application we've just made gets

109+ -- used in place of the general one

109110 ist <- getIState

110111 let pats_transformed = transformPats ist pats

111112

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

134135 numArgs <- tclift $ sameLength pdef

135136

136137 case specNames opts of

137− Just _ -> logLvl 1 $ "Partially evaluated:\n" ++ show pats

138+ Just _ ->

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

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

138141 _ -> return ()

139142

140143 erInfo <- getErasureInfo <$> getIState

@@ -257,22 +260,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

257260

258261 getLHS (_, l, _) = l

259262

260− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x,

261− force (normalisePats ctxt [] y))

263+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

262264 simple_lhs ctxt t = t

263265

264266 simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

265267 (rt_simplify ctxt [] y)))

266268

267− -- this is so pattern types are in the right form for erasure

268− normalisePats ctxt env (Bind n (PVar t) sc)

269− = let t' = normalise ctxt env t in

270− Bind n (PVar t') (normalisePats ctxt ((n, PVar t') : env) sc)

271− normalisePats ctxt env (Bind n (PVTy t) sc)

272− = let t' = normalise ctxt env t in

273− Bind n (PVTy t') (normalisePats ctxt ((n, PVar t') : env) sc)

274− normalisePats ctxt env t = t

275−

276269 specNames [] = Nothing

277270 specNames (Specialise ns : _) = Just ns

278271 specNames (_ : xs) = specNames xs

@@ -287,15 +280,19 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

287280 -- Partially evaluate, if the definition is marked as specialisable

288281 doPartialEval ist pats =

289282 case specNames opts of

290− Nothing -> pats

291− Just ns -> partial_eval (tt_ctxt ist) ns pats

292−

293−-- | Find 'static' applications in a term and partially evaluate them

294−elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()

283+ Nothing -> return pats

284+ Just ns -> case partial_eval (tt_ctxt ist) ns pats of

285+ Just t -> return t

286+ Nothing -> ierror (At fc (Msg "No specialisation achieved"))

287+

288+-- | Find 'static' applications in a term and partially evaluate them.

289+-- Return any new transformation rules

290+elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]

295291elabPE info fc caller r =

296292 do ist <- getIState

297293 let sa = getSpecApps ist [] r

298− mapM_ (mkSpecialised ist) sa

294+ rules <- mapM mkSpecialised sa

295+ return $ concat rules

299296 where

300297 -- Make a specialised version of the application, and

301298 -- add a PTerm level transformation rule, which is basically the

@@ -305,41 +302,48 @@ elabPE info fc caller r =

305302

306303 -- Transformation rules are applied after every PClause elaboration

307304

308− mkSpecialised ist specapp_in = do

305+ mkSpecialised :: (Name, [(PEArgType, Term)]) -> Idris [(Term, Term)]

306+ mkSpecialised specapp_in = do

307+ ist <- getIState

309308 let (specTy, specapp) = getSpecTy ist specapp_in

310309 let (n, newnm, (lhs, rhs)) = getSpecClause ist specapp

311− let undef = case lookupDef newnm (tt_ctxt ist) of

312− [] -> True

310+ let undef = case lookupDefExact newnm (tt_ctxt ist) of

311+ Nothing -> True

313312 _ -> False

314− logLvl 3 $ show (newnm, map (concreteArg ist) (snd specapp))

313+ logLvl 5 $ show (newnm, undef, map (concreteArg ist) (snd specapp))

315314 idrisCatch

316− (when (undef && all (concreteArg ist) (snd specapp)) $ do

317− cgns <- getAllNames n

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

319− mapMaybe specName (snd specapp))]

320− logLvl 3 $ "Specialising application: " ++ show specapp

321− ++ " with " ++ show opts

322− logLvl 3 $ "New name: " ++ show newnm

323− logLvl 3 $ "PE definition type : " ++ (show specTy)

324− ++ "\n" ++ show opts

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

326−-- showSep "\n"

327−-- (map (\ (lhs, rhs) ->

328− (showTmImpls lhs ++ " = " ++

329− showTmImpls rhs) -- pats)

330−

331− logLvl 2 $ show n ++ " transformation rule: " ++

332− show rhs ++ " ==> " ++ show lhs

333−

334− elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

335− let def = -- map (\ (lhs, rhs) ->

336− [PClause fc newnm lhs [] rhs []] --) pats

337− elabTransform info fc False rhs lhs

338− elabClauses info fc opts newnm def)

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

316+ cgns <- getAllNames n

317+ let cgns' = filter (/= n) cgns

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

319+ (n, Just 65536) :

320+ mapMaybe specName (snd specapp))]

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

322+ ++ " with " ++ show opts

323+ logLvl 3 $ "New name: " ++ show newnm

324+ logLvl 3 $ "PE definition type : " ++ (show specTy)

325+ ++ "\n" ++ show opts

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

327+ -- showSep "\n"

328+ -- (map (\ (lhs, rhs) ->

329+ (showTmImpls lhs ++ " = " ++

330+ showTmImpls rhs) -- pats)

331+

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

333+ show rhs ++ " ==> " ++ show lhs

334+

335+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

336+ let def = -- map (\ (lhs, rhs) ->

337+ [PClause fc newnm lhs [] rhs []] --) pats

338+ trans <- elabTransform info fc False rhs lhs

339+ elabClauses info fc opts newnm def

340+ return [trans]

341+ else return [])

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

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

341344 -- lifted out).

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

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

346+ return [])

343347

344348 specName (ImplicitS, tm)

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

@@ -370,7 +374,7 @@ elabPE info fc caller r =

370374

371375 -- get the clause of a specialised application

372376 getSpecClause ist (n, args)

373− = let newnm = sUN ("PE_"++ show (nsroot n) ++ "_" ++

377+ = let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++

374378 qhash 0 (showSep "_" (map showArg args))) in

375379 -- UN (show n ++ show (map snd args)) in

376380 (n, newnm, mkPE_TermDecl ist newnm n args)

src/Idris/Elab/Transform.hs+2−1

@@ -48,7 +48,7 @@ import Data.List.Split (splitOn)

4848

4949import Util.Pretty(pretty, text)

5050

51−elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

51+elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)

5252elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

5353 = do ctxt <- getContext

5454 i <- getIState

@@ -88,6 +88,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

8888 (P _ tfname _, _) -> do addTrans tfname (clhs_tm, crhs_tm)

8989 addIBC (IBCTrans tf (clhs_tm, crhs_tm))

9090 _ -> ierror (At fc (Msg "Invalid transformation rule (must be function application)"))

91+ return (clhs_tm, crhs_tm)

9192

9293 where

9394 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

src/Idris/ElabDecls.hs+2−1

@@ -254,6 +254,7 @@ elabDecl' what info (PProvider syn fc provWhat n)

254254 = do iLOG $ "Elaborating type provider " ++ show n

255255 elabProvider info syn fc provWhat n

256256elabDecl' what info (PTransform fc safety old new)

257− = elabTransform info fc safety old new

257+ = do elabTransform info fc safety old new

258+ return ()

258259elabDecl' _ _ _ = return () -- skipped this time

259260

src/Idris/Interactive.hs+1−1

@@ -188,7 +188,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

188188 pprintPTerm defaultPPOption [] [] (idris_infixes i)

189189 (stripNS

190190 (dropCtxt envlen

191− (delab i (specialise ctxt [] [(mn, 1)] tm)))))

191+ (delab i (fst (specialise ctxt [] [(mn, 1)] tm))))))

192192 (\e -> return ("?" ++ show n))

193193 if updatefile then

194194 do let fb = fn ++ "~"

src/Idris/PartialEval.hs+17−6

@@ -13,20 +13,31 @@ import Control.Monad.State

1313import Debug.Trace

1414

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

16−partial_eval :: Context -> [(Name, Maybe Int)] ->

16+-- It is an error if partial evaluation fails to make any progress.

17+-- Making progress is defined as: all of the names given with explicit

18+-- reduction limits must have reduced at least once.

19+partial_eval :: Context ->

20+ [(Name, Maybe Int)] ->

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

18− [Either Term (Term, Term)]

19−partial_eval ctxt ns tms = map peClause tms where

22+ Maybe [Either Term (Term, Term)]

23+partial_eval ctxt ns tms = mapM peClause tms where

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

21− peClause (Left t) = Left t

25+ peClause (Left t) = Just $ Left t

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

2327 peClause (Right (lhs, rhs))

24− = let rhs' = specialise ctxt [] (map toLimit ns) rhs in

25− Right (lhs, rhs')

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

29+ do checkProgress ns reductions

30+ return (Right (lhs, rhs'))

2631

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

2833 toLimit (n, Just l) = (n, l)

2934

35+ checkProgress ns [] = return ()

36+ checkProgress ns ((n, r) : rs)

37+ | Just (Just start) <- lookup n ns

38+ = if r < start then checkProgress ns rs else Nothing

39+ | otherwise = checkProgress ns rs

40+

3041-- | Specialises the type of a partially evaluated TT function returning

3142-- a pair of the specialised type and the types of expected arguments.

3243specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])

src/Idris/Transforms.hs+37−13

@@ -1,6 +1,9 @@

11{-# LANGUAGE PatternGuards #-}

3−module Idris.Transforms(transformPats, applyTransRules) where

3+module Idris.Transforms(transformPats,

4+ transformPatsWith,

5+ applyTransRulesWith,

6+ applyTransRules) where

58import Idris.AbsSyntax

69import Idris.Core.CaseTree

@@ -16,19 +19,40 @@ transformPats ist ps = map tClause ps where

1619 = let rhs' = applyTransRules ist rhs in

1720 Right (lhs, rhs')

1821

22+transformPatsWith :: [(Term, Term)] -> [Either Term (Term, Term)] ->

23+ [Either Term (Term, Term)]

24+transformPatsWith rs ps = map tClause ps where

25+ tClause (Left t) = Left t -- not a clause, leave it alone

26+ tClause (Right (lhs, rhs)) -- apply transforms on RHS

27+ = let rhs' = applyTransRulesWith rs rhs in

28+ Right (lhs, rhs')

29+

30+-- Work on explicitly named terms, so we don't have to manipulate

31+-- de Bruijn indices

1932applyTransRules :: IState -> Term -> Term

20−applyTransRules ist tm = applyAll (idris_transforms ist) tm

33+applyTransRules ist tm = finalise $ applyAll [] (idris_transforms ist) (vToP tm)

34+

35+-- Work on explicitly named terms, so we don't have to manipulate

36+-- de Bruijn indices

37+applyTransRulesWith :: [(Term, Term)] -> Term -> Term

38+applyTransRulesWith rules tm

39+ = finalise $ applyAll rules emptyContext (vToP tm)

2140

22−applyAll :: Ctxt [(Term, Term)] -> Term -> Term

23−applyAll ts ap@(App f a)

41+applyAll :: [(Term, Term)] -> Ctxt [(Term, Term)] -> Term -> Term

42+applyAll extra ts ap@(App f a)

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

25− = case lookupCtxtExact fn ts of

26− Just rules -> case applyFnRules rules ap of

44+ = let rules = case lookupCtxtExact fn ts of

45+ Just r -> extra ++ r

46+ Nothing -> extra in

47+ case rules of

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

49+ rs -> case applyFnRules rs ap of

2750 Just tm' -> tm'

28− _ -> App (applyAll ts f) (applyAll ts a)

29− Nothing -> App (applyAll ts f) (applyAll ts a)

30−applyAll ts (Bind n b sc) = Bind n (fmap (applyAll ts) b) (applyAll ts sc)

31−applyAll ts t = t

51+ _ -> App (applyAll extra ts f)

52+ (applyAll extra ts a)

53+applyAll extra ts (Bind n b sc) = Bind n (fmap (applyAll extra ts) b)

54+ (applyAll extra ts sc)

55+applyAll extra ts t = t

3256

3357applyFnRules :: [(Term, Term)] -> Term -> Maybe Term

3458applyFnRules [] tm = Nothing

@@ -40,12 +64,12 @@ applyRule (lhs, rhs) tm

4064 | Just ms <- matchTerm lhs tm

4165-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++

4266-- "\n" ++ show rhs

43−-- ++ "\n" ++ show tm) $

44− = Just $ depat ms rhs

67+-- ++ "\n" ++ show tm ++ " GIVES\n" ++ show (depat ms rhs)) $

68+ = Just $ depat ms rhs

4569 | otherwise = Nothing

4670 where depat ms (Bind n (PVar t) sc)

4771 = case lookup n ms of

48− Just tm -> depat ms (instantiate tm sc)

72+ Just tm -> depat ms (subst n tm sc)

4973 _ -> depat ms sc -- no occurrence? Shouldn't happen

5074 depat ms tm = tm

5175