[isabelle-dev] BNF: dead or alive?

[Christian Sternagel]

Dear list,

sorry for the subject ;)

René and I are currently at adapting the Show(_Generator) entry of the 
AFP to the new datatype package. And again we stumbled across some 
difficulties we already encountered when adapting the Order_Generator 
(and which are not resolved yet).

I think it best to first demonstrate what I intend to achieve and why 
our "recipe" looks as it does. So please bear with me.

The goal is, for a given datatype, say "'a list", to automatically 
generate a show-function, i.e., of type

(nat => 'a => shows) => nat => 'a list => shows

that can be used to convert lists into a string-representation (where 
"shows" is an abbreviation for "string => string" and the additional 
"nat" argument is there to indicate whether the result should be 
parenthesized).

Moreover this construction should work via plain 'primrec' (since 
otherwise the jungle of cong-rules and set-simps that looms ahead is too 
daunting). Lets come back to lists:

primrec showsp_list :: "('a => nat => shows) => nat => 'a list => shows"
where
   "showsp_list s p Nil = shows_string ''Nil''" |
   "showsp_list s p (Cons x xs) =
     shows_pl p o shows_string ''Cons'' o shows_space o
       s 1 x o shows_space o
       showsp_list s 1 xs o
     shows_pr p"

Well, this works fine. Now a slightly more complex datatype

datatype 'a tree = Tree 'a "'a tree list"

and its show-function:

primrec showsp_tree :: "(nat ⇒ 'a ⇒ shows) ⇒ nat ⇒ 'a tree ⇒ shows"
where
   "showsp_tree s p (Tree x y) =
     shows_pl p o shows_string ''Tree'' o shows_space o
       showsp_list (showsp_tree s) 1 y o
     shows_pr p"

But wait a minute. This results in:

primrec error:
   Invalid map function in "showsp_list (showsp_tree s) 1"

Which is the reason for doing everything a little bit different. Namely, 
we start with show-functions that assume that all type parameters where 
already replaced by "shows" (we call them partial show-functions, 
because parts of their argument are already turned into "shows"). Then 
the above turns into:

primrec pshowsp_list :: "nat ⇒ shows list ⇒ shows"
where
   "pshowsp_list p Nil = shows_string ''Nil''" |
   "pshowsp_list p (Cons x xs) =
     shows_pl p o shows_string ''Cons'' o shows_space o
       x o shows_space o
       pshowsp_list 1 xs o
     shows_pr p"

primrec pshowsp_tree :: "nat ⇒ shows tree ⇒ shows"
where
   "pshowsp_tree p (Tree x y) =
     shows_pl p o shows_string ''Tree'' o shows_space o
       pshowsp_list 1 (map (pshowsp_tree 1) y) o
     shows_pr p"

And we obtain our originally desired functions by

definition "showsp_list s p xs = pshowsp_list p (map (s 1) xs)"
definition "showsp_tree s p t = pshowsp_tree p (map_tree (s 1) t)"

This seems to work pretty well as long as there are no dead type 
parameters involved. *HOWEVER*, how should we go about turning some 
datatype "(dead 'a, 'b) dt" into "(shows, shows) dt" if their is no way 
of mapping the "'a"?

In general, why not create map-functions that allow to map over *all* 
type parameters. (As I understand it, this was done just a few month 
ago. What where the reasons for the change?).

When we last brought up this point, Dmitriy suggested that users that 
use "dead" in their datatypes know what they are doing and that it is 
not a problem when packages "break" on such types. However, in IsaFoR we 
sometimes kill type parameters just because otherwise the (huge) 
datatype declaration would take to much resources (in terms of memory 
and time). Still, there is no compelling reason (as far as I see) to not 
having compare- and/or show-functions for those types. Wouldn't it be 
generally useful to always have "total" map-functions (and appropriately 
plug in "id"s in the internal BNF constructions)?.

cheers

chris

Maybe unrelated: The datatype declaration

datatype (dead 'a, 'b) dlist = DNil | DCons "'a" "'b" "('a, 'b) dlist"

work, but

datatype (dead 'a, 'b) dlist = DNil | DCons "'a × 'b" "('a, 'b) dlist"

results in an internal tactic failure.