Re: [isabelle] Turning on tracing for mode inference?



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

On 10/11/16 10:06, Mark Wassell wrote:
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





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