val print_dbg : bool -> string -> Tac unit
let print_dbg debug s =
  if debug then print s
val print_dbg : bool -> string -> Tac unit
let print_dbg debug s =
if debug then print s
FStar.InteractiveHelpers.Base.fst.checked
prims.fst.checked FStar.Tactics.Util.fst.checked FStar.Tactics.fst.checked FStar.Sealed.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
FStar.InteractiveHelpers.Base.fst
Prims.bool Prims.string FStar.Tactics.V1.Builtins.print Prims.unit
module FStar.InteractiveHelpers.Base

open FStar.List
open FStar.Tactics
open FStar.Mul

#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"

(*** Utilities *)
val bv_eq : bv -> bv -> Tot bool
let bv_eq (bv1 bv2 : bv) =
  let bvv1 = inspect_bv bv1 in
  let bvv2 = inspect_bv bv2 in
  (* We don't check for type equality: the fact that no two different binders
   * have the same name and index is an invariant which must be enforced -
   * and actually we could limit ourselves to checking the index *)
  bvv1.bv_index = bvv2.bv_index

val fv_eq : fv -> fv -> Tot bool
let fv_eq fv1 fv2 =
  let n1 = inspect_fv fv1 in
  let n2 = inspect_fv fv2 in
  n1 = n2

// TODO: use everywhere
val fv_eq_name : fv -> name -> Tot bool
let fv_eq_name fv n =
  let fvn = inspect_fv fv in
  fvn = n

// TODO: use more
val opt_apply (#a #b : Type) (f : a -> Tot b) (x : option a) : Tot (option b)
let opt_apply #a #b f x =
  match x with
  | None -> None
  | Some x' -> Some (f x')

val opt_tapply (#a #b : Type) (f : a -> Tac b) (x : option a) : Tac (option b)
let opt_tapply #a #b f x =
  match x with
  | None -> None
  | Some x' -> Some (f x')

val option_to_string : (#a : Type) -> (a -> Tac string) -> option a -> Tac string
let option_to_string #a f x =
  match x with
  | None -> "None"
  | Some x' -> "Some (" ^ f x' ^ ")"


let opt_cons (#a : Type) (opt_x : option a) (ls : list a) : Tot (list a) =
  match opt_x with
  | Some x -> x :: ls
  | None -> ls

val list_to_string : #a : Type -> (a -> Tac string) -> list a -> Tac string
let list_to_string #a f ls =
  (Tactics.Util.fold_left (fun s x -> s ^ " (" ^ f x ^ ");") "[" ls) ^ "]"


/// Apply a term to a list of parameters, normalize the result to make sure
/// all the abstractions are simplified
val mk_app_norm : env -> term -> list term -> Tac term
let mk_app_norm e t params =
  let t1 = mk_e_app t params in
  let t2 = norm_term_env e [] t1 in
  t2

val opt_mk_app_norm : env -> option term -> list term -> Tac (option term)
let opt_mk_app_norm e opt_t params =
  opt_tapply (fun t -> mk_app_norm e t params) opt_t

// TODO: remove
let rec unzip #a #b (l : list (a & b)) : Tot (list a & list b) =
  match l with
  | [] -> ([],[])
  | (hd1,hd2)::tl ->
       let (tl1,tl2) = unzip tl in
       (hd1::tl1,hd2::tl2)

/// Alternative ``bv_to_string`` function where we print the index of the bv.
/// It can be very useful for debugging.
let abv_to_string bv : Tac string =
  let bvv = inspect_bv bv in
  name_of_bv bv ^ " (%" ^ string_of_int (bvv.bv_index) ^ ")"

let print_binder_info (full : bool) (b : binder) : Tac unit =
  let open inspect_binder b <: binder_view in
  let qual_str = match binder_qual with
    | Q_Implicit -> "Implicit"
    | Q_Explicit -> "Explicit"
    | Q_Meta t -> "Meta: " ^ term_to_string t
  in
  let bview = inspect_bv binder_bv in
  if full then
    print (
      "> print_binder_info:" ^
      "\n- name: " ^ (name_of_binder b) ^
      "\n- as string: " ^ (binder_to_string b) ^
      "\n- aqual: " ^ qual_str ^
      "\n- ppname: " ^ name_of_bv binder_bv ^
      "\n- index: " ^ string_of_int bview.bv_index ^
      "\n- sort: " ^ term_to_string binder_sort
    )
  else print (binder_to_string b)

let print_binders_info (full : bool) (e:env) : Tac unit =
  iter (print_binder_info full) (binders_of_env e)

let acomp_to_string (c:comp) : Tac string =
  match inspect_comp c with
  | C_Total ret ->
    "C_Total (" ^ term_to_string ret ^ ")"
  | C_GTotal ret ->
    "C_GTotal (" ^ term_to_string ret ^ ")"
  | C_Lemma pre post patterns ->
    "C_Lemma (" ^ term_to_string pre ^ ") (" ^ term_to_string post ^ ")"
  | C_Eff us eff_name result eff_args _ ->
    let eff_arg_to_string (a : term) : Tac string =
      " (" ^ term_to_string a ^ ")"
    in
    let args_str = map (fun (x, y) -> eff_arg_to_string x) eff_args in
    let args_str = List.Tot.fold_left (fun x y -> x ^ y) "" args_str in
    "C_Eff (" ^ flatten_name eff_name ^ ") (" ^ term_to_string result ^ ")" ^ args_str

exception MetaAnalysis of string
let mfail str =
  raise (MetaAnalysis str)

(*** Debugging *)
/// Some debugging facilities
val print_dbg : bool -> string -> Tac unit
val print_dbg : bool -> string -> Tac unit
debug: Prims.bool -> s: Prims.string -> FStar.Tactics.Effect.Tac Prims.unit