Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation failing with lift_definition

Email Gateway (Nov 23 2022 at 11:33):

From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,

Consider the following:

theory Scratch imports Main begin

typedef 'v mem = ‹{ ((f::nat ⇀ 'v), (a::nat)). ∀x>a. x ∉ dom f }›
  by (rule_tac x=‹(Map.empty, 0)› in exI) auto

setup_lifting type_definition_mem

lift_definition empty :: ‹'v mem› is ‹(Map.empty, 0)› by auto
lift_definition alloc_mem :: ‹'v mem ⇒ (nat × 'v mem)› is
    ‹λm. (snd m, (fst m, 1 + snd m))›
  by (clarsimp simp add: domIff)
lift_definition write_mem :: ‹'v mem ⇒ nat ⇒ 'v ⇒ 'v mem› is
  ‹λm a v. ((fst m)(a ↦ v), 1 + a + snd m)›
  by clarsimp (metis Suc_lessD add.commute add_lessD1 domIff
option.distinct(1))
lift_definition read_mem :: ‹'v mem ⇒ nat ⇒ 'v option› is
  ‹λm a. (fst m) a› .

end

Now, code generation works for these definitions:

export_code empty read_mem write_mem in Scala

But fails with "No code equations" for alloc_mem. There appears to be
nothing out of the ordinary that would cause this failure at first glance.
Does anybody know what is wrong?

Thanks,
Dominic

Email Gateway (Nov 23 2022 at 12:09):

From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Dominic,

This is a recurrent topic. ;) This behavior occurs because alloc_mem’s return type nests the abstract type (mem) in another type (prod). In such cases, a code generator restriction prevents using the rep_eq theorem generated by lift_definition as a code equation.

You can pass the code_dt option to lift_definition to ask it to derive a different code equation that works with the code generator.

lift_definition (code_dt) alloc_mem :: ‹'v mem ⇒ (nat × 'v mem)› is
‹λm. (snd m, (fst m, 1 + snd m))›
by (clarsimp simp add: domIff)

This is documented in Kunčar's PhD thesis (https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf, Section 6.4) and in isar-ref (page 282 for the Isabelle2022 edition).

Dmitriy

Email Gateway (Nov 23 2022 at 12:39):

From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Many thanks, Dmitriy. That's fixed my problem!

Last updated: Jan 04 2025 at 20:18 UTC