diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-12 18:34:01 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-12 18:34:01 -0400 |
commit | 478b56dd5d8f4dd45e0d8a5474482176da35dcc8 (patch) | |
tree | e7ca63423d4aa6a6031a3cf3361ca0ebe177ccbd /src | |
parent | 951939fd55d7ad8178ac095189bc8399f2124640 (diff) |
Add reflective compose, notation for Z.Syntax.{Expr,Interp}
Diffstat (limited to 'src')
26 files changed, 92 insertions, 72 deletions
diff --git a/src/Compilers/ExprInversion.v b/src/Compilers/ExprInversion.v index 48ea30907..4820b5f39 100644 --- a/src/Compilers/ExprInversion.v +++ b/src/Compilers/ExprInversion.v @@ -54,6 +54,11 @@ Section language. Definition invert_Abs {T} (e : expr T) : interp_flat_type_gen var (domain T) -> exprf (codomain T) := match e with Abs _ _ f => f end. + Definition compose {A B C} (f : expr (B -> C)) (g : expr (A -> B)) + : expr (A -> C) + := Abs (fun v => LetIn (invert_Abs g v) + (invert_Abs f)). + Definition exprf_code {t} (e : exprf t) : exprf t -> Prop := match e with | TT => fun e' => TT = e' @@ -148,6 +153,10 @@ Section language. : Syntax.interpf interp_op (@invert_Abs interp_base_type T e x) = Syntax.interp interp_op e x. Proof using Type. destruct e; reflexivity. Qed. + + Definition Compose {A B C} (f : Expr (B -> C)) (g : Expr (A -> B)) + : Expr (A -> C) + := fun var => compose (f var) (g var). End language. Global Arguments invert_Var {_ _ _ _} _. @@ -156,6 +165,12 @@ Global Arguments invert_LetIn {_ _ _ _} _. Global Arguments invert_Pair {_ _ _ _ _} _. Global Arguments invert_Abs {_ _ _ _} _ _. +Module Export Notations. + Infix "∘" := Compose : expr_scope. + Infix "∘f" := compose : expr_scope. + Infix "∘ᶠ" := compose : expr_scope. +End Notations. + Ltac invert_one_expr e := preinvert_one_type e; intros ? e; diff --git a/src/Compilers/Syntax.v b/src/Compilers/Syntax.v index 0e8f924da..c86567c6d 100644 --- a/src/Compilers/Syntax.v +++ b/src/Compilers/Syntax.v @@ -148,6 +148,7 @@ Module Export Notations. Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope. Notation "( )" := TT : expr_scope. Notation "()" := TT : expr_scope. + Infix "^" := (@tuple _) : ctype_scope. Bind Scope ctype_scope with flat_type. Bind Scope ctype_scope with type. End Notations. diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index 6cb922129..5a5b95a22 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -10,7 +10,6 @@ Require Import Crypto.Util.ZUtil.Definitions. Section language. Context (convert_adc_to_sbb : bool). Local Notation exprf := (@exprf base_type op). - Local Notation Expr := (@Expr base_type op). Section with_var. Context {var : base_type -> Type}. diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v index b55f069e1..cd76a3479 100644 --- a/src/Compilers/Z/ArithmeticSimplifierInterp.v +++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v @@ -22,7 +22,6 @@ Require Import Crypto.Util.Tactics.UniquePose. Local Notation exprf := (@exprf base_type op interp_base_type). Local Notation expr := (@expr base_type op interp_base_type). -Local Notation Expr := (@Expr base_type op). Local Ltac fin_t := first [ exact I @@ -103,7 +102,7 @@ Local Arguments lift_op / . Local Opaque Z.pow. Lemma InterpSimplifyArith {convert_adc_to_sbb} {t} (e : Expr t) - : forall x, Interp interp_op (SimplifyArith convert_adc_to_sbb e) x = Interp interp_op e x. + : forall x, Interp (SimplifyArith convert_adc_to_sbb e) x = Interp e x. Proof. apply InterpRewriteOp; intros; unfold simplify_op_expr. Time break_innermost_match; diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v index 33f3c3335..ff690688a 100644 --- a/src/Compilers/Z/ArithmeticSimplifierWf.v +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -21,7 +21,6 @@ Require Import Crypto.Util.HProp. Local Notation exprf := (@exprf base_type op). Local Notation expr := (@expr base_type op). -Local Notation Expr := (@Expr base_type op). Local Notation wff := (@wff base_type op). Local Notation Wf := (@Wf base_type op). diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v index dc557f6ec..25762401d 100644 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -1,6 +1,6 @@ Require Import Coq.ZArith.ZArith. -Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Relations. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. @@ -285,10 +285,10 @@ Module Import Bounds. := let good_lgsz := List.filter (Nat.leb lgsz) allowable_lgsz in List.fold_right (fun a b => Some (option_min a b)) None good_lgsz. - Definition ComputeBounds {t} (e : Expr base_type op t) + Definition ComputeBounds {t} (e : Expr t) (input_bounds : interp_flat_type interp_base_type (domain t)) : interp_flat_type interp_base_type (codomain t) - := Interp (@interp_op) e input_bounds. + := Compilers.Syntax.Interp (@interp_op) e input_bounds. Definition is_tighter_thanb' {T} : interp_base_type T -> interp_base_type T -> bool := is_tighter_than_bool. diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v index 28e305a8f..1217cd721 100644 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v @@ -14,15 +14,15 @@ Require Import Crypto.Util.PointedProp. Lemma MapCastCorrect {round_up} - {t} (e : Expr base_type op t) + {t} (e : Expr t) (Hwf : Wf e) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e')) v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) (Hside : to_prop (InterpSideConditions e v)), - Interp (@Bounds.interp_op) e input_bounds = b - /\ Bounds.is_bounded_by b (Interp interp_op e v) - /\ cast_back_flat_const (Interp interp_op e' v') = (Interp interp_op e v). + Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds = b + /\ Bounds.is_bounded_by b (Compilers.Syntax.Interp interp_op e v) + /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v). Proof. apply MapCastCorrect; auto. { apply is_bounded_by_interp_op. } @@ -31,18 +31,18 @@ Qed. Lemma MapCastCorrect_eq {round_up} - {t} (e : Expr base_type op t) + {t} (e : Expr t) {evb ev} (Hwf : Wf e) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e')) v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) (Hside : to_prop (InterpSideConditions e v)) - (Hevb : evb = Interp (@Bounds.interp_op) e input_bounds) - (Hev : ev = Interp interp_op e v), + (Hevb : evb = Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds) + (Hev : ev = Compilers.Syntax.Interp interp_op e v), evb = b /\ Bounds.is_bounded_by b ev - /\ cast_back_flat_const (Interp interp_op e' v') = ev. + /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = ev. Proof. intros; subst; apply MapCastCorrect; auto. Qed. diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v index 7432b752b..fabb8b2b8 100644 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v @@ -10,7 +10,7 @@ Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. Definition Wf_MapCast {round_up} - {t} (e : Expr base_type op t) + {t} (e : Expr t) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) {b} e' (He' : MapCast round_up e input_bounds = Some (existT _ b e')) (Hwf : Wf e) @@ -23,7 +23,7 @@ Definition Wf_MapCast Definition Wf_MapCast_arrow {round_up} - {s d} (e : Expr base_type op (Arrow s d)) + {s d} (e : Expr (Arrow s d)) (input_bounds : interp_flat_type Bounds.interp_base_type s) {b} e' (He' : MapCast round_up e input_bounds = Some (existT _ b e')) (Hwf : Wf e) diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index c4973debf..34cb7a47a 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -33,7 +33,7 @@ Require Import Crypto.Compilers.Z.ArithmeticSimplifierInterp. (** *** Definition of the Pre-Wf Pipeline *) (** Do not change the name or the type of this definition *) -Definition PreWfPipeline {t} (e : Expr base_type op t) : Expr base_type op _ +Definition PreWfPipeline {t} (e : Expr t) : Expr _ := ExprEta (SimplifyArith false (Linearize e)). (** *** Correctness proof of the Pre-Wf Pipeline *) @@ -41,8 +41,8 @@ Definition PreWfPipeline {t} (e : Expr base_type op t) : Expr base_type op _ change it's proof, either; all of the relevant lemmas should be in the [reflective_interp] rewrite database. If they're not, you should find the file where they are defined and add them. *) -Lemma InterpPreWfPipeline {t} (e : Expr base_type op t) - : forall x, Interp interp_op (PreWfPipeline e) x = Interp interp_op e x. +Lemma InterpPreWfPipeline {t} (e : Expr t) + : forall x, Interp (PreWfPipeline e) x = Interp e x. Proof. unfold PreWfPipeline; intro. repeat autorewrite with reflective_interp. @@ -86,8 +86,8 @@ Definition default_PipelineOptions := the expression. *) Definition PostWfPreBoundsPipeline (opts : PipelineOptions) - {t} (e : Expr base_type op t) - : Expr base_type op t + {t} (e : Expr t) + : Expr t := let e := InlineConst e in let e := InlineConst (Linearize (SimplifyArith false e)) in let e := InlineConst (Linearize (SimplifyArith false e)) in @@ -117,8 +117,8 @@ Definition PostWfPreBoundsPipeline Definition PostWfBoundsPipeline round_up (opts : PipelineOptions) - {t} (e0 : Expr base_type op t) - (e : Expr base_type op t) + {t} (e0 : Expr t) + (e : Expr t) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) : option (@ProcessedReflectivePackage round_up) := Build_ProcessedReflectivePackage_from_option_sigma @@ -167,7 +167,7 @@ Section with_round_up_list. Definition PostWfPipelineCorrect opts {t} - (e : Expr base_type op t) + (e : Expr t) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) (Hwf : Wf e) (e' := PostWfPreBoundsPipeline opts e) @@ -177,8 +177,8 @@ Section with_round_up_list. (v' : interp_flat_type Syntax.interp_base_type (pick_type input_bounds)) (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) (Hside : to_prop (InterpSideConditions e' v)) - : Bounds.is_bounded_by b (Interp interp_op e v) - /\ cast_back_flat_const (Interp interp_op e'' v') = Interp interp_op e v. + : Bounds.is_bounded_by b (Interp e v) + /\ cast_back_flat_const (Interp e'' v') = Interp e v. Proof using Type. (** These first two lines probably shouldn't change much *) unfold PostWfBoundsPipeline, PostWfPreBoundsPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map, projT2_map in *; subst e'. diff --git a/src/Compilers/Z/Bounds/Pipeline/OutputType.v b/src/Compilers/Z/Bounds/Pipeline/OutputType.v index 88e38fbf6..028dd23a9 100644 --- a/src/Compilers/Z/Bounds/Pipeline/OutputType.v +++ b/src/Compilers/Z/Bounds/Pipeline/OutputType.v @@ -16,16 +16,16 @@ Section with_round_up_list. Record ProcessedReflectivePackage := { InputType : _; - input_expr : Expr base_type op InputType; + input_expr : Expr InputType; input_bounds : interp_flat_type Bounds.interp_base_type (domain InputType); output_bounds :> interp_flat_type Bounds.interp_base_type (codomain InputType); - output_expr :> Expr base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }. + output_expr :> Expr (Arrow (pick_type input_bounds) (pick_type output_bounds)) }. Definition Build_ProcessedReflectivePackage_from_option_sigma - {t} (e : Expr base_type op t) + {t} (e : Expr t) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) (result : option { output_bounds : interp_flat_type Bounds.interp_base_type (codomain t) - & Expr base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }) + & Expr (Arrow (pick_type input_bounds) (pick_type output_bounds)) }) : option ProcessedReflectivePackage := option_map (fun be @@ -35,10 +35,10 @@ Section with_round_up_list. Definition ProcessedReflectivePackage_to_sigT (x : ProcessedReflectivePackage) : { InputType : _ - & Expr base_type op InputType + & Expr InputType * { bounds : interp_flat_type Bounds.interp_base_type (domain InputType) * interp_flat_type Bounds.interp_base_type (codomain InputType) - & Expr base_type op (Arrow (pick_type (fst bounds)) (pick_type (snd bounds))) } }%type + & Expr (Arrow (pick_type (fst bounds)) (pick_type (snd bounds))) } }%type := let (a, b, c, d, e) := x in existT _ a (b, (existT _ (c, d) e)). End with_round_up_list. diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v index 9194f49db..a4b289c8e 100644 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -212,7 +212,7 @@ Section with_round_up_list. {e_pre_pkg} {e_pkg} (** ** reification *) - (rexpr_sig : { rexpr : Expr base_type op t | forall x, Interp Syntax.interp_op rexpr x = fZ x }) + (rexpr_sig : { rexpr : Expr t | forall x, Interp rexpr x = fZ x }) (** ** pre-wf pipeline *) (He : e = PreWfPipeline (proj1_sig rexpr_sig)) (** ** proving wf *) @@ -232,7 +232,7 @@ Section with_round_up_list. (Hbounds_sane : pick_type given_output_bounds = pick_type b) (Hbounds_sane_refl : e_final_newtype - = eq_rect _ (fun t => Expr base_type op (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane)) + = eq_rect _ (fun t => Expr (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane)) (** ** instantiation of original evar *) (Hevar : final_e_evar = InterpEta (t:=Arrow _ _) Syntax.interp_op e_final_newtype v') (** ** side conditions (boundedness) *) @@ -255,8 +255,8 @@ Section with_round_up_list. rewrite !@InterpPreWfPipeline in Hpost_correct. unshelve eapply relax_output_bounds; try eassumption; []. match goal with - | [ |- context[Interp _ (@eq_rect ?A ?x ?P ?k ?y ?pf) ?v] ] - => rewrite (@ap_transport A P _ x y pf (fun t e => Interp interp_op e v) k) + | [ |- context[Interp (@eq_rect ?A ?x ?P ?k ?y ?pf) ?v] ] + => rewrite (@ap_transport A P _ x y pf (fun t e => Interp e v) k) end. rewrite <- transport_pp, concat_Vp; simpl. apply Hpost_correct. diff --git a/src/Compilers/Z/CommonSubexpressionElimination.v b/src/Compilers/Z/CommonSubexpressionElimination.v index c2b4775c6..2493f6041 100644 --- a/src/Compilers/Z/CommonSubexpressionElimination.v +++ b/src/Compilers/Z/CommonSubexpressionElimination.v @@ -218,13 +218,13 @@ Definition cse inline_symbolic_expr_in_lookup {var} (prefix : list _) {t} (v : e normalize_symbolic_expr_mod_c inline_symbolic_expr_in_lookup var prefix t v xs. -Definition CSE_gen inline_symbolic_expr_in_lookup {t} (e : Expr _ _ t) (prefix : forall var, list { t : flat_type base_type & exprf _ _ t }) - : Expr _ _ t +Definition CSE_gen inline_symbolic_expr_in_lookup {t} (e : Expr t) (prefix : forall var, list { t : flat_type base_type & exprf _ _ t }) + : Expr t := @CSE base_type symbolic_op base_type_beq symbolic_op_beq internal_base_type_dec_bl op symbolize_op normalize_symbolic_expr_mod_c inline_symbolic_expr_in_lookup t e prefix. -Definition CSE inline_symbolic_expr_in_lookup {t} (e : Expr _ _ t) - : Expr _ _ t +Definition CSE inline_symbolic_expr_in_lookup {t} (e : Expr t) + : Expr t := @CSE_gen inline_symbolic_expr_in_lookup t e (fun _ => nil). diff --git a/src/Compilers/Z/CommonSubexpressionEliminationInterp.v b/src/Compilers/Z/CommonSubexpressionEliminationInterp.v index 280039058..7e7f7910a 100644 --- a/src/Compilers/Z/CommonSubexpressionEliminationInterp.v +++ b/src/Compilers/Z/CommonSubexpressionEliminationInterp.v @@ -6,16 +6,16 @@ Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.CommonSubexpressionEliminationInterp. Require Import Crypto.Compilers.Z.CommonSubexpressionElimination. -Lemma InterpCSE_gen inline_symbolic_expr_in_lookup t (e : Expr _ _ t) prefix +Lemma InterpCSE_gen inline_symbolic_expr_in_lookup t (e : Expr t) prefix (Hwf : Wf e) - : forall x, Interp interp_op (@CSE_gen inline_symbolic_expr_in_lookup t e prefix) x = Interp interp_op e x. + : forall x, Interp (@CSE_gen inline_symbolic_expr_in_lookup t e prefix) x = Interp e x. Proof. apply InterpCSE; auto using internal_base_type_dec_bl, internal_base_type_dec_lb, internal_symbolic_op_dec_bl, internal_symbolic_op_dec_lb, denote_symbolic_op. Qed. -Lemma InterpCSE inline_symbolic_expr_in_lookup t (e : Expr _ _ t) (Hwf : Wf e) - : forall x, Interp interp_op (@CSE inline_symbolic_expr_in_lookup t e) x = Interp interp_op e x. +Lemma InterpCSE inline_symbolic_expr_in_lookup t (e : Expr t) (Hwf : Wf e) + : forall x, Interp (@CSE inline_symbolic_expr_in_lookup t e) x = Interp e x. Proof. apply InterpCSE_gen; auto. Qed. diff --git a/src/Compilers/Z/CommonSubexpressionEliminationWf.v b/src/Compilers/Z/CommonSubexpressionEliminationWf.v index a7365397c..93d422b2d 100644 --- a/src/Compilers/Z/CommonSubexpressionEliminationWf.v +++ b/src/Compilers/Z/CommonSubexpressionEliminationWf.v @@ -5,7 +5,7 @@ Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.CommonSubexpressionEliminationWf. Require Import Crypto.Compilers.Z.CommonSubexpressionElimination. -Lemma Wf_CSE_gen inline_symbolic_expr_in_lookup t (e : Expr _ _ t) +Lemma Wf_CSE_gen inline_symbolic_expr_in_lookup t (e : Expr t) prefix (Hlen : forall var1 var2, length (prefix var1) = length (prefix var2)) (Hprefix : forall var1 var2 n t1 t2 e1 e2, @@ -18,7 +18,7 @@ Proof. apply Wf_CSE; auto using internal_base_type_dec_bl, internal_base_type_dec_lb, internal_symbolic_op_dec_bl, internal_symbolic_op_dec_lb. Qed. -Lemma Wf_CSE inline_symbolic_expr_in_lookup t (e : Expr _ _ t) +Lemma Wf_CSE inline_symbolic_expr_in_lookup t (e : Expr t) (Hwf : Wf e) : Wf (@CSE inline_symbolic_expr_in_lookup t e). Proof. diff --git a/src/Compilers/Z/FoldTypes.v b/src/Compilers/Z/FoldTypes.v index fc6aa9406..7b3059e43 100644 --- a/src/Compilers/Z/FoldTypes.v +++ b/src/Compilers/Z/FoldTypes.v @@ -7,11 +7,11 @@ Section min_or_max. Context (f : base_type -> base_type -> base_type) (init : base_type). - Definition TypeFold {t} (e : Expr base_type op t) : base_type + Definition TypeFold {t} (e : Expr t) : base_type := TypeFold (fun t => t) f init e. End min_or_max. -Definition MaxTypeUsed {t} (e : Expr base_type op t) : base_type +Definition MaxTypeUsed {t} (e : Expr t) : base_type := TypeFold base_type_max (TWord 0) e. -Definition MinTypeUsed {t} (e : Expr base_type op t) : base_type +Definition MinTypeUsed {t} (e : Expr t) : base_type := TypeFold base_type_min TZ e. diff --git a/src/Compilers/Z/Inline.v b/src/Compilers/Z/Inline.v index df46c0ecf..cbe6dbfde 100644 --- a/src/Compilers/Z/Inline.v +++ b/src/Compilers/Z/Inline.v @@ -3,8 +3,8 @@ Require Import Crypto.Compilers.Inline. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Syntax.Util. -Definition InlineConstAndOpp {t} (e : Expr base_type op t) : Expr base_type op t +Definition InlineConstAndOpp {t} (e : Expr t) : Expr t := @InlineConst base_type op (is_const_or_opp) t e. -Definition InlineConst {t} (e : Expr base_type op t) : Expr base_type op t +Definition InlineConst {t} (e : Expr t) : Expr t := @InlineConst base_type op (is_const) t e. diff --git a/src/Compilers/Z/InlineInterp.v b/src/Compilers/Z/InlineInterp.v index 46e5064e9..6413a68cd 100644 --- a/src/Compilers/Z/InlineInterp.v +++ b/src/Compilers/Z/InlineInterp.v @@ -4,12 +4,12 @@ Require Import Crypto.Compilers.InlineInterp. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Inline. -Definition InterpInlineConstAndOpp {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e) - : forall x, Interp interp_op (InlineConstAndOpp e) x = Interp interp_op e x +Definition InterpInlineConstAndOpp {interp_base_type interp_op} {t} (e : Expr t) (Hwf : Wf e) + : forall x, Compilers.Syntax.Interp interp_op (InlineConstAndOpp e) x = Compilers.Syntax.Interp interp_op e x := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf. -Definition InterpInlineConst {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e) - : forall x, Interp interp_op (InlineConst e) x = Interp interp_op e x +Definition InterpInlineConst {interp_base_type interp_op} {t} (e : Expr t) (Hwf : Wf e) + : forall x, Compilers.Syntax.Interp interp_op (InlineConst e) x = Compilers.Syntax.Interp interp_op e x := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf. Hint Rewrite @InterpInlineConstAndOpp @InterpInlineConst using solve_wf_side_condition : reflective_interp. diff --git a/src/Compilers/Z/InlineWf.v b/src/Compilers/Z/InlineWf.v index d6b846460..b7726987b 100644 --- a/src/Compilers/Z/InlineWf.v +++ b/src/Compilers/Z/InlineWf.v @@ -4,11 +4,11 @@ Require Import Crypto.Compilers.InlineWf. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Inline. -Definition Wf_InlineConstAndOpp {t} (e : Expr base_type op t) (Hwf : Wf e) +Definition Wf_InlineConstAndOpp {t} (e : Expr t) (Hwf : Wf e) : Wf (InlineConstAndOpp e) := @Wf_InlineConst _ _ _ t e Hwf. -Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e) +Definition Wf_InlineConst {t} (e : Expr t) (Hwf : Wf e) : Wf (InlineConst e) := @Wf_InlineConst _ _ _ t e Hwf. diff --git a/src/Compilers/Z/InterpSideConditions.v b/src/Compilers/Z/InterpSideConditions.v index 7429eaba7..bc3c8f6a9 100644 --- a/src/Compilers/Z/InterpSideConditions.v +++ b/src/Compilers/Z/InterpSideConditions.v @@ -5,5 +5,5 @@ Require Import Crypto.Compilers.InterpSideConditions. Require Import Crypto.Util.PointedProp. Require Import Crypto.Util.Notations. -Definition InterpSideConditions {t} (e : Expr base_type op t) : interp_flat_type interp_base_type (domain t) -> pointed_Prop +Definition InterpSideConditions {t} (e : Expr t) : interp_flat_type interp_base_type (domain t) -> pointed_Prop := InterpSideConditions interp_op (@interped_op_side_conditions) e. diff --git a/src/Compilers/Z/MapCastByDeBruijnInterp.v b/src/Compilers/Z/MapCastByDeBruijnInterp.v index 068c74ef2..0103342f4 100644 --- a/src/Compilers/Z/MapCastByDeBruijnInterp.v +++ b/src/Compilers/Z/MapCastByDeBruijnInterp.v @@ -41,15 +41,15 @@ Section language. := (@MapCast interp_base_type_bounds interp_op_bounds pick_typeb cast_op). Lemma MapCastCorrect - {t} (e : Expr base_type op t) + {t} (e : Expr t) (Hwf : Wf e) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')) v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v) (Hside : to_prop (InterpSideConditions e v)), - Interp interp_op_bounds e input_bounds = b - /\ @inbounds _ b (Interp interp_op e v) - /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v). + Compilers.Syntax.Interp interp_op_bounds e input_bounds = b + /\ @inbounds _ b (Compilers.Syntax.Interp interp_op e v) + /\ cast_back _ _ (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v). Proof using Type*. apply MapCastCorrect; auto using internal_base_type_dec_lb. Qed. diff --git a/src/Compilers/Z/MapCastByDeBruijnWf.v b/src/Compilers/Z/MapCastByDeBruijnWf.v index cce16e5fe..791e33886 100644 --- a/src/Compilers/Z/MapCastByDeBruijnWf.v +++ b/src/Compilers/Z/MapCastByDeBruijnWf.v @@ -36,7 +36,7 @@ Section language. := (@MapCast interp_base_type_bounds interp_op_bounds pick_typeb cast_op). Definition Wf_MapCast - {t} (e : Expr base_type op t) + {t} (e : Expr t) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) {b} e' (He' : MapCast e input_bounds = Some (existT _ b e')) (Hwf : Wf e) @@ -45,7 +45,7 @@ Section language. _ _ _ internal_base_type_dec_bl internal_base_type_dec_lb _ _ _ _ _ t e input_bounds b e' He' Hwf. Definition Wf_MapCast_arrow - {s d} (e : Expr base_type op (Arrow s d)) + {s d} (e : Expr (Arrow s d)) (input_bounds : interp_flat_type interp_base_type_bounds s) {b} e' (He' : MapCast e input_bounds = Some (existT _ b e')) (Hwf : Wf e) diff --git a/src/Compilers/Z/RewriteAddToAdc.v b/src/Compilers/Z/RewriteAddToAdc.v index 5f3fc05c5..838c92b75 100644 --- a/src/Compilers/Z/RewriteAddToAdc.v +++ b/src/Compilers/Z/RewriteAddToAdc.v @@ -24,8 +24,8 @@ Local Open Scope bool_scope. Section language. Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl). - Definition RewriteAdc {t} (e : Expr base_type op t) - : Expr base_type op t + Definition RewriteAdc {t} (e : Expr t) + : Expr t := let is_good e' := match option_map (wf_unit (Context:=PContext _) empty) e' with | Some (Some trivial) => true | _ => false @@ -49,7 +49,7 @@ Section language. then let e' := option_map interp_to_phoas e' in match e' with | Some e' - => match t return Expr _ _ (Arrow (domain t) (codomain t)) -> Expr _ _ t with + => match t return Expr (Arrow (domain t) (codomain t)) -> Expr t with | Arrow _ _ => fun x => x end e' | None => e diff --git a/src/Compilers/Z/RewriteAddToAdcInterp.v b/src/Compilers/Z/RewriteAddToAdcInterp.v index 0fdb2e46c..28953a3fb 100644 --- a/src/Compilers/Z/RewriteAddToAdcInterp.v +++ b/src/Compilers/Z/RewriteAddToAdcInterp.v @@ -20,8 +20,8 @@ Section language. Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl). Lemma InterpRewriteAdc - {t} (e : Expr base_type op t) (Hwf : Wf e) - : forall x, Interp interp_op (RewriteAdc e) x = Interp interp_op e x. + {t} (e : Expr t) (Hwf : Wf e) + : forall x, Compilers.Syntax.Interp interp_op (RewriteAdc e) x = Compilers.Syntax.Interp interp_op e x. Proof. intro x; unfold RewriteAdc, option_map; break_innermost_match; try reflexivity; match goal with |- ?x = ?y => cut (Some x = Some y); [ congruence | ] end; @@ -39,7 +39,7 @@ Section language. => let lhs := match goal with |- ?lhs = _ => lhs end in let H := fresh in destruct lhs eqn:H; [ apply (f_equal (@Some _)); eapply @Interp_rewrite_expr in H | ] - | [ H : Compile.compile (?e _) _ = Some ?e'', H' : Syntax.Named.Interp ?e'' ?x = Some ?v' |- ?v' = Interp ?interp_op' ?e ?x ] + | [ H : Compile.compile (?e _) _ = Some ?e'', H' : Syntax.Named.Interp ?e'' ?x = Some ?v' |- ?v' = Compilers.Syntax.Interp ?interp_op' ?e ?x ] => eapply @Interp_compile with (v:=x) (interp_op:=interp_op') in H end | intros; exact (@PositiveContextOk _ _ base_type_beq internal_base_type_dec_bl internal_base_type_dec_lb) diff --git a/src/Compilers/Z/RewriteAddToAdcWf.v b/src/Compilers/Z/RewriteAddToAdcWf.v index cabe61b03..984d2a3e1 100644 --- a/src/Compilers/Z/RewriteAddToAdcWf.v +++ b/src/Compilers/Z/RewriteAddToAdcWf.v @@ -13,7 +13,7 @@ Require Import Crypto.Util.Bool. Section language. Local Hint Resolve internal_base_type_dec_lb internal_base_type_dec_lb dec_rel_of_bool_dec_rel : typeclass_instances. - Lemma Wf_RewriteAdc {t} (e : Expr base_type op t) (Hwf : Wf e) + Lemma Wf_RewriteAdc {t} (e : Expr t) (Hwf : Wf e) : Wf (RewriteAdc e). Proof. unfold RewriteAdc, option_map; break_innermost_match; diff --git a/src/Compilers/Z/Syntax.v b/src/Compilers/Z/Syntax.v index 818fa1ad5..de4626adb 100644 --- a/src/Compilers/Z/Syntax.v +++ b/src/Compilers/Z/Syntax.v @@ -98,3 +98,6 @@ Definition Zinterp_op src dst (f : op src dst) Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := lift_op (Zinterp_op src dst f). + +Notation Expr := (Expr base_type op). +Notation Interp := (Interp interp_op). diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 5581dcbc4..206b25d9c 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -10,6 +10,10 @@ Require Export Crypto.Util.GlobalSettings. Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "()" (at level 0). +Reserved Infix "∘" (at level 40, left associativity). +Reserved Infix "∘ᶠ" (at level 40, left associativity). +Reserved Infix "∘f" (at level 40, left associativity). +Reserved Infix "'o'" (at level 40, left associativity). Reserved Infix "=?" (at level 70, no associativity). Reserved Infix "<?" (at level 70, no associativity). Reserved Infix "<=?" (at level 70, no associativity). |