Stream: Beginner Questions

Topic: Code export with uncomputable branches

Yong Kiam (Sep 19 2023 at 04:22):

I would like to preface this by saying that, I am aware this is probably a bad idea

I would like to export some code where some branches are not computable/exportable, but where I have blocked them off using Code.abort

Small example:

definition foo ::" nat ⇒ real"
where "
  foo n = (
  if n = 0
  then 0
  else Code.abort (STR ''foo'') (λ_. ln n))"

export_code
  foo
  in SML
  file_prefix "foo"

The above export call results in a well-sortedness error when trying to export ln:

Wellsortedness error
(in code equation ln_real_inst.ln_real ?x ≡
                  THE u. equal_real_inst.equal_real (exp u) ?x,
with dependency "foo" -> "ln [real]"):
Type real not of sort enum
No type arity real :: enum

Note that ln here is just an example. My question is whether one can make the code exporter ignore things behind Code.abort?

(In my specific use case, I know how to work around this, but it's annoying)

Hanno Becker (Sep 23 2023 at 05:26):

Have you considered using declare [[code abort: function_to_be_ignored]]? page 13 in https://isabelle.in.tum.de/doc/codegen.pdf

Yong Kiam (Sep 23 2023 at 08:14):

ah, that's right, I think I can make it work with this by defining a dummy function that wraps around that branch and then using code abort on it. I wanted something more granular, where I can block off a branch directly, but this will work for my use case, thank you.

Last updated: Apr 27 2024 at 12:25 UTC