Re: [isabelle] Predicate compiler: mode and term do not match
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:
(modes: evaluate_match: ... as ..
and evaluate_list: ... as ..
and evaluate: ... as ..)
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,
On 22/07/14 14:21, Lars Hupel wrote:
I have three mutually-defined inductive predicates:
evaluate_match :: "bool ⇒ all_env ⇒(v)count_store ⇒ v ⇒(pat*exp)list ⇒ v ⇒(v)count_store*((v),(v))result ⇒ bool"
evaluate_list :: "bool ⇒ all_env ⇒(v)count_store ⇒(exp)list ⇒(v)count_store*(((v)list),(v))result ⇒ bool"
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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and