diff options
author | Jason Gross <jgross@mit.edu> | 2017-03-19 18:38:47 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-03-19 18:38:47 -0400 |
commit | 8974f0676f16d583417e05413c51dc318f8de9f5 (patch) | |
tree | 88e33c0a9c0b890ecfa078053f803fd21a038a64 | |
parent | 2c2462799a8fc095754ade9cad82f9bbc8a81a10 (diff) |
Finish MapCastCorrect
-rw-r--r-- | src/Reflection/MapCastByDeBruijnInterp.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Reflection/MapCastByDeBruijnInterp.v index 97133bdaf..da5a4b3ca 100644 --- a/src/Reflection/MapCastByDeBruijnInterp.v +++ b/src/Reflection/MapCastByDeBruijnInterp.v @@ -4,8 +4,10 @@ Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.Named.Syntax. Require Import Crypto.Reflection.Named.ContextDefinitions. Require Import Crypto.Reflection.Named.MapCastInterp. +Require Import Crypto.Reflection.Named.MapCastWf. Require Import Crypto.Reflection.Named.InterpretToPHOASInterp. Require Import Crypto.Reflection.Named.CompileInterp. +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. @@ -88,10 +90,16 @@ Section language. | repeat first [ rewrite !lookupb_empty by (apply PositiveContextOk; assumption) | intro | congruence ] ]; - repeat first [ rewrite <- Interp_InterpToPHOAS; [ reflexivity | ] ]. + unfold Interp, InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen; + [ + | rewrite <- interp_interp_to_phoas; [ reflexivity | ] ]. { erewrite (interp_compile (ContextOk:=PositiveContextOk)), interp_linearize; [ reflexivity | apply wf_linearize; auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } - { - Admitted. + { intro; eapply wf_map_cast with (oldValues := empty); eauto using PositiveContextOk with typeclass_instances. + { eapply (wf_compile (ContextOk:=PositiveContextOk)); + [ apply wf_linearize; auto | .. | eassumption ]. + auto using name_list_unique_DefaultNamesFor. } + { intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence. } } + Qed. End language. |