val fstar_options_of_cmd_option (options: ref (list cmd_option)) (o: cmd_option)
    : Tot (list FStar.Getopt.opt)
let fstar_options_of_cmd_option
  (options: ref (list cmd_option))
  (o: cmd_option)
: Tot (list FStar.Getopt.opt)
= match o with
  | CmdFStarOption f -> [f]
  | CmdOption name kind desc implies ->
    begin match kind with
    | OptBool v ->
      [
        (FStar.Getopt.noshort, name, FStar.Getopt.ZeroArgs (fun _ -> set_implies options implies; v := true), desc);
        (FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := false), negate_description desc);
      ]
    | OptStringOption arg_desc valid v ->
      [
        (
          FStar.Getopt.noshort, name,
          FStar.Getopt.OneArg (
            (fun (x: string) ->
              if valid x
              then begin
                set_implies options implies;
                v := Some x
              end else
                failwith (Printf.sprintf "Bad argument to %s: got %s, expected %s" name x arg_desc)
            ),
            arg_desc
          ),
          desc
        );
        (FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := None), negate_description desc)
      ]
    | OptList arg_desc valid v ->
      [
        (
          FStar.Getopt.noshort, name,
          FStar.Getopt.OneArg (
            (fun (x: string) ->
              if valid x
              then begin
                set_implies options implies;
                v := x :: !v
              end else
                failwith (Printf.sprintf "Bad argument to %s: got %s, expected %s" name x arg_desc)
            ),
            arg_desc
          ),
          desc
        );
        (
          FStar.Getopt.noshort, negate_name name,
          FStar.Getopt.ZeroArgs (fun _ -> v := []),
          desc
        );
      ]
    end
val fstar_options_of_cmd_option (options: ref (list cmd_option)) (o: cmd_option)
    : Tot (list FStar.Getopt.opt)
let fstar_options_of_cmd_option (options: ref (list cmd_option)) (o: cmd_option)
    : Tot (list FStar.Getopt.opt) =
match o with
| CmdFStarOption f -> [f]
| CmdOption name kind desc implies ->
  match kind with
  | OptBool v ->
    [
      (FStar.Getopt.noshort,
        name,
        FStar.Getopt.ZeroArgs
        (fun _ ->
            set_implies options implies;
            v := true),
        desc);
      (FStar.Getopt.noshort,
        negate_name name,
        FStar.Getopt.ZeroArgs (fun _ -> v := false),
        negate_description desc)
    ]
  | OptStringOption arg_desc valid v ->
    [
      (FStar.Getopt.noshort,
        name,
        FStar.Getopt.OneArg
        ((fun (x: string) ->
              if valid x
              then
                (set_implies options implies;
                  v := Some x)
              else
                failwith (Printf.sprintf "Bad argument to %s: got %s, expected %s" name x arg_desc)),
          arg_desc),
        desc);
      (FStar.Getopt.noshort,
        negate_name name,
        FStar.Getopt.ZeroArgs (fun _ -> v := None),
        negate_description desc)
    ]
  | OptList arg_desc valid v ->
    [
      (FStar.Getopt.noshort,
        name,
        FStar.Getopt.OneArg
        ((fun (x: string) ->
              if valid x
              then
                (set_implies options implies;
                  v := x :: !v)
              else
                failwith (Printf.sprintf "Bad argument to %s: got %s, expected %s" name x arg_desc)),
          arg_desc),
        desc);
      (FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := []), desc)
    ]
Options.fst.checked
Version.fsti.checked prims.fst.checked OS.fsti.checked HashingOptions.fst.checked FStar.UInt8.fsti.checked FStar.String.fsti.checked FStar.ST.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.Getopt.fsti.checked FStar.Char.fsti.checked FStar.All.fst.checked
Options.fst
FStar.ST.ref Prims.list Options.cmd_option FStar.Getopt.opt Prims.Cons Prims.Nil Prims.string Options.cmd_option_kind Prims.bool FStar.Pervasives.Native.Mktuple4 FStar.Char.char FStar.Getopt.opt_variant Prims.unit FStar.Getopt.noshort FStar.Getopt.ZeroArgs FStar.ST.op_Colon_Equals FStar.Heap.trivial_preorder Options.set_implies Options.negate_name Options.negate_description FStar.Pervasives.Native.option Options.valid_string FStar.Getopt.OneArg FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.Some FStar.All.failwith FStar.Printf.sprintf FStar.Pervasives.Native.None FStar.ST.op_Bang
module Options
open HashingOptions
open FStar.All
open FStar.ST
module U8 = FStar.UInt8
module OS = OS

#push-options "--warn_error -272" //top-level effects are okay

inline_for_extraction
let valid_string
  (valid: (string -> Tot bool))
: Tot Type0
= (s: string { valid s == true })

let always_valid (_: string) : Tot bool = true

let starts_with_capital (s: string) : Tot bool =
  String.length s >= 1 &&
  begin let first = String.sub s 0 1 in
    String.compare first "A" >= 0 && String.compare first "Z" <= 0
  end

let ends_with (s:string) (suffix:string) : bool =
  let l = String.length s in
  let sl = String.length suffix in
  if sl > l || sl = 0
  then false
  else let suffix' = String.sub s (l - sl) sl in
       suffix = suffix'

let check_config_file_name (fn:string) 
  : bool
  = let fn = OS.basename fn in
    starts_with_capital fn &&
    ends_with fn ".3d.config"

let strip_suffix (fn:string) (sfx:string { ends_with fn sfx })
  : string
  = String.sub fn 0 (String.length fn - String.length sfx)
  
inline_for_extraction
let vstring = valid_string always_valid

(* NOTE: default arguments here MUST be set to false, [] or None *)

