From 8ffc337b2122a1a7deb47ae987f466e6208d8a81 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 1 Aug 2024 16:28:10 +0200
Subject: [PATCH] coqPackages.rewriter: init at 0.0.11

---
 .../coq-modules/rewriter/default.nix          | 22 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 2 files changed, 23 insertions(+)
 create mode 100644 pkgs/development/coq-modules/rewriter/default.nix

diff --git a/pkgs/development/coq-modules/rewriter/default.nix b/pkgs/development/coq-modules/rewriter/default.nix
new file mode 100644
index 000000000000..f5b425cd4811
--- /dev/null
+++ b/pkgs/development/coq-modules/rewriter/default.nix
@@ -0,0 +1,22 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+mkCoqDerivation {
+  pname = "rewriter";
+  owner = "mit-plv";
+  inherit version;
+  defaultVersion = let inherit (lib.versions) range; in
+    lib.switch coq.coq-version [
+      { case = range "8.17" "8.19"; out = "0.0.11"; }
+    ] null;
+  release = {
+    "0.0.11".sha256  = "sha256-aYoO08nwItlOoE5BnKRGib2Zk4Fz4Ni/L4QaqkObPow=";
+  };
+  releaseRev = v: "v${v}";
+
+  mlPlugin = true;
+
+  meta = {
+    description = "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography";
+    license = lib.licenses.mit;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index c6a6ce952f71..5a862d26d68b 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -123,6 +123,7 @@ let
       QuickChick = callPackage ../development/coq-modules/QuickChick {};
       reglang = callPackage ../development/coq-modules/reglang {};
       relation-algebra = callPackage ../development/coq-modules/relation-algebra {};
+      rewriter = callPackage ../development/coq-modules/rewriter {};
       semantics = callPackage ../development/coq-modules/semantics {};
       serapi = callPackage ../development/coq-modules/serapi {};
       simple-io = callPackage ../development/coq-modules/simple-io { };