Adding the induction and destruct tactics.

3 files changed, 66 insertions, 5 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index b678b65b82..7e421c8577 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -17,6 +17,10 @@ open Proofview.Notations
 
 module Value = Tac2ffi
 
+let return x = Proofview.tclUNIT x
+let v_unit = Value.of_unit ()
+let thaw f = Tac2interp.interp_app f [v_unit]
+
 let to_pair f g = function
 | ValBlk (0, [| x; y |]) -> (f x, g y)
 | _ -> assert false
@@ -119,13 +123,28 @@ and to_intro_patterns il =
   let map ipat = Loc.tag (to_intro_pattern ipat) in
   Value.to_list map il
 
+let to_destruction_arg = function
+| ValBlk (0, [| c |]) ->
+  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)
+| _ -> assert false
+
+let to_induction_clause = function
+| ValBlk (0, [| arg; eqn; as_; in_ |]) ->
+  let arg = to_destruction_arg arg in
+  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_)
+| _ ->
+  assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
 
-let return x = Proofview.tclUNIT x
-let v_unit = Value.of_unit ()
-
 let lift tac = tac <*> return v_unit
 
 let wrap f =
@@ -134,8 +153,6 @@ let wrap f =
 let wrap_unit f =
   return () >>= fun () -> f (); return v_unit
 
-let thaw f = Tac2interp.interp_app f [v_unit]
-
 let define_prim0 name tac =
   let tac = function
   | [_] -> lift tac
@@ -245,6 +262,20 @@ let () = define_prim4 "tac_set" begin fun ev idopt c cl ->
   Tactics.letin_pat_tac ev None na (sigma, c) cl
 end
 
+let () = define_prim3 "tac_destruct" begin fun ev ic using ->
+  let ev = Value.to_bool ev in
+  let ic = Value.to_list to_induction_clause ic in
+  let using = Value.to_option to_constr_with_bindings using in
+  Tac2tactics.induction_destruct false ev ic using
+end
+
+let () = define_prim3 "tac_induction" begin fun ev ic using ->
+  let ev = Value.to_bool ev in
+  let ic = Value.to_list to_induction_clause ic in
+  let using = Value.to_option to_constr_with_bindings using in
+  Tac2tactics.induction_destruct true ev ic using
+end
+
 let () = define_prim1 "tac_red" begin fun cl ->
   let cl = to_clause cl in
   Tactics.reduce (Red false) cl
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 2590d7daed..439250db78 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -6,7 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Misctypes
+open Tactypes
 open Tactics
+open Proofview
 open Tacmach.New
 open Tacticals.New
 open Proofview.Notations
@@ -23,3 +26,21 @@ let apply adv ev cb cl =
   match cl with
   | None -> Tactics.apply_with_delayed_bindings_gen adv ev cb
   | Some (id, cl) -> Tactics.apply_delayed_in adv ev id cb cl
+
+type induction_clause =
+  EConstr.constr with_bindings tactic destruction_arg *
+  intro_pattern_naming option *
+  or_and_intro_pattern option *
+  Locus.clause option
+
+let map_destruction_arg = function
+| ElimOnConstr c -> ElimOnConstr (delayed_of_tactic c)
+| ElimOnIdent id -> ElimOnIdent id
+| ElimOnAnonHyp n -> ElimOnAnonHyp n
+
+let map_induction_clause ((clear, arg), eqn, as_, occ) =
+  ((clear, map_destruction_arg arg), (eqn, as_), occ)
+
+let induction_destruct isrec ev ic using =
+  let ic = List.map map_induction_clause ic in
+  Tactics.induction_destruct isrec ev (ic, using)
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 86278f177e..f29793411a 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -16,3 +16,12 @@ open Proofview
 val apply : advanced_flag -> evars_flag ->
   EConstr.constr with_bindings tactic list ->
   (Id.t * intro_pattern option) option -> unit tactic
+
+type induction_clause =
+  EConstr.constr with_bindings tactic destruction_arg *
+  intro_pattern_naming option *
+  or_and_intro_pattern option *
+  Locus.clause option
+
+val induction_destruct : rec_flag -> evars_flag ->
+  induction_clause list -> EConstr.constr with_bindings option -> unit Proofview.tactic