[CakeML] translator

[Konrad Slind]

Hi Yong Kiam,

To get the asts printed, Magnus advised invoking

  ml_translatorLib.print_asts := true

in my Script file, after I had made all the definitions and before
export_theory().

Will this still work?

Thanks,
Konrad.


On Wed, Aug 12, 2015 at 10:11 AM, Yong Kiam Tan <tanyongkiam at gmail.com>
wrote:

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