let arg0 : ref (option vstring) = alloc None
let add_include : ref (list vstring) = alloc []
let batch : ref bool = alloc false
let clang_format : ref bool = alloc false
let clang_format_executable : ref (option vstring) = alloc None
let cleanup : ref bool = alloc false
let config_file : ref (option (valid_string check_config_file_name)) = alloc None
let debug : ref bool = alloc false
let inplace_hashes : ref (list vstring) = alloc []
let input_file : ref (list string) = alloc []
let json : ref bool = alloc false
let no_copy_everparse_h : ref bool = alloc false
let output_dir : ref (option vstring) = alloc None
let save_hashes : ref bool = alloc false
let save_z3_transcript: ref (option vstring) = alloc None
let skip_c_makefiles : ref bool = alloc false
let skip_deps: ref bool = alloc false
let skip_o_rules: ref bool = alloc false

let valid_micro_step (str: string) : Tot bool = match str with
  | "verify"
  | "extract"
  | "copy_clang_format"
  | "emit_config"
    -> true
  | _ -> false

let micro_step : ref (option (valid_string valid_micro_step)) = alloc None

let produce_c_from_existing_krml : ref bool = alloc false

let valid_makefile (str: string) : Tot bool = match str with
  | "gmake"
  | "nmake"
  -> true
  | _ -> false

let makefile : ref (option (valid_string valid_makefile)) = alloc None
let makefile_name : ref (option vstring) = alloc None

let valid_equate_types (str: string) : Tot bool =
     let l = String.split [','] str in
     match l with
     | [m1;m2] -> true
     | _ -> false

let equate_types_list : ref (list (valid_string valid_equate_types)) = alloc []

let valid_check_hashes : string -> Tot bool = function
| "weak"
| "strong"
| "inplace"
  -> true
| _ -> false

let check_hashes : ref (option (valid_string valid_check_hashes)) = alloc None

let valid_input_stream_binding : string -> Tot bool = function
| "buffer"
| "extern"
| "static"
  -> true
| _ -> false

let input_stream_binding : ref (option (valid_string valid_input_stream_binding)) = alloc None

let input_stream_include : ref (option vstring) = alloc None

let emit_output_types_defs : ref bool = alloc true

let emit_smt_encoding : ref bool = alloc false

let z3_diff_test: ref (option (valid_string valid_equate_types)) = alloc None

let z3_test : ref (option vstring) = alloc None

let valid_z3_test_mode : string -> Tot bool = function
| "pos"
| "neg"
| "all"
-> true
| _ -> false

let z3_test_mode : ref (option (valid_string valid_z3_test_mode)) = alloc None

let z3_witnesses : ref (option vstring) = alloc None

let z3_executable : ref (option vstring) = alloc None

noeq
type cmd_option_kind =
  | OptBool:
      (v: ref bool) ->
      cmd_option_kind
  | OptStringOption:
      (arg_desc: string) ->
      (valid: (string -> Tot bool)) ->
      (v: ref (option (valid_string valid))) ->
      cmd_option_kind
  | OptList:
      (arg_desc: string) ->
      (valid: (string -> Tot bool)) ->
      (v: ref (list (valid_string valid))) ->
      cmd_option_kind

noeq
type cmd_option
= | CmdOption:
    (name: string) ->
    (kind: cmd_option_kind) ->
    (desc: string) ->
    (implies: list string) (* name of OptBool to set to true *) ->
    cmd_option
  | CmdFStarOption of FStar.Getopt.opt

let cmd_option_name (a: cmd_option) : Tot string =
  match a with
  | CmdFStarOption (_, name', _, _)
  | CmdOption name' _ _ _
    -> name'

let rec find_cmd_option (name: string) (l: list cmd_option): Tot (option cmd_option) = match l with
  | [] -> None
  | a :: q ->
    if name = cmd_option_name a then Some a else find_cmd_option name q

let cmd_option_description (a: cmd_option) : Tot string =
  match a with
  | CmdOption _ _ desc _
  | CmdFStarOption (_, _, _, desc) ->
    desc

let cmd_option_arg_desc (a: cmd_option) : Tot string =
  match a with
  | CmdFStarOption (_, _, arg, _) ->
    begin match arg with
    | FStar.Getopt.OneArg (_, argdesc) -> argdesc
    | _ -> ""
    end
  | CmdOption _ kind _ _ ->
    begin match kind with
    | OptStringOption argdesc _ _
    | OptList argdesc _ _
      -> argdesc
    | _ -> ""
    end

let set_implies (options: ref (list cmd_option)) (implies: list string) : ML unit =
  List.iter
    (fun name ->
      match find_cmd_option name !options with
      | Some (CmdOption _ (OptBool x) _ _) -> x := true
      | _ -> ()
    )
    implies

let string_starts_with (big small: string) : Tot bool =
  let small_len = String.length small in
  if String.length big < small_len
  then false
  else String.sub big 0 small_len = small

let negate_string_gen (s: string) (negation: string) =
  if s `string_starts_with` negation
  then String.sub s (String.length negation) (String.length s - String.length negation)
  else negation ^ s

let name_is_negated (s: string) : Tot bool = s `string_starts_with` "no_"
let negate_name (s: string) : Tot string = negate_string_gen s "no_"
let negate_description (s: string) : Tot string = negate_string_gen s "Do not"

let fstar_options_of_cmd_option
  (options: ref (list cmd_option))
  (o: cmd_option)
val fstar_options_of_cmd_option (options: ref (list cmd_option)) (o: cmd_option)
    : Tot (list FStar.Getopt.opt)
options: FStar.ST.ref (Prims.list Options.cmd_option) -> o: Options.cmd_option
  -> Prims.list FStar.Getopt.opt