diff options
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 45 | ||||
| -rw-r--r-- | src/Reflection/CommonSubexpressionElimination.v | 8 | ||||
| -rw-r--r-- | src/Reflection/Inline.v | 4 | ||||
| -rw-r--r-- | src/Reflection/InlineWf.v | 18 | ||||
| -rw-r--r-- | src/Reflection/InputSyntax.v | 10 | ||||
| -rw-r--r-- | src/Reflection/Linearize.v | 10 | ||||
| -rw-r--r-- | src/Reflection/LinearizeWf.v | 12 | ||||
| -rw-r--r-- | src/Reflection/Reify.v | 4 | ||||
| -rw-r--r-- | src/Reflection/Syntax.v | 14 | ||||
| -rw-r--r-- | src/Reflection/WfReflective.v | 6 | ||||
| -rw-r--r-- | src/Reflection/WfRel.v | 4 | ||||
| -rw-r--r-- | src/Specific/FancyMachine256/Core.v | 2 | ||||
| -rw-r--r-- | src/Util/LetIn.v | 9 | ||||
| -rw-r--r-- | src/Util/Notations.v | 9 |
14 files changed, 80 insertions, 75 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index be2986ce6..ebf14a00e 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -6,6 +6,7 @@ Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.Tactics. Require Import Crypto.ModularArithmetic.Pow2Base Crypto.BaseSystemProofs. +Require Import Crypto.Util.Notations. Require Export Crypto.Util.FixCoqMistakes. Require Crypto.BaseSystem. Local Open Scope Z_scope. @@ -86,7 +87,7 @@ Section Pow2BaseProofs. reflexivity. + simpl in nth_err_w. apply nth_error_map in nth_err_w. - destruct nth_err_w as [x [A B]]. + destruct nth_err_w as [x [A B] ]. subst. replace (two_p w * (two_p a * x)) with (two_p a * (two_p w * x)) by ring. apply map_nth_error. @@ -555,7 +556,7 @@ Section Pow2BaseProofs. autorewrite with distr_length simpl_sum_firstn pull_Zpow. reflexivity. Qed. - + Lemma bounded_nil_r : forall l, (forall x, In x l -> 0 <= x) -> bounded l nil. Proof. cbv [bounded]; intros. @@ -681,7 +682,7 @@ Section BitwiseDecodeEncode. intros; induction i; simpl encode'; repeat match goal with | |- _ => progress intros - | |- _ => progress autorewrite with push_nth_default in * + | |- _ => progress autorewrite with push_nth_default in * | |- _ => progress autorewrite with Ztestbit | |- _ => progress rewrite ?firstn_O, ?Nat.sub_diag in * | |- _ => rewrite Z.testbit_pow2_mod by auto @@ -699,7 +700,7 @@ Section BitwiseDecodeEncode. progress replace a with b in * by omega | H : bounded _ _ |- bounded _ _ => apply pow2_mod_bounded_iff; rewrite pow2_mod_bounded_iff in H - | |- _ => solve [auto] + | |- _ => solve [auto] | |- _ => contradiction | |- _ => reflexivity end. @@ -961,7 +962,7 @@ Section SplitIndex. limb_widths [26,25,26] : split_index 30 = (1,4) limb_widths [26,25,26] : split_index 51 = (2,0) *) - Local Notation "u # i" := (nth_default 0 u i) (at level 30). + Local Notation "u # i" := (nth_default 0 u i). Function split_index' i index lw := match lw with @@ -1093,7 +1094,7 @@ Section SplitIndex. Lemma testbit_decode_full : forall us n, length us = length limb_widths -> bounded limb_widths us -> - Z.testbit (BaseSystem.decode base us) n = + Z.testbit (BaseSystem.decode base us) n = if Z_le_dec 0 n then (if Z_lt_dec n (bitsIn limb_widths) then Z.testbit (us # digit_index n) (bit_index n) @@ -1140,7 +1141,7 @@ Section SplitIndex. Qed. Lemma rem_bits_in_digit_pos : forall i, 0 <= i < bitsIn limb_widths -> - 0 < limb_widths # digit_index i - bit_index i. + 0 < (limb_widths # digit_index i) - bit_index i. Proof. repeat match goal with | |- _ => progress intros @@ -1152,7 +1153,7 @@ Section SplitIndex. Lemma rem_bits_in_digit_le_rem_bits : forall i, 0 <= i < bitsIn limb_widths -> - i + (limb_widths # digit_index i - bit_index i) <= bitsIn limb_widths. + i + ((limb_widths # digit_index i) - bit_index i) <= bitsIn limb_widths. Proof. intros. rewrite <-(split_index_eqn i) at 1 by lia. @@ -1167,7 +1168,7 @@ Section SplitIndex. Lemma same_digit : forall i j, 0 <= i <= j -> j < bitsIn limb_widths -> - j < i + (limb_widths # (digit_index i) - bit_index i) -> + j < i + ((limb_widths # (digit_index i)) - bit_index i) -> (digit_index i = digit_index j)%nat. Proof. intros. @@ -1241,7 +1242,7 @@ Section Conversion. Context (bits_fit : bitsIn limb_widthsA <= bitsIn limb_widthsB). Local Notation decodeA := (BaseSystem.decode (base_from_limb_widths limb_widthsA)). Local Notation decodeB := (BaseSystem.decode (base_from_limb_widths limb_widthsB)). - Local Notation "u # i" := (nth_default 0 u i) (at level 30). + Local Notation "u # i" := (nth_default 0 u i). Local Hint Resolve in_eq in_cons nth_default_limb_widths_nonneg sum_firstn_limb_widths_nonneg Nat2Z.is_nonneg. Local Opaque bounded. @@ -1254,7 +1255,7 @@ Section Conversion. let digitB := digit_index limb_widthsB (Z.of_nat i) in let indexA := bit_index limb_widthsA (Z.of_nat i) in let indexB := bit_index limb_widthsB (Z.of_nat i) in - let dist := Z.min (limb_widthsA # digitA - indexA) (limb_widthsB # digitB - indexB) in + let dist := Z.min ((limb_widthsA # digitA) - indexA) ((limb_widthsB # digitB) - indexB) in let bitsA := Z.pow2_mod ((inp # digitA) >> indexA) dist in convert' inp (i + Z.to_nat dist)%nat (update_nth digitB (update_by_concat_bits indexB bitsA) out). Proof. @@ -1267,7 +1268,7 @@ Section Conversion. | H : forall x : Z, In x ?lw -> 0 <= x |- appcontext [bit_index ?lw ?i] => unique pose proof (bit_index_not_done lw i) | H : forall x : Z, In x ?lw -> 0 <= x |- appcontext [bit_index ?lw ?i] => - unique assert (0 <= i < bitsIn lw -> i + (lw # digit_index lw i - bit_index lw i) <= bitsIn lw) by auto using rem_bits_in_digit_le_rem_bits + unique assert (0 <= i < bitsIn lw -> i + ((lw # digit_index lw i) - bit_index lw i) <= bitsIn lw) by auto using rem_bits_in_digit_le_rem_bits | |- _ => rewrite Z2Nat.id | |- _ => rewrite Nat2Z.inj_add | |- (Z.to_nat _ < Z.to_nat _)%nat => apply Z2Nat.inj_lt @@ -1291,8 +1292,8 @@ Section Conversion. let digitB := digit_index limb_widthsB (Z.of_nat i) in let indexA := bit_index limb_widthsA (Z.of_nat i) in let indexB := bit_index limb_widthsB (Z.of_nat i) in - let dist := Z.min (limb_widthsA # digitA - indexA) - (limb_widthsB # digitB - indexB) in + let dist := Z.min ((limb_widthsA # digitA) - indexA) + ((limb_widthsB # digitB) - indexB) in let bitsA := Z.pow2_mod ((inp # digitA) >> indexA) dist in 0 < dist -> bounded limb_widthsB (update_nth digitB (update_by_concat_bits indexB bitsA) out). @@ -1321,8 +1322,8 @@ Section Conversion. let digitB := digit_index limb_widthsB (Z.of_nat i) in let indexA := bit_index limb_widthsA (Z.of_nat i) in let indexB := bit_index limb_widthsB (Z.of_nat i) in - let dist := Z.min (limb_widthsA # digitA - indexA) - (limb_widthsB # digitB - indexB) in + let dist := Z.min ((limb_widthsA # digitA) - indexA) + ((limb_widthsB # digitB) - indexB) in let bitsA := Z.pow2_mod ((inp # digitA) >> indexA) dist in 0 < dist -> Z.of_nat i < bitsIn limb_widthsA -> @@ -1353,8 +1354,8 @@ Section Conversion. let digitB := digit_index limb_widthsB (Z.of_nat i) in let indexA := bit_index limb_widthsA (Z.of_nat i) in let indexB := bit_index limb_widthsB (Z.of_nat i) in - let dist := Z.min (limb_widthsA # digitA - indexA) - (limb_widthsB # digitB - indexB) in + let dist := Z.min ((limb_widthsA # digitA) - indexA) + ((limb_widthsB # digitB) - indexB) in let bitsA := Z.pow2_mod ((inp # digitA) >> indexA) dist in 0 < dist -> Z.of_nat i < bitsIn limb_widthsA -> @@ -1398,7 +1399,7 @@ Section Conversion. H : digit_index ?lw ?i = ?d |- _ => let X := fresh "H" in ((pose proof (same_digit_bit_index_sub lw i j) as X; - forward X; [ subst_let | subst_lia | lia | lia ]) || + forward X; [ subst_let | subst_lia | lia | lia ]) || (pose proof (same_digit_bit_index_sub lw j i) as X; forward X; [ subst_let | subst_lia | lia | lia ])) | |- Z.testbit _ (bit_index ?lw _ - bit_index ?lw ?i + _) = false => @@ -1406,12 +1407,12 @@ Section Conversion. rewrite (same_digit_bit_index_sub) by subst_lia; rewrite <-(split_index_eqn limb_widthsA i) at 2 by lia | |- ?lw # ?b <= ?a - ((sum_firstn ?lw ?b) + ?c) + ?c => replace (a - (sum_firstn lw b + c) + c) with (a - sum_firstn lw b) by ring; apply Z.le_add_le_sub_r - | |- ?lw # ?n + sum_firstn ?lw ?n <= _ => + | |- (?lw # ?n) + sum_firstn ?lw ?n <= _ => rewrite <-sum_firstn_succ_default; transitivity (bitsIn lw); [ | lia]; - apply sum_firstn_prefix_le; auto; lia + apply sum_firstn_prefix_le; auto; lia | |- _ => lia | |- _ => assumption - | |- _ => solve [auto] + | |- _ => solve [auto] | |- _ => rewrite <-testbit_decode by (assumption || lia || auto); assumption | |- _ => repeat (f_equal; try congruence); lia end. diff --git a/src/Reflection/CommonSubexpressionElimination.v b/src/Reflection/CommonSubexpressionElimination.v index 1f44f333d..dc1d2e670 100644 --- a/src/Reflection/CommonSubexpressionElimination.v +++ b/src/Reflection/CommonSubexpressionElimination.v @@ -107,7 +107,7 @@ Section symbolic. | Op _ _ op args => option_map (fun sargs => SOp (symbolize_op _ _ op) sargs) (@symbolize_exprf _ args) - | Let _ ex _ eC => None + | LetIn _ ex _ eC => None | Pair _ ex _ ey => match @symbolize_exprf _ ex, @symbolize_exprf _ ey with | Some sx, Some sy => Some (SPair sx sy) | _, _ => None @@ -155,13 +155,13 @@ Section symbolic. {t} (v : @exprf fsvar t) (xs : mapping) : @exprf var t := match v in @Syntax.exprf _ _ _ _ t return exprf t with - | Let tx ex _ eC => let sx := symbolize_exprf ex in + | LetIn tx ex _ eC => let sx := symbolize_exprf ex in let ex' := @csef _ ex xs in let sv := smart_lookupo tx sx xs in match sv with | Some v => @csef _ (eC v) xs | None - => Let ex' (fun x => let x' := symbolicify_smart_var xs sx x in + => LetIn ex' (fun x => let x' := symbolicify_smart_var xs sx x in @csef _ (eC x') (smart_add_mapping xs x')) end | Const _ x => Const x @@ -177,7 +177,7 @@ Section symbolic. : @exprf fsvar t := match ls with | nil => e - | x :: xs => Let (projT2 x) (fun _ => @prepend_prefix _ e xs) + | x :: xs => LetIn (projT2 x) (fun _ => @prepend_prefix _ e xs) end. Fixpoint cse {t} (v : @expr fsvar t) (xs : mapping) {struct v} : @expr var t diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v index e10b7c1ea..88454cbe7 100644 --- a/src/Reflection/Inline.v +++ b/src/Reflection/Inline.v @@ -24,11 +24,11 @@ Section language. Fixpoint inline_const_genf {t} (e : @exprf (@exprf var) t) : @exprf var t := match e in Syntax.exprf _ _ _ t return @exprf var t with - | Let _ ex tC eC + | LetIn _ ex tC eC => match postprocess _ (@inline_const_genf _ 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) | Var _ x => fun eC => eC (Var x) - | ex => fun eC => Let ex (fun x => eC (SmartVarVar x)) + | ex => fun eC => LetIn ex (fun x => eC (SmartVarVar x)) end (fun x => @inline_const_genf _ (eC x)) | Var _ x => x | Const _ x => Const x diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v index 5822066e3..025602066 100644 --- a/src/Reflection/InlineWf.v +++ b/src/Reflection/InlineWf.v @@ -84,10 +84,10 @@ Section language. end) | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 return match v1 return Prop with - | Let _ _ _ _ => retP G t v1 v2 + | LetIn _ _ _ _ => retP G t v1 v2 | _ => forall P : Prop, P -> P end with - | WfLet _ _ _ _ _ _ _ _ _ => _ + | WfLetIn _ _ _ _ _ _ _ _ _ => _ | _ => fun _ p => p end) | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 @@ -118,25 +118,25 @@ Section language. 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 + | generalize (match e1v return match e1v with LetIn _ _ _ _ => _ | _ => _ 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 + | generalize (match e1v return match e1v with LetIn _ _ _ _ => _ | _ => _ end with + | LetIn _ 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) + generalize (match e1v return match e1v with LetIn _ _ _ _ => _ | _ => _ end with + | LetIn _ 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 + | generalize (match e1v return match e1v with LetIn _ _ _ _ => _ | _ => _ end with | Pair _ ex _ ey => wff_inline_constf _ ex | _ => I end); - generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with + generalize (match e1v return match e1v with LetIn _ _ _ _ => _ | _ => _ end with | Pair _ ex _ ey => wff_inline_constf _ ey | _ => I end); diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 4a5dc810b..ad101e62f 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -31,7 +31,7 @@ Section language. | Const {t : flat_type} : interp_type t -> exprf t | Var {t} : var t -> exprf t | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR - | Let : forall {tx}, exprf tx -> forall {tC}, (var tx -> exprf tC) -> exprf tC + | LetIn : forall {tx}, exprf tx -> forall {tC}, (var tx -> exprf tC) -> exprf tC | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2) | MatchPair : forall {t1 t2}, exprf (Prod t1 t2) -> forall {tC}, (var t1 -> var t2 -> exprf tC) -> exprf tC. Inductive expr : type -> Type := @@ -50,7 +50,7 @@ Section language. | Const _ x => x | Var _ x => x | Op _ _ op args => @interp_op _ _ op (@interpf _ args) - | Let _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x) + | LetIn _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x) | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey) | MatchPair _ _ ex _ eC => match @interpf _ ex with pair x y => @interpf _ (eC x y) end end. @@ -71,9 +71,9 @@ Section language. | Const _ x => Syntax.Const x | Var _ x => Syntax.SmartVar x | Op _ _ op args => Syntax.Op op (@compilef _ args) - | Let _ ex _ eC => Syntax.Let (@compilef _ ex) (fun x => @compilef _ (eC x)) + | LetIn _ ex _ eC => Syntax.LetIn (@compilef _ ex) (fun x => @compilef _ (eC x)) | Pair _ ex _ ey => Syntax.Pair (@compilef _ ex) (@compilef _ ey) - | MatchPair _ _ ex _ eC => Syntax.Let (@compilef _ ex) (fun xy => @compilef _ (eC (fst xy) (snd xy))) + | MatchPair _ _ ex _ eC => Syntax.LetIn (@compilef _ ex) (fun xy => @compilef _ (eC (fst xy) (snd xy))) end. Fixpoint compile {t} (e : @expr (interp_flat_type_gen var) t) : @Syntax.expr base_type_code interp_base_type op var t @@ -123,7 +123,7 @@ End language. Global Arguments Const {_ _ _ _ _} _. Global Arguments Var {_ _ _ _ _} _. Global Arguments Op {_ _ _ _ _ _} _ _. -Global Arguments Let {_ _ _ _ _} _ {_} _. +Global Arguments LetIn {_ _ _ _ _} _ {_} _. Global Arguments MatchPair {_ _ _ _ _ _} _ {_} _. Global Arguments Pair {_ _ _ _ _} _ {_} _. Global Arguments Return {_ _ _ _ _} _. diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v index f60352e66..7a8830aba 100644 --- a/src/Reflection/Linearize.v +++ b/src/Reflection/Linearize.v @@ -28,17 +28,17 @@ Section language. | Prod A B => fun e _ C => @let_bind_const A (fst e) _ (fun x => @let_bind_const B (snd e) _ (fun y => C (x, y))) - | Syntax.Tbase _ => fun e _ C => Let (Const e) C + | Syntax.Tbase _ => fun e _ C => LetIn (Const e) C end e. Fixpoint under_letsf {t} (e : exprf t) : forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC := match e in Syntax.exprf _ _ _ t return forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC with - | Let _ ex _ eC + | LetIn _ ex _ eC => fun _ C => @under_letsf _ ex _ (fun v => @under_letsf _ (eC v) _ C) | Const _ x => fun _ C => let_bind_const x C | Var _ x => fun _ C => C x - | Op _ _ op args as e => fun _ C => Let e C + | Op _ _ op args as e => fun _ C => LetIn e C | Pair A x B y => fun _ C => @under_letsf A x _ (fun x => @under_letsf B y _ (fun y => C (x, y))) @@ -47,12 +47,12 @@ Section language. Fixpoint linearizef {t} (e : exprf t) : exprf t := match e in Syntax.exprf _ _ _ t return exprf t with - | Let _ ex _ eC + | LetIn _ ex _ eC => under_letsf (@linearizef _ ex) (fun x => @linearizef _ (eC x)) | Const _ x => Const x | Var _ x => Var x | Op _ _ op args - => under_letsf (@linearizef _ args) (fun args => Let (Op op (SmartVar args)) SmartVar) + => under_letsf (@linearizef _ args) (fun args => LetIn (Op op (SmartVar args)) SmartVar) | Pair A ex B ey => under_letsf (@linearizef _ ex) (fun x => under_letsf (@linearizef _ ey) (fun y => diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v index f06db6594..2c2fe67cb 100644 --- a/src/Reflection/LinearizeWf.v +++ b/src/Reflection/LinearizeWf.v @@ -93,10 +93,10 @@ Section language. end) | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 return match v1 return Prop with - | Let _ _ _ _ => retP G t v1 v2 + | LetIn _ _ _ _ => retP G t v1 v2 | _ => forall P : Prop, P -> P end with - | WfLet _ _ _ _ _ _ _ _ _ => _ + | WfLetIn _ _ _ _ _ _ _ _ _ => _ | _ => fun _ p => p end) | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2 @@ -121,12 +121,12 @@ Section language. [ clear wff_under_letsf | clear wff_under_letsf | clear wff_under_letsf - | generalize (fun G => match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with - | Let _ ex _ eC => wff_under_letsf G _ ex + | generalize (fun G => match e1v return match e1v with LetIn _ _ _ _ => _ | _ => _ end with + | LetIn _ ex _ eC => wff_under_letsf G _ ex | _ => I end); generalize (fun G => match e1v return match e1v with - | Let tx0 _ tC1 e0 => (* 8.4's type inferencer is broken, so we copy/paste the term from 8.5. This entire clause could just be [_], if Coq 8.4 worked *) + | LetIn tx0 _ tC1 e0 => (* 8.4's type inferencer is broken, so we copy/paste the term from 8.5. This entire clause could just be [_], if Coq 8.4 worked *) forall (x : @interp_flat_type_gen base_type_code var1 tx0) (e3 : exprf tC1) (tC2 : flat_type) (eC3 : @interp_flat_type_gen base_type_code var1 tC1 -> exprf tC2) (eC4 : @interp_flat_type_gen base_type_code var2 tC1 -> exprf tC2), @@ -137,7 +137,7 @@ Section language. wff G (@under_letsf base_type_code interp_base_type op var1 tC1 (e0 x) tC2 eC3) (@under_letsf base_type_code interp_base_type op var2 tC1 e3 tC2 eC4) | _ => _ end with - | Let _ ex tC' eC => fun x => wff_under_letsf G tC' (eC x) + | LetIn _ ex tC' eC => fun x => wff_under_letsf G tC' (eC x) | _ => I end); clear wff_under_letsf diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index e202cc804..19d3e9a5a 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -108,7 +108,7 @@ Ltac debug_leave_reify_rec e := Ltac reifyf base_type_code interp_base_type op var e := let reify_rec e := reifyf base_type_code interp_base_type op var e in - let mkLet ex eC := constr:(Let (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in + let mkLetIn ex eC := constr:(LetIn (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in let mkPair ex ey := constr:(Pair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex ey) in let mkVar T ex := constr:(Var (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in @@ -120,7 +120,7 @@ Ltac reifyf base_type_code interp_base_type op var e := | let x := ?ex in @?eC x => let ex := reify_rec ex in let eC := reify_rec eC in - mkLet ex eC + mkLetIn ex eC | pair ?a ?b => let a := reify_rec a in let b := reify_rec b in diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 87ca9274e..061bb5d8c 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -87,7 +87,7 @@ Section language. | Const {t : flat_type} : interp_type t -> exprf t | Var {t} : var t -> exprf t | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR - | Let : forall {tx}, exprf tx -> forall {tC}, (interp_flat_type_gen var tx -> exprf tC) -> exprf tC + | LetIn : forall {tx}, exprf tx -> forall {tC}, (interp_flat_type_gen var tx -> exprf tC) -> exprf tC | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2). Bind Scope expr_scope with exprf. Inductive expr : type -> Type := @@ -143,7 +143,7 @@ Section language. | Const _ x => x | Var _ x => x | Op _ _ op args => @interp_op _ _ op (@interpf _ args) - | Let _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x) + | LetIn _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x) | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey) end. Fixpoint interp {t} (e : @expr interp_type t) : interp_type t @@ -173,7 +173,7 @@ Section language. | Const _ x => Const x | Var _ x => Var (fvar12 _ x) | Op _ _ op args => Op op (@mapf _ args) - | Let _ ex _ eC => Let (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type_gen x))) + | LetIn _ ex _ eC => LetIn (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type_gen x))) | Pair _ ex _ ey => Pair (@mapf _ ex) (@mapf _ ey) end. End map. @@ -203,10 +203,10 @@ Section language. | WfOp : forall G {t} {tR} (e : @exprf var1 t) (e' : @exprf var2 t) op, wff G e e' -> wff G (Op (tR := tR) op e) (Op (tR := tR) op e') - | WfLet : forall G t1 t2 e1 e1' (e2 : interp_flat_type_gen var1 t1 -> @exprf var1 t2) e2', + | WfLetIn : forall G t1 t2 e1 e1' (e2 : interp_flat_type_gen var1 t1 -> @exprf var1 t2) e2', wff G e1 e1' -> (forall x1 x2, wff (flatten_binding_list x1 x2 ++ G) (e2 x1) (e2' x2)) - -> wff G (Let e1 e2) (Let e1' e2') + -> wff G (LetIn e1 e2) (LetIn e1' e2') | WfPair : forall G {t1} {t2} (e1: @exprf var1 t1) (e2: @exprf var1 t2) (e1': @exprf var2 t1) (e2': @exprf var2 t2), wff G e1 e1' @@ -239,7 +239,7 @@ Global Arguments SmartVal {_} T _ t. Global Arguments SmartVarVar {_ _ _ _ _} _. Global Arguments SmartConst {_ _ _ _ _} _. Global Arguments Op {_ _ _ _ _ _} _ _. -Global Arguments Let {_ _ _ _ _} _ {_} _. +Global Arguments LetIn {_ _ _ _ _} _ {_} _. Global Arguments Pair {_ _ _ _ _} _ {_} _. Global Arguments Return {_ _ _ _ _} _. Global Arguments Abs {_ _ _ _ _ _} _. @@ -256,6 +256,6 @@ 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 "'slet' x := A 'in' b" := (LetIn A (fun x => b)) : expr_scope. Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope. diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v index 843829b71..c5adc3630 100644 --- a/src/Reflection/WfReflective.v +++ b/src/Reflection/WfReflective.v @@ -265,7 +265,7 @@ Section language. | Const _ x => Const x | Var _ x => Var (snd x) | Op _ _ op args => Op op (@unnatize_exprf _ _ base args) - | Let _ ex _ eC => Let (@unnatize_exprf _ _ base ex) + | LetIn _ ex _ eC => LetIn (@unnatize_exprf _ _ base ex) (fun x => let v := natize_interp_flat_type_gen base x in @unnatize_exprf _ _ (fst v) (eC (snd v))) | Pair _ x _ y => Pair (@unnatize_exprf _ _ base x) (@unnatize_exprf _ _ base y) @@ -301,7 +301,7 @@ Section language. | _, _ => None end | Op _ _ _ _, _ => None - | Let tx ex tC eC, Let tx' ex' tC' eC' + | LetIn tx ex tC eC, LetIn tx' ex' tC' eC' => match @reflect_wffT G tx tx' ex ex', @flatten_binding_list2 tx tx', flat_type_eq_semidec_transparent tC tC' with | Some p, Some G0, Some _ => Some (p /\ inject (forall (x : interp_flat_type_gen var1 tx) (x' : interp_flat_type_gen var2 tx'), @@ -313,7 +313,7 @@ Section language. end)) | _, _, _ => None end - | Let _ _ _ _, _ => None + | LetIn _ _ _ _, _ => None | Pair tx ex ty ey, Pair tx' ex' ty' ey' => match @reflect_wffT G tx tx' ex ex', @reflect_wffT G ty ty' ey ey' with | Some p, Some q => Some (p /\ q) diff --git a/src/Reflection/WfRel.v b/src/Reflection/WfRel.v index 0671c7fcd..1232ab314 100644 --- a/src/Reflection/WfRel.v +++ b/src/Reflection/WfRel.v @@ -39,10 +39,10 @@ Section language. | RWfOp : forall G {t} {tR} (e : exprf1 t) (e' : exprf2 t) op, rel_wff G e e' -> rel_wff G (Op (tR := tR) op e) (Op (tR := tR) op e') - | RWfLet : forall G t1 t2 e1 e1' (e2 : interp_flat_type_gen var1 t1 -> exprf1 t2) e2', + | RWfLetIn : forall G t1 t2 e1 e1' (e2 : interp_flat_type_gen var1 t1 -> exprf1 t2) e2', rel_wff G e1 e1' -> (forall x1 x2, rel_wff (flatten_binding_list base_type_code x1 x2 ++ G) (e2 x1) (e2' x2)) - -> rel_wff G (Let e1 e2) (Let e1' e2') + -> rel_wff G (LetIn e1 e2) (LetIn e1' e2') | RWfPair : forall G {t1} {t2} (e1: exprf1 t1) (e2: exprf1 t2) (e1': exprf2 t1) (e2': exprf2 t2), rel_wff G e1 e1' diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v index 19f04fd89..2392f7ede 100644 --- a/src/Specific/FancyMachine256/Core.v +++ b/src/Specific/FancyMachine256/Core.v @@ -316,7 +316,7 @@ Section assemble. | OPaddm , cPair (cPair x y) RegMod => cAddm x y | _, _ => cINVALID op end - | Syntax.Let tx ex _ eC + | Syntax.LetIn tx ex _ eC => let ex' := @assemble_syntaxf _ ex in let eC' := fun x => @assemble_syntaxf _ (eC x) in let special := match ex' with diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v index 479d3a454..a15204c96 100644 --- a/src/Util/LetIn.v +++ b/src/Util/LetIn.v @@ -1,10 +1,9 @@ Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. -Notation "'Let' x := y 'in' f" := (Let_In y (fun x => f)) - (format "'[' 'Let' x := y 'in' ']' '/' '[' f ']'", - at level 200, f at level 200). +Notation "'Let' x := y 'in' f" := (Let_In y (fun x => f)). Global Instance Proper_Let_In_nd_changebody {A P R} {Reflexive_R:@Reflexive P R} : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)). @@ -22,7 +21,7 @@ Proof. intros. cbv [Let_In]. reflexivity. Qed. Class _call_let_in_to_Let_In {T} (e:T) := _let_in_to_Let_In_return : T. (* : forall T, gallina T -> gallina T, structurally recursive in the argument *) -Ltac let_in_to_Let_In e := +Ltac let_in_to_Let_In e := lazymatch e with | let x := ?ex in @?eC x => let ex := let_in_to_Let_In ex in @@ -44,4 +43,4 @@ Hint Extern 0 (_call_let_in_to_Let_In ?e) => ( Ltac change_let_in_with_Let_In := let g := get_goal in let g' := let_in_to_Let_In g in - change g'.
\ No newline at end of file + change g'. diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 166130824..e0215061f 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -55,12 +55,17 @@ Reserved Notation "$$ v" (at level 40). Reserved Notation "& x" (at level 30). Reserved Notation "** x" (at level 30). Reserved Notation "A <- X ; B" (at level 70, right associativity). -Reserved Notation "'plet' x := y 'in' z" (at level 60). Reserved Notation "u [ i ]" (at level 30). Reserved Notation "v [[ i ]]" (at level 30). Reserved Notation "u {{ i }}" (at level 30). +Reserved Notation "a # b" (at level 55, no associativity). (* match with theories/QArith/QArith_base.v *) +Reserved Notation "'plet' x := y 'in' z" + (at level 200, z at level 200, format "'plet' x := y 'in' '//' z"). Reserved Notation "'slet' x := A 'in' b" (at level 200, b at level 200, format "'slet' x := A 'in' '//' b"). +(* TODO(@andres-erbsen): Add a comment about why the syntax below is + different from [slet] and [plet], or make it match. *) +Reserved Notation "'Let' x := y 'in' f" + (at level 200, f at level 200, format "'[' 'Let' x := y 'in' ']' '/' '[' f ']'"). Reserved Notation "'λ' x .. y , t" (at level 200, x binder, y binder, right associativity). Reserved Notation "'λn' x .. y , t" (at level 200, right associativity). -(* FIXME: breaks Reflection.Syntax: Reserved Notation "'Let' x := y 'in' f" (at level 200, f at level 200). *)
\ No newline at end of file |