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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
