diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-19 19:35:24 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-19 19:35:24 -0500 |
commit | fa027c4a37ed455a26a5bb12c6f3d54ae4bd8774 (patch) | |
tree | 4e6d08d6d36595a068f3facf2c70f540bae0e8b1 /src/Reflection | |
parent | 320c013f0c5550aed168dd7fd25274dbb9756590 (diff) |
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
Diffstat (limited to 'src/Reflection')
47 files changed, 1191 insertions, 1430 deletions
diff --git a/src/Reflection/Application.v b/src/Reflection/Application.v index 59e00ef1d..878af9c3f 100644 --- a/src/Reflection/Application.v +++ b/src/Reflection/Application.v @@ -112,29 +112,29 @@ Section language. | Arrow _ _ => fun x => snd x end args. - Fixpoint Apply' n {var t} (x : @expr base_type interp_base_type op var t) + Fixpoint Apply' n {var t} (x : @expr base_type op var t) : forall (args : binders_for' n t var), - @expr base_type interp_base_type op var (remove_binders' n t) - := match x in (@expr _ _ _ _ t), n return (binders_for' n t var -> @expr _ _ _ _ (remove_binders' n t)) with + @expr base_type op var (remove_binders' n t) + := match x in (@expr _ _ _ t), n return (binders_for' n t var -> @expr _ _ _ (remove_binders' n t)) with | Return _ _ as y, _ => fun _ => y | Abs _ _ f, 0 => f | Abs src dst f, S n' => fun args => @Apply' n' var dst (f (fst args)) (snd args) end. - Definition Apply n {var t} (x : @expr base_type interp_base_type op var t) + Definition Apply n {var t} (x : @expr base_type op var t) : forall (args : binders_for n t var), - @expr base_type interp_base_type op var (remove_binders n t) - := match n return binders_for n t var -> @expr _ _ _ _ (remove_binders n t) with + @expr base_type op var (remove_binders n t) + := match n return binders_for n t var -> @expr _ _ _ (remove_binders n t) with | 0 => fun _ => x | S n' => @Apply' n' var t x end. - Fixpoint ApplyAll {var t} (x : @expr base_type interp_base_type op var t) + Fixpoint ApplyAll {var t} (x : @expr base_type op var t) : forall (args : interp_all_binders_for t var), - @exprf base_type interp_base_type op var (remove_all_binders t) - := match x in @expr _ _ _ _ t + @exprf base_type op var (remove_all_binders t) + := match x in @expr _ _ _ t return (forall (args : interp_all_binders_for t var), - @exprf base_type interp_base_type op var (remove_all_binders t)) + @exprf base_type op var (remove_all_binders t)) with | Return _ x => fun _ => x | Abs src dst f => fun args => @ApplyAll var dst (f (fst_binder args)) (snd_binder args) @@ -187,10 +187,10 @@ Arguments count_binders {_} !_ / . Arguments binders_for {_} !_ !_ _ / . Arguments remove_binders {_} !_ !_ / . (* Work around bug #5175 *) -Arguments Apply {_ _ _ _ _ _} _ _ , {_ _ _} _ {_ _} _ _. -Arguments Apply _ _ _ !_ _ _ !_ !_ / . +Arguments Apply {_ _ _ _ _} _ _ , {_ _} _ {_ _} _ _. +Arguments Apply _ _ !_ _ _ !_ !_ / . Arguments ApplyInterped {_ _ !_ !_} _ _ / . Arguments ApplyInterped' {_ _} _ {_} _ _. -Arguments ApplyAll {_ _ _ _ !_} !_ _ / . +Arguments ApplyAll {_ _ _ !_} !_ _ / . Arguments ApplyInterpedAll' {_ _ !_} _ _ / . Arguments ApplyInterpedAll {_ _ !_} _ _ / . diff --git a/src/Reflection/ApplicationLemmas.v b/src/Reflection/ApplicationLemmas.v index f39e03776..e8105c2f0 100644 --- a/src/Reflection/ApplicationLemmas.v +++ b/src/Reflection/ApplicationLemmas.v @@ -8,7 +8,7 @@ Section language. {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}. Lemma interp_apply' {n t} - (x : @expr base_type interp_base_type op _ t) + (x : @expr base_type op _ t) (args : binders_for' n t interp_base_type) : interp interp_op (Apply' n x args) = ApplyInterped' n (interp interp_op x) args. Proof. @@ -19,7 +19,7 @@ Section language. Qed. Lemma interp_apply {n t} - (x : @expr base_type interp_base_type op _ t) + (x : @expr base_type op _ t) (args : binders_for n t interp_base_type) : interp interp_op (Apply n x args) = ApplyInterped (interp interp_op x) args. Proof. @@ -76,7 +76,7 @@ Section language. Qed. Lemma interp_apply_all' {t} - (x : @expr base_type interp_base_type op _ t) + (x : @expr base_type op _ t) (args : interp_all_binders_for' t interp_base_type) : interp interp_op (ApplyAll x (interp_all_binders_for_of' args)) = ApplyInterpedAll' (interp interp_op x) args. Proof. @@ -86,7 +86,7 @@ Section language. Qed. Lemma interp_apply_all {t} - (x : @expr base_type interp_base_type op _ t) + (x : @expr base_type op _ t) (args : interp_all_binders_for t interp_base_type) : interp interp_op (ApplyAll x args) = ApplyInterpedAll (interp interp_op x) args. Proof. @@ -95,7 +95,7 @@ Section language. Qed. Lemma interp_apply_all_to' {t} - (x : @expr base_type interp_base_type op _ t) + (x : @expr base_type op _ t) (args : interp_all_binders_for t interp_base_type) : interp interp_op (ApplyAll x args) = ApplyInterpedAll' (interp interp_op x) (interp_all_binders_for_to' args). Proof. diff --git a/src/Reflection/CommonSubexpressionElimination.v b/src/Reflection/CommonSubexpressionElimination.v index cf5f66fc7..bb4a2d763 100644 --- a/src/Reflection/CommonSubexpressionElimination.v +++ b/src/Reflection/CommonSubexpressionElimination.v @@ -5,8 +5,8 @@ Require Import Crypto.Util.Tactics Crypto.Util.Bool. Local Open Scope list_scope. -Inductive symbolic_expr {base_type_code SConstT op_code} : Type := -| SConst (v : SConstT) +Inductive symbolic_expr {base_type_code op_code} : Type := +| STT | SVar (v : base_type_code) (n : nat) | SOp (op : op_code) (args : symbolic_expr) | SPair (x y : symbolic_expr) @@ -17,7 +17,6 @@ Arguments symbolic_expr : clear implicits. Ltac inversion_symbolic_expr_step := match goal with - | [ H : SConst _ = SConst _ |- _ ] => inversion H; clear H | [ H : SVar _ _ = SVar _ _ |- _ ] => inversion H; clear H | [ H : SOp _ _ = SOp _ _ |- _ ] => inversion H; clear H | [ H : SPair _ _ = SPair _ _ |- _ ] => inversion H; clear H @@ -28,37 +27,30 @@ Local Open Scope ctype_scope. Section symbolic. (** Holds decidably-equal versions of raw expressions, for lookup. *) Context (base_type_code : Type) - (SConstT : Type) (op_code : Type) (base_type_code_beq : base_type_code -> base_type_code -> bool) - (SConstT_beq : SConstT -> SConstT -> 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) - (SConstT_bl : forall x y, SConstT_beq x y = true -> x = y) - (SConstT_lb : forall x y, x = y -> SConstT_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) (interp_base_type : base_type_code -> Type) (op : flat_type base_type_code -> flat_type base_type_code -> Type) - (symbolize_const : forall t, interp_base_type t -> SConstT) (symbolize_op : forall s d, op s d -> op_code). - Local Notation symbolic_expr := (symbolic_expr base_type_code SConstT op_code). - Local Notation symbolic_expr_beq := (@symbolic_expr_beq base_type_code SConstT op_code base_type_code_beq SConstT_beq op_code_beq). - Local Notation symbolic_expr_lb := (@internal_symbolic_expr_dec_lb base_type_code SConstT op_code base_type_code_beq SConstT_beq op_code_beq base_type_code_lb SConstT_lb op_code_lb). - Local Notation symbolic_expr_bl := (@internal_symbolic_expr_dec_bl base_type_code SConstT op_code base_type_code_beq SConstT_beq op_code_beq base_type_code_bl SConstT_bl op_code_bl). + 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). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. Local Notation interp_type := (interp_type interp_base_type). Local Notation interp_flat_type_gen := interp_flat_type. Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - Local Notation Expr := (@Expr base_type_code interp_base_type op). + 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. @@ -96,14 +88,11 @@ Section symbolic. Definition add_mapping {t} (v : var t) (sv : symbolic_expr) (xs : mapping) : mapping := mapping_update_type t xs (fun ls => (v, sv) :: ls). - Definition symbolize_smart_const {t} : interp_flat_type t -> symbolic_expr - := smart_interp_flat_map base_type_code (g:=fun _ => symbolic_expr) (fun t v => SConst (symbolize_const t v)) (fun A B => SPair). - Fixpoint symbolize_exprf {t} (v : @exprf fsvar t) {struct v} : option symbolic_expr := match v with - | Const t x => Some (symbolize_smart_const x) + | TT => Some STT | Var _ x => Some (snd x) | Op _ _ op args => option_map (fun sargs => SOp (symbolize_op _ _ op) sargs) @@ -119,7 +108,8 @@ Section symbolic. (t : flat_type) (sv : symbolic_expr) (xs : mapping) {struct t} : option (interp_flat_type_gen f t) := match t return option (interp_flat_type_gen f t) with - | Syntax.Tbase t => option_map (fun v => proj t (v, sv)) (lookup t sv xs) + | Tbase t => option_map (fun v => proj t (v, sv)) (lookup t sv xs) + | Unit => Some tt | Prod A B => match @smart_lookup_gen f proj A sv xs, @smart_lookup_gen f proj B sv xs with | Some a, Some b => Some (a, b) | _, _ => None @@ -141,10 +131,12 @@ Section symbolic. | Some sv => sv | None => symbolicify_var v xs end)) + tt (fun A B => @pair _ _). Fixpoint smart_add_mapping {t : flat_type} (xs : mapping) : interp_flat_type_gen fsvar t -> mapping := match t return interp_flat_type_gen fsvar t -> mapping with - | Syntax.Tbase t => fun v => add_mapping (fst v) (snd v) xs + | Tbase t => fun v => add_mapping (fst v) (snd v) xs + | Unit => fun _ => xs | Prod A B => fun v => let xs := @smart_add_mapping B xs (snd v) in let xs := @smart_add_mapping A xs (fst v) in @@ -155,7 +147,7 @@ Section symbolic. (csef : forall {t} (v : @exprf fsvar t) (xs : mapping), @exprf var t) {t} (v : @exprf fsvar t) (xs : mapping) : @exprf var t - := match v in @Syntax.exprf _ _ _ _ t return exprf t with + := match v in @Syntax.exprf _ _ _ t return exprf t with | LetIn tx ex _ eC => let sx := symbolize_exprf ex in let ex' := @csef _ ex xs in let sv := smart_lookupo tx sx xs in @@ -165,7 +157,7 @@ Section symbolic. => LetIn ex' (fun x => let x' := symbolicify_smart_var xs sx x in @csef _ (eC x') (smart_add_mapping xs x')) end - | Const _ x => Const x + | TT => TT | Var _ x => Var (fst x) | Op _ _ op args => Op op (@csef _ args xs) | Pair _ ex _ ey => Pair (@csef _ ex xs) (@csef _ ey xs) @@ -182,7 +174,7 @@ Section symbolic. end. Fixpoint cse {t} (v : @expr fsvar t) (xs : mapping) {struct v} : @expr var t - := match v in @Syntax.expr _ _ _ _ t return expr t with + := match v in @Syntax.expr _ _ _ t return expr t with | Return _ x => Return (csef (prepend_prefix x prefix) xs) | Abs _ _ f => Abs (fun x => let x' := symbolicify_var x xs in @cse _ (f (x, x')) (add_mapping x x' xs)) @@ -194,6 +186,6 @@ Section symbolic. := fun var => cse (prefix _) (e _) empty_mapping. End symbolic. -Global Arguments csef {_} SConstT op_code base_type_code_beq SConstT_beq op_code_beq base_type_code_bl {_ _} symbolize_const symbolize_op {var t} _ _. -Global Arguments cse {_} SConstT op_code base_type_code_beq SConstT_beq op_code_beq base_type_code_bl {_ _} symbolize_const symbolize_op {var} prefix {t} _ _. -Global Arguments CSE {_} SConstT op_code base_type_code_beq SConstT_beq op_code_beq base_type_code_bl {_ _} symbolize_const symbolize_op {t} e prefix var. +Global Arguments csef {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op {var t} _ _. +Global Arguments cse {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op {var} prefix {t} _ _. +Global Arguments CSE {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op {t} e prefix var. diff --git a/src/Reflection/Conversion.v b/src/Reflection/Conversion.v index b1add2222..f06b7e5b9 100644 --- a/src/Reflection/Conversion.v +++ b/src/Reflection/Conversion.v @@ -8,18 +8,16 @@ Section language. Context (base_type_code : Type). Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). Section map. - Context (interp_base_type1 interp_base_type2 : base_type_code -> Type). - Context (f_const : forall t, interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t). Context {var1 var2 : base_type_code -> Type}. Context (f_var12 : forall t, var1 t -> var2 t) (f_var21 : forall t, var2 t -> var1 t). Fixpoint mapf {t} - (e : @exprf base_type_code interp_base_type1 op var1 t) - : @exprf base_type_code interp_base_type2 op var2 t - := match e in @exprf _ _ _ _ t return @exprf _ _ _ _ t with - | Const _ x => Const (f_const _ x) + (e : @exprf base_type_code op var1 t) + : @exprf base_type_code op var2 t + := match e in @exprf _ _ _ t return @exprf _ _ _ t with + | TT => TT | Var _ x => Var (f_var12 _ x) | Op _ _ op args => Op op (@mapf _ args) | LetIn _ ex _ eC => LetIn (@mapf _ ex) @@ -28,8 +26,8 @@ Section language. (@mapf _ ey) end. - Fixpoint map {t} (e : @expr base_type_code interp_base_type1 op var1 t) - : @expr base_type_code interp_base_type2 op var2 t + Fixpoint map {t} (e : @expr base_type_code op var1 t) + : @expr base_type_code op var2 t := match e with | Return _ x => Return (mapf x) | Abs _ _ f => Abs (fun x => @map _ (f (f_var21 _ x))) @@ -38,13 +36,10 @@ Section language. Section mapf_id. Context (functional_extensionality : forall {A B} (f g : A -> B), (forall x, f x = g x) -> f = g) - {interp_base_type : base_type_code -> Type} {var : base_type_code -> Type}. Lemma mapf_idmap_ext {t} e - : @mapf interp_base_type interp_base_type - (fun _ x => x) - var var + : @mapf var var (fun _ x => x) (fun _ x => x) t e = e. @@ -59,7 +54,7 @@ Section language. | _ => apply functional_extensionality; intro end. clear e IHe H. - revert dependent tC; induction tx; simpl; [ reflexivity | ]; intros. + revert dependent tC; induction tx; simpl; [ reflexivity | reflexivity | ]; intros. destruct x as [x0 x1]; simpl in *. lazymatch goal with | [ |- ?e0 (?x0', ?x1')%core = _ ] @@ -76,17 +71,13 @@ Section language. Section mapf_id_interp. Context {interp_base_type : base_type_code -> Type} (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst) - (f_const : forall t, interp_flat_type interp_base_type t -> interp_flat_type interp_base_type t) (f_var12 f_var21 : forall t, interp_base_type t -> interp_base_type t) - (f_const_id : forall t x, f_const t x = x) (f_var12_id : forall t x, f_var12 t x = x) (f_var21_id : forall t x, f_var21 t x = x). Lemma mapf_idmap {t} e : interpf interp_op - (@mapf interp_base_type interp_base_type - f_const - _ _ + (@mapf _ _ f_var12 f_var21 t e) = interpf interp_op e. @@ -103,7 +94,7 @@ Section language. clear H IHe. generalize (interpf interp_op e); intro x; clear e. revert dependent tC; induction tx; simpl; - [ intros; rewrite_hyp ?*; reflexivity | ]; intros. + [ intros; rewrite_hyp ?*; reflexivity | reflexivity | ]; intros. destruct x as [x0 x1]; simpl in *. lazymatch goal with | [ |- interpf _ (?e0 (?x0', ?x1')%core) = _ ] diff --git a/src/Reflection/CountLets.v b/src/Reflection/CountLets.v index 8de6e7a2f..85b6e3ad7 100644 --- a/src/Reflection/CountLets.v +++ b/src/Reflection/CountLets.v @@ -4,18 +4,16 @@ Require Import Crypto.Reflection.Syntax. Local Open Scope ctype_scope. Section language. Context {base_type_code : Type} - {interp_base_type : 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 interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation Expr := (@Expr base_type_code interp_base_type op). + Local Notation Expr := (@Expr base_type_code op). Fixpoint count_pairs (t : flat_type) : nat := match t with | Tbase _ => 1 + | Unit => 0 | Prod A B => count_pairs A + count_pairs B end%nat. @@ -23,8 +21,8 @@ Section language. Context {var : base_type_code -> Type} (mkVar : forall t, var t). - Local Notation exprf := (@exprf base_type_code interp_base_type op var). - Local Notation expr := (@expr base_type_code interp_base_type op var). + Local Notation exprf := (@exprf base_type_code op var). + Local Notation expr := (@expr base_type_code op var). Section gen. Context (count_type_let : flat_type -> nat). diff --git a/src/Reflection/Equality.v b/src/Reflection/Equality.v index d6b7b24fc..ddd9a3f6a 100644 --- a/src/Reflection/Equality.v +++ b/src/Reflection/Equality.v @@ -14,9 +14,11 @@ Section language. Fixpoint flat_type_beq (X Y : flat_type) {struct X} : bool := match X, Y with | Tbase T, Tbase T0 => eq_base_type_code T T0 + | Unit, Unit => true | Prod A B, Prod A0 B0 => (flat_type_beq A A0 && flat_type_beq B B0)%bool | Tbase _, _ | Prod _ _, _ + | Unit, _ => false end. Local Ltac t := diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v index 06a4f5b30..c403ed5e6 100644 --- a/src/Reflection/ExprInversion.v +++ b/src/Reflection/ExprInversion.v @@ -8,91 +8,132 @@ Require Import Crypto.Util.Notations. Section language. Context {base_type_code : Type} {interp_base_type : base_type_code -> Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - {var : 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 Tbase := (@Tbase base_type_code). Local Notation interp_type := (interp_type interp_base_type). + Local Notation interp_flat_type_gen := interp_flat_type. Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op var). - Local Notation expr := (@expr base_type_code interp_base_type op var). - Local Notation Expr := (@Expr base_type_code interp_base_type op). + Local Notation Expr := (@Expr base_type_code op). - Definition invert_Const {t} (e : exprf t) : option (interp_type t) - := match e with Const _ v => Some v | _ => None end. - Definition invert_Var {t} (e : exprf (Tbase t)) : option (var t) - := match e in Syntax.exprf _ _ _ t' - return option (var match t' with - | Syntax.Tbase t' => t' - | _ => t - end) - with - | Var _ v => Some v - | _ => None - end. - Definition invert_Op {t} (e : exprf t) : option { t1 : flat_type & op t1 t * exprf t1 }%type - := match e with Op _ _ opc args => Some (existT _ _ (opc, args)) | _ => None end. - Definition invert_LetIn {A} (e : exprf A) : option { B : _ & exprf B * (Syntax.interp_flat_type var B -> exprf A) }%type - := match e in Syntax.exprf _ _ _ t return option { B : _ & _ * (_ -> exprf t) }%type with - | LetIn _ ex _ eC => Some (existT _ _ (ex, eC)) - | _ => None - end. - Definition invert_Pair {A B} (e : exprf (Prod A B)) : option (exprf A * exprf B) - := match e in Syntax.exprf _ _ _ t - return option match t with - | Prod _ _ => _ - | _ => unit - end with - | Pair _ x _ y => Some (x, y)%core - | _ => None + Fixpoint codomain (t : type) : flat_type + := match t with + | Tflat T => T + | Arrow src dst => codomain dst end. - Local Ltac t' := - repeat first [ intro - | progress simpl in * - | reflexivity - | assumption - | progress destruct_head False - | progress subst - | progress inversion_option - | progress inversion_sigma - | progress break_match ]. - Local Ltac t := - lazymatch goal with - | [ |- _ = Some ?v -> ?e = _ ] - => revert v; - refine match e with - | Const _ _ => _ - | _ => _ - end - end; - t'. + Section with_var. + Context {var : base_type_code -> Type}. + + Local Notation exprf := (@exprf base_type_code op var). + Local Notation expr := (@expr base_type_code op var). + + Definition invert_Var {t} (e : exprf (Tbase t)) : option (var t) + := match e in Syntax.exprf _ _ t' + return option (var match t' with + | Tbase t' => t' + | _ => t + end) + with + | Var _ v => Some v + | _ => None + end. + Definition invert_Op {t} (e : exprf t) : option { t1 : flat_type & op t1 t * exprf t1 }%type + := match e with Op _ _ opc args => Some (existT _ _ (opc, args)) | _ => None end. + Definition invert_LetIn {A} (e : exprf A) : option { B : _ & exprf B * (Syntax.interp_flat_type var B -> exprf A) }%type + := match e in Syntax.exprf _ _ t return option { B : _ & _ * (_ -> exprf t) }%type with + | LetIn _ ex _ eC => Some (existT _ _ (ex, eC)) + | _ => None + end. + Definition invert_Pair {A B} (e : exprf (Prod A B)) : option (exprf A * exprf B) + := match e in Syntax.exprf _ _ t + return option match t with + | Prod _ _ => _ + | _ => unit + end with + | Pair _ x _ y => Some (x, y)%core + | _ => None + end. + Definition invert_Abs {A B} (e : expr (Arrow A B)) : var A -> expr B + := match e with Abs _ _ f => f end. + Definition invert_Return {t} (e : expr (Tflat t)) : exprf t + := match e with Return _ v => v end. + + Local Ltac t' := + repeat first [ intro + | progress simpl in * + | reflexivity + | assumption + | progress destruct_head False + | progress subst + | progress inversion_option + | progress inversion_sigma + | progress break_match ]. + Local Ltac t := + lazymatch goal with + | [ |- _ = Some ?v -> ?e = _ ] + => revert v; + refine match e with + | Var _ _ => _ + | _ => _ + end + | [ |- _ = ?v -> ?e = _ ] + => revert v; + refine match e with + | Abs _ _ _ => _ + | Return _ _ => _ + end + end; + t'. + + Lemma invert_Var_Some {t e v} + : @invert_Var t e = Some v -> e = Var v. + Proof. t. Defined. + + Lemma invert_Op_Some {t e v} + : @invert_Op t e = Some v -> e = Op (fst (projT2 v)) (snd (projT2 v)). + Proof. t. Defined. - Lemma invert_Const_Some {t e v} - : @invert_Const t e = Some v -> e = Const v. - Proof. t. Defined. + Lemma invert_LetIn_Some {t e v} + : @invert_LetIn t e = Some v -> e = LetIn (fst (projT2 v)) (snd (projT2 v)). + Proof. t. Defined. - Lemma invert_Var_Some {t e v} - : @invert_Var t e = Some v -> e = Var v. - Proof. t. Defined. + Lemma invert_Pair_Some {A B e v} + : @invert_Pair A B e = Some v -> e = Pair (fst v) (snd v). + Proof. t. Defined. - Lemma invert_Op_Some {t e v} - : @invert_Op t e = Some v -> e = Op (fst (projT2 v)) (snd (projT2 v)). - Proof. t. Defined. + Lemma invert_Abs_Some {A B e v} + : @invert_Abs A B e = v -> e = Abs v. + Proof. t. Defined. - Lemma invert_LetIn_Some {t e v} - : @invert_LetIn t e = Some v -> e = LetIn (fst (projT2 v)) (snd (projT2 v)). - Proof. t. Defined. + Lemma invert_Return_Some {t e v} + : @invert_Return t e = v -> e = Return v. + Proof. t. Qed. + End with_var. - Lemma invert_Pair_Some {A B e v} - : @invert_Pair A B e = Some v -> e = Pair (fst v) (snd v). - Proof. t. Defined. + Lemma interpf_invert_Abs interp_op {A B e} x + : Syntax.interp interp_op (@invert_Abs interp_base_type A B e x) + = Syntax.interp interp_op e x. + Proof. + refine (match e in expr _ _ t + return match t return expr _ _ t -> _ with + | Arrow src dst + => fun e + => (forall x : interp_base_type src, + interp _ (invert_Abs e x) = interp _ e x) + | Tflat _ => fun _ => True + end e with + | Abs _ _ _ => fun _ => eq_refl + | Return _ _ => I + end x). + Qed. End language. -Global Arguments invert_Const {_ _ _ _ _} _. -Global Arguments invert_Var {_ _ _ _ _} _. -Global Arguments invert_Op {_ _ _ _ _} _. -Global Arguments invert_LetIn {_ _ _ _ _} _. -Global Arguments invert_Pair {_ _ _ _ _ _} _. +Global Arguments codomain {_} _. +Global Arguments invert_Var {_ _ _ _} _. +Global Arguments invert_Op {_ _ _ _} _. +Global Arguments invert_LetIn {_ _ _ _} _. +Global Arguments invert_Pair {_ _ _ _ _} _. +Global Arguments invert_Abs {_ _ _ _ _} _ _. +Global Arguments invert_Return {_ _ _ _} _. diff --git a/src/Reflection/FilterLive.v b/src/Reflection/FilterLive.v index 446f9195c..57e296df7 100644 --- a/src/Reflection/FilterLive.v +++ b/src/Reflection/FilterLive.v @@ -9,7 +9,6 @@ Local Notation eta x := (fst x, snd x). Local Open Scope ctype_scope. Section language. Context (base_type_code : Type) - (interp_base_type : base_type_code -> Type) (op : flat_type base_type_code -> flat_type base_type_code -> Type) (Name : Type) (dead_name : Name) @@ -20,13 +19,10 @@ Section language. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). Local Notation var := (fun t : base_type_code => list Name). - Local Notation exprf := (@exprf base_type_code interp_base_type op var). - Local Notation expr := (@expr base_type_code interp_base_type op var). - Local Notation Expr := (@Expr base_type_code interp_base_type op var). + Local Notation exprf := (@exprf base_type_code op var). + Local Notation expr := (@expr base_type_code op var). + Local Notation Expr := (@Expr base_type_code op var). Fixpoint merge_name_lists (ls1 ls2 : list Name) : list Name := match ls1, ls2 with @@ -36,11 +32,11 @@ Section language. end. Definition names_to_list {t} : interp_flat_type (fun _ => Name) t -> list Name - := smart_interp_flat_map base_type_code (g:=fun _ => list Name) (fun _ x => x :: nil)%list (fun _ _ x y => x ++ y)%list. + := smart_interp_flat_map base_type_code (g:=fun _ => list Name) (fun _ x => x :: nil)%list nil (fun _ _ x y => x ++ y)%list. Fixpoint filter_live_namesf (prefix remaining : list Name) {t} (e : exprf t) : list Name := match e with - | Const _ x => prefix + | TT => prefix | Var _ x => x | Op _ _ op args => @filter_live_namesf prefix remaining _ args | LetIn tx ex _ eC @@ -58,13 +54,17 @@ Section language. end. Fixpoint filter_live_names (prefix remaining : list Name) {t} (e : expr t) : list Name - := match e, remaining with - | Return _ x, _ => filter_live_namesf prefix remaining x - | Abs src _ ef, cons n remaining' - => let prefix' := (prefix ++ (n :: nil))%list in - @filter_live_names - prefix' remaining' _ - (ef prefix') - | Abs _ _ _, nil => nil + := match e with + | Return _ x => filter_live_namesf prefix remaining x + | Abs src _ ef + => let '(ns, remaining') := eta (split_names (Tbase src) remaining) in + match ns with + | Some n => + let prefix' := (prefix ++ names_to_list n)%list in + @filter_live_names + prefix' remaining' _ + (ef (SmartValf _ (fun _ => prefix') (Tbase src))) + | None => nil + end end. End language. diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v index a42df2b68..91ad0886e 100644 --- a/src/Reflection/Inline.v +++ b/src/Reflection/Inline.v @@ -4,18 +4,16 @@ Require Import Crypto.Util.Tactics. Local Open Scope ctype_scope. Section language. - Context (base_type_code : Type). - Context (interp_base_type : base_type_code -> Type). - Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). + 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). Let Tbase := @Tbase base_type_code. Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - Local Notation Expr := (@Expr base_type_code interp_base_type op). + 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}. @@ -28,12 +26,12 @@ Section language. Context (postprocess : forall {t}, @exprf var t -> inline_directive t). Fixpoint inline_const_genf {t} (e : @exprf (@exprf var) t) : @exprf var t - := match e in Syntax.exprf _ _ _ t return @exprf var t with + := match e in Syntax.exprf _ _ t return @exprf var t with | LetIn tx ex tC eC => match postprocess _ (@inline_const_genf _ ex) in inline_directive t' return (interp_flat_type _ t' -> @exprf var tC) -> @exprf var tC with | default_inline _ ex - => match ex in Syntax.exprf _ _ _ t' return (interp_flat_type _ t' -> @exprf var tC) -> @exprf var tC with - | Const _ x => fun eC => eC (SmartConstf (op:=op) (var:=var) x) + => match ex in Syntax.exprf _ _ t' return (interp_flat_type _ t' -> @exprf var tC) -> @exprf var tC with + | TT => fun eC => eC tt | Var _ x => fun eC => eC (Var x) | ex => fun eC => LetIn ex (fun x => eC (SmartVarVarf x)) end @@ -42,33 +40,49 @@ Section language. | inline _ ex => fun eC => eC ex end (fun x => @inline_const_genf _ (eC x)) | Var _ x => x - | Const _ x => Const x + | TT => TT | Pair _ ex _ ey => Pair (@inline_const_genf _ ex) (@inline_const_genf _ ey) | Op _ _ op args => Op op (@inline_const_genf _ args) end. Fixpoint inline_const_gen {t} (e : @expr (@exprf var) t) : @expr var t - := match e in Syntax.expr _ _ _ t return @expr var t with + := match e in Syntax.expr _ _ t return @expr var t with | Return _ x => Return (inline_const_genf x) | Abs _ _ f => Abs (fun x => @inline_const_gen _ (f (Var x))) end. + + Section with_is_const. + Context (is_const : forall s d, op s d -> bool). + + Definition postprocess_for_const (t : flat_type) (v : @exprf var t) : inline_directive t + := if match v with Op _ _ op _ => @is_const _ _ op | _ => false end + then match t return @exprf _ t -> inline_directive t with + | Syntax.Tbase _ => @inline _ + | _ => @default_inline _ + end v + else default_inline v. + End with_is_const. End with_var. - Definition inline_constf {var t} := @inline_const_genf var (fun _ x => default_inline x) t. - Definition inline_const {var t} := @inline_const_gen var (fun _ x => default_inline x) t. + + Definition inline_constf is_const {var t} + := @inline_const_genf var (postprocess_for_const is_const) t. + Definition inline_const is_const {var t} + := @inline_const_gen var (postprocess_for_const is_const) t. Definition InlineConstGen (postprocess : forall var t, @exprf var t -> @inline_directive var t) {t} (e : Expr t) : Expr t := fun var => inline_const_gen (postprocess _) (e _). - Definition InlineConst {t} := @InlineConstGen (fun _ _ x => default_inline x) t. + Definition InlineConst is_const {t} + := @InlineConstGen (fun var => postprocess_for_const is_const) t. End language. -Global Arguments inline_directive {_} _ _ _ _, {_ _ _ _} _. -Global Arguments no_inline {_ _ _ _ _} _. -Global Arguments inline {_ _ _ _ _} _. -Global Arguments default_inline {_ _ _ _ _} _. -Global Arguments inline_const_genf {_ _ _ _} postprocess {_} _. -Global Arguments inline_const_gen {_ _ _ _} postprocess {_} _. -Global Arguments InlineConstGen {_ _ _} postprocess {_} _ var. -Global Arguments inline_constf {_ _ _ _ _} _. -Global Arguments inline_const {_ _ _ _ _} _. -Global Arguments InlineConst {_ _ _ _} _ var. +Global Arguments inline_directive {_} _ _ _, {_ _ _} _. +Global Arguments no_inline {_ _ _ _} _. +Global Arguments inline {_ _ _ _} _. +Global Arguments default_inline {_ _ _ _} _. +Global Arguments inline_const_genf {_ _ _} postprocess {_} _. +Global Arguments inline_const_gen {_ _ _} postprocess {_} _. +Global Arguments InlineConstGen {_ _} postprocess {_} _ var. +Global Arguments inline_constf {_ _} is_const {_ t} _. +Global Arguments inline_const {_ _} is_const {_ t} _. +Global Arguments InlineConst {_ _} is_const {_} _ var. diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v index 27811914c..1d92d1480 100644 --- a/src/Reflection/InlineInterp.v +++ b/src/Reflection/InlineInterp.v @@ -1,5 +1,6 @@ (** * Inline: Remove some [Let] expressions *) Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.InlineWf. Require Import Crypto.Reflection.InterpProofs. Require Import Crypto.Reflection.Inline. @@ -15,23 +16,21 @@ Section language. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Let interp_type := interp_type interp_base_type. - Let interp_flat_type := interp_flat_type interp_base_type. - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - Local Notation Expr := (@Expr base_type_code interp_base_type op). - Local Notation wff := (@wff base_type_code interp_base_type op). - Local Notation wf := (@wf base_type_code interp_base_type op). + Local Notation interp_type := (interp_type interp_base_type). + Local Notation interp_flat_type := (interp_flat_type interp_base_type). + 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 wff := (@wff base_type_code op). + Local Notation wf := (@wf base_type_code op). - Local Hint Extern 1 => eapply interpf_SmartConstf. Local Hint Extern 1 => eapply interpf_SmartVarVarf. Local Ltac t_fin := repeat match goal with | _ => reflexivity | _ => progress simpl in * + | _ => progress unfold postprocess_for_const in * | _ => progress intros | _ => progress inversion_sigma | _ => progress inversion_prod @@ -49,14 +48,14 @@ Section language. | [ H : _ |- _ ] => rewrite H end. - Lemma interpf_inline_constf G {t} e1 e2 + Lemma interpf_inline_constf is_const G {t} e1 e2 (wf : @wff _ _ G t e1 e2) (H : forall t x x', List.In - (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) t + (existT (fun t : base_type_code => (exprf (Tbase t) * interp_base_type t)%type) t (x, x')) G -> interpf interp_op x = x') - : interpf interp_op (inline_constf e1) = interpf interp_op e2. + : interpf interp_op (inline_constf is_const e1) = interpf interp_op e2. Proof. clear -wf H. induction wf; t_fin. @@ -64,19 +63,19 @@ Section language. Local Hint Resolve interpf_inline_constf. - Lemma interp_inline_const G {t} e1 e2 + Lemma interp_inline_const is_const G {t} e1 e2 (wf : @wf _ _ G t e1 e2) (H : forall t x x', List.In - (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) t + (existT (fun t : base_type_code => (exprf (Tbase t) * interp_base_type t)%type) t (x, x')) G -> interpf interp_op x = x') : interp_type_gen_rel_pointwise (fun _ => @eq _) - (interp interp_op (inline_const e1)) + (interp interp_op (inline_const is_const e1)) (interp interp_op e2). Proof. induction wf. - { eapply interpf_inline_constf; eauto. } + { eapply (interpf_inline_constf is_const); eauto. } { simpl in *; intro. match goal with | [ H : _ |- _ ] @@ -84,13 +83,13 @@ Section language. end. } Qed. - Lemma Interp_InlineConst {t} (e : Expr t) + Lemma Interp_InlineConst is_const {t} (e : Expr t) (wf : Wf e) : interp_type_gen_rel_pointwise (fun _ => @eq _) - (Interp interp_op (InlineConst e)) + (Interp interp_op (InlineConst is_const e)) (Interp interp_op e). Proof. unfold Interp, InlineConst. - eapply interp_inline_const with (G := nil); simpl; intuition. + eapply (interp_inline_const is_const) with (G := nil); simpl; intuition. Qed. End language. diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v index 5b9f27f48..5e402bf97 100644 --- a/src/Reflection/InlineWf.v +++ b/src/Reflection/InlineWf.v @@ -6,21 +6,17 @@ Require Import Crypto.Util.Tactics.SpecializeBy Crypto.Util.Tactics.DestructHead Local Open Scope ctype_scope. Section language. - Context (base_type_code : Type). - Context (interp_base_type : base_type_code -> Type). - Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). + 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). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Let interp_type := interp_type interp_base_type. - Let interp_flat_type := interp_flat_type interp_base_type. - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - Local Notation Expr := (@Expr base_type_code interp_base_type op). - Local Notation wff := (@wff base_type_code interp_base_type op). - Local Notation wf := (@wf base_type_code interp_base_type op). + Local Notation Tbase := (@Tbase 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 wff := (@wff base_type_code op). + Local Notation wf := (@wf base_type_code op). Section with_var. Context {var1 var2 : base_type_code -> Type}. @@ -33,7 +29,7 @@ Section language. Local Hint Extern 1 => progress unfold List.In in *. Local Hint Resolve wff_in_impl_Proper. Local Hint Resolve wff_SmartVarf. - Local Hint Resolve wff_SmartConstf. + Local Hint Resolve wff_SmartVarVarf. Local Ltac t_fin := repeat first [ intro @@ -42,21 +38,20 @@ Section language. | tauto | progress subst | solve [ auto with nocore - | eapply (@wff_SmartVarVarf _ _ _ _ _ _ _ (_ * _)); auto - | eapply wff_SmartConstf; eauto with nocore + | eapply (@wff_SmartVarVarf _ _ _ _ _ _ (_ * _)); auto | eapply wff_SmartVarVarf; eauto with nocore ] | progress simpl in * | constructor | solve [ eauto ] ]. - Lemma wff_inline_constf {t} e1 e2 G G' - (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf t * exprf t)%type) t (x, x')) G' + Lemma wff_inline_constf is_const {t} e1 e2 G G' + (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G' -> wff G x x') (wf : wff G' e1 e2) - : @wff var1 var2 G t (inline_constf e1) (inline_constf e2). + : @wff var1 var2 G t (inline_constf is_const e1) (inline_constf is_const e2). Proof. revert dependent G; induction wf; simpl in *; intros; auto; - specialize_by auto. + specialize_by auto; unfold postprocess_for_const. repeat match goal with | [ H : context[List.In _ (_ ++ _)] |- _ ] => setoid_rewrite List.in_app_iff in H @@ -65,40 +60,41 @@ Section language. | [ H : _ |- _ ] => pose proof (IHwf _ H) as IHwf' end. - generalize dependent (inline_constf e1); generalize dependent (inline_constf e1'); intros. + generalize dependent (inline_constf is_const e1); generalize dependent (inline_constf is_const e1'); intros. destruct IHwf'; simpl in *; + try match goal with |- context[@is_const ?x ?y ?z] => is_var y; destruct (@is_const x y z), y end; repeat constructor; auto; intros; match goal with | [ H : _ |- _ ] - => apply H; intros; progress destruct_head' or + => apply H; intros; progress destruct_head_hnf' or end; t_fin. Qed. - Lemma wf_inline_const {t} e1 e2 G G' - (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf t * exprf t)%type) t (x, x')) G' + Lemma wf_inline_const is_const {t} e1 e2 G G' + (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x, x')) G' -> wff G x x') (Hwf : wf G' e1 e2) - : @wf var1 var2 G t (inline_const e1) (inline_const e2). + : @wf var1 var2 G t (inline_const is_const e1) (inline_const is_const e2). Proof. revert dependent G; induction Hwf; simpl; constructor; intros; - [ eapply wff_inline_constf; eauto | ]. - match goal with - | [ H : _ |- _ ] - => apply H; simpl; intros; progress destruct_head' or - end; + [ eapply (wff_inline_constf is_const); [ | solve [ eauto ] ] | ]; + match goal with + | [ H : _ |- _ ] + => apply H; simpl; intros; progress destruct_head' or + end; inversion_sigma; inversion_prod; repeat subst; simpl. { constructor; left; reflexivity. } { eauto. } Qed. End with_var. - Lemma WfInlineConst {t} (e : Expr t) + Lemma WfInlineConst is_const {t} (e : Expr t) (Hwf : Wf e) - : Wf (InlineConst e). + : Wf (InlineConst is_const e). Proof. intros var1 var2. - apply (@wf_inline_const var1 var2 t (e _) (e _) nil nil); simpl; [ tauto | ]. + apply (@wf_inline_const var1 var2 is_const t (e _) (e _) nil nil); simpl; [ tauto | ]. apply Hwf. Qed. End language. diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index dd9cab21d..3cd688cf3 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -1,6 +1,7 @@ (** * PHOAS Representation of Gallina which allows exact denotation *) Require Import Coq.Strings.String. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.InterpProofs. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. @@ -16,7 +17,6 @@ Section language. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Local Notation Tbase := (@Tbase base_type_code). Section expr_param. Context (interp_base_type : base_type_code -> Type). @@ -29,7 +29,7 @@ Section language. (** N.B. [Let] destructures pairs *) Inductive exprf : flat_type -> Type := - | Const {t : flat_type} : interp_type t -> exprf t + | Const {t : flat_type} : interp_flat_type t -> exprf t | Var {t} : var t -> exprf t | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR | LetIn : forall {tx}, exprf tx -> forall {tC}, (var tx -> exprf tC) -> exprf tC @@ -55,7 +55,7 @@ Section language. | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey) | MatchPair _ _ ex _ eC => match @interpf _ ex with pair x y => @interpf _ (eC x y) end end. - Fixpoint interp {t} (e : @expr interp_type t) : interp_type t + Fixpoint interp {t} (e : @expr interp_flat_type t) : interp_type t := match e in expr t return interp_type t with | Return _ x => interpf x | Abs _ _ f => fun x => @interp _ (f x) @@ -65,11 +65,20 @@ Section language. End interp. Section compile. - Context {var : base_type_code -> Type}. + Context {var : base_type_code -> Type} + (make_const : forall t, interp_base_type t -> op Unit (Tbase t)). + + Fixpoint SmartConst (t : flat_type) : interp_flat_type t -> Syntax.exprf base_type_code op (var:=var) t + := match t return interp_flat_type t -> Syntax.exprf _ _ t with + | Unit => fun _ => TT + | Tbase _ => fun v => Syntax.Op (make_const _ v) TT + | Prod _ _ => fun v => Syntax.Pair (@SmartConst _ (fst v)) + (@SmartConst _ (snd v)) + end. - Fixpoint compilef {t} (e : @exprf (interp_flat_type_gen var) t) : @Syntax.exprf base_type_code interp_base_type op var t - := match e in exprf t return @Syntax.exprf _ _ _ _ t with - | Const _ x => Syntax.Const x + Fixpoint compilef {t} (e : @exprf (interp_flat_type_gen var) t) : @Syntax.exprf base_type_code op var t + := match e in exprf t return @Syntax.exprf _ _ _ t with + | Const _ x => @SmartConst _ x | Var _ x => Syntax.SmartVarf x | Op _ _ op args => Syntax.Op op (@compilef _ args) | LetIn _ ex _ eC => Syntax.LetIn (@compilef _ ex) (fun x => @compilef _ (eC x)) @@ -77,21 +86,31 @@ Section language. | MatchPair _ _ ex _ eC => Syntax.LetIn (@compilef _ ex) (fun xy => @compilef _ (eC (fst xy) (snd xy))) end. - Fixpoint compile {t} (e : @expr (interp_flat_type_gen var) t) : @Syntax.expr base_type_code interp_base_type op var t - := match e in expr t return @Syntax.expr _ _ _ _ t with + Fixpoint compile {t} (e : @expr (interp_flat_type_gen var) t) : @Syntax.expr base_type_code op var t + := match e in expr t return @Syntax.expr _ _ _ t with | Return _ x => Syntax.Return (compilef x) | Abs a _ f => Syntax.Abs (fun x : var a => @compile _ (f x)) end. End compile. - Definition Compile {t} (e : Expr t) : Syntax.Expr base_type_code interp_base_type op t - := fun var => compile (e _). + Definition Compile + (make_const : forall t, interp_base_type t -> op Unit (Tbase t)) + {t} (e : Expr t) : Syntax.Expr base_type_code op t + := fun var => compile make_const (e _). Section compile_correct. - Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). + Context (make_const : forall t, interp_base_type t -> op Unit (Tbase t)) + (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst) + (make_const_correct : forall T v, interp_op Unit (Tbase T) (make_const T v) tt = v). + + Lemma SmartConst_correct t v + : Syntax.interpf interp_op (SmartConst make_const t v) = v. + Proof. + induction t; try destruct v; simpl in *; congruence. + Qed. Lemma compilef_correct {t} (e : @exprf interp_flat_type t) - : Syntax.interpf interp_op (compilef e) = interpf interp_op e. + : Syntax.interpf interp_op (compilef make_const e) = interpf interp_op e. Proof. induction e; repeat match goal with @@ -99,6 +118,7 @@ Section language. | _ => progress unfold LetIn.Let_In | _ => progress simpl in * | _ => rewrite interpf_SmartVarf + | _ => rewrite SmartConst_correct | _ => rewrite <- surjective_pairing | _ => progress rewrite_hyp * | [ |- context[let (x, y) := ?v in _] ] @@ -108,7 +128,7 @@ Section language. Lemma Compile_correct {t} (e : @Expr t) : interp_type_gen_rel_pointwise (fun _ => @eq _) - (Syntax.Interp interp_op (Compile e)) + (Syntax.Interp interp_op (Compile make_const e)) (Interp interp_op e). Proof. unfold Interp, Compile, Syntax.Interp; simpl. @@ -121,7 +141,7 @@ Section language. Qed. Lemma Compile_flat_correct {t : flat_type} (e : @Expr t) - : Syntax.Interp interp_op (Compile e) = Interp interp_op e. + : Syntax.Interp interp_op (Compile make_const e) = Interp interp_op e. Proof. exact (@Compile_correct t e). Qed. End compile_correct. End expr_param. @@ -135,4 +155,4 @@ Global Arguments MatchPair {_ _ _ _ _ _} _ {_} _. Global Arguments Pair {_ _ _ _ _} _ {_} _. Global Arguments Return {_ _ _ _ _} _. Global Arguments Abs {_ _ _ _ _ _} _. -Global Arguments Compile {_ _ _ t} _ _. +Global Arguments Compile {_ _ _} make_const {t} _ _. diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v index 4e49050b0..abd54ec3b 100644 --- a/src/Reflection/InterpProofs.v +++ b/src/Reflection/InterpProofs.v @@ -9,12 +9,10 @@ Section language. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. Context (interp_base_type : base_type_code -> Type). Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type). - Let interp_type := interp_type interp_base_type. - Let interp_flat_type := interp_flat_type interp_base_type. + Local Notation interp_type := (interp_type interp_base_type). + Local Notation interp_flat_type := (interp_flat_type interp_base_type). Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). Lemma interpf_LetIn tx ex tC eC @@ -35,29 +33,15 @@ Section language. end. Qed. - Lemma interpf_SmartConstf {t t'} v x x' - (Hin : List.In - (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type) - t (x, x')) - (flatten_binding_list (t := t') base_type_code (SmartConstf v) v)) - : interpf interp_op x = x'. - Proof. - clear -Hin. - induction t'; simpl in *. - { intuition (inversion_sigma; inversion_prod; subst; eauto). } - { apply List.in_app_iff in Hin. - intuition (inversion_sigma; inversion_prod; subst; eauto). } - Qed. - Lemma interpf_SmartVarVarf {t t'} v x x' (Hin : List.In - (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type) + (existT (fun t : base_type_code => (exprf base_type_code op (Tbase t) * interp_base_type t)%type) t (x, x')) (flatten_binding_list (t := t') base_type_code (SmartVarVarf v) v)) : interpf interp_op x = x'. Proof. clear -Hin. - induction t'; simpl in *. + induction t'; simpl in *; try tauto. { intuition (inversion_sigma; inversion_prod; subst; eauto). } { apply List.in_app_iff in Hin. intuition (inversion_sigma; inversion_prod; subst; eauto). } @@ -66,7 +50,7 @@ Section language. Lemma interpf_SmartVarVarf_eq {t t'} v v' x x' (Heq : v = v') (Hin : List.In - (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type) + (existT (fun t : base_type_code => (exprf base_type_code op (Tbase t) * interp_base_type t)%type) t (x, x')) (flatten_binding_list (t := t') base_type_code (SmartVarVarf v') v)) : interpf interp_op x = x'. diff --git a/src/Reflection/InterpWf.v b/src/Reflection/InterpWf.v index c53389b8c..c26c1c3ce 100644 --- a/src/Reflection/InterpWf.v +++ b/src/Reflection/InterpWf.v @@ -1,5 +1,6 @@ Require Import Coq.Strings.String Coq.Classes.RelationClasses. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Prod. @@ -14,9 +15,9 @@ Section language. {op : flat_type base_type_code -> flat_type base_type_code -> Type} (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst). - Local Notation exprf := (@exprf base_type_code interp_base_type op interp_base_type). - Local Notation expr := (@expr base_type_code interp_base_type op interp_base_type). - Local Notation Expr := (@Expr base_type_code interp_base_type op). + Local Notation exprf := (@exprf base_type_code op interp_base_type). + Local Notation expr := (@expr base_type_code op interp_base_type). + Local Notation Expr := (@Expr base_type_code op). Local Notation interpf := (@interpf base_type_code interp_base_type op interp_op). Local Notation interp := (@interp base_type_code interp_base_type op interp_op). Local Notation Interp := (@Interp base_type_code interp_base_type op interp_op). @@ -27,7 +28,7 @@ Section language. (flatten_binding_list base_type_code (t:=T) e e)) : x = x'. Proof. - induction T; simpl in *; [ | rewrite List.in_app_iff in HIn ]; + induction T; simpl in *; [ | | rewrite List.in_app_iff in HIn ]; repeat first [ progress destruct_head or | progress destruct_head False | progress destruct_head and diff --git a/src/Reflection/InterpWfRel.v b/src/Reflection/InterpWfRel.v index 9057e2ba5..eeee8073e 100644 --- a/src/Reflection/InterpWfRel.v +++ b/src/Reflection/InterpWfRel.v @@ -1,6 +1,6 @@ Require Import Coq.Strings.String Coq.Classes.RelationClasses. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.WfRel. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Prod. @@ -20,12 +20,11 @@ Section language. -> interp_flat_type_rel_pointwise2 R (interp_op1 src dst op sv1) (interp_op2 src dst op sv2)). - Local Notation exprf1 := (@exprf base_type_code interp_base_type1 op interp_base_type1). - Local Notation exprf2 := (@exprf base_type_code interp_base_type2 op interp_base_type2). - Local Notation expr1 := (@expr base_type_code interp_base_type1 op interp_base_type1). - Local Notation expr2 := (@expr base_type_code interp_base_type2 op interp_base_type2). - Local Notation Expr1 := (@Expr base_type_code interp_base_type1 op). - Local Notation Expr2 := (@Expr base_type_code interp_base_type2 op). + Local Notation exprf1 := (@exprf base_type_code op interp_base_type1). + Local Notation exprf2 := (@exprf base_type_code op interp_base_type2). + Local Notation expr1 := (@expr base_type_code op interp_base_type1). + Local Notation expr2 := (@expr base_type_code op interp_base_type2). + Local Notation Expr := (@Expr base_type_code op). Local Notation interpf1 := (@interpf base_type_code interp_base_type1 op interp_op1). Local Notation interpf2 := (@interpf base_type_code interp_base_type2 op interp_op2). Local Notation interp1 := (@interp base_type_code interp_base_type1 op interp_op1). @@ -40,7 +39,7 @@ Section language. (flatten_binding_list base_type_code (t:=T) e1 e2)) : R t x x'. Proof. - induction T; simpl in *; [ | rewrite List.in_app_iff in HIn ]; + induction T; simpl in *; try tauto; [ | rewrite List.in_app_iff in HIn ]; repeat first [ progress destruct_head or | progress destruct_head False | progress destruct_head and @@ -53,13 +52,13 @@ Section language. Local Hint Resolve List.in_app_or List.in_or_app interp_flat_type_rel_pointwise2_flatten_binding_list. Section wf. - Lemma interpf_rel_wff + Lemma interpf_wff {t} {e1 : exprf1 t} {e2 : exprf2 t} {G} (HG : forall t x x', List.In (existT (fun t : base_type_code => (interp_base_type1 t * interp_base_type2 t)%type) t (x, x')%core) G -> R t x x') - (Rwf : rel_wff R G e1 e2) + (Rwf : wff G e1 e2) : interp_flat_type_rel_pointwise2 R (interpf1 e1) (interpf2 e2). Proof. induction Rwf; simpl; auto. @@ -73,15 +72,15 @@ Section language. end. Qed. - Local Hint Resolve interpf_rel_wff. + Local Hint Resolve interpf_wff. - Lemma interp_rel_wf + Lemma interp_wf {t} {e1 : expr1 t} {e2 : expr2 t} {G} (HG : forall t x x', List.In (existT (fun t : base_type_code => (interp_base_type1 t * interp_base_type2 t)%type) t (x, x')%core) G -> R t x x') - (Rwf : rel_wf R G e1 e2) + (Rwf : wf G e1 e2) : interp_type_rel_pointwise2 R (interp1 e1) (interp2 e2). Proof. induction Rwf; simpl; repeat intro; simpl in *; eauto. @@ -92,12 +91,12 @@ Section language. inversion_sigma; inversion_prod; repeat subst; simpl; auto. Qed. - Lemma InterpRelWf - {t} {e1 : Expr1 t} {e2 : Expr2 t} - (Rwf : RelWf R e1 e2) - : interp_type_rel_pointwise2 R (Interp1 e1) (Interp2 e2). + Lemma InterpWf + {t} {e : Expr t} + (Rwf : Wf e) + : interp_type_rel_pointwise2 R (Interp1 e) (Interp2 e). Proof. - unfold Interp, RelWf in *; apply (interp_rel_wf (G:=nil)); simpl; intuition. + unfold Interp, Wf in *; apply (interp_wf (G:=nil)); simpl; intuition. Qed. End wf. End language. diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v index 810d9115b..432907d5c 100644 --- a/src/Reflection/Linearize.v +++ b/src/Reflection/Linearize.v @@ -4,40 +4,26 @@ Require Import Crypto.Util.Tactics. Local Open Scope ctype_scope. Section language. - Context (base_type_code : Type). - Context (interp_base_type : base_type_code -> Type). - Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). + 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). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type_gen := interp_flat_type. - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation Expr := (@Expr base_type_code interp_base_type op). + Local Notation Tbase := (@Tbase base_type_code). + Local Notation Expr := (@Expr base_type_code op). Section with_var. Context {var : base_type_code -> Type}. - Local Notation exprf := (@exprf base_type_code interp_base_type op var). - Local Notation expr := (@expr base_type_code interp_base_type op var). + Local Notation exprf := (@exprf base_type_code op var). + Local Notation expr := (@expr base_type_code op var). Section under_lets. - Fixpoint let_bind_const {t} (e : interp_flat_type t) {struct t} - : forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC - := match t return forall (e : interp_flat_type t) {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC with - | Prod A B => fun e _ C => @let_bind_const A (fst e) _ (fun x => - @let_bind_const B (snd e) _ (fun y => - C (x, y))) - | Syntax.Tbase _ => fun e _ C => LetIn (Const e) C - end e. - Fixpoint under_letsf {t} (e : exprf t) - : forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC - := match e in Syntax.exprf _ _ _ t return forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC with + : forall {tC} (C : interp_flat_type var t -> exprf tC), exprf tC + := match e in Syntax.exprf _ _ t return forall {tC} (C : interp_flat_type var t -> exprf tC), exprf tC with | LetIn _ ex _ eC => fun _ C => @under_letsf _ ex _ (fun v => @under_letsf _ (eC v) _ C) - | Const _ x => fun _ C => let_bind_const x C + | TT => fun _ C => C tt | Var _ x => fun _ C => C x | Op _ _ op args as e => fun _ C => LetIn e C | Pair A x B y => fun _ C => @under_letsf A x _ (fun x => @@ -47,10 +33,10 @@ Section language. End under_lets. Fixpoint linearizef {t} (e : exprf t) : exprf t - := match e in Syntax.exprf _ _ _ t return exprf t with + := match e in Syntax.exprf _ _ t return exprf t with | LetIn _ ex _ eC => under_letsf (@linearizef _ ex) (fun x => @linearizef _ (eC x)) - | Const _ x => Const x + | TT => TT | Var _ x => Var x | Op _ _ op args => under_letsf (@linearizef _ args) (fun args => LetIn (Op op (SmartVarf args)) SmartVarf) @@ -61,7 +47,7 @@ Section language. end. Fixpoint linearize {t} (e : expr t) : expr t - := match e in Syntax.expr _ _ _ t return expr t with + := match e in Syntax.expr _ _ t return expr t with | Return _ x => linearizef x | Abs _ _ f => Abs (fun x => @linearize _ (f x)) end. @@ -71,8 +57,7 @@ Section language. := fun var => linearize (e _). End language. -Global Arguments let_bind_const {_ _ _ _ t} _ {tC} _. -Global Arguments under_letsf {_ _ _ _ _} _ {tC} _. -Global Arguments linearizef {_ _ _ _ _} _. -Global Arguments linearize {_ _ _ _ _} _. -Global Arguments Linearize {_ _ _ _} _ var. +Global Arguments under_letsf {_ _ _ _} _ {tC} _. +Global Arguments linearizef {_ _ _ _} _. +Global Arguments linearize {_ _ _ _} _. +Global Arguments Linearize {_ _ _} _ var. diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v index 3ee3960d5..ffa7119c6 100644 --- a/src/Reflection/LinearizeInterp.v +++ b/src/Reflection/LinearizeInterp.v @@ -1,5 +1,6 @@ (** * Linearize: Place all and only operations in let binders *) Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.LinearizeWf. Require Import Crypto.Reflection.InterpProofs. Require Import Crypto.Reflection.Linearize. @@ -15,17 +16,14 @@ Section language. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Let interp_type := interp_type interp_base_type. - Let interp_flat_type := interp_flat_type interp_base_type. - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - Local Notation Expr := (@Expr base_type_code interp_base_type op). - Local Notation wff := (@wff base_type_code interp_base_type op). - Local Notation wf := (@wf base_type_code interp_base_type op). + Local Notation interp_type := (interp_type interp_base_type). + Local Notation interp_flat_type := (interp_flat_type interp_base_type). + 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 wff := (@wff base_type_code op). + Local Notation wf := (@wf base_type_code op). - Local Hint Extern 1 => eapply interpf_SmartConstf. Local Hint Extern 1 => eapply interpf_SmartVarVarf. Local Ltac t_fin := @@ -50,19 +48,11 @@ Section language. | [ H : _ |- _ ] => rewrite H end. - Lemma interpf_let_bind_const {t tC} ex (eC : _ -> exprf tC) - : interpf interp_op (let_bind_const (t:=t) ex eC) = interpf interp_op (eC ex). - Proof. - clear. - revert tC eC; induction t; t_fin. - Qed. - Lemma interpf_under_letsf {t tC} (ex : exprf t) (eC : _ -> exprf tC) : interpf interp_op (under_letsf ex eC) = let x := interpf interp_op ex in interpf interp_op (eC x). Proof. clear. induction ex; t_fin. - rewrite interpf_let_bind_const; reflexivity. Qed. Lemma interpf_linearizef {t} e diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v index 36c9efecb..3055c7662 100644 --- a/src/Reflection/LinearizeWf.v +++ b/src/Reflection/LinearizeWf.v @@ -6,22 +6,17 @@ Require Import Crypto.Util.Tactics Crypto.Util.Sigma. Local Open Scope ctype_scope. Section language. - Context (base_type_code : Type). - Context (interp_base_type : base_type_code -> Type). - Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). + 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). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type_gen := interp_flat_type. - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - Local Notation Expr := (@Expr base_type_code interp_base_type op). - Local Notation wff := (@wff base_type_code interp_base_type op). - Local Notation wf := (@wf base_type_code interp_base_type op). + Local Notation Tbase := (@Tbase 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 wff := (@wff base_type_code op). + Local Notation wf := (@wf base_type_code op). Section with_var. Context {var1 var2 : base_type_code -> Type}. @@ -48,15 +43,6 @@ Section language. end. Local Ltac t_fin tac := repeat t_fin_step tac. - Lemma wff_let_bind_const G {t} v {tC} eC1 eC2 - : (forall (x1 : interp_flat_type_gen var1 t) (x2 : interp_flat_type_gen var2 t), - wff (flatten_binding_list base_type_code x1 x2 ++ G) (eC1 x1) (eC2 x2)) - -> @wff var1 var2 G tC (let_bind_const v eC1) (let_bind_const v eC2). - Proof. - revert G tC eC1 eC2; induction t; t_fin idtac. - Qed. - - Local Hint Resolve wff_let_bind_const. Local Hint Constructors Syntax.wff. Local Hint Resolve List.in_app_or List.in_or_app. @@ -68,15 +54,15 @@ Section language. pattern G0, t0, e1, e2; lazymatch goal with | [ |- ?retP _ _ _ _ ] - => first [ refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + => first [ refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2 return match v1 return Prop with - | Const _ _ => retP G t v1 v2 + | TT => retP G t v1 v2 | _ => forall P : Prop, P -> P end with - | WfConst _ _ _ => _ + | WfTT _ => _ | _ => fun _ p => p end) - | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + | refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2 return match v1 return Prop with | Var _ _ => retP G t v1 v2 | _ => forall P : Prop, P -> P @@ -84,7 +70,7 @@ Section language. | WfVar _ _ _ _ _ => _ | _ => fun _ p => p end) - | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + | refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2 return match v1 return Prop with | Op _ _ _ _ => retP G t v1 v2 | _ => forall P : Prop, P -> P @@ -92,7 +78,7 @@ Section language. | WfOp _ _ _ _ _ _ _ => _ | _ => fun _ p => p end) - | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + | refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2 return match v1 return Prop with | LetIn _ _ _ _ => retP G t v1 v2 | _ => forall P : Prop, P -> P @@ -100,7 +86,7 @@ Section language. | WfLetIn _ _ _ _ _ _ _ _ _ => _ | _ => fun _ p => p end) - | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + | refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2 return match v1 return Prop with | Pair _ _ _ _ => retP G t v1 v2 | _ => forall P : Prop, P -> P @@ -111,7 +97,7 @@ Section language. end. Fixpoint wff_under_letsf G {t} e1 e2 {tC} eC1 eC2 (wf : @wff var1 var2 G t e1 e2) - (H : forall (x1 : interp_flat_type_gen var1 t) (x2 : interp_flat_type_gen var2 t), + (H : forall (x1 : interp_flat_type var1 t) (x2 : interp_flat_type var2 t), wff (flatten_binding_list base_type_code x1 x2 ++ G) (eC1 x1) (eC2 x2)) {struct e1} : @wff var1 var2 G tC (under_letsf e1 eC1) (under_letsf e2 eC2). @@ -128,15 +114,15 @@ Section language. end); generalize (fun G => match e1v return match e1v with | LetIn tx0 _ tC1 e0 => (* 8.4's type inferencer is broken, so we copy/paste the term from 8.5. This entire clause could just be [_], if Coq 8.4 worked *) - forall (x : @interp_flat_type_gen base_type_code var1 tx0) (e3 : exprf tC1) - (tC2 : flat_type) (eC3 : @interp_flat_type_gen base_type_code var1 tC1 -> exprf tC2) - (eC4 : @interp_flat_type_gen base_type_code var2 tC1 -> exprf tC2), + forall (x : @interp_flat_type base_type_code var1 tx0) (e3 : exprf tC1) + (tC2 : flat_type) (eC3 : @interp_flat_type base_type_code var1 tC1 -> exprf tC2) + (eC4 : @interp_flat_type base_type_code var2 tC1 -> exprf tC2), wff G (e0 x) e3 -> - (forall (x1 : @interp_flat_type_gen base_type_code var1 tC1) - (x2 : @interp_flat_type_gen base_type_code var2 tC1), + (forall (x1 : @interp_flat_type base_type_code var1 tC1) + (x2 : @interp_flat_type base_type_code var2 tC1), wff (@flatten_binding_list base_type_code var1 var2 tC1 x1 x2 ++ G) (eC3 x1) (eC4 x2)) -> - wff G (@under_letsf base_type_code interp_base_type op var1 tC1 (e0 x) tC2 eC3) - (@under_letsf base_type_code interp_base_type op var2 tC1 e3 tC2 eC4) + wff G (@under_letsf base_type_code op var1 tC1 (e0 x) tC2 eC3) + (@under_letsf base_type_code op var2 tC1 e3 tC2 eC4) | _ => _ end with | LetIn _ ex tC' eC => fun x => wff_under_letsf G tC' (eC x) | _ => I 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. diff --git a/src/Reflection/MapCastWithCastOp.v b/src/Reflection/MapCastWithCastOp.v index 189399fad..ae41e1181 100644 --- a/src/Reflection/MapCastWithCastOp.v +++ b/src/Reflection/MapCastWithCastOp.v @@ -10,7 +10,6 @@ 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} @@ -18,40 +17,44 @@ Section language. (base_type_code1_beq : base_type_code1 -> base_type_code1 -> bool) (base_type_code1_bl : forall x y, base_type_code1_beq x y = true -> x = y) (base_type_code1_lb : forall x y, x = y -> base_type_code1_beq x y = true) - (failv : forall {t}, interp_base_type1 t) + (failv : forall {var t}, @exprf base_type_code1 op1 var (Tbase 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)) - (Cast : forall var t1 t2, @exprf base_type_code1 interp_base_type1 op1 var (Tbase t1) - -> @exprf base_type_code1 interp_base_type1 op1 var (Tbase t2)) + (Cast : forall var t1 t2, @exprf base_type_code1 op1 var (Tbase t1) + -> @exprf base_type_code1 op1 var (Tbase t2)) (is_cast : forall t1 t2, op1 t1 t2 -> bool). 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))). Local Notation new_type := (@new_type base_type_code1 base_type_code2 interp_base_type2 new_base_type). Context (new_op : forall ovar src1 dst1 src2 dst2 (opc1 : op1 src1 dst1) (opc2 : op2 src2 dst2) - args2, - option { new_src : _ & (@exprf base_type_code1 interp_base_type1 op1 ovar new_src - -> @exprf base_type_code1 interp_base_type1 op1 ovar (new_flat_type (interpf interp_op2 (Op opc2 args2))))%type }). + args2, + option { new_src : _ & (@exprf base_type_code1 op1 ovar new_src + -> @exprf base_type_code1 op1 ovar (new_flat_type (interpf interp_op2 (Op opc2 args2))))%type }). + Local Notation SmartFail + := (SmartValf _ (@failv _)). + Local Notation failf t (* {t} : @exprf base_type_code1 op1 ovar t*) + := (SmartPairf (SmartFail t)). - Fixpoint VarBound {var} T1 T2 : interp_flat_type var T1 -> exprf _ interp_base_type1 op1 (var:=var) T2 - := match T1, T2 return interp_flat_type var T1 -> exprf _ _ _ T2 with + Fixpoint VarBound {var} T1 T2 : interp_flat_type var T1 -> exprf _ op1 (var:=var) T2 + := match T1, T2 return interp_flat_type var T1 -> exprf _ _ T2 with | Tbase T1', Tbase T2' => fun v : var T1' => Cast _ _ _ (Var v) + | _, Unit => fun _ => TT | Prod A1 B1, Prod A2 B2 => fun xy => Pair (@VarBound _ _ _ (fst xy)) (@VarBound _ _ _ (snd xy)) | Tbase _, _ | Prod _ _, _ - => fun _ => Const (SmartValf _ (@failv) _) + | Unit, _ + => fun _ => failf _ end. - Fixpoint SmartBound {var t1 t2} (v : @exprf _ interp_base_type1 op1 var t1) : @exprf _ interp_base_type1 op1 var t2. + Fixpoint SmartBound {var t1 t2} (v : @exprf _ op1 var t1) : @exprf _ op1 var t2. Proof. refine match Sumbool.sumbool_of_bool (flat_type_beq _ base_type_code1_beq t1 t2) with - | left pf => match flat_type_dec_bl _ _ base_type_code1_bl _ _ pf in (_ = y) return exprf _ _ _ y with + | left pf => match flat_type_dec_bl _ _ base_type_code1_bl _ _ pf in (_ = y) return exprf _ _ y with | eq_refl => v end | right _ => _ end. - refine (match v in exprf _ _ _ t1, t2 return (exprf _ _ _ _ -> exprf _ _ _ t2) -> exprf _ _ _ t2 with + refine (match v in exprf _ _ t1, t2 return (exprf _ _ _ -> exprf _ _ t2) -> exprf _ _ t2 with | Op t1 tR opc args, _ => if is_cast _ _ opc then fun _ => @SmartBound _ _ _ args @@ -59,12 +62,14 @@ Section language. | Pair _ ex _ ey, Prod _ _ => fun _ => Pair (@SmartBound _ _ _ ex) (@SmartBound _ _ _ ey) | v', _ => fun default => default v' end _). - refine (match t1, t2 return exprf _ _ _ t1 -> exprf _ _ _ t2 with + refine (match t1, t2 return exprf _ _ t1 -> exprf _ _ t2 with | Tbase t1', Tbase t2' => Cast _ _ _ + | _, Unit => fun _ => TT | Prod A1 B1, Prod A2 B2 => fun x => LetIn x (VarBound _ _) | Tbase _, _ | Prod _ _, _ - => fun _ => Const (SmartValf _ (@failv) _) + | Unit, _ + => fun _ => failf _ end). Defined. Definition bound_op ovar @@ -72,28 +77,29 @@ Section language. (opc1 : op1 src1 dst1) (opc2 : op2 src2 dst2) : forall 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))) := if is_cast _ _ opc1 then fun _ x => SmartBound x else fun args2 args' => match new_op _ _ _ _ _ opc1 opc2 args2 with | Some f => projT2 f (SmartBound args') - | None => Const (SmartValf _ (@failv) _) + | None => failf _ end. 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). Fixpoint bound_var tx1 tx2 tC1 {struct tx2} - : forall (f : interp_flat_type ivarf tx1 -> exprf _ interp_base_type1 op1 (var:=ovar) tC1) + : forall (f : interp_flat_type ivarf tx1 -> exprf _ op1 (var:=ovar) tC1) (v : interp_flat_type ivarf tx2), - exprf _ interp_base_type1 op1 (var:=ovar) tC1 + exprf _ op1 (var:=ovar) tC1 := match tx1, tx2 return (interp_flat_type _ tx1 -> _) -> interp_flat_type _ tx2 -> _ with | Tbase T1, Tbase T2 => fun f v => f (SmartBound v) + | Unit, _ => fun f _ => f tt | Prod A1 B1, Prod A2 B2 => fun f v => @bound_var @@ -102,30 +108,50 @@ Section language. (fst v) | Tbase _, _ | Prod _ _, _ - => fun f _ => f (SmartValf _ (fun t => Const (t:=Tbase _) (@failv t)) _) + => fun f _ => f (SmartValf _ (fun t => failf _) _) end. Definition mapf_interp_cast_with_cast_op - {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) - : @exprf base_type_code1 interp_base_type1 op1 ovar (@new_flat_type _ (interpf interp_op2 e2)) + {t1} (e1 : @exprf base_type_code1 op1 ivarf t1) + {t2} (e2 : @exprf base_type_code2 op2 interp_base_type2 t2) + : @exprf base_type_code1 op1 ovar (@new_flat_type _ (interpf interp_op2 e2)) := @mapf_interp_cast - base_type_code1 base_type_code2 interp_base_type1 interp_base_type2 op1 op2 - interp_op2 (@failv) new_base_type transfer_base_const bound_op + base_type_code1 base_type_code2 interp_base_type2 op1 op2 + interp_op2 (@failv) new_base_type bound_op ovar bound_var t1 e1 t2 e2. Definition map_interp_cast_with_cast_op - {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) : 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)) + @expr base_type_code1 op1 ovar (@new_type _ args2 (interp interp_op2 e2)) := @map_interp_cast - base_type_code1 base_type_code2 interp_base_type1 interp_base_type2 op1 op2 - interp_op2 (@failv) new_base_type transfer_base_const bound_op + base_type_code1 base_type_code2 interp_base_type2 op1 op2 + interp_op2 (@failv) new_base_type bound_op ovar bound_var t1 e1 t2 e2. End with_var. End language. -Global Arguments mapf_interp_cast_with_cast_op {_ _ _ _ _ _ _} base_type_code1_beq base_type_code1_bl failv {_} transfer_base_const Cast is_cast new_op {ovar} {t1} e1 {t2} e2. -Global Arguments map_interp_cast_with_cast_op {_ _ _ _ _ _ _} base_type_code1_beq base_type_code1_bl failv {_} transfer_base_const Cast is_cast new_op {ovar} {t1} e1 {t2} e2 args2. +Global Arguments mapf_interp_cast_with_cast_op {_ _ _ _ _ _} base_type_code1_beq base_type_code1_bl failv {_} Cast is_cast new_op {ovar} {t1} e1 {t2} e2. +Global Arguments map_interp_cast_with_cast_op {_ _ _ _ _ _} base_type_code1_beq base_type_code1_bl failv {_} Cast is_cast new_op {ovar} {t1} e1 {t2} e2 args2. + +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) + (base_type_code_beq : base_type_code -> base_type_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) + (failv : forall {var t}, @exprf base_type_code op var (Tbase t)) + {new_base_type : forall t, interp_base_type2 t -> base_type_code} + (Cast : forall var t1 t2, @exprf base_type_code op var (Tbase t1) + -> @exprf base_type_code op var (Tbase t2)) + (is_cast : forall t1 t2, op t1 t2 -> bool). + Definition MapInterpCastWithCastOp + new_op + {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_with_cast_op base_type_code_beq base_type_code_bl (@failv) Cast is_cast new_op (e _) (e _) args. +End homogenous. diff --git a/src/Reflection/MapInterp.v b/src/Reflection/MapInterp.v deleted file mode 100644 index bdb7c8a25..000000000 --- a/src/Reflection/MapInterp.v +++ /dev/null @@ -1,43 +0,0 @@ -(** * Changing the interp function on PHOAS Representation of Gallina *) -Require Import Coq.Strings.String Coq.Classes.RelationClasses. -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Tactics. -Require Import Crypto.Util.Notations. - -Local Open Scope ctype_scope. -Local Open Scope expr_scope. -Section language. - Context {base_type_code : Type} - {interp_base_type1 interp_base_type2 : base_type_code -> Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (f : forall t, interp_base_type1 t -> interp_base_type2 t). - - Section with_var. - Context {var : base_type_code -> Type}. - - Fixpoint mapf_interp {t} (e : @exprf base_type_code interp_base_type1 op var t) - : @exprf base_type_code interp_base_type2 op var t - := match e in exprf _ _ _ t return exprf _ _ _ t with - | Const tx x => Const (mapf_interp_flat_type f x) - | Var _ x => Var x - | Op _ _ op args => Op op (@mapf_interp _ args) - | LetIn _ ex _ eC => LetIn (@mapf_interp _ ex) (fun x => @mapf_interp _ (eC x)) - | Pair _ ex _ ey => Pair (@mapf_interp _ ex) (@mapf_interp _ ey) - end. - - Fixpoint map_interp {t} (e : @expr base_type_code interp_base_type1 op var t) - : @expr base_type_code interp_base_type2 op var t - := match e in expr _ _ _ t return expr _ _ _ t with - | Return _ x => Return (mapf_interp x) - | Abs _ _ f => Abs (fun x => @map_interp _ (f x)) - end. - End with_var. - - Definition MapInterp {t} (e : @Expr base_type_code interp_base_type1 op t) - : @Expr base_type_code interp_base_type2 op t - := fun var => map_interp (e _). -End language. -Global Arguments mapf_interp {_ _ _ _} f {_ t} e. -Global Arguments map_interp {_ _ _ _} f {_ t} e. -Global Arguments MapInterp {_ _ _ _} f {t} e _. diff --git a/src/Reflection/MapInterpWf.v b/src/Reflection/MapInterpWf.v deleted file mode 100644 index cbe16b7ba..000000000 --- a/src/Reflection/MapInterpWf.v +++ /dev/null @@ -1,59 +0,0 @@ -(** * Well-foundedness of changing the interp function on PHOAS Representation of Gallina *) -Require Import Coq.Strings.String Coq.Classes.RelationClasses. -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.WfRel. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Tactics. -Require Import Crypto.Util.Notations. - -Local Open Scope ctype_scope. -Local Open Scope expr_scope. -Section language. - Context {base_type_code : Type} - {interp_base_type interp_base_type1 interp_base_type2 : base_type_code -> Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (f1 : forall t, interp_base_type t -> interp_base_type1 t) - (f2 : forall t, interp_base_type t -> interp_base_type2 t) - (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop) - (Rf12 : forall t v, R t (f1 t v) (f2 t v)). - - Section with_var. - Context {var1 var2 : base_type_code -> Type}. - - Lemma flat_rel_pointwise2_mapf {t} (v : interp_flat_type interp_base_type t) - : interp_flat_type_rel_pointwise2 - R - (mapf_interp_flat_type f1 v) - (mapf_interp_flat_type f2 v). - Proof. induction t; simpl; auto. Qed. - - Lemma wff_mapf_interp {t e1 e2} G - (Hwf : @wff base_type_code interp_base_type op var1 var2 G t e1 e2) - : wff G (mapf_interp f1 e1) (mapf_interp f1 e2). - Proof. induction Hwf; constructor; auto. Qed. - - Lemma rel_wff_mapf_interp {t e1 e2} G - (Hwf : @wff base_type_code interp_base_type op var1 var2 G t e1 e2) - : rel_wff R G (mapf_interp f1 e1) (mapf_interp f2 e2). - Proof. induction Hwf; constructor; auto using flat_rel_pointwise2_mapf. Qed. - - Lemma wf_map_interp {t e1 e2} G - (Hwf : @wf base_type_code interp_base_type op var1 var2 G t e1 e2) - : wf G (map_interp f1 e1) (map_interp f1 e2). - Proof. induction Hwf; constructor; auto using wff_mapf_interp. Qed. - - Lemma rel_wf_map_interp {t e1 e2} G - (Hwf : @wf base_type_code interp_base_type op var1 var2 G t e1 e2) - : rel_wf R G (map_interp f1 e1) (map_interp f2 e2). - Proof. induction Hwf; constructor; auto using rel_wff_mapf_interp. Qed. - End with_var. - - Lemma WfMapInterp {t e} (Hwf : @Wf base_type_code interp_base_type op t e) - : Wf (MapInterp f1 e). - Proof. repeat intro; apply wf_map_interp, Hwf. Qed. - - Lemma RelWfMapInterp {t e} (Hwf : @Wf base_type_code interp_base_type op t e) - : RelWf R (MapInterp f1 e) (MapInterp f2 e). - Proof. repeat intro; apply rel_wf_map_interp, Hwf. Qed. -End language. diff --git a/src/Reflection/MapWithInterpInfo.v b/src/Reflection/MapWithInterpInfo.v deleted file mode 100644 index e64d2de66..000000000 --- a/src/Reflection/MapWithInterpInfo.v +++ /dev/null @@ -1,215 +0,0 @@ -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.ExprInversion. -Require Import Crypto.Reflection.WfInversion. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Option. - -Local Open Scope ctype_scope. -Local Open Scope expr_scope. -Section language. - Context {base_type_code : Type} - {interp_base_type : base_type_code -> Type} - {op : flat_type base_type_code -> flat_type base_type_code -> Type} - (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst) - (new_type : forall t, interp_base_type t -> base_type_code) - (transfer_constant : forall t v, interp_base_type (new_type t v)) - (transfer_op - : forall src dst (opc : op src dst) - (src' : interp_flat_type interp_base_type src), - op (SmartFlatTypeMap new_type src') - (SmartFlatTypeMap new_type (interp_op src dst opc src'))). - Axiom admit : forall {T}, T. - Section with_var. - Context {ovar : base_type_code -> Type}. - Local Notation ivar t := { v : interp_base_type t & ovar (new_type t v) } (only parsing). - Local Notation ivarf := (fun t => ivar t). - - Fixpoint mapf_interp - {t} (e : @exprf base_type_code interp_base_type op ivarf t) - : { val : interp_flat_type interp_base_type t & @exprf base_type_code interp_base_type op ovar (SmartFlatTypeMap new_type val) }. - Proof. - refine (match e in exprf _ _ _ t - return { val : interp_flat_type _ t & _ } with - | Const tx x - => existT _ x (Const (SmartFlatTypeMapInterp transfer_constant x)) - | Var _ x - => existT _ (projT1 x) (Var admit (* need ≈ CSE / lookup here *)) - | Op _ _ op args - => let mapf_interp_args := @mapf_interp _ args in - existT - _ - (interp_op _ _ op (projT1 mapf_interp_args)) - (Op (transfer_op _ _ op _) (projT2 mapf_interp_args)) - | LetIn _ ex _ eC - => let mapf_interp_ex := @mapf_interp _ ex in - let mapf_interp_eC := fun v => @mapf_interp _ (eC v) in - let impossible1 := admit in - existT - _ - impossible1 (* This is impossible; we need a second expression which lines up nicely here *) - (LetIn - (projT2 mapf_interp_ex) - (fun v => let v' : interp_flat_type ivarf _ := admit in - let impossible : projT1 (mapf_interp_eC v') = impossible1 := admit in - match impossible in _ = y - return exprf _ _ _ (SmartFlatTypeMap new_type y) - with - | eq_refl => projT2 (mapf_interp_eC v') - end)) - | Pair _ ex _ ey - => let mapf_interp_ex := @mapf_interp _ ex in - let mapf_interp_ey := @mapf_interp _ ey in - existT - _ - (projT1 mapf_interp_ex, projT1 mapf_interp_ey)%core - (Pair (projT2 mapf_interp_ex) (projT2 mapf_interp_ey)) - end). - Defined. - - Fixpoint mapf_interp' - {t1} (e1 : @exprf base_type_code interp_base_type op ivarf t1) - {t2} (e2 : @exprf base_type_code interp_base_type op interp_base_type t2) - G - (wf : { pf : t2 = t1 | wff G e1 (eq_rect _ (exprf _ _ _) e2 _ pf) }) - {struct e1} - : @exprf base_type_code interp_base_type op ovar (SmartFlatTypeMap new_type (interpf interp_op e2)). - Proof. - Local Ltac t wf mapf_interp' invert_wff_ex := - let mytac := fun _ - => (try clear mapf_interp'; - try clear invert_wff_ex; - repeat match goal with - | [ H : ex _ |- _ ] => destruct H - | [ H : sig _ |- _ ] => destruct H - | [ H : and _ _ |- _ ] => destruct H - | [ |- ?x = ?x ] => reflexivity - | _ => progress subst - | _ => progress simpl in * - | _ => progress inversion_prod - | _ => progress inversion_option - | _ => progress inversion_wff - | [ H : Pair _ _ = _ |- _ ] - => apply (f_equal invert_Pair) in H - | [ H : LetIn _ _ = _ |- _ ] - => apply (f_equal invert_LetIn) in H - | [ |- exists pf : ?x = ?x, _ ] => exists eq_refl - | [ |- { pf : ?x = ?x | _ } ] => exists eq_refl - | _ => assumption - | [ H : Prod ?A ?B = Prod ?A' ?B' |- _ ] - => let A'' := fresh A' in (* TODO: Find a better way to do this *) - let B'' := fresh B' in - revert dependent H; intro H; move H at top; - revert dependent B'; intros B'' H; move H at top; - revert dependent A'; intros A'' H; move H at top; - refine (match H with eq_refl => _ end); clear A'' B'' H; - intros - | [ H : Tbase ?A = Tbase ?A' |- _ ] - => let A'' := fresh A' in (* TODO: Find a better way to do this *) - revert dependent H; intro H; move H at top; - revert dependent A'; intros A'' H; move H at top; - refine (match H with eq_refl => _ end); clear A'' H; - intros - | _ => solve [ auto with nocore ] - end) in - lazymatch goal with - | [ |- False ] - => clear -wf; - abstract ( - destruct wf as [pf H]; (subst || inversion pf); simpl @eq_rect in *; - clear -H; inversion H - ) - | [ |- sig _ ] => mytac () - | [ |- ex _ ] => mytac () - | [ |- _ = _ ] => mytac () - | _ => idtac - end. - revert wf. - refine (match e1 in exprf _ _ _ t1, e2 in exprf _ _ _ t2 - return { pf : t2 = t1 | wff _ e1 (eq_rect _ _ e2 _ pf) } -> exprf _ _ _ (SmartFlatTypeMap _ (interpf _ e2)) with - | Const tx1 x1, Const tx2 x2 - => fun wf => Const (SmartFlatTypeMapInterp transfer_constant _) - | Var _ x1, Var _ x2 - => fun wf => Var admit (* need something ≈ CSE here? *) - | Op _ _ op1 args1, Op _ _ op2 args2 - => fun wf - => let invert_wff := _ in - let mapf_interp'_args := @mapf_interp' _ args1 _ args2 G invert_wff in - Op - (transfer_op _ _ op2 _) - mapf_interp'_args - | LetIn _ ex1 _ eC1, LetIn _ ex2 _ eC2 - => fun wf - => let invert_wff_ex := _ in - let invert_wff_eC := _ in - let mapf_interp'_ex := @mapf_interp' _ ex1 _ ex2 G invert_wff_ex in - let mapf_interp'_eC := fun v1 v2 (pf : _ = _) => @mapf_interp' _ (eC1 v1) _ (eC2 v2) (flatten_binding_list base_type_code v1 (eq_rect _ _ v2 _ pf) ++ G)%list (invert_wff_eC v1 v2 pf) in - LetIn - mapf_interp'_ex - (fun v => let v1 := _ in - let v2 := _ in - let pf := _ in - mapf_interp'_eC v1 v2 pf) - | Pair _ ex1 _ ey1, Pair _ ex2 _ ey2 - => fun wf - => let invert_wff_ex := _ in - let invert_wff_ey := _ in - let mapf_interp'_ex := @mapf_interp' _ ex1 _ ex2 G invert_wff_ex in - let mapf_interp'_ey := @mapf_interp' _ ey1 _ ey2 G invert_wff_ey in - Pair mapf_interp'_ex mapf_interp'_ey - | Const _ _, _ - | Var _ _, _ - | Op _ _ _ _, _ - | LetIn _ _ _ _, _ - | Pair _ _ _ _, _ - => fun wf => match _ : False with end - end); - t wf mapf_interp' invert_wff_ex; admit. - (* - Grab Existential Variables. - { t wf mapf_interp' invert_wff_ex. } - { repeat match goal with - | [ H := _ |- _ ] => clearbody H - | [ H : ex _ |- _ ] => destruct H - | [ H : sig _ |- _ ] => destruct H - | _ => progress subst - | _ => progress simpl in * - end. - clear -v. - refine (SmartFlatTypeMapUnInterp - (fun t x (p : ovar (new_type t x)) => existT _ x p) - v). } - { intros; t wf (@mapf_interp') invert_wff_ex. - match goal with - | [ H : ?x = ?x |- _ ] => assert (eq_refl = H) by exact admit; subst (* XXX TODO: FIXME *) - end. - simpl in *; auto. } - { t wf mapf_interp' invert_wff_ex. }*) - Admitted. - - (* - Fixpoint mapf_interp {t} (e : @exprf base_type_code interp_base_type1 op var t) - : @exprf base_type_code interp_base_type2 op var t - := match e in exprf _ _ _ t return exprf _ _ _ t with - | Const tx x => Const (mapf_interp_flat_type f x) - | Var _ x => Var x - | Op _ _ op args => Op op (@mapf_interp _ args) - | LetIn _ ex _ eC => LetIn (@mapf_interp _ ex) (fun x => @mapf_interp _ (eC x)) - | Pair _ ex _ ey => Pair (@mapf_interp _ ex) (@mapf_interp _ ey) - end. - - Fixpoint map_interp {t} (e : @expr base_type_code interp_base_type1 op var t) - : @expr base_type_code interp_base_type2 op var t - := match e in expr _ _ _ t return expr _ _ _ t with - | Return _ x => Return (mapf_interp x) - | Abs _ _ f => Abs (fun x => @map_interp _ (f x)) - end.*) - End with_var. - - (*Definition MapInterp {t} (e : @Expr base_type_code interp_base_type1 op t) - : @Expr base_type_code interp_base_type2 op t - := fun var => map_interp (e _).*) -End language. -(*Global Arguments mapf_interp {_ _ _ _} f {_ t} e. -Global Arguments map_interp {_ _ _ _} f {_ t} e. -Global Arguments MapInterp {_ _ _ _} f {t} e _.*) 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 => diff --git a/src/Reflection/Named/Compile.v b/src/Reflection/Named/Compile.v index 973b2b2e7..7ffc5fded 100644 --- a/src/Reflection/Named/Compile.v +++ b/src/Reflection/Named/Compile.v @@ -10,25 +10,20 @@ Local Open Scope nexpr_scope. Local Open Scope expr_scope. Section language. Context (base_type_code : Type) - (interp_base_type : base_type_code -> Type) (op : flat_type base_type_code -> flat_type base_type_code -> Type) (Name : Type). Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op (fun _ => Name)). - Local Notation expr := (@expr base_type_code interp_base_type op (fun _ => Name)). - Local Notation nexprf := (@Named.exprf base_type_code interp_base_type op Name). - Local Notation nexpr := (@Named.expr base_type_code interp_base_type op Name). + Local Notation exprf := (@exprf base_type_code op (fun _ => Name)). + Local Notation expr := (@expr base_type_code op (fun _ => Name)). + Local Notation nexprf := (@Named.exprf base_type_code op Name). + Local Notation nexpr := (@Named.expr base_type_code op Name). Fixpoint ocompilef {t} (e : exprf t) (ls : list (option Name)) {struct e} : option (nexprf t) - := match e in @Syntax.exprf _ _ _ _ t return option (nexprf t) with - | Const _ x => Some (Named.Const x) + := match e in @Syntax.exprf _ _ _ t return option (nexprf t) with + | TT => Some Named.TT | Var _ x => Some (Named.Var x) | Op _ _ op args => option_map (Named.Op op) (@ocompilef _ args ls) | LetIn tx ex _ eC @@ -45,7 +40,7 @@ Section language. Fixpoint ocompile {t} (e : expr t) (ls : list (option Name)) {struct e} : option (nexpr t) - := match e in @Syntax.expr _ _ _ _ t return option (nexpr t) with + := match e in @Syntax.expr _ _ _ t return option (nexpr t) with | Return _ x => option_map Named.Return (ocompilef x ls) | Abs _ _ f => match ls with @@ -59,7 +54,7 @@ Section language. Definition compile {t} (e : expr t) (ls : list Name) := @ocompile t e (List.map (@Some _) ls). End language. -Global Arguments ocompilef {_ _ _ _ _} e ls. -Global Arguments ocompile {_ _ _ _ _} e ls. -Global Arguments compilef {_ _ _ _ _} e ls. -Global Arguments compile {_ _ _ _ _} e ls. +Global Arguments ocompilef {_ _ _ _} e ls. +Global Arguments ocompile {_ _ _ _} e ls. +Global Arguments compilef {_ _ _ _} e ls. +Global Arguments compile {_ _ _ _} e ls. diff --git a/src/Reflection/Named/DeadCodeElimination.v b/src/Reflection/Named/DeadCodeElimination.v index a2b39347c..d48c0bbbe 100644 --- a/src/Reflection/Named/DeadCodeElimination.v +++ b/src/Reflection/Named/DeadCodeElimination.v @@ -16,28 +16,23 @@ Local Open Scope nexpr_scope. Local Open Scope expr_scope. Section language. Context (base_type_code : Type) - (interp_base_type : base_type_code -> Type) (op : flat_type base_type_code -> flat_type base_type_code -> Type) (Name : Type) {Context : Context Name (fun _ : base_type_code => positive)}. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op (fun _ => Name)). - Local Notation expr := (@expr base_type_code interp_base_type op (fun _ => Name)). - Local Notation Expr := (@Expr base_type_code interp_base_type op). - (*Local Notation lexprf := (@Syntax.exprf base_type_code interp_base_type op (fun _ => list (option Name))). - Local Notation lexpr := (@Syntax.expr base_type_code interp_base_type op (fun _ => list (option Name))).*) - Local Notation nexprf := (@Named.exprf base_type_code interp_base_type op Name). - Local Notation nexpr := (@Named.expr base_type_code interp_base_type op Name). + Local Notation exprf := (@exprf base_type_code op (fun _ => Name)). + Local Notation expr := (@expr base_type_code op (fun _ => Name)). + Local Notation Expr := (@Expr base_type_code op). + (*Local Notation lexprf := (@Syntax.exprf base_type_code op (fun _ => list (option Name))). + Local Notation lexpr := (@Syntax.expr base_type_code op (fun _ => list (option Name))).*) + Local Notation nexprf := (@Named.exprf base_type_code op Name). + Local Notation nexpr := (@Named.expr base_type_code op Name). (*Definition get_live_namesf (names : list (option Name)) {t} (e : lexprf t) : list (option Name) := filter_live_namesf - base_type_code interp_base_type op + base_type_code op (option Name) None (fun x y => match x, y with | Some x, _ => Some x @@ -47,7 +42,7 @@ Section language. nil names e. Definition get_live_names (names : list (option Name)) {t} (e : lexpr t) : list (option Name) := filter_live_names - base_type_code interp_base_type op + base_type_code op (option Name) None (fun x y => match x, y with | Some x, _ => Some x @@ -67,4 +62,4 @@ Section language. end. End language. -Global Arguments CompileAndEliminateDeadCode {_ _ _ _ _ t} e ls. +Global Arguments CompileAndEliminateDeadCode {_ _ _ _ t} e ls. diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v index b2be2d19b..7822985e1 100644 --- a/src/Reflection/Named/EstablishLiveness.v +++ b/src/Reflection/Named/EstablishLiveness.v @@ -29,17 +29,12 @@ Fixpoint merge_liveness (ls1 ls2 : list liveness) := Section language. Context (base_type_code : Type) - (interp_base_type : 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). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). + Local Notation exprf := (@exprf base_type_code op). + Local Notation expr := (@expr base_type_code op). Section internal. Context (Name : Type) @@ -52,8 +47,8 @@ Section language. {t} (e : exprf Name t) (prefix : list liveness) : list liveness := match e with - | Const _ x => prefix - | Var t' name => match lookup ctx t' name with + | TT => prefix + | Var t' name => match lookup ctx (Tbase t') name with | Some ls => ls | _ => nil end @@ -78,8 +73,8 @@ Section language. := match e with | Return _ x => compute_livenessf ctx x prefix | Abs src _ n f - => let prefix := prefix ++ (live::nil) in - let ctx := extendb (t:=src) ctx n prefix in + => let prefix := prefix ++ repeat live (count_pairs (Tbase src)) in + let ctx := extend (t:=Tbase src) ctx n (SmartValf _ (fun _ => prefix) (Tbase src)) in @compute_liveness ctx _ f prefix end. @@ -104,6 +99,6 @@ Section language. End internal. End language. -Global Arguments compute_livenessf {_ _ _ _ _} ctx {t} e prefix. -Global Arguments compute_liveness {_ _ _ _ _} ctx {t} e prefix. -Global Arguments insert_dead_names {_ _ _ _ _ _} default_out {t} e lsn. +Global Arguments compute_livenessf {_ _ _ _} ctx {t} e prefix. +Global Arguments compute_liveness {_ _ _ _} ctx {t} e prefix. +Global Arguments insert_dead_names {_ _ _ _ _} default_out {t} e lsn. diff --git a/src/Reflection/Named/NameUtil.v b/src/Reflection/Named/NameUtil.v index d9ef0f9b1..9d910aaef 100644 --- a/src/Reflection/Named/NameUtil.v +++ b/src/Reflection/Named/NameUtil.v @@ -13,7 +13,7 @@ Section language. (t : flat_type base_type_code) (ls : list MName) : option (interp_flat_type (fun _ => Name) t) * list MName := match t return option (@interp_flat_type base_type_code (fun _ => Name) t) * _ with - | Syntax.Tbase _ + | Tbase _ => match ls with | cons n ls' => match force n with @@ -22,6 +22,7 @@ Section language. end | nil => (None, nil) end + | Unit => (Some tt, ls) | Prod A B => let '(a, ls) := eta (@split_mnames A ls) in let '(b, ls) := eta (@split_mnames B ls) in diff --git a/src/Reflection/Named/RegisterAssign.v b/src/Reflection/Named/RegisterAssign.v index 749019fa4..ce8188ee5 100644 --- a/src/Reflection/Named/RegisterAssign.v +++ b/src/Reflection/Named/RegisterAssign.v @@ -11,17 +11,12 @@ Local Open Scope ctype_scope. Delimit Scope nexpr_scope with nexpr. Section language. Context (base_type_code : Type) - (interp_base_type : 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). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). + Local Notation exprf := (@exprf base_type_code op). + Local Notation expr := (@expr base_type_code op). Section internal. Context (InName OutName : Type) @@ -36,8 +31,8 @@ Section language. (ctxi : InContext) (ctxr : ReverseContext) {t} (e : exprf InName t) (new_names : list (option OutName)) : option (exprf OutName t) - := match e in Named.exprf _ _ _ _ t return option (exprf _ t) with - | Const _ x => Some (Const x) + := match e in Named.exprf _ _ _ t return option (exprf _ t) with + | TT => Some TT | Var t' name => match lookupb ctxi name t' with | Some new_name => match lookupb ctxr new_name t' with @@ -75,10 +70,10 @@ Section language. Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext) {t} (e : expr InName t) (new_names : list (option OutName)) : option (expr OutName t) - := match e in Named.expr _ _ _ _ t return option (expr _ t) with + := match e in Named.expr _ _ _ t return option (expr _ t) with | Return _ x => option_map Return (register_reassignf ctxi ctxr x new_names) | Abs src _ n f - => let '(n', new_names') := eta (split_onames src new_names) in + => let '(n', new_names') := eta (split_onames (Tbase src) new_names) in match n' with | Some n' => let ctxi := extendb (t:=src) ctxi n n' in @@ -120,5 +115,5 @@ End language. Global Arguments pos_context {_ _} var. Global Arguments pos_context_nd : clear implicits. -Global Arguments register_reassign {_ _ _ _ _ _ _} _ ctxi ctxr {t} e _. -Global Arguments register_reassignf {_ _ _ _ _ _ _} _ ctxi ctxr {t} e _. +Global Arguments register_reassign {_ _ _ _ _ _} _ ctxi ctxr {t} e _. +Global Arguments register_reassignf {_ _ _ _ _ _} _ ctxi ctxr {t} e _. diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v index e77947693..f6ce5d1f5 100644 --- a/src/Reflection/Named/Syntax.v +++ b/src/Reflection/Named/Syntax.v @@ -31,8 +31,6 @@ Module Export Named. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. Local Notation interp_type := (interp_type interp_base_type). Local Notation interp_flat_type_gen := interp_flat_type. Local Notation interp_flat_type := (interp_flat_type interp_base_type). @@ -41,8 +39,8 @@ Module Export Named. Section expr_param. Section expr. Inductive exprf : flat_type -> Type := - | Const {t : flat_type} : interp_type t -> exprf t - | Var {t : base_type_code} : Name -> exprf t + | TT : exprf Unit + | Var {t : base_type_code} : Name -> exprf (Tbase t) | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR | LetIn : forall {tx}, interp_flat_type_gen (fun _ => Name) tx -> exprf tx -> forall {tC}, exprf tC -> exprf tC | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2). @@ -56,9 +54,7 @@ Module Export Named. pair-projections and [Pair] as necessary to handle [flat_type], and not just [base_type_code] *) Definition SmartVar {t} : interp_flat_type_gen (fun _ => Name) t -> exprf t - := smart_interp_flat_map (f:=fun _ => Name) (g:=exprf) _ (fun t => Var) (fun A B x y => Pair x y). - Definition SmartConst {t} : interp_flat_type t -> @interp_flat_type_gen base_type_code exprf t - := smart_interp_flat_map (g:=@interp_flat_type_gen base_type_code exprf) _ (fun t => Const (t:=t)) (fun A B x y => pair x y). + := smart_interp_flat_map (f:=fun _ => Name) (g:=exprf) _ (fun t => Var) TT (fun A B x y => Pair x y). End expr. Section with_context. @@ -69,7 +65,8 @@ Module Export Named. (n : interp_flat_type_gen (fun _ => Name) t) (v : interp_flat_type_gen var t) : Context := match t return interp_flat_type_gen (fun _ => Name) t -> interp_flat_type_gen var t -> Context with - | Syntax.Tbase t => fun n v => extendb ctx n v + | Tbase t => fun n v => extendb ctx n v + | Unit => fun _ _ => ctx | Prod A B => fun n v => let ctx := @extend ctx A (fst n) (fst v) in let ctx := @extend ctx B (snd n) (snd v) in @@ -80,7 +77,8 @@ Module Export Named. (n : interp_flat_type_gen (fun _ => Name) t) : Context := match t return interp_flat_type_gen (fun _ => Name) t -> Context with - | Syntax.Tbase t => fun n => removeb ctx n t + | Tbase t => fun n => removeb ctx n t + | Unit => fun _ => ctx | Prod A B => fun n => let ctx := @remove ctx A (fst n) in let ctx := @remove ctx B (snd n) in @@ -93,6 +91,7 @@ Module Export Named. base_type_code (g := fun t => option (interp_flat_type_gen var t)) (fun t v => lookupb ctx v) + (Some tt) (fun A B x y => match x, y with | Some x', Some y' => Some (x', y')%core | _, _ => None @@ -101,7 +100,7 @@ Module Export Named. Section wf. Fixpoint wff (ctx : Context) {t} (e : exprf t) : option pointed_Prop := match e with - | Const _ x => Some trivial + | TT => Some trivial | Var t n => match lookupb ctx n t return bool with | Some _ => true | None => false @@ -114,14 +113,14 @@ Module Export Named. Fixpoint wf (ctx : Context) {t} (e : expr t) : Prop := match e with | Return _ x => prop_of_option (wff ctx x) - | Abs src _ n f => forall v, @wf (extend ctx (t:=src) n v) _ f + | Abs src _ n f => forall v, @wf (extend ctx (t:=Tbase src) n v) _ f end. End wf. Section interp_gen. Context (output_interp_flat_type : flat_type -> Type) - (interp_const : forall t, interp_flat_type t -> output_interp_flat_type t) - (interp_var : forall t, var t -> output_interp_flat_type t) + (interp_tt : output_interp_flat_type Unit) + (interp_var : forall t, var t -> output_interp_flat_type (Tbase t)) (interp_op : forall src dst, op src dst -> output_interp_flat_type src -> output_interp_flat_type dst) (interp_let : forall (tx : flat_type) (ex : output_interp_flat_type tx) tC (eC : interp_flat_type_gen var tx -> output_interp_flat_type tC), @@ -133,13 +132,13 @@ Module Export Named. Fixpoint interp_genf (ctx : Context) {t} (e : exprf t) : prop_of_option (wff ctx e) -> output_interp_flat_type t := match e in exprf t return prop_of_option (wff ctx e) -> output_interp_flat_type t with - | Const _ x => fun _ => interp_const _ x + | TT => fun _ => interp_tt | Var t' x => match lookupb ctx x t' as v return prop_of_option (match v return bool with | Some _ => true | None => false end) - -> output_interp_flat_type t' + -> output_interp_flat_type (Tbase t') with | Some v => fun _ => interp_var _ v | None => fun bad => match bad : False with end @@ -164,7 +163,7 @@ Module Export Named. prop_of_option (wff ctx e) -> interp_flat_type t := @interp_genf interp_base_type Context interp_flat_type - (fun _ x => x) (fun _ x => x) interp_op (fun _ y _ f => let x := y in f x) + tt (fun _ x => x) interp_op (fun _ y _ f => let x := y in f x) (fun _ x _ y => (x, y)%core). Fixpoint interp (ctx : Context) {t} (e : expr t) @@ -178,24 +177,24 @@ Module Export Named. End language. End Named. -Global Arguments Const {_ _ _ _ _} _. -Global Arguments Var {_ _ _ _ _} _. -Global Arguments SmartVar {_ _ _ _ _} _. -Global Arguments SmartConst {_ _ _ _ _} _. -Global Arguments Op {_ _ _ _ _ _} _ _. -Global Arguments LetIn {_ _ _ _} _ _ _ {_} _. -Global Arguments Pair {_ _ _ _ _} _ {_} _. -Global Arguments Return {_ _ _ _ _} _. -Global Arguments Abs {_ _ _ _ _ _} _ _. +Global Arguments TT {_ _ _}. +Global Arguments Var {_ _ _ _} _. +Global Arguments SmartVar {_ _ _ _} _. +Global Arguments Op {_ _ _ _ _} _ _. +Global Arguments LetIn {_ _ _} _ _ _ {_} _. +Global Arguments Pair {_ _ _ _} _ {_} _. +Global Arguments Return {_ _ _ _} _. +Global Arguments Abs {_ _ _ _ _} _ _. Global Arguments extend {_ _ _ _} ctx {_} _ _. Global Arguments remove {_ _ _ _} ctx {_} _. Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _. -Global Arguments wff {_ _ _ _ _ _} ctx {t} _. -Global Arguments wf {_ _ _ _ _ _} ctx {t} _. -Global Arguments interp_genf {_ _ _ _ var _} _ _ _ _ _ _ {ctx t} _ _. +Global Arguments wff {_ _ _ _ _} ctx {t} _. +Global Arguments wf {_ _ _ _ _} ctx {t} _. +Global Arguments interp_genf {_ _ _ var _} _ _ _ _ _ _ {ctx t} _ _. Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _ _. Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _. Notation "'slet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope. Notation "'λn' x .. y , t" := (Abs x .. (Abs y t%nexpr) .. ) : nexpr_scope. Notation "( x , y , .. , z )" := (Pair .. (Pair x%nexpr y%nexpr) .. z%nexpr) : nexpr_scope. +Notation "()" := TT : nexpr_scope. diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 1a2f22eca..7da426d50 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -3,12 +3,54 @@ judgmental equality of the denotation of the reified term. *) Require Import Coq.Strings.String. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.InputSyntax. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. +(** Change this with [Ltac reify_debug_level ::= constr:(1).] to get + more debugging. *) +Ltac reify_debug_level := constr:(0). +Module Import ReifyDebugNotations. + Export Reflection.Syntax.Notations. + Export Util.LetIn. + Open Scope string_scope. +End ReifyDebugNotations. + +Ltac debug_enter_reify_idtac funname e := + let s := (eval compute in (String.append funname ": Attempting to reify:")) in + cidtac2 s e. +Ltac debug_reifyf_case_idtac case := + let s := (eval compute in (String.append "reifyf: " case)) in + cidtac s. +Ltac debug1 tac := + let lvl := reify_debug_level in + match lvl with + | S _ => tac () + | _ => constr:(Set) + end. +Ltac debug2 tac := + let lvl := reify_debug_level in + match lvl with + | S (S _) => tac () + | _ => constr:(Set) + end. +Ltac debug3 tac := + let lvl := reify_debug_level in + match lvl with + | S (S (S _)) => tac () + | _ => constr:(Set) + end. +Ltac debug_enter_reify2 funname e := debug2 ltac:(fun _ => debug_enter_reify_idtac funname e). +Ltac debug_enter_reify3 funname e := debug2 ltac:(fun _ => debug_enter_reify_idtac funname e). +Ltac debug_enter_reify_flat_type e := debug_enter_reify3 "reify_flat_type" e. +Ltac debug_enter_reify_type e := debug_enter_reify3 "reify_type" e. +Ltac debug_enter_reifyf e := debug_enter_reify2 "reifyf" e. +Ltac debug_reifyf_case case := debug3 ltac:(fun _ => debug_reifyf_case_idtac case). +Ltac debug_enter_reify_abs e := debug_enter_reify2 "reify_abs" e. + Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T. Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False. Arguments reify_var_for_in_is _ {T} _ _ {eT} _. @@ -29,6 +71,7 @@ Ltac base_reify_type T := strip_type_cast (_ : reify type T). Ltac reify_base_type T := base_reify_type T. Ltac reify_flat_type T := + let dummy := debug_enter_reify_flat_type T in lazymatch T with | prod ?A ?B => let a := reify_flat_type A in @@ -39,6 +82,7 @@ Ltac reify_flat_type T := constr:(@Tbase _ v) end. Ltac reify_type T := + let dummy := debug_enter_reify_type T in lazymatch T with | (?A -> ?B)%type => let a := reify_base_type A in @@ -75,26 +119,6 @@ Ltac reify_op op op_head expr := let t := base_reify_op op op_head expr in constr:(op_info t). -(** Change this with [Ltac reify_debug_level ::= constr:(1).] to get - more debugging. *) -Ltac reify_debug_level := constr:(0). -Module Import ReifyDebugNotations. - Open Scope string_scope. -End ReifyDebugNotations. - -Ltac debug_enter_reifyf e := - let lvl := reify_debug_level in - match lvl with - | S (S _) => cidtac2 "reifyf: Attempting to reify:" e - | _ => constr:(Set) - end. -Ltac debug_enter_reify_abs e := - let lvl := reify_debug_level in - match lvl with - | S (S _) => cidtac2 "reify_abs: Attempting to reify:" e - | _ => constr:(Set) - end. - Ltac debug_enter_reify_rec := let lvl := reify_debug_level in match lvl with @@ -120,18 +144,22 @@ Ltac reifyf base_type_code interp_base_type op var e := let dummy := debug_enter_reifyf e in lazymatch e with | let x := ?ex in @?eC x => + let dummy := debug_reifyf_case "let in" in let ex := reify_rec ex in let eC := reify_rec eC in mkLetIn ex eC - | dlet x := ?ex in @?eC x => + | (dlet x := ?ex in @?eC x) => + let dummy := debug_reifyf_case "dlet in" in let ex := reify_rec ex in let eC := reify_rec eC in mkLetIn ex eC | pair ?a ?b => + let dummy := debug_reifyf_case "pair" in let a := reify_rec a in let b := reify_rec b in mkPair a b | (fun x : ?T => ?C) => + let dummy := debug_reifyf_case "fun" in let t := reify_flat_type T in (* Work around Coq 8.5 and 8.6 bug *) (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *) @@ -143,11 +171,13 @@ Ltac reifyf base_type_code interp_base_type op var e := (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *) with fun _ v _ => @?C v => C end | match ?ev with pair a b => @?eC a b end => + let dummy := debug_reifyf_case "matchpair" in let t := (let T := match type of eC with _ -> _ -> ?T => T end in reify_flat_type T) in let v := reify_rec ev in let C := reify_rec eC in mkMatchPair t v C | ?x => + let dummy := debug_reifyf_case "generic" in let t := lazymatch type of x with ?t => reify_flat_type t end in let retv := match constr:(Set) with | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv) @@ -247,9 +277,9 @@ Ltac Reify' base_type_code interp_base_type op e := lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with (fun var => ?C) => constr:(fun (var : flat_type base_type_code -> Type) => C) (* copy the term but not the type cast *) end. -Ltac Reify base_type_code interp_base_type op e := +Ltac Reify base_type_code interp_base_type op make_const e := let r := Reify' base_type_code interp_base_type op e in - constr:(@InputSyntax.Compile base_type_code interp_base_type op _ r). + constr:(@InputSyntax.Compile base_type_code interp_base_type op make_const _ r). Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end. Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end. @@ -290,15 +320,16 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := Ltac prove_compile_correct := fun _ => lazymatch goal with - | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ] - => exact (@InputSyntax.Compile_flat_correct base_type_code interp_base_type op interp_op t e) - | [ |- interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (@Compile _ _ _ _ ?e)) _ ] - => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e) - end. + | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ ?make_const _ ?e) = _ ] + => apply (fun pf => @InputSyntax.Compile_flat_correct base_type_code interp_base_type op make_const interp_op pf t e) + | [ |- interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (@Compile _ _ _ ?make_const _ ?e)) _ ] + => apply (fun pf => @InputSyntax.Compile_correct base_type_code interp_base_type op make_const interp_op pf t e) + end; + let T := fresh in intro T; destruct T; reflexivity. -Ltac Reify_rhs base_type_code interp_base_type op interp_op := +Ltac Reify_rhs base_type_code interp_base_type op make_const interp_op := Reify_rhs_gen - ltac:(Reify base_type_code interp_base_type op) + ltac:(Reify base_type_code interp_base_type op make_const) prove_compile_correct interp_op ltac:(fun tac => tac ()). diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v new file mode 100644 index 000000000..bc8b58f35 --- /dev/null +++ b/src/Reflection/Relations.v @@ -0,0 +1,147 @@ +Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Util.Tactics. + +Local Open Scope ctype_scope. +Section language. + Context {base_type_code : Type}. + + Let Tbase := (@Tbase base_type_code). + Local Coercion Tbase : base_type_code >-> flat_type. + Local Notation flat_type := (flat_type base_type_code). + Local Notation type := (type base_type_code). + + Section type. + Context (interp_flat_type : flat_type -> Type) + (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop). + Local Notation interp_type_gen := (interp_type_gen interp_flat_type). + Fixpoint interp_type_gen_rel_pointwise (t : type) + : interp_type_gen t -> interp_type_gen t -> Prop := + match t with + | Tflat t => R t + | Arrow _ y => fun f g => forall x, interp_type_gen_rel_pointwise y (f x) (g x) + end. + Global Instance interp_type_gen_rel_pointwise_Reflexive {H : forall t, Reflexive (R t)} + : forall t, Reflexive (interp_type_gen_rel_pointwise t). + Proof. induction t; repeat intro; reflexivity. Qed. + Global Instance interp_type_gen_rel_pointwise_Symmetric {H : forall t, Symmetric (R t)} + : forall t, Symmetric (interp_type_gen_rel_pointwise t). + Proof. induction t; simpl; repeat intro; symmetry; eauto. Qed. + Global Instance interp_type_gen_rel_pointwise_Transitive {H : forall t, Transitive (R t)} + : forall t, Transitive (interp_type_gen_rel_pointwise t). + Proof. induction t; simpl; repeat intro; etransitivity; eauto. Qed. + End type. + + Section flat_type. + Context {interp_base_type : base_type_code -> Type} + (R : forall t, interp_base_type t -> interp_base_type t -> Prop). + Local Notation interp_flat_type := (interp_flat_type interp_base_type). + Fixpoint interp_flat_type_rel_pointwise (t : flat_type) + : interp_flat_type t -> interp_flat_type t -> Prop := + match t with + | Syntax.Tbase t => R t + | Unit => fun _ _ => True + | Prod _ _ => fun x y => interp_flat_type_rel_pointwise _ (fst x) (fst y) + /\ interp_flat_type_rel_pointwise _ (snd x) (snd y) + end. + Definition interp_type_rel_pointwise + := interp_type_gen_rel_pointwise _ interp_flat_type_rel_pointwise. + End flat_type. + + Section rel_pointwise2. + Section type. + Section hetero. + Context (interp_src1 interp_src2 : base_type_code -> Type) + (interp_dst1 interp_dst2 : flat_type -> Type) + (Rsrc : forall t, interp_src1 t -> interp_src2 t -> Prop) + (Rdst : forall t, interp_dst1 t -> interp_dst2 t -> Prop). + + Fixpoint interp_type_gen_rel_pointwise2_hetero (t : type) + : interp_type_gen_hetero interp_src1 interp_dst1 t + -> interp_type_gen_hetero interp_src2 interp_dst2 t + -> Prop + := match t with + | Tflat t => Rdst t + | Arrow src dst => @respectful_hetero _ _ _ _ (Rsrc src) (fun _ _ => interp_type_gen_rel_pointwise2_hetero dst) + end. + End hetero. + Section homogenous. + Context (interp_flat_type1 interp_flat_type2 : flat_type -> Type) + (R : forall t, interp_flat_type1 t -> interp_flat_type2 t -> Prop). + + Definition interp_type_gen_rel_pointwise2 + : forall t, + interp_type_gen interp_flat_type1 t + -> interp_type_gen interp_flat_type2 t + -> Prop + := interp_type_gen_rel_pointwise2_hetero interp_flat_type1 interp_flat_type2 + interp_flat_type1 interp_flat_type2 + R R. + End homogenous. + End type. + Section flat_type. + Context (interp_base_type1 interp_base_type2 : base_type_code -> Type). + Section gen_prop. + Context (P : Type) + (and : P -> P -> P) + (True : P) + (R : forall t, interp_base_type1 t -> interp_base_type2 t -> P). + + Fixpoint interp_flat_type_rel_pointwise2_gen_Prop (t : flat_type) + : interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> P + := match t with + | Syntax.Tbase t => R t + | Unit => fun _ _ => True + | Prod x y => fun a b => and (interp_flat_type_rel_pointwise2_gen_Prop x (fst a) (fst b)) + (interp_flat_type_rel_pointwise2_gen_Prop y (snd a) (snd b)) + end. + End gen_prop. + + Definition interp_flat_type_rel_pointwise2 + := @interp_flat_type_rel_pointwise2_gen_Prop Prop and True. + + Definition interp_type_rel_pointwise2 R + : forall t, interp_type interp_base_type1 t + -> interp_type interp_base_type2 t + -> Prop + := interp_type_gen_rel_pointwise2 _ _ (interp_flat_type_rel_pointwise2 R). + End flat_type. + End rel_pointwise2. + + Section lifting. + Section flat_type. + Context {interp_base_type : base_type_code -> Type}. + Local Notation interp_flat_type := (interp_flat_type interp_base_type). + Context (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop) + (RUnit : R Unit tt tt). + Section RProd. + Context (RProd : forall A B x y, R A (fst x) (fst y) /\ R B (snd x) (snd y) -> R (Prod A B) x y) + (RProd' : forall A B x y, R (Prod A B) x y -> R A (fst x) (fst y) /\ R B (snd x) (snd y)). + Lemma lift_interp_flat_type_rel_pointwise1 t (x y : interp_flat_type t) + : interp_flat_type_rel_pointwise R t x y -> R t x y. + Proof. clear RProd'; induction t; simpl; destruct_head_hnf' unit; intuition. Qed. + Lemma lift_interp_flat_type_rel_pointwise2 t (x y : interp_flat_type t) + : R t x y -> interp_flat_type_rel_pointwise R t x y. + Proof. clear RProd; induction t; simpl; destruct_head_hnf' unit; split_and; intuition. Qed. + End RProd. + Section RProd_iff. + Context (RProd : forall A B x y, R A (fst x) (fst y) /\ R B (snd x) (snd y) <-> R (Prod A B) x y). + Lemma lift_interp_flat_type_rel_pointwise t (x y : interp_flat_type t) + : interp_flat_type_rel_pointwise R t x y <-> R t x y. + Proof. + split_iff; split; auto using lift_interp_flat_type_rel_pointwise1, lift_interp_flat_type_rel_pointwise2. + Qed. + End RProd_iff. + End flat_type. + End lifting. +End language. + +Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _. +Global Arguments interp_type_gen_rel_pointwise2_hetero {_ _ _ _ _} Rsrc Rdst {t} _ _. +Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _. +Global Arguments interp_flat_type_rel_pointwise2_gen_Prop {_ _ _ P} and True R {t} _ _. +Global Arguments interp_flat_type_rel_pointwise2 {_ _ _} R {t} _ _. +Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _. +Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _. +Global Arguments interp_type_gen_rel_pointwise {_ _} _ {_} _ _. +Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _. diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index f8d7cdcf3..58000fdca 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -1,6 +1,5 @@ (** * PHOAS Representation of Gallina *) Require Import Coq.Strings.String Coq.Classes.RelationClasses Coq.Classes.Morphisms. -Require Import Crypto.Util.Tuple. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. @@ -16,7 +15,7 @@ Local Open Scope expr_scope. Section language. Context (base_type_code : Type). - Inductive flat_type := Tbase (T : base_type_code) | Prod (A B : flat_type). + Inductive flat_type := Tbase (T : base_type_code) | Unit | Prod (A B : flat_type). Bind Scope ctype_scope with flat_type. Inductive type := Tflat (T : flat_type) | Arrow (A : base_type_code) (B : type). @@ -27,16 +26,19 @@ Section language. Notation "A -> B" := (Arrow A B) : ctype_scope. Local Coercion Tbase : base_type_code >-> flat_type. - Fixpoint tuple' T n := - match n with - | O => T - | S n' => (tuple' T n' * T)%ctype - end. - Definition tuple T n := - match n with - | O => T (* default value; no empty tuple *) - | S n' => tuple' T n' - end. + Section tuple. + Context (T : flat_type). + Fixpoint tuple' n := + match n with + | O => T + | S n' => (tuple' n' * T)%ctype + end. + Definition tuple n := + match n with + | O => Unit + | S n' => tuple' n' + end. + End tuple. Section interp. Section type. @@ -49,134 +51,19 @@ Section language. | Arrow x y => (interp_src_type x -> interp_type_gen_hetero y)%type end. End hetero. - Section homogenous. - Context (interp_flat_type : flat_type -> Type). - Definition interp_type_gen := interp_type_gen_hetero interp_flat_type interp_flat_type. - Section rel. - Context (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop). - Fixpoint interp_type_gen_rel_pointwise (t : type) - : interp_type_gen t -> interp_type_gen t -> Prop := - match t with - | Tflat t => R t - | Arrow _ y => fun f g => forall x, interp_type_gen_rel_pointwise y (f x) (g x) - end. - Global Instance interp_type_gen_rel_pointwise_Reflexive {H : forall t, Reflexive (R t)} - : forall t, Reflexive (interp_type_gen_rel_pointwise t). - Proof. induction t; repeat intro; reflexivity. Qed. - Global Instance interp_type_gen_rel_pointwise_Symmetric {H : forall t, Symmetric (R t)} - : forall t, Symmetric (interp_type_gen_rel_pointwise t). - Proof. induction t; simpl; repeat intro; symmetry; eauto. Qed. - Global Instance interp_type_gen_rel_pointwise_Transitive {H : forall t, Transitive (R t)} - : forall t, Transitive (interp_type_gen_rel_pointwise t). - Proof. induction t; simpl; repeat intro; etransitivity; eauto. Qed. - End rel. - End homogenous. + Definition interp_type_gen (interp_flat_type : flat_type -> Type) + := interp_type_gen_hetero interp_flat_type interp_flat_type. End type. Section flat_type. Context (interp_base_type : base_type_code -> Type). Fixpoint interp_flat_type (t : flat_type) := match t with | Tbase t => interp_base_type t + | Unit => unit | Prod x y => prod (interp_flat_type x) (interp_flat_type y) end. Definition interp_type := interp_type_gen interp_flat_type. - Fixpoint flat_interp_tuple' {T n} : interp_flat_type (tuple' T n) -> Tuple.tuple' (interp_flat_type T) n - := match n return interp_flat_type (tuple' T n) -> Tuple.tuple' (interp_flat_type T) n with - | O => fun x => x - | S n' => fun xy => (@flat_interp_tuple' _ n' (fst xy), snd xy) - end. - Definition flat_interp_tuple {T n} : interp_flat_type (tuple T n) -> Tuple.tuple (interp_flat_type T) n - := match n return interp_flat_type (tuple T n) -> Tuple.tuple (interp_flat_type T) n with - | O => fun _ => tt - | S n' => @flat_interp_tuple' T n' - end. - Fixpoint flat_interp_untuple' {T n} : Tuple.tuple' (interp_flat_type T) n -> interp_flat_type (tuple' T n) - := match n return Tuple.tuple' (interp_flat_type T) n -> interp_flat_type (tuple' T n) with - | O => fun x => x - | S n' => fun xy => (@flat_interp_untuple' _ n' (fst xy), snd xy) - end. - Lemma flat_interp_untuple'_tuple' {T n v} - : @flat_interp_untuple' T n (flat_interp_tuple' v) = v. - Proof. induction n; [ reflexivity | simpl; rewrite IHn; destruct v; reflexivity ]. Qed. - Lemma flat_interp_untuple'_tuple {T n v} - : flat_interp_untuple' (@flat_interp_tuple T (S n) v) = v. - Proof. apply flat_interp_untuple'_tuple'. Qed. - Lemma flat_interp_tuple'_untuple' {T n v} - : @flat_interp_tuple' T n (flat_interp_untuple' v) = v. - Proof. induction n; [ reflexivity | simpl; rewrite IHn; destruct v; reflexivity ]. Qed. - Lemma flat_interp_tuple_untuple' {T n v} - : @flat_interp_tuple T (S n) (flat_interp_untuple' v) = v. - Proof. apply flat_interp_tuple'_untuple'. Qed. - Definition tuple_map {A B n} (f : interp_flat_type A -> interp_flat_type B) (v : interp_flat_type (tuple A n)) - : interp_flat_type (tuple B n) - := let fv := Tuple.map f (flat_interp_tuple v) in - match n return interp_flat_type (tuple A n) -> Tuple.tuple (interp_flat_type B) n -> interp_flat_type (tuple B n) with - | 0 => fun v _ => f v - | S _ => fun v fv => flat_interp_untuple' fv - end v fv. - Section rel. - Context (R : forall t, interp_base_type t -> interp_base_type t -> Prop). - Fixpoint interp_flat_type_rel_pointwise (t : flat_type) - : interp_flat_type t -> interp_flat_type t -> Prop := - match t with - | Tbase t => R t - | Prod _ _ => fun x y => interp_flat_type_rel_pointwise _ (fst x) (fst y) - /\ interp_flat_type_rel_pointwise _ (snd x) (snd y) - end. - Definition interp_type_rel_pointwise - := interp_type_gen_rel_pointwise _ interp_flat_type_rel_pointwise. - End rel. End flat_type. - Section rel_pointwise2. - Section type. - Section hetero. - Context (interp_src1 interp_src2 : base_type_code -> Type) - (interp_flat_type1 interp_flat_type2 : flat_type -> Type) - (Rsrc : forall t, interp_src1 t -> interp_src2 t -> Prop) - (R : forall t, interp_flat_type1 t -> interp_flat_type2 t -> Prop). - - Fixpoint interp_type_gen_rel_pointwise2_hetero (t : type) - : interp_type_gen_hetero interp_src1 interp_flat_type1 t - -> interp_type_gen_hetero interp_src2 interp_flat_type2 t - -> Prop - := match t with - | Tflat t => R t - | Arrow src dst => @respectful_hetero _ _ _ _ (Rsrc src) (fun _ _ => interp_type_gen_rel_pointwise2_hetero dst) - end. - End hetero. - Section homogenous. - Context (interp_flat_type1 interp_flat_type2 : flat_type -> Type) - (R : forall t, interp_flat_type1 t -> interp_flat_type2 t -> Prop). - - Definition interp_type_gen_rel_pointwise2 - := interp_type_gen_rel_pointwise2_hetero interp_flat_type1 interp_flat_type2 - interp_flat_type1 interp_flat_type2 - R R. - End homogenous. - End type. - Section flat_type. - Context (interp_base_type1 interp_base_type2 : base_type_code -> Type). - Section gen_prop. - Context (P : Type) - (and : P -> P -> P) - (R : forall t, interp_base_type1 t -> interp_base_type2 t -> P). - - Fixpoint interp_flat_type_rel_pointwise2_gen_Prop (t : flat_type) - : interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> P - := match t with - | Tbase t => R t - | Prod x y => fun a b => and (interp_flat_type_rel_pointwise2_gen_Prop x (fst a) (fst b)) - (interp_flat_type_rel_pointwise2_gen_Prop y (snd a) (snd b)) - end. - End gen_prop. - - Definition interp_flat_type_rel_pointwise2 - := @interp_flat_type_rel_pointwise2_gen_Prop Prop and. - - Definition interp_type_rel_pointwise2 R - := interp_type_gen_rel_pointwise2 _ _ (interp_flat_type_rel_pointwise2 R). - End flat_type. - End rel_pointwise2. End interp. Section expr_param. @@ -190,7 +77,7 @@ Section language. (** N.B. [Let] binds the components of a pair to separate variables, and does so recursively *) Inductive exprf : flat_type -> Type := - | Const {t : flat_type} (x : interp_type t) : exprf t + | TT : exprf Unit | Var {t} (v : var t) : exprf t | Op {t1 tR} (opc : op t1 tR) (args : exprf t1) : exprf tR | LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type_gen var tx -> exprf tC) : exprf tC @@ -201,32 +88,6 @@ Section language. | Abs {src dst} (f : var src -> expr dst) : expr (Arrow src dst). Bind Scope expr_scope with expr. Global Coercion Return : exprf >-> expr. - Definition UnReturn {t} (e : expr (Tflat t)) : exprf t - := match e with - | Return _ v => v - | Abs _ _ _ => I - end. - Definition UnAbs {src dst} (e : expr (Arrow src dst)) : var src -> expr dst - := match e with - | Return _ _ => I - | Abs _ _ f => f - end. - Definition UnReturn_eta {t} (e : expr (Tflat t)) : Return (UnReturn e) = e - := match e in expr T return match T return expr T -> Prop with - | Tflat _ => fun e => Return (UnReturn e) = e - | _ => fun _ => I = I - end e with - | Return _ _ => eq_refl - | Abs _ _ _ => eq_refl - end. - Definition UnAbs_eta {src dst} (e : expr (Arrow src dst)) : Abs (UnAbs e) = e - := match e in expr T return match T return expr T -> Prop with - | Arrow src dst => fun e => Abs (UnAbs e) = e - | _ => fun _ => I = I - end e with - | Return _ _ => eq_refl - | Abs _ _ _ => eq_refl - end. (** Sometimes, we want to deal with partially-interpreted expressions, things like [prod (exprf A) (exprf B)] rather than [exprf (Prod A B)], or like [prod (var A) (var B)] when @@ -239,25 +100,28 @@ Section language. [interp_base_type] into [exprf])). *) Fixpoint smart_interp_flat_map {f g} (h : forall x, f x -> g (Tbase x)) + (tt : g Unit) (pair : forall A B, g A -> g B -> g (Prod A B)) {t} : interp_flat_type_gen f t -> g t := match t return interp_flat_type_gen f t -> g t with | Tbase _ => h _ + | Unit => fun _ => tt | Prod A B => fun v => pair _ _ - (@smart_interp_flat_map f g h pair A (fst v)) - (@smart_interp_flat_map f g h pair B (snd v)) + (@smart_interp_flat_map f g h tt pair A (fst v)) + (@smart_interp_flat_map f g h tt pair B (snd v)) end. Fixpoint smart_interp_map_hetero {f g g'} (h : forall x, f x -> g (Tflat (Tbase x))) + (tt : g Unit) (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B)) (abs : forall A B, (g' A -> g B) -> g (Arrow A B)) {t} : interp_type_gen_hetero g' (interp_flat_type_gen f) t -> g t := match t return interp_type_gen_hetero g' (interp_flat_type_gen f) t -> g t with - | Tflat _ => @smart_interp_flat_map f (fun x => g (Tflat x)) h pair _ + | Tflat _ => @smart_interp_flat_map f (fun x => g (Tflat x)) h tt pair _ | Arrow A B => fun v => abs _ _ - (fun x => @smart_interp_map_hetero f g g' h pair abs B (v x)) + (fun x => @smart_interp_map_hetero f g g' h tt pair abs B (v x)) end. Fixpoint smart_interp_map_gen {f g} (h : forall x, f x -> g (Tflat (Tbase x))) @@ -274,44 +138,51 @@ Section language. Definition smart_interp_map {f g} (h : forall x, f x -> g (Tflat (Tbase x))) (h' : forall x, g (Tflat (Tbase x)) -> f x) + (tt : g Unit) (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B)) (abs : forall A B, (g (Tflat (Tbase A)) -> g B) -> g (Arrow A B)) {t} : interp_type_gen (interp_flat_type_gen f) t -> g t - := @smart_interp_map_gen f g h h' (@smart_interp_flat_map f (fun x => g (Tflat x)) h pair) abs t. + := @smart_interp_map_gen f g h h' (@smart_interp_flat_map f (fun x => g (Tflat x)) h tt pair) abs t. Fixpoint SmartValf {T} (val : forall t : base_type_code, T t) t : interp_flat_type_gen T t := match t return interp_flat_type_gen T t with | Tbase _ => val _ + | Unit => tt | Prod A B => (@SmartValf T val A, @SmartValf T val B) end. Fixpoint SmartArrow (A : flat_type) (B : type) : type := match A with | Tbase A' => Arrow A' B + | Unit => B | Prod A0 A1 => SmartArrow A0 (SmartArrow A1 B) end. Fixpoint SmartAbs {A B} {struct A} : forall (f : exprf A -> expr B), expr (SmartArrow A B) := match A return (exprf A -> expr B) -> expr (SmartArrow A B) with | Tbase x => fun f => Abs (fun x => f (Var x)) + | Unit => fun f => f TT | Prod x y => fun f => @SmartAbs x _ (fun x' => @SmartAbs y _ (fun y' => f (Pair x' y'))) end. (** [SmartVar] is like [Var], except that it inserts pair-projections and [Pair] as necessary to handle [flat_type], and not just [base_type_code] *) + Definition SmartPairf {t} : interp_flat_type_gen exprf t -> exprf t + := @smart_interp_flat_map exprf exprf (fun t x => x) TT (fun A B x y => Pair x y) t. Definition SmartVarf {t} : interp_flat_type_gen var t -> exprf t - := @smart_interp_flat_map var exprf (fun t => Var) (fun A B x y => Pair x y) t. + := @smart_interp_flat_map var exprf (fun t => Var) TT (fun A B x y => Pair x y) t. Definition SmartVarfMap {var var'} (f : forall t, var t -> var' t) {t} : interp_flat_type_gen var t -> interp_flat_type_gen var' t - := @smart_interp_flat_map var (interp_flat_type_gen var') f (fun A B x y => pair x y) t. + := @smart_interp_flat_map var (interp_flat_type_gen var') f tt (fun A B x y => pair x y) t. Definition SmartFlatTypeMap {var'} (f : forall t, var' t -> base_type_code) {t} : interp_flat_type_gen var' t -> flat_type - := @smart_interp_flat_map var' (fun _ => flat_type) f (fun _ _ => Prod) t. + := @smart_interp_flat_map var' (fun _ => flat_type) f Unit (fun _ _ => Prod) t. Fixpoint SmartFlatTypeMapInterp {var' var''} (f : forall t, var' t -> base_type_code) (fv : forall t v, var'' (f t v)) t {struct t} : forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v) := match t return forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v) with | Tbase x => fv _ + | Unit => fun v => v | Prod A B => fun xy => (@SmartFlatTypeMapInterp _ _ f fv A (fst xy), @SmartFlatTypeMapInterp _ _ f fv B (snd xy)) end. @@ -323,19 +194,20 @@ Section language. := match t return forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v) -> interp_flat_type_gen var''' t with | Tbase x => fv _ + | Unit => fun _ v => v | Prod A B => fun v xy => (@SmartFlatTypeMapUnInterp _ _ _ f fv A _ (fst xy), @SmartFlatTypeMapUnInterp _ _ _ f fv B _ (snd xy)) end. Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t} : interp_type_gen (interp_flat_type_gen var) t -> interp_type_gen (interp_flat_type_gen var') t - := @smart_interp_map var (interp_type_gen (interp_flat_type_gen var')) f f' (fun A B x y => pair x y) (fun A B f x => f x) t. + := @smart_interp_map var (interp_type_gen (interp_flat_type_gen var')) f f' tt (fun A B x y => pair x y) (fun A B f x => f x) t. Definition SmartVarMap_hetero {vars vars' var var'} (f : forall t, var t -> var' t) (f' : forall t, vars' t -> vars t) {t} : interp_type_gen_hetero vars (interp_flat_type_gen var) t -> interp_type_gen_hetero vars' (interp_flat_type_gen var') t - := @smart_interp_map_hetero var (interp_type_gen_hetero vars' (interp_flat_type_gen var')) vars f (fun A B x y => pair x y) (fun A B f x => f (f' _ x)) t. + := @smart_interp_map_hetero var (interp_type_gen_hetero vars' (interp_flat_type_gen var')) vars f tt (fun A B x y => pair x y) (fun A B f x => f (f' _ x)) t. Definition SmartVarVarf {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t := SmartVarfMap (fun t => Var). - Definition SmartConstf {t} : interp_flat_type t -> interp_flat_type_gen exprf t - := SmartVarfMap (fun t => Const (t:=t)). + (*Definition SmartConstf {t} : interp_flat_type t -> interp_flat_type_gen exprf t + := SmartVarfMap (fun t => Const (t:=t)).*) End expr. Definition Expr (t : type) := forall var, @expr var t. @@ -347,7 +219,7 @@ Section language. (interpf : forall {t} (e : @exprf interp_flat_type t), interp_flat_type t) {t} (e : @exprf interp_flat_type t) : interp_flat_type t := match e in exprf t return interp_flat_type t with - | Const _ x => x + | TT => tt | Var _ x => x | Op _ _ op args => @interp_op _ _ op (@interpf _ args) | LetIn _ ex _ eC => dlet x := @interpf _ ex in @interpf _ (eC x) @@ -375,13 +247,14 @@ Section language. : interp_flat_type_gen var1 t := match t return interp_flat_type_gen _ t -> interp_flat_type_gen _ t with | Tbase _ => fvar21 _ + | Unit => fun v : unit => v | Prod x y => fun xy => (@mapf_interp_flat_type _ (fst xy), @mapf_interp_flat_type _ (snd xy)) end e. Fixpoint mapf {t} (e : @exprf var1 t) : @exprf var2 t := match e in exprf t return exprf t with - | Const _ x => Const x + | TT => TT | Var _ x => Var (fvar12 _ x) | Op _ _ op args => Op op (@mapf _ args) | LetIn _ ex _ eC => LetIn (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type x))) @@ -397,11 +270,12 @@ Section language. Fixpoint flatten_binding_list {t} (x : interp_flat_type_gen var1 t) (y : interp_flat_type_gen var2 t) : list (sigT eP) := (match t return interp_flat_type_gen var1 t -> interp_flat_type_gen var2 t -> list _ with | Tbase _ => fun x y => (x == y) :: nil + | Unit => fun x y => nil | Prod t0 t1 => fun x y => @flatten_binding_list _ (snd x) (snd y) ++ @flatten_binding_list _ (fst x) (fst y) end x y)%list. Inductive wff : list (sigT eP) -> forall {t}, @exprf var1 t -> @exprf var2 t -> Prop := - | WfConst : forall t G n, @wff G t (Const n) (Const n) + | WfTT : forall G, @wff G _ TT TT | WfVar : forall G (t : base_type_code) x x', List.In (x == x') G -> @wff G t (Var x) (Var x') | WfOp : forall G {t} {tR} (e : @exprf var1 t) (e' : @exprf var2 t) op, wff G e e' @@ -429,6 +303,7 @@ Section language. End language. Global Arguments tuple' {_}%type_scope _%ctype_scope _%nat_scope. Global Arguments tuple {_}%type_scope _%ctype_scope _%nat_scope. +Global Arguments Unit {_}%type_scope. Global Arguments Prod {_}%type_scope (_ _)%ctype_scope. Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope. Global Arguments Tbase {_}%type_scope _%ctype_scope. @@ -436,47 +311,33 @@ Global Arguments Tflat {_}%type_scope _%ctype_scope. Ltac admit_Wf := apply Wf_admitted. -Global Arguments Const {_ _ _ _ _} _. -Global Arguments Var {_ _ _ _ _} _. -Global Arguments SmartVarf {_ _ _ _ _} _. +Global Arguments Var {_ _ _ _} _. +Global Arguments SmartVarf {_ _ _ _} _. +Global Arguments SmartPairf {_ _ _ t} _. Global Arguments SmartValf {_} T _ t. -Global Arguments SmartVarVarf {_ _ _ _ _} _. +Global Arguments SmartVarVarf {_ _ _ _} _. Global Arguments SmartVarfMap {_ _ _} _ {_} _. Global Arguments SmartFlatTypeMap {_ _} _ {_} _. Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _. Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _. Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _. Global Arguments SmartVarMap {_ _ _} _ _ {_} _. -Global Arguments SmartConstf {_ _ _ _ _} _. -Global Arguments Op {_ _ _ _ _ _} _ _. -Global Arguments LetIn {_ _ _ _ _} _ {_} _. -Global Arguments Pair {_ _ _ _ _} _ {_} _. -Global Arguments Return {_ _ _ _ _} _. -Global Arguments Abs {_ _ _ _ _ _} _. -Global Arguments SmartAbs {_ _ _ _ _ _} _. -Global Arguments UnReturn {_ _ _ _ _} _. -Global Arguments UnAbs {_ _ _ _ _ _} _ _. -Global Arguments UnReturn_eta {_ _ _ _ _} _. -Global Arguments UnAbs_eta {_ _ _ _ _ _} _. -Global Arguments flat_interp_tuple' {_ _ _ _} _. -Global Arguments flat_interp_tuple {_ _ _ _} _. -Global Arguments flat_interp_untuple' {_ _ _ _} _. -Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _. -Global Arguments interp_type_gen_rel_pointwise2_hetero {_ _ _ _ _} Rsrc R {t} _ _. -Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _. -Global Arguments interp_flat_type_rel_pointwise2_gen_Prop {_ _ _ P} and R {t} _ _. -Global Arguments interp_flat_type_rel_pointwise2 {_ _ _} R {t} _ _. +(*Global Arguments SmartConstf {_ _ _ _ _} _.*) +Global Arguments TT {_ _ _}. +Global Arguments Op {_ _ _ _ _} _ _. +Global Arguments LetIn {_ _ _ _} _ {_} _. +Global Arguments Pair {_ _ _ _} _ {_} _. +Global Arguments Return {_ _ _ _} _. +Global Arguments Abs {_ _ _ _ _} _. +Global Arguments SmartAbs {_ _ _ _ _} _. Global Arguments mapf_interp_flat_type {_ _ _} _ {t} _. Global Arguments interp_type_gen_hetero {_} _ _ _. Global Arguments interp_type_gen {_} _ _. Global Arguments interp_flat_type {_} _ _. -Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _. -Global Arguments interp_type_gen_rel_pointwise {_ _} _ {_} _ _. -Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _. Global Arguments interp_type {_} _ _. -Global Arguments wff {_ _ _ _ _} G {t} _ _. -Global Arguments wf {_ _ _ _ _} G {t} _ _. -Global Arguments Wf {_ _ _ t} _. +Global Arguments wff {_ _ _ _} G {t} _ _. +Global Arguments wf {_ _ _ _} G {t} _ _. +Global Arguments Wf {_ _ t} _. Global Arguments Interp {_ _ _} interp_op {t} _. Global Arguments interp {_ _ _} interp_op {t} _. Global Arguments interpf {_ _ _} interp_op {t} _. @@ -485,6 +346,7 @@ Section hetero_type. Fixpoint flatten_flat_type {base_type_code} (t : flat_type (flat_type base_type_code)) : flat_type base_type_code := match t with | Tbase T => T + | Unit => Unit | Prod A B => Prod (@flatten_flat_type _ A) (@flatten_flat_type _ B) end. @@ -493,12 +355,13 @@ Section hetero_type. Definition SmartFlatTypeMap2 {var' : base_type_code1 -> Type} (f : forall t, var' t -> flat_type base_type_code2) {t} : interp_flat_type var' t -> flat_type base_type_code2 - := @smart_interp_flat_map base_type_code1 var' (fun _ => flat_type base_type_code2) f (fun _ _ => Prod) t. + := @smart_interp_flat_map base_type_code1 var' (fun _ => flat_type base_type_code2) f Unit (fun _ _ => Prod) t. Fixpoint SmartFlatTypeMapInterp2 {var' var''} (f : forall t, var' t -> flat_type base_type_code2) (fv : forall t v, interp_flat_type var'' (f t v)) t {struct t} : forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v) := match t return forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v) with | Tbase x => fv _ + | Unit => fun v => v | Prod A B => fun xy => (@SmartFlatTypeMapInterp2 _ _ f fv A (fst xy), @SmartFlatTypeMapInterp2 _ _ f fv B (snd xy)) end. @@ -510,6 +373,7 @@ Section hetero_type. := match t return forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v) -> interp_flat_type var''' t with | Tbase x => fv _ + | Unit => fun _ v => v | Prod A B => fun v xy => (@SmartFlatTypeMapUnInterp2 _ _ _ f fv A _ (fst xy), @SmartFlatTypeMapUnInterp2 _ _ _ f fv B _ (snd xy)) end. @@ -521,11 +385,14 @@ Global Arguments SmartFlatTypeMapInterp2 {_ _ _ _ _} _ {_} _. Global Arguments SmartFlatTypeMapUnInterp2 {_ _ _ _ _ _} fv {_ _} _. Module Export Notations. + Notation "()" := (@Unit _) : ctype_scope. Notation "A * B" := (@Prod _ A B) : ctype_scope. Notation "A -> B" := (@Arrow _ A B) : ctype_scope. Notation "'slet' x := A 'in' b" := (LetIn A (fun x => b)) : expr_scope. Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope. + Notation "( )" := TT : expr_scope. + Notation "()" := TT : expr_scope. Bind Scope ctype_scope with flat_type. Bind Scope ctype_scope with type. End Notations. diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index 640db3824..2d70dfd3e 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -11,12 +11,12 @@ Require Import Crypto.Reflection.CommonSubexpressionElimination. Require Crypto.Reflection.Linearize Crypto.Reflection.Inline. Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Reflection.Conversion. +Require Import Crypto.Util.NatUtil. Import ReifyDebugNotations. Local Set Boolean Equality Schemes. Local Set Decidable Equality Schemes. -Scheme Equality for nat. Inductive base_type := Tnat. Definition interp_base_type (v : base_type) : Type := match v with @@ -24,11 +24,14 @@ Definition interp_base_type (v : base_type) : Type := end. Local Notation tnat := (Tbase Tnat). Inductive op : flat_type base_type -> flat_type base_type -> Type := +| Const (v : nat) : op Unit tnat | Add : op (Prod tnat tnat) tnat | Mul : op (Prod tnat tnat) tnat | Sub : op (Prod tnat tnat) tnat. +Definition is_const s d (v : op s d) : bool := match v with Const _ => true | _ => false end. Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f with + | Const v => fun _ => v | Add => fun xy => fst xy + snd xy | Mul => fun xy => fst xy * snd xy | Sub => fun xy => fst xy - snd xy @@ -39,26 +42,30 @@ Global Instance: reify_op op mult 2 Mul := I. Global Instance: reify_op op minus 2 Sub := I. Global Instance: reify type nat := Tnat. +Definition make_const (t : base_type) : interp_base_type t -> op Unit (Tbase t) + := match t with + | Tnat => fun v => Const v + end. Ltac Reify' e := Reify.Reify' base_type interp_base_type op e. -Ltac Reify e := Reify.Reify base_type interp_base_type op e. -Ltac Reify_rhs := Reify.Reify_rhs base_type interp_base_type op interp_op. +Ltac Reify e := Reify.Reify base_type interp_base_type op make_const e. +Ltac Reify_rhs := Reify.Reify_rhs base_type interp_base_type op make_const interp_op. (*Ltac reify_debug_level ::= constr:(2).*) Goal (flat_type base_type -> Type) -> False. intro var. let x := reifyf base_type interp_base_type op var 1%nat in pose x. - let x := Reify' 1%nat in unify x (fun var => Return (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)). + let x := Reify' 1%nat in unify x (fun var => Return (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)). let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x. - let x := Reify' (1 + 1)%nat in unify x (fun var => Return (Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). + let x := Reify' (1 + 1)%nat in unify x (fun var => Return (Op Add (Pair (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x. - let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). + let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x. let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x. let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in let x := (eval vm_compute in x) in pose x. let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in unify x (fun var => Abs (fun x' => - let c1 := (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in + let c1 := (InputSyntax.Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in MatchPair (tC:=tnat) (Pair c1 c1) (fun x0 _ : var tnat => Op Add (Pair (Var x0) (Var x'))))). let x := reifyf base_type interp_base_type op var (let x := 5 in let y := 6 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. @@ -78,11 +85,11 @@ Import Linearize Inline. Goal True. let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x - a + c + d) + y)%nat in - pose (InlineConst (Linearize x)) as e. + pose (InlineConst is_const (Linearize x)) as e. vm_compute in e. Abort. -Definition example_expr : Syntax.Expr base_type interp_base_type op (Arrow Tnat (Arrow Tnat (Tflat tnat))). +Definition example_expr : Syntax.Expr base_type op (Arrow Tnat (Arrow Tnat (Tflat tnat))). Proof. let x := Reify (fun z w => let unused := 1 + 1 in let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + (x + x) + (x + x) - (x + x) - a + c + d) + y + z + w)%nat in exact x. @@ -99,6 +106,8 @@ Proof. Qed. Definition op_beq t1 tR : op t1 tR -> op t1 tR -> reified_Prop := fun x y => match x, y return bool with + | Const a, Const b => NatUtil.nat_beq a b + | Const _, _ => false | Add, Add => true | Add, _ => false | Mul, Mul => true @@ -110,7 +119,16 @@ Lemma op_beq_bl t1 tR (x y : op t1 tR) : to_prop (op_beq t1 tR x y) -> x = y. Proof. destruct x; simpl; - refine match y with Add => _ | _ => _ end; simpl; tauto. + refine match y with Add => _ | _ => _ end; + repeat match goal with + | _ => progress simpl in * + | _ => progress unfold op_beq in * + | [ |- context[reified_Prop_of_bool ?b] ] + => destruct b eqn:?; unfold reified_Prop_of_bool + | _ => progress nat_beq_to_eq + | _ => congruence + | _ => tauto + end. Qed. Ltac reflect_Wf := WfReflective.reflect_Wf base_type_eq_semidec_is_dec op_beq_bl. @@ -132,21 +150,18 @@ Proof. Time reflect_Wf. (* 0.008 s *) Qed. Section cse. Let SConstT := nat. - Inductive op_code : Set := SAdd | SMul | SSub. - Definition symbolicify_const (t : base_type) : interp_base_type t -> SConstT - := match t with - | Tnat => fun x => x - end. + Inductive op_code : Set := SConst (v : nat) | SAdd | SMul | SSub. Definition symbolicify_op s d (v : op s d) : op_code := match v with + | Const v => SConst v | Add => SAdd | Mul => SMul | Sub => SSub end. - Definition CSE {t} e := @CSE base_type SConstT op_code base_type_beq nat_beq op_code_beq internal_base_type_dec_bl interp_base_type op symbolicify_const symbolicify_op t e (fun _ => nil). + Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op t e (fun _ => nil). End cse. -Definition example_expr_simplified := Eval vm_compute in InlineConst (Linearize example_expr). +Definition example_expr_simplified := Eval vm_compute in InlineConst is_const (Linearize example_expr). Compute CSE example_expr_simplified. Definition example_expr_compiled @@ -184,30 +199,28 @@ Module bounds. match v with | Tnat => { b : bounded | lower b <= value b <= upper b } end. - Definition interp_op_bounds src dst (f : op src dst) : interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst - := match f with - | Add => fun xy => add_bounded_pf (fst xy) (snd xy) - | Mul => fun xy => mul_bounded_pf (fst xy) (snd xy) - | Sub => fun xy => sub_bounded_pf (fst xy) (snd xy) - end%nat. Definition constant_bounded t (x : interp_base_type t) : interp_base_type_bounds t. Proof. destruct t. exists {| lower := x ; value := x ; upper := x |}. simpl; split; reflexivity. Defined. + Definition interp_op_bounds src dst (f : op src dst) : interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst + := match f with + | Const v => fun _ => constant_bounded Tnat v + | Add => fun xy => add_bounded_pf (fst xy) (snd xy) + | Mul => fun xy => mul_bounded_pf (fst xy) (snd xy) + | Sub => fun xy => sub_bounded_pf (fst xy) (snd xy) + end%nat. Fixpoint constant_bounds t : interp_flat_type interp_base_type t -> interp_flat_type interp_base_type_bounds t := match t with | Tbase t => constant_bounded t + | Unit => fun _ => tt | Prod _ _ => fun x => (constant_bounds _ (fst x), constant_bounds _ (snd x)) end. - Definition example_expr_bounds : Syntax.Expr base_type interp_base_type_bounds op (Arrow Tnat (Arrow Tnat (Tflat tnat))) := - Eval vm_compute in - (fun var => map base_type op interp_base_type interp_base_type_bounds constant_bounds (fun _ x => x) (fun _ x => x) (example_expr (fun t => var t))). - - Compute (fun x xpf y ypf => proj1_sig (Syntax.Interp interp_op_bounds example_expr_bounds + Compute (fun x xpf y ypf => proj1_sig (Syntax.Interp interp_op_bounds example_expr (exist _ {| lower := 0 ; value := x ; upper := 10 |} xpf) (exist _ {| lower := 100 ; value := y ; upper := 1000 |} ypf))). End bounds. diff --git a/src/Reflection/Tuple.v b/src/Reflection/Tuple.v new file mode 100644 index 000000000..6071f13c2 --- /dev/null +++ b/src/Reflection/Tuple.v @@ -0,0 +1,62 @@ +Require Import Crypto.Util.Tuple. +Require Import Crypto.Reflection.Syntax. + +Local Open Scope ctype_scope. +Section language. + Context {base_type_code : Type}. + + Local Notation flat_type := (flat_type base_type_code). + + Section interp. + Section flat_type. + Context {interp_base_type : base_type_code -> Type}. + Local Notation interp_flat_type := (interp_flat_type interp_base_type). + + Fixpoint flat_interp_tuple' {T n} : interp_flat_type (tuple' T n) -> Tuple.tuple' (interp_flat_type T) n + := match n return interp_flat_type (tuple' T n) -> Tuple.tuple' (interp_flat_type T) n with + | O => fun x => x + | S n' => fun xy => (@flat_interp_tuple' _ n' (fst xy), snd xy) + end. + Definition flat_interp_tuple {T n} : interp_flat_type (tuple T n) -> Tuple.tuple (interp_flat_type T) n + := match n return interp_flat_type (tuple T n) -> Tuple.tuple (interp_flat_type T) n with + | O => fun x => x + | S n' => @flat_interp_tuple' T n' + end. + Fixpoint flat_interp_untuple' {T n} : Tuple.tuple' (interp_flat_type T) n -> interp_flat_type (tuple' T n) + := match n return Tuple.tuple' (interp_flat_type T) n -> interp_flat_type (tuple' T n) with + | O => fun x => x + | S n' => fun xy => (@flat_interp_untuple' _ n' (fst xy), snd xy) + end. + Definition flat_interp_untuple {T n} : Tuple.tuple (interp_flat_type T) n -> interp_flat_type (tuple T n) + := match n return Tuple.tuple (interp_flat_type T) n -> interp_flat_type (tuple T n) with + | O => fun x => x + | S n' => @flat_interp_untuple' T n' + end. + Lemma flat_interp_untuple'_tuple' {T n v} + : @flat_interp_untuple' T n (flat_interp_tuple' v) = v. + Proof. induction n; [ reflexivity | simpl; rewrite IHn; destruct v; reflexivity ]. Qed. + Lemma flat_interp_untuple_tuple {T n v} + : flat_interp_untuple (@flat_interp_tuple T n v) = v. + Proof. destruct n; [ reflexivity | apply flat_interp_untuple'_tuple' ]. Qed. + Lemma flat_interp_tuple'_untuple' {T n v} + : @flat_interp_tuple' T n (flat_interp_untuple' v) = v. + Proof. induction n; [ reflexivity | simpl; rewrite IHn; destruct v; reflexivity ]. Qed. + Lemma flat_interp_tuple_untuple {T n v} + : @flat_interp_tuple T n (flat_interp_untuple v) = v. + Proof. destruct n; [ reflexivity | apply flat_interp_tuple'_untuple' ]. Qed. + + Definition tuple_map {A B n} (f : interp_flat_type A -> interp_flat_type B) (v : interp_flat_type (tuple A n)) + : interp_flat_type (tuple B n) + := let fv := Tuple.map f (flat_interp_tuple v) in + match n return interp_flat_type (tuple A n) -> Tuple.tuple (interp_flat_type B) n -> interp_flat_type (tuple B n) with + | 0 => fun v x => x + | S _ => fun v fv => flat_interp_untuple' fv + end v fv. + End flat_type. + End interp. +End language. +Global Arguments flat_interp_tuple' {_ _ _ _} _. +Global Arguments flat_interp_tuple {_ _ _ _} _. +Global Arguments flat_interp_untuple' {_ _ _ _} _. +Global Arguments flat_interp_untuple {_ _ _ _} _. +Global Arguments tuple_map {_ _ _ _ n} _ _. diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v index e63cfc931..4543dce48 100644 --- a/src/Reflection/WfInversion.v +++ b/src/Reflection/WfInversion.v @@ -8,20 +8,16 @@ Require Import Crypto.Util.Notations. Section language. Context {base_type_code : Type} - {interp_base_type : 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 Tbase := (@Tbase base_type_code). - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - Local Notation Expr := (@Expr base_type_code interp_base_type op). - Local Notation wff := (@wff base_type_code interp_base_type op). - Local Notation wf := (@wf base_type_code interp_base_type op). - Local Notation Wf := (@Wf base_type_code interp_base_type op). + 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 wff := (@wff base_type_code op). + Local Notation wf := (@wf base_type_code op). + Local Notation Wf := (@Wf base_type_code op). Section with_var. Context {var1 var2 : base_type_code -> Type}. @@ -30,10 +26,10 @@ Section language. Local Notation "x == y" := (existT eP _ (x, y)). Definition wff_code (G : list (sigT eP)) {t} (e1 : @exprf var1 t) : forall (e2 : @exprf var2 t), Prop - := match e1 in Syntax.exprf _ _ _ t return exprf t -> Prop with - | Const t x + := match e1 in Syntax.exprf _ _ t return exprf t -> Prop with + | TT => fun e2 - => Some x = invert_Const e2 + => TT = e2 | Var t v1 => fun e2 => match invert_Var e2 with @@ -86,7 +82,6 @@ Section language. | _ => progress subst | _ => progress inversion_option | [ H : Some _ = _ |- _ ] => symmetry in H - | [ H : invert_Const _ = _ |- _ ] => apply invert_Const_Some in H | [ H : invert_Var _ = _ |- _ ] => apply invert_Var_Some in H | [ H : invert_Op _ = _ |- _ ] => apply invert_Op_Some in H | [ H : invert_LetIn _ = _ |- _ ] => apply invert_LetIn_Some in H @@ -120,6 +115,8 @@ Section language. destruct e1; simpl in *; move e2 at top; lazymatch type of e2 with + | exprf Unit + => subst; reflexivity | exprf (Tbase ?t) => revert dependent t; intros ? e2 @@ -134,7 +131,7 @@ Section language. intros ? e2 end; refine match e2 with - | Const _ _ => _ + | TT => _ | _ => _ end; t'. diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v index 5f3c46a27..dda347f00 100644 --- a/src/Reflection/WfProofs.v +++ b/src/Reflection/WfProofs.v @@ -4,20 +4,15 @@ Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod. Local Open Scope ctype_scope. Section language. - Context (base_type_code : Type). - Context (interp_base_type : base_type_code -> Type). - Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). + 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). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - Local Notation Expr := (@Expr base_type_code interp_base_type op). - Local Notation wff := (@wff base_type_code interp_base_type op). + 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 wff := (@wff base_type_code op). Section with_var. Context {var1 var2 : base_type_code -> Type}. @@ -80,48 +75,12 @@ Section language. Local Hint Resolve wff_SmartVarf. - Lemma wff_Const_eta G {A B} v1 v2 - : @wff var1 var2 G (Prod A B) (Const v1) (Const v2) - -> (@wff var1 var2 G A (Const (fst v1)) (Const (fst v2)) - /\ @wff var1 var2 G B (Const (snd v1)) (Const (snd v2))). - Proof. - intro wf. - assert (H : Some v1 = Some v2). - { refine match wf in @Syntax.wff _ _ _ _ _ G t e1 e2 return invert_Const e1 = invert_Const e2 with - | WfConst _ _ _ => eq_refl - | _ => eq_refl - end. } - inversion H; subst; repeat constructor. - Qed. - - Definition wff_Const_eta_fst G {A B} v1 v2 H - := proj1 (@wff_Const_eta G A B v1 v2 H). - Definition wff_Const_eta_snd G {A B} v1 v2 H - := proj2 (@wff_Const_eta G A B v1 v2 H). - - Local Hint Resolve wff_Const_eta_fst wff_Const_eta_snd. - - Lemma wff_SmartConstf G {t t'} v1 v2 x1 x2 - (Hin : List.In (existT (fun t : base_type_code => (@exprf var1 t * @exprf var2 t)%type) t (x1, x2)) - (flatten_binding_list base_type_code (SmartConstf v1) (SmartConstf v2))) - (Hwf : @wff var1 var2 G t' (Const v1) (Const v2)) - : @wff var1 var2 G t x1 x2. - Proof. - induction t'. simpl in *. - { intuition (inversion_sigma; inversion_prod; subst; eauto). } - { unfold SmartConstf in *; simpl in *. - apply List.in_app_iff in Hin. - intuition (inversion_sigma; inversion_prod; subst; eauto). } - Qed. - - Local Hint Resolve wff_SmartConstf. - Lemma wff_SmartVarVarf G {t t'} v1 v2 x1 x2 - (Hin : List.In (existT (fun t : base_type_code => (exprf t * exprf t)%type) t (x1, x2)) + (Hin : List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x1, x2)) (flatten_binding_list base_type_code (SmartVarVarf v1) (SmartVarVarf v2))) - : @wff var1 var2 (flatten_binding_list base_type_code (t:=t') v1 v2 ++ G) t x1 x2. + : @wff var1 var2 (flatten_binding_list base_type_code (t:=t') v1 v2 ++ G) (Tbase t) x1 x2. Proof. - revert dependent G; induction t'; intros. simpl in *. + revert dependent G; induction t'; intros; simpl in *; try tauto. { intuition (inversion_sigma; inversion_prod; subst; simpl; eauto). constructor; eauto. } { unfold SmartVarVarf in *; simpl in *. diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v index 8a8eef38f..88e6bf5b0 100644 --- a/src/Reflection/WfReflective.v +++ b/src/Reflection/WfReflective.v @@ -64,7 +64,6 @@ Section language. enforced, but it will block [vm_compute] when trying to use the lemma in this file.) *) Context (base_type_code : Type). - Context (interp_base_type : base_type_code -> Type). Context (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)). Context (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2). Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). @@ -83,26 +82,15 @@ Section language. (* convenience notations that fill in some arguments used across the section *) Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type := (interp_type interp_base_type). - Local Notation interp_flat_type := (interp_flat_type interp_base_type). - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). + Local Notation exprf := (@exprf base_type_code op). + Local Notation expr := (@expr base_type_code op). Local Notation duplicate_type := (@duplicate_type base_type_code var1 var2). - Local Notation reflect_wffT := (@reflect_wffT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2). - Local Notation reflect_wfT := (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2). + Local Notation reflect_wffT := (@reflect_wffT base_type_code base_type_eq_semidec_transparent op op_beq var1 var2). + Local Notation reflect_wfT := (@reflect_wfT base_type_code base_type_eq_semidec_transparent op op_beq var1 var2). Local Notation flat_type_eq_semidec_transparent := (@flat_type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent). Local Notation preflatten_binding_list2 := (@preflatten_binding_list2 base_type_code base_type_eq_semidec_transparent var1 var2). Local Notation type_eq_semidec_transparent := (@type_eq_semidec_transparent base_type_code base_type_eq_semidec_transparent). - Lemma interp_flat_type_rel_pointwise2_eq {t} (x y : interp_flat_type t) - : interp_flat_type_rel_pointwise2 (fun _ => eq) x y <-> x = y. - Proof. - induction t; simpl in *; [ reflexivity | ]. - rewrite_hyp !*; intuition (simpl in *; try congruence). - Qed. - Local Ltac handle_op_beq_correct := repeat match goal with | [ H : to_prop (op_beq ?t1 ?tR ?x ?y) |- _ ] @@ -159,7 +147,7 @@ Section language. match flat_type_eq_semidec_transparent t1 t2 with | Some p => to_prop reflective_obligation - -> @wff base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2) + -> @wff base_type_code op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2) | None => True end. Proof. @@ -195,7 +183,7 @@ Section language. match type_eq_semidec_transparent t1 t2 with | Some p => to_prop reflective_obligation - -> @wf base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ expr (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2) + -> @wf base_type_code op var1 var2 G t2 (eq_rect _ expr (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2) | None => True end. Proof. @@ -204,7 +192,7 @@ Section language. [ clear reflect_wf; pose proof (@reflect_wff G t1 t2 e1 e2) | pose proof (fun x x' - => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with + => match preflatten_binding_list2 (Tbase tx) (Tbase tx') as v return match v with Some _ => _ | None => True end with | Some G0 => reflect_wf (G0 x x' ++ G)%list _ _ @@ -220,23 +208,22 @@ End language. Section Wf. Context (base_type_code : Type) - (interp_base_type : base_type_code -> Type) (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)) (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2) (op : flat_type base_type_code -> flat_type base_type_code -> Type) (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> reified_Prop) (op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y) {t : type base_type_code} - (e : @Expr base_type_code interp_base_type op t). + (e : @Expr base_type_code op t). (** Leads to smaller proofs, but is less generally applicable *) Theorem reflect_Wf_unnatize : (forall var1 var2, - to_prop (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2 nil t t (e _) (e _))) + to_prop (@reflect_wfT base_type_code base_type_eq_semidec_transparent op op_beq var1 var2 nil t t (e _) (e _))) -> Wf (fun var => unnatize_expr 0 (e (fun t => (nat * var t)%type))). Proof. intros H var1 var2; specialize (H var1 var2). - pose proof (@reflect_wf base_type_code interp_base_type base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 nil t t (e _) (e _)) as H'. + pose proof (@reflect_wf base_type_code base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 nil t t (e _) (e _)) as H'. rewrite type_eq_semidec_transparent_refl in H' by assumption; simpl in *. edestruct @reflect_wfT; simpl in *; tauto. Qed. @@ -246,7 +233,7 @@ Section Wf. Theorem reflect_Wf : (forall var1 var2, unnatize_expr 0 (e (fun t => (nat * var1 t)%type)) = e _ - /\ to_prop (@reflect_wfT base_type_code interp_base_type interp_base_type base_type_eq_semidec_transparent op (fun _ => rEq) op_beq var1 var2 nil t t (e _) (e _))) + /\ to_prop (@reflect_wfT base_type_code base_type_eq_semidec_transparent op op_beq var1 var2 nil t t (e _) (e _))) -> Wf e. Proof. intros H var1 var2. @@ -258,8 +245,8 @@ End Wf. Ltac generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl := lazymatch goal with - | [ |- @Wf ?base_type_code ?interp_base_type ?op ?t ?e ] - => generalize (@reflect_Wf_unnatize base_type_code interp_base_type _ base_type_eq_semidec_is_dec op _ op_beq_bl t e) + | [ |- @Wf ?base_type_code ?op ?t ?e ] + => generalize (@reflect_Wf_unnatize base_type_code _ base_type_eq_semidec_is_dec op _ op_beq_bl t e) end. Ltac use_reflect_Wf := let H := fresh in diff --git a/src/Reflection/WfReflectiveGen.v b/src/Reflection/WfReflectiveGen.v index 0d961ec97..a562531c3 100644 --- a/src/Reflection/WfReflectiveGen.v +++ b/src/Reflection/WfReflectiveGen.v @@ -63,11 +63,9 @@ Section language. enforced, but it will block [vm_compute] when trying to use the lemma in this file.) *) Context (base_type_code : Type) - (interp_base_type1 interp_base_type2 : base_type_code -> Type) (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)) (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2) - (op : flat_type base_type_code -> flat_type base_type_code -> Type) - (R : forall t, interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> reified_Prop). + (op : flat_type base_type_code -> flat_type base_type_code -> Type). (** In practice, semi-deciding equality of operators should either return [Some trivial] or [None], and not make use of the generality of [pointed_Prop]. However, we need to use @@ -83,16 +81,8 @@ Section language. (* convenience notations that fill in some arguments used across the section *) Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). - Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> Syntax.flat_type. - Local Notation interp_type1 := (interp_type interp_base_type1). - Local Notation interp_type2 := (interp_type interp_base_type2). - Local Notation interp_flat_type1 := (interp_flat_type interp_base_type1). - Local Notation interp_flat_type2 := (interp_flat_type interp_base_type2). - Local Notation exprf1 := (@exprf base_type_code interp_base_type1 op). - Local Notation exprf2 := (@exprf base_type_code interp_base_type2 op). - Local Notation expr1 := (@expr base_type_code interp_base_type1 op). - Local Notation expr2 := (@expr base_type_code interp_base_type2 op). + Local Notation exprf := (@exprf base_type_code op). + Local Notation expr := (@expr base_type_code op). Local Ltac inversion_base_type_code_step := match goal with @@ -105,10 +95,12 @@ Section language. (* lift [base_type_eq_semidec_transparent] across [flat_type] *) Fixpoint flat_type_eq_semidec_transparent (t1 t2 : flat_type) : option (t1 = t2) := match t1, t2 return option (t1 = t2) with - | Syntax.Tbase t1, Syntax.Tbase t2 + | Tbase t1, Tbase t2 => option_map (@f_equal _ _ Tbase _ _) - (base_type_eq_semidec_transparent t1 t2) - | Syntax.Tbase _, _ => None + (base_type_eq_semidec_transparent t1 t2) + | Tbase _, _ => None + | Unit, Unit => Some eq_refl + | Unit, _ => None | Prod A B, Prod A' B' => match flat_type_eq_semidec_transparent A A', flat_type_eq_semidec_transparent B B' with | Some p, Some q => Some (f_equal2 Prod p q) @@ -139,7 +131,7 @@ Section language. Lemma flat_type_eq_semidec_transparent_refl t : flat_type_eq_semidec_transparent t t = Some eq_refl. Proof. clear -base_type_eq_semidec_is_dec. - induction t as [t | A B IHt]; simpl. + induction t as [t | | A B IHt]; simpl; try reflexivity. { rewrite base_type_eq_semidec_transparent_refl; reflexivity. } { rewrite_hyp !*; reflexivity. } Qed. @@ -195,10 +187,6 @@ Section language. base_type_eq_semidec_transparent _ _ var1 var1 (fun _ => rEq) (fst (projT2 x)) (fst (projT2 y)) /\ eq_semidec_and_gen base_type_eq_semidec_transparent _ _ var2 var2 (fun _ => rEq) (snd (projT2 x)) (snd (projT2 y)))%reified_prop. - Definition rel_type_and_const (t t' : flat_type) (x : interp_flat_type1 t) (y : interp_flat_type2 t') - : reified_Prop - := eq_semidec_and_gen - flat_type_eq_semidec_transparent _ _ interp_flat_type1 interp_flat_type2 R x y. Definition duplicate_type (ls : list (sigT (fun t => var1 t * var2 t)%type)) : list (sigT eP) := List.map (fun v => existT eP (projT1 v, projT1 v) (projT2 v)) ls. @@ -247,59 +235,56 @@ Section language. let base := fst ret in let b := snd ret in (base, (a, b)) - | Syntax.Tbase t => fun v => (S base, (base, v)) + | Unit => fun _ => (base, tt) + | Tbase t => fun v => (S base, (base, v)) end v. Arguments natize_interp_flat_type {var t} _ _. Lemma length_natize_interp_flat_type1 {t} (base : nat) (v1 : interp_flat_type var1 t) (v2 : interp_flat_type var2 t) : fst (natize_interp_flat_type base v1) = length (flatten_binding_list base_type_code v1 v2) + base. Proof. - revert base; induction t; simpl; [ reflexivity | ]. + revert base; induction t; simpl; [ reflexivity | reflexivity | ]. intros; rewrite List.app_length, <- plus_assoc. rewrite_hyp <- ?*; reflexivity. Qed. Lemma length_natize_interp_flat_type2 {t} (base : nat) (v1 : interp_flat_type var1 t) (v2 : interp_flat_type var2 t) : fst (natize_interp_flat_type base v2) = length (flatten_binding_list base_type_code v1 v2) + base. Proof. - revert base; induction t; simpl; [ reflexivity | ]. + revert base; induction t; simpl; [ reflexivity | reflexivity | ]. intros; rewrite List.app_length, <- plus_assoc. rewrite_hyp <- ?*; reflexivity. Qed. (* This function strips De Bruijn indices from expressions *) - Fixpoint unnatize_exprf {interp_base_type var t} (base : nat) - (e : @Syntax.exprf base_type_code interp_base_type op (fun t => nat * var t)%type t) - : @Syntax.exprf base_type_code interp_base_type op var t - := match e in @Syntax.exprf _ _ _ _ t return Syntax.exprf _ _ _ t with - | Const _ x => Const x + Fixpoint unnatize_exprf {var t} (base : nat) + (e : @Syntax.exprf base_type_code op (fun t => nat * var t)%type t) + : @Syntax.exprf base_type_code op var t + := match e in @Syntax.exprf _ _ _ t return Syntax.exprf _ _ t with + | TT => TT | Var _ x => Var (snd x) - | Op _ _ op args => Op op (@unnatize_exprf _ _ _ base args) - | LetIn _ ex _ eC => LetIn (@unnatize_exprf _ _ _ base ex) + | Op _ _ op args => Op op (@unnatize_exprf _ _ base args) + | LetIn _ ex _ eC => LetIn (@unnatize_exprf _ _ base ex) (fun x => let v := natize_interp_flat_type base x in - @unnatize_exprf _ _ _ (fst v) (eC (snd v))) - | Pair _ x _ y => Pair (@unnatize_exprf _ _ _ base x) (@unnatize_exprf _ _ _ base y) + @unnatize_exprf _ _ (fst v) (eC (snd v))) + | Pair _ x _ y => Pair (@unnatize_exprf _ _ base x) (@unnatize_exprf _ _ base y) end. - Fixpoint unnatize_expr {interp_base_type var t} (base : nat) - (e : @Syntax.expr base_type_code interp_base_type op (fun t => nat * var t)%type t) - : @Syntax.expr base_type_code interp_base_type op var t - := match e in @Syntax.expr _ _ _ _ t return Syntax.expr _ _ _ t with + Fixpoint unnatize_expr {var t} (base : nat) + (e : @Syntax.expr base_type_code op (fun t => nat * var t)%type t) + : @Syntax.expr base_type_code op var t + := match e in @Syntax.expr _ _ _ t return Syntax.expr _ _ t with | Return _ x => unnatize_exprf base x - | Abs tx tR f => Abs (fun x : var tx => let v := natize_interp_flat_type (t:=tx) base x in - @unnatize_expr _ _ _ (fst v) (f (snd v))) + | Abs tx tR f => Abs (fun x : var tx => let v := natize_interp_flat_type (t:=Tbase tx) base x in + @unnatize_expr _ _ (fst v) (f (snd v))) end. Fixpoint reflect_wffT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) {t1 t2 : flat_type} - (e1 : @exprf1 (fun t => nat * var1 t)%type t1) - (e2 : @exprf2 (fun t => nat * var2 t)%type t2) + (e1 : @exprf (fun t => nat * var1 t)%type t1) + (e2 : @exprf (fun t => nat * var2 t)%type t2) {struct e1} : reified_Prop := match e1, e2 with - | Const t0 x, Const t1 y - => match flat_type_eq_semidec_transparent t0 t1 with - | Some p => R _ (eq_rect _ interp_flat_type1 x _ p) y - | None => rFalse - end - | Const _ _, _ => rFalse + | TT, TT => rTrue + | TT, _ => rFalse | Var t0 x, Var t1 y => match beq_nat (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with | true, Some v => eq_type_and_var v (existT _ (t0, t1) (snd x, snd y)) @@ -328,8 +313,8 @@ Section language. Fixpoint reflect_wfT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) {t1 t2 : type} - (e1 : @expr1 (fun t => nat * var1 t)%type t1) - (e2 : @expr2 (fun t => nat * var2 t)%type t2) + (e1 : @expr (fun t => nat * var1 t)%type t1) + (e2 : @expr (fun t => nat * var2 t)%type t2) {struct e1} : reified_Prop := match e1, e2 with @@ -337,9 +322,9 @@ Section language. => reflect_wffT G x y | Return _ _, _ => rFalse | Abs tx tR f, Abs tx' tR' f' - => match @flatten_binding_list2 tx tx', type_eq_semidec_transparent tR tR' with + => match @flatten_binding_list2 (Tbase tx) (Tbase tx'), type_eq_semidec_transparent tR tR' with | Some G0, Some _ - => ∀ (x : interp_flat_type var1 tx) (x' : interp_flat_type var2 tx'), + => ∀ (x : interp_flat_type var1 (Tbase tx)) (x' : interp_flat_type var2 (Tbase tx')), @reflect_wfT (G0 x x' ++ G)%list _ _ (f (snd (natize_interp_flat_type (List.length G) x))) (f' (snd (natize_interp_flat_type (List.length G) x'))) @@ -349,8 +334,8 @@ Section language. end%reified_prop. End language. -Global Arguments reflect_wffT {_ _ _} _ {op} R _ {var1 var2} G {t1 t2} _ _. -Global Arguments reflect_wfT {_ _ _} _ {op} R _ {var1 var2} G {t1 t2} _ _. -Global Arguments unnatize_exprf {_ _ _ _ _} _ _. -Global Arguments unnatize_expr {_ _ _ _ _} _ _. +Global Arguments reflect_wffT {_} _ {op} _ {var1 var2} G {t1 t2} _ _. +Global Arguments reflect_wfT {_} _ {op} _ {var1 var2} G {t1 t2} _ _. +Global Arguments unnatize_exprf {_ _ _ _} _ _. +Global Arguments unnatize_expr {_ _ _ _} _ _. Global Arguments natize_interp_flat_type {_ _ t} _ _. diff --git a/src/Reflection/WfRel.v b/src/Reflection/WfRel.v deleted file mode 100644 index 3e32d9b3f..000000000 --- a/src/Reflection/WfRel.v +++ /dev/null @@ -1,57 +0,0 @@ -Require Import Coq.Strings.String Coq.Classes.RelationClasses. -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Tactics. -Require Import Crypto.Util.Notations. -Local Open Scope ctype_scope. -Local Open Scope expr_scope. - -Section language. - Context (base_type_code : Type). - Context (interp_base_type1 interp_base_type2 : base_type_code -> Type). - Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). - Context (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop). - - Section wf. - Context {var1 var2 : base_type_code -> Type}. - - Local Notation eP := (fun t => var1 t * var2 t)%type (only parsing). - Local Notation "x == y" := (existT eP _ (x, y)%core). - - Notation exprf1 := (@exprf base_type_code interp_base_type1 op var1). - Notation exprf2 := (@exprf base_type_code interp_base_type2 op var2). - Notation expr1 := (@expr base_type_code interp_base_type1 op var1). - Notation expr2 := (@expr base_type_code interp_base_type2 op var2). - - Inductive rel_wff : list (sigT eP) -> forall {t}, exprf1 t -> exprf2 t -> Prop := - | RWfConst : forall t G n n', interp_flat_type_rel_pointwise2 R n n' -> @rel_wff G t (Const n) (Const n') - | RWfVar : forall G (t : base_type_code) x x', List.In (x == x') G -> @rel_wff G (Tbase t) (Var x) (Var x') - | RWfOp : forall G {t} {tR} (e : exprf1 t) (e' : exprf2 t) op, - rel_wff G e e' - -> rel_wff G (Op (tR := tR) op e) (Op (tR := tR) op e') - | RWfLetIn : forall G t1 t2 e1 e1' (e2 : interp_flat_type var1 t1 -> exprf1 t2) e2', - rel_wff G e1 e1' - -> (forall x1 x2, rel_wff (flatten_binding_list base_type_code x1 x2 ++ G) (e2 x1) (e2' x2)) - -> rel_wff G (LetIn e1 e2) (LetIn e1' e2') - | RWfPair : forall G {t1} {t2} (e1: exprf1 t1) (e2: exprf1 t2) - (e1': exprf2 t1) (e2': exprf2 t2), - rel_wff G e1 e1' - -> rel_wff G e2 e2' - -> rel_wff G (Pair e1 e2) (Pair e1' e2'). - - Inductive rel_wf : list (sigT eP) -> forall {t}, expr1 t -> expr2 t -> Prop := - | WfReturn : forall t G e e', @rel_wff G t e e' -> rel_wf G (Return e) (Return e') - | WfAbs : forall A B G e e', - (forall x x', @rel_wf ((x == x') :: G) B (e x) (e' x')) - -> @rel_wf G (Arrow A B) (Abs e) (Abs e'). - End wf. - - Definition RelWf {t} - (E1 : @Expr base_type_code interp_base_type1 op t) - (E2 : @Expr base_type_code interp_base_type2 op t) - := forall var1 var2, rel_wf nil (E1 var1) (E2 var2). -End language. - -Global Arguments rel_wff {_ _ _ _} R {_ _} G {t} _ _. -Global Arguments rel_wf {_ _ _ _} R {_ _} G {t} _ _. -Global Arguments RelWf {_ _ _ _} R {t} _ _. diff --git a/src/Reflection/Z/Interpretations128/Relations.v b/src/Reflection/Z/Interpretations128/Relations.v index 5ce0df08e..fcd7bf2d8 100644 --- a/src/Reflection/Z/Interpretations128/Relations.v +++ b/src/Reflection/Z/Interpretations128/Relations.v @@ -2,7 +2,8 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Psatz. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.Tuple. Require Import Crypto.Reflection.Z.InterpretationsGen. Require Import Crypto.Reflection.Z.Interpretations128. Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperationsProofs. @@ -152,7 +153,7 @@ Lemma related_tuples_None_left (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n))) : interp_flat_type_rel_pointwise2 R - (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option (n:=S n) None)) + (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option None)) v. Proof. induction n; simpl; intuition. @@ -162,16 +163,17 @@ Lemma related_tuples_Some_left n T interp_base_type' (R : forall t, T -> interp_base_type' t -> Prop) u - (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n))) + (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) n)) : interp_flat_type_rel_pointwise2 R - (flat_interp_untuple' (T:=Tbase TZ) u) + (flat_interp_untuple (T:=Tbase TZ) u) v <-> interp_flat_type_rel_pointwise2 (LiftOption.lift_relation R) - (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option (n:=S n) (Some u))) + (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option (Some u))) v. Proof. + destruct n as [|n]; [ reflexivity | ]. induction n; [ reflexivity | ]. simpl in *; rewrite <- IHn; clear IHn. reflexivity. @@ -181,14 +183,15 @@ Lemma related_tuples_Some_left_ext {n T interp_base_type'} {R : forall t, T -> interp_base_type' t -> Prop} {u v u'} - (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=S n) u) = Some u') + (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=n) u) = Some u') : interp_flat_type_rel_pointwise2 R - (flat_interp_untuple' (T:=Tbase TZ) u') v + (flat_interp_untuple (T:=Tbase TZ) u') v <-> interp_flat_type_rel_pointwise2 (LiftOption.lift_relation R) u v. Proof. + destruct n as [|n]; [ reflexivity | ]. induction n. { simpl in *; subst; reflexivity. } { destruct_head_hnf' prod. @@ -200,13 +203,14 @@ Qed. Lemma related_tuples_proj_eq_rel_untuple {n T interp_base_type'} {proj : forall t, T -> interp_base_type' t} - {u : Tuple.tuple _ (S n)} {v : Tuple.tuple _ (S n)} + {u : Tuple.tuple _ n} {v : Tuple.tuple _ n} : interp_flat_type_rel_pointwise2 (fun t => proj_eq_rel (proj t)) - (flat_interp_untuple' (T:=Tbase TZ) u) - (flat_interp_untuple' (T:=Tbase TZ) v) + (flat_interp_untuple (T:=Tbase TZ) u) + (flat_interp_untuple (T:=Tbase TZ) v) <-> (Tuple.map (proj _) u = v). Proof. + destruct n as [|n]; [ destruct_head_hnf' unit; simpl; tauto | ]. induction n; [ reflexivity | ]. destruct_head_hnf' prod. simpl @Tuple.tuple. @@ -222,27 +226,27 @@ Lemma related_tuples_proj_eq_rel_tuple : interp_flat_type_rel_pointwise2 (fun t => proj_eq_rel (proj t)) u v - <-> (Tuple.map (proj _) (flat_interp_tuple (n:=S n) (T:=Tbase TZ) u) + <-> (Tuple.map (proj _) (flat_interp_tuple (n:=n) (T:=Tbase TZ) u) = flat_interp_tuple (T:=Tbase TZ) v). Proof. - rewrite <- related_tuples_proj_eq_rel_untuple, !flat_interp_untuple'_tuple; reflexivity. + rewrite <- related_tuples_proj_eq_rel_untuple, !flat_interp_untuple_tuple; reflexivity. Qed. Local Arguments LiftOption.lift_relation2 _ _ _ _ !_ !_ / . -Lemma related_tuples_lift_relation2_untuple' +Lemma related_tuples_lift_relation2_untuple n T U (R : T -> U -> Prop) (t : option (Tuple.tuple T (S n))) (u : option (Tuple.tuple U (S n))) : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) - (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option t)) - (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option u)) + (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option t)) + (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option u)) <-> LiftOption.lift_relation2 (interp_flat_type_rel_pointwise2 (fun _ => R)) TZ - (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t) - (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u). + (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t) + (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u). Proof. induction n. { destruct_head' option; reflexivity. } @@ -255,7 +259,7 @@ Proof. try (simpl @interp_flat_type_rel_pointwise2; tauto). } Qed. -Lemma related_tuples_lift_relation2_untuple'_ext +Lemma related_tuples_lift_relation2_untuple_ext {n T U} {R : T -> U -> Prop} {t u} @@ -267,8 +271,8 @@ Lemma related_tuples_lift_relation2_untuple'_ext <-> LiftOption.lift_relation2 (interp_flat_type_rel_pointwise2 (fun _ => R)) TZ - (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t))) - (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))). + (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t))) + (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))). Proof. induction n. { destruct_head_hnf' option; reflexivity. } @@ -293,22 +297,22 @@ Proof. | progress break_match ] ]. } Qed. -Lemma lift_option_flat_interp_tuple' +Lemma lift_option_flat_interp_tuple {n T x y} - : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple' (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y) - <-> (x = flat_interp_untuple' (T:=Tbase TZ) (n:=n) (Tuple.push_option (n:=S n) (Some y))). + : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y) + <-> (x = flat_interp_untuple (T:=Tbase TZ) (n:=S n) (Tuple.push_option (n:=S n) (Some y))). Proof. rewrite Tuple.push_lift_option; generalize (Tuple.push_option (Some y)); intro. split; intro; subst; - rewrite ?flat_interp_tuple'_untuple', ?flat_interp_untuple'_tuple'; + rewrite ?flat_interp_tuple_untuple, ?flat_interp_untuple_tuple; reflexivity. Qed. Lemma lift_option_None_interp_flat_type_rel_pointwise2_1 T U n R x y (H : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) x y) - (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) x) = None) - : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) y) = None. + (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) x) = None) + : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) y) = None. Proof. induction n; [ | specialize (IHn (fst x) (fst y) (proj1 H)) ]; repeat first [ progress destruct_head_hnf' False @@ -328,12 +332,18 @@ Local Arguments LiftOption.lift_relation _ _ _ _ !_ _ / . Local Arguments LiftOption.of' _ _ !_ / . Local Arguments BoundedWordW.BoundedWordToBounds !_ / . +Local Ltac unfold_related_const := + intros; hnf; simpl; + unfold related_wordW, LiftOption.lift_relation, LiftOption.of', BoundedWordW.wordWToBoundedWord, BoundedWordW.SmartBuildBoundedWord, BoundedWordW.of_Z, BoundedWordW.of_wordW, BoundedWordW.wordWToBoundedWord; + simpl. + Lemma related_wordW_op : related_op related_wordW (@BoundedWordW.interp_op) (@WordW.interp_op). Proof. (let op := fresh in intros ?? op; destruct op; simpl); try first [ apply related_wordW_t_map1 | apply related_wordW_t_map2 - | apply related_wordW_t_map4 ]. + | apply related_wordW_t_map4 + | unfold_related_const; break_innermost_match; reflexivity ]. Qed. Lemma related_bounds_t_map1 opW opB pf @@ -383,9 +393,25 @@ Local Arguments Tuple.map : simpl never. Local Arguments Tuple.map2 : simpl never. Local Arguments ZBounds.SmartBuildBounds _ _ / . + +Local Ltac related_const_op_t := + unfold_related_const; break_innermost_match; try reflexivity; hnf; simpl; + repeat match goal with + | [ H : andb _ _ = true |- _ ] => apply andb_prop in H + | _ => progress destruct_head' and + | _ => progress Z.ltb_to_lt + | _ => rewrite WordW.wordWToZ_ZToWordW by (simpl @Z.of_nat; omega) + | [ H : _ |- _ ] => rewrite WordW.wordWToZ_ZToWordW in H by (simpl @Z.of_nat; omega) + | [ H : (Z.log2 ?x < ?y)%Z |- _ ] + => unique assert (x < 2^y)%Z by (apply WordW.log2_lt_pow2_alt_proj_r2l; omega) + | _ => reflexivity + | _ => omega + end. + Lemma related_bounds_op : related_op related_bounds (@BoundedWordW.interp_op) (@ZBounds.interp_op). Proof. let op := fresh in intros ?? op; destruct op; simpl. + { related_const_op_t. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } @@ -515,6 +541,7 @@ Local Arguments ZBounds.neg _ !_ / . Lemma related_Z_op : related_op related_Z (@BoundedWordW.interp_op) (@Z.interp_op). Proof. let op := fresh in intros ?? op; destruct op; simpl. + { related_const_op_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } diff --git a/src/Reflection/Z/Interpretations128/RelationsCombinations.v b/src/Reflection/Z/Interpretations128/RelationsCombinations.v index 64c0fceb1..2de4510c7 100644 --- a/src/Reflection/Z/Interpretations128/RelationsCombinations.v +++ b/src/Reflection/Z/Interpretations128/RelationsCombinations.v @@ -1,6 +1,7 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Z.InterpretationsGen. Require Import Crypto.Reflection.Z.Interpretations128. @@ -72,7 +73,8 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl; [ solve [ trivial | reflexivity ] | ]. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; + [ solve [ trivial | reflexivity ] | reflexivity | ]. intros [HA HB]. specialize (IHA _ _ HA); specialize (IHB _ _ HB). unfold R in *. @@ -122,7 +124,8 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj_option. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl; [ solve [ trivial | reflexivity ] | ]. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; + [ solve [ trivial | reflexivity ] | reflexivity | ]. intros [HA HB]. specialize (IHA _ _ HA); specialize (IHB _ _ HB). unfold R in *. @@ -181,7 +184,8 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj_option2. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl; [ solve [ trivial | reflexivity ] | ]. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; + [ solve [ trivial | reflexivity ] | reflexivity | ]. intros [HA HB]. specialize (IHA _ _ HA); specialize (IHB _ _ HB). unfold R in *. @@ -247,7 +251,7 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj_from_option2. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity. { cbv [LiftOption.lift_relation proj_eq_rel R]. break_match; try tauto; intros; subst. apply proj012. } @@ -318,7 +322,7 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj1_from_option2. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity. { cbv [LiftOption.lift_relation proj_eq_rel LiftOption.lift_relation2]. break_match; try tauto; intros; subst. apply proj012R. } diff --git a/src/Reflection/Z/Interpretations64/Relations.v b/src/Reflection/Z/Interpretations64/Relations.v index 80f3d139c..6b4279043 100644 --- a/src/Reflection/Z/Interpretations64/Relations.v +++ b/src/Reflection/Z/Interpretations64/Relations.v @@ -2,7 +2,8 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Psatz. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.Application. +Require Import Crypto.Reflection.Relations. +Require Import Crypto.Reflection.Tuple. Require Import Crypto.Reflection.Z.InterpretationsGen. Require Import Crypto.Reflection.Z.Interpretations64. Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperationsProofs. @@ -152,7 +153,7 @@ Lemma related_tuples_None_left (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n))) : interp_flat_type_rel_pointwise2 R - (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option (n:=S n) None)) + (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option None)) v. Proof. induction n; simpl; intuition. @@ -162,16 +163,17 @@ Lemma related_tuples_Some_left n T interp_base_type' (R : forall t, T -> interp_base_type' t -> Prop) u - (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) (S n))) + (v : interp_flat_type interp_base_type' (tuple (Tbase TZ) n)) : interp_flat_type_rel_pointwise2 R - (flat_interp_untuple' (T:=Tbase TZ) u) + (flat_interp_untuple (T:=Tbase TZ) u) v <-> interp_flat_type_rel_pointwise2 (LiftOption.lift_relation R) - (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option (n:=S n) (Some u))) + (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option (Some u))) v. Proof. + destruct n as [|n]; [ reflexivity | ]. induction n; [ reflexivity | ]. simpl in *; rewrite <- IHn; clear IHn. reflexivity. @@ -181,14 +183,15 @@ Lemma related_tuples_Some_left_ext {n T interp_base_type'} {R : forall t, T -> interp_base_type' t -> Prop} {u v u'} - (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=S n) u) = Some u') + (H : Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) (n:=n) u) = Some u') : interp_flat_type_rel_pointwise2 R - (flat_interp_untuple' (T:=Tbase TZ) u') v + (flat_interp_untuple (T:=Tbase TZ) u') v <-> interp_flat_type_rel_pointwise2 (LiftOption.lift_relation R) u v. Proof. + destruct n as [|n]; [ reflexivity | ]. induction n. { simpl in *; subst; reflexivity. } { destruct_head_hnf' prod. @@ -200,13 +203,14 @@ Qed. Lemma related_tuples_proj_eq_rel_untuple {n T interp_base_type'} {proj : forall t, T -> interp_base_type' t} - {u : Tuple.tuple _ (S n)} {v : Tuple.tuple _ (S n)} + {u : Tuple.tuple _ n} {v : Tuple.tuple _ n} : interp_flat_type_rel_pointwise2 (fun t => proj_eq_rel (proj t)) - (flat_interp_untuple' (T:=Tbase TZ) u) - (flat_interp_untuple' (T:=Tbase TZ) v) + (flat_interp_untuple (T:=Tbase TZ) u) + (flat_interp_untuple (T:=Tbase TZ) v) <-> (Tuple.map (proj _) u = v). Proof. + destruct n as [|n]; [ destruct_head_hnf' unit; simpl; tauto | ]. induction n; [ reflexivity | ]. destruct_head_hnf' prod. simpl @Tuple.tuple. @@ -222,27 +226,27 @@ Lemma related_tuples_proj_eq_rel_tuple : interp_flat_type_rel_pointwise2 (fun t => proj_eq_rel (proj t)) u v - <-> (Tuple.map (proj _) (flat_interp_tuple (n:=S n) (T:=Tbase TZ) u) + <-> (Tuple.map (proj _) (flat_interp_tuple (n:=n) (T:=Tbase TZ) u) = flat_interp_tuple (T:=Tbase TZ) v). Proof. - rewrite <- related_tuples_proj_eq_rel_untuple, !flat_interp_untuple'_tuple; reflexivity. + rewrite <- related_tuples_proj_eq_rel_untuple, !flat_interp_untuple_tuple; reflexivity. Qed. Local Arguments LiftOption.lift_relation2 _ _ _ _ !_ !_ / . -Lemma related_tuples_lift_relation2_untuple' +Lemma related_tuples_lift_relation2_untuple n T U (R : T -> U -> Prop) (t : option (Tuple.tuple T (S n))) (u : option (Tuple.tuple U (S n))) : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) - (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option t)) - (flat_interp_untuple' (T:=Tbase TZ) (Tuple.push_option u)) + (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option t)) + (flat_interp_untuple (T:=Tbase TZ) (Tuple.push_option u)) <-> LiftOption.lift_relation2 (interp_flat_type_rel_pointwise2 (fun _ => R)) TZ - (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t) - (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u). + (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t) + (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u). Proof. induction n. { destruct_head' option; reflexivity. } @@ -255,7 +259,7 @@ Proof. try (simpl @interp_flat_type_rel_pointwise2; tauto). } Qed. -Lemma related_tuples_lift_relation2_untuple'_ext +Lemma related_tuples_lift_relation2_untuple_ext {n T U} {R : T -> U -> Prop} {t u} @@ -267,8 +271,8 @@ Lemma related_tuples_lift_relation2_untuple'_ext <-> LiftOption.lift_relation2 (interp_flat_type_rel_pointwise2 (fun _ => R)) TZ - (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t))) - (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))). + (option_map (flat_interp_untuple (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t))) + (option_map (flat_interp_untuple (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))). Proof. induction n. { destruct_head_hnf' option; reflexivity. } @@ -293,22 +297,22 @@ Proof. | progress break_match ] ]. } Qed. -Lemma lift_option_flat_interp_tuple' +Lemma lift_option_flat_interp_tuple {n T x y} - : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple' (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y) - <-> (x = flat_interp_untuple' (T:=Tbase TZ) (n:=n) (Tuple.push_option (n:=S n) (Some y))). + : (Tuple.lift_option (n:=S n) (A:=T) (flat_interp_tuple (interp_base_type:=LiftOption.interp_base_type' _) (T:=Tbase TZ) x) = Some y) + <-> (x = flat_interp_untuple (T:=Tbase TZ) (n:=S n) (Tuple.push_option (n:=S n) (Some y))). Proof. rewrite Tuple.push_lift_option; generalize (Tuple.push_option (Some y)); intro. split; intro; subst; - rewrite ?flat_interp_tuple'_untuple', ?flat_interp_untuple'_tuple'; + rewrite ?flat_interp_tuple_untuple, ?flat_interp_untuple_tuple; reflexivity. Qed. Lemma lift_option_None_interp_flat_type_rel_pointwise2_1 T U n R x y (H : interp_flat_type_rel_pointwise2 (LiftOption.lift_relation2 R) x y) - (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) x) = None) - : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple' (T:=Tbase TZ) (n:=n) y) = None. + (HNone : Tuple.lift_option (A:=T) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) x) = None) + : Tuple.lift_option (A:=U) (n:=S n) (flat_interp_tuple (T:=Tbase TZ) (n:=S n) y) = None. Proof. induction n; [ | specialize (IHn (fst x) (fst y) (proj1 H)) ]; repeat first [ progress destruct_head_hnf' False @@ -328,12 +332,18 @@ Local Arguments LiftOption.lift_relation _ _ _ _ !_ _ / . Local Arguments LiftOption.of' _ _ !_ / . Local Arguments BoundedWordW.BoundedWordToBounds !_ / . +Local Ltac unfold_related_const := + intros; hnf; simpl; + unfold related_wordW, LiftOption.lift_relation, LiftOption.of', BoundedWordW.wordWToBoundedWord, BoundedWordW.SmartBuildBoundedWord, BoundedWordW.of_Z, BoundedWordW.of_wordW, BoundedWordW.wordWToBoundedWord; + simpl. + Lemma related_wordW_op : related_op related_wordW (@BoundedWordW.interp_op) (@WordW.interp_op). Proof. (let op := fresh in intros ?? op; destruct op; simpl); try first [ apply related_wordW_t_map1 | apply related_wordW_t_map2 - | apply related_wordW_t_map4 ]. + | apply related_wordW_t_map4 + | unfold_related_const; break_innermost_match; reflexivity ]. Qed. Lemma related_bounds_t_map1 opW opB pf @@ -383,9 +393,25 @@ Local Arguments Tuple.map : simpl never. Local Arguments Tuple.map2 : simpl never. Local Arguments ZBounds.SmartBuildBounds _ _ / . + +Local Ltac related_const_op_t := + unfold_related_const; break_innermost_match; try reflexivity; hnf; simpl; + repeat match goal with + | [ H : andb _ _ = true |- _ ] => apply andb_prop in H + | _ => progress destruct_head' and + | _ => progress Z.ltb_to_lt + | _ => rewrite WordW.wordWToZ_ZToWordW by (simpl @Z.of_nat; omega) + | [ H : _ |- _ ] => rewrite WordW.wordWToZ_ZToWordW in H by (simpl @Z.of_nat; omega) + | [ H : (Z.log2 ?x < ?y)%Z |- _ ] + => unique assert (x < 2^y)%Z by (apply WordW.log2_lt_pow2_alt_proj_r2l; omega) + | _ => reflexivity + | _ => omega + end. + Lemma related_bounds_op : related_op related_bounds (@BoundedWordW.interp_op) (@ZBounds.interp_op). Proof. let op := fresh in intros ?? op; destruct op; simpl. + { related_const_op_t. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. } @@ -515,6 +541,7 @@ Local Arguments ZBounds.neg _ !_ / . Lemma related_Z_op : related_op related_Z (@BoundedWordW.interp_op) (@Z.interp_op). Proof. let op := fresh in intros ?? op; destruct op; simpl. + { related_const_op_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } { apply related_Z_t_map2; related_Z_op_fin_t. } diff --git a/src/Reflection/Z/Interpretations64/RelationsCombinations.v b/src/Reflection/Z/Interpretations64/RelationsCombinations.v index ecb65591b..8777cd7ed 100644 --- a/src/Reflection/Z/Interpretations64/RelationsCombinations.v +++ b/src/Reflection/Z/Interpretations64/RelationsCombinations.v @@ -1,6 +1,7 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Reflection.Z.Syntax. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Application. Require Import Crypto.Reflection.Z.InterpretationsGen. Require Import Crypto.Reflection.Z.Interpretations64. @@ -72,7 +73,8 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl; [ solve [ trivial | reflexivity ] | ]. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; + [ solve [ trivial | reflexivity ] | reflexivity | ]. intros [HA HB]. specialize (IHA _ _ HA); specialize (IHB _ _ HB). unfold R in *. @@ -122,7 +124,8 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj_option. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl; [ solve [ trivial | reflexivity ] | ]. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; + [ solve [ trivial | reflexivity ] | reflexivity | ]. intros [HA HB]. specialize (IHA _ _ HA); specialize (IHB _ _ HB). unfold R in *. @@ -181,7 +184,8 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj_option2. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl; [ solve [ trivial | reflexivity ] | ]. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; + [ solve [ trivial | reflexivity ] | reflexivity | ]. intros [HA HB]. specialize (IHA _ _ HA); specialize (IHB _ _ HB). unfold R in *. @@ -247,7 +251,7 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj_from_option2. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity. { cbv [LiftOption.lift_relation proj_eq_rel R]. break_match; try tauto; intros; subst. apply proj012. } @@ -318,7 +322,7 @@ Module Relations. Proof. unfold interp_type_rel_pointwise2_uncurried_proj1_from_option2. induction t as [t|A B IHt]; simpl; unfold Morphisms.respectful_hetero in *. - { induction t as [t|A IHA B IHB]; simpl. + { induction t as [t| |A IHA B IHB]; simpl; destruct_head_hnf' unit; try reflexivity. { cbv [LiftOption.lift_relation proj_eq_rel LiftOption.lift_relation2]. break_match; try tauto; intros; subst. apply proj012R. } diff --git a/src/Reflection/Z/InterpretationsGen.v b/src/Reflection/Z/InterpretationsGen.v index c24506cc1..3b403acc8 100644 --- a/src/Reflection/Z/InterpretationsGen.v +++ b/src/Reflection/Z/InterpretationsGen.v @@ -61,6 +61,7 @@ Module InterpretationsGen (Bit : BitSize). base_type interp_base_type' interp_flat_type (fun t => match t with TZ => fun x => x end) + (Some tt) (fun _ _ x y => match x, y with | Some x', Some y' => Some (x', y') | _, _ => None @@ -70,6 +71,7 @@ Module InterpretationsGen (Bit : BitSize). Fixpoint to' {t} : interp_flat_type t -> Syntax.interp_flat_type interp_base_type' t := match t return interp_flat_type t -> Syntax.interp_flat_type interp_base_type' t with | Tbase TZ => fun x => x + | Unit => fun _ => tt | Prod A B => fun x => (@to' A (option_map (@fst _ _) x), @to' B (option_map (@snd _ _) x)) end. @@ -268,6 +270,7 @@ Module InterpretationsGen (Bit : BitSize). end. Definition interp_op {src dst} (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with + | OpConst v => fun _ => ZToWordW v | Add => fun xy => fst xy + snd xy | Sub => fun xy => fst xy - snd xy | Mul => fun xy => fst xy * snd xy @@ -415,6 +418,7 @@ Module InterpretationsGen (Bit : BitSize). := LiftOption.interp_base_type' bounds ty. Definition interp_op {src dst} (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with + | OpConst v => fun _ => SmartBuildBounds v v | Add => fun xy => fst xy + snd xy | Sub => fun xy => fst xy - snd xy | Mul => fun xy => fst xy * snd xy @@ -520,6 +524,11 @@ Module InterpretationsGen (Bit : BitSize). | TZ => to_bounds' end. + Definition SmartBuildBoundedWord (v : Z) : t + := if ((0 <=? v) && (Z.log2 v <? WordW.bit_width))%Z%bool + then of_Z TZ v + else None. + Definition t_map1 (opW : WordW.wordW -> WordW.wordW) (opB : ZBounds.t -> ZBounds.t) @@ -794,6 +803,7 @@ Module InterpretationsGen (Bit : BitSize). Definition interp_op {src dst} (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with + | OpConst v => fun _ => SmartBuildBoundedWord v | Add => fun xy => fst xy + snd xy | Sub => fun xy => fst xy - snd xy | Mul => fun xy => fst xy * snd xy diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v index 1b6dc3bef..111cf34d2 100644 --- a/src/Reflection/Z/Reify.v +++ b/src/Reflection/Z/Reify.v @@ -33,14 +33,15 @@ Ltac base_reify_type T ::= end. Ltac Reify' e := Reflection.Reify.Reify' base_type interp_base_type op e. Ltac Reify e := - let v := Reflection.Reify.Reify base_type interp_base_type op e in - constr:((*Inline _*) ((*CSE _*) (InlineConst (Linearize v)))). + let v := Reflection.Reify.Reify base_type interp_base_type op make_const e in + constr:((*Inline _*) ((*CSE _*) (InlineConst is_const (Linearize v)))). Ltac prove_InlineConst_Linearize_Compile_correct := fun _ - => lazymatch goal with - | [ |- Syntax.interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst (Linearize _))) _ ] + => intros; + lazymatch goal with + | [ |- ?R (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst ?is_const (Linearize _))) _ ] => etransitivity; - [ apply (@Interp_InlineConst base_type_code interp_base_type op interp_op t); + [ apply (@Interp_InlineConst base_type_code interp_base_type op interp_op is_const t); reflect_Wf base_type_eq_semidec_is_dec op_beq_bl | etransitivity; [ apply (@Interp_Linearize base_type_code interp_base_type op interp_op t) diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v index ea867d024..311ceb53a 100644 --- a/src/Reflection/Z/Syntax.v +++ b/src/Reflection/Z/Syntax.v @@ -30,6 +30,7 @@ Local Notation eta3 x := (eta (fst x), snd x). Local Notation eta4 x := (eta3 (fst x), snd x). Inductive op : flat_type base_type -> flat_type base_type -> Type := +| OpConst (z : Z) : op Unit tZ | Add : op (tZ * tZ) tZ | Sub : op (tZ * tZ) tZ | Mul : op (tZ * tZ) tZ @@ -41,8 +42,14 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type := | Cmovne : op (tZ * tZ * tZ * tZ) tZ | Cmovle : op (tZ * tZ * tZ * tZ) tZ. +Definition make_const t : interp_base_type t -> op Unit (Syntax.Tbase t) + := match t with TZ => OpConst end. +Definition is_const s d (v : op s d) : bool + := match v with OpConst _ => true | _ => false end. + Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with + | OpConst v => fun _ => v | Add => fun xy => fst xy + snd xy | Sub => fun xy => fst xy - snd xy | Mul => fun xy => fst xy * snd xy @@ -67,6 +74,8 @@ Qed. Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : reified_Prop := match f, g return bool with + | OpConst v, OpConst v' => Z.eqb v v' + | OpConst _, _ => false | Add, Add => true | Add, _ => false | Sub, Sub => true |