Re: [isabelle] Derive shows with List



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.