Re: unsolved constraint for termetric being well-founded
This worked! Thank you. :D
On Thursday, September 3, 2020 at 4:27:00 PM UTC-4 gmhwxi wrote:
> A termination metric is required to be non-negative. Try to change ..
> into ..
>
> On Thu, Sep 3, 2020 at 2:57 PM d4v3y_5c0n3s wrote:
>
>> So, I've been encountering this "unsolved constraint for termetric being
>> well-founded" error message, and I'm not sure how to fix it. Does this
>> mean that I'm not being strict enough with types?
>>
>> Here's my code:
>>
>> absvt@ype mesh
>>
>> assume mesh =
>> [v,t:nat]
>> [vl,tl:addr]
>> @{
>> v=int v, t=int t, vap=arrayptr(vertex, vl, v), tap=arrayptr(uint32, tl,
>> t)
>> }
>>
>> implement mesh_print ( m ) = let
>> fun vert_print_loop {i,j:int | 0 <= i+1; i+1 <= j} .. ( i: int i,
>> v_arr: &(arrayptr(vertex, j)) ): void =
>> if not(i < 0) then begin
>> vertex_print(v_arr[i]);
>> vert_print_loop(i-1, v_arr)
>> end else ()
>> fun tri_print_loop {i,j:int | 0 <= i+1; i+1 <= j} .. ( i: int i,
>> t_arr: &(arrayptr(uint32, j)) ): void =
>> if not(i < 0) then begin
>> println!(t_arr[i]);
>> tri_print_loop(i-1, t_arr)
>> end else ()
>> in
>> println!("Num Verts: ", m.v);
>> vert_print_loop(m.v-1, m.vap);
>> println!("Num Tris: ", m.t);
>> println!("Triangle Indicies");
>> tri_print_loop(m.t-1, m.tap)
>> end
>>
>> Here's the errors:
>>
>> patscc -tcats /home/tmj90/Goldelish-Engine/source/g_engine.dats
>> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 67738(line=2381,
>> offs=54) -- 67904(line=2385, offs=16): error(3): unsolved constraint for
>> termetric being well-founded: C3NSTRprop(C3TKtermet_isnat();
>> S2Eapp(S2Ecst(gte_int_int); S2Evar(i(8786)), S2Eint(0)))
>> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 67957(line=2386,
>> offs=53) -- 68118(line=2390, offs=16): error(3): unsolved constraint for
>> termetric being well-founded
>> typechecking has failed: there are some unsolved constraints: please
>> inspect the above reported error message(s) for information.
>> exit(ATS): uncaught exception:
>> _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>>
>> Please ask if you need any additional information.
>>
>> --
>> 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/442cef10-e62a-4873-96d9-00cec346390dn%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/ats-lang-users/442cef10-e62a-4873-96d9-00cec346390dn%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>
--
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/3c4423ca-d843-49d9-9401-ae80cbe89b80n%40googlegroups.com.
Re: unsolved constraint for termetric being well-founded
A termination metric is required to be non-negative. Try to change ..
into ..
On Thu, Sep 3, 2020 at 2:57 PM d4v3y_5c0n3s wrote:
> So, I've been encountering this "unsolved constraint for termetric being
> well-founded" error message, and I'm not sure how to fix it. Does this
> mean that I'm not being strict enough with types?
>
> Here's my code:
>
> absvt@ype mesh
>
> assume mesh =
> [v,t:nat]
> [vl,tl:addr]
> @{
> v=int v, t=int t, vap=arrayptr(vertex, vl, v), tap=arrayptr(uint32, tl,
> t)
> }
>
> implement mesh_print ( m ) = let
> fun vert_print_loop {i,j:int | 0 <= i+1; i+1 <= j} .. ( i: int i,
> v_arr: &(arrayptr(vertex, j)) ): void =
> if not(i < 0) then begin
> vertex_print(v_arr[i]);
> vert_print_loop(i-1, v_arr)
> end else ()
> fun tri_print_loop {i,j:int | 0 <= i+1; i+1 <= j} .. ( i: int i,
> t_arr: &(arrayptr(uint32, j)) ): void =
> if not(i < 0) then begin
> println!(t_arr[i]);
> tri_print_loop(i-1, t_arr)
> end else ()
> in
> println!("Num Verts: ", m.v);
> vert_print_loop(m.v-1, m.vap);
> println!("Num Tris: ", m.t);
> println!("Triangle Indicies");
> tri_print_loop(m.t-1, m.tap)
> end
>
> Here's the errors:
>
> patscc -tcats /home/tmj90/Goldelish-Engine/source/g_engine.dats
> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 67738(line=2381,
> offs=54) -- 67904(line=2385, offs=16): error(3): unsolved constraint for
> termetric being well-founded: C3NSTRprop(C3TKtermet_isnat();
> S2Eapp(S2Ecst(gte_int_int); S2Evar(i(8786)), S2Eint(0)))
> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 67957(line=2386,
> offs=53) -- 68118(line=2390, offs=16): error(3): unsolved constraint for
> termetric being well-founded
> typechecking has failed: there are some unsolved constraints: please
> inspect the above reported error message(s) for information.
> exit(ATS): uncaught exception:
> _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
>
> Please ask if you need any additional information.
>
> --
> 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/442cef10-e62a-4873-96d9-00cec346390dn%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/442cef10-e62a-4873-96d9-00cec346390dn%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAPPSPLrMphgPqrVe-R-7pFzKP1oJrOmL%2BX1w-Dp-FVAUX0Aa_Q%40mail.gmail.com.
Re: unsolved constraint for termetric being well-founded
Okay, thanks. I'll try to rework the loop then. Thank you, you've been a big help. :) On Thursday, September 3, 2020 at 3:24:59 PM UTC-4 ice.r...@gmail.com wrote: > that i >= 0 * > > чт, 3 сент. 2020 г. в 19:24, Dambaev Alexander : > >> hi >> as far as I can see, the error message asks to prove, that i > 0. You >> have constraint i+1 >= 0, so i can be ~1, which is not natural number, but >> quite from tutorial: >> ``` >> A termination metric is just a tuple of *natural* numbers and the >> standard lexicographic ordering on *natural* numbers is used to order >> such tuples. >> ``` >> and that is why you see ```C3TKtermet_isnat()``` >> > -- 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/5837819a-c930-4661-a45b-fadd6f173213n%40googlegroups.com.
Re: unsolved constraint for termetric being well-founded
hi as far as I can see, the error message asks to prove, that i > 0. You have constraint i+1 >= 0, so i can be ~1, which is not natural number, but quite from tutorial: ``` A termination metric is just a tuple of *natural* numbers and the standard lexicographic ordering on *natural* numbers is used to order such tuples. ``` and that is why you see ```C3TKtermet_isnat()``` -- 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/CAHjn2KzdbgR1CZ3MBtDjXD%2BzmaN8HHVBFHggCyVrBSaLdSf3tg%40mail.gmail.com.
Re: unsolved constraint for termetric being well-founded
that i >= 0 * чт, 3 сент. 2020 г. в 19:24, Dambaev Alexander : > hi > as far as I can see, the error message asks to prove, that i > 0. You have > constraint i+1 >= 0, so i can be ~1, which is not natural number, but quite > from tutorial: > ``` > A termination metric is just a tuple of *natural* numbers and the > standard lexicographic ordering on *natural* numbers is used to order > such tuples. > ``` > and that is why you see ```C3TKtermet_isnat()``` > -- 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/CAHjn2Kxe05-drMhkY4USk1i%3DTvz2D8dREz%3DVXde88_oWZiMW3A%40mail.gmail.com.
unsolved constraint for termetric being well-founded
So, I've been encountering this "unsolved constraint for termetric being
well-founded" error message, and I'm not sure how to fix it. Does this
mean that I'm not being strict enough with types?
Here's my code:
absvt@ype mesh
assume mesh =
[v,t:nat]
[vl,tl:addr]
@{
v=int v, t=int t, vap=arrayptr(vertex, vl, v), tap=arrayptr(uint32, tl, t)
}
implement mesh_print ( m ) = let
fun vert_print_loop {i,j:int | 0 <= i+1; i+1 <= j} .. ( i: int i,
v_arr: &(arrayptr(vertex, j)) ): void =
if not(i < 0) then begin
vertex_print(v_arr[i]);
vert_print_loop(i-1, v_arr)
end else ()
fun tri_print_loop {i,j:int | 0 <= i+1; i+1 <= j} .. ( i: int i,
t_arr: &(arrayptr(uint32, j)) ): void =
if not(i < 0) then begin
println!(t_arr[i]);
tri_print_loop(i-1, t_arr)
end else ()
in
println!("Num Verts: ", m.v);
vert_print_loop(m.v-1, m.vap);
println!("Num Tris: ", m.t);
println!("Triangle Indicies");
tri_print_loop(m.t-1, m.tap)
end
Here's the errors:
patscc -tcats /home/tmj90/Goldelish-Engine/source/g_engine.dats
/home/tmj90/Goldelish-Engine/source/g_engine.dats: 67738(line=2381,
offs=54) -- 67904(line=2385, offs=16): error(3): unsolved constraint for
termetric being well-founded: C3NSTRprop(C3TKtermet_isnat();
S2Eapp(S2Ecst(gte_int_int); S2Evar(i(8786)), S2Eint(0)))
/home/tmj90/Goldelish-Engine/source/g_engine.dats: 67957(line=2386,
offs=53) -- 68118(line=2390, offs=16): error(3): unsolved constraint for
termetric being well-founded
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
Please ask if you need any additional information.
--
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/442cef10-e62a-4873-96d9-00cec346390dn%40googlegroups.com.
