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

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
*From*: Christian Sternagel <c.sternagel at gmail.com>
*Date*: Thu, 24 Oct 2013 18:10:28 +0900
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

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

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