diff options
author | Jason Gross <jgross@mit.edu> | 2019-02-01 16:14:30 -0500 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2019-02-02 18:22:15 -0500 |
commit | d2b8d2b69b239ffd343d87078addab0c82ad1c43 (patch) | |
tree | 16793af5e92f3d0bcae0a4c5413b01cd2106d731 /src/PushButtonSynthesis/Primitives.v | |
parent | af2d2226b1fa739ed9ba9a279fe771109c7a9751 (diff) |
Rename docstring generator based on Andres' suggestion
Diffstat (limited to 'src/PushButtonSynthesis/Primitives.v')
-rw-r--r-- | src/PushButtonSynthesis/Primitives.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 392a63c78..96c57f132 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -565,21 +565,21 @@ Module CorrectnessStringification. let res := strip_lambdas res in res. - Notation stringify_correctness_with_ctx ctx evalf pre_extra correctness + Notation docstring_with_summary_from_lemma_with_ctx ctx evalf pre_extra 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 stringify_correctness evalf pre_extra correctness + Notation docstring_with_summary_from_lemma evalf pre_extra correctness := (match dyn_context.nil with - | ctx' => stringify_correctness_with_ctx ctx' evalf pre_extra correctness + | ctx' => docstring_with_summary_from_lemma_with_ctx ctx' evalf pre_extra correctness end) (only parsing). End CorrectnessStringification. -Notation "'stringify_correctness_with_ctx!' ctx evalf pre_extra correctness" - := (CorrectnessStringification.stringify_correctness_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 "'stringify_correctness!' evalf pre_extra correctness" - := (CorrectnessStringification.stringify_correctness 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 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). Section __. Context (n : nat) @@ -622,7 +622,7 @@ Section __. := Eval cbv beta in FromPipelineToString prefix "selectznz" selectznz - (stringify_correctness! + (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)). @@ -642,7 +642,7 @@ Section __. := Eval cbv beta in FromPipelineToString prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s) - (stringify_correctness! + (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)). @@ -663,7 +663,7 @@ Section __. := Eval cbv beta in FromPipelineToString prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s) - (stringify_correctness! + (docstring_with_summary_from_lemma! evalf (fun fname : string => ["The function " ++ fname ++ " is an addition with carry."]%string) (addcarryx_correct s)). @@ -683,7 +683,7 @@ Section __. := Eval cbv beta in FromPipelineToString prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s) - (stringify_correctness! + (docstring_with_summary_from_lemma! evalf (fun fname : string => ["The function " ++ fname ++ " is a subtraction with borrow."]%string) (subborrowx_correct s)). @@ -704,7 +704,7 @@ Section __. := Eval cbv beta in FromPipelineToString prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s) - (stringify_correctness! + (docstring_with_summary_from_lemma! evalf (fun fname : string => ["The function " ++ fname ++ " is a single-word conditional move."]%string) (cmovznz_correct s)). |