Merge PR #12579: Simplify Clenv API

Reviewed-by: ejgallego

5 files changed, 129 insertions, 180 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 87b4255b88..7fb3a21813 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -28,6 +28,7 @@ open Pretype_errors
 open Evarutil
 open Unification
 open Tactypes
+open Logic
 
 (******************************************************************)
 (* Clausal environments *)
@@ -41,7 +42,6 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let clenv_nf_meta clenv c = nf_meta clenv.env clenv.evd c
 let clenv_term clenv c = meta_instance clenv.env clenv.evd c
 let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv
 let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval
@@ -376,21 +376,21 @@ let adjust_meta_source evd mv = function
 *)
 
 let clenv_pose_metas_as_evars clenv dep_mvs =
-  let rec fold clenv evs = function
-  | [] -> clenv, evs
+  let rec fold clenv = function
+  | [] -> clenv
   | mv::mvs ->
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv])
+      if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
         let evd = clenv.evd in
         let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
         let clenv = clenv_assign mv evar {clenv with evd=evd} in
-        fold clenv (fst (destEvar evd evar) :: evs) mvs in
-  fold clenv [] dep_mvs
+        fold clenv mvs in
+  fold clenv dep_mvs
 
 (******************************************************************)
 
@@ -444,8 +444,6 @@ let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv =
 (***************************************************************)
 (* Bindings *)
 
