Merge PR #6338: Remove up-to-conversion term matching

9 files changed, 26 insertions, 70 deletions

diff --git a/API/API.mli b/API/API.mli
index c61dc4d90..93899d21c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4970,8 +4970,6 @@ sig
 
   val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
 
-  val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool
-
   val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list
 
   val pr_gls    : Goal.goal Evd.sigma -> Pp.t
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b0a76137b..766adfc63 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -141,7 +141,7 @@ let def_id = Id.of_string "def"
 let p_id = Id.of_string "p"
 let rec_res_id = Id.of_string "rec_res";;
 let lt = function () -> (coq_init_constant "lt")
-let le = function () -> (coq_init_constant "le")
+let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le")
 let ex = function () -> (coq_init_constant "ex")
 let nat = function () -> (coq_init_constant "nat")
 let iter_ref () =  
@@ -857,9 +857,13 @@ let rec prove_le g =
     Proofview.V82.of_tactic (apply (delayed_force le_n));
     begin
       try
-	let matching_fun = 
-	  pf_is_matching g
-	    (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in
+        let matching_fun c = match EConstr.kind sigma c with
+        | App (c, [| x0 ; _ |]) ->
+          EConstr.isVar sigma x0 &&
+          Id.equal (destVar sigma x0) (destVar sigma x) &&
+          is_global sigma (le ()) c
+        | _ -> false
+        in
 	let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
 	in 
 	let y = 
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 20ef65c88..478ba73fd 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Globnames
 open Termops
-open Reductionops
 open Term
 open EConstr
 open Vars
@@ -207,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst =
   in
   constrain sigma n c subst
       
-let matches_core env sigma convert allow_partial_app allow_bound_rels
+let matches_core env sigma allow_partial_app allow_bound_rels
     (binding_vars,pat) c =
   let open EConstr in
   let convref ref c = 
@@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
     | ConstRef c, Const (c',_) -> Constant.equal c c'
     | IndRef i, Ind (i', _) -> Names.eq_ind i i'
     | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
-    | _, _ -> 
-      (if convert then 
-	  let sigma,c' = Evd.fresh_global env sigma ref in
-	    is_conv env sigma (EConstr.of_constr c') c
-       else false)
+    | _, _ -> false
   in
   let rec sorec ctx env subst p t =
     let cT = strip_outer_cast sigma t in
@@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
   in
   sorec [] env (Id.Map.empty, Id.Map.empty) pat c
 
-let matches_core_closed env sigma convert allow_partial_app pat c =
-  let names, subst = matches_core env sigma convert allow_partial_app false pat c in
+let matches_core_closed env sigma allow_partial_app pat c =
+  let names, subst = matches_core env sigma allow_partial_app false pat c in
   (names, Id.Map.map snd subst)
 
-let extended_matches env sigma = matches_core env sigma false true true
+let extended_matches env sigma = matches_core env sigma true true
 
 let matches env sigma pat c =
-  snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c)
+  snd (matches_core_closed env sigma true (Id.Set.empty,pat) c)
 
 let special_meta = (-1)
 
@@ -412,7 +407,7 @@ let matches_head env sigma pat c =
 (* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ env sigma partial_app closed pat c mk_ctx =
   try
-    let subst = matches_core_closed env sigma false partial_app pat c in
+    let subst = matches_core_closed env sigma partial_app pat c in
     if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
     then (fun next -> next ())
     else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
@@ -552,10 +547,3 @@ let is_matching_appsubterm ?(closed=true) env sigma pat c =
   let pat = (Id.Set.empty,pat) in
   let results = sub_match ~partial_app:true ~closed env sigma pat c in
   not (IStream.is_empty results)
-
-let matches_conv env sigma p c =
-  snd (matches_core_closed env sigma true false (Id.Set.empty,p) c)
-
-let is_matching_conv env sigma pat n =
-  try let _ = matches_conv env sigma pat n in true
-  with PatternMatchingFailure -> false
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 780ccc23d..60e1c34a1 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -55,12 +55,6 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool
     prefix of it matches against [pat] *)
 val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool
 
-(** [matches_conv env sigma] matches up to conversion in environment
-   [(env,sigma)] when constants in pattern are concerned; it raises
-   [PatternMatchingFailure] if not matchable; bindings are given in
-   increasing order based on the numbers given in the pattern *)
-val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
-
 (** The type of subterm matching results: a substitution + a context
    (whose hole is denoted here with [special_meta]) *)
 type matching_result =
@@ -85,8 +79,3 @@ val match_subterm_gen : env -> Evd.evar_map ->
 (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
    against [pat] taking partial subterms into consideration *)
 val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool
-
-(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
-   up to conversion for constants in patterns *)
-val is_matching_conv :
-  env -> Evd.evar_map -> constr_pattern -> constr -> bool
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a8ec4d8ca..cab8d7b52 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -102,9 +102,6 @@ let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
-let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p c
-let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p c
-
 (********************************************)
 (* Definition of the most primitive tactics *)
 (********************************************)
@@ -223,8 +220,6 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl t)
 
-  let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
-
   let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d9496d2b4..e0fb8fbc5 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -12,9 +12,7 @@ open Environ
 open EConstr
 open Proof_type
 open Redexpr
-open Pattern
 open Locus
-open Ltac_pretype
 
 (** Operations for handling terms under a local typing context. *)
 
@@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
-
-
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
@@ -138,8 +132,6 @@ module New : sig
   val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr
   val pf_compute : 'a Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
-
   val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
 
 end
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 8e851375a..2c8ca1972 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -39,7 +39,6 @@ type testing_function  = Evd.evar_map -> EConstr.constr -> bool
 let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
-let meta3 = mkmeta 3
 
 let op2bool = function Some _ -> true | None -> false
 
@@ -460,22 +459,6 @@ let find_this_eq_data_decompose gl eqn =
       user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in
   (lbeq,u,eq_args)
 
-let match_eq_nf gls eqn (ref, hetero) =
-  let n = if hetero then 4 else 3 in
-  let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in
-  let pat = mkPattern (mkGAppRef ref args) in
-  match Id.Map.bindings (pf_matches gls pat eqn) with
-    | [(m1,t);(m2,x);(m3,y)] ->
-        assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-	(t,pf_whd_all gls x,pf_whd_all gls y)
-    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.")
-
-let dest_nf_eq gls eqn =
-  try
-    snd (first_match (match_eq_nf gls eqn) equalities)
-  with PatternMatchingFailure ->
-    user_err Pp.(str "Not an equality.")
-
 (*** Sigma-types *)
 
 let match_sigma env sigma ex =
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 8ff6fe95c..237ed42d5 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -144,9 +144,6 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool
    [t,u,T] and a boolean telling if equality is on the left side *)
 val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
 
-(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr)
-
 (** Match a negation *)
 val is_matching_not : Environ.env -> evar_map -> constr -> bool
 val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 46b10bf33..cb0bbfd0e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -334,6 +334,16 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
    If it can discriminate then the goal is proved, if not tries to use it as
    a rewrite rule. It erases the clause which is given as input *)
 
+let dest_nf_eq env sigma t = match EConstr.kind sigma t with
+| App (r, [| t; x; y |]) ->
+  let open Reductionops in
+  let lazy eq = Coqlib.coq_eq_ref in
+  if EConstr.is_global sigma eq r then
+    (t, whd_all env sigma x, whd_all env sigma y)
+  else user_err Pp.(str "Not an equality.")
+| _ ->
+  user_err Pp.(str "Not an equality.")
+
 let projectAndApply as_mode thin avoid id eqname names depids =
   let subst_hyp l2r id =
     tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id)))
@@ -344,7 +354,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
     let sigma = project gl in
     (** We only look at the type of hypothesis "id" *)
     let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
-    let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
+    let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in
     match (EConstr.kind sigma t1, EConstr.kind sigma t2) with
     | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
     | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2