Re: "Number is smaller than 0x8000, trust me"

[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.

On Thu, Jun 3, 2021, 6:26 PM David Smith  wrote:

> 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?
>
> d4v3y_5c0n3s schrieb am Samstag, 29. Mai 2021 um 15:39:37 UTC:
>
>> 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.)
>>
>> On Sunday, May 23, 2021 at 7:22:52 PM UTC-4 gmhwxi wrote:
>>
>>> 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.
>>>
>>> On Sun, May 23, 2021 at 6:28 PM David Smith  wrote:
>>>

 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.

 --

>>> 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
 
 .

>>> --
> 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-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/d55d521b-0a8b-4062-950b-40b315f9ed85n%40googlegroups.com
> 
> .
>

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAHa%2B7Mkk_jiF4G3LHb9ooYdeHFZOgR0YvkmqDzzRQ8YHaa-7PQ%40mail.gmail.com.

Re: "Number is smaller than 0x8000, trust me"

[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?

d4v3y_5c0n3s schrieb am Samstag, 29. Mai 2021 um 15:39:37 UTC:

> 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.)
>
> On Sunday, May 23, 2021 at 7:22:52 PM UTC-4 gmhwxi wrote:
>
>> 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.
>>
>> On Sun, May 23, 2021 at 6:28 PM David Smith  wrote:
>>
>>>
>>> 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.
>>>
>>> -- 
>>>
>> 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
>>>  
>>> 
>>> .
>>>
>>

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/d55d521b-0a8b-4062-950b-40b315f9ed85n%40googlegroups.com.

Re: "Number is smaller than 0x8000, trust me"

[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.)

On Sunday, May 23, 2021 at 7:22:52 PM UTC-4 gmhwxi wrote:

> 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.
>
> On Sun, May 23, 2021 at 6:28 PM David Smith  wrote:
>
>>
>> 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.
>>
>> -- 
>>
> 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
>>  
>> 
>> .
>>
>

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/f4a64ead-e20c-4389-a5d2-dbad4f7d8254n%40googlegroups.com.

Re: "Number is smaller than 0x8000, trust me"

[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.

On Sun, May 23, 2021 at 6:28 PM David Smith  wrote:

>
> 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.
>
> --
> 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-users+unsubscr...@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
> 
> .
>

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqwSYfL-jmkB4%2BiTrKWy2rZDWxwYzsZWb%2BecqqRTkhoyA%40mail.gmail.com.

Re: "Number is smaller than 0x8000, trust me"

[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.

--
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/9c2d81d7-38b7-de8d-a58-da11d030579b%40elronnd.net.

Re: "Number is smaller than 0x8000, trust me"

[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)...

Elronnd _ schrieb am Sonntag, 23. Mai 2021 um 22:30:15 UTC:

> What happens if you use addition instead of oring? The result should be 
> the same, and on modern processors performance is the same.
>
> On Sun, 23 May 2021, David Smith wrote:
>
> > 
> > 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.
> > 
> > --
> > 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
> .
> > 
> >
>

-- 
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/73172cef-4edf-41d2-beb1-795f3e32e708n%40googlegroups.com.

Re: "Number is smaller than 0x8000, trust me"

[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.


On Sun, 23 May 2021, David Smith wrote:



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.

--
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-users+unsubscr...@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.




--
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/ac619622-d8a5-4df-7ff1-4f3f84c1d72%40elronnd.net.

"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.

-- 
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-users+unsubscr...@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.