6bcf43a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1625 from edwinb/partial-eval

Partial evaluator fixes

commit6bcf43a2d8e5538fc7db29abac10d6435778d8d4 authorEdwin Brady <edwin.brady@gmail.com> dateSun 12 Oct 2014, 23:08 (12 years ago) parentabc2002 3ade599

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