ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Totality checker improvements (soundness)

Browse Source 
When spotting a cycle, need to check that the decreasing argument
is in the same position.

For the moment, this means we can't spot decreasing arguments which
change position across multiple calls - but soundness is more
important!
This commit is contained in:
Edwin Brady 2013-11-27 19:51:21 +00:00
parent ec3daa4a07
commit 58a12c1595
9 changed files with 65 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libs/prelude/Prelude/List.idr
View File

@ -58,10 +58,10 @@ last (x::y::ys) p = last (y::ys) refl
last' : (l : List a) -> Maybe a
last' [] = Nothing
last' (x::xs) =
last' (x::xs) =
case xs of
[] => Just x
y::ys => last' xs
[] => Just x
y :: ys => last' xs
init : (l : List a) -> (isCons l = True) -> List a
init [] refl impossible

19
src/Idris/Coverage.hs
View File

@ -630,12 +630,12 @@ checkMP ist i mp = if i > 0
= let res = tryPath d path mp arg in
trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality
tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
tryPath desc path [] _ = Total []
-- tryPath desc path ((UN "believe_me", _) : _) arg
-- = Partial BelieveMe
-- if we get to a constructor, it's fine as long as it's strictly positive
tryPath desc path ((f, _) :es) arg
tryPath desc path ((f, _) : es) arg
| [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)
= case lookupTotal f (tt_ctxt ist) of
[Total _] -> Unchecked -- okay so far
@ -646,12 +646,15 @@ checkMP ist i mp = if i > 0
tryPath desc path (e@(f, args) : es) arg
| e `elem` es && allNothing args = Partial (Mutual [f])
tryPath desc path (e@(f, nextargs) : es) arg
| Just d <- lookup e path
| Just d <- lookup (e, arg) path
= if desc > 0
then -- trace ("Descent " ++ show (desc - d) ++ " "
-- ++ show (path, e)) $
Total []
else Partial (Mutual (map (fst . fst) path ++ [f]))
else Partial (Mutual (map (fst . fst . fst) path ++ [f]))
| e `elem` map (fst . fst) path
&& not (f `elem` map fst es)
= Partial (Mutual (map (fst . fst . fst) path ++ [f]))
| [Unchecked] <- lookupTotal f (tt_ctxt ist) =
let argspos = case collapseNothing (zip nextargs [0..]) of
[] -> [(Nothing, 0)]
@ -664,24 +667,24 @@ checkMP ist i mp = if i > 0
-- rest definitely terminates without
-- any cycles with route so far,
-- then we might yet be total
case collapse (map (tryPath (-10000) ((e, 0):path) es)
case collapse (map (tryPath 0 (((e, arg), 0):path) es)
[0..length nextargs - 1]) of
Total _ -> return Unchecked
x -> return x
Just (nextarg, sc) ->
if nextarg == arg then
case sc of
Same -> return $ tryPath desc ((e, desc) : path)
Same -> return $ tryPath desc (((e, arg), desc) : path)
es pos
Smaller -> return $ tryPath (desc+1)
((e, desc):path)
(((e, arg), desc) : path)
es
pos
_ -> trace ("Shouldn't happen " ++ show e) $
return (Partial Itself)
else return Unchecked in
-- trace (show (desc, argspos, path, es, pathres)) $
collapse' Unchecked pathres
collapse' Unchecked pathres
| [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
| [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

5
src/Idris/ElabDecls.hs
View File

@ -705,7 +705,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
pdef pdef pdef_inl pdef' ty)
addIBC (IBCDef n)
setTotality n tot
when (not reflect) $ totcheck (fc, n)
when (not reflect) $ do totcheck (fc, n)
defer_totcheck (fc, n)
when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
i <- getIState
case lookupDef n (tt_ctxt i) of
@ -1006,8 +1007,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
addDeferred def''
when (not (null def')) $ do
-- check these at the end, when definitions are complete
defer_totcheck (fc, fname)
mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')
-- Now the remaining deferred (i.e. no type declarations) clauses

2
test/reg006/run
View File

@ -1,3 +1,3 @@
#!/usr/bin/env bash
idris $@ reg006.idr -o reg006
idris $@ reg006.idr --check
rm -f *.ibc

2
test/reg028/expected Normal file
View File

@ -0,0 +1,2 @@
reg028.idr:5:1:tbad.bad is possibly not total due to: {tbad.bad12}
reg028a.idr:11:1:tbad.qsort' is possibly not total due to: {tbad.qsort'14}

8
test/reg028/reg028.idr Normal file
View File

@ -0,0 +1,8 @@
module tbad
total
bad : Nat -> Nat
bad Z = Z
bad (S m) with (succ m)
bad _ | j = bad j

25
test/reg028/reg028a.idr Normal file
View File

@ -0,0 +1,25 @@
module tbad
partial
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x::xs) with (partition (<x) xs)
qsort (x::xs) | (ys, zs) = qsort ys ++ [x] ++ qsort zs
total
qsort' : Ord a => List a -> List a
qsort' [] = []
qsort' (x::xs) with (partition (<x) xs)
qsort' (x::xs) | (ys, zs) = ?qsortLemma
---------- Proofs ----------
qsortLemma = proof
intros
let ys' = qsort' ys
let zs' = qsort' zs
let ws = ys' ++ [x] ++ zs'
trivial

4
test/reg028/run Executable file
View File

@ -0,0 +1,4 @@
#!/usr/bin/env bash
idris $@ reg028.idr --check
idris $@ reg028a.idr --check
rm -f *.ibc

16
test/test017/test017.idr
View File

@ -20,14 +20,16 @@ ordElim (Suc o) P mZ mSuc mSup = mSuc o (ordElim o P mZ mSuc mSup)
ordElim (Sup f) P mZ mSuc mSup =
mSup f (\n => ordElim (f n) P mZ mSuc mSup)
myplus' : Nat -> Nat -> Nat
myplus : Nat -> Nat -> Nat
-- For now, not going to support this
myplus Z y = y
myplus (S k) y = S (myplus' k y)
myplus' Z y = y
myplus' (S k) y = S (myplus y k)
-- myplus' : Nat -> Nat -> Nat
-- myplus : Nat -> Nat -> Nat
--
-- myplus Z y = y
-- myplus (S k) y = S (myplus' k y)
--
-- myplus' Z y = y
-- myplus' (S k) y = S (myplus y k)
mnubBy : (a -> a -> Bool) -> List a -> List a
mnubBy = nubBy' []