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, 46 insertions, 45 deletions

diff --git a/src/Reflection/MapCast.v b/src/Reflection/MapCast.v
index a557aec1c..758b016f8 100644
--- a/src/Reflection/MapCast.v
+++ b/src/Reflection/MapCast.v
@@ -8,15 +8,12 @@ Local Open Scope ctype_scope.
 Local Open Scope expr_scope.
 Section language.
   Context {base_type_code1 base_type_code2 : Type}
-          {interp_base_type1 : base_type_code1 -> Type}
           {interp_base_type2 : base_type_code2 -> Type}
           {op1 : flat_type base_type_code1 -> flat_type base_type_code1 -> Type}
           {op2 : flat_type base_type_code2 -> flat_type base_type_code2 -> Type}
           (interp_op2 : forall src dst, op2 src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst)
-          (failv : forall {t}, interp_base_type1 t)
-          (new_base_type : forall t, interp_base_type2 t -> base_type_code1)
-          (transfer_base_const : forall t1 t2 (x1 : interp_base_type1 t1) (x2 : interp_base_type2 t2),
-              interp_base_type1 (new_base_type t2 x2)).
+          (failv : forall {var t}, @exprf base_type_code1 op1 var (Tbase t))
+          (new_base_type : forall t, interp_base_type2 t -> base_type_code1).
   Local Notation new_flat_type (*: forall t, interp_flat_type interp_base_type2 t -> flat_type base_type_code1*)
     := (@SmartFlatTypeMap2 _ _ interp_base_type2 (fun t v => Tbase (new_base_type t v))).
   Fixpoint new_type t
@@ -30,53 +27,36 @@ Section language.
                                 (opc1 : op1 src1 dst1)
                                 (opc2 : op2 src2 dst2)
                                 args2
-                                (args' : @exprf base_type_code1 interp_base_type1 op1 ovar (@new_flat_type _ (interpf interp_op2 args2))),
-              @exprf base_type_code1 interp_base_type1 op1 ovar (@new_flat_type _ (interpf interp_op2 (Op opc2 args2)))).
+                                (args' : @exprf base_type_code1 op1 ovar (@new_flat_type _ (interpf interp_op2 args2))),
+              @exprf base_type_code1 op1 ovar (@new_flat_type _ (interpf interp_op2 (Op opc2 args2)))).
 
 
   Section with_var.
     Context {ovar : base_type_code1 -> Type}.
-    Local Notation ivar t := (@exprf base_type_code1 interp_base_type1 op1 ovar (Tbase t)) (only parsing).
+    Local Notation ivar t := (@exprf base_type_code1 op1 ovar (Tbase t)) (only parsing).
     Local Notation ivarf := (fun t => ivar t).
     Context (transfer_var : forall tx1 tx2 tC1
-                                   (f : interp_flat_type ivarf tx1 -> exprf base_type_code1 interp_base_type1 op1 (var:=ovar) tC1)
+                                   (f : interp_flat_type ivarf tx1 -> exprf base_type_code1 op1 (var:=ovar) tC1)
                                    (v : interp_flat_type ivarf tx2),
-                exprf base_type_code1 interp_base_type1 op1 (var:=ovar) tC1).
+                exprf base_type_code1 op1 (var:=ovar) tC1).
     Local Notation SmartFail
-      := (SmartValf _ (@failv)).
-    Local Notation failf t (*{t} : @exprf base_type_code1 interp_base_type1 op1 ovar t*)
-      := (Const (SmartFail t)).
-    Fixpoint fail t : @expr base_type_code1 interp_base_type1 op1 ovar t
+      := (SmartValf _ (@failv _)).
+    Local Notation failf t (* {t} : @exprf base_type_code1 op1 ovar t*)
+      := (SmartPairf (SmartFail t)).
+    Fixpoint fail t : @expr base_type_code1 op1 ovar t
       := match t with
          | Tflat T => @failf _
          | Arrow A B => Abs (fun _ => @fail B)
          end.
-    Fixpoint mapf_interp_cast_const
-             {tx1 tx2}
-             {struct tx1}
-      : forall (x1 : interp_flat_type interp_base_type1 tx1)
-               (x2 : interp_flat_type interp_base_type2 tx2),
-        interp_flat_type interp_base_type1 (new_flat_type x2)
-      := match tx1, tx2 return forall (x1 : interp_flat_type _ tx1) (x2 : interp_flat_type _ tx2), interp_flat_type interp_base_type1 (new_flat_type x2) with
-         | Tbase T1, Tbase T2 => transfer_base_const T1 T2
-         | Prod A1 B1, Prod A2 B2
-           => fun x1 x2
-              => (@mapf_interp_cast_const _ _ (fst x1) (fst x2),
-                  @mapf_interp_cast_const _ _ (snd x1) (snd x2))%core
-         | Tbase _, _
-         | Prod _ _, _
-           => fun _ _ => SmartFail _
-         end.
 
     Fixpoint mapf_interp_cast
