Hi Christian,
On 21.11.2014 14:09, Christian Sternagel wrote:
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)"
Looks reasonable so far.
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?).
There was no change, our map functions always have ignored the dead
parameters. You are confusing this with phantom variables (which used to
be dead, but are now live, e.g. in "datatype 'a ref = Ref addr" from
Imperative_HOL)
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)?.
Let me cite the relevant part of my email that you refer to.
On 13.11.2014 15:40, Dmitriy Traytel wrote:
I would not care too much about such dead annotations. If a user made
a variable dead explicitly, she might be aware that this has some
disadvantages, so it is ok for some automatic tool to refuse working.
A more interesting question is if you can/want to handle datatypes
where the dead variable naturally arises, e.g., trees nested through
functions:
datatype ('a, 'b) tree = Node 'a "'b => ('a, 'b) tree"
under the assumption that you have the map function for tree which
would be contravariant in 'b, i.e. of type "('a => 'c) => ('d => 'b)
=> ('a, 'b) tree => ('c, 'd) tree". If the answer to this question is
yes, then BNF's indeed don't quite capture the right notion of maps
for you, and you might want to resort to the database collected by the
functor command. If the answer is no, this means that you do care
about the (truly) dead variables.
Now, that I see your concrete application, I believe the answer to my
question is "no". I.e. "(show, show) tree" is not an instance of show
(just as"(show, show) fun" is not). This means that you do care about
the dead parameters!
When you use the dead annotation for efficiency, guess where the
efficiency comes from---it comes mainly from not generating set
functions, generating a "smaller" map-function, and proving no (or less)
theorems about them.
This hijacks a semantic notion of being dead (which was originally used
only for contravariant parameters such as 'a in 'a => 'b) for the cause
of efficiency---of course it comes with some limitations.
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.
Thanks for the report! The tactic failure comes from the size plugin
(which we will repair soon). Temporarily one can disable the plugin to
get this declaration through.
datatype (plugins del: size) (dead 'a, 'b) dlist = DNil | DCons "'a ×
'b" "('a, 'b) dlist"
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
