val make_namedv_with_name (s: pp_name_t) (n: nat) : namedv_view
let make_namedv_with_name (s:pp_name_t) (n:nat) : namedv_view = {
  ppname = s;
  uniq   = n;
  sort   = sort_default;
}
val make_namedv_with_name (s: pp_name_t) (n: nat) : namedv_view
let make_namedv_with_name (s: pp_name_t) (n: nat) : namedv_view =
{ ppname = s; uniq = n; sort = sort_default }
FStar.Reflection.Typing.fsti.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Sealed.Inhabited.fst.checked FStar.Reflection.V2.Data.fsti.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
FStar.Reflection.Typing.fsti
FStar.Reflection.Typing.pp_name_t Prims.nat FStar.Reflection.V2.Data.Mknamedv_view FStar.Reflection.Typing.sort_default FStar.Reflection.V2.Data.namedv_view
(*
   Copyright 2008-2023 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module FStar.Reflection.Typing

(** This module defines a typing judgment for (parts of) the total
    and ghost fragment of F*.
    
    We are using it in the meta DSL framework as an
    official specification for the F* type system.

    We expect it to grow to cover more of the F* language.

    IT IS HIGHLY EXPERIMENTAL AND NOT YET READY TO USE.
  *)

open FStar.List.Tot
open FStar.Reflection.V2
module L = FStar.List.Tot
module R = FStar.Reflection.V2
module T = FStar.Tactics.V2
module RD = FStar.Reflection.V2.Data

(* MOVE to some helper module *)
let rec fold_left_dec #a #b
  (acc : a)
  (l : list b)
  (f : a -> (x:b{x << l}) -> a)
  : Tot a (decreases l)
  =
  match l with
  | [] -> acc
  | x::xs -> fold_left_dec (f acc x) xs f

let rec map_dec #a #b
  (l : list a)
  (f : (x:a{x << l}) -> b)
  : Tot (list b) (decreases l)
  =
  match l with
  | [] -> []
  | x::xs -> f x :: map_dec xs f

let rec zip2prop #a #b (f : a -> b -> Type0) (xs : list a) (ys : list b) : Type0 =
  match xs, ys with
  | [], [] -> True
  | x::xx, y::yy -> f x y /\ zip2prop f xx yy
  | _ -> False
(* / MOVE *)

val inspect_pack (t:R.term_view)
  : Lemma (ensures R.(inspect_ln (pack_ln t) == t))
          [SMTPat R.(inspect_ln (pack_ln t))]
  
val pack_inspect (t:R.term)
  : Lemma (requires ~(Tv_Unsupp? (inspect_ln t)))
          (ensures R.(pack_ln (inspect_ln t) == t))
          [SMTPat R.(pack_ln (inspect_ln t))]
  
val inspect_pack_namedv (t:R.namedv_view)
  : Lemma (ensures R.(inspect_namedv (pack_namedv t) == t))
          [SMTPat R.(inspect_namedv (pack_namedv t))]

val pack_inspect_namedv (t:R.namedv)
  : Lemma (ensures R.(pack_namedv (inspect_namedv t) == t))
          [SMTPat R.(pack_namedv (inspect_namedv t))]

val inspect_pack_bv (t:R.bv_view)
  : Lemma (ensures R.(inspect_bv (pack_bv t) == t))
          [SMTPat R.(inspect_bv (pack_bv t))]
  
val pack_inspect_bv (t:R.bv)
  : Lemma (ensures R.(pack_bv (inspect_bv t) == t))
          [SMTPat R.(pack_bv (inspect_bv t))]
  
val inspect_pack_binder (bview:R.binder_view)
  : Lemma (ensures R.(R.inspect_binder (R.pack_binder bview) == bview))
          [SMTPat R.(inspect_binder (pack_binder bview))]
  
val pack_inspect_binder (t:R.binder)
   : Lemma (ensures (R.pack_binder (R.inspect_binder t) == t))
           [SMTPat (R.pack_binder (R.inspect_binder t))]
  
val inspect_pack_comp (t:R.comp_view)
  : Lemma (ensures (R.inspect_comp (R.pack_comp t) == t))
          [SMTPat (R.inspect_comp (R.pack_comp t))]

val pack_inspect_comp (t:R.comp)
  : Lemma (ensures (R.pack_comp (R.inspect_comp t) == t))
          [SMTPat (R.pack_comp (R.inspect_comp t))]
  
val inspect_pack_fv (nm:R.name)
  : Lemma (ensures R.inspect_fv (R.pack_fv nm) == nm)
          [SMTPat (R.inspect_fv (R.pack_fv nm))]

val pack_inspect_fv (fv:R.fv)
  : Lemma (ensures R.pack_fv (R.inspect_fv fv) == fv)
          [SMTPat (R.pack_fv (R.inspect_fv fv))]

val inspect_pack_universe (u:R.universe_view)
  : Lemma (ensures R.inspect_universe (R.pack_universe u) == u)
          [SMTPat (R.inspect_universe (R.pack_universe u))]

val pack_inspect_universe (u:R.universe)
  : Lemma (requires ~(Uv_Unk? (inspect_universe u)))
          (ensures R.pack_universe (R.inspect_universe u) == u)
          [SMTPat (R.pack_universe (R.inspect_universe u))]

val lookup_bvar (e:env) (x:int) : option term

val lookup_fvar_uinst (e:R.env) (x:R.fv) (us:list R.universe) : option R.term

let lookup_fvar (e:env) (x:fv) : option term = lookup_fvar_uinst e x []

let pp_name_t = FStar.Sealed.Inhabited.sealed "x"
let pp_name_default : pp_name_t = FStar.Sealed.Inhabited.seal "x"
let seal_pp_name x : pp_name_t = FStar.Sealed.Inhabited.seal x

let tun = pack_ln Tv_Unknown

let sort_t = FStar.Sealed.Inhabited.sealed tun
let sort_default : sort_t = FStar.Sealed.Inhabited.seal tun
let seal_sort x : sort_t = FStar.Sealed.Inhabited.seal x

let mk_binder (pp_name:pp_name_t) (ty:term) (q:aqualv) : binder
  = pack_binder
      { ppname = pp_name;
        qual   = q;
        attrs  = [];
        sort   = ty}

let mk_simple_binder (pp_name:pp_name_t) (ty:term) : simple_binder
  = pack_binder
      { ppname = pp_name;
        qual   = Q_Explicit;
        attrs  = [];
        sort   = ty}

let extend_env (e:env) (x:var) (ty:term) : env =
  R.push_binding e ({
    ppname = seal_pp_name "x";
    uniq   = x;
    sort   = ty;
  })
  
val lookup_bvar_extend_env (g:env) (x y:var) (ty:term)
  : Lemma 
    (ensures (
           if x = y
           then lookup_bvar (extend_env g x ty) y == Some ty
           else lookup_bvar (extend_env g x ty) y == lookup_bvar g y))
    [SMTPat (lookup_bvar (extend_env g x ty) y)]

val lookup_fvar_extend_env (g:env) (x:fv) (us:universes) (y:var) (ty:term)
  : Lemma 
    (ensures lookup_fvar_uinst (extend_env g y ty) x us == lookup_fvar_uinst g x us)
    [SMTPat (lookup_fvar_uinst (extend_env g y ty) x us)]

let bv_index (x:bv)
  : var
  = (inspect_bv x).index

let namedv_uniq (x:namedv)
  : var
  = (inspect_namedv x).uniq

let binder_sort (b:binder) =
  (inspect_binder b).sort

let binder_qual (b:binder) =
  let { qual = q } = inspect_binder b in q

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)

