From a260aa2ad6302c4dec407419664f244541d2a075 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 31 Oct 2016 16:28:10 -0400 Subject: Add [f] to things that use [exprf] or [flat_type] --- src/Reflection/CountLets.v | 2 +- src/Reflection/FilterLive.v | 2 +- src/Reflection/Inline.v | 6 +++--- src/Reflection/InlineInterp.v | 4 ++-- src/Reflection/InlineWf.v | 10 +++++----- src/Reflection/InputSyntax.v | 4 ++-- src/Reflection/InterpProofs.v | 20 ++++++++++---------- src/Reflection/Linearize.v | 4 ++-- src/Reflection/LinearizeInterp.v | 6 +++--- src/Reflection/LinearizeWf.v | 2 +- src/Reflection/Named/EstablishLiveness.v | 2 +- src/Reflection/Syntax.v | 30 +++++++++++++++--------------- src/Reflection/WfProofs.v | 22 +++++++++++----------- 13 files changed, 57 insertions(+), 57 deletions(-) (limited to 'src') diff --git a/src/Reflection/CountLets.v b/src/Reflection/CountLets.v index 927e7a168..8de6e7a2f 100644 --- a/src/Reflection/CountLets.v +++ b/src/Reflection/CountLets.v @@ -33,7 +33,7 @@ Section language. Fixpoint count_lets_genf {t} (e : exprf t) : nat := match e with | LetIn tx _ _ eC - => count_type_let tx + @count_lets_genf _ (eC (SmartVal var mkVar tx)) + => count_type_let tx + @count_lets_genf _ (eC (SmartValf var mkVar tx)) | _ => 0 end. Fixpoint count_lets_gen {t} (e : expr t) : nat diff --git a/src/Reflection/FilterLive.v b/src/Reflection/FilterLive.v index 3c1c3c8f7..446f9195c 100644 --- a/src/Reflection/FilterLive.v +++ b/src/Reflection/FilterLive.v @@ -50,7 +50,7 @@ Section language. | Some n => @filter_live_namesf (prefix ++ repeat dead_name (count_pairs tx))%list remaining' _ - (eC (SmartVal (fun _ => list Name) (fun _ => namesx ++ names_to_list n)%list _)) + (eC (SmartValf (fun _ => list Name) (fun _ => namesx ++ names_to_list n)%list _)) | None => nil end | Pair _ ex _ ey => merge_name_lists (@filter_live_namesf prefix remaining _ ex) diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v index bfb3794c9..a42df2b68 100644 --- a/src/Reflection/Inline.v +++ b/src/Reflection/Inline.v @@ -33,12 +33,12 @@ Section language. => 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 (SmartConst (op:=op) (var:=var) x) + | Const _ x => fun eC => eC (SmartConstf (op:=op) (var:=var) x) | Var _ x => fun eC => eC (Var x) - | ex => fun eC => LetIn ex (fun x => eC (SmartVarVar x)) + | ex => fun eC => LetIn ex (fun x => eC (SmartVarVarf x)) end | no_inline _ ex - => fun eC => LetIn ex (fun x => eC (SmartVarVar x)) + => fun eC => LetIn ex (fun x => eC (SmartVarVarf x)) | inline _ ex => fun eC => eC ex end (fun x => @inline_const_genf _ (eC x)) | Var _ x => x diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v index 83751e4f2..27811914c 100644 --- a/src/Reflection/InlineInterp.v +++ b/src/Reflection/InlineInterp.v @@ -25,8 +25,8 @@ Section language. 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 Hint Extern 1 => eapply interpf_SmartConstf. + Local Hint Extern 1 => eapply interpf_SmartVarVarf. Local Ltac t_fin := repeat match goal with diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v index 781643a8a..dd0fb08a3 100644 --- a/src/Reflection/InlineWf.v +++ b/src/Reflection/InlineWf.v @@ -32,8 +32,8 @@ Section language. Local Hint Constructors Syntax.wff. 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. + Local Hint Resolve wff_SmartVarf. + Local Hint Resolve wff_SmartConstf. Local Ltac t_fin := repeat first [ intro @@ -42,9 +42,9 @@ Section language. | tauto | progress subst | solve [ auto with nocore - | eapply (@wff_SmartVarVar _ _ _ _ _ _ _ (_ * _)); auto - | eapply wff_SmartConst; eauto with nocore - | eapply wff_SmartVarVar; eauto with nocore ] + | eapply (@wff_SmartVarVarf _ _ _ _ _ _ _ (_ * _)); auto + | eapply wff_SmartConstf; eauto with nocore + | eapply wff_SmartVarVarf; eauto with nocore ] | progress simpl in * | constructor | solve [ eauto ] ]. diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 7a89a22d3..dd9cab21d 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -70,7 +70,7 @@ Section language. 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 - | Var _ x => Syntax.SmartVar 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)) | Pair _ ex _ ey => Syntax.Pair (@compilef _ ex) (@compilef _ ey) @@ -98,7 +98,7 @@ Section language. | _ => reflexivity | _ => progress unfold LetIn.Let_In | _ => progress simpl in * - | _ => rewrite interpf_SmartVar + | _ => rewrite interpf_SmartVarf | _ => rewrite <- surjective_pairing | _ => progress rewrite_hyp * | [ |- context[let (x, y) := ?v in _] ] diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v index 86e8190ea..880256f1d 100644 --- a/src/Reflection/InterpProofs.v +++ b/src/Reflection/InterpProofs.v @@ -16,10 +16,10 @@ Section language. Let 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_SmartVar t v - : Syntax.interpf interp_op (SmartVar (t:=t) v) = v. + Lemma interpf_SmartVarf t v + : Syntax.interpf interp_op (SmartVarf (t:=t) v) = v. Proof. - unfold SmartVar; induction t; + unfold SmartVarf; induction t; repeat match goal with | _ => reflexivity | _ => progress simpl in * @@ -28,11 +28,11 @@ Section language. end. Qed. - Lemma interpf_SmartConst {t t'} v x x' + 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 (SmartConst v) v)) + (flatten_binding_list (t := t') base_type_code (SmartConstf v) v)) : interpf interp_op x = x'. Proof. clear -Hin. @@ -42,11 +42,11 @@ Section language. intuition (inversion_sigma; inversion_prod; subst; eauto). } Qed. - Lemma interpf_SmartVarVar {t t'} v x x' + 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) t (x, x')) - (flatten_binding_list (t := t') base_type_code (SmartVarVar v) v)) + (flatten_binding_list (t := t') base_type_code (SmartVarVarf v) v)) : interpf interp_op x = x'. Proof. clear -Hin. @@ -56,14 +56,14 @@ Section language. intuition (inversion_sigma; inversion_prod; subst; eauto). } Qed. - Lemma interpf_SmartVarVar_eq {t t'} v v' x x' + 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) t (x, x')) - (flatten_binding_list (t := t') base_type_code (SmartVarVar v') v)) + (flatten_binding_list (t := t') base_type_code (SmartVarVarf v') v)) : interpf interp_op x = x'. Proof. - subst; eapply interpf_SmartVarVar; eassumption. + subst; eapply interpf_SmartVarVarf; eassumption. Qed. End language. diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v index 8dafbdc11..810d9115b 100644 --- a/src/Reflection/Linearize.v +++ b/src/Reflection/Linearize.v @@ -53,11 +53,11 @@ Section language. | Const _ x => Const x | Var _ x => Var x | Op _ _ op args - => under_letsf (@linearizef _ args) (fun args => LetIn (Op op (SmartVar args)) SmartVar) + => under_letsf (@linearizef _ args) (fun args => LetIn (Op op (SmartVarf args)) SmartVarf) | Pair A ex B ey => under_letsf (@linearizef _ ex) (fun x => under_letsf (@linearizef _ ey) (fun y => - SmartVar (t:=Prod A B) (x, y))) + SmartVarf (t:=Prod A B) (x, y))) end. Fixpoint linearize {t} (e : expr t) : expr t diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v index 35caa016c..3ee3960d5 100644 --- a/src/Reflection/LinearizeInterp.v +++ b/src/Reflection/LinearizeInterp.v @@ -25,8 +25,8 @@ Section language. 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 Hint Extern 1 => eapply interpf_SmartConstf. + Local Hint Extern 1 => eapply interpf_SmartVarVarf. Local Ltac t_fin := repeat match goal with @@ -70,7 +70,7 @@ Section language. Proof. clear. induction e; - repeat first [ progress rewrite ?interpf_under_letsf, ?interpf_SmartVar + repeat first [ progress rewrite ?interpf_under_letsf, ?interpf_SmartVarf | progress simpl | t_fin ]. Qed. diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v index 8a7ebb7af..36c9efecb 100644 --- a/src/Reflection/LinearizeWf.v +++ b/src/Reflection/LinearizeWf.v @@ -161,7 +161,7 @@ Section language. 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_SmartVarf. Lemma wff_linearizef G {t} e1 e2 : @wff var1 var2 G t e1 e2 diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v index b9d283013..b2be2d19b 100644 --- a/src/Reflection/Named/EstablishLiveness.v +++ b/src/Reflection/Named/EstablishLiveness.v @@ -62,7 +62,7 @@ Section language. | LetIn tx n ex _ eC => let lx := @compute_livenessf ctx _ ex prefix in let lx := merge_liveness lx (prefix ++ repeat live (count_pairs tx)) in - let ctx := extend ctx n (SmartVal _ (fun _ => lx) tx) in + let ctx := extend ctx n (SmartValf _ (fun _ => lx) tx) in @compute_livenessf ctx _ eC (prefix ++ repeat dead (count_pairs tx)) | Pair _ ex _ ey => merge_liveness (@compute_livenessf ctx _ ex prefix) diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 4e650203c..30e5b6270 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -167,27 +167,27 @@ Section language. | Arrow A B => fun v => abs _ _ (fun x => @smart_interp_map f g h h' pair abs B (v (h' _ x))) end. - Fixpoint SmartVal {T} (val : forall t : base_type_code, T t) t : interp_flat_type_gen T 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 _ - | Prod A B => (@SmartVal T val A, @SmartVal T val B) + | Prod A B => (@SmartValf T val A, @SmartValf T val B) 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 SmartVar {t} : interp_flat_type_gen var t -> exprf 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. - Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) {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. - Definition SmartVarMapT {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t} + 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. - Definition SmartVarVar {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t - := SmartVarMap (fun t => Var). - Definition SmartConst {t} : interp_flat_type t -> interp_flat_type_gen exprf t - := SmartVarMap (fun t => Const (t:=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)). End expr. Definition Expr (t : type) := forall var, @expr var t. @@ -289,12 +289,12 @@ Ltac admit_Wf := apply Wf_admitted. Global Arguments Const {_ _ _ _ _} _. Global Arguments Var {_ _ _ _ _} _. -Global Arguments SmartVar {_ _ _ _ _} _. -Global Arguments SmartVal {_} T _ t. -Global Arguments SmartVarVar {_ _ _ _ _} _. -Global Arguments SmartVarMap {_ _ _} _ {_} _. -Global Arguments SmartVarMapT {_ _ _} _ _ {_} _. -Global Arguments SmartConst {_ _ _ _ _} _. +Global Arguments SmartVarf {_ _ _ _ _} _. +Global Arguments SmartValf {_} T _ t. +Global Arguments SmartVarVarf {_ _ _ _ _} _. +Global Arguments SmartVarfMap {_ _ _} _ {_} _. +Global Arguments SmartVarMap {_ _ _} _ _ {_} _. +Global Arguments SmartConstf {_ _ _ _ _} _. Global Arguments Op {_ _ _ _ _ _} _ _. Global Arguments LetIn {_ _ _ _ _} _ {_} _. Global Arguments Pair {_ _ _ _ _} _ {_} _. diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v index 1e8eed632..acc72cc76 100644 --- a/src/Reflection/WfProofs.v +++ b/src/Reflection/WfProofs.v @@ -70,14 +70,14 @@ Section language. 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). + Lemma wff_SmartVarf {t} x1 x2 + : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVarf x1) (SmartVarf x2). Proof. - unfold SmartVar. + unfold SmartVarf. induction t; simpl; constructor; eauto. Qed. - Local Hint Resolve wff_SmartVar. + 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) @@ -100,30 +100,30 @@ Section language. Local Hint Resolve wff_Const_eta_fst wff_Const_eta_snd. - Lemma wff_SmartConst G {t t'} v1 v2 x1 x2 + 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 (SmartConst v1) (SmartConst v2))) + (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 SmartConst in *; simpl in *. + { unfold SmartConstf in *; simpl in *. apply List.in_app_iff in Hin. intuition (inversion_sigma; inversion_prod; subst; eauto). } Qed. - Local Hint Resolve wff_SmartConst. + Local Hint Resolve wff_SmartConstf. - Lemma wff_SmartVarVar G {t t'} v1 v2 x1 x2 + 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)) - (flatten_binding_list base_type_code (SmartVarVar v1) (SmartVarVar v2))) + (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. Proof. revert dependent G; induction t'; intros. simpl in *. { intuition (inversion_sigma; inversion_prod; subst; simpl; eauto). constructor; eauto. } - { unfold SmartVarVar in *; simpl in *. + { unfold SmartVarVarf in *; simpl in *. apply List.in_app_iff in Hin. intuition (inversion_sigma; inversion_prod; subst; eauto). { rewrite <- !List.app_assoc; eauto. } } -- cgit v1.2.3