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



Hi Lars,

It is hard to say what goes wrong here given that I do not know what your types in the signature of the inductive predicates are. From the error message, I guess that something goes wrong during the higher-order mode analysis in the predicate compiler. As a first step, I recommend to specify the modes for all predicates. The syntax looks as follows:

code_pred
  (modes: evaluate_match: ... as ..
      and evaluate_list: ... as ..
      and evaluate: ... as ..)
  evaluate .

If that does not solve the problem:
How are the types all_env, count_store, v, pat, list, and result defined? If any of these is a type synonym that expands to a function with boolean result, you might try to specify a higher-order mode for these.

Hope this helps,
Andreas

On 22/07/14 14:21, Lars Hupel wrote:
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.