1 files changed, 0 insertions, 120 deletions
diff --git a/src/Compilers/CommonSubexpressionEliminationDenote.v b/src/Compilers/CommonSubexpressionEliminationDenote.v
deleted file mode 100644
index 2218f62eb..000000000
--- a/src/Compilers/CommonSubexpressionEliminationDenote.v
+++ /dev/null
@@ -1,120 +0,0 @@
-(** * Common Subexpression Elimination for PHOAS Syntax *)
-Require Import Coq.Lists.List.
-Require Import Crypto.Compilers.Named.Context.
-Require Import Crypto.Compilers.Named.AListContext.
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.ExprInversion.
-Require Import Crypto.Compilers.Equality.
-Require Import Crypto.Compilers.SmartMap.
-Require Import Crypto.Compilers.CommonSubexpressionElimination.
-
-Section symbolic.
-  Context (base_type_code : Type)
-          (op_code : Type)
-          (base_type_code_beq : base_type_code -> base_type_code -> bool)
-          (op_code_beq : op_code -> op_code -> bool)
-          (base_type_code_bl : forall x y, base_type_code_beq x y = true -> x = y)
-          (base_type_code_lb : forall x y, x = y -> base_type_code_beq x y = true)
-          (op_code_bl : forall x y, op_code_beq x y = true -> x = y)
-          (op_code_lb : forall x y, x = y -> op_code_beq x y = true)
-          (op : flat_type base_type_code -> flat_type base_type_code -> Type)
-          (symbolize_op : forall s d, op s d -> op_code)
-          (denote_op : forall s d, op_code -> option (op s d))
-          (denote_symbolize_op : forall s d opc, denote_op s d (symbolize_op s d opc) = Some opc).
-
-  Local Notation symbolic_expr := (symbolic_expr base_type_code op_code).
-  Local Notation symbolic_expr_beq := (@symbolic_expr_beq base_type_code op_code base_type_code_beq op_code_beq).
-  Local Notation symbolic_expr_lb := (@internal_symbolic_expr_dec_lb base_type_code op_code base_type_code_beq op_code_beq base_type_code_lb op_code_lb).
-  Local Notation symbolic_expr_bl := (@internal_symbolic_expr_dec_bl base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op_code_bl).
-
-  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).
-
-  Local Notation flat_type_beq := (@flat_type_beq base_type_code base_type_code_beq).
-  Local Notation flat_type_dec_bl := (@flat_type_dec_bl base_type_code base_type_code_beq base_type_code_bl).
-
-  Local Notation symbolicify_smart_var := (@symbolicify_smart_var base_type_code op_code).
-  Local Notation symbolize_exprf := (@symbolize_exprf base_type_code op_code op symbolize_op).
-  Local Notation csef := (@csef base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
-  Local Notation cse := (@cse base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
-  Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
-  Local Notation SymbolicExprContext := (@SymbolicExprContext base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl).
-  Local Notation SymbolicExprContextOk := (@SymbolicExprContextOk base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl base_type_code_lb op_code_bl op_code_lb).
-  Local Notation prepend_prefix := (@prepend_prefix base_type_code op).
-
-  Section with_var.
-    Context {interp_base_type : base_type_code -> Type}
-            {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
-            (m : @SymbolicExprContext (interp_flat_type interp_base_type)).
-
-    Local Notation var_cast := (@var_cast _ (interp_flat_type interp_base_type) flat_type_beq flat_type_dec_bl).
-    Fixpoint denote_symbolic_expr
-             (t : flat_type)
-             (se : symbolic_expr)
-      : option (interp_flat_type interp_base_type t)
-      := match se, t with
-         | STT, Unit => Some tt
-         | SVar n, t
-           => match List.nth_error m (length m - S n) with
-              | Some e => @var_cast _ t (projT2 (snd e))
-              | None => None
-              end
-         | SOp argsT op args, _
-           => match denote_op argsT t op, @denote_symbolic_expr argsT args with
-              | Some opc, Some eargs => Some (interp_op _ _ opc eargs)
-              | Some _, None | None, Some _ | None, None => None
-              end
-         | SPair x y, Prod A B
-           => match @denote_symbolic_expr A x, @denote_symbolic_expr B y with
-              | Some ex, Some ey => Some (ex, ey)
-              | Some _, None | None, Some _ | None, None => None
-              end
-         | SFst A B x, A'
-           => if flat_type_beq A A'
-              then option_map (@fst _ _) (@denote_symbolic_expr (Prod A' B) x)
-              else None
-         | SSnd A B x, B'
-           => if flat_type_beq B B'
-              then option_map (@snd _ _) (@denote_symbolic_expr (Prod A B') x)
-              else None
-         | SInvalid, _
-         | STT, _
-         | SPair _ _, _
-           => None
-         end.
-
-    Fail Lemma denote_symbolize_exprf
-          (*(Hm : forall n v, List.nth_error m n = Some v -> denote_symbolic_expr *)
-          t e se e'
-      : @symbolize_exprf var t e = Some se
-        -> denote_symbolic_expr t se = Some e'
-        -> e' = e. (* The command has indeed failed with message:
-In environment
-base_type_code : Type
-op_code : Type
-base_type_code_beq : base_type_code -> base_type_code -> bool
-op_code_beq : op_code -> op_code -> bool
-base_type_code_bl : forall x y : base_type_code, base_type_code_beq x y = true -> x = y
-base_type_code_lb : forall x y : base_type_code, x = y -> base_type_code_beq x y = true
-op_code_bl : forall x y : op_code, op_code_beq x y = true -> x = y
-op_code_lb : forall x y : op_code, x = y -> op_code_beq x y = true
-op : flat_type -> flat_type -> Type
-symbolize_op : forall s d : flat_type, op s d -> op_code
-denote_op : forall s d : flat_type, op_code -> option (op s d)
-denote_symbolize_op : forall (s d : flat_type) (opc : op s d), denote_op s d (symbolize_op s d opc) = Some opc
-var : base_type_code -> Type
-m : SymbolicExprContext
-t : flat_type
-e : exprf t
-se : symbolic_expr
-e' : exprf t
-The term "e" has type
- "@Syntax.exprf base_type_code op
-    (fun t : base_type_code => prod (var t) (CommonSubexpressionElimination.symbolic_expr base_type_code op_code)) t"
-while it is expected to have type "@Syntax.exprf base_type_code op var t".
-                    *)
-  End with_var.
-End symbolic.