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/CLI.v | |
| parent | ef14767f91007ebf506f45f8d669a00f0b332345 (diff) | |
Also display the carry chain in a comment
Diffstat (limited to 'src/CLI.v')
| -rw-r--r-- | src/CLI.v | 17 |
1 files changed, 10 insertions, 7 deletions
@@ -222,7 +222,7 @@ Module ForExtraction. ; ("c", c, parse_c c:Dyn)] with | inr errs => inr errs | inl (n, machine_wordsize, s, c) - => let '(res, types_used) + => let '(extra_comment_header, res, types_used) := UnsaturatedSolinas.Synthesize n s c machine_wordsize prefix requests in let header := ((["/* Autogenerated */"; @@ -233,8 +233,9 @@ Module ForExtraction. "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */"; "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */"; ""]%string) - ++ ToString.C.String.typedef_header prefix types_used - ++ [""])%list in + ++ extra_comment_header + ++ ToString.C.String.typedef_header prefix types_used + ++ [""])%list in inl ([("check_args" ++ NewLine ++ String.concat NewLine header, UnsaturatedSolinas.check_args @@ -323,7 +324,7 @@ Module ForExtraction. ("m", m, parse_m m:Dyn)] with | inr errs => inr errs | inl (machine_wordsize, m) - => let '(res, types_used) + => let '(extra_comment_header, res, types_used) := WordByWordMontgomery.Synthesize m machine_wordsize prefix requests in let header := ((["/* Autogenerated */"; @@ -339,8 +340,9 @@ Module ForExtraction. "/* All functions also ensure that these two properties are true of */"; "/* return values. */"; ""]%string) - ++ ToString.C.String.typedef_header prefix types_used - ++ [""])%list in + ++ extra_comment_header + ++ ToString.C.String.typedef_header prefix types_used + ++ [""])%list in inl ([("check_args" ++ NewLine ++ String.concat NewLine header, WordByWordMontgomery.check_args @@ -424,7 +426,7 @@ Module ForExtraction. ; ("c", c, parse_c c:Dyn)] with | inr errs => inr errs | inl (machine_wordsize, s, c) - => let '(res, types_used) + => let '(extra_comment_header, res, types_used) := SaturatedSolinas.Synthesize s c machine_wordsize prefix requests in let header := ((["/* Autogenerated */"; @@ -434,6 +436,7 @@ Module ForExtraction. "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */"; "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */"; ""]%string) + ++ extra_comment_header ++ ToString.C.String.typedef_header prefix types_used ++ [""])%list in inl |