Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Composing BNFs

view this post on Zulip Email Gateway (Aug 22 2022 at 15:22):

From: Lars Hupel <hupel@in.tum.de>
Dear BNF experts,

I'm looking for a simple way to obtain a composed map function given a type.

For example, given

('a + 'b) option list

the result should be a term of type

('a ⇒ 'c) ⇒ ('b ⇒ 'd) ⇒ ('a + 'b) option list ⇒ ('c + 'd) option list

It doesn't necessarily need to be a constant; instead, it could be a
simple term composition of map functions.

I found "BNF_Comp.bnf_of_typ" but I'm a little confused about all the
parameters it takes. Is there a small, canonical example somewhere?
Also, can I get "bnf_of_typ" (or something else in BNF) to produce a
bunch of terms instead of constants, typedefs and everything?

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:22):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lars,

bnf_of_typ is the right function for that. Here is an example usage:

local_setup ‹ fn lthy =>
let
val live_As = [@{typ 'a}, @{typ 'b}]
val dead_As = []

fun flatten_tyargs Ass =
map dest_TFree live_As
|> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);

val ((bnf, _), (_, lthy)) =
BNF_Comp.bnf_of_typ false BNF_Def.Do_Inline I
flatten_tyargs (map dest_TFree live_As) (map dest_TFree dead_As)
@{typ "('a + 'b) option list"}
((BNF_Comp.empty_comp_cache, BNF_Comp.empty_unfolds), lthy)
val _ = BNF_Def.map_of_bnf bnf |> Syntax.string_of_term lthy |> warning
val _ = BNF_Def.map_of_bnf bnf |> fastype_of |> Syntax.string_of_typ lthy |> warning
in
lthy
end
›

Try to play with Do_Inline vs. Dont_Inline and observe the output (whether new map constants are defined or inlined, i.e. composed terms are used).

Hope that helps,
Dmitriy

view this post on Zulip Email Gateway (Aug 22 2022 at 15:22):

From: Lars Hupel <hupel@in.tum.de>
Hi Dmitriy,

thanks for that.

val live_As = [@{typ 'a}, @{typ 'b}]
val dead_As = []

Is there a reason why I need to specify the live variables? Surely the
internal bookkeeping of BNF already knows which variables are live and
which are dead.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:22):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lars,

sure, BNFs can figure this out by themselves indeed. But then very often the variables will not be in the order in which you expect them. (Same for the dead ones.) Therefore it is better to fix the order on the caller’s side.

Cheers,
Dmitriy

view this post on Zulip Email Gateway (Aug 22 2022 at 15:22):

From: Sebastiaan Joosten <sjcjoosten@gmail.com>
Hi Dimitriy,

this is really cool! I haven't looked into the BNF_.. code yet, so I have two questions out of ignorance, that I hope are quick to answer for you:

local_setup ‹ fn lthy =>
let
val live_As = [@{typ 'a}, @{typ 'b}, @{typ 'c}]
val dead_As = []

fun flatten_tyargs Ass =
map dest_TFree live_As
|> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);

val ((bnf, _), (_, lthy)) =
BNF_Comp.bnf_of_typ false BNF_Def.Do_Inline I
flatten_tyargs (map dest_TFree live_As) (map dest_TFree dead_As)
@{typ "('a option + 'b ) list + 'c"}
((BNF_Comp.empty_comp_cache, BNF_Comp.empty_unfolds), lthy)
val _ = BNF_Def.map_of_bnf bnf |> Syntax.string_of_term lthy |> warning
val _ = BNF_Def.map_of_bnf bnf |> fastype_of |> Syntax.string_of_typ lthy |> warning
in
lthy
end
›

(* Note that I could simply use the following term, indicating that no extra functions are required: *)
term "op o (map_sum o map_option) o op o map o map_sum"

view this post on Zulip Email Gateway (Aug 22 2022 at 15:23):

From: Lars Hupel <hupel@in.tum.de>

For my particular use case, that's not a problem. But I can't find the
definition of that constant, which means I can't unfold it. Is the
definition recorded somewhere?

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:23):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Lars,

Look for "xxx_def_of_bnf" in "bnf_def.ML", for suitable values of "xxx". But you should ask yourself whether you really need to unfold it or if you shouldn't instead rely on the abstract properties given by the BNF (the xxx_of_bnf functions returning "thm").

Jasmin

view this post on Zulip Email Gateway (Aug 22 2022 at 15:23):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Sebastiaan,

On 10 Apr 2017, at 17:15, Sebastiaan Joosten <sjcjoosten@gmail.com> wrote:

Hi Dimitriy,

this is really cool! I haven't looked into the BNF_.. code yet, so I have two questions out of ignorance, that I hope are quick to answer for you:

Can you give a more precise type of the function you want? Folds (or more precisely recursors) are available for datatypes, but not for compositions of datatypes.

Those intermediate definitions are introduced to avoid large terms. The bnf_of_typ function actually returns something of type unfold_set. However the implementation of this type is not exposed, and it seems that we never needed to actually get the contents outside of the BNF_Comp structure.

Attached is a small patch that exports the internal representation of unfold_set. For some reason, I can’t push to Isabelle right now (@Lars: is there some known maintenance in Munich, or shall I contact the MTAs? Also feel free to push this.)

The theorems from the unfold_set returned by bnf_of_typ can be then used to unfold all those intermediate constants in the resulting BNF. This is best done by creating morphism and applying it using BNF_Def.morph_bnf (see some example usages in bnf_comp.ML).

Dmitriy
unfold_set.patch

view this post on Zulip Email Gateway (Aug 22 2022 at 15:23):

From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,

I checked, but unless I'm missing something, "map_def_of" is just the theorem "x = x".

The reason I'm asking about unfolding is because in my case, it's a composition of datatypes and I need to use map/constructor commutativity.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:23):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Lars,

I checked, but unless I'm missing something, "map_def_of" is just the theorem "x = x".

Of course. The constant stands for an intermediate term.

If you look at the type of "bnf_of_typ", you'll see "unfold_set" as one of the components of the result. This should contain the theorem you are looking for.

Cheers,

Jasmin

view this post on Zulip Email Gateway (Aug 22 2022 at 15:23):

From: Lars Hupel <hupel@in.tum.de>
Hi,

Attached is a small patch that exports the internal representation of unfold_set. For some reason, I can’t push to Isabelle right now (@Lars: is there some known maintenance in Munich, or shall I contact the MTAs? Also feel free to push this.)

I myself also can't log in to our usual nodes. I'll contact our admins.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:23):

From: Lars Hupel <hupel@in.tum.de>
Hi Dmitriy,

Attached is a small patch that exports the internal representation of unfold_set. For some reason, I can’t push to Isabelle right now (@Lars: is there some known maintenance in Munich, or shall I contact the MTAs? Also feel free to push this.)

thanks for the explanation and the patch. I have pushed it to the
temporary repository.

The theorems from the unfold_set returned by bnf_of_typ can be then used to unfold all those intermediate constants in the resulting BNF. This is best done by creating morphism and applying it using BNF_Def.morph_bnf (see some example usages in bnf_comp.ML).

That seems to work. I'm kind of surprised that there seems to be no
canonical way to construct a morphism based on unfolding a bunch of
theorems. For the time being, I have copied "expand_term_const" which
you in turn have copied from "expand_term_free" :-)

Cheers
Lars

Last updated: Apr 26 2024 at 04:17 UTC