[CakeML] translator

[Konrad Slind]

Thanks Yong Kiam! I will give this a go and see what happens.

Konrad.


On Tue, Aug 25, 2015 at 10:41 AM, Yong Kiam Tan <tanyongkiam at gmail.com>
wrote:

> 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/19bad2f0/attachment-0001.html>