diff options
| -rw-r--r-- | tactics/autorewrite.ml | 69 | ||||
| -rw-r--r-- | tactics/autorewrite.mli | 19 |
2 files changed, 23 insertions, 65 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index eaefa2947a..cc56de066d 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -212,60 +212,37 @@ let inHintRewrite : string * HintDN.t -> Libobject.obj = ~cache:cache_hintrewrite ~subst:(Some subst_hintrewrite) -open Clenv - type hypinfo = { - hyp_cl : clausenv; - hyp_prf : constr; - hyp_ty : types; - hyp_car : constr; - hyp_rel : constr; - hyp_l2r : bool; - hyp_left : constr; - hyp_right : constr; + hyp_ty : EConstr.types; + hyp_pat : EConstr.constr; } -let decompose_applied_relation metas env sigma c ctype left2right = +let decompose_applied_relation env sigma c ctype left2right = let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in - let eqclause = - if metas then eqclause - else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)) - in - let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in - let rec split_last_two = function - | [c1;c2] -> [],(c1, c2) - | x::y::z -> - let l,res = split_last_two (y::z) in x::l, res - | _ -> raise Not_found - in - try - let others,(c1,c2) = split_last_two args in - let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in - (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) - let open EConstr in - let hyp_ty = Unsafe.to_constr ty in - let hyp_car = Unsafe.to_constr ty1 in - let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in - let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in - let hyp_left = Unsafe.to_constr @@ c1 in - let hyp_right = Unsafe.to_constr @@ c2 in -(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) -(* else *) - Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; } - with Not_found -> None + (* FIXME: this is nonsense, we generate evars and then we drop the + corresponding evarmap. This sometimes works because [Term_dnet] performs + evar surgery via [Termops.filtering]. *) + let sigma, ty = Clenv.make_evar_clause env sigma ty in + let (_, args) = Termops.decompose_app_vect sigma ty.Clenv.cl_concl in + let len = Array.length args in + if 2 <= len then + let c1 = args.(len - 2) in + let c2 = args.(len - 1) in + Some (if left2right then c1 else c2) + else None in match find_rel ctype with - | Some c -> Some c + | Some c -> Some { hyp_pat = c; hyp_ty = ctype } | None -> let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' ctx) with - | Some c -> Some c + let ctype = it_mkProd_or_LetIn t' ctx in + match find_rel ctype with + | Some c -> Some { hyp_pat = c; hyp_ty = ctype } | None -> None -let find_applied_relation ?loc metas env sigma c left2right = +let find_applied_relation ?loc env sigma c left2right = let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in - match decompose_applied_relation metas env sigma c ctype left2right with + match decompose_applied_relation env sigma c ctype left2right with | Some c -> c | None -> user_err ?loc ~hdr:"decompose_applied_relation" @@ -283,9 +260,9 @@ let add_rew_rules base lrul = List.fold_left (fun dn {CAst.loc;v=((c,ctx),b,t)} -> let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in - let info = find_applied_relation ?loc false env sigma c b in - let pat = if b then info.hyp_left else info.hyp_right in - let rul = { rew_lemma = c; rew_type = info.hyp_ty; + let info = find_applied_relation ?loc env sigma c b in + let pat = EConstr.Unsafe.to_constr info.hyp_pat in + let rul = { rew_lemma = c; rew_type = EConstr.Unsafe.to_constr info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; rew_tac = Option.map intern t} in incr counter; diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 8f7a1c8fcf..974aef8e8f 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -43,22 +43,3 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic val print_rewrite_hintdb : string -> Pp.t - -open Clenv - - -type hypinfo = { - hyp_cl : clausenv; - hyp_prf : constr; - hyp_ty : types; - hyp_car : constr; - hyp_rel : constr; - hyp_l2r : bool; - hyp_left : constr; - hyp_right : constr; -} - -val find_applied_relation : - ?loc:Loc.t -> bool -> - Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo - |