val default_context:Pulse.RuntimeUtils.context
let default_context : Pulse.RuntimeUtils.context = FStar.Sealed.seal []
val default_context:Pulse.RuntimeUtils.context
let default_context:Pulse.RuntimeUtils.context =
FStar.Sealed.seal []
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.Sealed.seal Prims.list FStar.Pervasives.Native.tuple2 Prims.string FStar.Pervasives.Native.option FStar.Range.range Prims.Nil
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)
val default_context:Pulse.RuntimeUtils.context
Pulse.RuntimeUtils.context