val display_usage_1 (options: ref (list cmd_option)) : ML unit
let display_usage_1 (options: ref (list cmd_option)) : ML unit =
  FStar.IO.print_string "EverParse/3d: verified data validation with dependent data descriptions\n";
  FStar.IO.print_string "\n";
  FStar.IO.print_string (Printf.sprintf "Usage: %s [options] path_to_input_file1.3d path_to_input_file2.3d ... \n" (get_arg0 ()));
  FStar.IO.print_string "\n";
  FStar.IO.print_string "Options:\n";
  List.iter
    (fun x ->
      let m = cmd_option_name x in
      let desc = cmd_option_description x in
      let argdesc = cmd_option_arg_desc x in
      let argdesc = if argdesc = "" then "" else Printf.sprintf " <%s>" argdesc in
      let negate = if CmdOption? x then Printf.sprintf " (opposite is --%s)" (negate_name m) else "" in
      let visible = not (m `string_starts_with` "__") in
      if visible then FStar.IO.print_string (Printf.sprintf "--%s%s%s\n\t%s\n" m argdesc negate desc)
    )
    !options
    ;
  FStar.IO.print_string (Printf.sprintf "\nCurrent options are:%s\n" (compute_current_options options []))
val display_usage_1 (options: ref (list cmd_option)) : ML unit
let display_usage_1 (options: ref (list cmd_option)) : ML unit =
FStar.IO.print_string "EverParse/3d: verified data validation with dependent data descriptions\n";
FStar.IO.print_string "\n";
FStar.IO.print_string (Printf.sprintf "Usage: %s [options] path_to_input_file1.3d path_to_input_file2.3d ... \n"
      (get_arg0 ()));
FStar.IO.print_string "\n";
FStar.IO.print_string "Options:\n";
List.iter (fun x ->
      let m = cmd_option_name x in
      let desc = cmd_option_description x in
      let argdesc = cmd_option_arg_desc x in
      let argdesc = if argdesc = "" then "" else Printf.sprintf " <%s>" argdesc in
      let negate =
        if CmdOption? x then Printf.sprintf " (opposite is --%s)" (negate_name m) else ""
      in
      let visible = not (m `string_starts_with` "__") in
      if visible
      then FStar.IO.print_string (Printf.sprintf "--%s%s%s\n\t%s\n" m argdesc negate desc))
  !options;
FStar.IO.print_string (Printf.sprintf "\nCurrent options are:%s\n"
      (compute_current_options options []))
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.IO.print_string Prims.unit Prims.string FStar.Printf.sprintf Options.compute_current_options Prims.Nil FStar.List.iter Prims.bool Prims.op_Negation Options.string_starts_with Options.uu___is_CmdOption Options.negate_name Prims.op_Equality Options.cmd_option_arg_desc Options.cmd_option_description Options.cmd_option_name FStar.ST.op_Bang FStar.Heap.trivial_preorder Options.get_arg0
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)
: 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

let compute_current_options (options: ref (list cmd_option)) (ignore: list string) : ML string =
  (* we would like to output a normalized sequence of options so that its semantics does not depend on whether any other options are prepended (i.e. whether 3d is run from 3d or from everparse.cmd or from everparse.sh *)
  (* first print the values of current options except untoggled boolean options *)
  let print (msg: string) (opt: cmd_option) : ML string =
    if List.Tot.mem (cmd_option_name opt) ignore
    then msg
    else
    match opt with
    | CmdOption name kind desc implies ->
      begin match kind with
      | OptBool v ->
        if !v
        then Printf.sprintf "%s --%s" msg name
        else msg
      | OptStringOption _ _ v ->
        begin match !v with
        | None -> Printf.sprintf "%s --%s" msg (negate_name name)
        | Some v -> Printf.sprintf "%s --%s %s" msg name v
        end
      | OptList _ _ v ->
        let v = !v in
        let msg = Printf.sprintf "%s --%s" msg (negate_name name) in
        let app (msg: string) (s: string) = Printf.sprintf "%s --%s %s" msg name s in
        List.Tot.fold_left app msg (List.Tot.rev v) (* list was accumulated as a fifo *)
      end
    | _ -> msg
  in
  let msg = List.fold_left print "" !options in
  (* then print the untoggled boolean options *)
  let print_untoggle (msg: string) (opt: cmd_option) : ML string =
    match opt with
    | CmdOption name (OptBool v) _ _ ->
      if (if not (List.Tot.mem name ignore) then not !v else false)
      then Printf.sprintf "%s --%s" msg (negate_name name)
      else msg
    | _ -> msg
  in
  List.fold_left print_untoggle msg !options

let get_arg0 () : ML string =
  match !arg0 with
  | None -> "3d"
  | Some v -> v
val display_usage_1 (options: ref (list cmd_option)) : ML unit
options: FStar.ST.ref (Prims.list Options.cmd_option) -> FStar.All.ML Prims.unit