val mk_env (f:RT.fstar_top_env) : g:env { fstar_env g == f }
let mk_env (f:RT.fstar_top_env) : env =
  { f; bs = []; names=[]; m = empty_bmap; ctxt = default_context }
val mk_env (f:RT.fstar_top_env) : g:env { fstar_env g == f }
let mk_env (f: RT.fstar_top_env) : env =
{ f = f; bs = []; names = []; m = empty_bmap; ctxt = default_context }
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
FStar.Reflection.Typing.fstar_top_env Pulse.Typing.Env.Mkenv Prims.Nil FStar.Pervasives.Native.tuple2 Pulse.Syntax.Base.var Pulse.Syntax.Base.typ Pulse.Syntax.Base.ppname Pulse.Typing.Env.empty_bmap Pulse.Typing.Env.default_context Pulse.Typing.Env.env Prims.eq2 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 []
val mk_env (f:RT.fstar_top_env) : g:env { fstar_env g == f }
f: FStar.Reflection.Typing.fstar_top_env
  -> g: Pulse.Typing.Env.env{Pulse.Typing.Env.fstar_env g == f}