git.iko.soy/Idris-dev
on master help sign in
Apply forcing optimisation on LHS

This means that the case trees generated are much smaller, because we don't bother matching on things we already know about. Needs some care, because it affects some existing erasure results. For the moment, we only force arguments when there's *no* occurrence of a variable below a non-constructor name. This may be an issue with erasure warnings rather than forcing, but it solves the problem for now. Fixes #2657

commit0f3e4e38d9be705f95ed778c9578278c21910866 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 19 Nov 2016, 14:39 (10 years ago) parent001dfed
8 files changed+135−38
compare with master
unifiedsplit
src/Idris/ASTUtils.hs+4−1 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Core/CaseTree.hs+19−17 src/Idris/Elab/Clause.hs+57−14 src/Idris/Elab/Data.hs+46 src/Idris/Elab/Utils.hs+1−1 src/Idris/Erasure.hs+1−1 src/Idris/IBC.hs+5−3
src/Idris/ASTUtils.hs+4−1
@@ -41,7 +41,7 @@ module Idris.ASTUtils(
4141 Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState
4242 , fputState, idris_fixities, ist_callgraph, ist_optimisation
4343 , known_interfaces, known_terms, opt_detaggable, opt_inaccessible
44− , opts_idrisCmdline, repl_definitions
44+ , opt_forceable, opts_idrisCmdline, repl_definitions
4545 ) where
4646
4747import Idris.AbsSyntaxTree
@@ -111,6 +111,7 @@ ist_optimisation n =
111111 maybe_default Optimise
112112 { inaccessible = []
113113 , detaggable = False
114+ , forceable = []
114115 }
115116 . ctxt_lookup n
116117 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
@@ -122,6 +123,8 @@ opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
122123opt_detaggable :: Field OptInfo Bool
123124opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
124125
126+opt_forceable :: Field OptInfo [Int]
127+opt_forceable = Field forceable (\v opt -> opt{ forceable = v })
125128
126129-- | callgraph record for the given (exact) name
127130ist_callgraph :: Name -> Field IState CGInfo
src/Idris/AbsSyntaxTree.hs+2−1
@@ -1440,6 +1440,7 @@ deriving instance Binary FnInfo
14401440data OptInfo = Optimise {
14411441 inaccessible :: [(Int,Name)] -- includes names for error reporting
14421442 , detaggable :: Bool
1443+ , forceable :: [Int] -- argument positions which are forced by other values
14431444 } deriving (Show, Generic)
14441445{-!
14451446deriving instance Binary OptInfo
@@ -2564,5 +2565,5 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm
25642565getErasureInfo :: IState -> Name -> [Int]
25652566getErasureInfo ist n =
25662567 case lookupCtxtExact n (idris_optimisation ist) of
2567− Just (Optimise inacc detagg) -> map fst inacc
2568+ Just (Optimise inacc detag force) -> map fst inacc
25682569 Nothing -> []
src/Idris/Core/CaseTree.hs+19−17
@@ -36,6 +36,7 @@ import Control.Monad.State
3636import Data.List hiding (partition)
3737import qualified Data.List (partition)
3838import Data.Maybe
39+import qualified Data.Set as S
3940import Debug.Trace
4041import GHC.Generics (Generic)
4142
@@ -153,33 +154,34 @@ findCalls :: SC -> [Name] -> [(Name, [[Name]])]
153154findCalls = findCalls' False
154155
155156findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]
156−findCalls' ignoreasserts sc topargs = nub $ nu' topargs sc where
157− nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)
158− nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts
159− nu' ps (STerm t) = nub $ nut ps t
160− nu' ps _ = []
161−
162− nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc)
163− nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc)
157+findCalls' ignoreasserts sc topargs = S.toList $ nu' topargs sc where
158+ nu' ps (Case _ n alts) = S.unions $ map (nua (n : ps)) alts
159+ nu' ps (ProjCase t alts) = S.unions $ nut ps t : map (nua ps) alts
160+ nu' ps (STerm t) = nut ps t
161+ nu' ps _ = S.empty
162+
163+ nua ps (ConCase n i args sc) = nu' (ps ++ args) sc
164+ nua ps (FnCase n args sc) = nu' (ps ++ args) sc
164165 nua ps (ConstCase _ sc) = nu' ps sc
165166 nua ps (SucCase _ sc) = nu' ps sc
166167 nua ps (DefaultCase sc) = nu' ps sc
167168
168− nut ps (P _ n _) | n `elem` ps = []
169− | otherwise = [(n, [])] -- tmp
169+ nut ps (P _ n _) | n `elem` ps = S.empty
170+ | otherwise = S.singleton (n, [])
170171 nut ps fn@(App _ f a)
171172 | (P _ n _, args) <- unApply fn
172173 = if ignoreasserts && n == sUN "assert_total"
173− then []
174+ then S.empty
174175 else if n `elem` ps
175− then nut ps f ++ nut ps a
176− else [(n, map argNames args)] ++ concatMap (nut ps) args
177− | (P (TCon _ _) n _, _) <- unApply fn = []
178− | otherwise = nut ps f ++ nut ps a
179− nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc
176+ then S.union (nut ps f) (nut ps a)
177+ else S.insert (n, map argNames args)
178+ (S.unions $ map (nut ps) args)
179+ | (P (TCon _ _) n _, _) <- unApply fn = S.empty
180+ | otherwise = S.union (nut ps f) (nut ps a)
181+ nut ps (Bind n (Let t v) sc) = S.union (nut ps v) (nut (n:ps) sc)
180182 nut ps (Proj t _) = nut ps t
181183 nut ps (Bind n b sc) = nut (n:ps) sc
182− nut ps _ = []
184+ nut ps _ = S.empty
183185
184186 argNames tm = let ns = directUse tm in
185187 filter (\x -> x `elem` ns) topargs
src/Idris/Elab/Clause.hs+57−14
@@ -86,11 +86,16 @@ elabClauses info' fc opts n_in cs =
8686 cs_elab <- mapM (elabClause info opts)
8787 (zip [0..] cs)
8888 ctxt <- getContext
89− -- pats_raw is the version we'll work with at compile time:
90− -- no simplification or PE
89+ -- pats_raw is the basic type checked version, no PE or forcing
90+ let optinfo = idris_optimisation ist
9191 let (pats_in, cs_full) = unzip cs_elab
9292 let pats_raw = map (simple_lhs ctxt) pats_in
93+ -- We'll apply forcing to the left hand side here, so that we don't
94+ -- do any unnecessary case splits
95+ let pats_forced = map (force_lhs optinfo) pats_raw
96+
9397 logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw
98+ logElab 5 $ "Forced patterns:\n" ++ show pats_forced
9499
95100 solveDeferred fc n
96101
@@ -109,9 +114,10 @@ elabClauses info' fc opts n_in cs =
109114 -- If the definition is specialisable, this reduces the
110115 -- RHS
111116 pe_tm <- doPartialEval ist tpats
117+
112118 let pats_pe = if petrans
113− then map (simple_lhs ctxt) pe_tm
114− else pats_raw
119+ then map (force_lhs optinfo . simple_lhs ctxt) pe_tm
120+ else pats_forced
115121
116122 let tcase = opt_typecase (idris_options ist)
117123
@@ -138,11 +144,19 @@ elabClauses info' fc opts n_in cs =
138144
139145 -- addCaseDef builds case trees from <pdef> and <pdef'>
140146
141− -- pdef is the compile-time pattern definition.
142− -- This will get further inlined to help with totality checking.
143− let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ map debind pats_raw
147+ -- pdef is the compile-time pattern definition, after forcing
148+ -- optimisation applied to LHS
149+ let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $
150+ map debind pats_forced
151+ -- pdef_cov is the pattern definition without forcing, which
152+ -- we feed to the coverage checker (we need to know what the
153+ -- programmer wrote before forcing erasure)
154+ let pdef_cov
155+ = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $
156+ map debind pats_raw
144157 -- pdef_pe is the one which will get further optimised
145− -- for run-time, and, partially evaluated
158+ -- for run-time, with no forcing optimisation of the LHS because
159+ -- the affects erasure. Also, it's partially evaluated
146160 let pdef_pe = map debind pats_transformed
147161
148162 logElab 5 $ "Initial typechecked patterns:\n" ++ show pats_raw
@@ -171,12 +185,12 @@ elabClauses info' fc opts n_in cs =
171185 pmissing <-
172186 if cov && not (hasDefault pats_raw)
173187 then do -- Generate clauses from the given possible cases
174− missing <- genClauses fc n (map getLHS pdef) cs_full
188+ missing <- genClauses fc n (map getLHS pdef_cov) cs_full
175189 -- missing <- genMissing n scargs sc
176190 missing' <- filterM (checkPossible info fc True n) missing
177191 -- Filter out the ones which match one of the
178192 -- given cases (including impossible ones)
179− let clhs = map getLHS pdef
193+ let clhs = map getLHS pdef_cov
180194 logElab 2 $ "Must be unreachable:\n" ++
181195 showSep "\n" (map showTmImpls missing') ++
182196 "\nAgainst: " ++
@@ -228,6 +242,7 @@ elabClauses info' fc opts n_in cs =
228242 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)
229243 (idris_patdefs ist) })
230244 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)
245+
231246 case lookupTyExact n ctxt of
232247 Just ty ->
233248 do ctxt' <- do ctxt <- getContext
@@ -238,7 +253,7 @@ elabClauses info' fc opts n_in cs =
238253 (AssertTotal `elem` opts)
239254 atys
240255 inacc
241− pats_pe
256+ pats_forced
242257 pdef
243258 pdef' ty
244259 ctxt
@@ -329,9 +344,13 @@ elabClauses info' fc opts n_in cs =
329344
330345 -- Simplify the left hand side of a definition, to remove any lets
331346 -- that may have arisen during elaboration
332− simple_lhs ctxt (Right (x, y)) = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)
347+ simple_lhs ctxt (Right (x, y))
348+ = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)
333349 simple_lhs ctxt t = t
334350
351+ force_lhs opts (Right (x, y)) = Right (forceWith opts x, y)
352+ force_lhs opts t = t
353+
335354 simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p
336355 (rt_simplify ctxt [] y)))
337356
@@ -354,6 +373,28 @@ elabClauses info' fc opts n_in cs =
354373 Just t -> return t
355374 Nothing -> ierror (At fc (Msg "No specialisation achieved"))
356375
376+forceWith :: Ctxt OptInfo -> Term -> Term
377+forceWith opts lhs = -- trace (show lhs ++ "\n==>\n" ++ show (force lhs) ++ "\n----") $
378+ force lhs
379+ where
380+ -- If there's forced arguments, erase them
381+ force ap@(App _ _ _)
382+ | (fn@(P _ c _), args) <- unApply ap,
383+ Just copt <- lookupCtxtExact c opts
384+ = let args' = eraseArg 0 (forceable copt) args in
385+ mkApp fn (map force args')
386+ force (App t f a)
387+ = App t (force f) (force a)
388+ -- We might have pat bindings, so go under them
389+ force (Bind n b sc) = Bind n b (force sc)
390+ -- Everything else, leave it alone
391+ force t = t
392+
393+ eraseArg i fs (n : ns) | i `elem` fs = Erased : eraseArg (i + 1) fs ns
394+ | otherwise = n : eraseArg (i + 1) fs ns
395+ eraseArg i _ [] = []
396+
397+
357398-- | Find 'static' applications in a term and partially evaluate them.
358399-- Return any new transformation rules
359400elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]
@@ -667,7 +708,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
667708 then recheckC_borrowing False (PEGenerated `notElem` opts)
668709 [] (constraintNS info) fc id [] lhs_tm
669710 else return (lhs_tm, lhs_ty)
670− let clhs = Idris.Core.Evaluate.simplify ctxt [] clhs_c
711+ let clhs = normalise ctxt [] clhs_c
671712 let borrowed = borrowedNames [] clhs
672713
673714 -- These are the names we're not allowed to use on the RHS, because
@@ -925,7 +966,9 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
925966 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
926967 let static_names = getStaticNames i lhs_tm
927968 logElab 5 (show lhs_tm ++ "\n" ++ show static_names)
928− (clhs, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm
969+ (clhs_c, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm
970+ let clhs = normalise ctxt [] clhs_c
971+
929972 logElab 5 ("Checked " ++ show clhs)
930973 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
931974 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in
src/Idris/Elab/Data.hs+46
@@ -189,9 +189,13 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
189189
190190 -- Check that the constructor type is, in fact, a part of the family being defined
191191 tyIs n cty'
192+ let force = if tn == sUN "Delayed"
193+ then [] -- TMP HACK! Totality checker needs this info
194+ else forceArgs ctxt cty'
192195
193196 logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t
194197 logElab 5 $ "Inaccessible args: " ++ show inacc
198+ logElab 5 $ "Forceable args: " ++ show force
195199 logElab 2 $ "---> " ++ show n ++ " : " ++ show cty
196200
197201 -- Add to the context (this is temporary, so that later constructors
@@ -206,6 +210,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
206210 addDocStr n doc' argDocs'
207211 addIBC (IBCDoc n)
208212 fputState (opt_inaccessible . ist_optimisation n) inacc
213+ fputState (opt_forceable . ist_optimisation n) force
209214 addIBC (IBCOpt n)
210215 return (n, cty)
211216 where
@@ -255,6 +260,47 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
255260 = tclift $ tfail (At fc (UniqueKindError AllTypes n))
256261 checkUniqueKind _ _ = return ()
257262
263+forceArgs :: Context -> Type -> [Int]
264+forceArgs ctxt ty = forceFrom 0 ty
265+ where
266+ -- for each argument, substitute in MN pos "FF"
267+ -- then when we look at the return type, if we see MN pos name
268+ -- constructor guarded, then 'pos' is a forceable position
269+ forceFrom :: Int -> Type -> [Int]
270+ forceFrom i (Bind n (Pi _ _ _) sc)
271+ = forceFrom (i + 1) (substV (P Ref (sMN i "FF") Erased) sc)
272+ forceFrom i sc
273+ -- Go under the top level type application
274+ -- We risk affecting erasure of more complex indices, so we'll only
275+ -- mark something forced if *everything* which appears in an index
276+ -- is forceable
277+ -- (FIXME: Actually the real risk is if we erase something a programmer
278+ -- definitely wants, which is particularly the case with 'views'.
279+ -- So perhaps we need a way of marking that in the source?)
280+ | (P _ ty _, args) <- unApply sc
281+ = if null (concatMap (findNonForcePos True) args)
282+ then nub (concatMap findForcePos args)
283+ else []
284+ forceFrom i sc = []
285+
286+ findForcePos (P _ (MN i ff) _)
287+ | ff == txt "FF" = [i]
288+ -- Only look under constructors in applications
289+ findForcePos ap@(App _ f a)
290+ | (P _ con _, args) <- unApply ap,
291+ isDConName con ctxt
292+ = nub $ concatMap findForcePos args
293+ findForcePos _ = []
294+
295+ findNonForcePos fok (P _ (MN i ff) _)
296+ | ff == txt "FF" = if fok then [] else [i]
297+ -- Look under non-constructors in applications for things which can't
298+ -- be forced
299+ findNonForcePos fok ap@(App _ f a)
300+ | (P _ con _, args) <- unApply ap
301+ = nub $ concatMap (findNonForcePos (fok && isConName con ctxt)) args
302+ findNonForcePos _ _ = []
303+
258304addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
259305addParamConstraints fc ps cty cons
260306 = case getRetTy cty of
src/Idris/Elab/Utils.hs+1−1
@@ -438,7 +438,7 @@ setDetaggable n = do
438438 let opt = idris_optimisation ist
439439 case lookupCtxt n opt of
440440 [oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt }
441− _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }
441+ _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True []) opt }
442442
443443displayWarnings :: EState -> Idris ()
444444displayWarnings est
src/Idris/Erasure.hs+1−1
@@ -134,7 +134,7 @@ performUsageAnalysis startNames = do
134134
135135 checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
136136 checkAccessibility opt (n, reachable)
137− | Just (Optimise inaccessible dt) <- lookupCtxtExact n opt
137+ | Just (Optimise inaccessible dt force) <- lookupCtxtExact n opt
138138 , eargs@(_:_) <- [fmt n (S.toList rs) | (i,n) <- inaccessible, rs <- maybeToList $ IM.lookup i reachable]
139139 = warn $ show n ++ ": inaccessible arguments reachable:\n " ++ intercalate "\n " eargs
140140
src/Idris/IBC.hs+5−3
@@ -47,7 +47,7 @@ import System.Directory
4747import System.FilePath
4848
4949ibcVersion :: Word16
50−ibcVersion = 154
50+ibcVersion = 155
5151
5252-- | When IBC is being loaded - we'll load different things (and omit
5353-- different structures/definitions) depending on which phase we're in.
@@ -2396,13 +2396,15 @@ instance Binary RecordInfo where
23962396 return (RI x1 x2 x3)
23972397
23982398instance Binary OptInfo where
2399− put (Optimise x1 x2)
2399+ put (Optimise x1 x2 x3)
24002400 = do put x1
24012401 put x2
2402+ put x3
24022403 get
24032404 = do x1 <- get
24042405 x2 <- get
2405− return (Optimise x1 x2)
2406+ x3 <- get
2407+ return (Optimise x1 x2 x3)
24062408
24072409instance Binary FnInfo where
24082410 put (FnInfo x1)