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

Hi Lars,

I don't know either what it is that triggers this exception, but I suspect that it has
something to do with all those tuples in your types. If you enable exception tracing, you
can see that the error occurs only during the correctness proof of the compiled
expression. If you just want to execute evaluate for some test cases, it might be
sufficient to trust the predicate compiler and disable the proofs with the option
[skip_proof]. Then, code_pred digests your semantics. Otherwise, you probably have to look
into the proof tactic.

However, for values, you also have to do the termination proofs for the functions pmatch,
do_eq and pat_bindings. In summary, the following works in Isabelle2013-2:

  (modes: evaluate:       i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool
      and evaluate_list:  i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool
      and evaluate_match: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool)
  evaluate .

termination pmatch by lexicographic_order
termination do_eq by lexicographic_order
termination pat_bindings by lexicographic_order


On 22/07/14 14:58, Lars Hupel wrote:
Hi Andreas,

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 far as I can tell, there is no higher-order-ness involved.

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 ..)
   evaluate .

This gives an even lower-level error:

exception THM 1 raised (line 332 of "drule.ML"):
   RSN: no unifiers
   xh  [xh]
   ?s = ?t ⟹ ?t = ?s

I have attached a self-contained zip file. The problematic invocation is
in "Scratch.thy", which should be loaded with the "CakeML" image (see ROOT).


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