Merge Clenvtac into Clenv.

Having two different modules led to the availability of internal API in
the mli.

1 files changed, 119 insertions, 0 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 87b4255b88..4f19f943a8 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 *)
@@ -598,6 +599,124 @@ 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, 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
+
 (****************************************************************)
 (* Clausal environment for an application *)