9e350ac · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Inline assert_smaller correctly

Also add to CHANGELOG

commit9e350ac6faf13666e14761561c99ef5a21d46e6b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 1 Feb 2014, 22:59 (13 years ago) parentff819b4

2 files changed+5−1

unifiedsplit

CHANGELOG+4

@@ -18,6 +18,10 @@ New in 0.9.11:

1818 when disambiguating overloaded names. For example, it is possible to

1919 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",

2020 because the Vect constructors are defined in a namespace called Vect.

21+* assert_smaller internal function, which marks an expression as smaller than

22+ a pattern for use in totality checking.

23+ e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be

24+ structurally smaller than "(x :: xs)"

2125

2226Internal changes

2327

src/IRTS/Compiler.hs+1−1

@@ -182,7 +182,7 @@ instance ToIR (TT Name) where

182182 l == txt "lazy"

183183 = do arg' <- ir' env arg

184184 return $ LLazyExp arg'

185− | (P _ (UN a) _, [_, _, _, arg]) <- unApply tm,

185+ | (P _ (UN a) _, [_, _, arg]) <- unApply tm,

186186 a == txt "assert_smaller"

187187 = ir' env arg

188188 | (P _ (UN p) _, [_, arg]) <- unApply tm,