Remove the Const constructor of exprf

We instead use the [Op] constructor for constants.  This allows [exprf]
to not depend on the interpretation function; this means we don't need
to map over it to change the interpretation function.  This saves us
about 300 lines of code and about 30s of build time, total.

After     | File Name                                                              | Before    || Change
-----------------------------------------------------------------------------------------------------------
18m11.34s | Total                                                                  | 18m46.86s || -0m35.52s
-----------------------------------------------------------------------------------------------------------
0m19.99s  | Specific/GF25519ReflectiveAddCoordinates                               | 0m31.78s  || -0m11.79s
1m53.69s  | Specific/GF25519Reflective/Reified/LadderStep                          | 2m01.32s  || -0m07.62s
1m27.74s  | Specific/GF25519Reflective/Reified/AddCoordinates                      | 1m34.03s  || -0m06.29s
0m01.45s  | Specific/GF25519Reflective                                             | 0m06.31s  || -0m04.85s
0m04.62s  | Reflection/InlineInterp                                                | 0m01.52s  || +0m03.10s
1m19.68s  | CompleteEdwardsCurve/ExtendedCoordinates                               | 1m21.19s  || -0m01.50s
0m02.90s  | Reflection/InlineWf                                                    | 0m01.80s  || +0m01.09s
   N/A    | Reflection/MapWithInterpInfo                                           | 0m01.70s  || -0m01.70s
