Re: [isabelle] Derive shows with List



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.

On 11/22/2018 02:23 PM, Mark Wassell wrote:
> 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
> 
> On Fri, 18 May 2018 at 11:52, Christian Sternagel <c.sternagel at gmail.com
> <mailto:c.sternagel at gmail.com>> wrote:
> 
>     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
> 
>     On 05/18/2018 12:11 PM, Peter Lammich wrote:
>     > 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
>     > *)
>     >
> 




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