Ltac2 Util: Add various destKind helpers

_CoqProject.in

@@ -112,6 +112,23 @@ src/Rewriter/Util/Tactics2/Array.v
 src/Rewriter/Util/Tactics2/Char.v
 src/Rewriter/Util/Tactics2/Constr.v
 src/Rewriter/Util/Tactics2/DecomposeLambda.v
+src/Rewriter/Util/Tactics2/DestApp.v
+src/Rewriter/Util/Tactics2/DestCase.v
+src/Rewriter/Util/Tactics2/DestCast.v
+src/Rewriter/Util/Tactics2/DestCoFix.v
+src/Rewriter/Util/Tactics2/DestConstant.v
+src/Rewriter/Util/Tactics2/DestConstructor.v
+src/Rewriter/Util/Tactics2/DestEvar.v
+src/Rewriter/Util/Tactics2/DestFix.v
+src/Rewriter/Util/Tactics2/DestInd.v
+src/Rewriter/Util/Tactics2/DestLambda.v
+src/Rewriter/Util/Tactics2/DestLetIn.v
+src/Rewriter/Util/Tactics2/DestMeta.v
+src/Rewriter/Util/Tactics2/DestProd.v
+src/Rewriter/Util/Tactics2/DestProj.v
+src/Rewriter/Util/Tactics2/DestRel.v
+src/Rewriter/Util/Tactics2/DestSort.v
+src/Rewriter/Util/Tactics2/DestVar.v
 src/Rewriter/Util/Tactics2/FixNotationsForPerformance.v
 src/Rewriter/Util/Tactics2/Head.v
 src/Rewriter/Util/Tactics2/HeadReference.v

src/Rewriter/Util/Tactics2/DestApp.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_an_app (kind) ].
+Ltac2 destApp (c : constr) :=
+  let k := kind c in
+  match k with
+  | App f args => (f, args)
+  | _ => Control.throw (Not_an_app k)
+  end.

src/Rewriter/Util/Tactics2/DestCase.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_case (kind) ].
+Ltac2 destCase (c : constr) :=
+  let k := kind c in
+  match k with
+  | Case a b c d e => (a, b, c, d, e)
+  | _ => Control.throw (Not_a_case k)
+  end.

src/Rewriter/Util/Tactics2/DestCast.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_cast (kind) ].
+Ltac2 destCast (c : constr) :=
+  let k := kind c in
+  match k with
+  | Cast x y z => (x, y, z)
+  | _ => Control.throw (Not_a_cast k)
+  end.

src/Rewriter/Util/Tactics2/DestCoFix.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_cofix (kind) ].
+Ltac2 destCoFix (c : constr) :=
+  let k := kind c in
+  match k with
+  | CoFix x y z => (x, y, z)
+  | _ => Control.throw (Not_a_cofix k)
+  end.

src/Rewriter/Util/Tactics2/DestConstant.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_constant (kind) ].
+Ltac2 destConstant (c : constr) :=
+  let k := kind c in
+  match k with
+  | Constant e inst => (e, inst)
+  | _ => Control.throw (Not_a_constant k)
+  end.

src/Rewriter/Util/Tactics2/DestConstructor.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_constructor (kind) ].
+Ltac2 destConstructor (c : constr) :=
+  let k := kind c in
+  match k with
+  | Constructor e inst => (e, inst)
+  | _ => Control.throw (Not_a_constructor k)
+  end.

src/Rewriter/Util/Tactics2/DestEvar.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_an_evar (kind) ].
+Ltac2 destEvar (c : constr) :=
+  let k := kind c in
+  match k with
+  | Evar e inst => (e, inst)
+  | _ => Control.throw (Not_an_evar k)
+  end.

src/Rewriter/Util/Tactics2/DestFix.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_fix (kind) ].
+Ltac2 destFix (c : constr) :=
+  let k := kind c in
+  match k with
+  | Fix x y z w => (x, y, z, w)
+  | _ => Control.throw (Not_a_fix k)
+  end.

src/Rewriter/Util/Tactics2/DestInd.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_an_ind (kind) ].
+Ltac2 destInd (c : constr) :=
+  let k := kind c in
+  match k with
+  | Ind e inst => (e, inst)
+  | _ => Control.throw (Not_an_ind k)
+  end.

src/Rewriter/Util/Tactics2/DestLambda.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_lambda (kind) ].
+Ltac2 destLambda (c : constr) :=
+  let k := kind c in
+  match k with
+  | Lambda x f => (x, f)
+  | _ => Control.throw (Not_a_lambda k)
+  end.

src/Rewriter/Util/Tactics2/DestLetIn.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_let_in (kind) ].
+Ltac2 destLetIn (c : constr) :=
+  let k := kind c in
+  match k with
+  | LetIn x y z => (x, y, z)
+  | _ => Control.throw (Not_a_let_in k)
+  end.

src/Rewriter/Util/Tactics2/DestMeta.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_meta (kind) ].
+Ltac2 destMeta (c : constr) :=
+  let k := kind c in
+  match k with
+  | Meta e => e
+  | _ => Control.throw (Not_a_meta k)
+  end.

src/Rewriter/Util/Tactics2/DestProd.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_prod (kind) ].
+Ltac2 destProd (c : constr) :=
+  let k := kind c in
+  match k with
+  | Prod x f => (x, f)
+  | _ => Control.throw (Not_a_prod k)
+  end.

src/Rewriter/Util/Tactics2/DestProj.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_proj (kind) ].
+Ltac2 destProj (c : constr) :=
+  let k := kind c in
+  match k with
+  | Proj p v => (p, v)
+  | _ => Control.throw (Not_a_proj k)
+  end.

src/Rewriter/Util/Tactics2/DestRel.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_rel (kind) ].
+Ltac2 destRel (c : constr) :=
+  let k := kind c in
+  match k with
+  | Rel i => i
+  | _ => Control.throw (Not_a_rel k)
+  end.

src/Rewriter/Util/Tactics2/DestSort.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_sort (kind) ].
+Ltac2 destSort (c : constr) :=
+  let k := kind c in
+  match k with
+  | Sort s => s
+  | _ => Control.throw (Not_a_sort k)
+  end.

src/Rewriter/Util/Tactics2/DestVar.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_var (kind) ].
+Ltac2 destVar (c : constr) :=
+  let k := kind c in
+  match k with
+  | Var v => v
+  | _ => Control.throw (Not_a_var k)
+  end.