-type arg_bindings = constr explicit_bindings
-
 (* [clenv_independent clenv]
  * returns a list of metavariables which appear in the term cval,
  * and which are not dependent.  That is, they do not appear in
@@ -598,6 +596,121 @@ let clenv_constrain_dep_args hyps_only bl clenv =
       else
         error_not_right_number_missing_arguments (List.length occlist)
 
+
+(* This function put casts around metavariables whose type could not be
+ * inferred by the refiner, that is head of applications, predicates and
+ * subject of Cases.
+ * Does check that the casted type is closed. Anyway, the refiner would
+ * fail in this case... *)
+
+let clenv_cast_meta clenv =
+  let rec crec u =
+    match EConstr.kind clenv.evd u with
+      | App _ | Case _ -> crec_hd u
+      | Cast (c,_,_) when isMeta clenv.evd c -> u
+      | Proj (p, c) -> mkProj (p, crec_hd c)
+      | _  -> EConstr.map clenv.evd crec u
+
+  and crec_hd u =
+    match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with
+      | Meta mv ->
+          (try
+            let b = Typing.meta_type clenv.env clenv.evd mv in
+            assert (not (occur_meta clenv.evd b));
+            if occur_meta clenv.evd b then u
+            else mkCast (mkMeta mv, DEFAULTcast, b)
+          with Not_found -> u)
+      | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
+      | Case(ci,p,c,br) ->
+          mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+      | Proj (p, c) -> mkProj (p, crec_hd c)
+      | _ -> u
+  in
+  crec
+
+let clenv_value_cast_meta clenv =
+    clenv_cast_meta clenv (clenv_value clenv)
+
+let clenv_pose_dependent_evars ?(with_evars=false) clenv =
+  let dep_mvs = clenv_dependent clenv in
+  let env, sigma = clenv.env, clenv.evd in
+  if not (List.is_empty dep_mvs) && not with_evars then
+    raise
+      (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
+  clenv_pose_metas_as_evars clenv dep_mvs
+
+let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
+  Proofview.Goal.enter begin fun gl ->
+  let clenv = clenv_pose_dependent_evars ~with_evars clenv in
+  let evd' =
+    if with_classes then
+      let evd' =
+        Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
+          ~fail:(not with_evars) clenv.env clenv.evd
+      in
+      (* After an apply, all the subgoals including those dependent shelved ones are in
+         the hands of the user and resolution won't be called implicitely on them. *)
+      Typeclasses.make_unresolvables (fun x -> true) evd'
+    else clenv.evd
+  in
+  let clenv = { clenv with evd = evd' } in
+  Proofview.tclTHEN
+    (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
+    (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
+  end
+
+open Unification
+
+let dft = default_unify_flags
+
+let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv =
+  Proofview.Goal.enter begin fun gl ->
+    let clenv = clenv_unique_resolver ~flags clenv gl in
+    clenv_refine ?with_evars ~with_classes clenv
+  end
+
+(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
+   particulier ne semblent pas vérifier que des instances différentes
+   d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
+   provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
+
+let fail_quick_core_unif_flags = {
+  modulo_conv_on_closed_terms = Some TransparentState.full;
+  use_metas_eagerly_in_conv_on_closed_terms = false;
+  use_evars_eagerly_in_conv_on_closed_terms = false;
+  modulo_delta = TransparentState.empty;
+  modulo_delta_types = TransparentState.full;
+  check_applied_meta_types = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = true; (* ? *)
+  allowed_evars = AllowAll;
+  restrict_conv_on_strict_subterms = false; (* ? *)
+  modulo_betaiota = false;
+  modulo_eta = true;
+}
+
+let fail_quick_unif_flags = {
+  core_unify_flags = fail_quick_core_unif_flags;
+  merge_unify_flags = fail_quick_core_unif_flags;
+  subterm_unify_flags = fail_quick_core_unif_flags;
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = false
+}
+
+(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
+let unify ?(flags=fail_quick_unif_flags) m =
+  Proofview.Goal.enter begin fun gl ->
+    let env = Tacmach.New.pf_env gl in
+    let n = Tacmach.New.pf_concl gl in
+    let evd = clear_metas (Tacmach.New.project gl) in
+    try
+      let evd' = w_unify env evd CONV ~flags m n in
+        Proofview.Unsafe.tclEVARSADVANCE evd'
+    with e when CErrors.noncritical e ->
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info e
+  end
+
 (****************************************************************)
 (* Clausal environment for an application *)
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 4279ab4768..fd1e2fe593 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -37,9 +37,6 @@ val clenv_value     : clausenv -> constr
 (** type of clenv (instantiated) *)
 val clenv_type      : clausenv -> types
 
-(** substitute resolved metas *)
-val clenv_nf_meta   : clausenv -> EConstr.constr -> EConstr.constr
-
 (** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
@@ -62,18 +59,8 @@ val clenv_fchain :
 val clenv_unify :
   ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
-(** unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
-  ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv
-
-val clenv_dependent : clausenv -> metavariable list
-
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list
-
 (** {6 Bindings } *)
 
-type arg_bindings = constr explicit_bindings
-
 (** bindings where the key is the position in the template of the
    clenv (dependent or not). Positions can be negative meaning to
    start from the rightmost argument of the template. *)
@@ -109,6 +96,14 @@ val make_clenv_binding :
 exception NotExtensibleClause
 val clenv_push_prod : clausenv -> clausenv
 
+(** {6 Clenv tactics} *)
+
+val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
+val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
+
+val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
+val clenv_value_cast_meta : clausenv -> constr
+
 (** {6 Pretty-print (debug only) } *)
 val pr_clenv : clausenv -> Pp.t
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
deleted file mode 100644
index 007d53f911..0000000000
--- a/proofs/clenvtac.ml
+++ /dev/null
@@ -1,135 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Constr
-open Termops
-open Evd
-open EConstr
-open Logic
-open Reduction
-open Clenv
-
-(* This function put casts around metavariables whose type could not be
- * inferred by the refiner, that is head of applications, predicates and
- * subject of Cases.
- * Does check that the casted type is closed. Anyway, the refiner would
- * fail in this case... *)
-
-let clenv_cast_meta clenv =
-  let rec crec u =
-    match EConstr.kind clenv.evd u with
-      | App _ | Case _ -> crec_hd u
-      | Cast (c,_,_) when isMeta clenv.evd c -> u
-      | Proj (p, c) -> mkProj (p, crec_hd c)
-      | _  -> EConstr.map clenv.evd crec u
-
-  and crec_hd u =
-    match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with
-      | Meta mv ->
-          (try
-            let b = Typing.meta_type clenv.env clenv.evd mv in
-            assert (not (occur_meta clenv.evd b));
-            if occur_meta clenv.evd b then u
-            else mkCast (mkMeta mv, DEFAULTcast, b)
-          with Not_found -> u)
-      | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
-      | Case(ci,p,c,br) ->
-          mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
-      | Proj (p, c) -> mkProj (p, crec_hd c)
-      | _ -> u
-  in
-  crec
-
-let clenv_value_cast_meta clenv =
-    clenv_cast_meta clenv (clenv_value clenv)
-
-let clenv_pose_dependent_evars ?(with_evars=false) clenv =
-  let dep_mvs = clenv_dependent clenv in
-  let env, sigma = clenv.env, clenv.evd in
-  if not (List.is_empty dep_mvs) && not with_evars then
-    raise
-      (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
-  clenv_pose_metas_as_evars clenv dep_mvs
-
-let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
-  Proofview.Goal.enter begin fun gl ->
-  let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
-  let evd' =
-    if with_classes then
-      let evd' =
-        Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
-          ~fail:(not with_evars) clenv.env clenv.evd
-      in
-      (* After an apply, all the subgoals including those dependent shelved ones are in
-         the hands of the user and resolution won't be called implicitely on them. *)
-      Typeclasses.make_unresolvables (fun x -> true) evd'
-    else clenv.evd
-  in
-  let clenv = { clenv with evd = evd' } in
-  Proofview.tclTHEN
-    (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
-    (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
-  end
-
-let clenv_pose_dependent_evars ?(with_evars=false) clenv =
-  fst (clenv_pose_dependent_evars ~with_evars clenv)
-
-open Unification
-
-let dft = default_unify_flags
-
-let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv =
-  Proofview.Goal.enter begin fun gl ->
-    let clenv = clenv_unique_resolver ~flags clenv gl in
-    clenv_refine ?with_evars ~with_classes clenv
-  end
-
-(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
-   particulier ne semblent pas vérifier que des instances différentes
-   d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
-   provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
-
-let fail_quick_core_unif_flags = {
-  modulo_conv_on_closed_terms = Some TransparentState.full;
-  use_metas_eagerly_in_conv_on_closed_terms = false;
-  use_evars_eagerly_in_conv_on_closed_terms = false;
-  modulo_delta = TransparentState.empty;
-  modulo_delta_types = TransparentState.full;
-  check_applied_meta_types = false;
-  use_pattern_unification = false;
-  use_meta_bound_pattern_unification = true; (* ? *)
-  allowed_evars = AllowAll;
-  restrict_conv_on_strict_subterms = false; (* ? *)
-  modulo_betaiota = false;
-  modulo_eta = true;
-}
-
-let fail_quick_unif_flags = {
-  core_unify_flags = fail_quick_core_unif_flags;
-  merge_unify_flags = fail_quick_core_unif_flags;
-  subterm_unify_flags = fail_quick_core_unif_flags;
-  allow_K_in_toplevel_higher_order_unification = false;
-  resolve_evars = false
-}
-
-(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unify ?(flags=fail_quick_unif_flags) m =
-  Proofview.Goal.enter begin fun gl ->
-    let env = Tacmach.New.pf_env gl in
-    let n = Tacmach.New.pf_concl gl in
-    let evd = clear_metas (Tacmach.New.project gl) in
-    try
-      let evd' = w_unify env evd CONV ~flags m n in
-        Proofview.Unsafe.tclEVARSADVANCE evd'
-    with e when CErrors.noncritical e ->
-      let info = Exninfo.reify () in
-      Proofview.tclZERO ~info e
-  end
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
deleted file mode 100644
index 6eafca359b..0000000000
--- a/proofs/clenvtac.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Legacy components of the previous proof engine. *)
-
-open Clenv
-open EConstr
-open Unification
-
-(** Tactics *)
-val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
-val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
-val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
-
-val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
-val clenv_value_cast_meta : clausenv -> constr
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 756fef0511..790a9dd2cc 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -9,4 +9,3 @@ Proof_bullet
 Refiner
 Tacmach
 Clenv
-Clenvtac