val genv_abstract_bvs : genv -> Tot (list (bv & typ))
let genv_abstract_bvs ge =
  List.Tot.concatMap
    (fun (bv, (ty, abs, _)) -> if abs then [bv,ty] else []) ge.bmap
val genv_abstract_bvs : genv -> Tot (list (bv & typ))
let genv_abstract_bvs ge =
List.Tot.concatMap (fun (bv, (ty, abs, _)) -> if abs then [bv, ty] else []) ge.bmap
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
FStar.InteractiveHelpers.Base.genv FStar.List.Tot.Base.concatMap FStar.Pervasives.Native.tuple2 FStar.Reflection.Types.bv FStar.Pervasives.Native.tuple3 FStar.Reflection.Types.typ Prims.bool FStar.Reflection.Types.term Prims.Cons FStar.Pervasives.Native.Mktuple2 Prims.Nil Prims.list FStar.InteractiveHelpers.Base.__proj__Mkgenv__item__bmap
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
let print_dbg debug s =
  if debug then print s

/// Return the qualifier of a term as a string
val term_view_construct (t : term_view) : Tac string

let term_view_construct (t : term_view) : Tac string =
  match t with
  | Tv_Var _ -> "Tv_Var"
  | Tv_BVar _ -> "Tv_BVar"
  | Tv_FVar _ -> "Tv_FVar"
  | Tv_App _ _ -> "Tv_App"
  | Tv_Abs _ _ -> "Tv_Abs"
  | Tv_Arrow _ _ -> "Tv_Arrow"
  | Tv_Type _ -> "Tv_Type"
  | Tv_Refine _ _ _ -> "Tv_Refine"
  | Tv_Const _ -> "Tv_Const"
  | Tv_Uvar _ _ -> "Tv_Uvar"
  | Tv_Let _ _ _ _ _ _ -> "Tv_Let"
  | Tv_Match _ _ _ -> "Tv_Match"
  | Tv_AscribedT _ _ _ _ -> "Tv_AscribedT"
  | Tv_AscribedC _ _ _ _ -> "Tv_AScribedC"
  | _ -> "Tv_Unknown"

val term_construct (t : term) : Tac string

let term_construct (t : term) : Tac string =
  term_view_construct (inspect t)

(*** Pretty printing *)
/// There are many issues linked to terms (pretty) printing.
/// The first issue is that when parsing terms, F* automatically inserts
/// ascriptions, which then clutter the terms printed to the user. The current
/// workaround is to filter those ascriptions in the terms before exploiting them.
/// TODO: this actually doesn't work for some unknown reason: some terms like [a /\ b]
/// become [l_and a b]...

val filter_ascriptions : bool -> term -> Tac term

let filter_ascriptions dbg t =
  print_dbg dbg ("[> filter_ascriptions: " ^ term_view_construct t ^ ": " ^ term_to_string t );
  visit_tm (fun t ->
    match inspect t with
    | Tv_AscribedT e _ _ _
    | Tv_AscribedC e _ _ _ -> e
    | _ -> t) t

/// Our prettification function. Apply it to all the terms which might be printed
/// back to the user. Note that the time at which the function is applied is
/// important: we can't apply it on all the assertions we export to the user, just
/// before exporting, because we may have inserted ascriptions on purpose, which
/// would then be filtered away.
val prettify_term : bool -> term -> Tac term
let prettify_term dbg t = filter_ascriptions dbg t

(*** Environments *)
/// We need a way to handle environments with variable bindings
/// and name shadowing, to properly display the context to the user.

/// A map linking variables to terms. For now we use a list to define it, because
/// there shouldn't be too many bindings.
type bind_map (a : Type) = list (bv & a)