let subst = list subst_elt

let shift_subst_n (n:nat) = L.map (shift_subst_elt n)

let shift_subst = shift_subst_n 1

let maybe_uniq_of_term (x:term) =
  match inspect_ln x with
  | Tv_Var namedv -> Some (namedv_uniq namedv)
  | _ -> None

let rec find_matching_subst_elt_bv (s:subst) (bv:bv) : option subst_elt =
  match s with
  | [] -> None
  | (DT j t)::ss ->
    if j = bv_index bv
    then Some (DT j t)
    else find_matching_subst_elt_bv ss bv
  | _::ss -> find_matching_subst_elt_bv ss bv

let subst_db (bv:bv) (s:subst) : term =
  match find_matching_subst_elt_bv s bv with
  | Some (DT _ t) ->
    (match maybe_uniq_of_term t with
     | None -> t
     | Some k ->
       //if we're substituting a name j for a name k, retain the pp_name of j
       let v : namedv = pack_namedv {
         sort = (inspect_bv bv).sort;
         ppname = (inspect_bv bv).ppname;
         uniq = k;
       } in
       pack_ln (Tv_Var v))
  | _ -> pack_ln (Tv_BVar bv)

let rec find_matching_subst_elt_var (s:subst) (v:namedv) : option subst_elt =
  match s with
  | [] -> None
  | (NT y _)::rest 
  | (ND y _)::rest ->
    if y = namedv_uniq v
    then Some (L.hd s)
    else find_matching_subst_elt_var rest v
  | _::rest -> find_matching_subst_elt_var rest v

let subst_var (v:namedv) (s:subst) : term =
  match find_matching_subst_elt_var s v with
  | Some (NT _ t) ->
    (match maybe_uniq_of_term t with
     | None -> t
     | Some k ->
       pack_ln (Tv_Var (pack_namedv { inspect_namedv v with uniq = k })))
  | Some (ND _ i) ->
    let bv = pack_bv {
      sort = (inspect_namedv v).sort;
      ppname = (inspect_namedv v).ppname;
      index = i;
    } in
    pack_ln (Tv_BVar bv)
  | _ -> pack_ln (Tv_Var v)

let make_bv (n:nat) : bv_view = {
  ppname = pp_name_default;
  index = n;
  sort = sort_default;
}
let make_bv_with_name (s:pp_name_t) (n:nat) : bv_view = {
  ppname = s;
  index  = n;
  sort   = sort_default;
}


let var_as_bv (v:nat) = pack_bv (make_bv v)

let make_namedv (n:nat) : namedv_view = {
  ppname = pp_name_default;
  uniq   = n;
  sort   = sort_default;
}
val make_namedv_with_name (s: pp_name_t) (n: nat) : namedv_view
s: FStar.Reflection.Typing.pp_name_t -> n: Prims.nat -> FStar.Reflection.V2.Data.namedv_view