1m32.32s  | Test/Curve25519SpecTestVectors                                         | 1m32.25s  || +0m00.06s
1m12.79s  | Experiments/Ed25519                                                    | 1m13.17s  || -0m00.38s
0m40.52s  | ModularArithmetic/Conversion                                           | 0m40.44s  || +0m00.08s
0m34.57s  | Spec/Ed25519                                                           | 0m34.53s  || +0m00.03s
0m30.82s  | ModularArithmetic/ModularBaseSystemProofs                              | 0m30.89s  || -0m00.07s
0m30.11s  | Specific/GF25519Bounded                                                | 0m30.21s  || -0m00.10s
0m23.20s  | Experiments/MontgomeryCurve                                            | 0m23.26s  || -0m00.06s
0m22.16s  | Reflection/Z/Interpretations128/Relations                              | 0m21.72s  || +0m00.44s
0m21.69s  | ModularArithmetic/Pow2BaseProofs                                       | 0m21.58s  || +0m00.11s
0m20.25s  | Algebra                                                                | 0m20.27s  || -0m00.01s
0m19.81s  | Specific/GF25519                                                       | 0m19.83s  || -0m00.01s
0m18.82s  | Reflection/Z/Interpretations64/Relations                               | 0m18.50s  || +0m00.32s
0m18.19s  | EdDSARepChange                                                         | 0m18.26s  || -0m00.07s
0m17.08s  | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems                      | 0m17.16s  || -0m00.08s
0m14.10s  | Util/ZUtil                                                             | 0m14.03s  || +0m00.07s
0m10.05s  | Testbit                                                                | 0m10.02s  || +0m00.03s
0m08.95s  | Specific/GF25519BoundedCommon                                          | 0m08.90s  || +0m00.04s
0m08.87s  | BoundedArithmetic/ArchitectureToZLikeProofs                            | 0m08.81s  || +0m00.05s
0m08.80s  | Assembly/GF25519                                                       | 0m08.82s  || -0m00.01s
0m08.80s  | ModularArithmetic/Montgomery/ZProofs                                   | 0m08.87s  || -0m00.06s
0m08.51s  | Encoding/PointEncoding                                                 | 0m08.53s  || -0m00.01s
0m08.37s  | BoundedArithmetic/Double/Proofs/Multiply                               | 0m08.39s  || -0m00.02s
0m08.34s  | Specific/GF1305                                                        | 0m08.31s  || +0m00.02s
0m07.85s  | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate          | 0m07.86s  || -0m00.01s
0m07.60s  | Specific/GF25519Reflective/Reified/Mul                                 | 0m07.52s  || +0m00.08s
0m07.13s  | MxDHRepChange                                                          | 0m07.08s  || +0m00.04s
0m06.85s  | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate                    | 0m06.77s  || +0m00.08s
0m06.62s  | Reflection/Z/InterpretationsGen                                        | 0m06.62s  || +0m00.00s
0m05.69s  | Reflection/Z/Interpretations64/RelationsCombinations                   | 0m05.60s  || +0m00.09s
0m05.68s  | Reflection/Z/Interpretations128/RelationsCombinations                  | 0m05.67s  || +0m00.00s
0m05.48s  | Specific/SC25519                                                       | 0m05.38s  || +0m00.10s
0m05.40s  | BoundedArithmetic/Double/Proofs/RippleCarryAddSub                      | 0m05.36s  || +0m00.04s
0m04.93s  | ModularArithmetic/ModularBaseSystemListProofs                          | 0m04.96s  || -0m00.03s
0m04.87s  | WeierstrassCurve/Pre                                                   | 0m04.83s  || +0m00.04s
0m04.45s  | Specific/GF25519Reflective/Reified/PreFreeze                           | 0m04.56s  || -0m00.10s
0m04.33s  | Specific/GF25519Reflective/CommonBinOp                                 | 0m04.55s  || -0m00.21s
0m03.95s  | ModularArithmetic/BarrettReduction/ZHandbook                           | 0m03.98s  || -0m00.02s
0m03.87s  | Specific/GF25519Reflective/CommonUnOp                                  | 0m04.08s  || -0m00.20s
0m03.86s  | Encoding/PointEncodingPre                                              | 0m03.88s  || -0m00.02s
0m03.84s  | BaseSystemProofs                                                       | 0m03.88s  || -0m00.04s
0m03.75s  | Specific/GF25519Reflective/CommonUnOpWireToFE                          | 0m03.96s  || -0m00.20s
0m03.64s  | CompleteEdwardsCurve/Pre                                               | 0m03.60s  || +0m00.04s
0m03.51s  | BoundedArithmetic/InterfaceProofs                                      | 0m03.42s  || +0m00.08s
0m03.41s  | ModularArithmetic/Tutorial                                             | 0m03.38s  || +0m00.03s
0m03.30s  | Reflection/LinearizeWf                                                 | 0m04.24s  || -0m00.94s
0m03.20s  | Specific/GF25519Reflective/Reified/CarrySub                            | 0m03.28s  || -0m00.07s
0m03.14s  | ModularArithmetic/ZBoundedZ                                            | 0m03.14s  || +0m00.00s
0m03.14s  | ModularArithmetic/BarrettReduction/ZGeneralized                        | 0m03.14s  || +0m00.00s
0m02.95s  | Specific/GF25519Reflective/Reified/CarryAdd                            | 0m02.93s  || +0m00.02s
0m02.92s  | Specific/GF25519Reflective/Common9_4Op                                 | 0m02.89s  || +0m00.02s
0m02.82s  | Specific/GF25519Reflective/Reified/CarryOpp                            | 0m02.95s  || -0m00.13s
0m02.82s  | BoundedArithmetic/Double/Proofs/Decode                                 | 0m02.90s  || -0m00.08s
0m02.69s  | BoundedArithmetic/Double/Proofs/ShiftRight                             | 0m02.69s  || +0m00.00s
0m02.66s  | ModularArithmetic/ModularArithmeticTheorems                            | 0m02.67s  || -0m00.00s
0m02.63s  | Specific/FancyMachine256/Montgomery                                    | 0m02.24s  || +0m00.38s
0m02.61s  | Specific/GF25519Reflective/CommonUnOpFEToWire                          | 0m02.76s  || -0m00.14s
0m02.58s  | BoundedArithmetic/Double/Proofs/ShiftLeft                              | 0m02.58s  || +0m00.00s
0m02.56s  | Specific/GF25519Reflective/Common                                      | 0m02.60s  || -0m00.04s
0m02.52s  | Specific/FancyMachine256/Barrett                                       | 0m02.20s  || +0m00.31s
0m02.50s  | Specific/GF25519BoundedAddCoordinates                                  | 0m02.60s  || -0m00.10s
0m02.39s  | ModularArithmetic/BarrettReduction/ZBounded                            | 0m02.31s  || +0m00.08s
0m02.34s  | ModularArithmetic/ModularBaseSystemOpt                                 | 0m02.31s  || +0m00.02s
0m02.02s  | Specific/GF25519Reflective/Reified/Sub                                 | 0m02.01s  || +0m00.01s
0m01.98s  | Reflection/WfReflective                                                | 0m02.54s  || -0m00.56s
0m01.94s  | Specific/GF25519Reflective/Reified/Pack                                | 0m02.07s  || -0m00.12s
0m01.93s  | Assembly/Evaluables                                                    | 0m01.93s  || +0m00.00s
0m01.92s  | Specific/GF25519Reflective/Reified/Unpack                              | 0m02.04s  || -0m00.12s
0m01.90s  | Specific/FancyMachine256/Core                                          | 0m01.79s  || +0m00.10s
0m01.79s  | ModularArithmetic/Montgomery/ZBounded                                  | 0m01.86s  || -0m00.07s
0m01.77s  | Specific/GF25519ExtendedAddCoordinates                                 | 0m01.76s  || +0m00.01s
0m01.68s  | Specific/GF25519Reflective/Reified/Add                                 | 0m01.69s  || -0m00.01s
0m01.67s  | Specific/GF25519BoundedExtendedAddCoordinates                          | 0m01.79s  || -0m00.12s
0m01.63s  | Experiments/Ed25519Extraction                                          | 0m01.66s  || -0m00.03s
0m01.62s  | Specific/GF25519Reflective/Reified/Opp                                 | 0m01.72s  || -0m00.09s
0m01.54s  | Specific/GF25519Reflective/Reified/GeModulus                           | 0m01.59s  || -0m00.05s
0m01.50s  | Reflection/TestCase                                                    | 0m01.42s  || +0m00.08s
0m01.47s  | ModularArithmetic/BarrettReduction/Z                                   | 0m01.47s  || +0m00.00s
0m01.43s  | Assembly/Compile                                                       | 0m01.46s  || -0m00.03s
0m01.33s  | Reflection/WfProofs                                                    | 0m01.95s  || -0m00.61s
0m01.26s  | ModularArithmetic/PrimeFieldTheorems                                   | 0m01.28s  || -0m00.02s
0m01.20s  | Assembly/Conversions                                                   | 0m01.19s  || +0m00.01s
0m01.16s  | ModularArithmetic/ExtendedBaseVector                                   | 0m01.22s  || -0m00.06s
0m01.16s  | BaseSystem                                                             | 0m01.15s  || +0m00.01s
0m01.09s  | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.11s  || -0m00.02s
0m00.99s  | Util/NumTheoryUtil                                                     | 0m00.96s  || +0m00.03s
0m00.96s  | Assembly/HL                                                            | 0m00.96s  || +0m00.00s
0m00.94s  | Assembly/LL                                                            | 0m00.99s  || -0m00.05s
0m00.94s  | Assembly/Pipeline                                                      | 0m00.92s  || +0m00.01s
0m00.88s  | Reflection/WfInversion                                                 | 0m01.21s  || -0m00.32s
0m00.86s  | Assembly/PhoasCommon                                                   | 0m00.91s  || -0m00.05s
0m00.86s  | Specific/GF25519Reflective/CommonUnOpFEToZ                             | 0m01.02s  || -0m00.16s
0m00.85s  | BoundedArithmetic/Double/Proofs/LoadImmediate                          | 0m00.86s  || -0m00.01s
0m00.84s  | BoundedArithmetic/Double/Proofs/BitwiseOr                              | 0m00.91s  || -0m00.07s
0m00.82s  | BoundedArithmetic/X86ToZLikeProofs                                     | 0m00.85s  || -0m00.03s
0m00.79s  | Util/IterAssocOp                                                       | 0m00.82s  || -0m00.02s
0m00.75s  | Reflection/Z/Syntax                                                    | 0m00.67s  || +0m00.07s
0m00.73s  | Util/PartiallyReifiedProp                                              | 0m00.73s  || +0m00.00s
0m00.70s  | Encoding/ModularWordEncodingTheorems                                   | 0m00.76s  || -0m00.06s
0m00.70s  | Specific/GF25519Reflective/Reified                                     | 0m00.72s  || -0m00.02s
0m00.66s  | BoundedArithmetic/Double/Repeated/Proofs/Multiply                      | 0m00.62s  || +0m00.04s
0m00.66s  | ModularArithmetic/PseudoMersenneBaseParamProofs                        | 0m00.66s  || +0m00.00s
0m00.64s  | Encoding/ModularWordEncodingPre                                        | 0m00.63s  || +0m00.01s
0m00.61s  | ModularArithmetic/ModularBaseSystem                                    | 0m00.66s  || -0m00.05s
0m00.61s  | Util/AdditionChainExponentiation                                       | 0m00.64s  || -0m00.03s
0m00.60s  | ModularArithmetic/ExtPow2BaseMulProofs                                 | 0m00.64s  || -0m00.04s
0m00.60s  | Reflection/MultiSizeTest2                                              | 0m00.71s  || -0m00.10s
0m00.60s  | Spec/EdDSA                                                             | 0m00.65s  || -0m00.05s
0m00.59s  | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.51s  || +0m00.07s
0m00.58s  | BoundedArithmetic/Interface                                            | 0m00.60s  || -0m00.02s
0m00.58s  | ModularArithmetic/ModularBaseSystemList                                | 0m00.61s  || -0m00.03s
0m00.55s  | Spec/ModularWordEncoding                                               | 0m00.63s  || -0m00.07s
0m00.55s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                | 0m00.50s  || +0m00.05s
0m00.55s  | Reflection/InterpWfRel                                                 | 0m00.58s  || -0m00.02s
0m00.54s  | BoundedArithmetic/X86ToZLike                                           | 0m00.55s  || -0m00.01s
0m00.54s  | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.53s  || +0m00.01s
0m00.54s  | BoundedArithmetic/Double/Proofs/SelectConditional                      | 0m00.62s  || -0m00.07s
0m00.54s  | Reflection/WfReflectiveGen                                             | 0m00.58s  || -0m00.03s
0m00.52s  | BoundedArithmetic/ArchitectureToZLike                                  | 0m00.41s  || +0m00.11s
0m00.51s  | BoundedArithmetic/Double/Core                                          | 0m00.48s  || +0m00.03s
0m00.50s  | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.51s  || -0m00.01s
0m00.49s  | Spec/WeierstrassCurve                                                  | 0m00.42s  || +0m00.07s
0m00.48s  | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.54s  || -0m00.06s
0m00.47s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.58s  || -0m00.10s
0m00.47s  | Reflection/InterpWf                                                    | 0m00.50s  || -0m00.03s
0m00.47s  | ModularArithmetic/Pre                                                  | 0m00.48s  || -0m00.01s
0m00.47s  | BoundedArithmetic/Double/Repeated/Core                                 | 0m00.46s  || +0m00.00s
0m00.46s  | Reflection/Z/Interpretations64                                         | 0m00.49s  || -0m00.02s
0m00.45s  | Reflection/InputSyntax                                                 | 0m00.42s  || +0m00.03s
   N/A    | Reflection/MapInterpWf                                                 | 0m00.44s  || -0m00.44s
