From 7af112e5c46bc915b3209d28184ef2f90bf37aef Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 14 May 2017 16:44:20 -0400 Subject: More debug info in reification --- src/Compilers/Reify.v | 10 +++++----- src/Util/Tactics/DebugPrint.v | 36 ++++++++++++++---------------------- 2 files changed, 19 insertions(+), 27 deletions(-) diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v index 810db4d9b..49d32824d 100644 --- a/src/Compilers/Reify.v +++ b/src/Compilers/Reify.v @@ -26,9 +26,9 @@ End ReifyDebugNotations. Ltac debug_enter_reify_idtac funname e := let s := (eval compute in (String.append funname ": Attempting to reify:")) in cidtac2 s e. -Ltac debug_leave_reify_success_idtac funname e := +Ltac debug_leave_reify_success_idtac funname e ret := let s := (eval compute in (String.append funname ": Success in reifying:")) in - cidtac2 s e. + cidtac4 s e " as " ret. Ltac debug_leave_reify_failure_idtac funname e := let s := (eval compute in (String.append funname ": Failure in reifying:")) in cfail2 s e. @@ -60,12 +60,12 @@ Ltac debug3 tac := | _ => check_debug_level_then_Set () end. Ltac debug_enter_reify2 funname e := debug2 ltac:(fun _ => debug_enter_reify_idtac funname e). -Ltac debug_leave_reify3_success funname e := debug3 ltac:(fun _ => debug_leave_reify_success_idtac funname e). +Ltac debug_leave_reify3_success funname e ret := debug3 ltac:(fun _ => debug_leave_reify_success_idtac funname e ret). Ltac debug_enter_reify3 funname e := debug2 ltac:(fun _ => debug_enter_reify_idtac funname e). Ltac debug_enter_reify_flat_type e := debug_enter_reify3 "reify_flat_type" e. Ltac debug_enter_reify_type e := debug_enter_reify3 "reify_type" e. Ltac debug_enter_reifyf e := debug_enter_reify2 "reifyf" e. -Ltac debug_leave_reifyf_success e := debug_leave_reify3_success "reifyf" e. +Ltac debug_leave_reifyf_success e ret := debug_leave_reify3_success "reifyf" e ret. Ltac debug_leave_reifyf_failure e := debug_leave_reify_failure_idtac "reifyf" e. Ltac debug_reifyf_case case := debug3 ltac:(fun _ => debug_reifyf_case_idtac case). Ltac debug_enter_reify_abs e := debug_enter_reify2 "reify_abs" e. @@ -314,7 +314,7 @@ Ltac reifyf base_type_code interp_base_type op var e := => cfail2 "Failed to reify:"%string x end end in - let dummy := debug_leave_reifyf_success e in + let dummy := debug_leave_reifyf_success e ret in ret | _ => debug_leave_reifyf_failure e end. diff --git a/src/Util/Tactics/DebugPrint.v b/src/Util/Tactics/DebugPrint.v index b35a3e77f..5c16b4403 100644 --- a/src/Util/Tactics/DebugPrint.v +++ b/src/Util/Tactics/DebugPrint.v @@ -17,6 +17,8 @@ Class cidtac2 {T1 T2} (msg1 : T1) (msg2 : T2) := Build_cidtac2 : True. Hint Extern 0 (cidtac2 ?msg1 ?msg2) => idtac msg1 msg2; exact I : typeclass_instances. Class cidtac3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cidtac3 : True. Hint Extern 0 (cidtac3 ?msg1 ?msg2 ?msg3) => idtac msg1 msg2 msg3; exact I : typeclass_instances. +Class cidtac4 {T1 T2 T3 T4} (msg1 : T1) (msg2 : T2) (msg3 : T3) (msg4 : T4) := Build_cidtac4 : True. +Hint Extern 0 (cidtac4 ?msg1 ?msg2 ?msg3 ?msg4) => idtac msg1 msg2 msg3 msg4; exact I : typeclass_instances. Class cfail {T} (msg : T) := Build_cfail : True. Hint Extern 0 (cfail ?msg) => idtac "Error:" msg; exact I : typeclass_instances. @@ -25,36 +27,26 @@ Hint Extern 0 (cfail2 ?msg1 ?msg2) => idtac "Error:" msg1 msg2; exact I : typecl Class cfail3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cfail3 : True. Hint Extern 0 (cfail3 ?msg1 ?msg2 ?msg3) => idtac "Error:" msg1 msg2 msg3; exact I : typeclass_instances. -Ltac cidtac msg := +Ltac constr_run_tac tac := let dummy := match goal with - | _ => idtac msg + | _ => tac () end in constr:(I). + +Ltac cidtac msg := + constr_run_tac ltac:(fun _ => idtac msg). Ltac cidtac2 msg1 msg2 := - let dummy := match goal with - | _ => idtac msg1 msg2 - end in - constr:(I). + constr_run_tac ltac:(fun _ => idtac msg1 msg2). Ltac cidtac3 msg1 msg2 msg3 := - let dummy := match goal with - | _ => idtac msg1 msg2 msg3 - end in - constr:(I). + constr_run_tac ltac:(fun _ => idtac msg1 msg2 msg3). +Ltac cidtac4 msg1 msg2 msg3 msg4 := + constr_run_tac ltac:(fun _ => idtac msg1 msg2 msg3 msg4). Ltac cfail msg := - let dummy := match goal with - | _ => idtac "Error:" msg - end in - constr:(I : I). + constr_run_tac ltac:(fun _ => idtac "Error:" msg). Ltac cfail2 msg1 msg2 := - let dummy := match goal with - | _ => idtac "Error:" msg1 msg2 - end in - constr:(I : I). + constr_run_tac ltac:(fun _ => idtac "Error:" msg1 msg2). Ltac cfail3 msg1 msg2 msg3 := - let dummy := match goal with - | _ => idtac "Error:" msg1 msg2 msg3 - end in - constr:(I : I). + constr_run_tac ltac:(fun _ => idtac "Error:" msg1 msg2 msg3). Ltac idtac_goal := lazymatch goal with |- ?G => idtac "Goal:" G end. Ltac idtac_context := -- cgit v1.2.3