Email Gateway (Aug 22 2022 at 14:36): Email Gateway (Aug 22 2022 at 14:36):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I have an inductive relation that I am attempting to generate code for.
It's a reduction relation:
reduce :: "e ⇒ store ⇒ e ⇒ store ⇒ bool"
I believe that there is one rule that is preventing mode inference from
deriving any functions (ie things like reduce_i_i_i_i)
Is there a way to turn on tracing here? I see in the ML code lines that
look like they would output trace information but have had no luck enabling
the trace.
I have tried
declare [[code_runtime_trace=true,code_simp_trace=true]]
Cheers
Mark
Email Gateway (Aug 22 2022 at 14:36):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Mark,
The predicate compiler offers various tracing options that you can pass to the code_pred
command. (It is independent of the code generator, so the tracing settings for the code
generator do not apply.)
Here is a command that enables as much tracing as possible:
code_pred
[show_steps,
show_proof_trace,
show_intermediate_results,
show_mode_inference,
show_modes,
show_compilation,
show_invalid_clauses]
my_inductive_predicate
Just delete those options that you are not interested in. Probably you want to keep
show_mode_inference.
Hope this helps,
Andreas
Last updated: Apr 24 2024 at 12:33 UTC