4be2fba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow second argument of assert_smaller to be of different type than

first argument since this could be useful for functions that are written with Universe-style pattern matching, i.e., where the rhs pattern has different type than the lhs expression.

commit4be2fba22d070622fdd537271619eae39c9f8a57 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateFri 18 Apr 2014, 19:38 (13 years ago) parente07c13d

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)