From 47eb0278a3cdf93129b1742e314681d65bd6475a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Aug 2017 14:11:48 +0200
Subject: More bindings to primitive tactics.

---
 src/tac2stdlib.ml   | 26 ++++++++++++++++++++++++++
 src/tac2tactics.ml  | 49 ++++++++++++++++++++++++++++++++++++++++++++++++-
 src/tac2tactics.mli | 10 +++++++++-
 3 files changed, 83 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index eccaf95ab3..d88402cbf2 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -481,10 +481,36 @@ end
 
 (** Tactics from extratactics *)
 
+let () = define_prim2 "tac_discriminate" begin fun ev arg ->
+  let ev = Value.to_bool ev in
+  let arg = Value.to_option (fun arg -> None, to_destruction_arg arg) arg in
+  Tac2tactics.discriminate ev arg
+end
+
+let () = define_prim3 "tac_injection" begin fun ev ipat arg ->
+  let ev = Value.to_bool ev in
+  let ipat = Value.to_option to_intro_patterns ipat in
+  let arg = Value.to_option (fun arg -> None, to_destruction_arg arg) arg in
+  Tac2tactics.injection ev ipat arg
+end
+
 let () = define_prim1 "tac_absurd" begin fun c ->
   Contradiction.absurd (Value.to_constr c)
 end
 
+let () = define_prim1 "tac_contradiction" begin fun c ->
+  let c = Value.to_option to_constr_with_bindings c in
+  Contradiction.contradiction c
+end
+
+let () = define_prim4 "tac_autorewrite" begin fun all by ids cl ->
+  let all = Value.to_bool all in
+  let by = Value.to_option (fun tac -> Proofview.tclIGNORE (thaw tac)) by in
+  let ids = Value.to_list Value.to_ident ids in
+  let cl = to_clause cl in
+  Tac2tactics.autorewrite ~all by ids cl
+end
+
 let () = define_prim1 "tac_subst" begin fun ids ->
   let ids = Value.to_list Value.to_ident ids in
   Equality.subst ids
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 2f4965783f..25a00fdc2e 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -16,6 +16,15 @@ open Genredexpr
 open Proofview
 open Proofview.Notations
 
+type destruction_arg = EConstr.constr with_bindings tactic Misctypes.destruction_arg
+
+let tactic_infer_flags with_evar = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.solve_unification_constraints = true;
+  Pretyping.use_hook = None;
+  Pretyping.fail_evar = not with_evar;
+  Pretyping.expand_evars = true }
+
 (** FIXME: export a better interface in Tactics *)
 let delayed_of_tactic tac env sigma =
   let _, pv = Proofview.init sigma [] in
@@ -30,7 +39,7 @@ let apply adv ev cb cl =
   | Some (id, cl) -> Tactics.apply_delayed_in adv ev id cb cl
 
 type induction_clause =
-  EConstr.constr with_bindings tactic destruction_arg *
+  destruction_arg *
   intro_pattern_naming option *
   or_and_intro_pattern option *
   Locus.clause option
@@ -112,3 +121,41 @@ let vm where cl =
 let native where cl =
   let where = Option.map map_pattern_with_occs where in
   Tactics.reduce (CbvNative where) cl
+
+let on_destruction_arg tac ev arg =
+  Proofview.Goal.enter begin fun gl ->
+  match arg with
+  | None -> tac ev None
+  | Some (clear, arg) ->
+    let arg = match arg with
+    | ElimOnConstr c ->
+      let env = Proofview.Goal.env gl in
+      Proofview.tclEVARMAP >>= fun sigma ->
+      c >>= fun (c, lbind) ->
+      Proofview.tclEVARMAP >>= fun sigma' ->
+      let flags = tactic_infer_flags ev in
+      let (sigma', c) = Unification.finish_evar_resolution ~flags env sigma' (sigma, c) in
+      Proofview.tclUNIT (Some sigma', ElimOnConstr (c, lbind))
+    | ElimOnIdent id -> Proofview.tclUNIT (None, ElimOnIdent id)
+    | ElimOnAnonHyp n -> Proofview.tclUNIT (None, ElimOnAnonHyp n)
+    in
+    arg >>= fun (sigma', arg) ->
+    let arg = Some (clear, arg) in
+    match sigma' with
+    | None -> tac ev arg
+    | Some sigma' ->
+      Tacticals.New.tclWITHHOLES ev (tac ev arg) sigma'
+  end
+
+let discriminate ev arg = on_destruction_arg Equality.discr_tac ev arg
+
+let injection ev ipat arg =
+  let tac ev arg = Equality.injClause ipat ev arg in
+  on_destruction_arg tac ev arg
+
+let autorewrite ~all by ids cl =
+  let conds = if all then Some Equality.AllMatches else None in
+  let ids = List.map Id.to_string ids in
+  match by with
+  | None -> Autorewrite.auto_multi_rewrite ?conds ids cl
+  | Some by -> Autorewrite.auto_multi_rewrite_with ?conds by ids cl
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index d835f768a1..8939d2a9dd 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -14,6 +14,8 @@ open Misctypes
 open Tactypes
 open Proofview
 
+type destruction_arg = EConstr.constr with_bindings tactic Misctypes.destruction_arg
+
 (** Local reimplementations of tactics variants from Coq *)
 
 val apply : advanced_flag -> evars_flag ->
@@ -21,7 +23,7 @@ val apply : advanced_flag -> evars_flag ->
   (Id.t * intro_pattern option) option -> unit tactic
 
 type induction_clause =
-  EConstr.constr with_bindings tactic destruction_arg *
+  destruction_arg *
   intro_pattern_naming option *
   or_and_intro_pattern option *
   clause option
@@ -51,3 +53,9 @@ val unfold : (global_reference * occurrences_expr) list -> clause -> unit tactic
 val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
 
 val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+
+val discriminate : evars_flag -> destruction_arg option -> unit tactic
+
+val injection : evars_flag -> intro_pattern list option -> destruction_arg option -> unit tactic
+
+val autorewrite : all:bool -> unit tactic option -> Id.t list -> clause -> unit tactic
-- 
cgit v1.2.3