Re: [isabelle] Predicate Compiler fails with "No specification for ..."



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

On 2/21/21 9:10 AM, Andreas Lochbihler wrote:
> 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
> 
> 
> On 20.02.21 19:32, Florian Märkl wrote:
>> 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
>>
>> On 2/20/21 6:07 PM, Tobias Nipkow wrote:
>>> "No specification for Rep_mynat": I suspect the code generator just
>>> cannot handle types specified by "typedef".
>>>
>>> Tobias
>>>
>>> On 19/02/2021 15:03, Florian Märkl wrote:
>>>> 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
>>>>
>>>
>>
>>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.