Commit 584f9fe5 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'debug_drivers' into 'master'

Added debugging for driver's transformations

See merge request !38
parents a22212ec eae0fc9e
...@@ -21,6 +21,10 @@ open Trans ...@@ -21,6 +21,10 @@ open Trans
open Driver_ast open Driver_ast
open Call_provers open Call_provers
let driver_debug =
Debug.register_flag "interm_task"
~desc:"Print intermediate task generated during processing of a driver"
(** drivers *) (** drivers *)
type driver = { type driver = {
...@@ -324,11 +328,21 @@ let update_task = let ht = Hint.create 5 in fun drv -> ...@@ -324,11 +328,21 @@ let update_task = let ht = Hint.create 5 in fun drv ->
add_tdecl task goal add_tdecl task goal
| task -> update task | task -> update task
(* Apply driver's transformations to the task *)
let prepare_task drv task = let prepare_task drv task =
let lookup_transform t = lookup_transform t drv.drv_env in let lookup_transform t = lookup_transform t drv.drv_env, t in
let transl = List.map lookup_transform drv.drv_transform in let transl = List.map lookup_transform drv.drv_transform in
let apply task tr = Trans.apply tr task in let apply task (tr,name) =
let task = Trans.apply tr task in
Debug.dprintf driver_debug "Task after transformation: %s\n%a@."
name Pretty.print_task task;
task
in
Debug.dprintf driver_debug "Task before driver's transformation\n%a@."
Pretty.print_task task;
let task = update_task drv task in let task = update_task drv task in
Debug.dprintf driver_debug "Task after update\n%a@."
Pretty.print_task task;
List.fold_left apply task transl List.fold_left apply task transl
let print_task_prepared ?old drv fmt task = let print_task_prepared ?old drv fmt task =
......
...@@ -62,6 +62,8 @@ val prove_task : ...@@ -62,6 +62,8 @@ val prove_task :
driver -> Task.task -> Call_provers.prover_call driver -> Task.task -> Call_provers.prover_call
(** Split the previous function in two simpler functions *) (** Split the previous function in two simpler functions *)
(* Apply driver's transformations to the task *)
val prepare_task : driver -> Task.task -> Task.task val prepare_task : driver -> Task.task -> Task.task
val print_task_prepared : val print_task_prepared :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment