From e844ba2919fd2795d1e0082f69e018dc5ddb093d Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 28 Oct 2018 14:22:35 -0400
Subject: Add CPSId tactics

---
 _CoqProject              |  1 +
 src/Util/Tactics.v       |  1 +
 src/Util/Tactics/CPSId.v | 41 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 43 insertions(+)
 create mode 100644 src/Util/Tactics/CPSId.v

diff --git a/_CoqProject b/_CoqProject
index eab813601..54f1cd4f7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6568,6 +6568,7 @@ src/Util/Strings/OctalString.v
 src/Util/Strings/Show.v
 src/Util/Strings/String.v
 src/Util/Tactics/BreakMatch.v
+src/Util/Tactics/CPSId.v
 src/Util/Tactics/CacheTerm.v
 src/Util/Tactics/ChangeInAll.v
 src/Util/Tactics/ClearAll.v
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index cd045fdbb..ee27e598f 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -8,6 +8,7 @@ Require Export Crypto.Util.Tactics.ClearDuplicates.
 Require Export Crypto.Util.Tactics.ClearbodyAll.
 Require Export Crypto.Util.Tactics.Contains.
 Require Export Crypto.Util.Tactics.ConvoyDestruct.
+Require Export Crypto.Util.Tactics.CPSId.
 Require Export Crypto.Util.Tactics.DebugPrint.
 Require Export Crypto.Util.Tactics.DestructHead.
 Require Export Crypto.Util.Tactics.DestructHyps.
diff --git a/src/Util/Tactics/CPSId.v b/src/Util/Tactics/CPSId.v
new file mode 100644
index 000000000..a7672ca51
--- /dev/null
+++ b/src/Util/Tactics/CPSId.v
@@ -0,0 +1,41 @@
+(** * [cps_id] is a scaffold for writing tactics that convert to cps normal form (where the continuation is the identity *)
+
+Ltac ensure_complex_continuation allow_option k :=
+  lazymatch k with
+  | id => fail
+  | (fun x => x) => fail
+  | _
+    => lazymatch allow_option with
+       | true => lazymatch k with
+                 | @Some _ => fail
+                 | (fun x => Some x) => fail
+                 | _ => idtac
+                 end
+       | false => idtac
+       | ?ao => fail 100 "Argument allow_option to ensure_complex_continuation must be true or false, not" ao
+       end
+  end.
+
+Ltac cps_id_step allow_option match_to_cont_lem :=
+  match goal with
+  | [ |- context[?e] ]
+    => let res := match_to_cont_lem e in
+       lazymatch res with
+       | (?k, ?lem)
+         => ensure_complex_continuation allow_option k;
+            (* sometimes reduction mismatches happen, so we cast [lem] to fix them *)
+            (rewrite lem || rewrite (lem : e = _))
+       end
+  | [ H : context[?e] |- _ ]
+    => let res := match_to_cont_lem e in
+       lazymatch res with
+       | (?k, ?lem)
+         => ensure_complex_continuation allow_option k;
+            (* sometimes reduction mismatches happen, so we cast [lem] to fix them *)
+            (rewrite lem in H || rewrite (lem : e = _) in H)
+       end
+  end.
+
+Ltac cps_id allow_option match_to_cont_lem := repeat cps_id_step allow_option match_to_cont_lem.
+Ltac cps_id_with_option match_to_cont_lem := cps_id true match_to_cont_lem.
+Ltac cps_id_no_option match_to_cont_lem := cps_id false match_to_cont_lem.
-- 
cgit v1.2.3