Merge PR #12579: Simplify Clenv API

Reviewed-by: ejgallego

1 files changed, 121 insertions, 8 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 *)