"Number is smaller than 0x8000, trust me"

[David Smith]

Hey, I have a small convenience function that takes 3 5 bit bit numbers to produce a 15 bit color, that's guaranteed to be <0x8000.

Now, apparently the typechecker doesn't know much about `lor`. Is there any way I could say "hey trust me, if these three numbers are < 0x20 then the result is < 0x8000"?

Thanks in advance.

[Elijah Stone]

What happens if you use addition instead of oring? The result should be
the same, and on modern processors performance is the same.

> --
> You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/4f5589ed-b80d-4662-918c-ac1fa81d04c9n%40googlegroups.com.
>
>

[David Smith]

Eh, I actually thought about that, but I really don't like the idea, plus this isn't really a modern system (talking about a GBA here)...

[Elijah Stone]

On Sun, 23 May 2021, David Smith wrote:

> GBA

Apparently it's still the same speed on a GBA
(https://problemkaputt.de/gbatek.htm#arminstructionsummary).

But I agree it would be nicer if the direct solution would work correctly.

[Hongwei Xi]

This kind of guarantee can always be established with a run-time check.

If you want to solve constraints involving 'lor', then you need to use an external solver like Z3.

But it would require a lot of effort.

I would suggest using a run-time check for now. And you could always come back to fix it later

if really needed.

--

[d4v3y_5c0n3s]

Hey David, have you tried using the "praxi" syntax?  It allows you to define an axiom, essentially telling ATS: "I'm not going to prove that X is true, but just assume it is."  I'd recommend reading the theorem proving sections of Intro to ATS if you haven't already.

Here's an example of a praxi that should suit your needs:

sortdef invals = {iv:int | iv < 0x20}

praxi lor_assumption {a,b,c:invals}{r:int} (

a:int a, b:int b, c:int c,

result: int r

) : [r < 0x8000] void

If you'd like me to explain what I'm doing here, just ask me and I can tell you how this works.  (By the way, I tested and this code compiles.)

[David Smith]

Ah, that sounds like a pretty neat solution.

How exactly do I make ATS know that my function that does the or-ing should make use of that proof?

[Troy Jacobs]

Well, I believe that you could just call the praxi in the body of your "or" function just like you would with any function.  I don't have the ability to test this at the moment, but later I will try to show you an example of what I mean.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/d55d521b-0a8b-4062-950b-40b315f9ed85n%40googlegroups.com.