<div dir="ltr">The same problem applies to quicksortProg (which I can fix).<br><br>There's also an unbound variable in the definition of sort in sortProg (namely, "sorted" in "List.app print sorted" is unbound).<br>I'll leave you to fix that last one Scott, since I'm not sure exactly what you wanted to do (app the array, or convert it to a list first?).<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 26 March 2017 at 16:31, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Looking at it now, it seems like the problem is that mlarrayProg doesn't add hardly any of the Array functions to the ml_progLib state it exports. So for example Array.fromList is out of scope because it was never added to the basis. I will try adding the ones you're using (I don't know why they're not all added... I think I remember Connor saying things were too slow?)<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 26 March 2017 at 07:35, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">Common problems include:<div dir="auto">- The spec theorem has type variables that need instantiation,</div><div dir="auto">- The function is not in scope,</div><div dir="auto">- The function is applied to the wrong number of arguments</div><div dir="auto"><br></div><div dir="auto">I think the middle one can reduce your goal to false whereas the others can raise exceptions. Does your p variable have 'ffi ffi_proj type?</div><div dir="auto"><br></div><div dir="auto">I'll try to have a look at some point. (Currently at AITP.)</div></div><div class="m_645153383569702128HOEnZb"><div class="m_645153383569702128h5"><div class="gmail_extra"><br><div class="gmail_quote">On 25 Mar 2017 20:09, "Yong Kiam" <<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Those tactics are defined in the tactic libs in characteristic/, I fixed a few issues back on env-refactor by stepping through them.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Mar 25, 2017 at 2:46 PM, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Ok. I think I have the dependencies right now. However, I still have 4 cf_apps where xapp and xapp_spec fail, and I have no idea why, or how to even start debugging the problem. This is on the sort_example branch, characteristic/examples/sortPr<wbr>ogScript.sml. Any hints would be greatly appreciated.<br>
<span class="m_645153383569702128m_746777920506666997m_-195553722216766323HOEnZb"><font color="#888888"><br>
Scott<br>
</font></span><div class="m_645153383569702128m_746777920506666997m_-195553722216766323HOEnZb"><div class="m_645153383569702128m_746777920506666997m_-195553722216766323h5"><br>
> On 2017/03/25, at 02:46, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
><br>
> Add arrays into the same linear sequence that includes I/O and update the basis/dependency-order file accordingly.<br>
><br>
> The longer term solution is to get the abstract translator working. (There is an issue, and was some discussion on a wiki page.)<br>
><br>
> On Friday, 24 March 2017, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>> wrote:<br>
> > I’m trying to verify a program with CF that uses both arrays and I/O from the basis. I don’t see how to make this work, since you only seem to be able to do 1 translation_extends. Any ideas?<br>
> ><br>
> > Scott<br>
> > ______________________________<wbr>_________________<br>
> > Developers mailing list<br>
> > <a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
> > <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
> ><br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
</div></div></blockquote></div><br></div>
</blockquote></div></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>