[CakeML] translator

David Hardin david.hardin at rockwellcollins.com
Mon Aug 17 05:08:35 UTC 2015


Konrad,

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

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.


Thanks,

DSH


On Sat, Aug 15, 2015 at 5:29 PM, Konrad Slind <konrad.slind at gmail.com>
wrote:

> Oh sure. All I had to do is do a minor edit to the declaration of the
> datatype of regexps.
> See attached. The generated code is in regexpML_ml.txt. I am also
> attaching the original hand-written regexp.cake file. At the end of that
> file are some examples, which should be easy to adapt to and run on
> the generated code. I will do this once I get back from having a really
> great Saturday night, but you can have a go at getting that to run if
> you can't wait.
>
> (Note to cakeML folk: is there a way to have the declared type be "regexp"
> instead of
>  "regexp_regexp" --- which I assume is the concatenation of theory and
>  type name?)
>
> Konrad.
>
>
>
> On Sat, Aug 15, 2015 at 4:57 PM, David Hardin <
> david.hardin at rockwellcollins.com> wrote:
>
>> 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?
>>
>> 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.
>>
>>
>> DSH
>>
>>
>> On Sat, Aug 15, 2015 at 7:15 AM, Michael Norrish <
>> Michael.Norrish at nicta.com.au> wrote:
>>
>>> 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.
>>>
>>> Michael
>>>
>>> > On 15 Aug 2015, at 18:59, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>>> >
>>> > 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).
>>> >
>>> > -Scott
>>> >
>>> >> On 2015/08/15, at 01:19, Konrad Slind <konrad.slind at gmail.com> wrote:
>>> >>
>>> >> Example of Problem 2:
>>> >>
>>> >> SOME(1,2)  and
>>> >> SOME((1,2))
>>> >
>>> > _______________________________________________
>>> > Users mailing list
>>> > Users at cakeml.org
>>> > https://lists.cakeml.org/listinfo/users
>>>
>>> ________________________________
>>>
>>> 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.
>>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20150817/e4e96a71/attachment.html>


More information about the Users mailing list