Dear All,
I am trying re-use some demo code that I wrote some years ago and am getting different output from what I previously got.
A cut-down version of the code is as follows:
local datatype THEOREM = D of (int * int); in type THEOREM = THEOREM; infix D; fun axiom m = if m <> 0 then m D m else raise NOT_ALLOWED; end; axiom 1;
The output I used to get was:
infix 0 D eqtype THEOREM val axiom = fn: int -> THEOREM val it = 1 D 1: THEOREM
The output I now get is:
infix 0 D eqtype THEOREM val axiom = fn: int -> THEOREM val it = D (1, 1): THEOREM
Can I do something to persuade the pretty-printer to use infix notation for the constructor D? (In a real application, I would install my own pretty-printer for the type THEOREM, but that would be an annoying distraction in the talk that the demo code accompanies.)
Regards,
Rob.
Apologies, a line from the cut-down example went missing. It should read:
local datatype THEOREM = D of (int * int); in type THEOREM = THEOREM; exception NOT_ALLOWED; infix D; fun axiom m = if m <> 0 then m D m else raise NOT_ALLOWED; end;
On 31 Oct 2024, at 21:42, Rob Arthan <rda at lemma-one.com> wrote:
Dear All,
I am trying re-use some demo code that I wrote some years ago and am getting different output from what I previously got.
A cut-down version of the code is as follows:
local datatype THEOREM = D of (int * int); in type THEOREM = THEOREM; infix D; fun axiom m = if m <> 0 then m D m else raise NOT_ALLOWED; end; axiom 1;
The output I used to get was:
infix 0 D eqtype THEOREM val axiom = fn: int -> THEOREM val it = 1 D 1: THEOREM
The output I now get is:
infix 0 D eqtype THEOREM val axiom = fn: int -> THEOREM val it = D (1, 1): THEOREM
Can I do something to persuade the pretty-printer to use infix notation for the constructor D? (In a real application, I would install my own pretty-printer for the type THEOREM, but that would be an annoying distraction in the talk that the demo code accompanies.)
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Hi Rob, Pretty printing of datatypes changed some years ago; I can't remember exactly when.
Originally all the printing was done at run-time but that meant that the type information and all the environments had to be reachable at run-time. That could be very large. I changed it so that a default print function was generated for a datatype when the datatype was declared. I have a feeling that the old version did indeed handle infix constructors but that could have been removed.
Regards, David
On 31/10/2024 21:42, Rob Arthan wrote:
Dear All,
I am trying re-use some demo code that I wrote some years ago and am getting different output from what I previously got.
A cut-down version of the code is as follows:
local datatype THEOREM = D of (int * int); in type THEOREM = THEOREM; infix D; fun axiom m = if m <> 0 then m D m else raise NOT_ALLOWED; end; axiom 1;
The output I used to get was:
infix 0 D eqtype THEOREM val axiom = fn: int -> THEOREM val it = 1 D 1: THEOREM
The output I now get is:
infix 0 D eqtype THEOREM val axiom = fn: int -> THEOREM val it = D (1, 1): THEOREM
Can I do something to persuade the pretty-printer to use infix notation for the constructor D? (In a real application, I would install my own pretty-printer for the type THEOREM, but that would be an annoying distraction in the talk that the demo code accompanies.)
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 03/11/2024 18:25, David Matthews wrote:
Originally all the printing was done at run-time but that meant that the type information and all the environments had to be reachable at run-time.? That could be very large.? I changed it so that a default print function was generated for a datatype when the datatype was declared.? I have a feeling that the old version did indeed handle infix constructors but that could have been removed.
That was 15 years ago. See the following proof in the Isabelle history:
changeset: 33545:d8903f0002e5 user: wenzelm date: Tue Nov 10 13:05:35 2009 +0100 files: src/Pure/ML-Systems/install_pp_polyml-5.3.ML description: home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
https://isabelle-dev.sketis.net/rISABELLEd8903f0002e5
Makarius
David, Makarius,
Thanks for the reminders. I?ll sneak a custom pretty-printer into my demo code.
Regards,
Rob.
On 3 Nov 2024, at 17:39, Makarius <makarius at sketis.net> wrote:
On 03/11/2024 18:25, David Matthews wrote:
Originally all the printing was done at run-time but that meant that the type information and all the environments had to be reachable at run-time. That could be very large. I changed it so that a default print function was generated for a datatype when the datatype was declared. I have a feeling that the old version did indeed handle infix constructors but that could have been removed.
That was 15 years ago. See the following proof in the Isabelle history:
changeset: 33545:d8903f0002e5 user: wenzelm date: Tue Nov 10 13:05:35 2009 +0100 files: src/Pure/ML-Systems/install_pp_polyml-5.3.ML description: home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
https://isabelle-dev.sketis.net/rISABELLEd8903f0002e5
Makarius
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
rda＠lemma-one.com