From 3e71c616fdafd86652bf9e14505ae1379a6f37bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Sep 2017 12:23:29 +0200
Subject: Binding the inversion family of tactics.

---
 src/tac2stdlib.ml   | 26 ++++++++++++++++++++------
 src/tac2tactics.ml  | 29 +++++++++++++++++++++++++++++
 src/tac2tactics.mli |  2 ++
 3 files changed, 51 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index a0eb0d60e5..03141805ef 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -128,9 +128,9 @@ let to_destruction_arg = function
 | ValBlk (0, [| c |]) ->
   (** FIXME: lost backtrace *)
   let c = thaw [] c >>= fun c -> return (to_constr_with_bindings c) in
-  ElimOnConstr c
-| ValBlk (1, [| id |]) -> ElimOnIdent (Loc.tag (Value.to_ident id))
-| ValBlk (2, [| n |]) -> ElimOnAnonHyp (Value.to_int n)
+  None, ElimOnConstr c
+| ValBlk (1, [| id |]) -> None, ElimOnIdent (Loc.tag (Value.to_ident id))
+| ValBlk (2, [| n |]) -> None, ElimOnAnonHyp (Value.to_int n)
 | _ -> assert false
 
 let to_induction_clause = function
@@ -139,7 +139,7 @@ let to_induction_clause = function
   let eqn = Value.to_option (fun p -> Loc.tag (to_intro_pattern_naming p)) eqn in
   let as_ = Value.to_option (fun p -> Loc.tag (to_or_and_intro_pattern p)) as_ in
   let in_ = Value.to_option to_clause in_ in
-  ((None, arg), eqn, as_, in_)
+  (arg, eqn, as_, in_)
 | _ ->
   assert false
 
@@ -170,6 +170,12 @@ let to_strategy = function
 | ValInt 1 -> Class_tactics.Dfs
 | _ -> assert false
 
+let to_inversion_kind = function
+| ValInt 0 -> Misctypes.SimpleInversion
+| ValInt 1 -> Misctypes.FullInversion
+| ValInt 2 -> Misctypes.FullInversionClear
+| _ -> assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -470,6 +476,14 @@ let () = define_prim4 "tac_rewrite" begin fun bt ev rw cl by ->
   Tac2tactics.rewrite ev rw cl by
 end
 
+let () = define_prim4 "tac_inversion" begin fun bt knd arg pat ids ->
+  let knd = to_inversion_kind knd in
+  let arg = to_destruction_arg arg in
+  let pat = Value.to_option (fun ipat -> Loc.tag (to_intro_pattern ipat)) pat in
+  let ids = Value.to_option (fun l -> Value.to_list Value.to_ident l) ids in
+  Tac2tactics.inversion knd arg pat ids
+end
+
 (** Tactics from coretactics *)
 
 let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity
@@ -592,14 +606,14 @@ end
 
 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
+  let arg = Value.to_option to_destruction_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
+  let arg = Value.to_option to_destruction_arg arg in
   Tac2tactics.injection ev ipat arg
 end
 
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 447f602f7a..b069e57235 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -252,3 +252,32 @@ let typeclasses_eauto strategy depth dbs =
     false, dbs
   in
   Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
+
+(** Inversion *)
+
+let inversion knd arg pat ids =
+  let ids = match ids with
+  | None -> []
+  | Some l -> l
+  in
+  begin match pat with
+  | None -> Proofview.tclUNIT None
+  | Some (_, IntroAction (IntroOrAndPattern p)) ->
+    Proofview.tclUNIT (Some (Loc.tag p))
+  | Some _ ->
+    Tacticals.New.tclZEROMSG (str "Inversion only accept disjunctive patterns")
+  end >>= fun pat ->
+  let inversion _ arg =
+    begin match arg with
+    | None -> assert false
+    | Some (_, ElimOnAnonHyp n) ->
+      Inv.inv_clause knd pat ids (AnonHyp n)
+    | Some (_, ElimOnIdent (_, id)) ->
+      Inv.inv_clause knd pat ids (NamedHyp id)
+    | Some (_, ElimOnConstr c) ->
+      let anon = Loc.tag @@ IntroNaming IntroAnonymous in
+      Tactics.specialize c (Some anon) >>= fun () ->
+      Tacticals.New.onLastHypId (fun id -> Inv.inv_clause knd pat ids (NamedHyp id))
+    end
+  in
+  on_destruction_arg inversion true (Some arg)
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 78d421303a..8b466cd529 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -99,3 +99,5 @@ val eauto : Hints.debug -> int option -> int option -> constr tactic list ->
 
 val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
+
+val inversion : inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
-- 
cgit v1.2.3