Hanno Becker (Jan 12 2024 at 09:28): Hanno Becker (Jan 12 2024 at 09:28):Hi all. As documented e.g. in 3.2 of the 2013 article https://isabelle.in.tum.de/~haftmann/pdf/data_refinement_in_isabelle_hol_haftmann_krauss_kuncar_nipkow.pdf, code generation does not support code equations for lifted definitions resulting in compound abstract types. Here's a simple example:
typedef nat_pos = ‹{ n :: nat . n > 0 }›
by (simp add: gt_ex)
setup_lifting nat_pos.type_definition_nat_pos
definition nat_minus_one :: ‹nat ⇒ nat option›
where ‹nat_minus_one n ≡ if n - 1 > 0 then Some (n - 1) else None›
lift_definition nat_pos_minus_one :: ‹nat_pos ⇒ nat_pos option›
is ‹nat_minus_one› by (auto simp add: nat_minus_one_def)
export_code nat_pos_minus_one in OCaml (* No code equations for nat_pos_minus_one *)
I am aware that one can work around this by realizing nat_pos option as a subtype of nat option, but this quickly becomes impractical in non-toy examples.
Reading loc.cit. above suggests that the issue is with the code generator having to guarantee that Abs_C is only ever applied to terms satisfying the subtype invariant. However, the lift_definition nat_pos_minus_one ... command above _does_ already generate the correct proof obligation here: ⋀nat. 0 < nat ⟹ pred_option ((<) 0) (nat_minus_one nat). This being discharged, it confuses me that the resulting theorem nat_pos_minus_one ≡ map_fun Rep_nat_pos (map_option Abs_nat_pos) nat_minus_one is not used as a code equation. It seems that the hard part is already done?
Has there been any progress on this limitation since 2013? Are there any other workaround than realizing nat_pos option as a subtype of nat option? I'm OK with a bit of ML hacking as well, so long as it can be done atop of the existing ML interfaces.
Hanno Becker (Jan 12 2024 at 10:38):The following would work:
definition [code del]: ‹Abs_nat_pos' ≡ Abs_nat_pos›
code_printing constant Abs_nat_pos' ⇀ (OCaml) "Abs'_nat'_pos"
declare nat_pos_minus_one_def[folded Abs_nat_pos'_def, code]
export_code nat_pos_minus_one in OCaml
Of course, code_printing is generally unsound, but here we are only forcing instances of Abs_C in definitions emitted by lift_definition, and those [so it seems to me] have already been proved to preserve the invariant. So the above seems sound... or am I missing something? If it is indeed sound, it is unclear to me why the code generator doesn't do this automatically.
Mathias Fleury (Jan 12 2024 at 11:03):I am not sure what the question is, but https://isabelle.in.tum.de/doc/codegen.pdf, Section 3.3?
Mathias Fleury (Jan 12 2024 at 11:04):Or is the point that you do not want to see the new types at all?
Hanno Becker (Jan 12 2024 at 11:04):The question is, primarily: Is there a way to extract code for examples like nat_pos_minus_one above, which does not require the definition of intermediate types? And, second, why the code generator does not export code equations already, given that lift_definition does seem to generate the relevant side conditions correctly even when the result type is compound.
Mathias Fleury (Jan 12 2024 at 11:17):Typedef supports any set, so I do not think a general translation is possible:
typedef nat_pos = ‹(λn. (SOME x. x > n)) ` { n :: nat . n > 0 }›
by (simp add: gt_ex)
I don't follow yet -- can you elaborate this into an example? Note that I am assuming that there is a concrete and extractable 'blueprint' definition nat_minus_one :: ‹nat ⇒ nat option› for the function nat_pos => nat_pos option I'm after. lift_definition already generates the right obligations, so why is nat_pos_minus_one ≡ map_fun Rep_nat_pos (map_option Abs_nat_pos) nat_minus_one not accepted as a code equation afterwards?
Mathias Fleury (Jan 12 2024 at 11:23):You cannot generate code for Abs_nat_pos in general
Hanno Becker (Jan 12 2024 at 11:29):It's understood that Abs_C should only be code-extracted when it can be argued that its inputs will satisfy the respective invariant. My point is that this _is_ being proved as part of lift_definition, regardless of whether the target is a compound type or not. But when it is, somehow no code equation is being generated.
Hanno Becker (Jan 12 2024 at 11:36):Maybe I wasn't clear enough: The issue is _wholly_ about lift_definition when the target of the function is a type expression involving the abstract type, but where the abstract type does not appear at the top level.
The following, for example, works absolutely fine:
lift_definition nat_pos_minus_one' :: ‹nat_pos ⇒ nat_pos›
is ‹λn. if n - 1 > 0 then n - 1 else 42› by auto
export_code nat_pos_minus_one'
But as soon as you use any compound type, like 'a + nat_pos, nat_pos option, nat_pos x 'b, or whatever -- subsequent code generation doesn't work anymore, even though lift_definition itself is still generating the right (a) conditions and (b) equations.
Hanno Becker (Jan 14 2024 at 14:46):For the record: lift_definition (code_dt) does the trick.
Last updated: Apr 27 2024 at 16:16 UTC