val batch:ref bool
let batch : ref bool = alloc false
val batch:ref bool
let batch:ref bool =
alloc 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
FStar.ST.alloc Prims.bool FStar.Heap.trivial_preorder FStar.ST.mref
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
val batch:ref bool
FStar.ST.ref Prims.bool