diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 81 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 4 |
2 files changed, 47 insertions, 38 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 552a4048b1..5eb106cc26 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -16,6 +16,7 @@ open Pp open Genarg open Stdarg open Term +open Context module CoqConstr = Constr open CoqConstr open Vars @@ -96,14 +97,20 @@ let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c let prl_constr_expr = pr_lconstr_expr let pr_constr_expr = pr_constr_expr -let prl_glob_constr_and_expr = function - | _, Some c -> prl_constr_expr c +let prl_glob_constr_and_expr env sigma = function + | _, Some c -> prl_constr_expr env sigma c | c, None -> prl_glob_constr c -let pr_glob_constr_and_expr = function - | _, Some c -> pr_constr_expr c +let pr_glob_constr_and_expr env sigma = function + | _, Some c -> pr_constr_expr env sigma c | c, None -> pr_glob_constr c -let pr_term (k, c, _) = pr_guarded (guard_term k) pr_glob_constr_and_expr c -let prl_term (k, c, _) = pr_guarded (guard_term k) prl_glob_constr_and_expr c +let pr_term (k, c, _) = + let env = Global.env () in + let sigma = Evd.from_env env in + pr_guarded (guard_term k) (pr_glob_constr_and_expr env sigma) c +let prl_term (k, c, _) = + let env = Global.env () in + let sigma = Evd.from_env env in + pr_guarded (guard_term k) (prl_glob_constr_and_expr env sigma) c (** Adding a new uninterpreted generic argument type *) let add_genarg tag pr = @@ -112,7 +119,7 @@ let add_genarg tag pr = let glob ist x = (ist, x) in let subst _ x = x in let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in - let gen_pr _ _ _ = pr in + let gen_pr env sigma _ _ _ = pr env sigma in let () = Genintern.register_intern0 wit glob in let () = Genintern.register_subst0 wit subst in let () = Geninterp.register_interp0 wit interp in @@ -213,7 +220,7 @@ let unif_EQ_args env sigma pa a = loop 0 let unif_HO env ise p c = - try Evarconv.the_conv_x env p c ise + try Evarconv.unify_delay env ise p c with Evarconv.UnableToUnify(ise, err) -> raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) @@ -361,10 +368,9 @@ let isRigid c = match kind c with | _ -> false let hole_var = mkVar (Id.of_string "_") -let pr_constr_pat c0 = +let pr_constr_pat env sigma c0 = let rec wipe_evar c = if isEvar c then hole_var else map wipe_evar c in - let sigma, env = Pfedit.get_current_context () in pr_constr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) @@ -383,7 +389,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = | Context.Named.Declaration.LocalDef (x, b, t) -> d, mkNamedLetIn x (put b) (put t) c | Context.Named.Declaration.LocalAssum (x, t) -> - mkVar x :: d, mkNamedProd x (put t) c in + mkVar x.binder_name :: d, mkNamedProd x (put t) c in let a, t = Context.Named.fold_inside abs_dc ~init:([], (put @@ EConstr.Unsafe.to_constr evi.evar_concl)) @@ -416,7 +422,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = (match p_origin with None -> CErrors.user_err Pp.(str "indeterminate pattern") | Some (dir, rule) -> errorstrm (str "indeterminate " ++ pr_dir_side dir - ++ str " in " ++ pr_constr_pat rule)) + ++ str " in " ++ pr_constr_pat env ise rule)) | LetIn (_, v, _, b) -> if b <> mkRel 1 then KpatLet, f, a else KpatFlex, v, a | Lambda _ -> KpatLam, f, a @@ -548,7 +554,7 @@ let match_upats_FO upats env sigma0 ise orig_c = if skip || not (closed0 c') then () else try let _ = match u.up_k with | KpatFlex -> - let kludge v = mkLambda (Anonymous, mkProp, v) in + let kludge v = mkLambda (make_annot Anonymous Sorts.Relevant, mkProp, v) in unif_FO env ise (kludge u.up_FO) (kludge c') | KpatLet -> let kludge vla = @@ -636,8 +642,8 @@ let assert_done r = let assert_done_multires r = match !r with | None -> CErrors.anomaly (str"do_once never called.") - | Some (n, xs) -> - r := Some (n+1,xs); + | Some (e, n, xs) -> + r := Some (e, n+1,xs); try List.nth xs n with Failure _ -> raise NoMatch type subst = Environ.env -> constr -> constr -> int -> constr @@ -683,14 +689,15 @@ let mk_tpattern_matcher ?(all_instances=false) | _ -> false) | _ -> unif_EQ env sigma u.up_f in let p2t p = mkApp(p.up_f,p.up_a) in -let source () = match upats_origin, upats with +let source env = match upats_origin, upats with | None, [p] -> (if fixed_upat ise p then str"term " else str"partial term ") ++ - pr_constr_pat (p2t p) ++ spc() + pr_constr_pat env ise (p2t p) ++ spc() | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ - pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl() + pr_constr_pat env ise rule ++ fnl() ++ ws 4 ++ + pr_constr_pat env ise (p2t p) ++ fnl() | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ - pr_constr_pat rule ++ spc() + pr_constr_pat env ise rule ++ spc() | _, [] | None, _::_::_ -> CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in let on_instance, instances = @@ -720,23 +727,23 @@ let rec uniquize = function if not all_instances then match_upats_FO upats env sigma0 ise c; failed_because_of_TC:=match_upats_HO ~on_instance upats env sigma0 ise c; raise NoMatch - with FoundUnif sigma_u -> 0,[sigma_u] + with FoundUnif sigma_u -> env,0,[sigma_u] | (NoMatch|NoProgress) when all_instances && instances () <> [] -> - 0, uniquize (instances ()) + env, 0, uniquize (instances ()) | NoMatch when (not raise_NoMatch) -> if !failed_because_of_TC then - errorstrm (source ()++strbrk"matches but type classes inference fails") + errorstrm (source env++strbrk"matches but type classes inference fails") else - errorstrm (source () ++ str "does not match any subterm of the goal") + errorstrm (source env ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> let dir = match upats_origin with Some (d,_) -> d | _ -> CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in - errorstrm (str"all matches of "++source()++ + errorstrm (str"all matches of "++source env++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); 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 + else List.hd (pi3(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 @@ -765,18 +772,18 @@ let rec uniquize = function mkApp (f', Array.map_left (subst_loop acc) a) in subst_loop (env,h) c) : find_P), ((fun () -> - let sigma, uc, ({up_f = pf; up_a = pa} as u) = + let env, (sigma, uc, ({up_f = pf; up_a = pa} as u)) = match !upat_that_matched with - | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch + | Some (env,_,x) -> env,List.hd x | None when raise_NoMatch -> raise NoMatch | None -> CErrors.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) else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++ str(String.plural !nocc " occurrence") ++ match upats_origin with - | None -> str" of" ++ spc() ++ pr_constr_pat p' + | None -> str" of" ++ spc() ++ pr_constr_pat env sigma p' | Some (dir,rule) -> str" of the " ++ pr_dir_side dir ++ fnl() ++ - ws 4 ++ pr_constr_pat p' ++ fnl () ++ - str"of " ++ pr_constr_pat rule)) : conclude) + ws 4 ++ pr_constr_pat env sigma p' ++ fnl () ++ + str"of " ++ pr_constr_pat env sigma rule)) : conclude) type ('ident, 'term) ssrpattern = | T of 'term @@ -815,11 +822,11 @@ let pr_pattern_aux pr_constr = function pr_constr e ++ str " in " ++ pr_constr x ++ str " in " ++ pr_constr t | 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_pat (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p +let pp_pattern env (sigma, p) = + pr_pattern_aux (fun t -> pr_constr_pat env sigma (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p let pr_cpattern = pr_term -let wit_rpatternty = add_genarg "rpatternty" pr_pattern +let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern) let glob_ssrterm gs = function | k, (_, Some c), None -> @@ -1246,8 +1253,10 @@ let fill_occ_term env cl occ sigma0 (sigma, t) = if sigma' != sigma0 then raise NoMatch else cl, (Evd.merge_universe_context sigma' uc, t') with _ -> - errorstrm (str "partial term " ++ pr_constr_pat (EConstr.Unsafe.to_constr t) - ++ str " does not match any subterm of the goal") + errorstrm (str "partial term " ++ + pr_constr_pat env sigma + (EConstr.to_constr ~abort_on_undefined_evars:false 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 @@ -1286,7 +1295,7 @@ let ssrpatterntac _ist arg gl = 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 concl = EConstr.mkLetIn (Name (Id.of_string "selected"), t, tty, concl_x) 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 concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index ff2c900130..1143bcc813 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -46,7 +46,7 @@ type ('ident, 'term) ssrpattern = | E_As_X_In_T of 'term * 'ident * 'term type pattern = evar_map * (constr, constr) ssrpattern -val pp_pattern : pattern -> Pp.t +val pp_pattern : env -> pattern -> Pp.t (** Extracts the redex and applies to it the substitution part of the pattern. @raise Anomaly if called on [In_T] or [In_X_In_T] *) @@ -222,7 +222,7 @@ val loc_of_cpattern : cpattern -> Loc.t option val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool val cpattern_of_id : Names.Id.t -> cpattern -val pr_constr_pat : constr -> Pp.t +val pr_constr_pat : env -> evar_map -> constr -> Pp.t val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma |