From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/ssr/ssrfwd.ml | 319 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 319 insertions(+) create mode 100644 plugins/ssr/ssrfwd.ml (limited to 'plugins/ssr/ssrfwd.ml') diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml new file mode 100644 index 00000000..a5765feb --- /dev/null +++ b/plugins/ssr/ssrfwd.ml @@ -0,0 +1,319 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* ist, Ssrcommon.ssrterm_of_ast_closure_term t + | None -> assert false in + let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in + posetac id t (pf_merge_uc ucst gl) + +let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = + let pty = Option.map (fun { Ssrast.body; interp_env } -> + let ist = Option.get interp_env in + (mkRHole, Some body), ist) pty in + let pat = interp_cpattern gl pat pty in + let cl, sigma, env = pf_concl gl, project gl, pf_env gl in + let (c, ucst), cl = + let cl = EConstr.Unsafe.to_constr cl in + try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 + with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in + let gl = pf_merge_uc ucst gl in + let c = EConstr.of_constr c in + let cl = EConstr.of_constr cl in + if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++ + pr_constr_pat (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++ + str"Did you mean pose?") else + let c, (gl, cty) = match EConstr.kind sigma c with + | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) + | _ -> c, pfe_type_of gl c in + let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in + Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl + +open Util + +open Printer + +open Ssrast +open Ssripats + +let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false + +let inHaveTCResolution = Libobject.declare_object { + (Libobject.default_object "SSRHAVETCRESOLUTION") with + Libobject.cache_function = (fun (_,v) -> ssrhaveNOtcresolution := v); + Libobject.load_function = (fun _ (_,v) -> ssrhaveNOtcresolution := v); + Libobject.classify_function = (fun v -> Libobject.Keep v); +} +let _ = + Goptions.declare_bool_option + { Goptions.optname = "have type classes"; + Goptions.optkey = ["SsrHave";"NoTCResolution"]; + Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); + Goptions.optdepr = false; + Goptions.optwrite = (fun b -> + Lib.add_anonymous_leaf (inHaveTCResolution b)) } + + +open Constrexpr +open Glob_term +open Misctypes + +let combineCG t1 t2 f g = match t1, t2 with + | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) + | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2)) + | _, (_, (_, None)) -> anomaly "have: mixed C-G constr" + | _ -> anomaly "have: mixed G-C constr" + +let basecuttac name c gl = + let hd, gl = pf_mkSsrConst name gl in + let t = EConstr.mkApp (hd, [|c|]) in + let gl, _ = pf_e_type_of gl t in + Proofview.V82.of_tactic (Tactics.apply t) gl + +let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats) + +let havetac ist + (transp,((((clr, pats), binders), simpl), (((fk, _), t), hint))) + suff namefst gl += + let concl = pf_concl gl in + let skols, pats = + List.partition (function IPatAbstractVars _ -> true | _ -> false) pats in + let itac_mkabs = introstac skols in + let itac_c = introstac (IPatClear clr :: pats) in + let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in + let binderstac n = + let rec aux = function 0 -> [] | n -> IPatAnon One :: aux (n-1) in + Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC) + (introstac binders) in + let simpltac = introstac simpl in + let fixtc = + not !ssrhaveNOtcresolution && + match fk with FwdHint(_,true) -> false | _ -> true in + let hint = hinttac ist true hint in + let cuttac t gl = + if transp then + let have_let, gl = pf_mkSsrConst "ssr_have_let" gl in + let step = EConstr.mkApp (have_let, [|concl;t|]) in + let gl, _ = pf_e_type_of gl step in + applyn ~with_evars:true ~with_shelve:false 2 step gl + else basecuttac "ssr_have" t gl in + (* Introduce now abstract constants, so that everything sees them *) + let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in + let unlock_abs (idty,args_id) gl = + let gl, _ = pf_e_type_of gl idty in + pf_unify_HO gl args_id.(2) abstract_key in + Tacticals.tclTHENFIRST itac_mkabs (fun gl -> + let mkt t = mk_term xNoFlag t in + let mkl t = (xNoFlag, (t, None)) in + let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in + let interp_ty gl rtc t = + let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc ist gl t in a,b,u in + let open CAst in + let ct, cty, hole, loc = match Ssrcommon.ssrterm_of_ast_closure_term t with + | _, (_, Some { loc; v = CCast (ct, CastConv cty)}) -> + mkt ct, mkt cty, mkt (mkCHole None), loc + | _, (_, Some ct) -> + mkt ct, mkt (mkCHole None), mkt (mkCHole None), None + | _, (t, None) -> + begin match DAst.get t with + | GCast (ct, CastConv cty) -> + mkl ct, mkl cty, mkl mkRHole, t.CAst.loc + | _ -> mkl t, mkl mkRHole, mkl mkRHole, None + end + in + let gl, cut, sol, itac1, itac2 = + match fk, namefst, suff with + | FwdHave, true, true -> + 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 gl = pf_merge_uc uc gl in + let gl, ty = pfe_type_of gl t in + let ctx, _ = EConstr.decompose_prod_n_assum (project gl) 1 ty in + let assert_is_conv gl = + try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl + with _ -> errorstrm (str "Given proof term is not of type " ++ + pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in + gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c + | FwdHave, false, false -> + let skols = List.flatten (List.map (function + | IPatAbstractVars ids -> ids + | _ -> assert false) skols) in + let skols_args = + List.map (fun id -> Ssripats.Internal.examine_abstract (EConstr.mkVar id) gl) skols in + let gl = List.fold_right unlock_abs skols_args gl in + let sigma, t, uc, n_evars = + interp gl false (combineCG ct cty (mkCCast ?loc) mkRCast) in + if skols <> [] && n_evars <> 0 then + CErrors.user_err (Pp.strbrk @@ "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) -> + Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in + let tacopen_skols gl = + let stuff, g = Refiner.unpackage gl in + Refiner.repackage stuff (gs @ [g]) in + let gl, ty = pf_e_type_of gl t in + gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id, + Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac) + (Tacticals.tclTHEN tacopen_skols (fun gl -> + let abstract, gl = pf_mkSsrConst "abstract" gl in + Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl)) + | _,true,true -> + let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in + gl, EConstr.mkArrow ty concl, hint, itac, clr + | _,false,true -> + let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in + gl, EConstr.mkArrow ty concl, hint, id, itac_c + | _, false, false -> + let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in + gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac + | _, true, false -> assert false in + Tacticals.tclTHENS (cuttac cut) [ Tacticals.tclTHEN sol itac1; itac2 ] gl) + gl +;; + +let destProd_or_LetIn sigma c = + match EConstr.kind sigma c with + | Prod (n,ty,c) -> RelDecl.LocalAssum (n, ty), c + | LetIn (n,bo,ty,c) -> RelDecl.LocalDef (n, bo, ty), c + | _ -> raise DestKO + +let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = + let mkabs gen = abs_wgen false (fun x -> x) gen in + let mkclr gen clrs = clr_of_wgen gen clrs in + let mkpats = function + | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats + | _ -> fun x -> x in + let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with + | (a, (b, Some ct)) -> + begin match ct.CAst.v with + | CCast (_, CastConv cty) -> a, (b, Some cty) + | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" + end + | (a, (t, None)) -> + begin match DAst.get t with + | GCast (_, CastConv cty) -> a, (cty, None) + | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" + end + in + let cut_implies_goal = not (suff || ghave <> `NoGen) in + let c, args, ct, gl = + let gens = List.filter (function _, Some _ -> true | _ -> false) gens in + let concl = pf_concl gl in + let c = EConstr.mkProp in + let c = if cut_implies_goal then EConstr.mkArrow c concl else c in + let gl, args, c = List.fold_right mkabs gens (gl,[],c) in + let env, _ = + List.fold_left (fun (env, c) _ -> + let rd, c = destProd_or_LetIn (project gl) c in + EConstr.push_rel rd env, c) (pf_env gl, c) gens in + let sigma = project gl in + let (sigma, ev) = Evarutil.new_evar env sigma EConstr.mkProp in + let k, _ = EConstr.destEvar sigma ev in + let fake_gl = {Evd.it = k; Evd.sigma = sigma} in + let _, ct, _, uc = pf_interp_ty ist fake_gl ct in + let rec var2rel c g s = match EConstr.kind sigma c, g with + | Prod(Anonymous,_,c), [] -> EConstr.mkProd(Anonymous, EConstr.Vars.subst_vars s ct, c) + | Sort _, [] -> EConstr.Vars.subst_vars s ct + | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) + | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) + | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in + let c = var2rel c gens [] in + let rec pired c = function + | [] -> c + | t::ts as args -> match EConstr.kind sigma c with + | Prod(_,_,c) -> pired (EConstr.Vars.subst1 t c) ts + | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args) + | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in + c, args, pired c args, pf_merge_uc uc gl in + let tacipat pats = introstac pats in + let tacigens = + Tacticals.tclTHEN + (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0]))) + (introstac (List.fold_right mkpats gens [])) in + let hinttac = hinttac ist true hint in + let cut_kind, fst_goal_tac, snd_goal_tac = + match suff, ghave with + | true, `NoGen -> "ssr_wlog", Tacticals.tclTHEN hinttac (tacipat pats), tacigens + | false, `NoGen -> "ssr_wlog", hinttac, Tacticals.tclTHEN tacigens (tacipat pats) + | true, `Gen _ -> assert false + | false, `Gen id -> + if gens = [] then errorstrm(str"gen have requires some generalizations"); + let clear0 = old_cleartac clr0 in + let id, name_general_hyp, cleanup, pats = match id, pats with + | None, (IPatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats + | None, _ -> None, Tacticals.tclIDTAC, clear0, pats + | Some (Some id),_ -> Some id, introid id, clear0, pats + | Some _,_ -> + let id = mk_anon_id "tmp" (Tacmach.pf_ids_of_hyps gl) in + Some id, introid id, Tacticals.tclTHEN clear0 (Proofview.V82.of_tactic (Tactics.clear [id])), pats in + let tac_specialize = match id with + | None -> Tacticals.tclIDTAC + | Some id -> + if pats = [] then Tacticals.tclIDTAC else + let args = Array.of_list args in + ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); + ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); + Tacticals.tclTHENS (basecuttac "ssr_have" ct) + [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in + "ssr_have", + (if hint = nohint then tacigens else hinttac), + Tacticals.tclTHENLIST [name_general_hyp; tac_specialize; tacipat pats; cleanup] + in + Tacticals.tclTHENS (basecuttac cut_kind c) [fst_goal_tac; snd_goal_tac] gl + +(** The "suffice" tactic *) + +let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = + let htac = Tacticals.tclTHEN (introstac pats) (hinttac ist true hint) in + let c = match Ssrcommon.ssrterm_of_ast_closure_term c with + | (a, (b, Some ct)) -> + begin match ct.CAst.v with + | CCast (_, CastConv cty) -> a, (b, Some cty) + | _ -> anomaly "suff: ssr cast hole deleted by typecheck" + end + | (a, (t, None)) -> + begin match DAst.get t with + | GCast (_, CastConv cty) -> a, (cty, None) + | _ -> anomaly "suff: ssr cast hole deleted by typecheck" + end + in + let ctac gl = + let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in + basecuttac "ssr_suff" ty gl in + Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))] -- cgit v1.2.3