diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/g_ssrmatching.mlg | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 104 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 8 |
3 files changed, 52 insertions, 62 deletions
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 33e523a4a4..2252435658 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -107,7 +107,7 @@ ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY { pr_rpattern } END TACTIC EXTEND ssrinstoftpat -| [ "ssrinstancesoftpat" cpattern(arg) ] -> { Proofview.V82.tactic (ssrinstancesof arg) } +| [ "ssrinstancesoftpat" cpattern(arg) ] -> { ssrinstancesof arg } END { diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index d5a781e472..adaf7c8cc1 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -14,7 +14,6 @@ open Ltac_plugin open Names open Pp open Genarg -open Stdarg open Term open Context module CoqConstr = Constr @@ -22,7 +21,6 @@ open CoqConstr open Vars open Libnames open Tactics -open Tacticals open Termops open Recordops open Tacmach @@ -173,8 +171,6 @@ let loc_ofCG = function let mk_term k c ist = k, (mkRHole, Some c), ist let mk_lterm = mk_term ' ' -let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty - let nf_evar sigma c = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) @@ -932,31 +928,15 @@ let id_of_Cterm t = match id_of_cpattern t with | Some x -> x | None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here" -let of_ftactic ftac gl = - let r = ref None in - let tac = Ftactic.run ftac (fun ans -> r := Some ans; Proofview.tclUNIT ()) in - let tac = Proofview.V82.of_tactic tac in - let { sigma = sigma } = tac gl in - let ans = match !r with - | None -> assert false (* If the tactic failed we should not reach this point *) - | Some ans -> ans - in - (sigma, ans) - -let interp_wit wit ist gl x = - let globarg = in_gen (glbwit wit) x in - let arg = interp_genarg ist globarg in - let (sigma, arg) = of_ftactic arg gl in - sigma, Value.cast (topwit wit) arg -let interp_open_constr ist gl gc = - interp_wit wit_open_constr ist gl gc -let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c +let interp_open_constr ist env sigma gc = + Tacinterp.interp_open_constr ist env sigma gc +let pf_intern_term env sigma (_, c, ist) = glob_constr ist env sigma c let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t -let interp_term gl = function +let interp_term env sigma = function | (_, c, Some ist) -> - on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c) + on_snd EConstr.Unsafe.to_constr (interp_open_constr ist env sigma c) | _ -> errorstrm (str"interpreting a term with no ist") let thin id sigma goal = @@ -982,7 +962,7 @@ let pr_ist { lfun= lfun } = pr_id id ++ str":" ++ Geninterp.Val.pr ty) (Id.Map.bindings lfun) *) -let interp_pattern ?wit_ssrpatternarg gl red redty = +let interp_pattern ?wit_ssrpatternarg env sigma0 red redty = pp(lazy(str"interpreting: " ++ pr_pattern red)); let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in @@ -990,7 +970,7 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = let mkG ?(k=' ') x ist = k,(x,None), ist in let ist_of (_,_,ist) = ist in let decode (_,_,ist as t) ?reccall f g = - try match DAst.get (pf_intern_term gl t) with + try match DAst.get (pf_intern_term env sigma0 t) with | GCast(t,CastConv c) when isGHole t && isGLambda c-> let (x, c) = destGLambda c in f x (' ',(c,None),ist) @@ -1008,7 +988,7 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = let cleanup_XinE h x rp sigma = let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in let to_clean, update = (* handle rename if x is already used *) - let ctx = pf_hyps gl in + let ctx = Environ.named_context env in let len = Context.Named.length ctx in let name = ref None in try ignore(Context.Named.lookup x ctx); (name, fun k -> @@ -1019,7 +999,6 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = name := Some (Context.Named.Declaration.get_id (List.nth nctx (nlen - len - 1))) end) with Not_found -> ref (Some x), fun _ -> () in - let sigma0 = project gl in let new_evars = let rec aux acc t = match kind t with | Evar (k,_) -> @@ -1072,13 +1051,13 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = match red with | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast) | X_In_T (x,t) -> - let gty = pf_intern_term gl ty in + let gty = pf_intern_term env sigma0 ty in E_As_X_In_T (mkG (mkRCast mkRHole gty) (ist_of ty), x, t) | E_In_X_In_T (e,x,t) -> - let ty = mkG (pf_intern_term gl ty) (ist_of ty) in + let ty = mkG (pf_intern_term env sigma0 ty) (ist_of ty) in E_In_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | E_As_X_In_T (e,x,t) -> - let ty = mkG (pf_intern_term gl ty) (ist_of ty) in + let ty = mkG (pf_intern_term env sigma0 ty) (ist_of ty) in E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | red -> red in pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); @@ -1086,12 +1065,12 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)), ist | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None), ist in match red with - | T t -> let sigma, t = interp_term gl t in sigma, T t - | In_T t -> let sigma, t = interp_term gl t in sigma, In_T t + | T t -> let sigma, t = interp_term env sigma0 t in sigma, T t + | In_T t -> let sigma, t = interp_term env sigma0 t in sigma, In_T t | X_In_T (x, rp) | In_X_In_T (x, rp) -> let mk x p = match red with X_In_T _ -> X_In_T(x,p) | _ -> In_X_In_T(x,p) in let rp = mkXLetIn (Name x) rp in - let sigma, rp = interp_term gl rp in + let sigma, rp = interp_term env sigma0 rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in let rp = subst1 h (nf_evar sigma rp) in @@ -1100,15 +1079,15 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = let mk e x p = match red with E_In_X_In_T _ ->E_In_X_In_T(e,x,p)|_->E_As_X_In_T(e,x,p) in let rp = mkXLetIn (Name x) rp in - let sigma, rp = interp_term gl rp in + let sigma, rp = interp_term env sigma0 rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in let rp = subst1 h (nf_evar sigma rp) in - let sigma, e = interp_term (re_sig (sig_it gl) sigma) e in + let sigma, e = interp_term env sigma e in sigma, mk e h rp ;; -let interp_cpattern gl red redty = interp_pattern gl (T red) redty;; -let interp_rpattern ~wit_ssrpatternarg gl red = interp_pattern ~wit_ssrpatternarg gl red None;; +let interp_cpattern env sigma red redty = interp_pattern env sigma (T red) redty;; +let interp_rpattern ~wit_ssrpatternarg env sigma red = interp_pattern ~wit_ssrpatternarg env sigma red None;; let id_of_pattern = function | _, T t -> (match kind t with Var id -> Some id | _ -> None) @@ -1245,23 +1224,23 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let rdx, _, (sigma, uc, p) = end_U () in sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx -let fill_occ_term env cl occ sigma0 (sigma, t) = +let fill_occ_term env sigma0 cl occ (sigma, t) = try let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars") - else cl, (Evd.merge_universe_context sigma' uc, t') + else cl, t' with NoMatch -> try let sigma', uc, t' = unif_end env sigma0 (create_evar_defs sigma) t (fun _ -> true) in if sigma' != sigma0 then raise NoMatch - else cl, (Evd.merge_universe_context sigma' uc, t') + else cl, t' with _ -> errorstrm (str "partial term " ++ pr_econstr_pat env sigma t ++ str " does not match any subterm of the goal") let pf_fill_occ_term gl occ t = let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in - let cl,(_,t) = fill_occ_term env concl occ sigma0 t in + let cl, t = fill_occ_term env sigma0 concl occ t in cl, t let cpattern_of_id id = @@ -1286,18 +1265,23 @@ let wit_ssrpatternarg = wit_rpatternty let interp_rpattern = interp_rpattern ~wit_ssrpatternarg -let ssrpatterntac _ist arg gl = - let pat = interp_rpattern gl arg in - let sigma0 = project gl in - let concl0 = pf_concl gl in +let ssrpatterntac _ist arg = + let open Proofview.Notations in + Proofview.Goal.enter begin fun gl -> + let sigma0 = Proofview.Goal.sigma gl in + let concl0 = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let pat = interp_rpattern env sigma0 arg in let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = - fill_occ_pattern (pf_env gl) sigma0 concl0 pat noindex 1 in + fill_occ_pattern env sigma0 concl0 pat noindex 1 in let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in - let gl, tty = pf_type_of gl t in + let sigma, tty = Typing.type_of env sigma0 t in let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in - Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl + Proofview.Unsafe.tclEVARS sigma <*> + convert_concl ~check:true concl DEFAULTcast + end (* Register "ssrpattern" tactic *) let () = @@ -1305,7 +1289,7 @@ let () = let arg = let v = Id.Map.find (Names.Id.of_string "pattern") ist.lfun in Value.cast (topwit wit_ssrpatternarg) v in - Proofview.V82.tactic (ssrpatterntac ist arg) in + ssrpatterntac ist arg in let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = @@ -1315,25 +1299,29 @@ let () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in Mltop.declare_cache_obj obj "ssrmatching_plugin" -let ssrinstancesof arg gl = +let ssrinstancesof arg = + Proofview.Goal.enter begin fun gl -> let ok rhs lhs ise = true in (* not (equal lhs (Evarutil.nf_evar ise rhs)) in *) - let env, sigma, concl = pf_env gl, project gl, pf_concl gl in - let concl = EConstr.Unsafe.to_constr concl in - let sigma0, cpat = interp_cpattern gl arg None in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let concl = EConstr.to_constr ~abort_on_undefined_evars:false sigma concl in + let sigma0, cpat = interp_cpattern env sigma 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_env (pf_env gl) (gl.sigma) p ++ spc() - ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) c)); c in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env env (Proofview.Goal.sigma gl) p ++ spc() + ++ str "matches:" ++ spc() ++ pr_constr_env env (Proofview.Goal.sigma gl) 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 + with NoMatch -> ppnl (str"END INSTANCES"); Tacticals.New.tclIDTAC + end module Internal = struct diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 31b414cc42..17b47227cb 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -57,7 +57,7 @@ val redex_of_pattern : (** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat] in the current [Ltac] interpretation signature [ise] and tactic input [gl]*) val interp_rpattern : - goal sigma -> + Environ.env -> Evd.evar_map -> rpattern -> pattern @@ -65,7 +65,7 @@ val interp_rpattern : in the current [Ltac] interpretation signature [ise] and tactic input [gl]. [ty] is an optional type for the redex of [cpat] *) val interp_cpattern : - goal sigma -> + Environ.env -> Evd.evar_map -> cpattern -> (glob_constr_and_expr * Geninterp.interp_sign) option -> pattern @@ -191,6 +191,8 @@ val mk_tpattern_matcher : * by [Rel 1] and the instance of [t] *) val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t +val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t + (* It may be handy to inject a simple term into the first form of cpattern *) val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> cpattern @@ -230,7 +232,7 @@ val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma (* One can also "Set SsrMatchingDebug" from a .v *) val debug : bool -> unit -val ssrinstancesof : cpattern -> Tacmach.tactic +val ssrinstancesof : cpattern -> unit Proofview.tactic (** Functions used for grammar extensions. Do not use. *) |