diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 52 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 | 96 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.mli | 9 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 52 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 | 96 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli | 9 | ||||
| -rw-r--r-- | mathcomp/ssrtest/explain_match.v | 12 |
7 files changed, 254 insertions, 72 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index d214dc3..fc895a5 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -4649,7 +4649,7 @@ END let simplintac occ rdx sim gl = let simptac gl = let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in - let simp env c _ = red_safe Tacred.simpl env sigma0 c in + let simp env c _ _ = red_safe Tacred.simpl env sigma0 c in Proofview.V82.of_tactic (convert_concl_no_check (eval_pattern env0 sigma0 concl0 rdx occ simp)) gl in @@ -4687,8 +4687,8 @@ let unfoldintac occ rdx t (kt,_) gl = let ise, u = mk_tpattern env0 sigma0 (ise,t) all_ok L2R t in let find_T, end_T = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in - (fun env c h -> - try find_T env c h (fun env c _ -> body env t c) + (fun env c _ h -> + try find_T env c h (fun env c _ _ -> body env t c) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm (str"No occurrence of " ++ pr_constr_pat t ++ spc() ++ str "in " ++ pr_constr c)), @@ -4696,7 +4696,7 @@ let unfoldintac occ rdx t (kt,_) gl = | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") | _ -> - (fun env (c as orig_c) h -> + (fun env (c as orig_c) _ h -> if const then let rec aux c = match kind_of_term c with @@ -4734,10 +4734,10 @@ let foldtac occ rdx ft gl = let ise, ut = mk_tpattern env0 sigma0 (ise,t) all_ok L2R ut in let find_T, end_T = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in - (fun env c h -> try find_T env c h (fun env t _ -> t) with NoMatch -> c), + (fun env c _ h -> try find_T env c h (fun env t _ _ -> t) with NoMatch ->c), (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ()) | _ -> - (fun env c h -> try let sigma = unify_HO env sigma c t in fs sigma t + (fun env c _ h -> try let sigma = unify_HO env sigma c t in fs sigma t with _ -> errorstrm (str "fold pattern " ++ pr_constr_pat t ++ spc () ++ str "does not match redex " ++ pr_constr_pat c)), fake_pmatcher_end in @@ -4902,7 +4902,7 @@ let closed0_check cl p gl = if closed0 cl then errorstrm (str"No occurrence of redex "++pf_pr_constr gl (project gl) p) -let rwrxtac occ rdx_pat dir rule gl = +let rwprocess_rule dir rule gl = let env = pf_env gl in let coq_prod = lz_coq_prod () in let is_setoid = ssr_is_setoid env in @@ -4973,7 +4973,13 @@ let rwrxtac occ rdx_pat dir rule gl = in let sigma, r = rule in let t = Retyping.get_type_of env sigma r in - loop dir sigma r t [] 0 in + loop dir sigma r t [] 0 + in + r_sigma, rules + +let rwrxtac occ rdx_pat dir rule gl = + let env = pf_env gl in + let r_sigma, rules = rwprocess_rule dir rule gl in let find_rule rdx = let rec rwtac = function | [] -> @@ -4998,11 +5004,11 @@ let rwrxtac occ rdx_pat dir rule gl = sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in - find_R ~k:(fun _ _ h -> mkRel h), + (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T (e,_,_))) -> let r = ref None in - (fun env c h -> do_once r (fun () -> find_rule c, c); mkRel h), + (fun env c _ h -> do_once r (fun () -> find_rule c, c); mkRel h), (fun concl -> closed0_check concl e gl; assert_done r) in let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in @@ -5015,6 +5021,32 @@ let rwrxtac occ rdx_pat dir rule gl = prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl ;; +let ssrinstancesofrule ist dir arg gl = + let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in + let rule = interp_term ist gl arg in + let r_sigma, rules = rwprocess_rule dir rule gl in + let find, conclude = + let upats_origin = dir, snd rule in + let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) = + let sigma, pat = + mk_tpattern env sigma0 (sigma,r) (rw_progress rhs) d lhs in + sigma, pats @ [pat] in + let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in + mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + ppnl (str"BEGIN INSTANCES"); + try + while true do + ignore(find env0 concl0 1 ~k:print) + done; raise NoMatch + with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl + +TACTIC EXTEND ssrinstofruleL2R +| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist L2R arg) ] +END +TACTIC EXTEND ssrinstofruleR2L +| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist R2L arg) ] +END (* Resolve forward reference *) let _ = diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 index effd193..b697050 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 @@ -621,7 +621,7 @@ let match_upats_FO upats env sigma0 ise c = ;; -let match_upats_HO upats env sigma0 ise c = +let match_upats_HO ~on_instance upats env sigma0 ise c = let it_did_match = ref false in let rec aux upats env sigma0 ise c = let f, a = splay_app ise c in let i0 = ref (-1) in @@ -650,7 +650,7 @@ let match_upats_HO upats env sigma0 ise c = let ise'' = unif_HO_args env ise' u.up_a (i - Array.length u.up_a) a in let lhs = mkSubApp f i a in let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in - raise (FoundUnif (ungen_upat lhs pt' u)) + on_instance (ungen_upat lhs pt' u) with FoundUnif _ as sigma_u -> raise sigma_u | NoProgress -> it_did_match := true | _ -> () in @@ -663,8 +663,8 @@ let match_upats_HO upats env sigma0 ise c = if !it_did_match then raise NoProgress let prof_HO = mk_profiler "match_upats_HO";; -let match_upats_HO upats env sigma0 ise c = - prof_HO.profile (match_upats_HO upats env sigma0) ise c +let match_upats_HO ~on_instance upats env sigma0 ise c = + prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c ;; @@ -677,7 +677,14 @@ let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) let assert_done r = match !r with Some x -> x | None -> Errors.anomaly (str"do_once never called") -type subst = Environ.env -> Term.constr -> int -> Term.constr +let assert_done_multires r = + match !r with + | None -> Errors.anomaly (str"do_once never called") + | Some (n, xs) -> + r := Some (n+1,xs); + try List.nth xs n with Failure _ -> raise NoMatch + +type subst = Environ.env -> Term.constr -> Term.constr -> int -> Term.constr type find_P = Environ.env -> Term.constr -> int -> k:subst -> @@ -686,7 +693,7 @@ type conclude = unit -> Term.constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * Term.constr) (* upats_origin makes a better error message only *) -let mk_tpattern_matcher +let mk_tpattern_matcher ?(all_instances=false) ?(raise_NoMatch=false) ?upats_origin sigma0 occ (ise, upats) = let nocc = ref 0 and skip_occ = ref false in @@ -729,13 +736,35 @@ let source () = match upats_origin, upats with pr_constr_pat rule ++ spc() | _, [] | None, _::_::_ -> Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in +let on_instance, instances = + let instances = ref [] in + (fun x -> + if all_instances then instances := !instances @ [x] + else raise (FoundUnif x)), + (fun () -> !instances) in +let rec uniquize = function + | [] -> [] + | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs -> + let t = Reductionops.nf_evar sigma t in + let f = Reductionops.nf_evar sigma f in + let a = Array.map (Reductionops.nf_evar sigma) a in + let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) = + let t1 = Reductionops.nf_evar sigma1 t1 in + let f1 = Reductionops.nf_evar sigma1 f1 in + let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in + not (Term.eq_constr t t1 && + Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in + x :: uniquize (List.filter neq xs) in + ((fun env c h ~k -> do_once upat_that_matched (fun () -> try - match_upats_FO upats env sigma0 ise c; - match_upats_HO upats env sigma0 ise c; + if not all_instances then match_upats_FO upats env sigma0 ise c; + match_upats_HO ~on_instance upats env sigma0 ise c; raise NoMatch - with FoundUnif sigma_u -> sigma_u + with FoundUnif sigma_u -> 0,[sigma_u] + | (NoMatch|NoProgress) when all_instances && instances () <> [] -> + 0, uniquize (instances ()) | NoMatch when (not raise_NoMatch) -> errorstrm (source () ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> @@ -744,9 +773,11 @@ let source () = match upats_origin, upats with errorstrm (str"all matches of "++source()++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); - let sigma, _, ({up_f = pf; up_a = pa} as u) = assert_done upat_that_matched in + let sigma, _, ({up_f = pf; up_a = pa} as u) = + if all_instances then assert_done_multires upat_that_matched + else List.hd (snd(assert_done upat_that_matched)) in pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); - if !skip_occ then (ignore(k env u.up_t 0); c) else + if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else let match_EQ = match_EQ env sigma u in let pn = Array.length pa in let rec subst_loop (env,h as acc) c' = @@ -755,7 +786,7 @@ let source () = match upats_origin, upats with if Array.length a >= pn && match_EQ f && unif_EQ_args env sigma pa a then let a1, a2 = Array.chop (Array.length pa) a in let fa1 = mkApp (f, a1) in - let f' = if subst_occ () then k env u.up_t h else fa1 in + let f' = if subst_occ () then k env u.up_t fa1 h else fa1 in mkApp (f', Array.map_left (subst_loop acc) a2) else (* TASSI: clear letin values to avoid unfolding *) @@ -766,7 +797,7 @@ let source () = match upats_origin, upats with ((fun () -> let sigma, uc, ({up_f = pf; up_a = pa} as u) = match !upat_that_matched with - | Some x -> x | None when raise_NoMatch -> raise NoMatch + | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch | None -> Errors.anomaly (str"companion function never called") in let p' = mkApp (pf, pa) in if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t) @@ -1088,7 +1119,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 1 + | None -> do_subst env0 concl0 concl0 1 | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in @@ -1107,7 +1138,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = (* we start from sigma, so hole is considered a rigid head *) let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in - let concl = find_T env0 concl0 1 (fun env c h -> + let concl = find_T env0 concl0 1 (fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) c p in let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h @@ -1123,10 +1154,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_X, end_X = mk_tpattern_matcher sigma noindex holep in let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in - let concl = find_T env0 concl0 1 (fun env c h -> + let concl = find_T env0 concl0 1 (fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) c p in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h (fun env c h -> + fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> find_E env e_body h do_subst))) in let _ = end_E () in let _ = end_X () in let _ = end_T () in concl @@ -1140,13 +1171,13 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher sigma occ holep in - let concl = find_TE env0 concl0 1 (fun env c h -> + let concl = find_TE env0 concl0 1 (fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) c p in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h (fun env c h -> + fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> let e_sigma = unify_HO env sigma e_body e in let e_body = fs e_sigma e in - do_subst env e_body h))) in + do_subst env e_body e_body h))) in let _ = end_X () in let _ = end_TE () in concl ;; @@ -1162,7 +1193,7 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let find_R, conclude = let r = ref None in - (fun env c h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context); + (fun env c _ h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context); mkRel (h'+h-1)), (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in @@ -1180,7 +1211,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let ise, u = mk_tpattern env sigma0 (ise,t) ok L2R p in let find_U, end_U = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in - let concl = find_U env concl h (fun _ _ -> mkRel) in + let concl = find_U env concl h (fun _ _ _ -> mkRel) in let rdx, _, (sigma, uc, p) = end_U () in sigma, uc, p, concl, rdx @@ -1238,6 +1269,27 @@ TACTIC EXTEND ssrat | [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic (ssrpatterntac ist arg) ] END +let ssrinstancesof ist arg gl = + let ok rhs lhs ise = true in +(* not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *) + let env, sigma, concl = pf_env gl, project gl, pf_concl gl in + let sigma0, cpat = interp_cpattern ist gl arg None in + let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in + let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in + let find, conclude = + mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true + sigma None (etpat,[tpat]) in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + ppnl (str"BEGIN INSTANCES"); + try + while true do + ignore(find env concl 1 ~k:print) + done; raise NoMatch + with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl + +TACTIC EXTEND ssrinstoftpat +| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof ist arg) ] +END (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli b/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli index 0976be7..b7d8d18 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli +++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli @@ -77,9 +77,9 @@ val interp_cpattern : * to signal the complement of this set (i.e. {-1 3}) *) type occ = (bool * int list) option -(** Substitution function. The [int] argument is the number of binders - traversed so far *) -type subst = env -> constr -> int -> constr +(** [subst e p t i]. [i] is the number of binders + traversed so far, [p] the term from the pattern, [t] the matched one *) +type subst = env -> constr -> constr -> int -> constr (** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every [occ] occurrence of [pat]. The [int] argument is the number of @@ -120,7 +120,7 @@ val pr_dir_side : ssrdir -> Pp.std_ppcmds (** a pattern for a term with wildcards *) type tpattern -(** [mk_tpattern env sigma0 sigma_t ok p_origin dir p] compiles a term [t] +(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern]. The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok] callback is used to filter occurrences. @@ -161,6 +161,7 @@ type conclude = be passed to tune the [UserError] eventually raised (useful if the pattern is coming from the LHS/RHS of an equation) *) val mk_tpattern_matcher : + ?all_instances:bool -> ?raise_NoMatch:bool -> ?upats_origin:ssrdir * constr -> evar_map -> occ -> evar_map * tpattern list -> diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 index d5d7bf3..9452aa2 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 @@ -4643,7 +4643,7 @@ END let simplintac occ rdx sim gl = let simptac gl = let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in - let simp env c _ = red_safe Tacred.simpl env sigma0 c in + let simp env c _ _ = red_safe Tacred.simpl env sigma0 c in Proofview.V82.of_tactic (convert_concl_no_check (eval_pattern env0 sigma0 concl0 rdx occ simp)) gl in @@ -4681,8 +4681,8 @@ let unfoldintac occ rdx t (kt,_) gl = let ise, u = mk_tpattern env0 sigma0 (ise,t) all_ok L2R t in let find_T, end_T = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in - (fun env c h -> - try find_T env c h (fun env c _ -> body env t c) + (fun env c _ h -> + try find_T env c h (fun env c _ _ -> body env t c) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm (str"No occurrence of " ++ pr_constr_pat t ++ spc() ++ str "in " ++ pr_constr c)), @@ -4690,7 +4690,7 @@ let unfoldintac occ rdx t (kt,_) gl = | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") | _ -> - (fun env (c as orig_c) h -> + (fun env (c as orig_c) _ h -> if const then let rec aux c = match kind_of_term c with @@ -4728,10 +4728,10 @@ let foldtac occ rdx ft gl = let ise, ut = mk_tpattern env0 sigma0 (ise,t) all_ok L2R ut in let find_T, end_T = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in - (fun env c h -> try find_T env c h (fun env t _ -> t) with NoMatch -> c), + (fun env c _ h -> try find_T env c h (fun env t _ _ -> t) with NoMatch ->c), (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ()) | _ -> - (fun env c h -> try let sigma = unify_HO env sigma c t in fs sigma t + (fun env c _ h -> try let sigma = unify_HO env sigma c t in fs sigma t with _ -> errorstrm (str "fold pattern " ++ pr_constr_pat t ++ spc () ++ str "does not match redex " ++ pr_constr_pat c)), fake_pmatcher_end in @@ -4896,7 +4896,7 @@ let closed0_check cl p gl = if closed0 cl then errorstrm (str"No occurrence of redex "++pf_pr_constr gl (project gl) p) -let rwrxtac occ rdx_pat dir rule gl = +let rwprocess_rule dir rule gl = let env = pf_env gl in let coq_prod = lz_coq_prod () in let is_setoid = ssr_is_setoid env in @@ -4967,7 +4967,13 @@ let rwrxtac occ rdx_pat dir rule gl = in let sigma, r = rule in let t = Retyping.get_type_of env sigma r in - loop dir sigma r t [] 0 in + loop dir sigma r t [] 0 + in + r_sigma, rules + +let rwrxtac occ rdx_pat dir rule gl = + let env = pf_env gl in + let r_sigma, rules = rwprocess_rule dir rule gl in let find_rule rdx = let rec rwtac = function | [] -> @@ -4992,11 +4998,11 @@ let rwrxtac occ rdx_pat dir rule gl = sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in - find_R ~k:(fun _ _ h -> mkRel h), + (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T (e,_,_))) -> let r = ref None in - (fun env c h -> do_once r (fun () -> find_rule c, c); mkRel h), + (fun env c _ h -> do_once r (fun () -> find_rule c, c); mkRel h), (fun concl -> closed0_check concl e gl; assert_done r) in let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in @@ -5009,6 +5015,32 @@ let rwrxtac occ rdx_pat dir rule gl = prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl ;; +let ssrinstancesofrule ist dir arg gl = + let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in + let rule = interp_term ist gl arg in + let r_sigma, rules = rwprocess_rule dir rule gl in + let find, conclude = + let upats_origin = dir, snd rule in + let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) = + let sigma, pat = + mk_tpattern env sigma0 (sigma,r) (rw_progress rhs) d lhs in + sigma, pats @ [pat] in + let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in + mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + ppnl (str"BEGIN INSTANCES"); + try + while true do + ignore(find env0 concl0 1 ~k:print) + done; raise NoMatch + with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl + +TACTIC EXTEND ssrinstofruleL2R +| [ "ssrinstancesofruleL2R" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist L2R arg) ] +END +TACTIC EXTEND ssrinstofruleR2L +| [ "ssrinstancesofruleR2L" ssrterm(arg) ] -> [ Proofview.V82.tactic (ssrinstancesofrule ist R2L arg) ] +END (* Resolve forward reference *) let _ = diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 index c47c946..7a58c61 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 @@ -621,7 +621,7 @@ let match_upats_FO upats env sigma0 ise c = ;; -let match_upats_HO upats env sigma0 ise c = +let match_upats_HO ~on_instance upats env sigma0 ise c = let it_did_match = ref false in let rec aux upats env sigma0 ise c = let f, a = splay_app ise c in let i0 = ref (-1) in @@ -650,7 +650,7 @@ let match_upats_HO upats env sigma0 ise c = let ise'' = unif_HO_args env ise' u.up_a (i - Array.length u.up_a) a in let lhs = mkSubApp f i a in let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in - raise (FoundUnif (ungen_upat lhs pt' u)) + on_instance (ungen_upat lhs pt' u) with FoundUnif _ as sigma_u -> raise sigma_u | NoProgress -> it_did_match := true | _ -> () in @@ -663,8 +663,8 @@ let match_upats_HO upats env sigma0 ise c = if !it_did_match then raise NoProgress let prof_HO = mk_profiler "match_upats_HO";; -let match_upats_HO upats env sigma0 ise c = - prof_HO.profile (match_upats_HO upats env sigma0) ise c +let match_upats_HO ~on_instance upats env sigma0 ise c = + prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c ;; @@ -677,7 +677,14 @@ let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) let assert_done r = match !r with Some x -> x | None -> Errors.anomaly (str"do_once never called") -type subst = Environ.env -> Term.constr -> int -> Term.constr +let assert_done_multires r = + match !r with + | None -> Errors.anomaly (str"do_once never called") + | Some (n, xs) -> + r := Some (n+1,xs); + try List.nth xs n with Failure _ -> raise NoMatch + +type subst = Environ.env -> Term.constr -> Term.constr -> int -> Term.constr type find_P = Environ.env -> Term.constr -> int -> k:subst -> @@ -686,7 +693,7 @@ type conclude = unit -> Term.constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * Term.constr) (* upats_origin makes a better error message only *) -let mk_tpattern_matcher +let mk_tpattern_matcher ?(all_instances=false) ?(raise_NoMatch=false) ?upats_origin sigma0 occ (ise, upats) = let nocc = ref 0 and skip_occ = ref false in @@ -729,13 +736,35 @@ let source () = match upats_origin, upats with pr_constr_pat rule ++ spc() | _, [] | None, _::_::_ -> Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in +let on_instance, instances = + let instances = ref [] in + (fun x -> + if all_instances then instances := !instances @ [x] + else raise (FoundUnif x)), + (fun () -> !instances) in +let rec uniquize = function + | [] -> [] + | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs -> + let t = Reductionops.nf_evar sigma t in + let f = Reductionops.nf_evar sigma f in + let a = Array.map (Reductionops.nf_evar sigma) a in + let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) = + let t1 = Reductionops.nf_evar sigma1 t1 in + let f1 = Reductionops.nf_evar sigma1 f1 in + let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in + not (Term.eq_constr t t1 && + Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in + x :: uniquize (List.filter neq xs) in + ((fun env c h ~k -> do_once upat_that_matched (fun () -> try - match_upats_FO upats env sigma0 ise c; - match_upats_HO upats env sigma0 ise c; + if not all_instances then match_upats_FO upats env sigma0 ise c; + match_upats_HO ~on_instance upats env sigma0 ise c; raise NoMatch - with FoundUnif sigma_u -> sigma_u + with FoundUnif sigma_u -> 0,[sigma_u] + | (NoMatch|NoProgress) when all_instances && instances () <> [] -> + 0, uniquize (instances ()) | NoMatch when (not raise_NoMatch) -> errorstrm (source () ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> @@ -744,9 +773,11 @@ let source () = match upats_origin, upats with errorstrm (str"all matches of "++source()++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); - let sigma, _, ({up_f = pf; up_a = pa} as u) = assert_done upat_that_matched in + let sigma, _, ({up_f = pf; up_a = pa} as u) = + if all_instances then assert_done_multires upat_that_matched + else List.hd (snd(assert_done upat_that_matched)) in pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); - if !skip_occ then (ignore(k env u.up_t 0); c) else + if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else let match_EQ = match_EQ env sigma u in let pn = Array.length pa in let rec subst_loop (env,h as acc) c' = @@ -755,7 +786,7 @@ let source () = match upats_origin, upats with if Array.length a >= pn && match_EQ f && unif_EQ_args env sigma pa a then let a1, a2 = Array.chop (Array.length pa) a in let fa1 = mkApp (f, a1) in - let f' = if subst_occ () then k env u.up_t h else fa1 in + let f' = if subst_occ () then k env u.up_t fa1 h else fa1 in mkApp (f', Array.map_left (subst_loop acc) a2) else (* TASSI: clear letin values to avoid unfolding *) @@ -766,7 +797,7 @@ let source () = match upats_origin, upats with ((fun () -> let sigma, uc, ({up_f = pf; up_a = pa} as u) = match !upat_that_matched with - | Some x -> x | None when raise_NoMatch -> raise NoMatch + | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch | None -> Errors.anomaly (str"companion function never called") in let p' = mkApp (pf, pa) in if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t) @@ -1088,7 +1119,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 1 + | None -> do_subst env0 concl0 concl0 1 | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in @@ -1107,7 +1138,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = (* we start from sigma, so hole is considered a rigid head *) let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in - let concl = find_T env0 concl0 1 (fun env c h -> + let concl = find_T env0 concl0 1 (fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) c p in let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h @@ -1123,10 +1154,10 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_X, end_X = mk_tpattern_matcher sigma noindex holep in let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in - let concl = find_T env0 concl0 1 (fun env c h -> + let concl = find_T env0 concl0 1 (fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) c p in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h (fun env c h -> + fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> find_E env e_body h do_subst))) in let _ = end_E () in let _ = end_X () in let _ = end_T () in concl @@ -1140,13 +1171,13 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher sigma occ holep in - let concl = find_TE env0 concl0 1 (fun env c h -> + let concl = find_TE env0 concl0 1 (fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) c p in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h (fun env c h -> + fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> let e_sigma = unify_HO env sigma e_body e in let e_body = fs e_sigma e in - do_subst env e_body h))) in + do_subst env e_body e_body h))) in let _ = end_X () in let _ = end_TE () in concl ;; @@ -1162,7 +1193,7 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let find_R, conclude = let r = ref None in - (fun env c h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context); + (fun env c _ h' -> do_once r (fun () -> c, Evd.empty_evar_universe_context); mkRel (h'+h-1)), (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in @@ -1180,7 +1211,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let ise, u = mk_tpattern env sigma0 (ise,t) ok L2R p in let find_U, end_U = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in - let concl = find_U env concl h (fun _ _ -> mkRel) in + let concl = find_U env concl h (fun _ _ _ -> mkRel) in let rdx, _, (sigma, uc, p) = end_U () in sigma, uc, p, concl, rdx @@ -1238,6 +1269,27 @@ TACTIC EXTEND ssrat | [ "ssrpattern" ssrpatternarg(arg) ] -> [ Proofview.V82.tactic (ssrpatterntac ist arg) ] END +let ssrinstancesof ist arg gl = + let ok rhs lhs ise = true in +(* not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *) + let env, sigma, concl = pf_env gl, project gl, pf_concl gl in + let sigma0, cpat = interp_cpattern ist gl arg None in + let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in + let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in + let find, conclude = + mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true + sigma None (etpat,[tpat]) in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + ppnl (str"BEGIN INSTANCES"); + try + while true do + ignore(find env concl 1 ~k:print) + done; raise NoMatch + with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl + +TACTIC EXTEND ssrinstoftpat +| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof ist arg) ] +END (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli index 0976be7..b7d8d18 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli +++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli @@ -77,9 +77,9 @@ val interp_cpattern : * to signal the complement of this set (i.e. {-1 3}) *) type occ = (bool * int list) option -(** Substitution function. The [int] argument is the number of binders - traversed so far *) -type subst = env -> constr -> int -> constr +(** [subst e p t i]. [i] is the number of binders + traversed so far, [p] the term from the pattern, [t] the matched one *) +type subst = env -> constr -> constr -> int -> constr (** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every [occ] occurrence of [pat]. The [int] argument is the number of @@ -120,7 +120,7 @@ val pr_dir_side : ssrdir -> Pp.std_ppcmds (** a pattern for a term with wildcards *) type tpattern -(** [mk_tpattern env sigma0 sigma_t ok p_origin dir p] compiles a term [t] +(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern]. The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok] callback is used to filter occurrences. @@ -161,6 +161,7 @@ type conclude = be passed to tune the [UserError] eventually raised (useful if the pattern is coming from the LHS/RHS of an equation) *) val mk_tpattern_matcher : + ?all_instances:bool -> ?raise_NoMatch:bool -> ?upats_origin:ssrdir * constr -> evar_map -> occ -> evar_map * tpattern list -> diff --git a/mathcomp/ssrtest/explain_match.v b/mathcomp/ssrtest/explain_match.v new file mode 100644 index 0000000..b79453b --- /dev/null +++ b/mathcomp/ssrtest/explain_match.v @@ -0,0 +1,12 @@ +Require Import ssreflect ssrbool ssrnat. + +Definition addnAC := (addnA, addnC). + +Lemma test x y z : x + y + z = x + y. + +ssrinstancesoftpat (_ + _). +ssrinstancesofruleL2R addnC. +ssrinstancesofruleR2L addnA. +ssrinstancesofruleR2L addnAC. +Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *) +Admitted.
\ No newline at end of file |