Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Derive shows with List

Email Gateway (Aug 22 2022 at 17:17):

From: Peter Lammich <lammich@in.tum.de>
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
*)

Email Gateway (Aug 22 2022 at 17:17):

From: Christian Sternagel <c.sternagel@gmail.com>
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

Email Gateway (Aug 22 2022 at 18:47):

From: Mark Wassell <mpwassell@gmail.com>
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

Email Gateway (Aug 22 2022 at 18:47):

From: Christian Sternagel <c.sternagel@gmail.com>
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.

Last updated: Apr 26 2024 at 20:16 UTC