<div dir="ltr">Konrad,<div><br></div><div>I was able to get my CakeML REPL to successfully consume the code in regexpML_ml.txt -- that's the good news. The bad news is that when I tried to concatenate the test code from regexp.cake, as you suggested, I got lots of type errors. I tried to fill in with other functions, etc. defined in your hand-coded regexp.cake, but without success. It's current failing on the definition of 'digit'.</div><div><br></div><div>Please have a look -- I'm sure it'll be clear to you, since you wrote the original, and know about 1000x more about ML than I do.</div><div><br></div><div><br></div><div>Thanks,</div><div><br></div><div>DSH</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Aug 15, 2015 at 5:29 PM, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</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">Oh sure. All I had to do is do a minor edit to the declaration of the datatype of regexps.<div>See attached. The generated code is in regexpML_ml.txt. I am also</div><div>attaching the original hand-written regexp.cake file. At the end of that</div><div>file are some examples, which should be easy to adapt to and run on</div><div>the generated code. I will do this once I get back from having a really</div><div>great Saturday night, but you can have a go at getting that to run if</div><div>you can't wait.</div><div><br></div><div><div>(Note to cakeML folk: is there a way to have the declared type be "regexp" instead of <br></div><div> "regexp_regexp" --- which I assume is the concatenation of theory and </div><div> type name?)</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Konrad.</div><div><br></div><div><br></div></font></span></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Aug 15, 2015 at 4:57 PM, David Hardin <span dir="ltr"><<a href="mailto:david.hardin@rockwellcollins.com" target="_blank">david.hardin@rockwellcollins.com</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">So, Konrad, does that mean you can cobble together a source file that I can play with, or do I have to wait? Sounds like you are close, but Michael's comments indicate that the final fixes to create a "proper" source file aren't going to appear overnight. I'm guessing that some hand-tweaking may be needed in the short term. Is that correct?<div><br></div><div>Thanks, Konrad, and thanks to everyone on the CakeML team for your help so far. I'm excited about the possibilities for CakeML, and can't wait to do more with it. BTW, I'm a big believer in pushing through third party examples like this -- nothing better for finding problems with one's tools.</div><div><br></div><div><br></div><div>DSH</div><div><br></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Aug 15, 2015 at 7:15 AM, Michael Norrish <span dir="ltr"><<a href="mailto:Michael.Norrish@nicta.com.au" target="_blank">Michael.Norrish@nicta.com.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">That's not fixed, and won't be until the parser gets access to arity information for constructors or if we adopt your idea of treating all constructor applications as function calls that resolve to primitives somehow. I don't know if the second approach also works for patterns. I'm happy to thread arity information through the parser but the toplevel state will have to pick it up and allow for the parser to change it.<br>
<br>
Michael<br>
<div><div><br>
> On 15 Aug 2015, at 18:59, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>> wrote:<br>
><br>
> I think that was fixed on the master branch, but we can’t generate a new executable as the master branch has some problems right now (possibly related to HOL updates).<br>
><br>
> -Scott<br>
><br>
>> On 2015/08/15, at 01:19, Konrad Slind <<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>> wrote:<br>
>><br>
>> Example of Problem 2:<br>
>><br>
>> SOME(1,2) and<br>
>> SOME((1,2))<br>
><br>
</div></div><span>> _______________________________________________<br>
> Users mailing list<br>
> <a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
<br>
</span>________________________________<br>
<br>
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.<br>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>