1 files changed, 0 insertions, 58 deletions
diff --git a/src/Compilers/Z/RewriteAddToAdc.v b/src/Compilers/Z/RewriteAddToAdc.v
deleted file mode 100644
index 838c92b75..000000000
--- a/src/Compilers/Z/RewriteAddToAdc.v
+++ /dev/null
@@ -1,58 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Compilers.Named.Context.
-Require Import Crypto.Compilers.Named.Syntax.
-Require Import Crypto.Compilers.Named.InterpretToPHOAS.
-Require Import Crypto.Compilers.Named.Compile.
-Require Import Crypto.Compilers.Named.Wf.
-Require Import Crypto.Compilers.Named.CountLets.
-Require Import Crypto.Compilers.Named.PositiveContext.
-Require Import Crypto.Compilers.Named.PositiveContext.Defaults.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.ExprInversion.
-Require Import Crypto.Compilers.Z.Syntax.
-Require Import Crypto.Compilers.Z.Named.DeadCodeElimination.
-Require Import Crypto.Compilers.Z.Named.RewriteAddToAdc.
-Require Import Crypto.Util.PointedProp.
-Require Import Crypto.Util.Decidable.
-
-(** N.B. This procedure only works when there are no nested lets,
-    i.e., nothing like [let x := let y := z in w] in the PHOAS syntax
-    tree.  This is a limitation of [compile]. *)
-
-Local Open Scope bool_scope.
-
-Section language.
-  Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl).
-
-  Definition RewriteAdc {t} (e : Expr t)
-    : Expr t
-    := let is_good e' := match option_map (wf_unit (Context:=PContext _) empty) e' with
-                         | Some (Some trivial) => true
-                         | _ => false
-                         end in
-       let interp_to_phoas := InterpToPHOAS (Context:=fun var => PContext var)
-                                            (fun _ t => Op (OpConst 0%Z) TT) in
-       let e' := compile (e _) (DefaultNamesFor e) in
-       let e' := option_map (rewrite_expr Pos.eqb) e' in
-       let good := is_good e' in
-       let e' := match e' with
-                 | Some e'
-                   => let ls := Named.default_names_for e' in
-                      match EliminateDeadCode (Context:=PContext _) e' ls with
-                      | Some e'' => Some e''
-                      | None => Some e'
-                      end
-                 | None => None
-                 end in
-       let good := good && is_good e' in
-       if good
-       then let e' := option_map interp_to_phoas e' in
-            match e' with
-            | Some e'
-              => match t return Expr (Arrow (domain t) (codomain t)) -> Expr t with
-                 | Arrow _ _ => fun x => x
-                 end e'
-            | None => e
-            end
-       else e.
-End language.