At Mon, 23 Aug 2010 17:58:41 -0700, Neil Toronto wrote: > It's fun to open the macro stepper and see "unsafe" scattered > everywhere, in all the places I expect it. Pretty much every time it's > not there is when I expect TR to be able to prove something it can't prove.
Do you have examples besides fixnum operations? > - Change (add1 i) into (unsafe-fx+ 1 i), prove it's safe We're looking into adding a OneLessThanMaxFixnum type that, when used as argument to add1 gives a return type of Fixnum. That would solve this problem. > - Replace match-define with multiple defines > > For the last, IIRC, on my version of Racket, match-define calls a > predicate to ensure the right struct type, but it's redundant in TR. Removing predicates made redundant by typechecking in the general case is on my todo list. > I had to do the following in my tests and test app: > > - Use flsqrt, flfloor, flceiling instead of non-fl* versions sqrt can indeed return a complex number, but if you pass it a Nonnegative-Float, the result should be a Nonnegative-Float. As for floor and ceiling, they should already preserve flonum-ness, and as such should be optimized. Can you send me an example where these could not be optimized? > - Use (* x x) instead of (sqr x) sqr should give you the right types. However, its type does not currently express its full behavior wrt the sign of the result. I'll fix that. > You'll want to rename it to with-asserts*, I suppose. I think if I were > to spend more time on it, I'd make the type-name part optional, and in > those cases use pred?'s syntax as a string as the second argument to > raise-type-error. Thanks, I'll add that. We're also thinking of having assert (and thus with-asserts*) take types as arguments, instead of just predicates. Vincent _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users

