diff options
Diffstat (limited to 'src/Experiments/NewPipeline/CLI.v')
| -rw-r--r-- | src/Experiments/NewPipeline/CLI.v | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/src/Experiments/NewPipeline/CLI.v b/src/Experiments/NewPipeline/CLI.v index ebe1fcca9..abcf70f1b 100644 --- a/src/Experiments/NewPipeline/CLI.v +++ b/src/Experiments/NewPipeline/CLI.v @@ -111,6 +111,7 @@ Module ForExtraction. (s : string) (c : string) (machine_wordsize : string) + (requests : list string) : list (string * Pipeline.ErrorT (list string)) + list string := let prefix := ("fiat_" ++ curve_description ++ "_")%string in let str_n := n in @@ -119,6 +120,7 @@ Module ForExtraction. let str_c := c in let str_s := s in let machine_wordsize := parse_machine_wordsize machine_wordsize in + let show_requests := match requests with nil => "(all)" | _ => String.concat ", " requests end in match parse_s s, parse_c c with | None, None => inr ["Could not parse s (" ++ s ++ ") nor c (" ++ c ++ ")"] @@ -128,10 +130,11 @@ Module ForExtraction. => inr ["Could not parse c (" ++ c ++ ")"] | Some s, Some c => let '(res, types_used) - := UnsaturatedSolinas.Synthesize n s c machine_wordsize prefix in + := UnsaturatedSolinas.Synthesize n s c machine_wordsize prefix requests in let header := ((["/* Autogenerated */"; "/* curve description: " ++ curve_description ++ " */"; + "/* requested operations: " ++ show_requests ++ "*/"; "/* n = " ++ show false n ++ " (from """ ++ str_n ++ """) */"; "/* s = " ++ Hex.show_Z false s ++ " (from """ ++ str_s ++ """) */"; "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */"; @@ -153,8 +156,9 @@ Module ForExtraction. (s : string) (c : string) (machine_wordsize : string) + (requests : list string) : list string + list string - := match CollectErrors (PipelineLines curve_description n s c machine_wordsize) with + := match CollectErrors (PipelineLines curve_description n s c machine_wordsize requests) with | inl ls => inl (List.map (fun s => String.concat NewLine s ++ NewLine ++ NewLine) @@ -173,10 +177,11 @@ Module ForExtraction. (s : string) (c : string) (machine_wordsize : string) + (requests : list string) (success : list string -> A) (error : list string -> A) : A - := match ProcessedLines curve_description n s c machine_wordsize with + := match ProcessedLines curve_description n s c machine_wordsize requests with | inl s => success s | inr s => error s end. @@ -188,14 +193,14 @@ Module ForExtraction. (error : list string -> A) : A := match argv with - | _::curve_description::n::s::c::machine_wordsize::nil + | _::curve_description::n::s::c::machine_wordsize::requests => Pipeline - curve_description n s c machine_wordsize + curve_description n s c machine_wordsize requests success error | nil => error ["empty argv"] | prog::args - => error ["Expected arguments curve_description, n, s, c, machine_wordsize, got " ++ show false (List.length args) ++ " arguments in " ++ prog] + => error ["Expected arguments curve_description, n, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog] end. End UnsaturatedSolinas. @@ -205,12 +210,14 @@ Module ForExtraction. (s : string) (c : string) (machine_wordsize : string) + (requests : list string) : list (string * Pipeline.ErrorT (list string)) + list string := let prefix := ("fiat_" ++ curve_description ++ "_")%string in let str_machine_wordsize := machine_wordsize in let str_c := c in let str_s := s in let machine_wordsize := parse_machine_wordsize machine_wordsize in + let show_requests := match requests with nil => "(all)" | _ => String.concat ", " requests end in match parse_s s, parse_c c with | None, None => inr ["Could not parse s (" ++ s ++ ") nor c (" ++ c ++ ")"] @@ -220,10 +227,11 @@ Module ForExtraction. => inr ["Could not parse c (" ++ c ++ ")"] | Some s, Some c => let '(res, types_used) - := SaturatedSolinas.Synthesize s c machine_wordsize prefix in + := SaturatedSolinas.Synthesize s c machine_wordsize prefix requests in let header := ((["/* Autogenerated */"; "/* curve description: " ++ curve_description ++ " */"; + "/* requested operations: " ++ show_requests ++ "*/"; "/* s = " ++ Hex.show_Z false s ++ " (from """ ++ str_s ++ """) */"; "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */"; "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */"; @@ -243,8 +251,9 @@ Module ForExtraction. (s : string) (c : string) (machine_wordsize : string) + (requests : list string) : list string + list string - := match CollectErrors (PipelineLines curve_description s c machine_wordsize) with + := match CollectErrors (PipelineLines curve_description s c machine_wordsize requests) with | inl ls => inl (List.map (fun s => String.concat NewLine s ++ NewLine ++ NewLine) @@ -262,10 +271,11 @@ Module ForExtraction. (s : string) (c : string) (machine_wordsize : string) + (requests : list string) (success : list string -> A) (error : list string -> A) : A - := match ProcessedLines curve_description s c machine_wordsize with + := match ProcessedLines curve_description s c machine_wordsize requests with | inl s => success s | inr s => error s end. @@ -277,14 +287,14 @@ Module ForExtraction. (error : list string -> A) : A := match argv with - | _::curve_description::s::c::machine_wordsize::nil + | _::curve_description::s::c::machine_wordsize::requests => Pipeline - curve_description s c machine_wordsize + curve_description s c machine_wordsize requests success error | nil => error ["empty argv"] | prog::args - => error ["Expected arguments curve_description, s, c, machine_wordsize, got " ++ show false (List.length args) ++ " arguments in " ++ prog] + => error ["Expected arguments curve_description, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog] end. End SaturatedSolinas. End ForExtraction. |