From 069e5cce23669707f11e59d9f68a31ad24990fe0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Feb 2019 16:28:41 -0500 Subject: More minor improvements in docstrings --- src/PushButtonSynthesis/Primitives.v | 58 +++++++++++++------------- src/PushButtonSynthesis/SaturatedSolinas.v | 16 ++++--- src/PushButtonSynthesis/UnsaturatedSolinas.v | 18 +++++--- src/PushButtonSynthesis/WordByWordMontgomery.v | 32 +++++++------- 4 files changed, 66 insertions(+), 58 deletions(-) diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 96c57f132..67b743ad3 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -351,10 +351,9 @@ Module CorrectnessStringification. | _ => false end. - Ltac stringify_rec0 evalf ctx correctness lvl := - let recurse v lvl := stringify_rec0 evalf ctx v lvl in + Ltac stringify_rec0 ctx correctness lvl := + let recurse v lvl := stringify_rec0 ctx v lvl in let name_of_var := find_head_in_ctx ctx correctness in - let weightf := lazymatch evalf with eval ?weightf _ => weightf | _ => I end in let stringify_if testv t f := let stest := recurse testv 200 in let st := recurse t 200 in @@ -424,12 +423,6 @@ Module CorrectnessStringification. | ?T' => let __ := match goal with _ => idtac "Error: Unrecognized type for equality:" T' end in constr:(I : I) end - | evalf ?v - => let sv := recurse v 9 in - maybe_parenthesize (("eval " ++ sv)%string) 10 lvl - | weightf ?v - => let sv := recurse v 9 in - maybe_parenthesize (("weight " ++ sv)%string) 10 lvl | eval (weight 8 1) _ ?v => let sv := recurse v 9 in maybe_parenthesize (("bytes_eval " ++ sv)%string) 10 lvl @@ -494,7 +487,7 @@ Module CorrectnessStringification. => recurse (n - 1)%nat lvl end | fun x : ?T => ?f - => let slam := stringify_function_binders ctx correctness ltac:(fun ctx body => stringify_rec0 evalf ctx body 200) in + => let slam := stringify_function_binders ctx correctness ltac:(fun ctx body => stringify_rec0 ctx body 200) in maybe_parenthesize ("λ" ++ slam) 200 lvl | ?v => let iv := test_is_var v in @@ -515,14 +508,14 @@ Module CorrectnessStringification. end end. - Ltac stringify_rec prefix evalf ctx correctness lvl := - let recurse' prefix v lvl := stringify_rec prefix evalf ctx v lvl in + Ltac stringify_rec prefix ctx correctness lvl := + let recurse' prefix v lvl := stringify_rec prefix ctx v lvl in let recurse := recurse' "" in - let default _ := let v := stringify_rec0 evalf ctx correctness lvl in + let default _ := let v := stringify_rec0 ctx correctness lvl in constr:((prefix ++ v)::nil) in lazymatch correctness with | ?A -> ?B - => let sA := stringify_rec0 evalf ctx A 98 in + => let sA := stringify_rec0 ctx A 98 in let sB := recurse B 200 in constr:((prefix ++ sA ++ " →")%string :: sB) | _ <= _ < _ => default () @@ -546,7 +539,7 @@ Module CorrectnessStringification. | ?v => v end. - Ltac stringify ctx correctness evalf fname arg_var_data out_var_data := + Ltac stringify ctx correctness fname arg_var_data out_var_data := let G := match goal with |- ?G => G end in let correctness := (eval hnf in correctness) in let correctness := (eval cbv [Partition.partition Arithmetic.WordByWordMontgomery.valid Arithmetic.WordByWordMontgomery.small] in correctness) in @@ -560,26 +553,26 @@ Module CorrectnessStringification. out_var_names ltac:( fun ctx T - => let v := stringify_rec "" evalf ctx T 200 in refine v + => let v := stringify_rec "" ctx T 200 in refine v ) in let res := strip_lambdas res in res. - Notation docstring_with_summary_from_lemma_with_ctx ctx evalf pre_extra correctness + Notation docstring_with_summary_from_lemma_with_ctx ctx summary correctness := (fun fname arg_var_data out_var_data - => ltac:(let res := stringify ctx correctness evalf fname arg_var_data out_var_data in - refine (List.app (pre_extra fname) res))) (only parsing). - Notation docstring_with_summary_from_lemma evalf pre_extra correctness + => ltac:(let res := stringify ctx correctness fname arg_var_data out_var_data in + refine (List.app (summary fname) res))) (only parsing). + Notation docstring_with_summary_from_lemma summary correctness := (match dyn_context.nil with - | ctx' => docstring_with_summary_from_lemma_with_ctx ctx' evalf pre_extra correctness + | ctx' => docstring_with_summary_from_lemma_with_ctx ctx' summary correctness end) (only parsing). End CorrectnessStringification. -Notation "'docstring_with_summary_from_lemma_with_ctx!' ctx evalf pre_extra correctness" - := (CorrectnessStringification.docstring_with_summary_from_lemma_with_ctx ctx evalf pre_extra correctness) (only parsing, at level 10, ctx at next level, evalf at next level, pre_extra at next level, correctness at next level). -Notation "'docstring_with_summary_from_lemma!' evalf pre_extra correctness" - := (CorrectnessStringification.docstring_with_summary_from_lemma evalf pre_extra correctness) (only parsing, at level 10, evalf at next level, pre_extra at next level, correctness at next level). +Notation "'docstring_with_summary_from_lemma_with_ctx!' ctx summary correctness" + := (CorrectnessStringification.docstring_with_summary_from_lemma_with_ctx ctx summary correctness) (only parsing, at level 10, ctx at next level, summary at next level, correctness at next level). +Notation "'docstring_with_summary_from_lemma!' summary correctness" + := (CorrectnessStringification.docstring_with_summary_from_lemma summary correctness) (only parsing, at level 10, summary at next level, correctness at next level). Section __. Context (n : nat) @@ -607,6 +600,16 @@ Section __. Local Notation dummy_weight := (weight 0 0). Local Notation evalf := (eval dummy_weight n). + Local Notation notations_for_docstring + := (CorrectnessStringification.dyn_context.cons + evalf "eval" + CorrectnessStringification.dyn_context.nil)%string. + Local Notation "'docstring_with_summary_from_lemma!' summary correctness" + := (docstring_with_summary_from_lemma_with_ctx! + notations_for_docstring + summary + correctness) + (only parsing, at level 10, summary at next level, correctness at next level). Definition selectznz := Pipeline.BoundsPipeline @@ -623,7 +626,6 @@ Section __. FromPipelineToString prefix "selectznz" selectznz (docstring_with_summary_from_lemma! - evalf (fun fname : string => ["The function " ++ fname ++ " is a multi-limb conditional select."]%string) (selectznz_correct dummy_weight n saturated_bounds_list)). @@ -643,7 +645,6 @@ Section __. FromPipelineToString prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s) (docstring_with_summary_from_lemma! - evalf (fun fname : string => ["The function " ++ fname ++ " is a multiplication, returning the full double-width result."]%string) (mulx_correct s)). @@ -664,7 +665,6 @@ Section __. FromPipelineToString prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s) (docstring_with_summary_from_lemma! - evalf (fun fname : string => ["The function " ++ fname ++ " is an addition with carry."]%string) (addcarryx_correct s)). @@ -684,7 +684,6 @@ Section __. FromPipelineToString prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s) (docstring_with_summary_from_lemma! - evalf (fun fname : string => ["The function " ++ fname ++ " is a subtraction with borrow."]%string) (subborrowx_correct s)). @@ -705,7 +704,6 @@ Section __. FromPipelineToString prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s) (docstring_with_summary_from_lemma! - evalf (fun fname : string => ["The function " ++ fname ++ " is a single-word conditional move."]%string) (cmovznz_correct s)). diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 47431eb09..0e7aaf6b2 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -137,14 +137,18 @@ Section __. Local Notation weightf := (weight machine_wordsize 1). Local Notation evalf := (eval weightf n). - Local Notation initial_ctx := (CorrectnessStringification.dyn_context.nil). - Local Notation "'docstring_with_summary_from_lemma!' pre_extra correctness" + Local Notation notations_for_docstring + := (CorrectnessStringification.dyn_context.cons + weightf "weight" + (CorrectnessStringification.dyn_context.cons + evalf "eval" + CorrectnessStringification.dyn_context.nil))%string. + Local Notation "'docstring_with_summary_from_lemma!' summary correctness" := (docstring_with_summary_from_lemma_with_ctx! - initial_ctx - evalf - pre_extra + notations_for_docstring + summary correctness) - (only parsing, at level 10, pre_extra at next level, correctness at next level). + (only parsing, at level 10, summary at next level, correctness at next level). Definition mul := Pipeline.BoundsPipeline diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index b25d648ea..0ac4c6cf4 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -260,14 +260,20 @@ else: Local Notation weightf := (weight (Qnum limbwidth) (QDen limbwidth)). Local Notation evalf := (eval weightf n). - Local Notation initial_ctx := (CorrectnessStringification.dyn_context.cons m "m"%string CorrectnessStringification.dyn_context.nil). - Local Notation "'docstring_with_summary_from_lemma!' pre_extra correctness" + Local Notation notations_for_docstring + := (CorrectnessStringification.dyn_context.cons + m "m" + (CorrectnessStringification.dyn_context.cons + weightf "weight" + (CorrectnessStringification.dyn_context.cons + evalf "eval" + CorrectnessStringification.dyn_context.nil)))%string. + Local Notation "'docstring_with_summary_from_lemma!' summary correctness" := (docstring_with_summary_from_lemma_with_ctx! - initial_ctx - evalf - pre_extra + notations_for_docstring + summary correctness) - (only parsing, at level 10, pre_extra at next level, correctness at next level). + (only parsing, at level 10, summary at next level, correctness at next level). Definition carry_mul := Pipeline.BoundsPipeline diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index 864c5c2eb..c92e0615a 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -228,25 +228,25 @@ Section __. Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). - Local Notation evalf := (@eval machine_wordsize n). - Local Notation initial_ctx prefix - := (CorrectnessStringification.dyn_context.cons - m "m"%string - (CorrectnessStringification.dyn_context.cons - r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string - (CorrectnessStringification.dyn_context.cons - from_montgomery_res "from_montgomery"%string - (CorrectnessStringification.dyn_context.cons - (@eval 8 n_bytes) "bytes_eval"%string - CorrectnessStringification.dyn_context.nil)))) + Local Notation notations_for_docstring prefix + := ((CorrectnessStringification.dyn_context.cons + m "m" + (CorrectnessStringification.dyn_context.cons + r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)") + (CorrectnessStringification.dyn_context.cons + from_montgomery_res "from_montgomery" + (CorrectnessStringification.dyn_context.cons + (@eval machine_wordsize n) "eval" + (CorrectnessStringification.dyn_context.cons + (@eval 8 n_bytes) "bytes_eval" + CorrectnessStringification.dyn_context.nil)))))%string) (only parsing). - Local Notation "'docstring_with_summary_from_lemma!' prefix pre_extra correctness" + Local Notation "'docstring_with_summary_from_lemma!' prefix summary correctness" := (docstring_with_summary_from_lemma_with_ctx! - (initial_ctx prefix) - evalf - pre_extra + (notations_for_docstring prefix) + summary correctness) - (only parsing, at level 10, prefix at next level, pre_extra at next level, correctness at next level). + (only parsing, at level 10, prefix at next level, summary at next level, correctness at next level). Definition mul := Pipeline.BoundsPipeline -- cgit v1.2.3