Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
Concerning Mapping.mapping xor Mapping.lookup as coercion: this lies
outside of the fragment for which we guarantee completenes (=if a term
can be coerced it will be coerced). In such cases a very simple
incomplete coercion insertion algorithm is used. E.g. in the following
example only one of the two terms will be coerced.
declare [[coercion Mapping.Mapping]]
term "f = Mapping.lookup f"
term "Mapping.lookup f = f"
So even more care is required than in the complete fragment.
Concerning the error messages: at least you should always get strictly
more information than without coercion inference (i.e. the error message
of the standard type-inference will always come first, only then
coercion inference will give additional hints). Of course, the
additional information can be distracting---maybe it should be hidden in
a popup or so). The problem of helpful type inference error messages is
not trivial, and coercions don't make it easier.
Am 28.10.2013 08:44, schrieb Andreas Lochbihler:
I haven't investigated in detail what exactly is missing. Whenever I
used mapping, I had code generation in mind, so my thinking might be a
bit biased. What I particularly like about 'a => 'b option is no
clutter: I can build new maps just from lambda abstraction and the
other usual HOL constants (if/case/Some/Option.map/Option.bind/...),
there's no need for coercing between ('a, 'b) mapping and 'a => 'b
option. Therefore, I don't have to worry where coercions are
automatically inserted. Nor do I care about what the simplifer does to
these coercions when. (By the way, if I enable automatic coercions,
the error messages for ill-typed terms sometimes do not help to
identify what's wrong at all, in particular if I got the number of
parameters of a function wrong.) Of course, these maps are not
(efficiently) executable, but I usually don't care in such situations:
I just use them inside proofs, e.g., as a witness to an existential
quantifier. In proofs, I use such maps as arguments to functions for
which I later generate code -- although not for these parameters.
There are certainly functions, lemmas and automation missing. When I
last looked at Mapping (which is already quite some time ago), I had
the impression that everything is still centered around code
generation, but inside a proof, I usually don't care about code
generation, I just want to quickly get the proof done. Although I must
say that I know one case where automation for ('a, 'b) mapping can in
principle be better than for 'a => 'b option: Element lookup is just
function application and the simplifier does not do well for equation
of the form "g (f x) = ..." where f is a free variable. With mapping,
this corresponding equation "g (lookup f x) = ..." works much better.
On 25/10/13 21:05, Florian Haftmann wrote:
Therefore, you have to switch to some other type. There are two
1. Use ('a, 'b) mapping. I recommend that you only use it for code
generation, the mapping type in its current state is not suitable for
proving lots of stuff.
once there has been the rough idea to reformulate Map.thy using a
dedicated type like in Mapping.thy. The user-visible difference would
be that element lookups need a dedicated function
lookup :: ('a, 'b) mapping => 'a => 'b option
But this could be inserted implicitly by coercions also whenever a ('a,
'b) mapping it used in place of a function.
I did not pursue this further, since my impression was that (unlike
sets) the syntax in Map.thy is not so pervasively common, so
specification requiring executable data structures can just be based on
Mapping.thy. Considering your statement about »easy going« of proofs in
Mapping.thy, maybe we have to rethink about it. Or is it just that
lemmas / automation are missing?
This archive was generated by a fusion of
Pipermail (Mailman edition) and