From 4fd4e2aa29c7a2dcda1910a484cd5b623db08dba Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 1 Apr 2017 18:36:57 -0400 Subject: Remove trailing whitespace in NewBaseSystem --- src/NewBaseSystem.v | 52 ++++++++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'src') diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index 44f6a7fe6..d962dae99 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -120,7 +120,7 @@ Fixpoint add_lists_cps (p q : list Z) {T} (f:list Z->T) := Now let's try some partial evaluation. The expression we'll evaluate is: ``` -Definition x := +Definition x := (fun a0 a1 a2 b0 b1 b2 => let r := add_lists [a0;a1;a2] [b0;b1;b2] in let rr := add_lists r r in @@ -130,7 +130,7 @@ Definition x := Or, using `add_lists_cps`: ``` -Definition y := +Definition y := (fun a0 a1 a2 b0 b1 b2 => add_lists_cps [a0;a1;a2] [b0;b1;b2] (fun r => add_lists_cps r r @@ -153,7 +153,7 @@ the `dlet` we put into the functions should help us avoid. Let's try ``` fun a0 a1 a2 b0 b1 b2 : Z => - (fix add_lists (p q : list Z) {struct p} : + (fix add_lists (p q : list Z) {struct p} : list Z := match p with | [] => [] @@ -165,7 +165,7 @@ fun a0 a1 a2 b0 b1 b2 : Z => sum :: add_lists p' q' end end) - ((fix add_lists (p q : list Z) {struct p} : + ((fix add_lists (p q : list Z) {struct p} : list Z := match p with | [] => [] @@ -187,7 +187,7 @@ fun a0 a1 a2 b0 b1 b2 : Z => :: (dlet sum0 := a1 + b1 in sum0 :: (dlet sum1 := a2 + b2 in [sum1])))) - ((fix add_lists (p q : list Z) {struct p} : + ((fix add_lists (p q : list Z) {struct p} : list Z := match p with | [] => [] @@ -268,7 +268,7 @@ Local Ltac prove_id := end. Create HintDb push_basesystem_eval discriminated. -Local Ltac prove_eval := +Local Ltac prove_eval := repeat match goal with | _ => progress intros | _ => progress simpl @@ -276,7 +276,7 @@ Local Ltac prove_eval := | _ => progress (autorewrite with push_basesystem_eval uncps push_id cancel_pair in * ) | _ => break_if | _ => break_match - | _ => split + | _ => split | H : _ /\ _ |- _ => destruct H | H : Some _ = Some _ |- _ => progress (inversion H; subst) | _ => discriminate @@ -298,20 +298,20 @@ Delimit Scope runtime_scope with RT. Definition runtime_mul := Z.mul. Global Notation "a * b" := (runtime_mul a%RT b%RT) : runtime_scope. Definition runtime_add := Z.add. -Global Notation "a + b" := (runtime_add a%RT b%RT) : runtime_scope. +Global Notation "a + b" := (runtime_add a%RT b%RT) : runtime_scope. Definition runtime_opp := Z.opp. -Global Notation "- a" := (runtime_opp a%RT) : runtime_scope. +Global Notation "- a" := (runtime_opp a%RT) : runtime_scope. Definition runtime_and := Z.land. -Global Notation "a &' b" := (runtime_and a%RT b%RT) : runtime_scope. +Global Notation "a &' b" := (runtime_and a%RT b%RT) : runtime_scope. Definition runtime_shr := Z.shiftr. -Global Notation "a >> b" := (runtime_shr a%RT b%RT) : runtime_scope. +Global Notation "a >> b" := (runtime_shr a%RT b%RT) : runtime_scope. Module B. Definition limb := (Z*Z)%type. (* position coefficient and run-time value *) Module Associational. Definition eval (p:list limb) : Z := List.fold_right Z.add 0%Z (List.map (fun t => fst t * snd t) p). - + Lemma eval_nil : eval nil = 0. Proof. reflexivity. Qed. Lemma eval_cons p q : eval (p::q) = (fst p) * (snd p) + eval q. Proof. reflexivity. Qed. Lemma eval_app p q: eval (p++q) = eval p + eval q. @@ -387,7 +387,7 @@ Module B. Proof. cbv [reduce_cps reduce]; prove_id. Qed. Hint Opaque reduce : uncps. Hint Rewrite reduce_cps_id : uncps. - + Lemma reduction_rule a b s c m (m_eq:Z.pos m = s - c): (a + s * b) mod m = (a + c * b) mod m. Proof. @@ -405,7 +405,7 @@ Module B. Hint Rewrite eval_reduce using (omega || assumption) : push_basesystem_eval. (* Why TF does this hint get picked up outside the section (while other eval_ hints do not?) *) - + Definition negate_snd_cps (p:list limb) {T} (f:list limb ->T) := map_cps (fun cx => (fst cx, (-snd cx)%RT)) p f. @@ -485,7 +485,7 @@ Module B. map_cps weight (seq 0 n) (fun r => to_list_cps n xs (fun rr => combine_cps r rr f)). - + Definition to_associational {n} xs := @to_associational_cps n xs _ id. Lemma to_associational_cps_id {n} x {T} f: @@ -513,7 +513,7 @@ Module B. Lemma eval_zeros n : eval (zeros n) = 0. Proof. cbv [eval Associational.eval to_associational_cps zeros]. - pose proof (seq_length n 0). generalize dependent (seq 0 n). + pose proof (seq_length n 0). generalize dependent (seq 0 n). intro xs; revert n; induction xs; intros; [autorewrite with uncps; reflexivity|]. intros; destruct n; [distr_length|]. @@ -525,7 +525,7 @@ Module B. Definition add_to_nth_cps {n} i x t {T} (f:tuple Z n->T) := @on_tuple_cps _ _ 0 (update_nth_cps i (runtime_add x)) n n t _ f. - + Definition add_to_nth {n} i x t := @add_to_nth_cps n i x t _ id. Lemma add_to_nth_cps_id {n} i x xs {T} f: @add_to_nth_cps n i x xs T f = f (add_to_nth i x xs). @@ -537,7 +537,7 @@ Module B. Qed. Hint Opaque add_to_nth : uncps. Hint Rewrite @add_to_nth_cps_id : uncps. - + Lemma eval_add_to_nth {n} (i:nat) (x:Z) (H:(i fold_right Z.add d [a;b;c]).` will produce [fun a b c d => (a + (b + (c + d)))].*) Definition chained_carries_cps {n} (p:tuple Z n) (idxs : list nat) {T} (f:tuple Z n->T) := fold_right_cps2 carry_cps p (rev idxs) f. - + Definition chained_carries {n} p idxs := @chained_carries_cps n p idxs _ id. Lemma chained_carries_id {n} p idxs : forall {T} f, @chained_carries_cps n p idxs T f = f (chained_carries p idxs). @@ -719,7 +719,7 @@ Module B. End Wrappers. Hint Unfold - Positional.add_cps + Positional.add_cps Positional.mul_cps Positional.reduce_cps Positional.carry_reduce_cps @@ -761,7 +761,7 @@ Module B. Context {modulo div:Z->Z->Z} {div_mod : forall a b:Z, b <> 0 -> a = b * (div a b) + modulo a b}. - + Definition Fencode (x : F m) : tuple Z sz := encode (div:=div) (modulo:=modulo) (F.to_Z x). @@ -815,7 +815,7 @@ Module B. End Positional. Hint Unfold - Positional.add_cps + Positional.add_cps Positional.mul_cps Positional.reduce_cps Positional.carry_reduce_cps @@ -873,8 +873,8 @@ Section DivMod. End DivMod. Import B. - -Ltac basesystem_partial_evaluation_RHS := + +Ltac basesystem_partial_evaluation_RHS := let t0 := match goal with |- _ _ ?t => t end in let t := (eval cbv delta [ (* this list must contain all definitions referenced by t that reference [Let_In], [runtime_add], [runtime_opp], [runtime_mul], [runtime_shr], or [runtime_and] *) @@ -928,4 +928,4 @@ Ltac solve_op_mod_eq wt x := apply f_equal; basesystem_partial_evaluation_RHS. -Ltac solve_op_F wt x := F_mod_eq; solve_op_mod_eq wt x. \ No newline at end of file +Ltac solve_op_F wt x := F_mod_eq; solve_op_mod_eq wt x. -- cgit v1.2.3