Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping

Dear Christian,

Thanks for testing. I have a few suggestions for your example. You find attached the updated theory file.

1. Mapping_match_term_list:
You can prove this lemma without induction: by transfer simp suffices if the simplifier already knows option_map_id.

2. 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 AST
>    data 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.


On 25/10/13 06:50, Christian Sternagel wrote:
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 σ = 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 = (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);



On 10/25/2013 12:19 AM, Ondřej Kunčar wrote:
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.


On 10/24/2013 03:43 PM, Christian Sternagel wrote:
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.



On 10/24/2013 06:59 PM, Ondřej Kunčar wrote:
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.


On 10/24/2013 11:35 AM, Peter Lammich wrote:
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.


[1]: Peter Lammich, Automatic Data Refinement, Proc. of ITP 2013

On Do, 2013-10-24 at 18:10 +0900, Christian Sternagel wrote:
Dear all (especially Andreas ;)),

is it possible to automatically get efficient code when code
a function involving the "('a, 'b) map" type (i.e., "'a => 'b

If I import AFP/Containers I can have this for "('a, 'b) mapping"
is a type-copy of "('a, 'b) map").

But in the actual formalization "('a, 'b) map" is more convenient to
since we have nice syntax like "m x" for lookup and "m (x |-> t)" for

Since according to the user guide the above is possible w.r.t. "'a
I was wondering what the obstacle is for "('a, 'b) map" (or maybe I
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
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!



Attachment: Matching_Test.thy
Description: application/extension-thy

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.