From: Florian Märkl <isabelle-users@florianmaerkl.de>

Hello,

I am trying to replicate something like discussed in

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2020-November/msg00013.html

(the part of the JinjaThreads theory), i.e. generating code for a

reflexive transitive closure predicate, however the [inductify] option

that I have to use on code_pred currently seems to give me some headaches.

In essence, what I have in my project is something like this:

theory "Scratch"

imports "HOL-Library.Transitive_Closure_Table" Main

begin

typedef mynat = "{n :: nat. True}" by auto

setup_lifting type_definition_mynat

definition P :: "mynat ⇒ mynat ⇒ bool" where

"P a b ≡ Rep_mynat a = Suc (Rep_mynat b)"

definition t where "t = (P)^**"

(* Fails with: "No specification for Rep_mynat" *)

code_pred (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) [inductify] t .

(* The final goal *)

export_code t in SML

end

I have some executable predicate P over which I want to execute the

reflexive transitive closure t.

Now from what I understand (please correct me if I am wrong), the

[inductify] option here is necessary so code_pred understands that this

is actually an inductive predicate by digging into the definitions.

But that also means it will go even deeper and try to inspect Rep_mynat

for example, which fails.

What I intuitively would want it to do is to only unfold the t, but then

consider P an opaque constant.

I have seen that code_pred has quite a few more undocumented options,

but didn't find anything yet that did what I need. Is something like

this possible somehow or am I misunderstanding the inner workings of the

predicate compiler here?

Florian

From: Tobias Nipkow <nipkow@in.tum.de>

"No specification for Rep_mynat": I suspect the code generator just cannot

handle types specified by "typedef".

Tobias

smime.p7s

From: Florian Märkl <isabelle-users@florianmaerkl.de>

Hello Tobias,

in my larger project I could probably get rid of the typdefd types in

this specific predicate by just duplicating the code of what is called P

here, operating directly on the underying type of the typedef.

However after doing this, I end up with another issue that can be seen

in this example:

theory "Scratch"

imports "HOL-Library.Transitive_Closure_Table" Main

begin

definition P :: "nat ⇒ nat ⇒ bool" where "P a b ≡ a ∈ set [b]"

definition t where "t ≡ (P)^**"

(* Fails with:

exception TERM raised (line 80 of

"~~/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML"):

defining_const_of_introrule failed: Not a constant

{x. x ∈ ?z} ≡ ?z

*)

code_pred (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) [inductify, show_steps,

show_intermediate_results] t .

(* The final goal *)

export_code t in SML

end

So it seems there is an issue with the ∈ operator now, which might be

possible to eliminate too (here by operating on the list [b], probably

similar in the real project) but this also brings me back to the

original problem: Is it somehow possible to use code_pred on a

definition like "t ≡ (P)^**" that does not use the "inductive" command

at the top level, without code_pred having to recurse through every

little definition that it contains?

Florian

From: Andreas Lochbihler <mail@andreas-lochbihler.de>

Hi Florian,

code_pred's [inductify] option has its quirks and doesn't always work; in particular set

comprehensions and set membership are tricky (code_pred was developed when "'a set" was a

type abbreviation for "'a => bool"). What you can do is to do the inductification

manually. In your example with the typedef, the following makes code_pred generate the

right equations (of course, you should manually fill in the sorrys)

lemma P_intro [code_pred_intro]: "P n m"

if "Rep_mynat n ≠ 0" "m = Abs_mynat (Rep_mynat n - 1)" sorry

code_pred (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) P sorry

code_pred (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) [inductify] t .

Now, however, export_code gives you a well-sortedness error that mynat isn't an instance

of equal. But that's something you probably want to provide anyway; I'm actually surprised

that the setup_lifting doesn't generate such an instance.

Hope this helps,

Andreas

From: Florian Märkl <isabelle-users@florianmaerkl.de>

Hello Andreas,

thank you very much, this does bring me one step forward.

Now considering the set example again, this is what I have now:

theory "Scratch"

imports "HOL-Library.Transitive_Closure_Table" Main

begin

definition P :: "nat ⇒ nat ⇒ bool" where "P a b ≡ a ∈ set [b]"

definition t where "t ≡ (P)^**"

lemma P_intro [code_pred_intro]: "P a b"

if "a ∈ set [b]" unfolding P_def using that .

code_pred (modes: i ⇒ i ⇒ bool) P

using P_def by auto

(*

Output:

Inferred modes:

Scratch.t:

*)

code_pred (* errors: (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool)*) [inductify,

show_modes] t .

export_code t in SML module_name Scratch

(*

exception Fail raised (line 26 of "generated code"):

Transitive_Closure.rtranclp

which is no wonder becuause the code is essentially this:

fun rtranclp _ _ _ = raise Fail "Transitive_Closure.rtranclp";

fun t x = rtranclp p x;

*)

value "t 0 1"

end

So in the end, with HOL-Library.Transitive_Closure_Table, the rtranclp

function ist just a one-liner raising an exception here.

What seems fishy to me is that the code_pred for t in this case does not

infer any modes at all, but I am not really sure what to make of this.

Florian

From: Andreas Lochbihler <mail@andreas-lochbihler.de>

Hi Florian,

For the predicate P, you've only inferred the mode i => i => bool, but that's not enough

to compute a transitive closure (as nat is infinite). If you add [show_mode] to the

code_pred rtranclp invocation in Transitive_Closure_Table, you'll see that the relation

must have mode i => o => bool. So you need to provide introduction rules for P that yield

such a mode. In your artificial example, you get this via

lemma [code_pred_intro]: "P a b" if "a = b"

Another example: If P was defined as "P a b = a : set [b, b + 1]", you'd get there via

lemma [code_pred_intro]: "a = b ==> P a b" "a = b + 1 ==> P a b"

Hope this helps,

Andreas

Last updated: Jan 25 2022 at 01:11 UTC