Email Gateway (Aug 19 2022 at 12:11): Email Gateway (Aug 19 2022 at 12:11):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all (especially Andreas ;)),
is it possible to automatically get efficient code when code generating
a function involving the "('a, 'b) map" type (i.e., "'a => 'b option").
If I import AFP/Containers I can have this for "('a, 'b) mapping" (which
is a type-copy of "('a, 'b) map").
But in the actual formalization "('a, 'b) map" is more convenient to use
since we have nice syntax like "m x" for lookup and "m (x |-> t)" for
update.
Since according to the user guide the above is possible w.r.t. "'a set",
I was wondering what the obstacle is for "('a, 'b) map" (or maybe I just
misunderstood something).
More concretely, what is your advice for a function like
match_list ::
(('f, 'v) term * ('f, 'v) term) list =>
('v => ('f, 'v) term option) => ('f, 'v) subst
where "match_list E Map.empty" gives a matcher for all equations in "E".
Would you change this to use "('v, ('f, 'v) term) mapping" instead, or
is there a way to get efficient code as it is? Thanks in advance!
cheers
chris
Email Gateway (Aug 19 2022 at 12:11):From: Peter Lammich <lammich@in.tum.de>
Hi Christian.
The problem is, that ('a,'b) map is just syntactic sugar for the type
'a => 'b option. The code-generator replacement of types by efficient
implementations only works for types represented by a single
type-constant (like ('a,'b) mapping or 'a set).
Moreover, note that, in general, you do not want to translate all
occurences of "'a -> 'b option" by a map implementation, as there are
also functions that return option-values, which are intended to be
translated as functions.
The automatic refinement framework [1] tries to tackle this problem,
however, it has to be employed manually before code generation, and
usually requires some setup overhead.
In order to use Containers, I believe that you should transform your
functions to use mapping. Maybe the transfer+lifting package of Brian
and Ondra may help you to automate this task.
Best,
Peter
[1]: Peter Lammich, Automatic Data Refinement, Proc. of ITP 2013
Email Gateway (Aug 19 2022 at 12:11):From: Christian Sternagel <c.sternagel@gmail.com>
Ah, right. I somehow repressed that "'a set" is no longer a type
synonym, which was the only reason why I was wondering about "('a, 'b)
map". Now everything is clear (including that my question was stupid ;)).
cheers
chris
Email Gateway (Aug 19 2022 at 12:12):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Christian,
The difference between 'a set and ('a, 'b) map is that set is a single type constructor of
its own, whereas map is just a type synonym for a compount type expression. Unfortunately,
the code generator supports only data refinement for single type constructors, on which
Containers relies. So there is no way to get this to work directly.
Therefore, you have to switch to some other type. There are two options:
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. In my AFP entry
Native Word (in AFP-devel: http://afp.sourceforge.net/devel-entries/Native_Word.shtml),
the userguide describes how one can easily deal with such type copies thanks to
transfer/lifting. I will see whether I can make it work for mapping, too.
Peter Lammics's Autoref tool (also in AFP-devel:
http://afp.sourceforge.net/devel-entries/Automatic_Refinement.shtml) also provides some
automation to specialise maps to efficient data structures. Internally, it produces copies
of your functions that directly operate on the implementation type (like a RBT).
Best,
Andreas
Email Gateway (Aug 19 2022 at 12:12):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Christian,
Peter has already explained the situation in general. I just want to add
that Lifting/Transfer can indeed help you a bit in moving your
specification from 'a => 'b option to ('a, 'b) mapping. Please see
Chapter 4 in our ITP 2013 paper: Data Refinement in Isabelle/HOL.
Best,
Ondrej
Email Gateway (Aug 19 2022 at 12:12):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
Thanks for the useful answers. For my concrete case: does
"lift_definition" also work for recursive functions (whith "match_list"
is). With my first attempt using "lift_definition" I just got a
"wrapper" around the recursive function that changed the type, which
doesn't solve the efficiency problem.
cheers
chris
Email Gateway (Aug 19 2022 at 12:12):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Christian,
yes, it can. I wrote some pre- and postprocessing to make the Transfer.transferred work
better with maps (theory attached, works with 2013-1-RC3 and Containers in AFP/devel).
There's a small example. Can you check whether that works for you in general? If so, it
might be a good idea to add this to Containers or even HOL/Library.
Best,
Andreas
Map_To_Mapping.thy
Email Gateway (Aug 19 2022 at 12:12):From: Ondřej Kunčar <kuncar@in.tum.de>
lift_definition gives you a logical definition of the new function. But
you have to still provide a code equation for this new function (as it
is described in the paper I've already referred to).
Then you have two options:
A) state the new code equation by yourself and prove it by transfer
(Isabelle 2013).
B) Since Isabelle 2013-1, there is a limited support for transferring
"in the other direction" by the attribute Transfer.transferred. The
problem in this solution is that the raw terms for map operations are
very general terms like term application (for map lookup) and so on.
Andreas showed us in his file a trick that actually Peter Lammich does
in his autoref framework, namely rewriting these term applications to an
ad-hoc constants by simplifier and then using Transfer.transferred. The
question is, of course how, much this solution scale. I am curious to
hear some report about that from you.
Ondrej
Email Gateway (Aug 19 2022 at 12:12):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Andreas and Ondřej,
here is my "report" ;) (I did however not systematically investigate my
options, but stopped immediately after having the first working solution).
For ease of reference please consult the attached theory file
(Matching_Test) which is (together with Andreas' Map_To_Mapping)
self-contained but is only concerned with code generation; thus a
"sorry" and no soundness or completeness statements for matching (but
this all exists of course on my local machine as part of IsaFoR).
A short explanation of the used functions and what I intended to do with
them:
- match_term_list: matching on lists of term pairs, but with an
accumulator that builds the result; thus depending on the initial value
of this accumulator this might not really compute a matcher
- match_list: the above where the accumulator is initialized to the
empty map (thus it really is matching on the given list of term pairs)
- for code generation only "match_list" is important (since
"match_term_list" is just an auxiliary function that is not used
directly); hence my goal was to get efficient code for "match_list"
- first get an efficient variant of "match_term_list" (called
"match_term_list'" and then prove a code equation which replaces
"match_term_list" inside the definition of "match_list" by
"match_term_list'" (together with necessary glue); what I wanted to
avoid at all cost, was to have to create a duplicate of "match_list" for
code generation (since than I would also have to "transfer" all existing
proofs to this constant)
Since I'm a newbie w.r.t. to lifting/transfer (well, I've read about it,
but never used it myself) I can only give some comments (which might be
trivial):
Andreas' "transferred_mapping" attribute worked "as advertised" in order
to get code equations for "match_term_list'"!
Afterwards I manually proved that
match_term_list E σ =
Option.map Mapping.lookup (match_term_list' E (Mapping σ))
(maybe this could also be done automatically?) and finally the code
equation for "match_list"
match_list E =
Option.map (subst_of_map undefined ∘ Mapping.lookup)
(match_term_list' E Mapping.empty)
I could have stopped after the first equation, but in the generated code
"Mapping sigma" was used to initialize "match_term_list" which I
understood to mean that the generated code would actually not use an
efficient version of maps, since maps are represented by an AST
data Mapping a b = Assoc_List_Mapping (DAList.Alist a b)
| RBT_Mapping (RBT_Mapping2.Mapping_rbt a b) | Mapping (a -> Maybe b);
cheers
chris
Matching_Test.thy
Email Gateway (Aug 19 2022 at 12:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
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?
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
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.
Andreas
Email Gateway (Aug 19 2022 at 12:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Christian,
Thanks for testing. I have a few suggestions for your example. You find attached the
updated theory file.
Mapping_match_term_list:
You can prove this lemma without induction: by transfer simp suffices if the simplifier
already knows option_map_id.
You can also use [transferred_mapping] to replace constants with lifted constants in
code equations of other constants, not just to transfer the code equations of lifted
constants. Concretely, if you also lift subst_of_map, then you get all your code equations
automatically.
However, [transferred_mapping] requires that all type variables in key/value positions
have sort type. Your definition theorem of subst_of_map does not adhere to that because
you have not specified the type of subst_of_map. Therefore, I have added the type signature.
I could have stopped after the first equation, but in the generated code "Mapping sigma"
was used to initialize "match_term_list" which I understood to mean that the generated
code would actually not use an efficient version of maps, since maps are represented by
an ASTdata Mapping a b = Assoc_List_Mapping (DAList.Alist a b)
| RBT_Mapping (RBT_Mapping2.Mapping_rbt a b) | Mapping (a -> Maybe b);
Yes, that's right. If you use the constant Mapping (from theory Mapping) in code equations
explicitly, then you specify that this map should be implemented with closures, i.e., you
override the mechanism that automatically selects a suitable implementation.
Best,
Andreas
Matching_Test.thy
Email Gateway (Aug 19 2022 at 12:14):From: Dmitriy Traytel <traytel@in.tum.de>
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_enabled]]
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.
Dmitriy
Email Gateway (Aug 19 2022 at 12:39):From: Makarius <makarius@sketis.net>
Concerning the "popup or so" you could experiment with Pretty.text_fold
(although the fold will be always open by default in currently published
Isabelle versions).
The Isabelle Pretty module started out as implementation of Oppen-style
pretty-printing by Larry Paulson, but it has acquired more and more
logical markup facilities over the years (e.g. Pretty.markup,
Pretty.paragraph, Pretty.item).
The full potential of this is still unused. (Display of advanced markup
requires a proper PIDE front-end.)
Makarius
Email Gateway (Aug 19 2022 at 12:40):From: Dmitriy Traytel <traytel@in.tum.de>
Thanks for the hint. There result of my experiments are in the
development repository (2bbcbf8cf47e).
It would be nice if the default status (folded or not) could be
indicated by a parameter to Pretty.text_fold (and respected by the
front-end).
Dmitriy
Email Gateway (Aug 19 2022 at 12:40):From: Makarius <makarius@sketis.net>
I will take a look soon, and continue this thread on isabelle-dev.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC