val ln_terms' (t: list (term & term)) (i: int) : bool
let rec ln_terms' (t:list (term & term)) (i:int) : bool =
  match t with
  | [] -> true
  | (t1, t2)::tl -> ln' t1 i && ln' t2 i && ln_terms' tl i
val ln_terms' (t: list (term & term)) (i: int) : bool
let rec ln_terms' (t: list (term & term)) (i: int) : bool =
match t with
| [] -> true
| (t1, t2) :: tl -> ln' t1 i && ln' t2 i && ln_terms' tl i
Pulse.Syntax.Naming.fsti.checked
Pulse.Syntax.Pure.fst.checked Pulse.Syntax.Base.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Elaborate.Pure.fst.checked Pulse.Common.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Reflection.Typing.Builtins.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Pulse.Syntax.Naming.fsti
Prims.list FStar.Pervasives.Native.tuple2 Pulse.Syntax.Base.term Prims.int Prims.op_AmpAmp Pulse.Syntax.Naming.ln' Pulse.Syntax.Naming.ln_terms' Prims.bool
module Pulse.Syntax.Naming

open FStar.List.Tot
open Pulse.Syntax.Base
open Pulse.Common

module L = FStar.List.Tot

module R = FStar.Reflection
module RTB = FStar.Reflection.Typing.Builtins
module RT = FStar.Reflection.Typing
module RU = Pulse.RuntimeUtils
module U = Pulse.Syntax.Pure
module E = Pulse.Elaborate.Pure

let rec freevars (t:term) 
  : Set.set var
  = match t.t with
    | Tm_Emp
    | Tm_VProp
    | Tm_Inames
    | Tm_EmpInames
    | Tm_Unknown -> Set.empty
    | Tm_Star t1 t2 ->
      Set.union (freevars t1) (freevars t2)
    | Tm_ExistsSL _ t1 t2
    | Tm_ForallSL _ t1 t2 ->
      Set.union (freevars t1.binder_ty) (freevars t2)
    | Tm_Pure p -> freevars p
    | Tm_FStar t -> RT.freevars t

let freevars_st_comp (s:st_comp) : Set.set var =
  freevars s.res `Set.union`
  freevars s.pre `Set.union`
  freevars s.post


let freevars_comp (c:comp) : Tot (Set.set var) (decreases c) =
  match c with
  | C_Tot t -> freevars t
  | C_ST s -> freevars_st_comp s
  | C_STAtomic inames s
  | C_STGhost inames s ->
    freevars inames `Set.union` freevars_st_comp s

let freevars_opt (f: 'a -> Set.set var) (x:option 'a) : Set.set var =
  match x with
  | None -> Set.empty
  | Some x -> f x

let freevars_term_opt (t:option term) : Set.set var =
  freevars_opt freevars t

let rec freevars_list (t:list term) : Set.set var =
  match t with
  | [] -> Set.empty
  | hd::tl -> freevars hd `Set.union` freevars_list tl

let rec freevars_pairs (pairs:list (term & term)) : Set.set var =
  match pairs with
  | [] -> Set.empty
  | (t1, t2)::tl -> Set.union (freevars t1) (freevars t2) `Set.union` freevars_pairs tl

let freevars_proof_hint (ht:proof_hint_type) : Set.set var = 
  match ht with
  | ASSERT { p }
  | FOLD { p }
  | UNFOLD { p } -> freevars p
  | RENAME { pairs; goal } ->
    Set.union (freevars_pairs pairs) (freevars_term_opt goal)
  | REWRITE { t1; t2 } ->
    Set.union (freevars t1) (freevars t2)

let rec freevars_st (t:st_term)
  : Set.set var
  = match t.term with
    | Tm_Return { term } ->
      freevars term
    | Tm_Abs { b; ascription; body } ->
      Set.union (freevars b.binder_ty) 
                (Set.union (freevars_st body)
                           (freevars_comp ascription))
    | Tm_STApp { head; arg } ->
      Set.union (freevars head) (freevars arg)
    | Tm_Bind { binder; head; body } ->
      Set.union 
        (Set.union (freevars binder.binder_ty) 
                   (freevars_st head))
        (freevars_st body)
    | Tm_TotBind { binder; head; body } ->
      Set.union
        (Set.union (freevars binder.binder_ty)
                   (freevars head))
        (freevars_st body)
    | Tm_If { b; then_; else_; post } ->
      Set.union (Set.union (freevars b) (freevars_st then_))
                (Set.union (freevars_st else_) (freevars_term_opt post))

    | Tm_Match { sc ; returns_; brs } ->
      let (@@) = Set.union in
      freevars sc
        @@ freevars_term_opt returns_
        @@ freevars_branches brs

    | Tm_IntroPure { p }
    | Tm_ElimExists { p } ->
      freevars p
    | Tm_IntroExists { p; witnesses } ->
      Set.union (freevars p) (freevars_list witnesses)
    | Tm_While { invariant; condition; body } ->
      Set.union (freevars invariant)
                (Set.union (freevars_st condition)
                           (freevars_st body))
    | Tm_Par { pre1; body1; post1; pre2; body2; post2 } ->
      Set.union
        (Set.union (freevars pre1)
                   (Set.union (freevars_st body1)
                              (freevars post1)))
        (Set.union (freevars pre2)
                   (Set.union (freevars_st body2)
                              (freevars post2)))

    | Tm_WithLocal { binder; initializer; body } ->
      Set.union (freevars binder.binder_ty)
                (Set.union (freevars initializer)
                           (freevars_st body))

    | Tm_WithLocalArray { binder; initializer; length; body } ->
      Set.union (freevars binder.binder_ty)
                (Set.union (freevars initializer)
                           (Set.union (freevars length)
                                      (freevars_st body)))

    | Tm_Rewrite { t1; t2 } ->
      Set.union (freevars t1) (freevars t2)

    | Tm_Admit { typ; post } ->
      Set.union (freevars typ)
                (freevars_term_opt post)

    | Tm_ProofHintWithBinders { binders; hint_type; t } ->
      Set.union (freevars_proof_hint hint_type) (freevars_st t)

and freevars_branches (t:list (pattern & st_term)) : Set.set var =
  match t with
  | [] -> Set.empty
  | (_, b)::tl -> freevars_st b `Set.union` freevars_branches tl

let rec ln' (t:term) (i:int) : Tot bool (decreases t) =
  match t.t with
  | Tm_Emp
  | Tm_VProp
  | Tm_Inames
  | Tm_EmpInames
  | Tm_Unknown -> true

  | Tm_Star t1 t2 ->
    ln' t1 i &&
    ln' t2 i

  | Tm_Pure p ->
    ln' p i

  | Tm_ExistsSL _ t body
  | Tm_ForallSL _ t body ->
    ln' t.binder_ty i &&
    ln' body (i + 1)
    
  | Tm_FStar t ->
    RT.ln' t i

let ln_st_comp (s:st_comp) (i:int) : bool =
  ln' s.res i &&
  ln' s.pre i &&
  ln' s.post (i + 1) (* post has 1 impliict abstraction *)


let ln_c' (c:comp) (i:int)
  : bool
  = match c with
    | C_Tot t -> ln' t i
    | C_ST s -> ln_st_comp s i
    | C_STAtomic inames s
    | C_STGhost inames s ->
      ln' inames i &&
      ln_st_comp s i

let ln_opt' (t:option term) (i:int) : bool =
  match t with
  | None -> true
  | Some t -> ln' t i

let rec ln_list' (t:list term) (i:int) : bool =
  match t with
  | [] -> true
  | hd::tl -> ln' hd i && ln_list' tl i
val ln_terms' (t: list (term & term)) (i: int) : bool
t: Prims.list (Pulse.Syntax.Base.term * Pulse.Syntax.Base.term) -> i: Prims.int -> Prims.bool