[isabelle] Derive shows with List

[Peter Lammich]

Hi,

when trying to derive a "show" class for a datatype, it fails with a
strange error if teh type has nested lists. Find attached a minimal
example.

Am I doing something wrong here?  

Thanks in advance for any help,
  Peter

Isabelle2017 with AFP:

theory Scratch
imports Main   "Show.Show_Instances"
begin

datatype 'a foo = C "'a list"

derive "show" foo

(*
deriving "show" instance for type "Scratch.foo"
generating show-function for type "Scratch.foo"
Proof failed.
 1. (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 1) x) (shows_pr p xa))))) =
    (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 0) x) (shows_pr p xa)))))
The error(s) above occurred for the goal statement⌂:
showsp_foo show⇩'⇩a p (C x) = shows_pl p ∘ shows_string ''C'' ∘
shows_space ∘ showsp_list show⇩'⇩a 1 x ∘ shows_pr p
*)

[Christian Sternagel]

Dear Peter,

thanks for reporting this issue.

Just to make it more concrete: the problem is that show⇩'⇩a is called
with precedence 0 on the left-hand side but with 1 on the right-hand side.

As to why this happens, I will have to check our code. Your datatype is
somewhat special (in comparison to our existing test-cases) that no
recursion is going on.

cheers

chris

Post by Peter Lammich
Hi,
when trying to derive a "show" class for a datatype, it fails with a
strange error if teh type has nested lists. Find attached a minimal
example.
Am I doing something wrong here?  
Thanks in advance for any help,
  Peter
theory Scratch
imports Main   "Show.Show_Instances"
begin
datatype 'a foo = C "'a list"
derive "show" foo
(*
deriving "show" instance for type "Scratch.foo"
generating show-function for type "Scratch.foo"
Proof failed.
 1. (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 1) x) (shows_pr p xa))))) =
    (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 0) x) (shows_pr p xa)))))
showsp_foo show⇩'⇩a p (C x) = shows_pl p ∘ shows_string ''C'' ∘
shows_space ∘ showsp_list show⇩'⇩a 1 x ∘ shows_pr p
*)

[Mark Wassell]

Hello,

I get a similar problem to this. When doing:

datatype 'a foo = C "nat*nat"
derive "show" foo

I get the output:

deriving "show" instance for type "PrettyPrint.foo"
generating show function for type "PrettyPrint.foo"
Proof failed.
1. (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_prod 1
(map_prod (showsp_nat 0) (showsp_nat 0) x) (shows_pr p xa))))) =
(λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_prod 1
(map_prod (showsp_nat 1) (showsp_nat 1) x) (shows_pr p xa)))))
The error(s) above occurred for the goal statement⌂:
showsp_foo p (C x) = shows_pl p ∘ shows_string ''C'' ∘ shows_space ∘
showsp_prod showsp_nat showsp_nat 1 x ∘ shows_pr p

Cheers

Mark

Post by Christian Sternagel
Dear Peter,
thanks for reporting this issue.
Just to make it more concrete: the problem is that show⇩'⇩a is called
with precedence 0 on the left-hand side but with 1 on the right-hand side.
As to why this happens, I will have to check our code. Your datatype is
somewhat special (in comparison to our existing test-cases) that no
recursion is going on.
cheers
chris

Post by Peter Lammich
Hi,
when trying to derive a "show" class for a datatype, it fails with a
strange error if teh type has nested lists. Find attached a minimal
example.
Am I doing something wrong here?
Thanks in advance for any help,
Peter
theory Scratch
imports Main "Show.Show_Instances"
begin
datatype 'a foo = C "'a list"
derive "show" foo
(*
deriving "show" instance for type "Scratch.foo"
generating show-function for type "Scratch.foo"
Proof failed.
1. (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 1) x) (shows_pr p xa))))) =
(λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 0) x) (shows_pr p xa)))))
showsp_foo show⇩'⇩a p (C x) = shows_pl p ∘ shows_string ''C'' ∘
shows_space ∘ showsp_list show⇩'⇩a 1 x ∘ shows_pr p
*)

[Christian Sternagel]

Dear Mark,

thanks for your report.

I am aware of the problem but not quite sure how to solve it (after
investigating it for a few hours some months ago). Without getting into
details (which I would have to refresh by looking at the code again),
this issue is caused by the desire to be able to safe perentheses by
using a precedence.

On the one hand, I do not want to give up this feature. On the other
hand it causes some loss of uniformity that I didn't recognize before.

Unfortunately, I do at the moment not have the resources (time, or
manpower other than myself) to work on it.

I will come back to this issue eventually, but please don't hold your
breath.

cheers

chris

PS: If anybody else is interested in working on this issue, please drop
me a line, so that we avoid multiplication of effort.

Post by Mark Wassell
Hello,
datatype 'a foo = C "nat*nat"
derive "show" foo
deriving "show" instance for type "PrettyPrint.foo"
generating show function for type "PrettyPrint.foo"
Proof failed.
 1. (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_prod 1
(map_prod (showsp_nat 0) (showsp_nat 0) x) (shows_pr p xa))))) =
    (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_prod 1
(map_prod (showsp_nat 1) (showsp_nat 1) x) (shows_pr p xa)))))
showsp_foo p (C x) = shows_pl p ∘ shows_string ''C'' ∘ shows_space ∘
showsp_prod showsp_nat showsp_nat 1 x ∘ shows_pr p
Cheers
Mark
Dear Peter,
thanks for reporting this issue.
Just to make it more concrete: the problem is that show⇩'⇩a is called
with precedence 0 on the left-hand side but with 1 on the right-hand side.
As to why this happens, I will have to check our code. Your datatype is
somewhat special (in comparison to our existing test-cases) that no
recursion is going on.
cheers
chris

Post by Peter Lammich
Hi,
when trying to derive a "show" class for a datatype, it fails with a
strange error if teh type has nested lists. Find attached a minimal
example.
Am I doing something wrong here?  
Thanks in advance for any help,
  Peter
theory Scratch
imports Main   "Show.Show_Instances"
begin
datatype 'a foo = C "'a list"
derive "show" foo
(*
deriving "show" instance for type "Scratch.foo"
generating show-function for type "Scratch.foo"
Proof failed.
 1. (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 1) x) (shows_pr p xa))))) =
    (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 0) x) (shows_pr p xa)))))
showsp_foo show⇩'⇩a p (C x) = shows_pl p ∘ shows_string ''C'' ∘
shows_space ∘ showsp_list show⇩'⇩a 1 x ∘ shows_pr p
*)