1 files changed, 0 insertions, 39 deletions
diff --git a/src/Compilers/Rewriter.v b/src/Compilers/Rewriter.v
deleted file mode 100644
index a23627480..000000000
--- a/src/Compilers/Rewriter.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Crypto.Compilers.Syntax.
-
-Section language.
-  Context {base_type_code : Type}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
-  Local Notation flat_type := (flat_type base_type_code).
-  Local Notation type := (type base_type_code).
-  Local Notation exprf := (@exprf base_type_code op).
-  Local Notation expr := (@expr base_type_code op).
-  Local Notation Expr := (@Expr base_type_code op).
-
-  Section with_var.
-    Context {var : base_type_code -> Type}.
-    Context (rewrite_op_expr : forall src dst (opc : op src dst),
-                exprf (var:=var) src -> exprf (var:=var) dst).
-
-    Fixpoint rewrite_opf {t} (e : @exprf var t) : @exprf var t
-      := match e in Syntax.exprf _ _ t return @exprf var t with
-         | LetIn tx ex tC eC
-           => LetIn (@rewrite_opf tx ex) (fun x => @rewrite_opf tC (eC x))
-         | Var _ x => Var x
-         | TT => TT
-         | Pair tx ex ty ey
-           => Pair (@rewrite_opf tx ex) (@rewrite_opf ty ey)
-         | Op t1 tR opc args => rewrite_op_expr _ _ opc (@rewrite_opf t1 args)
-         end.
-
-    Definition rewrite_op {t} (e : @expr var t) : @expr var t
-      := match e in Syntax.expr _ _ t return @expr var t with
-         | Abs _ _ f => Abs (fun x => rewrite_opf (f x))
-         end.
-  End with_var.
-
-  Definition RewriteOp
-             (rewrite_op_expr : forall var src dst, op src dst -> @exprf var src -> @exprf var dst)
-             {t} (e : Expr t)
-    : Expr t
-    := fun var => rewrite_op (rewrite_op_expr _) (e _).
-End language.