From 06075fb96b9da9e669e6378b0cb4ac8321051679 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 13 Nov 2023 20:43:50 -0800
Subject: [PATCH] WIP towards
 https://github.com/mit-plv/fiat-crypto/issues/1724

---
 src/CLI.v      | 38 +++++++++++++++++++++++++++++++++++---
 src/Util/Arg.v | 23 ++++++++++++++++-------
 2 files changed, 51 insertions(+), 10 deletions(-)

diff --git a/src/CLI.v b/src/CLI.v
index 36cbd05930e..f6e118d68be 100644
--- a/src/CLI.v
+++ b/src/CLI.v
@@ -17,6 +17,7 @@ Require Import Crypto.Util.Strings.NamingConventions.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.OptionList.
 Require Import Crypto.Util.Strings.Show.
+Require Import Crypto.Util.Strings.Show.Enum.
 Require Import Crypto.Util.Strings.Sorting.
 Require Import Crypto.Util.Strings.ParseFlagOptions.
 Require Import Crypto.Util.DebugMonad.
@@ -44,6 +45,32 @@ Import
   Stringification.C.Compilers.
 
 Module ForExtraction.
+  Variant SynthesisKind : Set :=
+    | word_by_word_montgomery
+    | unsaturated_solinas
+    | saturated_solinas
+    | dettman_multiplication
+    | solinas_reduction
+    | base_conversion
+  .
+
+  Derive SynthesisKind_Listable SuchThat (@FinitelyListable SynthesisKind SynthesisKind_Listable) As SynthesisKind_FinitelyListable.
+  Proof. prove_ListableDerive. Qed.
+  Global Existing Instances SynthesisKind_Listable SynthesisKind_FinitelyListable.
+
+  Global Instance show_SynthesisKind : Show SynthesisKind.
+  Proof. prove_Show_enum (). Defined.
+  Global Instance show_lvl_SynthesisKind : ShowLevel SynthesisKind := show_SynthesisKind.
+
+  Definition parse_SynthesisKind_list : list (string * SynthesisKind)
+    := Eval vm_compute in
+      List.map
+        (fun r => (String.replace "_" "-" (show r), r))
+        (list_all SynthesisKind).
+
+  Definition parse_SynthesisKind_act : ParserAction SynthesisKind
+    := parse_strs parse_SynthesisKind_list.
+
   Definition parse_string_and {T} (parse_T : string -> option T) (s : string) : option (string * T)
     := option_map (@pair _ _ s) (parse_T s).
   Definition parse_Z (s : string) : option Z := parseZ_arith_strict s.
@@ -62,6 +89,9 @@ Module ForExtraction.
           ls <-- List.map ParseArithmetic.Q_to_Z_strict ls;
           Some ls).
 
+  Definition parse_SynthesisKind (s : string) : option SynthesisKind
+    := finalize parse_SynthesisKind_act s.
+
   Definition parse_list_REG (s : string) : option (list REG)
     := finalize (parse_comma_list parse_REG) s.
 
@@ -77,9 +107,6 @@ Module ForExtraction.
   Definition parse_callee_saved_registers (s : string) : option assembly_callee_saved_registers_opt
     := finalize parse_assembly_callee_saved_registers_opt s.
 
-  (* Workaround for lack of notation in 8.8 *)
-  Local Notation "x =? y" := (if string_dec x y then true else false) : string_scope.
-
   Definition parse_n (n : string) : option MaybeLimbCount
     := match parse_nat n with
        | Some n => Some (NumLimbs n)
@@ -301,6 +328,10 @@ Module ForExtraction.
                     end)%string
                 special_options)).
 
+  Definition synthesis_kind_spec : anon_argT
+    := ("synthesis_kind",
+         Arg.CustomSymbol parse_SynthesisKind_list,
+         ["The algorithm for field arithmetic.  Further options depend on the choice of algorithm, and can be viewed by passing -h after this argument."]).
   Definition curve_description_spec : anon_argT
     := ("curve_description",
         Arg.String,
@@ -1003,6 +1034,7 @@ Module ForExtraction.
            end.
 
       Definition PipelineMain
+                 {prog_name_count : prog_name_countT}
                  {supported_languages : supported_languagesT}
                  {A}
                  {io_driver : IODriverAPI A}
diff --git a/src/Util/Arg.v b/src/Util/Arg.v
index f61be6b2807..3e9ea65ef82 100644
--- a/src/Util/Arg.v
+++ b/src/Util/Arg.v
@@ -548,15 +548,24 @@ Definition default_named_results {ls}
      | (_, s, _) :: ss => @default_named_results' _ ss default_named_result
      end.
 
-Definition parse_argv (argv : list string) (arg_spec : arg_spec)
+Class prog_name_countT := prog_name_count : nat.
+Global Typeclasses Opaque prog_name_countT.
+Ltac fill_default_prog_name_countT _
+  := lazymatch goal with
+     | [ H : prog_name_countT |- prog_name_countT ] => exact H
+     | [ |- prog_name_countT ] => exact 1%nat
+     end.
+Global Hint Extern 1 prog_name_countT => fill_default_prog_name_countT () : typeclass_instances.
+
+Definition parse_argv {prog_name_count : prog_name_countT} (argv : list string) (arg_spec : arg_spec)
   : parse_result (arg_spec_results arg_spec)
-  := match argv with
-     | nil => Error missing_prog_name
-     | prog_name :: argv
-       => (res <- consume_args (10 + (List.length argv)) argv arg_spec (missing prog_name) (wrong prog_name) (too_many_args prog_name) (internal_error prog_name) (no_keyed_arg prog_name) (help prog_name) (out_of_fuel prog_name);
+  := if (List.length argv <? prog_name_count)%nat
+     then Error missing_prog_name
+     else let '(prog_names, argv) := (List.firstn prog_name_count argv, List.skipn prog_name_count argv) in
+          let prog_name := String.concat " " prog_names in
+          (res <- consume_args (10 + (List.length argv)) argv arg_spec (missing prog_name) (wrong prog_name) (too_many_args prog_name) (internal_error prog_name) (no_keyed_arg prog_name) (help prog_name) (out_of_fuel prog_name);
           let '(upd, anon_data, anon_opt_data, anon_opt_repeated_data) := res in
-          Success (upd default_named_results, anon_data, anon_opt_data, anon_opt_repeated_data))
-     end%error.
+          Success (upd default_named_results, anon_data, anon_opt_data, anon_opt_repeated_data))%error.
 
 Definition is_real_error (e : parse_error) : bool := match e with help _ => false | _ => true end.