Re: [isabelle] Opaque ascription for SML code generation



Thanks to Florian, Makarius and David for the explanations.

Jørgen

-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of David Matthews
Sent: 13. juni 2016 13:36
To: Makarius; cl-isabelle-users at lists.cam.ac.uk
Cc: PolyML mailing list
Subject: Re: [isabelle] Opaque ascription for SML code generation

Pretty-printing isn't part of the ML standard so it's not always clear how to do it properly.  There have been various changes over the years. 
In particular, printing exception packets is difficult because the packet can contain values of types that exist only where the exception is raised.  In the example below, "t" may not actually be exported from the signature.  So, Poly/ML puts the print function that applies where the exception is raised into the exception packet and uses that if it needs to print the packet.  There are no plans to change this.

There have been some changes around the printing of types exported through opaque matching.  When a structure matches a signature containing a type through opaque matching the semantics says that this creates a new type "name".  Poly/ML creates a new ref to hold the pretty print function for the new type.  Previously this was initialised to the pretty print function for the implementing type but this was changed in
5.6.1 to default to printing "?".  It later became clear that this was too restrictive when the signature contained a datatype (e.g. "test" 
below) so there was a further change in commit 29985b1c in git master. 
So now if you install pretty printers both within the structure, (*1*) below, for the exception, and outside the signature (*2*) it will work as you expect.

David

On 12/06/2016 15:22, Makarius wrote:
> After the Isabelle2016 release, we have discontinued SML/NJ and old 
> versions of Poly/ML, so there is a bit more flexibility now in 
> canonical patterns for Isabelle/ML.
>
> The example with structure A3 from above is the difficult one, notably 
> the situation "does not work (overrides pp for int)". Defining the pp 
> outside of the structure basically works, but exceptions are not 
> printed correctly. This is how the problem with opaque ascription was 
> discovered many years ago, and the abstype solution took over.
>
>
> Here is an update of the example A3 from Stackoverflow above, using
> Isabelle2016 with its bundled Poly/ML 5.6:
>
> ML <
> structure A :>
> sig
>   type t
>   exception BAD of t
>   datatype test = Test of t
>   val a: t
>   val print: t -> string
> end =
> struct
>
> type t = int
>
> exception BAD of t
> datatype test = Test of t
>
> val a = 42
>
> fun print i = "{" ^ Int.toString i ^ "}"
>
> (*1*)
> (*val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn x => 
> PolyML.PrettyString (print x))*) end;
>
> (*2*)
> (*val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn x => 
> PolyML.PrettyString (A.print x))*) >
>
> ML <A.a; A.Test A.a; A.BAD A.a>
>
>
> This leads to a mix of results, depending on the place where the 
> pretty printer is installed.
>
> I still don't see how to get a simple and robust pretty printer setup, 
> so we can't use opaque ascription - unless David Matthews wants to 
> refine that again for a future release of Poly/ML.
>
>
> 	Makarius
>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.