From 879b5bb5ced7cc614beae873271319922fc47a52 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Dec 2023 16:59:26 -0500 Subject: [PATCH] Allow leaving over shelved goals when debugging cache_term --- src/Rewriter/Util/Tactics/CacheTerm.v | 54 +++++++++++++++++++++------ 1 file changed, 42 insertions(+), 12 deletions(-) diff --git a/src/Rewriter/Util/Tactics/CacheTerm.v b/src/Rewriter/Util/Tactics/CacheTerm.v index 679a7f624..451a438f2 100644 --- a/src/Rewriter/Util/Tactics/CacheTerm.v +++ b/src/Rewriter/Util/Tactics/CacheTerm.v @@ -1,12 +1,37 @@ Require Import Rewriter.Util.Tactics.EvarNormalize. Require Import Rewriter.Util.Tactics.ClearFree. -Ltac cache_term_with_type_by_gen ty abstract_tac id := +Ltac allow_debug_in_cache := constr:(false). + +Ltac abstract_tac_with_debug abstract_tac tac arg := + let ctrue := constr:(true) in + let cfalse := constr:(false) in + let T := lazymatch goal with |- ?T => T end in + let id' := fresh in + simple notypeclasses refine (match _ : T return T with id' => _ end); + [ lazymatch allow_debug_in_cache with + | false => solve [ unshelve tac ] + | true => tac; shelve + | ?v => fail 1000 "Invalid non-bool value for allow_debug_in_cache" v "(" "expected" ctrue "or" cfalse ")" + end + | let res := (eval cbv delta [id'] in id') in + clear id'; + lazymatch allow_debug_in_cache with + | false + => abstract_tac ltac:(exact_no_check res) arg + | true + => tryif abstract_tac ltac:(exact_no_check res) arg + then idtac + else exact res + | ?v => fail 1000 "Invalid non-bool value for allow_debug_in_cache" v "(" "expected" ctrue "or" cfalse ")" + end ]. + +Ltac cache_term_with_type_by_gen ty abstract_tac tac id := let id' := fresh id in let __ := lazymatch goal with | [ |- ?T ] => simple notypeclasses refine (match _ : ty return T with id' => _ end); - [ abstract_tac id' + [ abstract_tac_with_debug abstract_tac tac id' | ] end in let ret := (eval cbv [id'] in id') in @@ -14,10 +39,11 @@ Ltac cache_term_with_type_by_gen ty abstract_tac id := | _ => clear id' end in ret. + Ltac clear_cache_term_with_type_by do_clear ty tac id := - cache_term_with_type_by_gen ty ltac:(fun id' => do_clear (); transparent_abstract tac using id') id. + cache_term_with_type_by_gen ty ltac:(fun tac id' => do_clear (); transparent_abstract tac using id') ltac:(do_clear (); tac) id. Ltac clear_cache_proof_with_type_by do_clear ty tac id := - cache_term_with_type_by_gen ty ltac:(fun id' => do_clear (); abstract tac using id') id. + cache_term_with_type_by_gen ty ltac:(fun tac id' => do_clear (); abstract tac using id') ltac:(do_clear (); tac) id. Ltac cache_term_with_type_by ty tac id := clear_cache_term_with_type_by ltac:(fun _ => idtac) ty tac id. Ltac cache_proof_with_type_by ty tac id := clear_cache_proof_with_type_by ltac:(fun _ => idtac) ty tac id. Ltac cache_term_by tac id := @@ -41,10 +67,12 @@ Ltac cache_sig_red_with_type_by ty tac red_tac red_cast_no_check id := ltac:(let v := (eval cbv beta iota delta [id' proj1_sig] in (proj1_sig id')) in let v := red_tac v in (exists v); - abstract ( - refine (eq_rect _ P (proj2_sig id') _ _); - red_cast_no_check (eq_refl v) - )) + let tac := + refine (eq_rect _ P (proj2_sig id') _ _); + red_cast_no_check (eq_refl v) + in + abstract_tac_with_debug ltac:(fun tac _ => abstract tac) tac () + ) id. Ltac cache_sig_red_with_type ty term red_tac red_cast_no_check id := let id' := fresh id in @@ -56,10 +84,12 @@ Ltac cache_sig_red_with_type ty term red_tac red_cast_no_check id := ltac:(let v := (eval cbv beta iota delta [id' proj1_sig] in (proj1_sig id')) in let v := red_tac v in (exists v); - abstract ( - refine (eq_rect _ P (proj2_sig id') _ _); - red_cast_no_check (eq_refl v) - )) + let tac _ := + refine (eq_rect _ P (proj2_sig id') _ _); + red_cast_no_check (eq_refl v) + in + abstract_tac_with_debug ltac:(fun tac _ => abstract tac) tac () + ) id. Ltac cache_sig_with_type_by ty tac id := cache_sig_red_with_type_by ty tac ltac:(fun v => v) exact_no_check id.