From b3c186900c5122e032a2e34d513909a52149be78 Mon Sep 17 00:00:00 2001 From: Justus Matthiesen Date: Tue, 17 Oct 2023 19:00:46 +0100 Subject: [PATCH] [ fix #2954 ] use matrices to represent sc-graphs We also update sc-graph generation to - fully traverse `As` patterns - go under `Dotted` patterns - consider `f x <= f` --- src/Core/Binary.idr | 2 +- src/Core/Context/Context.idr | 4 +- src/Core/TTC.idr | 3 +- src/Core/Termination/CallGraph.idr | 187 ++++++++++++++-------------- src/Core/Termination/SizeChange.idr | 185 +++++++++++++-------------- src/Idris/REPL.idr | 10 +- 6 files changed, 197 insertions(+), 194 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 518350166..bd9a4e4ce 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -29,7 +29,7 @@ import public Libraries.Utils.Binary ||| version number if you're changing the version more than once in the same day. export ttcVersion : Int -ttcVersion = 2023_09_04_00 +ttcVersion = 2023_09_08_00 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Context/Context.idr b/src/Core/Context/Context.idr index bea139cde..6abf0e08f 100644 --- a/src/Core/Context/Context.idr +++ b/src/Core/Context/Context.idr @@ -11,12 +11,14 @@ import public Algebra.SizeChange import Data.IORef import Data.String +import Data.List1 import Libraries.Data.IntMap import Libraries.Data.IOArray import Libraries.Data.NameMap import Libraries.Data.UserNameMap import Libraries.Data.WithDefault +import Libraries.Data.SparseMatrix import Libraries.Utils.Binary import Libraries.Utils.Scheme @@ -266,7 +268,7 @@ public export record SCCall where constructor MkSCCall fnCall : Name -- Function called - fnArgs : List (Maybe (Nat, SizeChange)) + fnArgs : Matrix SizeChange -- relationship to arguments of calling function; argument position -- (in the calling function), and how its size changed in the call. -- 'Nothing' if it's not related to any of the calling function's diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 186527939..2d7e912b3 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -11,10 +11,11 @@ import Core.Name import Core.Options import Core.TT - +import Data.List1 import Data.Vect import Libraries.Data.NameMap import Libraries.Data.IOArray +import Libraries.Data.SparseMatrix import Libraries.Data.WithDefault import Libraries.Utils.Binary diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr index 1f92096b8..27b74f985 100644 --- a/src/Core/Termination/CallGraph.idr +++ b/src/Core/Termination/CallGraph.idr @@ -6,6 +6,8 @@ import Core.Env import Core.Normalise import Core.Value +import Libraries.Data.SparseMatrix + import Data.String %default covering @@ -18,24 +20,26 @@ Show Guardedness where show Guarded = "Guarded" show InDelay = "InDelay" --- Equal for the purposes of size change means, ignoring as patterns, all --- non-metavariable positions are equal -scEq : Term vars -> Term vars -> Bool -scEq (Local _ _ idx _) (Local _ _ idx' _) = idx == idx' -scEq (Ref _ _ n) (Ref _ _ n') = n == n' -scEq (Meta _ _ i args) _ = True -scEq _ (Meta _ _ i args) = True -scEq (Bind _ _ b sc) (Bind _ _ b' sc') = False -- not checkable -scEq (App _ f a) (App _ f' a') = scEq f f' && scEq a a' -scEq (As _ _ a p) p' = scEq p p' -scEq p (As _ _ a p') = scEq p p' -scEq (TDelayed _ _ t) (TDelayed _ _ t') = scEq t t' -scEq (TDelay _ _ t x) (TDelay _ _ t' x') = scEq t t' && scEq x x' -scEq (TForce _ _ t) (TForce _ _ t') = scEq t t' -scEq (PrimVal _ c) (PrimVal _ c') = c == c' -scEq (Erased _ _) (Erased _ _) = True -scEq (TType _ _) (TType _ _) = True -scEq _ _ = False +sizeEq : Term vars -> -- RHS + Term vars -> -- LHS: may contain dot-patterns, try both sides of as patterns + Bool +sizeEq (Local _ _ idx _) (Local _ _ idx' _) = idx == idx' +sizeEq (Ref _ _ n) (Ref _ _ n') = n == n' +sizeEq (Meta _ _ i args) (Meta _ _ i' args') + = i == i' && assert_total (all (uncurry sizeEq) (zip args args')) +sizeEq (Bind _ _ b sc) (Bind _ _ b' sc') = eqBinderBy sizeEq b b' && sizeEq sc (believe_me sc') +sizeEq (App _ f a) (App _ f' a') = sizeEq f f' && sizeEq a a' +sizeEq (As _ _ a p) p' = sizeEq p p' +sizeEq p (As _ _ a p') = sizeEq p a || sizeEq p p' +sizeEq (TDelayed _ _ t) (TDelayed _ _ t') = sizeEq t t' +sizeEq (TDelay _ _ t x) (TDelay _ _ t' x') = sizeEq t t' && sizeEq x x' +sizeEq (TForce _ _ t) (TForce _ _ t') = sizeEq t t' +sizeEq (PrimVal _ c) (PrimVal _ c') = c == c' +-- traverse dotted LHS terms +sizeEq t (Erased _ (Dotted t')) = sizeEq t t' +sizeEq (Erased _ i) (Erased _ i') = i == i' +sizeEq (TType _ _) (TType _ _) = True +sizeEq _ _ = False -- Remove all force and delay annotations which are nothing to do with -- coinduction meaning that all Delays left guard coinductive calls. @@ -66,13 +70,13 @@ mutual findSC : {vars : _} -> {auto c : Ref Ctxt Defs} -> Defs -> Env Term vars -> Guardedness -> - List (Nat, Term vars) -> -- LHS args and their position - Term vars -> -- Right hand side + List (Term vars) -> -- LHS args + Term vars -> -- RHS Core (List SCCall) findSC {vars} defs env g pats (Bind fc n b sc) = pure $ !(findSCbinder b) ++ - !(findSC defs (b :: env) g (map (\ (p, tm) => (p, weaken tm)) pats) sc) + !(findSC defs (b :: env) g (map weaken pats) sc) where findSCbinder : Binder (Term vars) -> Core (List SCCall) findSCbinder (Let _ c val ty) = findSC defs env g pats val @@ -104,25 +108,22 @@ mutual do Just ty <- lookupTyExact cn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Guarded pats fc cn 0 args - arity <- getArity defs [] ty - findSCcall defs env Guarded pats fc cn arity args + findSCcall defs env Guarded pats fc cn args + findSCcall defs env Guarded pats fc cn args (Toplevel, Ref fc (DataCon _ _) cn, args) => do Just ty <- lookupTyExact cn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Guarded pats fc cn 0 args - arity <- getArity defs [] ty - findSCcall defs env Guarded pats fc cn arity args + findSCcall defs env Guarded pats fc cn args + findSCcall defs env Guarded pats fc cn args (_, Ref fc Func fn, args) => do logC "totality" 50 $ pure $ "Looking up type of " ++ show !(toFullNames fn) Just ty <- lookupTyExact fn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Unguarded pats fc fn 0 args - arity <- getArity defs [] ty - findSCcall defs env Unguarded pats fc fn arity args + findSCcall defs env Unguarded pats fc fn args + findSCcall defs env Unguarded pats fc fn args (_, f, args) => do scs <- traverse (findSC defs env Unguarded pats) args pure (concat scs) @@ -131,7 +132,7 @@ mutual handleCase (Ref fc nt n) args = do n' <- toFullNames n if caseFn n' - then Just <$> findSCcall defs env g pats fc n 4 args + then Just <$> findSCcall defs env g pats fc n args else pure Nothing handleCase _ _ = pure Nothing @@ -145,49 +146,56 @@ mutual else pure $ Ref fc Func n conIfGuarded tm = pure tm - -- Expand the size change argument list with 'Nothing' to match the given - -- arity (i.e. the arity of the function we're calling) to ensure that - -- it's noted that we don't know the size change relationship with the - -- extra arguments. - expandToArity : Nat -> List (Maybe (Nat, SizeChange)) -> - List (Maybe (Nat, SizeChange)) - expandToArity Z xs = xs - expandToArity (S k) (x :: xs) = x :: expandToArity k xs - expandToArity (S k) [] = Nothing :: expandToArity k [] + knownOr : SizeChange -> Lazy SizeChange -> SizeChange + knownOr Unknown y = y + knownOr x _ = x + + plusLazy : SizeChange -> Lazy SizeChange -> SizeChange + plusLazy Smaller _ = Smaller + plusLazy x y = x |+| y -- Return whether first argument is structurally smaller than the second. - smaller : Bool -> -- Have we gone under a constructor yet? - Defs -> - Maybe (Term vars) -> -- Asserted bigger thing - Term vars -> -- Term we're checking - Term vars -> -- Argument it might be smaller than - Bool - smaller inc defs big _ (Erased _ _) = False -- Never smaller than an erased thing! + sizeCompare : Term vars -> -- RHS: term we're checking + Term vars -> -- LHS: argument it might be smaller than + SizeChange + + sizeCompareCon : Term vars -> Term vars -> Bool + sizeCompareConArgs : Term vars -> List (Term vars) -> Bool + sizeCompareApp : Term vars -> Term vars -> SizeChange + + sizeCompare s (Erased _ (Dotted t)) = sizeCompare s t + sizeCompare _ (Erased _ _) = Unknown -- incomparable! -- for an as pattern, it's smaller if it's smaller than either part - smaller inc defs big s (As _ _ p t) - = smaller inc defs big s p || smaller inc defs big s t - smaller True defs big s t - = s == t || smallerArg True defs big s t - smaller inc defs big s t = smallerArg inc defs big s t + sizeCompare s (As _ _ p t) + = knownOr (sizeCompare s p) (sizeCompare s t) + sizeCompare (As _ _ p s) t + = knownOr (sizeCompare p t) (sizeCompare s t) + sizeCompare s t + = if sizeCompareCon s t + then Smaller + else knownOr (sizeCompareApp s t) (if sizeEq s t then Same else Unknown) - assertedSmaller : Maybe (Term vars) -> Term vars -> Bool - assertedSmaller (Just b) a = scEq b a - assertedSmaller _ _ = False + sizeCompareCon s t + = let (f, args) = getFnArgs t in + case f of + Ref _ (DataCon t a) cn => sizeCompareConArgs s args + _ => False - smallerArg : Bool -> Defs -> - Maybe (Term vars) -> Term vars -> Term vars -> Bool - smallerArg inc defs big (As _ _ _ s) tm = smallerArg inc defs big s tm - smallerArg inc defs big s tm - -- If we hit a pattern that is equal to a thing we've asserted_smaller, - -- the argument must be smaller - = assertedSmaller big tm || - case getFnArgs tm of - (Ref _ (DataCon t a) cn, args) - => any (smaller True defs big s) args - _ => case s of - App _ f _ => smaller inc defs big f tm - -- Higher order recursive argument - _ => False + sizeCompareConArgs s [] = False + sizeCompareConArgs s (t :: ts) + = case sizeCompare s t of + Unknown => sizeCompareConArgs s ts + _ => True + + sizeCompareApp (App _ f _) t = sizeCompare f t + sizeCompareApp _ t = Unknown + + sizeCompareAsserted : Maybe (Term vars) -> Term vars -> SizeChange + sizeCompareAsserted (Just s) t + = case sizeCompare s t of + Unknown => Unknown + _ => Smaller + sizeCompareAsserted Nothing _ = Unknown -- if the argument is an 'assert_smaller', return the thing it's smaller than asserted : Name -> Term vars -> Maybe (Term vars) @@ -204,16 +212,11 @@ mutual -- in 'pats'; the position in 'pats' and the size change. -- Nothing if there is no relation with any of them. mkChange : Defs -> Name -> - (pats : List (Nat, Term vars)) -> + (pats : List (Term vars)) -> (arg : Term vars) -> - Maybe (Nat, SizeChange) - mkChange defs aSmaller [] arg = Nothing - mkChange defs aSmaller ((i, As _ _ p parg) :: pats) arg - = mkChange defs aSmaller ((i, p) :: (i, parg) :: pats) arg - mkChange defs aSmaller ((i, parg) :: pats) arg - = cond [(scEq arg parg, Just (i, Same)), - (smaller False defs (asserted aSmaller arg) arg parg, Just (i, Smaller))] - (mkChange defs aSmaller pats arg) + List SizeChange + mkChange defs aSmaller pats arg + = map (\p => plusLazy (sizeCompareAsserted (asserted aSmaller arg) p) (sizeCompare arg p)) pats -- Given a name of a case function, and a list of the arguments being -- passed to it, update the pattern list so that it's referring to the LHS @@ -222,10 +225,11 @@ mutual -- rather than treating the definitions separately. getCasePats : {auto c : Ref Ctxt Defs} -> {vars : _} -> - Defs -> Name -> List (Nat, Term vars) -> + Defs -> Name -> List (Term vars) -> List (Term vars) -> Core (Maybe (List (vs ** (Env Term vs, - List (Nat, Term vs), Term vs)))) + List (Term vs), Term vs)))) + getCasePats {vars} defs n pats args = do Just (PMDef _ _ _ _ pdefs) <- lookupDefExact n (gamma defs) | _ => pure Nothing @@ -238,7 +242,7 @@ mutual rhs <- toFullNames rhs pure $ " " ++ show lhs ++ " => " ++ show rhs new <- for pdefs' $ \ (_ ** (_, lhs, rhs)) => do - lhs <- traverse (toFullNames . snd) lhs + lhs <- traverse toFullNames lhs rhs <- toFullNames rhs pure $ " " ++ show lhs ++ " => " ++ show rhs pure $ unlines $ "Updated" :: old ++ " to:" :: new @@ -288,11 +292,11 @@ mutual else lookupTm tm tms updatePat : {vs, vs' : _} -> - List (Term vs, Term vs') -> (Nat, Term vs) -> (Nat, Term vs') - updatePat ms (n, tm) = (n, updateRHS ms tm) + List (Term vs, Term vs') -> Term vs -> Term vs' + updatePat ms tm = updateRHS ms tm matchArgs : (vs ** (Env Term vs, Term vs, Term vs)) -> - (vs ** (Env Term vs, List (Nat, Term vs), Term vs)) + (vs ** (Env Term vs, List (Term vs), Term vs)) matchArgs (_ ** (env', lhs, rhs)) = let patMatch = reverse (zip args (getArgs lhs)) in (_ ** (env', map (updatePat patMatch) pats, rhs)) @@ -300,10 +304,10 @@ mutual findSCcall : {vars : _} -> {auto c : Ref Ctxt Defs} -> Defs -> Env Term vars -> Guardedness -> - List (Nat, Term vars) -> - FC -> Name -> Nat -> List (Term vars) -> + List (Term vars) -> + FC -> Name -> List (Term vars) -> Core (List SCCall) - findSCcall defs env g pats fc fn_in arity args + findSCcall defs env g pats fc fn_in args -- Under 'assert_total' we assume that all calls are fine, so leave -- the size change list empty = do fn <- getFullName fn_in @@ -318,18 +322,18 @@ mutual ] (do scs <- traverse (findSC defs env g pats) args pure ([MkSCCall fn - (expandToArity arity + (fromListList (map (mkChange defs aSmaller pats) args)) fc] ++ concat scs)) findInCase : {auto c : Ref Ctxt Defs} -> Defs -> Guardedness -> - (vs ** (Env Term vs, List (Nat, Term vs), Term vs)) -> + (vs ** (Env Term vs, List (Term vs), Term vs)) -> Core (List SCCall) findInCase defs g (_ ** (env, pats, tm)) = do logC "totality" 10 $ - do ps <- traverse toFullNames (map snd pats) + do ps <- traverse toFullNames pats pure ("Looking in case args " ++ show ps) logTermNF "totality" 10 " =" env tm rhs <- normaliseOpts tcOnly defs env tm @@ -341,8 +345,7 @@ findCalls : {auto c : Ref Ctxt Defs} -> findCalls defs (_ ** (env, lhs, rhs_in)) = do let pargs = getArgs (delazy defs lhs) rhs <- normaliseOpts tcOnly defs env rhs_in - findSC defs env Toplevel - (zip (take (length pargs) [0..]) pargs) (delazy defs rhs) + findSC defs env Toplevel pargs (delazy defs rhs) getSC : {auto c : Ref Ctxt Defs} -> Defs -> Def -> Core (List SCCall) diff --git a/src/Core/Termination/SizeChange.idr b/src/Core/Termination/SizeChange.idr index 8d14222f9..898f0edfe 100644 --- a/src/Core/Termination/SizeChange.idr +++ b/src/Core/Termination/SizeChange.idr @@ -10,6 +10,12 @@ import Libraries.Data.NameMap import Libraries.Data.SortedMap import Libraries.Data.SortedSet +import Libraries.Data.SparseMatrix + +import Data.Nat +import Data.List +import Data.List1 + %default covering -- Based on: @@ -28,55 +34,55 @@ Arg : Type Arg = Nat ||| A change in (g y₀ ⋯ yₙ) with respect to (f x₀ ⋯ xₙ) is -||| for each argument yᵢ in g either: -||| Nothing if it's not related to any of the xⱼ -||| Just (j, rel) if yᵢ `rel` xⱼ +||| for argument yᵢ in g and xⱼ in f: +||| Smaller if yᵢ < xⱼ +||| Equal if yᵢ <= xⱼ +||| Unknown if yᵢ is not related to xⱼ Change : {- f g -} Type -Change = List (Maybe (Arg, SizeChange)) +Change = Matrix SizeChange -||| A path in the call graph lists the source location of the successive calls -||| and the name of each of the functions being called +||| A sequence in the call graph lists the source location of the successive +||| calls and the name of each of the functions being called ||| TODO: also record the arguments so that we can print e.g. ||| flip x y -> flop y x -> flip x y ||| instead of the less useful ||| flip -> flop -> flip public export -Path : {- f g -} Type -Path = List (FC, Name) +CallSeq : {- f g -} Type +CallSeq = List (FC, Name) -||| An arg change in g with respect to f is given by: +||| An edge from f to g is given by: ||| the actual changes in g with respect to f -||| the path in the call graph leading from f to g +||| the sequence in the call graph leading from f to g ||| The path is only here for error-reporting purposes -record ArgChange {- f g -} where - constructor MkArgChange +record Graph {- f g -} where + constructor MkGraph change : Change {- f g -} - path : Path {- f g -} + seq : CallSeq {- f g -} ||| Sc graphs to be added WorkList : Type -WorkList = SortedSet (Name, Name, ArgChange) +WorkList = SortedSet (Name, Name, Graph) ||| Transitively-closed (modulo work list) set of sc-graphs ||| Note: oh if only we had dependent name maps! SCSet : Type SCSet = NameMap {- \ f => -} $ NameMap {- \ g => -} - $ SortedSet $ ArgChange {- f g -} - + $ SortedSet $ Graph {- f g -} ------------------------------------------------------------------------ -- Instances --- ignore path -Eq ArgChange where +-- ignore call sequence +Eq Graph where (==) a1 a2 = a1.change == a2.change -Ord ArgChange where +Ord Graph where compare a1 a2 = compare a1.change a2.change -Show ArgChange where - show a = show a.change ++ " @" ++ show a.path +Show Graph where + show a = show a.change ++ "\n via call seq: " ++ show a.seq ++ "\n" ------------------------------------------------------------------------ -- Utility functions @@ -91,7 +97,7 @@ lookupMap n m = fromMaybe empty (lookup n m) lookupSet : Ord v => Name -> NameMap (SortedSet v) -> SortedSet v lookupSet n m = fromMaybe empty (lookup n m) -lookupGraphs : Name -> Name -> SCSet -> SortedSet ArgChange +lookupGraphs : Name -> Name -> SCSet -> SortedSet Graph lookupGraphs f g = lookupSet g . lookupMap f ||| Smart filter: only keep the paths starting from f @@ -102,7 +108,7 @@ selectDom f s = insert f (lookupMap f s) empty selectCod : Name -> SCSet -> SCSet selectCod g s = map (\m => insert g (lookupSet g m) empty) s -foldl : (acc -> Name -> Name -> ArgChange -> acc) -> acc -> SCSet -> acc +foldl : (acc -> Name -> Name -> Graph -> acc) -> acc -> SCSet -> acc foldl f_acc acc = foldlNames (\acc, f => foldlNames (\acc, g => @@ -110,7 +116,7 @@ foldl f_acc acc acc) acc -insertGraph : (f, g : Name) -> ArgChange {- f g -} -> SCSet -> SCSet +insertGraph : (f, g : Name) -> Graph {- f g -} -> SCSet -> SCSet insertGraph f g ch s = let s_f = lookupMap f s in let s_fg = lookupSet g s_f in @@ -122,48 +128,39 @@ insertGraph f g ch s ||| Diagrammatic composition: ||| Given a (Change f g) and a (Change g h), compute a (Change f h) composeChange : Change {- f g -} -> Change {- g h -} -> Change {- f h -} -composeChange c1 c2 - -- We have (giving more precise types) - -- h z₀ ⋯ zₚ, g y₀ ⋯ yₙ, f x₀ ⋯ xₘ - -- c1 : Vect n (Maybe (Fin m, SizeChange)) - -- c2 : Vect p (Maybe (Fin n, SizeChange)) - -- and we want - -- Vect p (Maybe (Fin m, SizeChange)) +composeChange -- We use the SizeChange monoid: Unknown is a 0, Same is a neutral - = map (>>= (\(i, r) => map (r <+>) <$> getArg i c1)) c2 - where - getArg : Nat -> List (Maybe a) -> Maybe a - getArg i c = join $ getAt i c + = mult ||| Diagrammatic composition: -||| Given an (ArgChange f g) and an (ArgChange g h), compute an (ArgChange f h) -composeArgChange : ArgChange {- f g -} -> ArgChange {- g h -} -> ArgChange {- f h -} -composeArgChange a1 a2 - = MkArgChange +||| Given an (Graph f g) and an (Graph g h), compute an (Graph f h) +composeGraph : Graph {- f g -} -> Graph {- g h -} -> Graph {- f h -} +composeGraph a1 a2 + = MkGraph (composeChange a1.change a2.change) - (a1.path ++ a2.path) + (a1.seq ++ a2.seq) -||| Precompose a given Arg change & insert it in the worklist (unless it's already known) -preCompose : (f : Name) -> ArgChange {- f g -} -> -- /!\ g bound later +||| Precompose a give an sc-graph & insert it in the worklist (unless it's already known) +preCompose : (f : Name) -> Graph {- f g -} -> -- /!\ g bound later SCSet -> WorkList -> - (g : Name) -> (h : Name) -> ArgChange {- g h -} -> + (g : Name) -> (h : Name) -> Graph {- g h -} -> WorkList preCompose f ch1 s work _ h ch2 - = let ch : ArgChange {- f h -} = composeArgChange ch1 ch2 in + = let ch : Graph {- f h -} = composeGraph ch1 ch2 in if contains ch (lookupGraphs f h s) then work else insert (f, h, ch) work ||| Precompose a given Arg change & insert it in the worklist (unless it's already known) -postCompose : (h : Name) -> ArgChange {- g h -} -> -- /!\ g bound later +postCompose : (h : Name) -> Graph {- g h -} -> -- /!\ g bound later SCSet -> WorkList -> - (f : Name) -> (g : Name) -> ArgChange {- f g -} -> + (f : Name) -> (g : Name) -> Graph {- f g -} -> WorkList postCompose h ch2 s work f _ ch1 - = let ch : ArgChange {- f h -} = composeArgChange ch1 ch2 in + = let ch : Graph {- f h -} = composeGraph ch1 ch2 in if contains ch (lookupGraphs f h s) then work else @@ -171,13 +168,13 @@ postCompose h ch2 s work f _ ch1 mutual addGraph : {auto c : Ref Ctxt Defs} -> - (f, g : Name) -> ArgChange {- f g -} -> + (f, g : Name) -> Graph {- f g -} -> WorkList -> SCSet -> SCSet addGraph f g ch work s_in = let s = insertGraph f g ch s_in - -- Now that (ch : ArgChange f g) has been added, we need to update + -- Now that (ch : Graph f g) has been added, we need to update -- the graph with the paths it has extended i.e. -- the ones start in g @@ -202,55 +199,51 @@ mutual addGraph f g ch work s -- find (potential) chain of calls to given function (inclusive) -prefixPath : NameMap (FC, Name) -> (g : Name) -> {- Exists \ f => -} Path {- f g -} -prefixPath pred g = go g [] +prefixCallSeq : NameMap (FC, Name) -> (g : Name) -> {- Exists \ f => -} CallSeq {- f g -} +prefixCallSeq pred g = go g [] where - go : Name -> Path -> Path - go g path + go : Name -> CallSeq -> CallSeq + go g seq = let Just (l, f) = lookup g pred - | Nothing => path in + | Nothing => seq in if f == g then -- we've reached the entry point! - path + seq else - go f ((l, g) :: path) + go f ((l, g) :: seq) --- returns `Just a.path` iff there is no self-decreasing edge, +-- returns `Just a.seq` iff there is no self-decreasing arc, -- i.e. there is no argument `n` with `index n a.change === (n, Smaller)` -checkNonDesc : ArgChange -> Maybe Path -checkNonDesc a = go Z a.change +checkNonDesc : Graph -> Maybe Graph +checkNonDesc a = if any selfDecArc a.change then Nothing else Just a where - go : Nat -> Change -> Maybe Path - go _ [] = Just a.path - go n (Just (k, Smaller) :: xs) = if n == k then Nothing else go (S n) xs - go n (_ :: xs) = go (S n) xs + selfDecArc : (Nat, Vector1 SizeChange) -> Bool + selfDecArc (i, xs) = lookupOrd1 i xs == Just Smaller ||| Finding non-terminating loops -findLoops : {auto c : Ref Ctxt Defs} -> SCSet -> - Core (NameMap {- $ \ f => -} (Maybe (Path {- f f -} ))) +findLoops : SCSet -> + NameMap {- $ \ f => -} (Maybe (Graph {- f f -} )) findLoops s - = do -- Comparing (f x₀ ⋯ xₙ) with (f xᵧ₍₀₎ ⋯ xᵧ₍ₙ₎) for size changes only makes - -- sense if the position for we can say something are stable under γ. - -- Hence the following filter: - let loops = filterEndos (\a => composeChange a.change a.change == a.change) s - log "totality.termination.calc" 7 $ "Loops: " ++ show loops - let terms = map (foldMap checkNonDesc) loops - pure terms + = -- Comparing (f x₀ ⋯ xₙ) with (f xᵧ₍₀₎ ⋯ xᵧ₍ₙ₎) for size changes only makes + -- sense if the position for we can say something are stable under γ. + -- Hence the following filter: + let loops = filterEndos (\a => composeChange a.change a.change == a.change) s + terms = map (foldMap checkNonDesc) loops in + terms where - filterEndos : (ArgChange -> Bool) -> SCSet -> NameMap (List ArgChange) + filterEndos : (Graph -> Bool) -> SCSet -> NameMap (List Graph) filterEndos p = mapWithKey (\f, m => filter p (Data.SortedSet.toList (lookupSet f m))) - -findNonTerminatingLoop : {auto c : Ref Ctxt Defs} -> SCSet -> Core (Maybe (Name, Path)) -findNonTerminatingLoop s - = do loops <- findLoops s - pure $ findNonTerminating loops +findNonTerminatingLoop : SCSet -> Maybe (Name, Graph) +findNonTerminatingLoop s = findNonTerminating (findLoops s) where - findNonTerminating : NameMap (Maybe Path) -> Maybe (Name, Path) + -- select first non-terminating loop + -- TODO: find smallest + findNonTerminating : NameMap (Maybe Graph) -> Maybe (Name, Graph) findNonTerminating = foldlNames (\acc, g, m => map (g,) m <+> acc) empty -||| Steps in a path leading to a loop are also problematic +||| Steps in a call sequence leading to a loop are also problematic setPrefixTerminating : {auto c : Ref Ctxt Defs} -> - Path -> Name -> Core () + CallSeq -> Name -> Core () setPrefixTerminating [] g = pure () setPrefixTerminating (_ :: []) g = pure () setPrefixTerminating ((l, f) :: p) g @@ -266,29 +259,29 @@ addFunctions : {auto c : Ref Ctxt Defs} -> addFunctions defs [] pred work = pure $ Right (work, pred) addFunctions defs (d1 :: ds) pred work - = do log "totality.termination.calc" 8 $ "Adding function: " ++ show d1.fullname + = do logC "totality.termination.calc" 8 $ do pure "Adding function: \{show d1.fullname}" calls <- foldlC resolveCall [] d1.sizeChange let Nothing = find isNonTerminating calls | Just (d2, l, _) => do let g = d2.fullname - log "totality.termination.calc" 7 $ "Non-terminating function call: " ++ show g - let init = prefixPath pred d1.fullname ++ [(l, g)] + logC "totality.termination.calc" 7 $ do pure "Non-terminating function call: \{show g}" + let init = prefixCallSeq pred d1.fullname ++ [(l, g)] setPrefixTerminating init g pure $ Left (NotTerminating (BadPath init g)) let (ds, pred, work) = foldl addCall (ds, pred, work) (filter isUnchecked calls) addFunctions defs ds pred work where - resolveCall : List (GlobalDef, FC, (Name, Name, ArgChange)) -> + resolveCall : List (GlobalDef, FC, (Name, Name, Graph)) -> SCCall -> - Core (List (GlobalDef, FC, (Name, Name, ArgChange))) + Core (List (GlobalDef, FC, (Name, Name, Graph))) resolveCall calls (MkSCCall g ch l) = do Just d2 <- lookupCtxtExact g (gamma defs) - | Nothing => do log "totality.termination.calc" 7 $ "Not found: " ++ show g + | Nothing => do logC "totality.termination.calc" 7 $ do pure "Not found: \{show g}" pure calls - pure ((d2, l, (d1.fullname, d2.fullname, MkArgChange ch [(l, d2.fullname)])) :: calls) + pure ((d2, l, (d1.fullname, d2.fullname, MkGraph ch [(l, d2.fullname)])) :: calls) addCall : (List GlobalDef, NameMap (FC, Name), WorkList) -> - (GlobalDef, FC, (Name, Name, ArgChange)) -> + (GlobalDef, FC, (Name, Name, Graph)) -> (List GlobalDef, NameMap (FC, Name), WorkList) addCall (ds, pred, work_in) (d2, l, c) = let work = insert c work_in in @@ -323,18 +316,18 @@ calcTerminating loc n = do defs <- get Ctxt logC "totality.termination.calc" 7 $ do pure $ "Calculating termination: " ++ show !(toFullNames n) Just def <- lookupCtxtExact n (gamma defs) - | Nothing => undefinedName loc n + | Nothing => undefinedName loc n IsTerminating <- totRefs defs (nub !(addCases defs (keys (refersTo def)))) - | bad => pure bad + | bad => pure bad Right (work, pred) <- initWork defs def - | Left bad => pure bad + | Left bad => pure bad let s = transitiveClosure work initSCSet - Nothing <- findNonTerminatingLoop s + let Nothing = findNonTerminatingLoop s | Just (g, loop) => ifThenElse (def.fullname == g) - (pure $ NotTerminating (RecPath loop)) - (do setTerminating EmptyFC g (NotTerminating (RecPath loop)) - let init = prefixPath pred g + (pure $ NotTerminating (RecPath loop.seq)) + (do setTerminating EmptyFC g (NotTerminating (RecPath loop.seq)) + let init = prefixCallSeq pred g setPrefixTerminating init g pure $ NotTerminating (BadPath init g)) pure IsTerminating diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index e81487b4c..bcfa21ce3 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -69,6 +69,7 @@ import Libraries.Data.PosMap import Data.Stream import Data.String import Libraries.Data.List.Extra +import Libraries.Data.SparseMatrix import Libraries.Data.String.Extra import Libraries.Data.Tap import Libraries.Data.WithDefault @@ -132,7 +133,7 @@ prettyInfo (n, idx, d) , (\ nms => header "Refers to" <++> enum pretty0 nms) <$> ifNotNull referCT , (\ nms => header "Refers to (runtime)" <++> enum pretty0 nms) <$> ifNotNull referRT , (\ flgs => header "Flags" <++> enum byShow flgs) <$> ifNotNull (flags d) - , (\ sz => header "Size change" <++> displayChg sz) <$> ifNotNull schanges + , (\ sz => header "Size change" <+> hardline <+> indent 2 (displayChg sz)) <$> ifNotNull schanges ] where @@ -142,10 +143,13 @@ prettyInfo (n, idx, d) enum : (a -> Doc IdrisDocAnn) -> List a -> Doc IdrisDocAnn enum p xs = hsep $ punctuate "," $ p <$> xs + enumLine : (a -> Doc IdrisDocAnn) -> List a -> Doc IdrisDocAnn + enumLine p xs = hcat $ punctuate hardline $ p <$> xs + displayChg : List SCCall -> Doc IdrisDocAnn displayChg sz = - let scinfo = \s => pretty0 (fnCall s) <+> ":" <++> pretty0 (show $ fnArgs s) in - enum scinfo sz + let scinfo = \s => pretty0 (fnCall s) <+> ":" <+> hardline <+> cast (prettyTable 1 (fnArgs s)) in + enumLine scinfo sz getEnvTerm : {vars : _} -> List Name -> Env Term vars -> Term vars ->