0m00.44s  | Spec/CompleteEdwardsCurve                                              | 0m00.39s  || +0m00.04s
0m00.44s  | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic                   | 0m00.42s  || +0m00.02s
0m00.44s  | Reflection/Z/Interpretations128                                        | 0m00.52s  || -0m00.08s
0m00.44s  | ModularArithmetic/ZBounded                                             | 0m00.45s  || -0m00.01s
0m00.42s  | BoundedArithmetic/StripCF                                              | 0m00.42s  || +0m00.00s
0m00.42s  | Reflection/Z/Reify                                                     | 0m00.43s  || -0m00.01s
0m00.42s  | ModularArithmetic/ModularBaseSystemListZOperationsProofs               | 0m00.47s  || -0m00.04s
0m00.41s  | Reflection/Named/DeadCodeElimination                                   | 0m00.43s  || -0m00.02s
0m00.41s  | ModularArithmetic/PseudoMersenneBaseParams                             | 0m00.38s  || +0m00.02s
0m00.41s  | Spec/ModularArithmetic                                                 | 0m00.34s  || +0m00.06s
0m00.41s  | Reflection/Named/RegisterAssign                                        | 0m00.37s  || +0m00.03s
0m00.41s  | Reflection/Reify                                                       | 0m00.39s  || +0m00.01s
0m00.40s  | ModularArithmetic/Pow2Base                                             | 0m00.42s  || -0m00.01s
0m00.40s  | Reflection/Named/EstablishLiveness                                     | 0m00.33s  || +0m00.07s
0m00.40s  | Reflection/ExprInversion                                               | 0m00.57s  || -0m00.16s
0m00.40s  | Reflection/Named/Syntax                                                | 0m00.40s  || +0m00.00s
0m00.38s  | Reflection/Named/Compile                                               | 0m00.34s  || +0m00.03s
   N/A    | Reflection/MapInterp                                                   | 0m00.38s  || -0m00.38s