let bind_map_push (#a:Type) (m:bind_map a) (b:bv) (x:a) = (b,x)::m

let rec bind_map_get (#a:Type) (m:bind_map a) (b:bv) : Tot (option a) =
  match m with
  | [] -> None
  | (b', x)::m' ->
    if compare_bv b b' = Order.Eq then Some x else bind_map_get m' b

let rec bind_map_get_from_name (#a:Type) (m:bind_map a) (name:string) :
  Tac (option (bv & a)) =
  match m with
  | [] -> None
  | (b', x)::m' ->
    let b'v = inspect_bv b' in
    if unseal b'v.bv_ppname = name then Some (b', x) else bind_map_get_from_name m' name

noeq type genv =
{
  env : env;
  (* Whenever we evaluate a let binding, we keep track of the relation between
   * the binder and its definition.
   * The boolean indicates whether or not the variable is considered abstract. We
   * often need to introduce variables which don't appear in the user context, for
   * example when we need to deal with a postcondition for Stack or ST, which handles
   * the previous and new memory states, and which may not be available in the user
   * context, or where we don't always know which variable to use.
   * In this case, whenever we output the term, we write its content as an
   * abstraction applied to those missing parameters. For instance, in the
   * case of the assertion introduced for a post-condition:
   * [> assert((fun h1 h2 -> post) h1 h2);
   * Besides the informative goal, the user can replace those parameters (h1
   * and h2 above) by the proper ones then normalize the assertion by using
   * the appropriate command to get a valid assertion. *)
  bmap : bind_map (typ & bool & term);
  (* Whenever we introduce a new variable, we check whether it shadows another
   * variable because it has the same name, and put it in the below
   * list. Of course, for the F* internals such shadowing is not an issue, because
   * the index of every variable should be different, but this is very important
   * when generating code for the user *)
  svars : list (bv & typ);
}

let get_env (e:genv) : env = e.env
let get_bind_map (e:genv) : bind_map (typ & bool & term) = e.bmap
let mk_genv env bmap svars : genv = Mkgenv env bmap svars
let mk_init_genv env : genv = mk_genv env [] []

val genv_to_string : genv -> Tac string
let genv_to_string ge =
  let binder_to_string (b : binder) : Tac string =
    abv_to_string (bv_of_binder b) ^ "\n"
  in
  let binders_str = map binder_to_string (binders_of_env ge.env) in
  let bmap_elem_to_string (e : bv & (typ & bool & term)) : Tac string =
    let bv, (_sort, abs, t) = e in
    "(" ^ abv_to_string bv ^" -> (" ^
    string_of_bool abs ^ ", " ^ term_to_string t ^ "))\n"
  in
  let bmap_str = map bmap_elem_to_string ge.bmap in
  let svars_str = map (fun (bv, _) -> abv_to_string bv ^ "\n") ge.svars in
  let flatten = List.Tot.fold_left (fun x y -> x ^ y) "" in
  "> env:\n" ^ flatten binders_str ^
  "> bmap:\n" ^ flatten bmap_str ^
  "> svars:\n" ^ flatten svars_str

let genv_get (ge:genv) (b:bv) : Tot (option (typ & bool & term)) =
  bind_map_get ge.bmap b

let genv_get_from_name (ge:genv) (name:string) : Tac (option ((bv & typ) & (bool & term))) =
  (* tweak return a bit to include sort *)
  match bind_map_get_from_name ge.bmap name with
  | None -> None
  | Some (bv, (sort, b, x)) -> Some ((bv, sort), (b, x))

/// Push a binder to a ``genv``. Optionally takes a ``term`` which provides the
/// term the binder is bound to (in a `let _ = _ in` construct for example).
let genv_push_bv (ge:genv) (b:bv) (sort:typ) (abs:bool) (t:option term) : Tac genv =
  let br = mk_binder b sort in
  let sv = genv_get_from_name ge (name_of_bv b) in
  let svars' = if Some? sv then fst (Some?.v sv) :: ge.svars else ge.svars in
  let e' = push_binder ge.env br in
  let tm = if Some? t then Some?.v t else pack (Tv_Var b) in
  let bmap' = bind_map_push ge.bmap b (sort, abs, tm) in
  mk_genv e' bmap' svars'

let genv_push_binder (ge:genv) (b:binder) (abs:bool) (t:option term) : Tac genv =
  genv_push_bv ge (bv_of_binder b) (binder_sort b) abs t

/// Check if a binder is shadowed by another more recent binder
let bv_is_shadowed (ge : genv) (bv : bv) : Tot bool =
  List.Tot.existsb (fun (b,_) -> bv_eq bv b) ge.svars

let binder_is_shadowed (ge : genv) (b : binder) : Tot bool =
  bv_is_shadowed ge (bv_of_binder b)

let find_shadowed_bvs (ge : genv) (bl : list bv) : Tot (list (bv & bool)) =
  List.Tot.map (fun b -> b, bv_is_shadowed ge b) bl

let find_shadowed_binders (ge : genv) (bl : list binder) : Tot (list (binder & bool)) =
  List.Tot.map (fun b -> b, binder_is_shadowed ge b) bl

val bv_is_abstract : genv -> bv -> Tot bool
let bv_is_abstract ge bv =
  match genv_get ge bv with
  | None -> false
  | Some (_, abs, _) -> abs

val binder_is_abstract : genv -> binder -> Tot bool
let binder_is_abstract ge b =
  bv_is_abstract ge (bv_of_binder b)

val genv_abstract_bvs : genv -> Tot (list (bv & typ))
val genv_abstract_bvs : genv -> Tot (list (bv & typ))
ge: FStar.InteractiveHelpers.Base.genv
  -> Prims.list (FStar.Reflection.Types.bv * FStar.Reflection.Types.typ)