[CakeML] translator
Konrad Slind
konrad.slind at gmail.com
Wed Aug 12 17:15:16 UTC 2015
Thanks for the redirect Ramana.
Re: vectors.
The HOL declaration
val _ = type_abbrev("charset", ``:bool vector``);
(*---------------------------------------------------------------------------*)
(* Datatype of extended regular expressions
*)
(*---------------------------------------------------------------------------*)
val _ = Hol_datatype
`regexp
= Chset of charset
| Cat of regexp => regexp
| Star of regexp
| Or of regexp list
| Neg of regexp`;
generates the following cakeML concrete syntax:
datatype regexp_regexp = Neg of regexp_regexp
| Or of regexp_regexp list
| Star of regexp_regexp
| Cat of regexp_regexp * regexp_regexp
| Chset of bool ml_translator_vector
which fails to parse in the REPL.
Further, the following definitions (using sub, length, and Vector),
val charset_mem_def =
Define
`charset_mem n cs = sub cs n`;
val toList_def =
Define
`toList V = toListAux V 0 (length V)`;
val charset_empty_def =
Define
`charset_empty:charset = Vector all_unset`
generate the following cakeML definitions, which fail to parse in the REPL.
fun charset_mem v2 = (fn v1 => App Vsub [v1; v2])
fun tolist v1 = tolistaux v1 0 App Vlength [v1]
val charset_empty = App VfromList [all_unset]
Also, the code generated from balanceL and balanceR (from
balanced_mapTheory)
doesn't parse. That will be harder to track down, since the definitions are
a bit
gnarly.
Thanks,
Konrad.
On Tue, Aug 11, 2015 at 4:47 PM, 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/2f8967a5/attachment.html>
More information about the Users
mailing list