[CakeML] translator

Wed Aug 12 15:11:00 UTC 2015

Hi Konrad,

I'm not sure how exactly you are printing the declarations, I have added
semicolons for each declaration in the pretty printer now but the way I
used to print them from HOL was to print the whole thing as a list of decls
(so the semicolons get automatically added after each decl).

For reference, my printing code was something like:
val _ = enable_astPP();
val _ = set_trace "pp_avoids_symbol_merges" 0;

val _ = finalise_translation();
val decls = get_decls() in print(term_to_string decls) end;

(I guess this now needs to change to print each decl separately instead of
just as a list).

Let me know if the latest update to astPP doesn't work for you (I could
probably help if you sent me the declarations you wanted printed as well
since I think those got lost in the email).

On Wed, Aug 12, 2015 at 5:47 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> (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.
>>>>>>>>>
>>>>>>>>>
>>>>>>
>>>>>
>>>>
>
> _______________________________________________
> 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/20150812/4d1ef587/attachment.html>