diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 5 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 78 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 40 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 20 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 12 |
6 files changed, 95 insertions, 62 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 6956120a6a..2a84469af0 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -246,6 +246,7 @@ let interp_refine ist gl rc = fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in @@ -1175,7 +1176,7 @@ let genstac (gens, clr) = tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens) let gen_tmp_ids - ?(ist=Geninterp.({ lfun = Id.Map.empty; extra = Tacinterp.TacStore.empty })) gl + ?(ist=Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })) gl = let gl, ctx = pull_ctx gl in push_ctxs ctx @@ -1232,7 +1233,7 @@ let abs_wgen keep_let f gen (gl,args,c) = let evar_closed t p = if occur_existential sigma t then CErrors.user_err ?loc:(loc_of_cpattern p) ~hdr:"ssreflect" - (pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++ + (pr_econstr_pat env sigma t ++ str" contains holes and matches no subterm of the goal") in match gen with | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 3fc05437da..350bb9019e 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -239,8 +239,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let elimty = Reductionops.whd_all env (project gl) elimty in seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl in - ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elim))); - ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elimty))); + let () = + let sigma = project gl in + ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); + ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) | _ -> assert false in @@ -255,38 +257,56 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = (* 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 + 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 = pfe_type_of gl arg in - match saturate_until gl c c_ty (fun c c_ty gl -> - pf_unify_HO (pf_unify_HO gl c_ty arg_ty) arg c) with - | Some (c, _, _, gl) -> Some (false, gl) - | None -> None in - 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 = pfe_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 Pp.(str"Unable to apply the eliminator to the term"++ - spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++ - pr_econstr_env env (project gl) inf_arg_ty) in + let rec first = function + | [] -> + errorstrm Pp.(str"Unable to apply the eliminator to the term"++ + spc()++pr_econstr_env env (project gl) c++spc()) + | x :: rest -> + match x () with + | None -> first rest + | Some (b,gl) -> b, gl + in + (* Unify two terms if their heads are not applied unif variables, eg + * not (?P x). The idea is to rule out cases where the problem is too + * vague to drive the current heuristics. *) + let pf_unify_HO_rigid gl a b = + let is_applied_evar x = match EConstr.kind (project gl) x with + | App(x,_) -> EConstr.isEvar (project gl) x + | _ -> false in + if is_applied_evar a || is_applied_evar b then + raise Evarconv.(UnableToUnify(project gl, + Pretype_errors.ProblemBeyondCapabilities)) + else pf_unify_HO gl a b in + let try_c_last_arg () = + (* 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 = pfe_type_of gl arg in + match saturate_until gl c c_ty (fun c c_ty gl -> + pf_unify_HO (pf_unify_HO_rigid gl c_ty arg_ty) arg c) with + | Some (c, _, _, gl) -> Some (false, gl) + | None -> None in + let try_c_last_pattern () = + (* we try to see if c unifies with the last inferred pattern *) + if inf_deps_r = [] then None else + let inf_arg = List.hd inf_deps_r in + let gl, inf_arg_ty = pfe_type_of gl inf_arg in + match saturate_until gl c c_ty (fun _ c_ty gl -> + pf_unify_HO_rigid gl c_ty inf_arg_ty) with + | Some (c, _, _,gl) -> Some(true, gl) + | None -> None in + first [try_c_last_arg;try_c_last_pattern] in ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pfe_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,_,occ) = Pp.(pr_occ occ ++ pp_pattern env p) in - let pp_inf_pat gl (_,_,t,_) = pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl t)) in + let pp_inf_pat gl (_,_,t,_) = pr_econstr_pat env (project gl) (fire_subst gl t) in let patterns, clr, gl = let rec loop patterns clr i = function | [],[] -> patterns, clr, gl @@ -300,7 +320,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> - ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr c))); + ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in @@ -323,7 +343,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let elim_pred, gen_eq_tac, clr, gl = let error gl t inf_t = errorstrm Pp.(str"The given pattern matches the term"++ spc()++pp_term gl t++spc()++str"while the inferred pattern"++ - spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in + spc()++pr_econstr_pat env (project gl) (fire_subst gl inf_t)++spc()++ str"doesn't") in let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) = let p = unif_redex gl p inf_t in if is_undef_pat p then @@ -408,7 +428,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = if not (Evar.Set.is_empty inter) then begin let i = Evar.Set.choose inter in let pat = List.find (fun t -> Evar.Set.mem i (evars_of_term t)) patterns in - errorstrm Pp.(str"Pattern"++spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr pat)++spc()++ + errorstrm Pp.(str"Pattern"++spc()++pr_econstr_pat env (project gl) pat++spc()++ str"was not completely instantiated and one of its variables"++spc()++ str"occurs in the type of another non-instantiated pattern variable"); end diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 15480c7a45..5abbc214de 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -205,7 +205,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with | App (c', _) -> get_evalref env sigma c' | Cast (c', _, _) -> get_evalref env sigma c' | Proj(c,_) -> EvalConstRef(Projection.constant c) - | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable") + | _ -> errorstrm Pp.(str "The term " ++ pr_econstr_pat (Global.env ()) sigma c ++ str " is not unfoldable") (* Strip a pattern generated by a prenex implicit to its constant. *) let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with @@ -244,7 +244,7 @@ let unfoldintac occ rdx t (kt,_) gl = try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c))) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of " - ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), + ++ pr_econstr_pat env sigma0 t ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), (fun () -> try end_T () with | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") @@ -270,12 +270,12 @@ let unfoldintac occ rdx t (kt,_) gl = else try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t) with _ -> errorstrm Pp.(str "The term " ++ - pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t))), + pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_econstr_pat env sigma t)), fake_pmatcher_end in let concl = let concl0 = EConstr.Unsafe.to_constr concl0 in try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) - with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat env0 sigma (EConstr.Unsafe.to_constr t)) in + with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in let _ = conclude () in Proofview.V82.of_tactic (convert_concl concl) gl ;; @@ -325,7 +325,7 @@ let rec strip_prod_assum c = match Constr.kind c with let rule_id = mk_internal_id "rewrite rule" -exception PRtype_error +exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (* ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *) @@ -351,7 +351,10 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in (* We check the proof is well typed *) let sigma, proof_ty = - try Typing.type_of env sigma proof with _ -> raise PRtype_error in + try Typing.type_of env sigma proof with + | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te))) + | e when CErrors.noncritical e -> raise (PRtype_error None) + in ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl @@ -412,7 +415,7 @@ let rwcltac cl rdx dir sr gl = let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = try EConstr.destCast (project gl) r2 with _ -> - errorstrm Pp.(str "no cast from " ++ pr_constr_pat (pf_env gl) (project gl) (EConstr.Unsafe.to_constr (snd sr)) + errorstrm Pp.(str "no cast from " ++ pr_econstr_pat (pf_env gl) (project gl) (snd sr) ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in @@ -423,13 +426,16 @@ let rwcltac cl rdx dir sr gl = in let cvtac' _ = try cvtac gl with - | PRtype_error -> + | PRtype_error e -> + let error = Option.cata (fun (env, sigma, te) -> + Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te)) + (Pp.mt ()) e in if occur_existential (project gl) (Tacmach.pf_concl gl) - then errorstrm Pp.(str "Rewriting impacts evars") + then errorstrm Pp.(str "Rewriting impacts evars" ++ error) else errorstrm Pp.(str "Dependent type error in rewrite of " - ++ pr_constr_env (pf_env gl) (project gl) - (Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant) - (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))) + ++ pr_econstr_env (pf_env gl) (project gl) + (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl) + ++ error) in tclTHEN cvtac' rwtac gl @@ -473,7 +479,7 @@ let rwprocess_rule dir rule gl = let t = if red = 1 then Tacred.hnf_constr env sigma t0 else Reductionops.whd_betaiotazeta sigma t0 in - ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat env sigma (EConstr.Unsafe.to_constr t))); + ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t)); match EConstr.kind sigma t with | Prod (_, xt, at) -> let sigma = Evd.create_evar_defs sigma in @@ -532,8 +538,8 @@ let rwprocess_rule dir rule gl = sigma, (d, r', lhs, rhs) :: rs | _ -> if red = 0 then loop d sigma r t rs 1 - else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) - ++ spc() ++ str "in rule " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr (snd rule))) + else errorstrm Pp.(str "not a rewritable relation: " ++ pr_econstr_pat env sigma t + ++ spc() ++ str "in rule " ++ pr_econstr_pat env sigma (snd rule)) in let sigma, r = rule in let t = Retyping.get_type_of env sigma r in @@ -547,9 +553,9 @@ let rwrxtac occ rdx_pat dir rule gl = let find_rule rdx = let rec rwtac = function | [] -> - errorstrm Pp.(str "pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr rdx) ++ + errorstrm Pp.(str "pattern " ++ pr_econstr_pat env (project gl) rdx ++ str " does not match " ++ pr_dir_side dir ++ - str " of " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (snd rule))) + str " of " ++ pr_econstr_pat env (project gl) (snd rule)) | (d, r, lhs, rhs) :: rs -> try let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index be9586fdd7..3cadc92bcc 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -50,7 +50,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = 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 env sigma (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++ + pr_econstr_pat env sigma 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) diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index e9fe1f3e48..3481b25c8b 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -369,18 +369,20 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl -> end end (*** [=> [: id]] ************************************************************) -[@@@ocaml.warning "-3"] let mk_abstract_id = let open Coqlib in let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in -begin fun () -> +begin fun env sigma -> + let sigma, zero = EConstr.fresh_global env sigma (lib_ref "num.nat.O") in + let sigma, succ = EConstr.fresh_global env sigma (lib_ref "num.nat.S") in let rec nat_of_n n = - if n = 0 then EConstr.mkConstruct path_of_O - else EConstr.mkApp (EConstr.mkConstruct path_of_S, [|nat_of_n (n-1)|]) in - incr ssr_abstract_id; nat_of_n !ssr_abstract_id + if n = 0 then zero + else EConstr.mkApp (succ, [|nat_of_n (n-1)|]) in + incr ssr_abstract_id; + sigma, nat_of_n !ssr_abstract_id end -let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl -> +let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl -> let env, concl = Goal.(env gl, concl gl) in let step = begin fun sigma -> let (sigma, (abstract_proof, abstract_ty)) = @@ -389,8 +391,8 @@ let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl -> let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in let (sigma, lock) = Evarutil.new_evar env sigma ablock in let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in - let abstract_ty = - EConstr.mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in + let (sigma, abstract_id) = mk_abstract_id env sigma in + let abstract_ty = EConstr.mkApp(abstract, [|ty; abstract_id; lock|]) in let sigma, m = Evarutil.new_evar env sigma abstract_ty in sigma, (m, abstract_ty) in let sigma, kont = @@ -409,7 +411,7 @@ end let tclMK_ABSTRACT_VARS ids = List.fold_right (fun id tac -> - Tacticals.New.tclTHENFIRST (tcltclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ()) + Tacticals.New.tclTHENFIRST (tclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ()) (* Debugging *) let tclLOG p t = diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index d3f89147fa..0a0d9b12fa 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -566,17 +566,21 @@ let print_view_hints env sigma kind l = } VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY -| [ "Print" "Hint" "View" ssrviewpos(i) ] -> +| ![proof] [ "Print" "Hint" "View" ssrviewpos(i) ] -> { - let sigma, env = Pfedit.get_current_context () in - match i with + fun ~pstate -> + (* XXX this is incorrect *) + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + (match i with | Some k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k) | None -> List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k)) [ Ssrview.AdaptorDb.Forward; Ssrview.AdaptorDb.Backward; - Ssrview.AdaptorDb.Equivalence ] + Ssrview.AdaptorDb.Equivalence ]); + pstate } END |