0m00.38s  | ModularArithmetic/Montgomery/Z                                         | 0m00.39s  || -0m00.01s
0m00.38s  | ModularArithmetic/ModularBaseSystemWord                                | 0m00.36s  || +0m00.02s
   N/A    | Reflection/WfRel                                                       | 0m00.38s  || -0m00.38s
0m00.38s  | Reflection/Tuple                                                       |    N/A    || +0m00.38s
0m00.37s  | Spec/MxDH                                                              | 0m00.39s  || -0m00.02s
0m00.37s  | BoundedArithmetic/Eta                                                  | 0m00.36s  || +0m00.01s
0m00.36s  | Reflection/Named/ContextOn                                             | 0m00.37s  || -0m00.01s
0m00.34s  | Reflection/FilterLive                                                  | 0m00.34s  || +0m00.00s
0m00.34s  | Reflection/LinearizeInterp                                             | 0m00.53s  || -0m00.19s
0m00.33s  | Reflection/Relations                                                   |    N/A    || +0m00.33s
0m00.32s  | Reflection/Equality                                                    | 0m00.41s  || -0m00.08s
0m00.30s  | Reflection/Syntax                                                      | 0m00.52s  || -0m00.22s
0m00.30s  | Reflection/InterpProofs                                                | 0m00.47s  || -0m00.17s
0m00.30s  | Reflection/ApplicationLemmas                                           | 0m00.43s  || -0m00.13s
0m00.30s  | Reflection/CommonSubexpressionElimination                              | 0m00.50s  || -0m00.20s
0m00.28s  | Reflection/Inline                                                      | 0m00.37s  || -0m00.08s
0m00.28s  | Reflection/Conversion                                                  | 0m00.44s  || -0m00.15s
0m00.27s  | Reflection/MapCastWithCastOp                                           | 0m00.38s  || -0m00.10s
0m00.26s  | Reflection/MapCast                                                     | 0m00.40s  || -0m00.14s
0m00.26s  | Reflection/ApplicationRelations                                        | 0m00.35s  || -0m00.08s
0m00.24s  | Reflection/Application                                                 | 0m00.38s  || -0m00.14s
0m00.23s  | Reflection/Linearize                                                   | 0m00.35s  || -0m00.11s
0m00.20s  | Reflection/CountLets                                                   | 0m00.33s  || -0m00.13s
0m00.20s  | Reflection/Named/NameUtil                                              | 0m00.36s  || -0m00.15s
0m00.09s  | Util/PointedProp                                                       | 0m00.08s  || +0m00.00s
0m00.05s  | Util/LetIn                                                             | 0m00.06s  || -0m00.00s
0m00.03s  | Util/Notations                                                         | 0m00.03s  || +0m00.00s
0m00.03s  | Util/AutoRewrite                                                       | 0m00.03s  || +0m00.00s

