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

[ refactor ] renamed checkDesc to checkNonDesc

Browse Source
This commit is contained in:
Justus Matthiesen 2023-04-23 13:21:47 +01:00 committed by Justus Matthiesen
parent 1d3bad7c0e
commit 360232de35
1 changed files with 11 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -214,6 +214,16 @@ prefixPath pred g = go g []
else
go f ((l, g) :: path)
-- returns `Just a.path` iff there is no self-decreasing edge,
-- i.e. there is no argument `n` with `index n a.change === (n, Smaller)`
checkNonDesc : ArgChange -> Maybe Path
checkNonDesc a = go Z a.change
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
||| Finding non-terminating loops
findLoops : {auto c : Ref Ctxt Defs} -> SCSet ->
Core (NameMap {- $ \ f => -} (Maybe (Path {- f f -} )))
@ -223,16 +233,12 @@ findLoops s
-- 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 (\a => checkDesc Z a.change a.path)) loops
let terms = map (foldMap checkNonDesc) loops
pure terms
where
filterEndos : (ArgChange -> Bool) -> SCSet -> NameMap (List ArgChange)
filterEndos p = mapWithKey (\f, m => filter p (Data.SortedSet.toList (lookupSet f m)))
checkDesc : Nat -> Change -> Path -> Maybe Path
checkDesc _ [] p = Just p
checkDesc n (Just (k, Smaller) :: xs) p = if n == k then Nothing else checkDesc (S n) xs p
checkDesc n (_ :: xs) p = checkDesc (S n) xs p
findNonTerminatingLoop : {auto c : Ref Ctxt Defs} -> SCSet -> Core (Maybe (Name, Path))
findNonTerminatingLoop s