diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-30 16:48:08 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-30 16:48:08 -0400 |
| commit | cb9e18103c6fe0580fa6598380b6c6ec66d261a0 (patch) | |
| tree | 38a66c5c1f8d9f8d022fb44d5edb62148f5b29bb /src/Reflection/MapCastByDeBruijnWf.v | |
| parent | 7d70da13d3d44c6eed92dfd490138d7a05120208 (diff) | |
Don't linearize and eta in MapCastByDeBruijn
Diffstat (limited to 'src/Reflection/MapCastByDeBruijnWf.v')
| -rw-r--r-- | src/Reflection/MapCastByDeBruijnWf.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v index 2cb7e2f40..7130c00ea 100644 --- a/src/Reflection/MapCastByDeBruijnWf.v +++ b/src/Reflection/MapCastByDeBruijnWf.v @@ -9,8 +9,6 @@ Require Import Crypto.Reflection.Named.CompileWf. Require Import Crypto.Reflection.Named.PositiveContext. Require Import Crypto.Reflection.Named.PositiveContext.Defaults. Require Import Crypto.Reflection.Named.PositiveContext.DefaultsProperties. -Require Import Crypto.Reflection.LinearizeWf. -Require Import Crypto.Reflection.EtaWf. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.MapCastByDeBruijn. Require Import Crypto.Util.Decidable. @@ -76,12 +74,11 @@ Section language. : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')), Wf e'. Proof. - unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, MapCastPreProcess, option_map; intros b e'. + unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, option_map; intros b e'. break_innermost_match; try congruence; intros ? v v'. inversion_option; inversion_sigma; subst; simpl in *; intros. unfold InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen. destruct t as [src dst]. - apply (proj2 (wf_expr_eta (t:=Arrow _ _))). eapply (@wf_interp_to_phoas base_type_code op FMapPositive.PositiveMap.key _ _ _ _ (PositiveContext base_type_code _ base_type_code_beq base_type_code_bl_transparent) @@ -90,9 +87,7 @@ Section language. (failb _) (failb _) _ e1); (eapply wf_map_cast with (fValues:=empty); eauto using PositiveContextOk with typeclass_instances); try (eapply (wf_compile (ContextOk:=PositiveContextOk)); - [ eapply (proj2 (wf_expr_eta (t:=Arrow _ _))); - [ eapply wf_linearize | .. ]; - eauto + [ eauto | .. | eassumption ]); try solve [ auto using name_list_unique_DefaultNamesFor |