val valid_check_hashes: string -> Tot bool
let valid_check_hashes : string -> Tot bool = function
| "weak"
| "strong"
| "inplace"
  -> true
| _ -> false
val valid_check_hashes: string -> Tot bool
let valid_check_hashes: string -> Tot bool =
function
| "weak" | "strong" | "inplace" -> true
| _ -> false
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
Prims.string Prims.bool
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 []
val valid_check_hashes: string -> Tot bool
_: Prims.string -> Prims.bool