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 | |
parent | 7d70da13d3d44c6eed92dfd490138d7a05120208 (diff) |
Don't linearize and eta in MapCastByDeBruijn
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/MapCastByDeBruijn.v | 19 | ||||
-rw-r--r-- | src/Reflection/MapCastByDeBruijnInterp.v | 23 | ||||
-rw-r--r-- | src/Reflection/MapCastByDeBruijnWf.v | 9 | ||||
-rw-r--r-- | src/Reflection/Z/Bounds/Interpretation.v (renamed from src/Reflection/Z/BoundsInterpretations.v) | 0 |
4 files changed, 18 insertions, 33 deletions
diff --git a/src/Reflection/MapCastByDeBruijn.v b/src/Reflection/MapCastByDeBruijn.v index 7998b0a37..68eb06a54 100644 --- a/src/Reflection/MapCastByDeBruijn.v +++ b/src/Reflection/MapCastByDeBruijn.v @@ -5,10 +5,12 @@ Require Import Crypto.Reflection.Named.InterpretToPHOAS. Require Import Crypto.Reflection.Named.Compile. Require Import Crypto.Reflection.Named.PositiveContext. Require Import Crypto.Reflection.Named.PositiveContext.Defaults. -Require Import Crypto.Reflection.Linearize. -Require Import Crypto.Reflection.Eta. Require Import Crypto.Reflection.Syntax. +(** N.B. This procedure only works when there are no nested lets, + i.e., nothing like [let x := let y := z in w] in the PHOAS syntax + tree. This is a limitation of [compile]. *) + Section language. Context {base_type_code : Type} {op : flat_type base_type_code -> flat_type base_type_code -> Type} @@ -28,14 +30,11 @@ Section language. Context {t} (e : Expr base_type_code op t) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)). - Definition MapCastPreProcess - := ExprEta (Linearize e). - Definition MapCastCompile (e' : Expr base_type_code op (domain t -> codomain t)) - := compile (e' _) (DefaultNamesFor e'). - Definition MapCastDoCast (e' : option (Named.expr base_type_code op BinNums.positive (domain t -> codomain t))) + Definition MapCastCompile + := compile (e _) (DefaultNamesFor e). + Definition MapCastDoCast (e' : option (Named.expr base_type_code op BinNums.positive t)) := option_map (fun e'' => map_cast - (t:=Arrow (domain t) (codomain t)) interp_op_bounds pick_typeb cast_op (BoundsContext:=PContext _) empty @@ -51,12 +50,12 @@ Section language. & Expr base_type_code op (Arrow (pick_type input_bounds) (pick_type output_bounds)) } := match e' with | Some (Some (existT output_bounds e'')) - => Some (existT _ output_bounds (Eta.ExprEta (InterpToPHOAS (Context:=fun var => PContext var) failb e''))) + => Some (existT _ output_bounds (InterpToPHOAS (Context:=fun var => PContext var) failb e'')) | Some None | None => None end. Definition MapCast : option { output_bounds : interp_flat_type interp_base_type_bounds (codomain t) & Expr base_type_code op (Arrow (pick_type input_bounds) (pick_type output_bounds)) } - := MapCastDoInterp (MapCastDoCast (MapCastCompile MapCastPreProcess)). + := MapCastDoInterp (MapCastDoCast MapCastCompile). End MapCast. End language. diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Reflection/MapCastByDeBruijnInterp.v index 7fa043791..74622223e 100644 --- a/src/Reflection/MapCastByDeBruijnInterp.v +++ b/src/Reflection/MapCastByDeBruijnInterp.v @@ -11,10 +11,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.EtaInterp. -Require Import Crypto.Reflection.EtaWf. -Require Import Crypto.Reflection.LinearizeInterp. -Require Import Crypto.Reflection.LinearizeWf. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.MapCastByDeBruijn. Require Import Crypto.Util.Decidable. @@ -83,7 +79,7 @@ Section language. /\ @inbounds _ b (Interp interp_op e v) /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v). 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. lazymatch goal with @@ -103,22 +99,17 @@ Section language. end | | change (interp interp_op (?e ?var) ?v') with (Interp interp_op e v'); - rewrite InterpExprEta; unfold Interp, InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen; rewrite <- interp_interp_to_phoas; [ reflexivity | ] ]. - { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _); - cbv [Eta.ExprEta Linearize.Linearize]; - [ rewrite interp_expr_eta, interp_linearize | .. ]; - [ reflexivity | eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ]; + { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=e _); + [ reflexivity | auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } - { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _); - cbv [Eta.ExprEta Linearize.Linearize]; - [ rewrite interp_expr_eta, interp_linearize | .. ]; - [ reflexivity | eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ]; + { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=e _); + [ reflexivity | auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } { intro; eapply wf_map_cast with (t := Arrow _ _) (fValues := empty); eauto using PositiveContextOk with typeclass_instances. - { eapply (wf_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _); - [ eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ]; + { eapply (wf_compile (ContextOk:=PositiveContextOk)) with (e':= e _); + [ auto | .. | eassumption ]; auto using name_list_unique_DefaultNamesFor. } { intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence. } } Qed. 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 diff --git a/src/Reflection/Z/BoundsInterpretations.v b/src/Reflection/Z/Bounds/Interpretation.v index 8e90213b6..8e90213b6 100644 --- a/src/Reflection/Z/BoundsInterpretations.v +++ b/src/Reflection/Z/Bounds/Interpretation.v |