[CakeML] translator

[Ramana Kumar]

(I actually think these emails should be on the CakeML Users mailing list -
redirecting there.)

Konrad, I think you're right that astPP should add semicolons, since CakeML
expects them. I'll add an issue for this.  (
https://github.com/CakeML/cakeml/issues/54)

You're also right that it probably doesn't do anything special regarding
vectors at the moment. But what should it do? (I.e., what's going wrong
with them?)

On 12 August 2015 at 02:16, Magnus Myreen <magnus.myreen at gmail.com> wrote:

> Got the wrong email address for Yong Kiam. This time with his gmail
> address.
>
> On Tue, 11 Aug 2015 at 18:12, Magnus Myreen <magnus.myreen at gmail.com>
> wrote:
>
>> I think Yong Kiam and Ramana ought to be included in these emails. I've
>> included them. -- Magnus
>> On Tue, 11 Aug 2015 at 18:03, Konrad Slind <konrad.slind at gmail.com>
>> wrote:
>>
>>> .... having some trouble expressing myself: print_ast prints out
>>> everything fine, but
>>> the generated syntax isn't accepted by the cakeml REPL.
>>>
>>> Konrad.
>>>
>>>
>>> On Tue, Aug 11, 2015 at 10:53 AM, Konrad Slind <konrad.slind at gmail.com>
>>> wrote:
>>>
>>>> print_asts works pretty well, but doesn't get all the way through the
>>>> file.
>>>> Quick comments:
>>>>
>>>> 1. cakeml repl demands semicolon to terminate declaration. But
>>>> print_ast doesn't
>>>>    add these.
>>>>
>>>> 2. print_asts may not know about Vector and operations on it.
>>>>
>>>> Konrad.
>>>>
>>>>
>>>> On Tue, Aug 11, 2015 at 9:09 AM, Konrad Slind <konrad.slind at gmail.com>
>>>> wrote:
>>>>
>>>>> Thanks!
>>>>>
>>>>>
>>>>> On Tue, Aug 11, 2015 at 9:06 AM, Magnus Myreen <
>>>>> magnus.myreen at gmail.com> wrote:
>>>>>
>>>>>> Yes, the translator can be made to print concrete syntax. The printer
>>>>>> isn't 100 % reliable (bug reports are appreciated). To print concrete
>>>>>> syntax, write
>>>>>>
>>>>>> val _ = (print_asts := true)
>>>>>>
>>>>>> in your script file where the translation happens. Running Holmake
>>>>>> should produce some sml files with the concrete syntax.
>>>>>>
>>>>>> I'm not at a computer at the moment so can't try this at the moment...
>>>>>>
>>>>>> Cheers,
>>>>>> Magnus
>>>>>>
>>>>>> On Tue, 11 Aug 2015 at 15:58, Konrad Slind <konrad.slind at gmail.com>
>>>>>> wrote:
>>>>>>
>>>>>>> Hi all,
>>>>>>>
>>>>>>>   My message was a bit terse. To build the example:
>>>>>>>
>>>>>>> 1. update
>>>>>>> <cakeml>/translator/{ml_translatorScript.sml,ml_translatorLib.sml}
>>>>>>>     with the attached files. Note that these new versions will build
>>>>>>> okasaki-examples
>>>>>>>     and other-examples directories.
>>>>>>> 2. Put all the other files in a new directory foo
>>>>>>> 3. Invoke Holmake regexpTheory.uo
>>>>>>>
>>>>>>> Now a question: using the translator I think I have built up an
>>>>>>> internal environment
>>>>>>> of cakeML ASTs corresponding to the original HOL definitions. Does
>>>>>>> cakeML
>>>>>>> provide a way to get these ASTs printed out in cakeML concrete
>>>>>>> syntax?
>>>>>>>
>>>>>>> Thanks,
>>>>>>> Konrad.
>>>>>>>
>>>>>>>
>>>>>>> On Mon, Aug 10, 2015 at 6:11 PM, Konrad Slind <
>>>>>>> konrad.slind at gmail.com> wrote:
>>>>>>>
>>>>>>>> Hi all,
>>>>>>>>
>>>>>>>>   I got the regexp matcher to finally get through the translator.
>>>>>>>> In order to do
>>>>>>>> this, I had to do some revision to the definitions, and I also had
>>>>>>>> to fix a
>>>>>>>> problem with "v" in ml_translatorLib.sml and
>>>>>>>> ml_translatorScript.sml.
>>>>>>>> All this should be in the attached files.
>>>>>>>>
>>>>>>>> Some notes on what I learned are in trans.notes.txt.
>>>>>>>>
>>>>>>>> The problem with v: some code in the translator depends on this
>>>>>>>> name. But if the
>>>>>>>> definition to be translated also has a variable named "v" problems
>>>>>>>> occur. I worked
>>>>>>>> around this by changing the translator to use "_v" in various
>>>>>>>> places, and also
>>>>>>>> changing the use of "v" in some definitions in
>>>>>>>> ml_translatorScript.sml.
>>>>>>>>
>>>>>>>> I am still puzzled that mergesort_def won't translate, but I've
>>>>>>>> swapped that out
>>>>>>>> in favour of QSORT, which translates with no problem.
>>>>>>>>
>>>>>>>> Cheers,
>>>>>>>> Konrad.
>>>>>>>>
>>>>>>>>
>>>>>
>>>>
>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20150812/c96332a6/attachment.html>