idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 17:21:59 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #2954 ] use matrices to represent sc-graphs

Browse Source 
We also update sc-graph generation to
- fully traverse `As` patterns
- go under `Dotted` patterns
- consider `f x <= f`
This commit is contained in:
Justus Matthiesen 2023-10-17 19:00:46 +01:00 committed by Justus Matthiesen
parent c4677edc5f
commit b3c186900c
6 changed files with 197 additions and 194 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Binary.idr
View File

@ -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 ()

4
src/Core/Context/Context.idr
View File

@ -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

3
src/Core/TTC.idr
View File

@ -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

187
src/Core/Termination/CallGraph.idr
View File

@ -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)

185
src/Core/Termination/SizeChange.idr
View File

@ -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

10
src/Idris/REPL.idr
View File

@ -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 ->