[CakeML] translator

[Yong Kiam Tan]

Hi Konrad,

I added the tuple -> let printing sometime ago.

You can set use_full_type_names:=false to get the behavior you want for
module names.

Additionally, this also fixes the generated name for vector (although the
REPL needs to be built from 3393ee which adds vector as a top-level type
abbreviation).


On Sun, Aug 16, 2015 at 6:29 AM, 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.
>>>
>>
>>
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20150825/063c3d86/attachment.html>