git.iko.soy/Idris-dev
on master help sign in
Calculate size change graphs
commitebb75fb379a0d332b4d50970c5413d052727d9df authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 25 Oct 2012, 16:00 (14 years ago) parent1d125cf
4 files changed+84−7
compare with master
unifiedsplit
src/Core/CaseTree.hs+30−3 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Coverage.hs+52−2 src/Idris/ElabDecls.hs+1−1
src/Core/CaseTree.hs+30−3
@@ -161,7 +161,7 @@ simpleCase tc cover phase fc cs
161161 ns = take numargs args
162162 (tree, st) = runState
163163 (match (rev phase ns) pats (defaultCase cover)) ([], numargs)
164− t = CaseDef ns (prune proj tree) (fst st) in
164+ t = CaseDef ns (prune proj (depatt ns tree)) (fst st) in
165165 if proj then return (stripLambdas t) else return t
166166 Error err -> Error (At fc err)
167167 where args = map (\i -> MN i "e") [0..]
@@ -341,10 +341,37 @@ varRule (v : vs) alts err =
341341 do let alts' = map (repVar v) alts
342342 match vs alts' err
343343 where
344− repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v (V 0)) res))
344+ repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v Erased) res))
345345 repVar v (PAny : ps , res) = (ps, res)
346346
347−prune :: Bool -> -- ^ Convert single brances to projections (only useful at runtime)
347+-- fix: case e of S k -> f (S k) ==> case e of S k -. f e
348+depatt :: [Name] -> SC -> SC
349+depatt ns tm = dp [] tm
350+ where
351+ dp ms (STerm tm) = STerm (applyMaps ms tm)
352+ dp ms (Case x alts) = Case x (map (dpa ms x) alts)
353+ dp ms sc = sc
354+
355+ dpa ms x (ConCase n i args sc)
356+ = ConCase n i args (dp ((x, (n, args)) : ms) sc)
357+ dpa ms x (ConstCase c sc) = ConstCase c (dp ms sc)
358+ dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)
359+
360+ applyMaps ms f@(App _ _)
361+ | (P nt cn pty, args) <- unApply f
362+ = let args' = map (applyMaps ms) args in
363+ applyMap ms nt cn pty args'
364+ where
365+ applyMap [] nt cn pty args' = mkApp (P nt cn pty) args'
366+ applyMap ((x, (n, args)) : ms) nt cn pty args'
367+ | and ((n == cn) : zipWith same args args') = P Ref x Erased
368+ | otherwise = applyMap ms nt cn pty args'
369+ same n (P _ n' _) = n == n'
370+ same _ _ = False
371+ applyMaps ms (App f a) = App (applyMaps ms f) (applyMaps ms a)
372+ applyMaps ms t = t
373+
374+prune :: Bool -> -- ^ Convert single branches to projections (only useful at runtime)
348375 SC -> SC
349376prune proj (Case n alts)
350377 = let alts' = filter notErased (map pruneAlt alts) in
src/Idris/AbsSyntaxTree.hs+1−1
@@ -89,7 +89,7 @@ deriving instance Binary SizeChange
8989
9090data CGInfo = CGInfo { argsdef :: [Name],
9191 calls :: [(Name, [[Name]])],
92− scg :: [(Name, [[Maybe (Name, SizeChange)]])],
92+ scg :: [(Name, [Maybe (Name, SizeChange)])],
9393 argsused :: [Name],
9494 unusedpos :: [Int] }
9595 deriving Show
src/Idris/Coverage.hs+52−2
@@ -432,6 +432,56 @@ checkDeclTotality (fc, n)
432432-- sizechange1 ... sizechange2 is how their size has changed wrt the input to f
433433-- Nothing, if the argument is unrelated to the input
434434
435−buildSCG :: SC -> [Name] -> [(Name, [[Maybe (Name, SizeChange)]])]
436−buildSCG _ _ = []
435+buildSCG :: IState -> SC -> [Name] -> [(Name, [Maybe (Name, SizeChange)])]
436+buildSCG ist sc args = scg sc (zip args args) (zip args (zip args (repeat Same)))
437+ where
438+ scg :: SC -> [(Name, Name)] -> -- local var, originating top level var
439+ [(Name, (Name, SizeChange))] -> -- map from orig to new and relationship
440+ [(Name, [Maybe (Name, SizeChange)])]
441+ scg (Case x alts) vars szs = concatMap (scgAlt x vars szs) alts
442+ scg (STerm tm) vars szs = scgTerm tm vars szs
443+ scg _ _ _ = []
444+
445+ -- how the arguments relate - either Smaller or Unknown
446+ argRels :: Name -> [(Name, SizeChange)]
447+ argRels n = let ctxt = tt_ctxt ist
448+ [ty] = lookupTy Nothing n ctxt -- must exist!
449+ P _ nty _ = fst (unApply (getRetTy ty))
450+ args = map snd (getArgTys ty) in
451+ map (getRel nty) (map (fst . unApply) args)
452+ where
453+ getRel ty (P _ n' _) | n' == ty = (n, Smaller)
454+ getRel ty _ = (n, Unknown)
455+
456+ scgAlt x vars szs (ConCase n _ args sc)
457+ -- all args smaller than top variable of x in sc
458+ -- (as long as they are in the same type family)
459+ | Just tvar <- lookup x vars
460+ = let arel = argRels n
461+ szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel ++ szs
462+ vars' = zip args (repeat tvar) ++ vars in
463+ scg sc vars' szs'
464+ | otherwise = scg sc vars szs
465+ scgAlt x vars szs (ConstCase _ sc) = scg sc vars szs
466+ scgAlt x vars szs (DefaultCase sc) = scg sc vars szs
467+
468+ scgTerm f@(App _ _) vars szs
469+ | (P _ fn _, args) <- unApply f
470+ = let rest = concatMap (\x -> scgTerm x vars szs) args in
471+ case lookup fn vars of
472+ Just _ -> rest
473+ Nothing -> (fn, map (mkChange szs) args) : rest
474+ scgTerm (App f a) vars szs
475+ = scgTerm f vars szs ++ scgTerm a vars szs
476+ scgTerm (Bind n (Let t v) e) vars szs
477+ = scgTerm v vars szs ++ scgTerm e vars szs
478+ scgTerm (Bind n _ e) vars szs
479+ = scgTerm e ((n, n) : vars) szs
480+ scgTerm _ _ _ = []
481+
482+ mkChange :: [(Name, (Name, SizeChange))] -> Term -> Maybe (Name, SizeChange)
483+ mkChange szs (P _ n ty) = case lookup n szs of
484+ Just (_, Unknown) -> Nothing
485+ t -> t
486+ mkChange _ _ = Nothing
437487
src/Idris/ElabDecls.hs+1−1
@@ -346,7 +346,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
346346 (CaseOp _ _ _ scargs sc scargs' sc' : _) ->
347347 do let calls = findCalls sc' scargs'
348348 let used = findUsedArgs sc' scargs'
349− let scg = buildSCG sc scargs
349+ let scg = buildSCG i sc scargs
350350 let cg = CGInfo scargs' calls scg used []
351351 logLvl 2 $ "Called names: " ++ show cg
352352 addToCG n cg