git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1079 from ahmadsalim/improvement/assert_smaller

Make assert_smaller : a -> b -> b

commit3c46202383815afa755724d849c99f90c21d6c58 authorEdwin Brady <edwin.brady@gmail.com> dateSun 20 Apr 2014, 16:30 (13 years ago) parent6d242db4be2fba
3 files changed+3−3
compare with master
unifiedsplit
libs/prelude/Builtins.idr+1−1 src/IRTS/Compiler.hs+1−1 src/Idris/Coverage.hs+1−1
libs/prelude/Builtins.idr+1−1
@@ -90,7 +90,7 @@ trace_malloc x = x -- compiled specially
9090||| x (which is typically a pattern argument)
9191||| @ x the larger value (typically a pattern argument)
9292||| @ y the smaller value (typically an argument to a recursive call)
93−assert_smaller : (x, y : a) -> a
93+assert_smaller : (x : a) -> (y : b) -> b
9494assert_smaller x y = y
9595
9696||| Assert to the totality checker than the given expression will always
src/IRTS/Compiler.hs+1−1
@@ -221,7 +221,7 @@ irTerm vs env tm@(App f a) = case unApply tm of
221221 | l == txt "Force"
222222 -> LForce <$> irTerm vs env arg
223223
224− (P _ (UN a) _, [_, _, arg])
224+ (P _ (UN a) _, [_, _, _, arg])
225225 | a == txt "assert_smaller"
226226 -> irTerm vs env arg
227227
src/Idris/Coverage.hs+1−1
@@ -517,7 +517,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
517517 -- find which argument in pargs <a> is smaller than, if any
518518 checkSize a (p : ps) i
519519 | a == p = Just (i, Same)
520− | (P _ (UN as) _, [_,arg,_]) <- unApply a,
520+ | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
521521 as == txt "assert_smaller" && arg == p
522522 = Just (i, Smaller)
523523 | smaller Nothing a (p, Nothing) = Just (i, Smaller)