unsolved constraint for termetric being well-founded

[d4v3y_5c0n3s]

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

[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()```

[Dambaev Alexander]

that i >= 0 *

чт, 3 сент. 2020 г. в 19:24, Dambaev Alexander <ice.r...@gmail.com>:

[d4v3y_5c0n3s]

Okay, thanks.  I'll try to rework the loop then.  Thank you, you've been a big help. :)

[Hongwei Xi]

A termination metric is required to be non-negative. Try to change .<i>. into .<i+1>.

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

[d4v3y_5c0n3s]

This worked!  Thank you. :D