diff options
Diffstat (limited to 'mathcomp/ssreflect/plugin')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 183 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 | 108 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.mli | 9 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 116 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 | 108 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli | 9 |
6 files changed, 390 insertions, 143 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 0e04221..e05526e 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -44,6 +44,7 @@ open Coqlib open Glob_term open Util open Evd +open Sigma.Notations open Extend open Goptions open Tacexpr @@ -563,7 +564,9 @@ let pf_partial_solution gl t evl = let pf_new_evar gl ty = let sigma, env, it = project gl, pf_env gl, sig_it gl in - let sigma, extra = Evarutil.new_evar env sigma ty in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (extra, sigma, _) = Evarutil.new_evar env sigma ty in + let sigma = Sigma.to_evar_map sigma in re_sig it sigma, extra (* Basic tactics *) @@ -1040,10 +1043,7 @@ let ssrtac_expr = ssrtac_atom let ssrevaltac ist gtac = - let debug = match TacStore.get ist.extra f_debug with - | None -> Tactic_debug.DebugOff | Some level -> level - in - Proofview.V82.of_tactic (interp_tac_gen ist.lfun [] debug (globTacticIn (fun _ -> gtac))) + Proofview.V82.of_tactic (eval_tactic_ist ist gtac) (* fun gl -> let lfun = [tacarg_id, val_interp ist gl gtac] in interp_tac_gen lfun [] ist.debug tacarg_expr gl *) @@ -2397,7 +2397,7 @@ let glob_view_hints lvh = let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh)) -VERNAC COMMAND EXTEND HintView CLASSIFIED AS QUERY +VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF | [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] -> [ mapviewpos (add_view_hints (glob_view_hints lvh)) n 2 ] END @@ -2873,23 +2873,33 @@ let mk_abstract_id () = incr ssr_abstract_id; nat_of_n !ssr_abstract_id let ssrmkabs id gl = let env, concl = pf_env gl, pf_concl gl in - let step sigma = + let step = { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in let sigma, abstract_proof, abstract_ty = let sigma, (ty, _) = Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in let sigma, ablock = mkSsrConst "abstract_lock" env sigma in - let sigma, lock = Evarutil.new_evar env sigma ablock in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (lock, sigma, _) = Evarutil.new_evar env sigma ablock in + let sigma = Sigma.to_evar_map sigma in let sigma, abstract = mkSsrConst "abstract" env sigma in let abstract_ty = mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in - let sigma, m = Evarutil.new_evar env sigma abstract_ty in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (m, sigma, _) = Evarutil.new_evar env sigma abstract_ty in + let sigma = Sigma.to_evar_map sigma in sigma, m, abstract_ty in let sigma, kont = let rd = Name id, None, abstract_ty in - Evarutil.new_evar (Environ.push_rel rd env) sigma concl in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = Evarutil.new_evar (Environ.push_rel rd env) sigma concl in + let sigma = Sigma.to_evar_map sigma in + (sigma, ev) + in pp(lazy(pr_constr concl)); let term = mkApp (mkLambda(Name id,abstract_ty,kont) ,[|abstract_proof|]) in let sigma, _ = Typing.type_of env sigma term in - sigma, term in + Sigma.Unsafe.of_pair (term, sigma) + end } in Proofview.V82.of_tactic (Proofview.tclTHEN (Tactics.New.refine step) @@ -3304,7 +3314,7 @@ let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t = let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in sigma, Evarutil.nf_evar sigma ct in let n, c, abstracted_away, ucst = pf_abs_evars gl t in - List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c, ucst + List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c, ucst, n let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = let n_binders = ref 0 in @@ -3368,9 +3378,12 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ (mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma else match kind_of_type ty with | ProdType (_, src, tgt) -> - let sigma, x = - Evarutil.new_evar env (create_evar_defs sigma) - (if bi_types then Reductionops.nf_betaiota sigma src else src) in + let sigma = create_evar_defs sigma in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (x, sigma, _) = + Evarutil.new_evar env sigma + (if bi_types then Reductionops.nf_betaiota (Sigma.to_evar_map sigma) src else src) in + let sigma = Sigma.to_evar_map sigma in loop (subst1 x tgt) ((m - n,x) :: args) sigma (n-1) | CastType (t, _) -> loop t args sigma n | LetInType (_, v, _, t) -> loop (subst1 v t) args sigma n @@ -3381,7 +3394,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ (Reductionops.whd_betadeltaiota env sigma) ty in match kind_of_type ty with | ProdType _ -> loop ty args sigma n - | _ -> anomaly "saturate did not find enough products" + | _ -> raise NotEnoughProducts in loop ty [] sigma m @@ -3904,7 +3917,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = | _ -> false in let match_pat env p occ h cl = let sigma0 = project orig_gl in - pp(lazy(str"matching: " ++ pp_pattern p)); + pp(lazy(str"matching: " ++ pr_occ occ ++ pp_pattern p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 cl p occ h in pp(lazy(str" got: " ++ pr_constr c)); @@ -3924,6 +3937,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = with e when Errors.noncritical e -> p in (* finds the eliminator applies it to evars and c saturated as needed *) (* obtaining "elim ??? (c ???)". pred is the higher order evar *) + (* cty is None when the user writes _ (hence we can't make a pattern *) let cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl = match elim with | Some elim -> @@ -3934,7 +3948,15 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in let pred = List.assoc pred_id elim_args in let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in - None, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl + let cty, gl = + if Option.is_empty oc then None, gl + else + let c = Option.get oc in let gl, c_ty = pf_type_of gl c in + let pc = match c_gen with + | Some p -> interp_cpattern (Option.get ist) orig_gl p None + | _ -> mkTpat gl c in + Some(c, c_ty, pc), gl in + cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl | None -> let c = Option.get oc in let gl, c_ty = pf_type_of gl c in let ((kn, i) as ind, _ as indu), unfolded_c_ty = @@ -3945,8 +3967,11 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = let t, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in gl, t else - pf_eapply (fun env sigma -> - Indrec.build_case_analysis_scheme env sigma indu true) gl sort in + pf_eapply (fun env sigma () -> + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ind, sigma, _) = Indrec.build_case_analysis_scheme env sigma indu true sort in + let sigma = Sigma.to_evar_map sigma in + (sigma, ind)) gl () in let gl, elimty = pf_type_of gl elim in let pred_id,n_elim_args,is_rec,elim_is_dep,n_pred_args = analyze_eliminator elimty env (project gl) in @@ -3964,7 +3989,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl in pp(lazy(str"elim= "++ pr_constr_pat elim)); - pp(lazy(str"elimty= "++ pr_constr elimty)); + pp(lazy(str"elimty= "++ pr_constr_pat elimty)); let inf_deps_r = match kind_of_type elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) | _ -> assert false in @@ -3973,11 +3998,17 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = let c, c_ty, _, gl = pf_saturate gl c ~ty:c_ty n in let gl' = f c c_ty gl in Some (c, c_ty, gl, gl') - with NotEnoughProducts -> None | _ -> loop (n+1) in loop 0 in - let elim_is_dep, gl = match cty with - | None -> true, gl + with + | NotEnoughProducts -> None + | e when Errors.noncritical e -> loop (n+1) in loop 0 in + (* Here we try to understand if the main pattern/term the user gave is + * the first pattern to be matched (i.e. if elimty ends in P t1 .. tn, + * weather tn is the t the user wrote in 'elim: t' *) + let c_is_head_p, gl = match cty with + | None -> true, gl (* The user wrote elim: _ *) | Some (c, c_ty, _) -> let res = + (* we try to see if c unifies with the last arg of elim *) if elim_is_dep then None else let arg = List.assoc (n_elim_args - 1) elim_args in let gl, arg_ty = pf_type_of gl arg in @@ -3988,21 +4019,22 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = match res with | Some x -> x | None -> + (* we try to see if c unifies with the last inferred pattern *) let inf_arg = List.hd inf_deps_r in let gl, inf_arg_ty = pf_type_of gl inf_arg in match saturate_until gl c c_ty (fun _ c_ty gl -> pf_unify_HO gl c_ty inf_arg_ty) with | Some (c, _, _,gl) -> true, gl | None -> - errorstrm (str"Unable to apply the eliminator to the term"++ - spc()++pr_constr c++spc()++str"or to unify it's type with"++ - pr_constr inf_arg_ty) in - pp(lazy(str"elim_is_dep= " ++ bool elim_is_dep)); + errorstrm (str"Unable to apply the eliminator to the term"++ + spc()++pr_constr c++spc()++str"or to unify it's type with"++ + pr_constr inf_arg_ty) in + pp(lazy(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pf_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed * looking at the ones provided by the user and the inferred ones looking at * the type of the elimination principle *) - let pp_pat (_,p,_,_) = pp_pattern p in + let pp_pat (_,p,_,occ) = pr_occ occ ++ pp_pattern p in let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (fire_subst gl t) in let patterns, clr, gl = let rec loop patterns clr i = function @@ -4018,12 +4050,12 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> - pp(lazy(str"adding inferred pattern " ++ pr_constr_pat c)); + pp(lazy(str"adding inf pattern " ++ pr_constr_pat c)); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm (str "Too many dependent abstractions") in - let deps, head_p, inf_deps_r = match what, elim_is_dep, cty with - | `EConstr _, _, None -> anomaly "Simple welim with no term" + let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with + | `EConstr _, _, None -> anomaly "Simple elim with no term" | _, false, _ -> deps, [], inf_deps_r | `EGen gen, true, None -> deps @ [gen], [], inf_deps_r | _, true, Some (c, _, pc) -> @@ -4083,7 +4115,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = let erefl, gl = mkRefl t c gl in let erefl = fire_subst gl erefl in apply_type new_concl [erefl], gl in - let rel = k + if elim_is_dep then 1 else 0 in + let rel = k + if c_is_head_p then 1 else 0 in let src, gl = mkProt mkProp (mkApp (eq,[|t; c; mkRel rel|])) gl in let concl = mkArrow src (lift 1 concl) in let clr = if deps <> [] then clr else [] in @@ -4461,7 +4493,10 @@ let newssrcongrtac arg ist gl = | None -> t_fail () gl in let mk_evar gl ty = let env, sigma, si = pf_env gl, project gl, sig_it gl in - let sigma, x = Evarutil.new_evar env (create_evar_defs sigma) ty in + let sigma = create_evar_defs sigma in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (x, sigma, _) = Evarutil.new_evar env sigma ty in + let sigma = Sigma.to_evar_map sigma in x, re_sig si sigma in let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = mkApp (arr, lr) in @@ -4649,7 +4684,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 +4722,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 +4731,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 +4769,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 @@ -4773,7 +4808,11 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let beta = Reductionops.clos_norm_flags Closure.beta env sigma in let sigma, p = let sigma = create_evar_defs sigma in - Evarutil.new_evar env sigma (beta (subst1 new_rdx pred)) in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma (beta (subst1 new_rdx pred)) in + let sigma = Sigma.to_evar_map sigma in + (sigma, ev) + in let pred = mkNamedLambda pattern_id rdx_ty pred in let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in @@ -4902,7 +4941,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 @@ -4914,7 +4953,10 @@ let rwrxtac occ rdx_pat dir rule gl = pp(lazy(str"rewrule="++pr_constr t)); match kind_of_term t with | Prod (_, xt, at) -> - let ise, x = Evarutil.new_evar env (create_evar_defs sigma) xt in + let sigma = create_evar_defs sigma in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (x, sigma, _) = Evarutil.new_evar env sigma xt in + let ise = Sigma.to_evar_map sigma in loop d ise (mkApp (r, [|x|])) (subst1 x at) rs 0 | App (pr, a) when is_ind_ref pr coq_prod.Coqlib.typ -> let sr sigma = match kind_of_term (Tacred.hnf_constr env sigma r) with @@ -4973,7 +5015,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 +5046,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 +5063,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 _ = @@ -5496,7 +5570,7 @@ ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd END let ssrposetac ist (id, (_, t)) gl = - let sigma, t, ucst = pf_abs_ssrterm ist gl t in + let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in posetac id t (pf_merge_uc ucst gl) @@ -5654,7 +5728,7 @@ let unfold cl = (List.map (fun c -> F.fCONST (fst (destConst c))) cl @ [F.fBETA; F.fIOTA]))) let havegentac ist t gl = - let sigma, c, ucst = pf_abs_ssrterm ist gl t in + let sigma, c, ucst, _ = pf_abs_ssrterm ist gl t in let gl = pf_merge_uc ucst gl in let gl, cty = pf_type_of gl c in apply_type (mkArrow cty (pf_concl gl)) [c] gl @@ -5710,7 +5784,7 @@ let havetac ist errorstrm (str"Suff have does not accept a proof term") | FwdHave, false, true -> let cty = combineCG cty hole (mkCArrow loc) mkRArrow in - let _, t, uc = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in + let _,t,uc,_ = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in let gl = pf_merge_uc uc gl in let gl, ty = pf_type_of gl t in let ctx, _ = decompose_prod_n 1 ty in @@ -5726,8 +5800,12 @@ let havetac ist let skols_args = List.map (fun id -> examine_abstract (mkVar id) gl) skols in let gl = List.fold_right unlock_abs skols_args gl in - let sigma, t, uc = + let sigma, t, uc, n_evars = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in + if skols <> [] && n_evars <> 0 then + Errors.error ("Automatic generalization of unresolved implicit "^ + "arguments together with abstract variables is "^ + "not supported"); let gl = re_sig (sig_it gl) (Evd.merge_universe_context sigma uc) in let gs = List.map (fun (_,a) -> @@ -5938,7 +6016,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = List.fold_left (fun (env, c) _ -> let rd, c = destProd_or_LetIn c in Environ.push_rel rd env, c) (pf_env gl, c) gens in - let sigma, ev = Evarutil.new_evar env (project gl) Term.mkProp in + let sigma = project gl in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma Term.mkProp in + let sigma = Sigma.to_evar_map sigma in let k, _ = Term.destEvar ev in let fake_gl = {Evd.it = k; Evd.sigma = sigma} in let _, ct, _, uc = pf_interp_ty ist fake_gl ct in diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 index effd193..aa44fec 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 - pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); - if !skip_occ then (ignore(k env u.up_t 0); c) else + 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 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) @@ -815,7 +846,7 @@ let pr_pattern_aux pr_constr = function | E_As_X_In_T (e,x,t) -> pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t let pp_pattern (sigma, p) = - pr_pattern_aux (fun t -> pr_constr (pi3 (nf_open_term sigma sigma t))) p + pr_pattern_aux (fun t -> pr_constr_pat (pi3 (nf_open_term sigma sigma t))) p let pr_cpattern = pr_term let pr_rpattern _ _ _ = pr_pattern @@ -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 ;; @@ -1161,9 +1192,13 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma 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); - mkRel (h'+h-1)), + let do_make_rel, occ = + if occ = Some(true,[]) then false, Some(false,[1]) else true, occ in + let find_R, conclude = + let r = ref None in + (fun env c _ h' -> + do_once r (fun () -> c, Evd.empty_evar_universe_context); + if do_make_rel then mkRel (h'+h-1) else c), (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 let e = conclude cl in @@ -1180,7 +1215,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 +1273,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 e6636cb..20fd720 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 @@ -2391,7 +2391,7 @@ let glob_view_hints lvh = let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh)) -VERNAC COMMAND EXTEND HintView CLASSIFIED AS QUERY +VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF | [ "Hint" "View" ssrviewposspc(n) ne_ssrhintref_list(lvh) ] -> [ mapviewpos (add_view_hints (glob_view_hints lvh)) n 2 ] END @@ -3298,7 +3298,7 @@ let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t = let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in sigma, Evarutil.nf_evar sigma ct in let n, c, abstracted_away, ucst = pf_abs_evars gl t in - List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c, ucst + List.fold_left Evd.remove sigma abstracted_away, pf_abs_cterm gl n c, ucst, n let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = let n_binders = ref 0 in @@ -3375,7 +3375,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ (Reductionops.whd_betadeltaiota env sigma) ty in match kind_of_type ty with | ProdType _ -> loop ty args sigma n - | _ -> anomaly "saturate did not find enough products" + | _ -> raise NotEnoughProducts in loop ty [] sigma m @@ -3898,7 +3898,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = | _ -> false in let match_pat env p occ h cl = let sigma0 = project orig_gl in - pp(lazy(str"matching: " ++ pp_pattern p)); + pp(lazy(str"matching: " ++ pr_occ occ ++ pp_pattern p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 cl p occ h in pp(lazy(str" got: " ++ pr_constr c)); @@ -3918,6 +3918,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = with e when Errors.noncritical e -> p in (* finds the eliminator applies it to evars and c saturated as needed *) (* obtaining "elim ??? (c ???)". pred is the higher order evar *) + (* cty is None when the user writes _ (hence we can't make a pattern *) let cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl = match elim with | Some elim -> @@ -3928,7 +3929,15 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in let pred = List.assoc pred_id elim_args in let elimty = Reductionops.whd_betadeltaiota env (project gl) elimty in - None, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl + let cty, gl = + if Option.is_empty oc then None, gl + else + let c = Option.get oc in let gl, c_ty = pf_type_of gl c in + let pc = match c_gen with + | Some p -> interp_cpattern (Option.get ist) orig_gl p None + | _ -> mkTpat gl c in + Some(c, c_ty, pc), gl in + cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl | None -> let c = Option.get oc in let gl, c_ty = pf_type_of gl c in let ((kn, i) as ind, _ as indu), unfolded_c_ty = @@ -3958,7 +3967,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl in pp(lazy(str"elim= "++ pr_constr_pat elim)); - pp(lazy(str"elimty= "++ pr_constr elimty)); + pp(lazy(str"elimty= "++ pr_constr_pat elimty)); let inf_deps_r = match kind_of_type elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) | _ -> assert false in @@ -3967,11 +3976,17 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = let c, c_ty, _, gl = pf_saturate gl c ~ty:c_ty n in let gl' = f c c_ty gl in Some (c, c_ty, gl, gl') - with NotEnoughProducts -> None | _ -> loop (n+1) in loop 0 in - let elim_is_dep, gl = match cty with - | None -> true, gl + with + | NotEnoughProducts -> None + | e when Errors.noncritical e -> loop (n+1) in loop 0 in + (* Here we try to understand if the main pattern/term the user gave is + * the first pattern to be matched (i.e. if elimty ends in P t1 .. tn, + * weather tn is the t the user wrote in 'elim: t' *) + let c_is_head_p, gl = match cty with + | None -> true, gl (* The user wrote elim: _ *) | Some (c, c_ty, _) -> let res = + (* we try to see if c unifies with the last arg of elim *) if elim_is_dep then None else let arg = List.assoc (n_elim_args - 1) elim_args in let gl, arg_ty = pf_type_of gl arg in @@ -3982,21 +3997,22 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = match res with | Some x -> x | None -> + (* we try to see if c unifies with the last inferred pattern *) let inf_arg = List.hd inf_deps_r in let gl, inf_arg_ty = pf_type_of gl inf_arg in match saturate_until gl c c_ty (fun _ c_ty gl -> pf_unify_HO gl c_ty inf_arg_ty) with | Some (c, _, _,gl) -> true, gl | None -> - errorstrm (str"Unable to apply the eliminator to the term"++ - spc()++pr_constr c++spc()++str"or to unify it's type with"++ - pr_constr inf_arg_ty) in - pp(lazy(str"elim_is_dep= " ++ bool elim_is_dep)); + errorstrm (str"Unable to apply the eliminator to the term"++ + spc()++pr_constr c++spc()++str"or to unify it's type with"++ + pr_constr inf_arg_ty) in + pp(lazy(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pf_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed * looking at the ones provided by the user and the inferred ones looking at * the type of the elimination principle *) - let pp_pat (_,p,_,_) = pp_pattern p in + let pp_pat (_,p,_,occ) = pr_occ occ ++ pp_pattern p in let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (fire_subst gl t) in let patterns, clr, gl = let rec loop patterns clr i = function @@ -4012,12 +4028,12 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> - pp(lazy(str"adding inferred pattern " ++ pr_constr_pat c)); + pp(lazy(str"adding inf pattern " ++ pr_constr_pat c)); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm (str "Too many dependent abstractions") in - let deps, head_p, inf_deps_r = match what, elim_is_dep, cty with - | `EConstr _, _, None -> anomaly "Simple welim with no term" + let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with + | `EConstr _, _, None -> anomaly "Simple elim with no term" | _, false, _ -> deps, [], inf_deps_r | `EGen gen, true, None -> deps @ [gen], [], inf_deps_r | _, true, Some (c, _, pc) -> @@ -4077,7 +4093,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl = let erefl, gl = mkRefl t c gl in let erefl = fire_subst gl erefl in apply_type new_concl [erefl], gl in - let rel = k + if elim_is_dep then 1 else 0 in + let rel = k + if c_is_head_p then 1 else 0 in let src, gl = mkProt mkProp (mkApp (eq,[|t; c; mkRel rel|])) gl in let concl = mkArrow src (lift 1 concl) in let clr = if deps <> [] then clr else [] in @@ -4643,7 +4659,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 +4697,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 +4706,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 +4744,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 +4912,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 +4983,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 +5014,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 +5031,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 _ = @@ -5490,7 +5538,7 @@ ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd END let ssrposetac ist (id, (_, t)) gl = - let sigma, t, ucst = pf_abs_ssrterm ist gl t in + let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in posetac id t (pf_merge_uc ucst gl) @@ -5648,7 +5696,7 @@ let unfold cl = (List.map (fun c -> F.fCONST (fst (destConst c))) cl @ [F.fBETA; F.fIOTA]))) let havegentac ist t gl = - let sigma, c, ucst = pf_abs_ssrterm ist gl t in + let sigma, c, ucst, _ = pf_abs_ssrterm ist gl t in let gl = pf_merge_uc ucst gl in let gl, cty = pf_type_of gl c in apply_type (mkArrow cty (pf_concl gl)) [c] gl @@ -5704,7 +5752,7 @@ let havetac ist errorstrm (str"Suff have does not accept a proof term") | FwdHave, false, true -> let cty = combineCG cty hole (mkCArrow loc) mkRArrow in - let _, t, uc = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in + let _,t,uc,_ = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in let gl = pf_merge_uc uc gl in let gl, ty = pf_type_of gl t in let ctx, _ = decompose_prod_n 1 ty in @@ -5720,8 +5768,12 @@ let havetac ist let skols_args = List.map (fun id -> examine_abstract (mkVar id) gl) skols in let gl = List.fold_right unlock_abs skols_args gl in - let sigma, t, uc = + let sigma, t, uc, n_evars = interp gl false (combineCG ct cty (mkCCast loc) mkRCast) in + if skols <> [] && n_evars <> 0 then + Errors.error ("Automatic generalization of unresolved implicit "^ + "arguments together with abstract variables is "^ + "not supported"); let gl = re_sig (sig_it gl) (Evd.merge_universe_context sigma uc) in let gs = List.map (fun (_,a) -> diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 index c47c946..74f42f6 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 - pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); - if !skip_occ then (ignore(k env u.up_t 0); c) else + 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 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) @@ -815,7 +846,7 @@ let pr_pattern_aux pr_constr = function | E_As_X_In_T (e,x,t) -> pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t let pp_pattern (sigma, p) = - pr_pattern_aux (fun t -> pr_constr (pi3 (nf_open_term sigma sigma t))) p + pr_pattern_aux (fun t -> pr_constr_pat (pi3 (nf_open_term sigma sigma t))) p let pr_cpattern = pr_term let pr_rpattern _ _ _ = pr_pattern @@ -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 ;; @@ -1161,9 +1192,13 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma 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); - mkRel (h'+h-1)), + let do_make_rel, occ = + if occ = Some(true,[]) then false, Some(false,[1]) else true, occ in + let find_R, conclude = + let r = ref None in + (fun env c _ h' -> + do_once r (fun () -> c, Evd.empty_evar_universe_context); + if do_make_rel then mkRel (h'+h-1) else c), (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 let e = conclude cl in @@ -1180,7 +1215,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 +1273,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 -> |