diff options
author | Jason Gross <jgross@mit.edu> | 2019-01-24 15:35:49 -0500 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2019-01-26 18:12:06 -0500 |
commit | 9b9adfa6437439cf133da6f062b0b6050a691cdf (patch) | |
tree | 7440a07ff5cad7936fb56dc6ae4cea2fc2dc05b2 /src/PushButtonSynthesis | |
parent | ef14767f91007ebf506f45f8d669a00f0b332345 (diff) |
Also display the carry chain in a comment
Diffstat (limited to 'src/PushButtonSynthesis')
-rw-r--r-- | src/PushButtonSynthesis/Primitives.v | 7 | ||||
-rw-r--r-- | src/PushButtonSynthesis/SaturatedSolinas.v | 4 | ||||
-rw-r--r-- | src/PushButtonSynthesis/UnsaturatedSolinas.v | 6 | ||||
-rw-r--r-- | src/PushButtonSynthesis/WordByWordMontgomery.v | 4 |
4 files changed, 13 insertions, 8 deletions
diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 4afa64433..f36f4cb9c 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -369,15 +369,16 @@ Section __. (** Note: If you change the name or type signature of this function, you will need to update the code in CLI.v *) - Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + Definition Synthesize (comment_header : list string) (function_name_prefix : string) (requests : list string) + : list string (* comment header *) * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) := let ls := match requests with | nil => List.map (fun '(_, sr) => sr function_name_prefix) known_functions | requests => List.map (synthesize_of_name function_name_prefix) requests end in let infos := aggregate_infos ls in let '(extra_ls, extra_bit_widths) := extra_synthesis function_name_prefix infos in - (extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, + (comment_header, + extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, PositiveSet.union extra_bit_widths (ToString.C.bitwidths_used infos)). End for_stringification. End __. diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index bcb93c4a1..334c2a475 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -176,9 +176,9 @@ Section __. (** Note: If you change the name or type signature of this function, you will need to update the code in CLI.v *) Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) := Primitives.Synthesize machine_wordsize valid_names known_functions (fun _ => nil) - function_name_prefix requests. + [] function_name_prefix requests. End for_stringification. End __. diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index cd70771d2..8923aa10e 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -13,6 +13,7 @@ Require Import Crypto.Util.ListUtil.FoldBool. Require Import Crypto.Util.Strings.Decimal. Require Import Crypto.Util.Strings.Equality. Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.Strings.Show. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -623,9 +624,12 @@ else: (** Note: If you change the name or type signature of this function, you will need to update the code in CLI.v *) Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) := Primitives.Synthesize machine_wordsize valid_names known_functions (extra_special_synthesis function_name_prefix) + ["/* Computed values: */"; + "/* carry_chain = " ++ show false idxs ++ " */"; + ""]%string function_name_prefix requests. End for_stringification. End __. diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index 3b28329c5..a97c829e2 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -754,9 +754,9 @@ Section __. (** Note: If you change the name or type signature of this function, you will need to update the code in CLI.v *) Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) := Primitives.Synthesize machine_wordsize valid_names known_functions (fun _ => nil) - function_name_prefix requests. + [] function_name_prefix requests. End for_stringification. End __. |