Re: Embedding differential equations into types
I skipped the constraint-solving part, which needs to be exported to Z3.
On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov wrote:
>
> On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:
>>
>> Adding a 2d-oscillator example:
>>
>>
>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/
>>
>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator_2d_anim.html
>>
>>
> What's this for?
>
> prval () =
> $UN.prop_assert{false}()
>
>
>
> Is it asserting falsity?
>
> On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:
>>>
>>> Renaming Github to GitHub:
>>>
>>>
>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
>>>
>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
>>>
>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html
>>>
>>>
>>> On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:
I'd like to report an interesting example of using types in ATS.
Here are two animations of bouncing balls:
http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
Cheers!
--
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/13297f0a-1c0d-4e21-bc14-1bb4652eb75c%40googlegroups.com.
Re: Embedding differential equations into types
On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote:
>
> Adding a 2d-oscillator example:
>
>
> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/
>
> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator_2d_anim.html
>
>
What's this for?
prval () =
$UN.prop_assert{false}()
Is it asserting falsity?
On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote:
>>
>> Renaming Github to GitHub:
>>
>>
>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
>>
>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
>>
>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html
>>
>>
>> On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote:
>>>
>>>
>>> I'd like to report an interesting example of using types in ATS.
>>>
>>> Here are two animations of bouncing balls:
>>>
>>>
>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/
>>>
>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html
>>>
>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html
>>>
>>> The graphics is uninteresting. What is interesting here is that the
>>> differential equations governing the movement of the ball are
>>> captured in the ATS types.
>>>
>>> Cheers!
>>>
>>>
--
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/5345aea8-4b44-4a10-8284-aff0c56fab80%40googlegroups.com.
Re: Embedding differential equations into types
Adding a 2d-oscillator example: http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/ http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator_2d_anim.html On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote: > > Renaming Github to GitHub: > > > http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/ > > http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html > > http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html > > > On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote: >> >> >> I'd like to report an interesting example of using types in ATS. >> >> Here are two animations of bouncing balls: >> >> >> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/ >> >> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html >> >> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html >> >> The graphics is uninteresting. What is interesting here is that the >> differential equations governing the movement of the ball are >> captured in the ATS types. >> >> Cheers! >> >> -- 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 post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5abf85eb-c16e-4686-b957-fa9d4f0672fc%40googlegroups.com.
Re: Embedding differential equations into types
Renaming Github to GitHub: http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/ http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote: > > > I'd like to report an interesting example of using types in ATS. > > Here are two animations of bouncing balls: > > > http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/ > > http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html > > http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html > > The graphics is uninteresting. What is interesting here is that the > differential equations governing the movement of the ball are > captured in the ATS types. > > Cheers! > > -- 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 post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/bcc905f1-2f7d-4e1e-84b9-fab8501973e6%40googlegroups.com.
