More bindings to primitive tactics.

5 files changed, 125 insertions, 3 deletions

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
diff --git a/theories/Notations.v b/theories/Notations.v
index d2c7059985..2d52904faf 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -130,6 +130,23 @@ Ltac2 Notation split := split.
 Ltac2 Notation "esplit" bnd(thunk(bindings)) := split0 true bnd.
 Ltac2 Notation esplit := esplit.
 
+Ltac2 exists0 ev bnds := match bnds with
+| [] => split0 ev (fun () => Std.NoBindings)
+| _ =>
+  let rec aux bnds := match bnds with
+  | [] => ()
+  | bnd :: bnds => split0 ev bnd; aux bnds
+  end in
+  aux bnds
+end.
+
+(*
+Ltac2 Notation "exists" bnd(list0(thunk(bindings), ",")) := exists0 false bnd.
+
+Ltac2 Notation "eexists" bnd(list0(thunk(bindings), ",")) := exists0 true bnd.
+Ltac2 Notation eexists := eexists.
+*)
+
 Ltac2 left0 ev bnd := enter_h ev Std.left bnd.
 
 Ltac2 Notation "left" bnd(thunk(bindings)) := left0 false bnd.
@@ -316,7 +333,7 @@ Ltac2 Notation "erewrite"
   tac(opt(seq("by", thunk(tactic)))) :=
   rewrite0 true rw cl tac.
 
-(** Other base tactics *)
+(** coretactics *)
 
 Ltac2 Notation reflexivity := Std.reflexivity ().
 
@@ -329,3 +346,17 @@ Ltac2 Notation admit := Std.admit ().
 Ltac2 Notation clear := Std.keep [].
 
 Ltac2 Notation refine := Control.refine.
+
+(** extratactics *)
+
+Ltac2 absurd0 c := Control.enter (fun _ => Std.absurd (c ())).
+
+Ltac2 Notation absurd := absurd0.
+
+Ltac2 subst0 ids := match ids with
+| [] => Std.subst_all ()
+| _ => Std.subst ids
+end.
+
+Ltac2 Notation "subst" ids(list0(ident)) := subst0 ids.
+Ltac2 Notation subst := subst.
diff --git a/theories/Std.v b/theories/Std.v
index dd81835c40..f380c10af8 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -184,7 +184,17 @@ Ltac2 @ external exact_no_check : constr -> unit := "ltac2" "tac_exactnocheck".
 Ltac2 @ external vm_cast_no_check : constr -> unit := "ltac2" "tac_vmcastnocheck".
 Ltac2 @ external native_cast_no_check : constr -> unit := "ltac2" "tac_nativecastnocheck".
 
+(** coretactics *)
+
+(** extratactics *)
+
+Ltac2 @ external discriminate : evar_flag -> destruction_arg option -> unit := "ltac2" "tac_discriminate".
+Ltac2 @ external injection : evar_flag -> intro_pattern list option -> destruction_arg option -> unit := "ltac2" "tac_injection".
+
 Ltac2 @ external absurd : constr -> unit := "ltac2" "tac_absurd".
+Ltac2 @ external contradiction : constr_with_bindings option -> unit := "ltac2" "tac_contradiction".
+
+Ltac2 @ external autorewrite : bool -> (unit -> unit) option -> ident list -> clause -> unit := "ltac2" "tac_autorewrite".
 
 Ltac2 @ external subst : ident list -> unit := "ltac2" "tac_subst".
 Ltac2 @ external subst_all : unit -> unit := "ltac2" "tac_substall".