val push_binding (g:env) (x:var { ~ (Set.mem x (dom g)) }) (n:ppname) (t:typ)
  : g':env { fstar_env g' == fstar_env g }
let push_binding g x p t =
  { g with bs = (x, t)::g.bs;
           names = p::g.names;
           m = Map.upd g.m x t }
val push_binding (g:env) (x:var { ~ (Set.mem x (dom g)) }) (n:ppname) (t:typ)
  : g':env { fstar_env g' == fstar_env g }
let push_binding g x p t =
{ g with bs = (x, t) :: g.bs; names = p :: g.names; m = Map.upd g.m x t }
Pulse.Typing.Env.fst.checked
Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Config.fsti.checked prims.fst.checked FStar.Stubs.Pprint.fsti.checked FStar.String.fsti.checked FStar.Set.fsti.checked FStar.Sealed.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Reflection.fst.checked FStar.Range.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Issue.fsti.checked FStar.IndefiniteDescription.fsti.checked FStar.Ghost.fsti.checked
Pulse.Typing.Env.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.var Prims.l_not Prims.b2t FStar.Set.mem Pulse.Typing.Env.dom Pulse.Syntax.Base.ppname Pulse.Syntax.Base.typ Pulse.Typing.Env.Mkenv Pulse.Typing.Env.__proj__Mkenv__item__f Prims.Cons FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 Pulse.Typing.Env.__proj__Mkenv__item__bs Pulse.Typing.Env.__proj__Mkenv__item__names FStar.Map.upd Pulse.Typing.Env.__proj__Mkenv__item__m Pulse.Typing.Env.__proj__Mkenv__item__ctxt Prims.eq2 FStar.Reflection.Typing.fstar_top_env Pulse.Typing.Env.fstar_env
module Pulse.Typing.Env

open Pulse.Syntax

module G = FStar.Ghost
module L = FStar.List.Tot

module R = FStar.Reflection
module RT = FStar.Reflection.Typing
module RU = Pulse.RuntimeUtils
open FStar.List.Tot

type bmap = m:Map.t var typ {
  forall (x:var). (~ (Map.contains m x)) ==> (Map.sel m x == tm_unknown)
}

let related (bs:list (var & typ)) (m:Map.t var typ) =
  (forall (b:var & typ).
          L.memP b bs ==> (Map.contains m (fst b) /\
                           Map.sel m (fst b) == snd b)) /\
  
  (forall (x:var). Map.contains m x ==> (List.Tot.memP (x, Map.sel m x) bs))

noeq
type env = {
  f : RT.fstar_top_env;
  bs : list (var & typ);
  names : list ppname;
  m : m:bmap { related bs m /\ L.length names == L.length bs };
  ctxt: Pulse.RuntimeUtils.context
}

let fstar_env g = RU.env_set_context g.f g.ctxt

let bindings g = g.bs

let as_map g = g.m

let bindings_as_map _ = ()

let empty_bmap : bmap = Map.const_on Set.empty tm_unknown

let rec equal_names (l1 l2:list ppname)
  : Lemma 
    (requires L.length l1 == L.length l2)
    (ensures l1 == l2) =
  match l1, l2 with
  | [], [] -> ()
  | n1::l1, n2::l2 ->
    equal_names l1 l2

let equal_elim g1 g2 =
  equal_names g1.names g2.names;
  assert (Map.equal g1.m g2.m)

let default_context : Pulse.RuntimeUtils.context = FStar.Sealed.seal []

let mk_env (f:RT.fstar_top_env) : env =
  { f; bs = []; names=[]; m = empty_bmap; ctxt = default_context }

let mk_env_bs _ = ()

let mk_env_dom _ = assert (Set.equal (Map.domain empty_bmap) Set.empty)
val push_binding (g:env) (x:var { ~ (Set.mem x (dom g)) }) (n:ppname) (t:typ)
  : g':env { fstar_env g' == fstar_env g }

    g: Pulse.Typing.Env.env ->
    x: Pulse.Syntax.Base.var{~(FStar.Set.mem x (Pulse.Typing.Env.dom g))} ->
    n: Pulse.Syntax.Base.ppname ->
    t: Pulse.Syntax.Base.typ
  -> g': Pulse.Typing.Env.env{Pulse.Typing.Env.fstar_env g' == Pulse.Typing.Env.fstar_env g}