irvin (Jan 03 2025 at 17:04): irvin (Jan 03 2025 at 17:04):Hi all. I was trying to use @Lars Hupel codegen for some examples and it failed. The reason was due to the issue of hupel code generation seeming to only work for function defined with fun since it requires the function induction theorem for a termination.
As a result I was wondering if either the code generator or function package could be modified to support proving that a set of code equations terminate since I believe that would be useful even for the trusted code generator.
I know i can just modify hupel's code generator to redefine a fun and use code_unfold as a workaround.
irvin (Jan 03 2025 at 17:04):Some examples that failed to generate was the If and also the equal generated by free_constructors.
(*"If P x y ≡ (THE z::'a. (P = True ⟶ z = x) ∧ (P = False ⟶ z = y))"*)
embed If' is If
oops
primrec primIf where
"primIf True a b = a" |
"primIf False a b = b"
embed primIf' is primIf
oops
fun funIf where
"funIf True a b = a" |
"funIf False a b = b"
embed funIf' is funIf (*Only this works*)
Code in question used to get induction theorem
val fun_induct = Option.mapPartial #inducts (try (Function.get_info lthy') (hd const_terms))
val bnf_induct = induct_of_bnf_const lthy' (hd const_terms)
val inducts = merge_options (fun_induct, bnf_induct)
val _ =
if is_none inducts andalso length simps > 1 then
warning ("No induction rule found (could be problematic). Did you run this through declassify?")
else ()
I cannot help you with the issue, but one remark: it is not possible to define if with a function because the arguments are evaluated (for example if b = 0 then 0 else a / b should not raise an exception but will with primIf)
irvin (Jan 05 2025 at 08:25):The main issue more right now isabelle code generator does not check that a set of code equations terminate and allows arbitrary code equations
irvin (Jan 05 2025 at 08:33):I would it to be possible to have a standardized way of proving that the code equations i give to a code generator terminate
irvin (Jan 05 2025 at 08:44):definition
"foo a = a"
declare foo_def[code del]
lemma nonterm[code]: "foo a = foo a"
by (fact refl)
export_code foo in SML
Hi @irvin! You have identified the problem correctly. The "plain" code generator admits non-terminating code equations, but the CakeML generator does not. If you define a function using fun (or with function and prove termination), it should work. In some situations, it will also try to guess a termination proof, but that is far from reliable. So if you want to use custom code equations for a function f, it's best if you just define them as a new fun f' and prove f = f'.
irvin (Jan 05 2025 at 16:58):btw. The code generator failure came from trying to generate code from the HOL-IMP.AExp and this function fails even when i modified to use nat
fun plus :: "aexp ⇒ aexp ⇒ aexp" where
"plus (N i⇩1) (N i⇩2) = N(i⇩1+i⇩2)" |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
"plus a (N i) = (if i=0 then a else Plus a (N i))" |
"plus a⇩1 a⇩2 = Plus a⇩1 a⇩2"
it fails due to not being able to embed If and (=). manually doing it is hacky and not scalable. I would kinda like it to work and once i fix it up to work with the new cakeml semantics (unverified for now). Isabelle code can be used for cakeml benchmarks.
Lars Hupel (Jan 05 2025 at 17:03):I can't remember if using = means that you have to run it through declassify first (probably yes)
irvin (Jan 05 2025 at 17:21):Lars Hupel said:
I can't remember if using
=means that you have to run it throughdeclassifyfirst (probably yes)
the issue seems = is generated by free_constructors and it does not provide an fundef_cong/induction theorem.
definition eq_nat :: "nat ⇒ nat ⇒ bool" where
"eq_nat a b = (a = b)"
declassify "(=)"
embed eq_nat' is eq_nat .
this fails
Lars Hupel (Jan 05 2025 at 17:25):Does it work if you declassify "eq_nat"?
irvin (Jan 05 2025 at 17:26):No. its precisely failing at
The error(s) above occurred for the goal statement⌂:
eq_nat' ⊢ Const (Name ''Nat_equal__nat__inst_equal__nat'') ↓ equal_nat_inst.equal_nat ```
I think i see whether i can just make the = case done automatically by derive.
irvin (Jan 05 2025 at 17:30):Wait i think i know the issue is caused by the code equation given is defined like this so there a implicit mutual recursion which is not being handled equal_class.equal (Suc ?x2.1) (Suc ?y2.1) ≡ ?x2.1 = ?y2.1
irvin (Jan 05 2025 at 17:43):irvin said:
Wait i think i know the issue is caused by the code equation given is defined like this so there a implicit mutual recursion which is not being handled
equal_class.equal (Suc ?x2.1) (Suc ?y2.1) ≡ ?x2.1 = ?y2.1
wait nvm its not the issue No fundef_cong rule can be derived; this will likely not work later
irvin (Jan 06 2025 at 06:29):Oh i figured it out this import is necessary for some reason
Lazy_Case.Lazy_Case (* FIXME why is this import necessary *)
irvin (Jan 06 2025 at 06:34):irvin said:
Oh i figured it out this import is necessary for some reason
Lazy_Case.Lazy_Case (* FIXME why is this import necessary *)
wait its not :upside_down:
irvin (Jan 06 2025 at 06:36):Ok so after a bunch of print_tac I have reconcluded is that declassify does not generate induction
irvin (Jan 06 2025 at 08:33):irvin said:
Ok so after a bunch of print_tac I have reconcluded is that declassify does not generate induction
No that's wrong. I think the issue is declassify is generating the inductive predicate wrongly due to code_post
irvin (Jan 06 2025 at 09:58):Oh i finally managed to get it to generate it turns out that i have to use the generated definition by declassify for the embed.
declassify asimp_thm: asimp
derive evaluate
aexp
embed (eval) asimp' is Aexp__compile_asimp
Last updated: Feb 28 2025 at 08:24 UTC