diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Inline.v | 50 | ||||
-rw-r--r-- | src/Reflection/InlineInterp.v | 96 | ||||
-rw-r--r-- | src/Reflection/InlineWf.v | 166 | ||||
-rw-r--r-- | src/Reflection/InterpProofs.v | 42 | ||||
-rw-r--r-- | src/Reflection/Linearize.v | 30 | ||||
-rw-r--r-- | src/Reflection/LinearizeInterp.v | 99 | ||||
-rw-r--r-- | src/Reflection/LinearizeWf.v | 106 | ||||
-rw-r--r-- | src/Reflection/Syntax.v | 9 | ||||
-rw-r--r-- | src/Reflection/TestCase.v | 4 | ||||
-rw-r--r-- | src/Reflection/WfProofs.v | 51 | ||||
-rw-r--r-- | src/Specific/FancyMachine256/Core.v | 1 |
11 files changed, 416 insertions, 238 deletions
diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v new file mode 100644 index 000000000..a565835b0 --- /dev/null +++ b/src/Reflection/Inline.v @@ -0,0 +1,50 @@ +(** * Inline: Remove some [Let] expressions *) +Require Import Crypto.Reflection.Syntax. +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). + + 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_gen interp_base_type. + Local Notation Expr := (@Expr base_type_code interp_base_type op). + + Section with_var. + Context {var : base_type_code -> Type}. + Local Notation exprf := (@exprf base_type_code interp_base_type op). + Local Notation expr := (@expr base_type_code interp_base_type op). + + Fixpoint inline_constf {t} (e : @exprf (@exprf var) t) : @exprf var t + := match e in Syntax.exprf _ _ _ t return @exprf var t with + | Let _ ex tC eC + => match @inline_constf _ ex in Syntax.exprf _ _ _ t' return (interp_flat_type_gen _ t' -> @exprf var tC) -> @exprf var tC with + | Const _ x => fun eC => eC (SmartConst (op:=op) (var:=var) x) + | ex => fun eC => Let ex (fun x => eC (SmartVarVar x)) + end (fun x => @inline_constf _ (eC x)) + | Var _ x => x + | Const _ x => Const x + | Pair _ ex _ ey => Pair (@inline_constf _ ex) (@inline_constf _ ey) + | Op _ _ op args => Op op (@inline_constf _ args) + end. + + Fixpoint inline_const {t} (e : @expr (@exprf var) t) : @expr var t + := match e in Syntax.expr _ _ _ t return @expr var t with + | Return _ x => Return (inline_constf x) + | Abs _ _ f => Abs (fun x => @inline_const _ (f (Var x))) + end. + End with_var. + + Definition InlineConst {t} (e : Expr t) : Expr t + := fun var => inline_const (e _). +End language. + +Global Arguments inline_constf {_ _ _ _ _} _. +Global Arguments inline_const {_ _ _ _ _} _. +Global Arguments InlineConst {_ _ _ _} _ var. diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v new file mode 100644 index 000000000..d24cc2799 --- /dev/null +++ b/src/Reflection/InlineInterp.v @@ -0,0 +1,96 @@ +(** * Inline: Remove some [Let] expressions *) +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.InlineWf. +Require Import Crypto.Reflection.InterpProofs. +Require Import Crypto.Reflection.Inline. +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 (interp_op : forall src dst, op src dst -> interp_flat_type_gen interp_base_type src -> interp_flat_type_gen interp_base_type dst). + + 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_gen 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 Hint Extern 1 => eapply interpf_SmartConst. + Local Hint Extern 1 => eapply interpf_SmartVarVar. + + Local Ltac t_fin := + repeat match goal with + | _ => reflexivity + | _ => progress simpl in * + | _ => progress intros + | _ => progress inversion_sigma + | _ => progress inversion_prod + | _ => solve [ intuition eauto ] + | _ => apply (f_equal (interp_op _ _ _)) + | _ => apply (f_equal2 (@pair _ _)) + | _ => progress specialize_by assumption + | _ => progress subst + | [ H : context[List.In _ (_ ++ _)] |- _ ] => setoid_rewrite List.in_app_iff in H + | [ H : or _ _ |- _ ] => destruct H + | _ => progress break_match + | _ => rewrite <- !surjective_pairing + | [ H : ?x = _, H' : context[?x] |- _ ] => rewrite H in H' + | [ H : _ |- _ ] => apply H + | [ H : _ |- _ ] => rewrite H + end. + + Lemma interpf_inline_constf 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 + (x, x')) G + -> interpf interp_op x = x') + : interpf interp_op (inline_constf e1) = interpf interp_op e2. + Proof. + clear -wf H. + induction wf; t_fin. + Qed. + + Local Hint Resolve interpf_inline_constf. + + Lemma interp_inline_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 + (x, x')) G + -> interpf interp_op x = x') + : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _) + (interp interp_op (inline_const e1)) + (interp interp_op e2). + Proof. + induction wf. + { eapply interpf_inline_constf; eauto. } + { simpl in *; intro. + match goal with + | [ H : _ |- _ ] + => apply H; intuition (inversion_sigma; inversion_prod; subst; eauto) + end. } + Qed. + + Lemma Interp_InlineConst {t} (e : Expr t) + (wf : Wf e) + : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _) + (Interp interp_op (InlineConst e)) + (Interp interp_op e). + Proof. + unfold Interp, InlineConst. + eapply interp_inline_const with (G := nil); simpl; intuition. + Qed. +End language. diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v new file mode 100644 index 000000000..5822066e3 --- /dev/null +++ b/src/Reflection/InlineWf.v @@ -0,0 +1,166 @@ +(** * Inline: Remove some [Let] expressions *) +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.WfProofs. +Require Import Crypto.Reflection.Inline. +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). + + 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_gen 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). + + Section with_var. + Context {var1 var2 : base_type_code -> Type}. + + Local Ltac t_fin_step tac := + match goal with + | _ => assumption + | _ => progress simpl in * + | _ => progress subst + | _ => progress inversion_sigma + | _ => setoid_rewrite List.in_app_iff + | [ H : context[List.In _ (_ ++ _)] |- _ ] => setoid_rewrite List.in_app_iff in H + | _ => progress intros + | _ => solve [ eauto ] + | _ => solve [ intuition (subst; eauto) ] + | [ H : forall (x : prod _ _) (y : prod _ _), _ |- _ ] => specialize (fun x x' y y' => H (x, x') (y, y')) + | _ => rewrite !List.app_assoc + | [ H : _ \/ _ |- _ ] => destruct H + | [ H : _ |- _ ] => apply H + | _ => eapply wff_in_impl_Proper; [ solve [ eauto ] | ] + | _ => progress tac + | [ |- wff _ _ _ ] => constructor + | [ |- wf _ _ _ ] => constructor + end. + Local Ltac t_fin tac := repeat t_fin_step tac. + + Local Hint Constructors Syntax.wff. + Local Hint Resolve List.in_app_or List.in_or_app. + + Local Ltac small_inversion_helper wf G0 e2 := + let t0 := match type of wf with wff (t:=?t0) _ _ _ => t0 end in + let e1 := match goal with + | |- context[wff _ (inline_constf ?e1) (inline_constf e2)] => e1 + end in + pattern G0, t0, e1, e2; + lazymatch goal with + | [ |- ?retP _ _ _ _ ] + => first [ refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + return match v1 return Prop with + | Const _ _ => retP G t v1 v2 + | _ => forall P : Prop, P -> P + end with + | WfConst _ _ _ => _ + | _ => fun _ p => p + end) + | 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 + end with + | WfVar _ _ _ _ _ => _ + | _ => fun _ p => p + end) + | 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 + end with + | WfOp _ _ _ _ _ _ _ => _ + | _ => fun _ p => p + end) + | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 + return match v1 return Prop with + | Let _ _ _ _ => retP G t v1 v2 + | _ => forall P : Prop, P -> P + end with + | WfLet _ _ _ _ _ _ _ _ _ => _ + | _ => fun _ p => p + end) + | 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 + end with + | WfPair _ _ _ _ _ _ _ _ _ => _ + | _ => fun _ p => p + end) ] + end. + + Local Hint Constructors or. + Local Hint Extern 1 => progress unfold List.In in *. + Local Hint Resolve wff_in_impl_Proper. + Local Hint Resolve wff_SmartVar. + Local Hint Resolve wff_SmartConst. + + Fixpoint 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' + -> wff G x x') + (wf : wff G' e1 e2) + {struct e1} + : @wff var1 var2 G t (inline_constf e1) (inline_constf e2). + Proof. + (*revert H. + set (e1v := e1) in *. + destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ]; + [ clear wff_inline_constf + | clear wff_inline_constf + | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Op _ _ _ args => wff_inline_constf _ args + | _ => I + end); + clear wff_inline_constf + | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Let _ ex _ eC => wff_inline_constf _ ex + | _ => I + end); + generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Let _ ex _ eC => fun x => wff_inline_constf _ (eC x) + | _ => I + end); + clear wff_inline_constf + | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Pair _ ex _ ey => wff_inline_constf _ ex + | _ => I + end); + generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + | Pair _ ex _ ey => wff_inline_constf _ ey + | _ => I + end); + clear wff_inline_constf ]; + revert G; + (* alas, Coq's refiner isn't smart enough to figure out these small inversions for us *) + small_inversion_helper wf G' e2; + t_fin idtac; + repeat match goal with + | [ H : context[(_ -> wff _ (inline_constf ?e) (inline_constf _))%type], e2 : exprf _ |- _ ] + => is_var e; not constr_eq e e2; specialize (H e2) + | [ H : context[wff _ (@inline_constf ?A ?B ?C ?D ?E ?e) _] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ] + => destruct (@inline_constf A B C D E e) + | [ H : context[wff _ _ (@inline_constf ?A ?B ?C ?D ?E ?e)] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ] + => destruct (@inline_constf A B C D E e) + | [ IHwf : forall x y : list _, _, H1 : forall z : _, _, H2 : wff _ _ _ |- _ ] + => solve [ specialize (IHwf _ _ H1 H2); inversion IHwf ] + | [ |- wff _ _ _ ] => constructor + end. + 3:t_fin idtac. + 4:t_fin idtac. + { match goal with + | [ H : _ |- _ ] => eapply H; [ | solve [ eauto ] ]; t_fin idtac + end. }*) + Abort. + End with_var. +End language. diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v index 2d4ad5e0f..eb3e617e5 100644 --- a/src/Reflection/InterpProofs.v +++ b/src/Reflection/InterpProofs.v @@ -1,5 +1,6 @@ Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Util.Tactics. +Require Import Crypto.Reflection.WfProofs. +Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod. Local Open Scope ctype_scope. Section language. @@ -26,4 +27,43 @@ Section language. | _ => rewrite <- surjective_pairing end. Qed. + + Lemma interpf_SmartConst {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 (SmartConst 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_SmartVarVar {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 (SmartVarVar 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_SmartVarVar_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) + t (x, x')) + (flatten_binding_list (t := t') base_type_code (SmartVarVar v') v)) + : interpf interp_op x = x'. + Proof. + eapply interpf_SmartVarVar; subst; eassumption. + Qed. End language. diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v index 0c5a9083d..f60352e66 100644 --- a/src/Reflection/Linearize.v +++ b/src/Reflection/Linearize.v @@ -66,35 +66,8 @@ Section language. end. End with_var. - Section inline. - Context {var : base_type_code -> Type}. - Local Notation exprf := (@exprf base_type_code interp_base_type op). - Local Notation expr := (@expr base_type_code interp_base_type op). - - Fixpoint inline_constf {t} (e : @exprf (@exprf var) t) : @exprf var t - := match e in Syntax.exprf _ _ _ t return @exprf var t with - | Let _ ex tC eC - => match @inline_constf _ ex in Syntax.exprf _ _ _ t' return (interp_flat_type_gen _ t' -> @exprf var tC) -> @exprf var tC with - | Const _ x => fun eC => eC (SmartConst (op:=op) (var:=var) x) - | ex => fun eC => Let ex (fun x => eC (SmartVarVar x)) - end (fun x => @inline_constf _ (eC x)) - | Var _ x => x - | Const _ x => Const x - | Pair _ ex _ ey => Pair (@inline_constf _ ex) (@inline_constf _ ey) - | Op _ _ op args => Op op (@inline_constf _ args) - end. - - Fixpoint inline_const {t} (e : @expr (@exprf var) t) : @expr var t - := match e in Syntax.expr _ _ _ t return @expr var t with - | Return _ x => Return (inline_constf x) - | Abs _ _ f => Abs (fun x => @inline_const _ (f (Var x))) - end. - End inline. - Definition Linearize {t} (e : Expr t) : Expr t := fun var => linearize (e _). - Definition InlineConst {t} (e : Expr t) : Expr t - := fun var => inline_const (e _). End language. Global Arguments let_bind_const {_ _ _ _ t} _ {tC} _. @@ -102,6 +75,3 @@ Global Arguments under_letsf {_ _ _ _ _} _ {tC} _. Global Arguments linearizef {_ _ _ _ _} _. Global Arguments linearize {_ _ _ _ _} _. Global Arguments Linearize {_ _ _ _} _ var. -Global Arguments inline_constf {_ _ _ _ _} _. -Global Arguments inline_const {_ _ _ _ _} _. -Global Arguments InlineConst {_ _ _ _} _ var. diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v index 0b477605d..e8c58a84a 100644 --- a/src/Reflection/LinearizeInterp.v +++ b/src/Reflection/LinearizeInterp.v @@ -25,45 +25,6 @@ Section language. Local Notation wff := (@wff base_type_code interp_base_type op). Local Notation wf := (@wf base_type_code interp_base_type op). - Lemma interpf_SmartConst {t t'} v x x' - (Hin : List.In - (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) - t (x, x')) - (flatten_binding_list (t := t') base_type_code (SmartConst 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_SmartVarVar {t t'} v x x' - (Hin : List.In - (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) - t (x, x')) - (flatten_binding_list (t := t') base_type_code (SmartVarVar 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_SmartVarVar_eq {t t'} v v' x x' - (Heq : v = v') - (Hin : List.In - (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) - t (x, x')) - (flatten_binding_list (t := t') base_type_code (SmartVarVar v') v)) - : interpf interp_op x = x'. - Proof. - eapply interpf_SmartVarVar; subst; eassumption. - Qed. - Local Hint Extern 1 => eapply interpf_SmartConst. Local Hint Extern 1 => eapply interpf_SmartVarVar. @@ -88,19 +49,6 @@ Section language. | [ H : _ |- _ ] => rewrite H end. - Lemma interpf_inline_constf 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 - (x, x')) G - -> interpf interp_op x = x') - : interpf interp_op (inline_constf e1) = interpf interp_op e2. - Proof. - clear -wf H. - induction wf; t_fin. - Qed. - 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. @@ -116,13 +64,6 @@ Section language. rewrite interpf_let_bind_const; reflexivity. Qed. - Lemma interpf_SmartVar {t} v - : interpf interp_op (SmartVar (t:=t) v) = v. - Proof. - clear. - unfold SmartVar; induction t; t_fin. - Qed. - Lemma interpf_linearizef {t} e : interpf interp_op (linearizef (t:=t) e) = interpf interp_op e. Proof. @@ -133,28 +74,6 @@ Section language. | t_fin ]. Qed. - Local Hint Resolve interpf_inline_constf. - - Lemma interp_inline_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 - (x, x')) G - -> interpf interp_op x = x') - : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _) - (interp interp_op (inline_const e1)) - (interp interp_op e2). - Proof. - induction wf. - { eapply interpf_inline_constf; eauto. } - { simpl in *; intro. - match goal with - | [ H : _ |- _ ] - => apply H; intuition (inversion_sigma; inversion_prod; subst; eauto) - end. } - Qed. - Local Hint Resolve interpf_linearizef. Lemma interp_linearize {t} e @@ -166,16 +85,6 @@ Section language. eapply interpf_linearizef. Qed. - Lemma Interp_InlineConst {t} (e : Expr t) - (wf : Wf e) - : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _) - (Interp interp_op (InlineConst e)) - (Interp interp_op e). - Proof. - unfold Interp, InlineConst. - eapply interp_inline_const with (G := nil); simpl; intuition. - Qed. - Lemma Interp_Linearize {t} (e : Expr t) : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _) (Interp interp_op (Linearize e)) @@ -184,12 +93,4 @@ Section language. unfold Interp, Linearize. eapply interp_linearize. Qed. - - Lemma Interp_InlineConst_Linearize {t} (e : Expr t) (wf : Wf e) - : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _) - (Interp interp_op (InlineConst (Linearize e))) - (Interp interp_op e). - Proof. - etransitivity; [ apply Interp_InlineConst, Wf_Linearize, wf | apply Interp_Linearize ]. - Qed. End language. diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v index 9cf82b3e2..f06db6594 100644 --- a/src/Reflection/LinearizeWf.v +++ b/src/Reflection/LinearizeWf.v @@ -2,7 +2,7 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.WfProofs. Require Import Crypto.Reflection.Linearize. -Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod. +Require Import Crypto.Util.Tactics Crypto.Util.Sigma. Local Open Scope ctype_scope. Section language. @@ -63,7 +63,6 @@ Section language. let t0 := match type of wf with wff (t:=?t0) _ _ _ => t0 end in let e1 := match goal with | |- context[wff G0 (under_letsf ?e1 _) (under_letsf e2 _)] => e1 - | |- context[wff _ (inline_constf ?e1) (inline_constf e2)] => e1 end in pattern G0, t0, e1, e2; lazymatch goal with @@ -161,14 +160,6 @@ Section language. Local Hint Constructors or. Local Hint Extern 1 => progress unfold List.In in *. Local Hint Resolve wff_in_impl_Proper. - - Lemma wff_SmartVar {t} x1 x2 - : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVar x1) (SmartVar x2). - Proof. - unfold SmartVar. - induction t; simpl; constructor; eauto. - Qed. - Local Hint Resolve wff_SmartVar. Lemma wff_linearizef G {t} e1 e2 @@ -186,101 +177,6 @@ Section language. Proof. induction 1; t_fin idtac. Qed. - - Definition invert_Const {var t} (e : @exprf var t) : option (interp_type t) - := match e with - | Const _ v => Some v - | _ => None - end. - - 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. - - Local Hint Resolve (fun G A B c1 c2 wf => proj1 (@wff_Const_eta G A B c1 c2 wf)) - (fun G A B c1 c2 wf => proj2 (@wff_Const_eta G A B c1 c2 wf)). - - Lemma wff_SmartConst 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 (SmartConst v1) (SmartConst 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 SmartConst in *; simpl in *. - apply List.in_app_iff in Hin. - intuition (inversion_sigma; inversion_prod; subst; eauto). } - Qed. - - Local Hint Resolve wff_SmartConst. - - Fixpoint 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' - -> wff G x x') - (wf : wff G' e1 e2) - {struct e1} - : @wff var1 var2 G t (inline_constf e1) (inline_constf e2). - Proof. - (*revert H. - set (e1v := e1) in *. - destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ]; - [ clear wff_inline_constf - | clear wff_inline_constf - | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with - | Op _ _ _ args => wff_inline_constf _ args - | _ => I - end); - clear wff_inline_constf - | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with - | Let _ ex _ eC => wff_inline_constf _ ex - | _ => I - end); - generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with - | Let _ ex _ eC => fun x => wff_inline_constf _ (eC x) - | _ => I - end); - clear wff_inline_constf - | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with - | Pair _ ex _ ey => wff_inline_constf _ ex - | _ => I - end); - generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with - | Pair _ ex _ ey => wff_inline_constf _ ey - | _ => I - end); - clear wff_inline_constf ]; - revert G; - (* alas, Coq's refiner isn't smart enough to figure out these small inversions for us *) - small_inversion_helper wf G' e2; - t_fin idtac; - repeat match goal with - | [ H : context[(_ -> wff _ (inline_constf ?e) (inline_constf _))%type], e2 : exprf _ |- _ ] - => is_var e; not constr_eq e e2; specialize (H e2) - | [ H : context[wff _ (@inline_constf ?A ?B ?C ?D ?E ?e) _] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ] - => destruct (@inline_constf A B C D E e) - | [ H : context[wff _ _ (@inline_constf ?A ?B ?C ?D ?E ?e)] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ] - => destruct (@inline_constf A B C D E e) - | [ IHwf : forall x y : list _, _, H1 : forall z : _, _, H2 : wff _ _ _ |- _ ] - => solve [ specialize (IHwf _ _ H1 H2); inversion IHwf ] - | [ |- wff _ _ _ ] => constructor - end. - 3:t_fin idtac. - 4:t_fin idtac. - { match goal with - | [ H : _ |- _ ] => eapply H; [ | solve [ eauto ] ]; t_fin idtac - end. }*) - Abort. End with_var. Lemma Wf_Linearize {t} (e : Expr t) : Wf e -> Wf (Linearize e). diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 784beeac3..87ca9274e 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -178,6 +178,14 @@ Section language. end. End map. + Section misc. + Definition invert_Const {var t} (e : @exprf var t) : option (interp_type t) + := match e with + | Const _ v => Some v + | _ => None + end. + End misc. + Section wf. Context {var1 var2 : base_type_code -> Type}. @@ -246,6 +254,7 @@ Global Arguments Wf {_ _ _ t} _. Global Arguments Interp {_ _ _} interp_op {t} _. Global Arguments interp {_ _ _} interp_op {t} _. Global Arguments interpf {_ _ _} interp_op {t} _. +Global Arguments invert_Const {_ _ _ _ _} _. Notation "'slet' x := A 'in' b" := (Let A (fun x => b)) : expr_scope. Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index 05b3dab4b..d5b374ec4 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -2,7 +2,7 @@ Require Import Crypto.Reflection.Syntax. Require Export Crypto.Reflection.Reify. Require Import Crypto.Reflection.InputSyntax. Require Import Crypto.Reflection.CommonSubexpressionElimination. -Require Crypto.Reflection.Linearize. +Require Crypto.Reflection.Linearize Crypto.Reflection.Inline. Require Import Crypto.Reflection.WfReflective. Import ReifyDebugNotations. @@ -67,7 +67,7 @@ Goal (0 = let x := 1 in let y := 2 in x * y)%nat. Reify_rhs. Abort. -Import Linearize. +Import Linearize Inline. Goal True. let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v index 83c253c43..226172b5d 100644 --- a/src/Reflection/WfProofs.v +++ b/src/Reflection/WfProofs.v @@ -1,5 +1,5 @@ Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod. Local Open Scope ctype_scope. Section language. @@ -36,5 +36,54 @@ Section language. | _ => solve [ intuition eauto ] end. Qed. + + Local Hint Resolve List.in_app_or List.in_or_app. + Local Hint Extern 1 => progress unfold List.In in *. + Local Hint Resolve wff_in_impl_Proper. + + Lemma wff_SmartVar {t} x1 x2 + : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVar x1) (SmartVar x2). + Proof. + unfold SmartVar. + induction t; simpl; constructor; eauto. + Qed. + + Local Hint Resolve wff_SmartVar. + + 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_SmartConst 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 (SmartConst v1) (SmartConst 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 SmartConst in *; simpl in *. + apply List.in_app_iff in Hin. + intuition (inversion_sigma; inversion_prod; subst; eauto). } + Qed. + + Local Hint Resolve wff_SmartConst. End with_var. End language. diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v index d11cfe6ad..19f04fd89 100644 --- a/src/Specific/FancyMachine256/Core.v +++ b/src/Specific/FancyMachine256/Core.v @@ -8,6 +8,7 @@ Require Export Crypto.Util.Tuple. Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod. Require Export Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Inline. Require Import Crypto.Reflection.CommonSubexpressionElimination. Require Export Crypto.Reflection.Reify. Require Export Crypto.Util.ZUtil. |