Version Util.Tactics2.{Constr,Proj,DestProj}

.gitignore

@@ -121,6 +121,10 @@ src/Rewriter/Util/plugins/ltac2_extra.mli
 src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg
 src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib
 
+src/Rewriter/Util/Tactics2/Constr.v
+src/Rewriter/Util/Tactics2/DestProj.v
+src/Rewriter/Util/Tactics2/Proj.v
+
 /.coq-version
 /.coq-version-compilation-date
 /.coq-version-config

Makefile.local.common

@@ -63,4 +63,7 @@ COMPATIBILITY_FILES := \
 	src/Rewriter/Util/plugins/RewriterBuild.v \
 	src/Rewriter/Util/plugins/StrategyTactic.v \
 	src/Rewriter/Util/plugins/Ltac2Extra.v \
+	src/Rewriter/Util/Tactics2/Constr.v \
+	src/Rewriter/Util/Tactics2/DestProj.v \
+	src/Rewriter/Util/Tactics2/Proj.v \
 	#

src/Rewriter/Util/Tactics2/Constr.v.v815

@@ -0,0 +1 @@
+Constr.v.v818

src/Rewriter/Util/Tactics2/Constr.v.v816

@@ -0,0 +1 @@
+Constr.v.v818

src/Rewriter/Util/Tactics2/Constr.v.v817

@@ -0,0 +1 @@
+Constr.v.v818

src/Rewriter/Util/Tactics2/Constr.v.v819

@@ -0,0 +1,100 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Require Rewriter.Util.Tactics2.Array.
+Require Rewriter.Util.Tactics2.Proj.
+Require Rewriter.Util.Tactics2.Option.
+Require Import Rewriter.Util.Tactics2.Iterate.
+Local Set Warnings Append "-masking-absolute-name".
+Require Import Rewriter.Util.plugins.Ltac2Extra.
+Import Ltac2.Constr.
+Import Ltac2.Bool.
+
+Ltac2 is_sort(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Sort _ => true
+  | _ => false
+  end.
+
+Module Unsafe.
+  Export Ltac2.Constr.Unsafe.
+
+  Ltac2 rec kind_nocast_gen kind (x : constr) :=
+    let k := kind x in
+    match k with
+    | Cast x _ _ => kind_nocast_gen kind x
+    | _ => k
+    end.
+
+  Ltac2 kind_nocast (x : constr) : kind := kind_nocast_gen kind x.
+
+  Module Case.
+    Ltac2 iter_invert (f : constr -> unit) (ci : case_invert) : unit :=
+      match ci with
+      | NoInvert => ()
+      | CaseInvert indices => Array.iter f indices
+      end.
+  End Case.
+
+  (** [iter f c] iters [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+  Ltac2 iter (f : constr -> unit) (c : constr) : unit :=
+    match kind c with
+    | Rel _ => () | Meta _ => () | Var _ => () | Sort _ => () | Constant _ _ => () | Ind _ _ => ()
+    | Constructor _ _ => () | Uint63 _ => () | Float _ => ()
+    | Cast c _ t => f c; f t
+    | Prod b c => f (Binder.type b); f c
+    | Lambda b c => f (Binder.type b); f c
+    | LetIn b t c => f (Binder.type b); f t; f c
+    | App c l => f c; Array.iter f l
+    | Evar _ l => () (* not possible to iter in Ltac2... *)
+    | Case _ x iv y bl
+      => Array.iter f bl;
+         Case.iter_invert f iv;
+         f x;
+         f y
+    | Proj _p c => f c
+    | Fix _ _ tl bl =>
+        Array.iter (fun b => f (Binder.type b)) tl;
+        Array.iter f bl
+    | CoFix _ tl bl =>
+        Array.iter (fun b => f (Binder.type b)) tl;
+        Array.iter f bl
+    | Array _u t def ty =>
+        Array.iter f t; f def; f ty
+    end.
+
+  (** [iter_with_binders g f n c] iters [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+  Ltac2 iter_with_binders (g : 'a -> 'a) (f : 'a -> constr -> unit) (n : 'a) (c : constr) : unit :=
+    match kind c with
+    | Rel _ => () | Meta _ => () | Var _ => () | Sort _ => () | Constant _ _ => () | Ind _ _ => ()
+    | Constructor _ _ => () | Uint63 _ => () | Float _ => ()
+    | Cast c _ t => f n c; f n t
+    | Prod b c => f n (Binder.type b); f (g n) c
+    | Lambda b c => f n (Binder.type b); f (g n) c
+    | LetIn b t c => f n (Binder.type b); f n t; f (g n) c
+    | App c l => f n c; Array.iter (f n) l
+    | Evar _ l => () (* not possible to iter in Ltac2... *)
+    | Case _ x iv y bl
+      => Array.iter (f n) bl;
+         Case.iter_invert (f n) iv;
+         f n x;
+         f n y
+    | Proj _p c => f n c
+    | Fix _ _ tl bl =>
+        Array.iter (fun b => f n (Binder.type b)) tl;
+        Array.iter (f (iterate g (Array.length tl) n)) bl
+    | CoFix _ tl bl =>
+        Array.iter (fun b => f n (Binder.type b)) tl;
+        Array.iter (f (iterate g (Array.length tl) n)) bl
+    | Array _u t def ty =>
+        Array.iter (f n) t; f n def; f n ty
+    end.
+End Unsafe.
+Import Unsafe.
+
+Ltac2 equal_nounivs : constr -> constr -> bool := Ltac2.Constr.equal_nounivs.

src/Rewriter/Util/Tactics2/DestProj.v.v815

@@ -0,0 +1 @@
+DestProj.v.v818

src/Rewriter/Util/Tactics2/DestProj.v.v816

@@ -0,0 +1 @@
+DestProj.v.v818

src/Rewriter/Util/Tactics2/DestProj.v.v817

@@ -0,0 +1 @@
+DestProj.v.v818

src/Rewriter/Util/Tactics2/DestProj.v.v819

@@ -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/Proj.v.v815

@@ -0,0 +1 @@
+Proj.v.v818

src/Rewriter/Util/Tactics2/Proj.v.v816

@@ -0,0 +1 @@
+Proj.v.v818

src/Rewriter/Util/Tactics2/Proj.v.v817

@@ -0,0 +1 @@
+Proj.v.v818

src/Rewriter/Util/Tactics2/Proj.v.v819

@@ -0,0 +1,8 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.
+Import Constr.Unsafe.
+
+Ltac2 equal (x : projection) (y : projection) : bool
+  := let dummy := make (Rel (-1)) in
+     Constr.equal (make (Proj x dummy)) (make (Proj y dummy)).