1 files changed, 29 insertions, 29 deletions

diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v
index 8dbc8f4ce..da5749f87 100644
--- a/src/Reflection/MultiSizeTest2.v
+++ b/src/Reflection/MultiSizeTest2.v
@@ -3,7 +3,6 @@ Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Equality.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapCastWithCastOp.
-Require Import Crypto.Reflection.MapInterp.
 
 (** * Preliminaries: bounded and unbounded number types *)
 
@@ -32,9 +31,13 @@ Local Notation TNat := (Tbase Nat).
 Local Notation TWord8 := (Tbase Word8).
 Local Notation TWord9 := (Tbase Word9).
 Inductive op : flat_type base_type -> flat_type base_type -> Set :=
+| Const {t} (v : interp_base_type t) : op Unit (Tbase t)
 | Plus (t : base_type) : op (Tbase t * Tbase t) (Tbase t)
 | Cast (t1 t2 : base_type) : op (Tbase t1) (Tbase t2).
 
+Definition Constf {var} {t} (v : interp_base_type t) : exprf base_type op (var:=var) (Tbase t)
+  := Op (Const v) TT.
+
 Theorem O_lt_S : forall n, O < S n.
 Proof.
   intros; omega.
@@ -81,6 +84,7 @@ Definition bound {t} : nat -> interp_base_type t :=
 
 Definition interp_op {src dst} (opc : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst
   := match opc in op src dst return interp_flat_type _ src -> interp_flat_type _ dst with
+     | Const _ v => fun _ => v
      | Plus Nat => fun xy => fst xy + snd xy
      | Plus Word8 => fun xy => fst xy +8 snd xy
      | Plus Word9 => fun xy => fst xy +9 snd xy
@@ -89,6 +93,7 @@ Definition interp_op {src dst} (opc : op src dst) : interp_flat_type interp_base
 
 Definition interp_op_bounds {src dst} (opc : op src dst) : interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst
   := match opc in op src dst return interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst with
+     | Const _ v => fun _ => unbound v
      | Plus _ => fun xy => fst xy + snd xy
      | Cast t1 t2 => fun x => x
      end.
@@ -106,6 +111,8 @@ Definition failv t : interp_base_type t
      | Word8 => exist _ 0 (O_lt_S _)
      | Word9 => exist _ 0 (O_lt_S _)
      end.
+Definition failf var t : @exprf base_type op var (Tbase t)
+  := Op (Const (failv t)) TT.
 
 Definition bound_base_const t1 t2 (x1 : interp_base_type t1) (x2 : interp_base_type_bounds t2) : interp_base_type (bound_type _ x2)
   := bound (unbound x1).
@@ -114,51 +121,44 @@ Local Notation new_flat_type (*: forall t, interp_flat_type interp_base_type2 t
 Definition bound_op
            ovar src1 dst1 src2 dst2 (opc1 : op src1 dst1) (opc2 : op src2 dst2)
   : forall args2,
-    option { new_src : _ & (@exprf _ interp_base_type op ovar new_src
-                            -> @exprf _ interp_base_type op ovar (new_flat_type (interpf (@interp_op_bounds) (Op opc2 args2))))%type }
+    option { new_src : _ & (@exprf _ op ovar new_src
+                            -> @exprf _ op ovar (new_flat_type (interpf (@interp_op_bounds) (Op opc2 args2))))%type }
   := match opc1 in op src1 dst1, opc2 in op src2 dst2
            return (forall args2,
-                      option { new_src : _ & (exprf _ _ _ new_src -> exprf _ _ _ (new_flat_type (interpf (@interp_op_bounds) (Op opc2 args2))))%type })
+                      option { new_src : _ & (exprf _ _ new_src -> exprf _ _ (new_flat_type (interpf (@interp_op_bounds) (Op opc2 args2))))%type })
      with
+     | Const t1 v1, Const t2 v2
+       => fun args2 => Some (existT _ Unit (fun x => Op (Const (@bound_base_const t1 t2 v1 _)) TT))
      | Plus T1, Plus T2 => fun args2 => Some (existT _ _ (Op (Plus (bound_type T2 _))))
      | Cast _ _, Plus _
+     | Cast _ _, Const _ _
      | Cast _ _, Cast _ _
        => fun args2 => Some (existT _ _ (fun args' => args'))
      | Plus _, _
+     | Const _ _, _
        => fun _ => None
      end.
 
-Definition mapf_to_bounds_interp {var t1} (e1 : @exprf base_type interp_base_type op var t1)
-  : @exprf base_type interp_base_type_bounds op var t1
-  := mapf_interp (@unbound) e1.
-Definition map_to_bounds_interp {var t1} (e1 : @expr base_type interp_base_type op var t1)
-  : @expr base_type interp_base_type_bounds op var t1
-  := map_interp (@unbound) e1.
-Definition MapToBoundsInterp {t1} (e1 : @Expr base_type interp_base_type op t1)
-  : @Expr base_type interp_base_type_bounds op t1
-  := fun var => map_to_bounds_interp (e1 _).
-
-Definition Boundify {t1} (e1 : Expr base_type interp_base_type op t1) args2
-  : Expr _ _ _ _
-  := fun ovar
-     => @map_interp_cast_with_cast_op
-          base_type base_type interp_base_type interp_base_type_bounds
-          op op (@interp_op_bounds) base_type_beq internal_base_type_dec_bl
-          (@failv) (@bound_type) bound_base_const
-          (fun var t1 t2 => Op (Cast t1 t2))
-          (fun _ _ opc => match opc with Cast _ _ => true | _ => false end)
-          bound_op ovar
-          t1 (e1 _) t1 (MapToBoundsInterp e1 _) (interp_all_binders_for_to' args2).
+Definition Boundify {t1} (e1 : Expr base_type op t1) args2
+  : Expr _ _ _
+  := @MapInterpCastWithCastOp
+       base_type interp_base_type_bounds
+       op (@interp_op_bounds) base_type_beq internal_base_type_dec_bl
+       (@failf) (@bound_type)
+       (fun var t1 t2 => Op (Cast t1 t2))
+       (fun _ _ opc => match opc with Cast _ _ => true | _ => false end)
+       bound_op
+       t1 e1 (interp_all_binders_for_to' args2).
 
 (** * Examples *)
 
-Example ex1 : Expr base_type interp_base_type op TNat := fun var =>
-  LetIn (Const (t:=TNat) 127) (fun a : var Nat =>
-  LetIn (Const (t:=TNat) 63) (fun b : var Nat =>
+Example ex1 : Expr base_type op TNat := fun var =>
+  LetIn (Constf (t:=Nat) 127) (fun a : var Nat =>
+  LetIn (Constf (t:=Nat) 63) (fun b : var Nat =>
   LetIn (Op (tR:=TNat) (Plus Nat) (Pair (Var a) (Var b))) (fun c : var Nat =>
   Op (Plus Nat) (Pair (Var c) (Var c))))).
 
-Example ex1f : Expr base_type interp_base_type op (Arrow Nat (Arrow Nat TNat)) := fun var =>
+Example ex1f : Expr base_type op (Arrow Nat (Arrow Nat TNat)) := fun var =>
   Abs (fun a0 =>
   Abs (fun b0 =>
   LetIn (Var a0) (fun a : var Nat =>