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

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!



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