val open_pat (p: R.pattern) (s: subst_t) : Tac (pattern & subst_t)
let rec open_pat (p : R.pattern) (s : subst_t) : Tac (pattern & subst_t) =
  match p with
  | R.Pat_Constant c ->
    Pat_Constant {c=c}, s

  | R.Pat_Var ssort n ->
    let sort = unseal ssort in
    let sort = subst_term s sort in
    let nvv : namedv = {
      uniq = fresh();
      sort = seal sort;
      ppname = n;
    }
    in
    let nv = pack_namedv nvv in
    Pat_Var {v=nvv; sort=seal sort}, (DB 0 nv) :: shift_subst 1 s

  | R.Pat_Cons head univs subpats ->
    let subpats, s = fold_left (fun (pats,s) (pat,b) ->
                        let pat, s' = open_pat pat s in
                        ((pat,b)::pats, s'))
                       ([], s) subpats
    in
    let subpats = List.Tot.rev subpats in
    Pat_Cons {head=head; univs=univs; subpats=subpats}, s

  | R.Pat_Dot_Term None ->
    Pat_Dot_Term {t=None}, s

  | R.Pat_Dot_Term (Some t) ->
    let t = subst_term s t in
    Pat_Dot_Term {t=Some t}, s
val open_pat (p: R.pattern) (s: subst_t) : Tac (pattern & subst_t)
let rec open_pat (p: R.pattern) (s: subst_t) : Tac (pattern & subst_t) =
match p with
| R.Pat_Constant c -> Pat_Constant ({ c = c }), s
| R.Pat_Var ssort n ->
  let sort = unseal ssort in
  let sort = subst_term s sort in
  let nvv:namedv = { uniq = fresh (); sort = seal sort; ppname = n } in
  let nv = pack_namedv nvv in
  Pat_Var ({ v = nvv; sort = seal sort }), (DB 0 nv) :: shift_subst 1 s
| R.Pat_Cons head univs subpats ->
  let subpats, s =
    fold_left (fun (pats, s) (pat, b) ->
          let pat, s' = open_pat pat s in
          ((pat, b) :: pats, s'))
      ([], s)
      subpats
  in
  let subpats = List.Tot.rev subpats in
  Pat_Cons ({ head = head; univs = univs; subpats = subpats }), s
| R.Pat_Dot_Term None -> Pat_Dot_Term ({ t = None }), s
| R.Pat_Dot_Term (Some t) ->
  let t = subst_term s t in
  Pat_Dot_Term ({ t = Some t }), s
FStar.Tactics.NamedView.fst.checked
prims.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.Util.fst.checked FStar.Tactics.Effect.fsti.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.Tactics.NamedView.fst
FStar.Reflection.V2.Data.pattern FStar.Stubs.Syntax.Syntax.subst_t FStar.Reflection.V2.Data.vconst FStar.Pervasives.Native.Mktuple2 FStar.Tactics.NamedView.pattern FStar.Tactics.NamedView.Pat_Constant FStar.Tactics.NamedView.Mkpattern__Pat_Constant__payload FStar.Pervasives.Native.tuple2 FStar.Sealed.sealed FStar.Reflection.Types.term FStar.Reflection.V2.Data.ppname_t FStar.Tactics.NamedView.Pat_Var FStar.Tactics.NamedView.Mkpattern__Pat_Var__payload FStar.Sealed.seal FStar.Reflection.Types.typ Prims.Cons FStar.Stubs.Syntax.Syntax.subst_elt FStar.Stubs.Syntax.Syntax.DB FStar.Reflection.V2.Derived.shift_subst FStar.Reflection.Types.namedv FStar.Reflection.V2.Builtins.pack_namedv FStar.Tactics.NamedView.namedv FStar.Reflection.V2.Data.Mknamedv_view Prims.nat FStar.Tactics.V2.Builtins.fresh FStar.Reflection.V2.Builtins.subst_term FStar.Tactics.Unseal.unseal FStar.Reflection.Types.fv FStar.Pervasives.Native.option FStar.Reflection.V2.Data.universes Prims.list Prims.bool FStar.Tactics.NamedView.Pat_Cons FStar.Tactics.NamedView.Mkpattern__Pat_Cons__payload FStar.List.Tot.Base.rev FStar.Tactics.Util.fold_left FStar.Tactics.NamedView.open_pat Prims.Nil FStar.Tactics.NamedView.Pat_Dot_Term FStar.Tactics.NamedView.Mkpattern__Pat_Dot_Term__payload FStar.Pervasives.Native.None FStar.Tactics.NamedView.term FStar.Pervasives.Native.Some
(*
   Copyright 2008-2018 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.Tactics.NamedView

(* inner let bindings not encoded, OK *)
#set-options "--warn_error -242"

(* This file is part of the tactics core, we open only what's needed. *)
open FStar.Tactics.Effect
open FStar.Tactics.Util
open FStar.Tactics.V2.Builtins

exception LengthMismatch
exception NotEnoughBinders

(* We work with reflection V2. *)
module R = FStar.Reflection.V2
module RD = FStar.Reflection.V2.Data

let open_universe_view (v:RD.universe_view) : named_universe_view =
  match v with
  | R.Uv_Zero -> Uv_Zero
  | R.Uv_Succ u -> Uv_Succ u
  | R.Uv_Max us -> Uv_Max us
  | R.Uv_BVar n -> Uv_BVar n
  | R.Uv_Name i -> Uv_Name (inspect_ident i)
  | R.Uv_Unif uvar -> Uv_Unif uvar
  | R.Uv_Unk -> Uv_Unk

let inspect_universe (u:universe) : named_universe_view =
  let v = R.inspect_universe u in
  open_universe_view v

let close_universe_view (v:named_universe_view) : R.universe_view =
  match v with
  | Uv_Zero -> R.Uv_Zero
  | Uv_Succ u -> R.Uv_Succ u
  | Uv_Max us -> R.Uv_Max us
  | Uv_BVar n -> R.Uv_BVar n
  | Uv_Name i -> R.Uv_Name (pack_ident i)
  | Uv_Unif uvar -> R.Uv_Unif uvar
  | Uv_Unk -> R.Uv_Unk

let pack_universe (uv:named_universe_view) : universe =
  let uv = close_universe_view uv in
  R.pack_universe uv

private
let __binding_to_binder (bnd : binding) (b : R.binder) : binder =
  {
      ppname = bnd.ppname;
      uniq   = bnd.uniq;
      sort   = bnd.sort;
      qual   = (inspect_binder b).qual;
      attrs  = (inspect_binder b).attrs;
  }

private
let r_binder_to_namedv (b : binder) : R.namedv =
  pack_namedv {
    uniq   = b.uniq;
    sort   = seal b.sort;
    ppname = b.ppname;
  }

private
let open_binder (b : R.binder) : Tac binder =
  let n = fresh () in
  let bv = inspect_binder b in
  {
    uniq   = n;
    sort   = bv.sort;
    ppname = bv.ppname;
    qual   = bv.qual;
    attrs  = bv.attrs;
  }

private
let close_binder (b : binder) : R.binder =
  pack_binder {
    sort   = b.sort;
    qual   = b.qual;
    ppname = b.ppname;
    attrs  = b.attrs;
  }

private
let open_term_with (b : R.binder) (nb : binder) (t : term) : Tac term =
  let nv : R.namedv = pack_namedv {
    uniq   = nb.uniq;
    sort   = seal nb.sort;
    ppname = nb.ppname;
  }
  in
  let t' = subst_term [DB 0 nv] t in
  t'

private
let open_term (b : R.binder) (t : term) : Tac (binder & term) =
  let bndr : binder = open_binder b in
  (bndr, open_term_with b bndr t)

let subst_comp (s : subst_t) (c : comp) : comp =
  inspect_comp (R.subst_comp s (pack_comp c))

private
let open_comp (b : R.binder) (t : comp) : Tac (binder & comp) =
  let n = fresh () in
  let bv : binder_view = inspect_binder b in
  let nv : R.namedv = pack_namedv {
    uniq   = n;
    sort   = seal bv.sort;
    ppname = bv.ppname;
  }
  in
  let t' = subst_comp [DB 0 nv] t in
  let bndr : binder = {
    uniq   = n;
    sort   = bv.sort;
    ppname = bv.ppname;
    qual   = bv.qual;
    attrs  = bv.attrs;
  }
  in
  (bndr, t')

private
let open_comp_with (b : R.binder) (nb : binder) (c : comp) : Tac comp =
  let nv : R.namedv = pack_namedv {
    uniq   = nb.uniq;
    sort   = seal nb.sort;
    ppname = nb.ppname;
  }
  in
  let t' = subst_comp [DB 0 nv] c in
  t'

(* FIXME: unfortunate duplication here. The effect means this proof cannot
be done extrinsically. Can we add a refinement to the binder? *)
private
let open_term_simple (b : R.simple_binder) (t : term) : Tac (simple_binder & term) =
  let n = fresh () in
  let bv : binder_view = inspect_binder b in
  let nv : R.namedv = pack_namedv {
    uniq   = n;
    sort   = seal bv.sort;
    ppname = bv.ppname;
  }
  in
  let t' = subst_term [DB 0 nv] t in
  let bndr : binder = {
    uniq   = n;
    sort   = bv.sort;
    ppname = bv.ppname;
    qual   = bv.qual;
    attrs  = bv.attrs;
  }
  in
  (bndr, t')

private
let open_comp_simple (b : R.simple_binder) (t : comp) : Tac (simple_binder & comp) =
  let n = fresh () in
  let bv : binder_view = inspect_binder b in
  let nv : R.namedv = pack_namedv {
    uniq   = n;
    sort   = seal bv.sort;
    ppname = bv.ppname;
  }
  in
  let t' = subst_comp [DB 0 nv] t in
  let bndr : binder = {
    uniq   = n;
    sort   = bv.sort;
    ppname = bv.ppname;
    qual   = bv.qual;
    attrs  = bv.attrs;
  }
  in
  (bndr, t')

(* This can be useful externally *)
let close_term (b:binder) (t:term) : R.binder & term =
  let nv = r_binder_to_namedv b in
  let t' = subst_term [NM nv 0] t in
  let b = pack_binder { sort = b.sort; ppname = b.ppname; qual = b.qual; attrs = b.attrs } in
  (b, t')
private
let close_comp (b:binder) (t:comp) : R.binder & comp =
  let nv = r_binder_to_namedv b in
  let t' = subst_comp [NM nv 0] t in
  let b = pack_binder { sort = b.sort; ppname = b.ppname; qual = b.qual; attrs = b.attrs } in
  (b, t')

private
let close_term_simple (b:simple_binder) (t:term) : R.simple_binder & term =
  let nv = r_binder_to_namedv b in
  let t' = subst_term [NM nv 0] t in
  let bv : binder_view = { sort = b.sort; ppname = b.ppname; qual = b.qual; attrs = b.attrs } in
  let b = pack_binder bv in
  inspect_pack_binder bv;
  (b, t')
private
let close_comp_simple (b:simple_binder) (t:comp) : R.simple_binder & comp =
  let nv = r_binder_to_namedv b in
  let t' = subst_comp [NM nv 0] t in
  let bv : binder_view = { sort = b.sort; ppname = b.ppname; qual = b.qual; attrs = b.attrs } in
  let b = pack_binder bv in
  inspect_pack_binder bv;
  (b, t')

private
let r_subst_binder_sort (s : subst_t) (b : R.binder) : R.binder =
  let v = inspect_binder b in
  let v = { v with sort = subst_term s v.sort } in
  pack_binder v

let subst_binder_sort (s : subst_t) (b : binder) : binder =
  { b with sort = subst_term s b.sort }

(* Can't define this inside open_term_n. See #2955 *)
private
let rec __open_term_n_aux (bs : list R.binder) (nbs : list binder) (s : subst_t) : Tac (list binder & subst_t) =
  match bs with
  | [] -> nbs, s
  | b::bs ->
    let b = r_subst_binder_sort s b in
    let b = open_binder b in
    let nv = r_binder_to_namedv b in
    __open_term_n_aux bs (b::nbs) (DB 0 nv :: shift_subst 1 s)

private
let open_term_n (bs : list R.binder) (t : term) : Tac (list binder & term) =
  let nbs, s = __open_term_n_aux bs [] [] in
  List.Tot.rev nbs, subst_term s t

private
let rec open_term_n_with (bs : list R.binder) (nbs : list binder) (t : term) : Tac term =
  match bs, nbs with
  | [], [] -> t
  | b::bs, nb::nbs ->
    let t' = open_term_n_with bs nbs t in
    let t'' = open_term_with b nb t' in
    t''
  | _ -> raise LengthMismatch

private
let close_term_n (bs : list binder) (t : term) : list R.binder & term =
  let rec aux (bs : list binder) (cbs : list R.binder) (s : subst_t) : list R.binder & subst_t =
    match bs with
    | [] -> cbs, s
    | b::bs ->
      let b = subst_binder_sort s b in
      let nv = r_binder_to_namedv b in
      let b = close_binder b in
      aux bs (b::cbs) (NM nv 0 :: shift_subst 1 s)
  in
  let cbs, s = aux bs [] [] in
  List.Tot.rev cbs, subst_term s t

private
let rec open_term_n_simple (bs : list R.simple_binder) (t : term) : Tac (list simple_binder & term) =
  match bs with
  | [] -> ([], t)
  | b::bs ->
    let bs', t' = open_term_n_simple bs t in
    let b', t'' = open_term_simple b t' in
    (b'::bs', t'')

private
let rec close_term_n_simple (bs : list simple_binder) (t : term) : list R.simple_binder & term =
  match bs with
  | [] -> ([], t)
  | b::bs ->
    let bs', t' = close_term_n_simple bs t in
    let b', t'' = close_term_simple b t' in
    (b'::bs', t'')

private
val open_pat (p: R.pattern) (s: subst_t) : Tac (pattern & subst_t)
p: FStar.Reflection.V2.Data.pattern -> s: FStar.Stubs.Syntax.Syntax.subst_t
  -> FStar.Tactics.Effect.Tac (FStar.Tactics.NamedView.pattern * FStar.Stubs.Syntax.Syntax.subst_t)