let subst = list subst_elt
let subst =
list subst_elt
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 Pulse.Syntax.Naming.subst_elt
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

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

let ln_proof_hint' (ht:proof_hint_type) (i:int) : bool =
  match ht with
  | ASSERT { p }
  | UNFOLD { p }
  | FOLD   { p } -> ln' p i
  | RENAME { pairs; goal } ->
    ln_terms' pairs i &&
    ln_opt' goal i
  | REWRITE { t1; t2 } ->
    ln' t1 i &&
    ln' t2 i

let rec pattern_shift_n (p:pattern)
  : Tot nat
  = match p with
    | Pat_Constant _ 
    | Pat_Dot_Term _ -> 
      0
    | Pat_Var _ _ ->
      1
    | Pat_Cons fv l ->
      pattern_args_shift_n l
and pattern_args_shift_n (ps:list (pattern & bool))
  : Tot nat
  = match ps with
    | [] -> 0
    | (p, _)::tl ->
      pattern_shift_n p + pattern_args_shift_n tl

let rec ln_pattern' (p : pattern) (i:int)
  : Tot bool (decreases p)
  = match p with
    | Pat_Constant _ 
    | Pat_Var _ _ 
    | Pat_Dot_Term None ->
      true
    | Pat_Dot_Term (Some e) ->
      ln' e i
    | Pat_Cons fv l ->
      ln_pattern_args' l i
 
and ln_pattern_args' (p:list (pattern & bool)) (i:int)
  : Tot bool (decreases p)
  = match p with
    | [] ->
      true
    | (p, _)::tl ->
      ln_pattern' p i &&
      ln_pattern_args' tl (i + pattern_shift_n p)

let rec ln_st' (t:st_term) (i:int)
  : Tot bool (decreases t)
  = match t.term with
    | Tm_Return { term } ->
      ln' term i
      
    | Tm_Abs { b; ascription; body } ->
      ln' b.binder_ty i &&
      ln_st' body (i + 1) &&
      ln_c' ascription (i + 1)

    | Tm_STApp { head; arg } ->
      ln' head i &&
      ln' arg i

    | Tm_Bind { binder; head; body } ->
      ln' binder.binder_ty i &&
      ln_st' head i &&
      ln_st' body (i + 1)

    | Tm_TotBind { binder; head; body } ->
      ln' binder.binder_ty i &&
      ln' head i &&
      ln_st' body (i + 1)

    | Tm_If { b; then_; else_; post } ->
      ln' b i &&
      ln_st' then_ i &&
      ln_st' else_ i &&
      ln_opt' post (i + 1)
  
    | Tm_Match {sc; returns_; brs } ->
      ln' sc i &&
      ln_opt' returns_ i &&
      ln_branches' t brs i

    | Tm_IntroPure { p }
    | Tm_ElimExists { p } ->
      ln' p i

    | Tm_IntroExists { p; witnesses } ->
      ln' p i &&
      ln_list' witnesses i
  
    | Tm_While { invariant; condition; body } ->
      ln' invariant (i + 1) &&
      ln_st' condition i &&
      ln_st' body i

    | Tm_Par { pre1; body1; post1; pre2; body2; post2 } ->
      ln' pre1 i &&
      ln_st' body1 i &&
      ln' post1 (i + 1) &&
      ln' pre2 i &&
      ln_st' body2 i &&
      ln' post2 (i + 1)

    | Tm_WithLocal { binder; initializer; body } ->
      ln' binder.binder_ty i &&
      ln' initializer i &&
      ln_st' body (i + 1)

    | Tm_WithLocalArray { binder; initializer; length; body } ->
      ln' binder.binder_ty i &&
      ln' initializer i &&
      ln' length i &&
      ln_st' body (i + 1)

    | Tm_Rewrite { t1; t2 } ->
      ln' t1 i &&
      ln' t2 i

    | Tm_Admit { typ; post } ->
      ln' typ i &&
      ln_opt' post (i + 1)

    | Tm_ProofHintWithBinders { binders; hint_type; t } ->
      let n = L.length binders in
      ln_proof_hint' hint_type (i + n) &&
      ln_st' t (i + n)

and ln_branch' (b : pattern & st_term) (i:int) : Tot bool (decreases b) =
  let (p, e) = b in
  ln_pattern' p i &&
  ln_st' e (i + pattern_shift_n p)
  
and ln_branches' (t:st_term) (brs : list branch{brs << t}) (i:int) : Tot bool (decreases brs) =
  for_all_dec t brs (fun b -> ln_branch' b i)

let ln (t:term) = ln' t (-1)
let ln_st (t:st_term) = ln_st' t (-1)
let ln_c (c:comp) = ln_c' c (-1)

noeq
type subst_elt =
  | DT : nat -> term -> subst_elt
  | NT : var -> term -> subst_elt
  | ND : var -> nat -> subst_elt

let shift_subst_elt (n:nat) = function
  | DT i t -> DT (i + n) t
  | NT x t -> NT x t
  | ND x i -> ND x (i + n)
val subst : Type0
Type0