astPP doesn't print algebraic datatype correctly

[redianthus]

Hi,

With the following datatype:

datatype 'a misc_app_list =
   Nil
|  Append of  'a misc_app_list *  'a misc_app_list
|  List of  'a list;

Here's an example of what is produced:

(Append(Append(v2,List([", "])),v5 v1))

I.e:

(Append
  (Append
    (v2,
     List([", "])
    ),
    v5 v1
  )
)

When it should be:

(Append
  (Append
    (v2)
    ( List([", "]) )
  )
  ( v5 v1 )
)

Shortly, Append x y is printed as Append (x, y) instead of Append (x) (y). My guess is that it's printed by the same function than the one used to print lists or things like:

case  v3 of 
   (v2,v1) => (* <- this *)

To fix this, it should not print a , but ) ( between things.

It's working for the constructor List, but I think it's because it takes only one argument, so the bug doesn't show.

[oskarabrahamsson]

But 'a misc_app_list * 'a misc_app_list is a pair of two 'a misc_app_lists?

[redianthus]

Actually, it's not.

I don't know what happened. I copy/pasted it from some output of the AST_pp IIRC. Now I'm not sure if I did something wrong or not. Will try a few things and see.

[tanyongkiam]

@zapashcanon is right, the right fix is, as mentioned, to print with spaces instead of commas.

Also, the corresponding pretty printing of the datatype definition has to be changed to the new style, because the one that it prints now is parsed as a tupled datatype.

More generally, I sometimes use astPP to print code that is compatible with SML and the above changes will unfortunately break that compatibility.

[xrchz]

Note that astPP is not verified. The only verified printer is the s-expression printer. A verified printer into concrete syntax would be welcome! (verified = is a one-sided inverse for the parser)

[redianthus]

More generally, I sometimes use astPP to print code that is compatible with SML and the above changes will unfortunately break that compatibility.

If think all depend on what we want to do: being compatible with SML or with ourself (CakeML).

I can open a PR to fix the two issues (type definition and algebraic datatype constructor) if you think it's better than being SML-like.

[myreen]

I would prefer there to be a switch which determines whether astPP is to produce SML or CakeML.

[tanyongkiam]

This could be useful if we revive/extend the use of astPP