[CakeML] translator

[Konrad Slind]

The latest updates on generating concrete syntax from asts makes my life
better. Thanks!

1. Semicolons are being added in the right place.
2. The problems with the concrete syntax for
balanced_mapTheory.balance{L,R}_def
    have gone away.
3. Vector operations get printed properly.

However, two small problems remain:

1. vector types don't get printed properly.
2. tuples as arguments to SOME aren't handled by the cakeML REPL,
    so the concrete syntax prettyprinter should map that case to a let.
    I presently work around this by putting the let into the original
    HOL definition, but it looks clumsy.

Example of Problem 1:

val _ = type_abbrev("charset", ``:bool ml_translator$vector``);

val _ = Hol_datatype
 `regexp
    = Chset of charset
    | Cat of regexp => regexp
    | Star of regexp
    | Or of regexp list
    | Neg of regexp`;

gets printed out on the cakeML side of the translation as

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;

but the last clause should presumably be

      | Chset of bool Vector.vector;

Example of Problem 2:

SOME(1,2)  and
SOME((1,2))

both aren't accepted by the REPL.

Cheers,
Konrad.


On Wed, Aug 12, 2015 at 11:03 PM, Konrad Slind <konrad.slind at gmail.com>
wrote:

> Thanks Yong Kiam,
>
>   I will try this tomorrow.
>
> Konrad.
>
>
> On Wed, Aug 12, 2015 at 9:45 PM, Yong Kiam Tan <tanyongkiam at gmail.com>
> wrote:
>
>> Replying to both emails here:
>>
>> 1) print_asts:=true should work (and has semicolons now) -- I tried it,
>> but let me know if it doesn't work for you
>>
>> 2) The regexp data type parses fine for me (but gives a type error?).
>>
>> 3) I'll add a more permanent solution to the pretty printer for all the
>> built-in ops that aren't being pretty printed at the moment but they'll
>> probably just be special case rules (I originally wrote the pretty printer
>> assuming the input was coming from the parser, which doesn't generate
>> primitives).
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20150814/2e3c9364/attachment.html>