[isabelle] Predicate compiler: mode and term do not match



Dear all,

I have three mutually-defined inductive predicates:

> inductive
>   evaluate_match :: "bool ⇒ all_env ⇒(v)count_store ⇒ v ⇒(pat*exp)list ⇒ v ⇒(v)count_store*((v),(v))result ⇒ bool"  
>   and
>   evaluate_list :: "bool ⇒ all_env ⇒(v)count_store ⇒(exp)list ⇒(v)count_store*(((v)list),(v))result ⇒ bool"  
>   and
>   evaluate :: "bool ⇒ all_env ⇒(v)count_store ⇒ exp ⇒(v)count_store*((v),(v))result ⇒ bool"

As far as I can see, their rules are relatively straightforward. I can
make proofs over them just fine by repeated application of "rule" and
some unfolding.

Now, I want to make them executable. The obvious invocation

> code_pred evaluate .

fails: despite there being no subgoals, the command fails after "." with:

> exception Fail raised (line 356 of "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML"): split_map_mode: mode and term do not match

I also tried to specify the mode explicitly, but to no avail:

> code_pred (modes: i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool as compute_evaluate) evaluate .

(same error message)

What am I doing wrong?

Cheers
Lars




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