-             {t1} (e1 : @exprf base_type_code1 interp_base_type1 op1 ivarf t1)
-             {t2} (e2 : @exprf base_type_code2 interp_base_type2 op2 interp_base_type2 t2)
+             {t1} (e1 : @exprf base_type_code1 op1 ivarf t1)
+             {t2} (e2 : @exprf base_type_code2 op2 interp_base_type2 t2)
              {struct e1}
-      : @exprf base_type_code1 interp_base_type1 op1 ovar (@new_flat_type _ (interpf interp_op2 e2))
-      := match e1 in exprf _ _ _ t1, e2 as e2 in exprf _ _ _ t2
-               return exprf _ _ _ (var:=ovar) (@new_flat_type _ (interpf interp_op2 e2)) with
-         | Const tx1 x1, Const tx2 x2 as e2'
-           => Const (mapf_interp_cast_const x1 x2)
+      : @exprf base_type_code1 op1 ovar (@new_flat_type _ (interpf interp_op2 e2))
+      := match e1 in exprf _ _ t1, e2 as e2 in exprf _ _ t2
+               return exprf _ _ (var:=ovar) (@new_flat_type _ (interpf interp_op2 e2)) with
+         | TT, TT => TT
          | Var tx1 x1, Var tx2 x2 as e2'
            => transfer_var (Tbase _) (Tbase _) (Tbase _) (fun x => x) x1
          | Op _ tR1 op1 args1, Op _ tR2 op2 args2
@@ -91,7 +71,7 @@ Section language.
            => Pair
                 (@mapf_interp_cast _ ex1 _ ex2)
                 (@mapf_interp_cast _ ey1 _ ey2)
-         | Const _ _, _
+         | TT, _
          | Var _ _, _
          | Op _ _ _ _, _
          | LetIn _ _ _ _, _
@@ -101,13 +81,13 @@ Section language.
     Arguments mapf_interp_cast {_} _ {_} _. (* 8.4 workaround for bad arguments *)
 
     Fixpoint map_interp_cast
-             {t1} (e1 : @expr base_type_code1 interp_base_type1 op1 ivarf t1)
-             {t2} (e2 : @expr base_type_code2 interp_base_type2 op2 interp_base_type2 t2)
+             {t1} (e1 : @expr base_type_code1 op1 ivarf t1)
+             {t2} (e2 : @expr base_type_code2 op2 interp_base_type2 t2)
              {struct e2}
       : forall (args2 : interp_all_binders_for' t2 interp_base_type2),
-        @expr base_type_code1 interp_base_type1 op1 ovar (@new_type _ args2 (interp interp_op2 e2))
-      := match e1 in expr _ _ _ t1, e2 in expr _ _ _ t2
-               return forall (args2 : interp_all_binders_for' t2 _), expr _ _ _ (new_type _ args2 (interp _ e2)) with
+        @expr base_type_code1 op1 ovar (@new_type _ args2 (interp interp_op2 e2))
+      := match e1 in expr _ _ t1, e2 in expr _ _ t2
+               return forall (args2 : interp_all_binders_for' t2 _), expr _ _ (new_type _ args2 (interp _ e2)) with
          | Return t1 ex1, Return t2 ex2
            => fun _ => mapf_interp_cast ex1 ex2
          | Abs src1 dst1 f1, Abs src2 dst2 f2
@@ -122,5 +102,26 @@ Section language.
   End with_var.
 End language.
 
-Global Arguments mapf_interp_cast {_ _ _ _ _ _ _} failv {_} transfer_base_const transfer_op {ovar} transfer_var {t1} e1 {t2} e2.
-Global Arguments map_interp_cast {_ _ _ _ _ _ _} failv {_} transfer_base_const transfer_op {ovar} transfer_var {t1} e1 {t2} e2 args2.
+Global Arguments mapf_interp_cast {_ _ _ _ _ _} failv {_} transfer_op {ovar} transfer_var {t1} e1 {t2} e2.
+Global Arguments map_interp_cast {_ _ _ _ _ _} failv {_} transfer_op {ovar} transfer_var {t1} e1 {t2} e2 args2.
+Global Arguments new_type {_ _ _} new_base_type {t} _ _.
+
+Section homogenous.
+  Context {base_type_code : Type}
+          {interp_base_type2 : base_type_code -> Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          (interp_op2 : forall src dst, op src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst)
+          (failv : forall {var t}, @exprf base_type_code op var (Tbase t))
+          (new_base_type : forall t, interp_base_type2 t -> base_type_code).
+
+  Definition MapInterpCast
+          transfer_op
+          (transfer_var : forall ovar tx1 tx2 tC1
+                                 (ivarf := fun t => @exprf base_type_code op ovar (Tbase t))
+                                 (f : interp_flat_type ivarf tx1 -> exprf base_type_code op (var:=ovar) tC1)
+                                 (v : interp_flat_type ivarf tx2),
+              exprf base_type_code op (var:=ovar) tC1)
+          {t} (e : Expr base_type_code op t) args
+    : Expr base_type_code op (new_type (@new_base_type) args (Interp interp_op2 e))
+    := fun var => map_interp_cast (@failv) transfer_op (transfer_var _) (e _) (e _) args.
+End homogenous.