Email Gateway (Aug 19 2022 at 14:59): Email Gateway (Aug 19 2022 at 14:59):From: Lars Hupel <hupel@in.tum.de>
Dear all,
I have three mutually-defined inductive predicates:
inductive
evaluate_match :: "bool ⇒ all_env ⇒(v)count_store ⇒ v ⇒(patexp)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
Email Gateway (Aug 19 2022 at 14:59):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 14:59):From: Lars Hupel <hupel@in.tum.de>
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:code_pred
(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).
Cheers
Lars
cakeml_bigstep.zip
Email Gateway (Aug 19 2022 at 15:00):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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:
code_pred
(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)
[skip_proof]
evaluate .
termination pmatch by lexicographic_order
termination do_eq by lexicographic_order
termination pat_bindings by lexicographic_order
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:00):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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:
code_pred
(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)
[skip_proof]
evaluate .
termination pmatch by lexicographic_order
termination do_eq by lexicographic_order
termination pat_bindings by lexicographic_order
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:00):From: Lars Hupel <hupel@in.tum.de>
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.
I'm afraid I can't change these definitions; this is code which is being
automatically generated by Lem from the CakeML sources.
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:code_pred
(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)
[skip_proof]
evaluate .termination pmatch by lexicographic_order
termination do_eq by lexicographic_order
termination pat_bindings by lexicographic_order
Great, that works like a charm. In the end, I'm probably not going to
need the code setup, but it might be worth investigating anyway why this
fails. I don't see any special things going on here.
Thanks for your help!
Lars
Email Gateway (Aug 19 2022 at 15:00):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,
I would appreciate if you invest some effort here.
Just the usual warning to refrain from ad-hoc changes before a release.
Good things take their while.
Cheers,
Florian
signature.asc
Last updated: Apr 18 2024 at 08:19 UTC