git.iko.soy/Idris-dev
on master help sign in
Allow second argument of assert_smaller to be of different type than
4be2fbaAhmad Salim Al-Sibahi
libs/prelude/Builtins.idr+1−1
compare with master
unifiedsplit
@@ -90,7 +90,7 @@ trace_malloc x = x -- compiled specially
90||| x (which is typically a pattern argument)
90||| x (which is typically a pattern argument)
91||| @ x the larger value (typically a pattern argument)
91||| @ x the larger value (typically a pattern argument)
92||| @ y the smaller value (typically an argument to a recursive call)
92||| @ 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
94assert_smaller x y = y
94assert_smaller x y = y
95
95
96||| Assert to the totality checker than the given expression will always
96||| 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
221 | l == txt "Force"
221 | l == txt "Force"
222 -> LForce <$> irTerm vs env arg
222 -> LForce <$> irTerm vs env arg
223
223
224− (P _ (UN a) _, [_, _, arg])
224+ (P _ (UN a) _, [_, _, _, arg])
225 | a == txt "assert_smaller"
225 | a == txt "assert_smaller"
226 -> irTerm vs env arg
226 -> irTerm vs env arg
227
227
src/Idris/Coverage.hs+1−1
@@ -517,7 +517,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
517 -- find which argument in pargs <a> is smaller than, if any
517 -- find which argument in pargs <a> is smaller than, if any
518 checkSize a (p : ps) i
518 checkSize a (p : ps) i
519 | a == p = Just (i, Same)
519 | a == p = Just (i, Same)
520− | (P _ (UN as) _, [_,arg,_]) <- unApply a,
520+ | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,
521 as == txt "assert_smaller" && arg == p
521 as == txt "assert_smaller" && arg == p
522 = Just (i, Smaller)
522 = Just (i, Smaller)
523 | smaller Nothing a (p, Nothing) = Just (i, Smaller)
523 | smaller Nothing a (p, Nothing) = Just (i, Smaller)