[isabelle] Constant folding during code generation from l... · Mirror: Isabelle Users Mailing List

I am running into issues with code generation in the context of nested
locales and sublocales.

Even a minimal example is rather elaborate, but focusing on the
high-level structure, the context is:

Using defines ... clauses for X, code-extractable global constants
are established. However, trying to export code for definitions from C
in Y using defines and rewrites fails because the constants from
X are not appropriately folded.

Please see below for a minimal example -- it's a toy example only, the
real application context is much more complicated and has nothing to do
with endomorphisms used in the example.

One can hack things manually as demonstrated in the example as well, but
it seems against the point of global_interpretation. Is there a way to
get the example to work without manual constant folding and provisioning
of code equations?

theory Scratch
   imports Main
begin

locale Endo =
   fixes f :: ‹'a ⇒ 'a›
   assumes ‹f=f›
begin
   definition ff where ‹ff ≡ f∘f›
end

locale EndoCopy =
   fixes h :: ‹'a ⇒ 'a›
   assumes ‹h=h›
begin
   definition hh where ‹hh ≡ h∘h›
end

locale CommutingEndos = Endo f for f :: ‹'a ⇒ 'a› +
   fixes g :: ‹'a ⇒ 'a›
   assumes ‹f ∘ g = g ∘ f›
begin
definition gg :: ‹'a ⇒ 'a› where ‹gg = g ∘ g›
end

definition p1 :: ‹nat ⇒ nat› where ‹p1 ≡ (+) 1›
definition p2 :: ‹nat ⇒ nat› where ‹p2 ≡ (+) 2›
definition p3 :: ‹nat ⇒ nat› where ‹p3 ≡ (+) 3›

sublocale CommutingEndos ⊆ EndoCopy ‹ff ∘ gg›
   by (simp add: EndoCopy.intro)

global_interpretation I0: Endo ‹p1›
   defines x = ‹I0.ff›
   by (simp add: Endo.intro p1_def)

thm I0.ff_def (* OK: x ≡ p1 ∘ p1 *)

global_interpretation I1: CommutingEndos p1 p2
   defines y = ‹I1.hh›
       and z = ‹I1.gg›
   by (simp add: CommutingEndos_axioms.intro CommutingEndos_def
Endo.intro o_def p1_def p2_def)

thm I1.gg_def (* OK: z = p2 ∘ p2 *)
thm z_def     (* z ≡ CommutingEndos.gg p2 *)

thm I1.hh_def (* BAD: I1.gg ≡ Endo.ff p1 ∘ z ∘ (Endo.ff p1 ∘ z) *)
thm y_def     (* BAD: y ≡ EndoCopy.hh (Endo.ff p1 ∘ CommutingEndos.gg
p2) *)

export_code y in OCaml (* No code equation for y *)

(* Can force it manually, but I thought the point of
global_interpretation is that
    this manual fiddling is not necessary: *)
thm y_def[folded z_def, simplified I1.hh_def, folded x_def] (* y ≡ x ∘ z
∘ (x ∘ z) *)
declare y_def[folded z_def, simplified I1.hh_def, folded x_def, code]

export_code y in OCaml (* OK *)

(* Manually adding a `rewrites` clause does not help either,
unfortunately: *)
global_interpretation I2: CommutingEndos p1 p3
   rewrites ‹Endo.ff p1 = x›
   defines y' = ‹I2.hh›
       and z' = ‹I2.gg›
   by (auto simp add: CommutingEndos_axioms.intro CommutingEndos_def
Endo.intro o_def
     p1_def p3_def x_def)

thm I2.gg_def  (* OK: z' = p3 ∘ p3 *)
thm z'_def     (* z ≡ CommutingEndos.gg p3 *)

thm I2.hh_def (* Better, but still not expected: I1.gg ≡  x ∘ z' ∘ (x ∘
z')
                  Need LHS to be folded into y'! *)
thm y'_def     (* BAD: y ≡ EndoCopy.hh (Endo.ff p1 ∘ CommutingEndos.gg
p3) *)

export_code y' in OCaml (* No code equation for y *)

(* Similar hacking still needed *)
thm y'_def[folded x_def z'_def, simplified I2.hh_def] (* y' ≡ x ∘ z' ∘
(x ∘ z') *)
lemmas y'_def[folded x_def z'_def, simplified I2.hh_def, code]

export_code y' in OCaml (* OK *)

end

Email Gateway (Feb 01 2024 at 12:42):

The explicit rewrite is definitely necessary – mixin rewrites do not
propagate along local hierarchies.

Why that still fails to apply as desired I cannot explain at the moment.
It might be that internally the composition ‹_ ∘ _› is blurred by
implicit eta-expansion which might ruin something, but that is entirely
speculative.

Email Gateway (Feb 02 2024 at 06:25):

Email Gateway (Feb 12 2024 at 19:44):

Can we follow up on this? The behaviour is rather unexpected (seeing
that hierarchies of global_interpretation do work with code
generation, as below), and cumbersome to work around.

It would be great if the example in the initial post could be supported
in Isabelle2024.

Email Gateway (Feb 17 2024 at 08:44):

Sorting out unclear behavior there requires considerable time and
concentration for a thorough analysis and if analysis suggests
modifications, these have to be discussed and evaluated diligently.

This is not realistic in a short time period. At the moment I cannot
forsee when I personally will be able to have a closer look at it.

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Constant folding during code generation from l...

Email Gateway (Jan 27 2024 at 09:04):

Email Gateway (Feb 01 2024 at 12:42):

Email Gateway (Feb 02 2024 at 06:25):

Email Gateway (Feb 12 2024 at 19:44):

Email Gateway (Feb 17 2024 at 08:44):

Email Gateway (Feb 18 2024 at 05:02):