val max (bs: list (var & typ)) (current: var)
    : v: var{current <= v /\ (forall (b: var & typ). List.Tot.memP b bs ==> fst b <= v)}
let rec max (bs:list (var & typ)) (current:var)
  : v:var { current <= v /\ (forall (b:var & typ). List.Tot.memP b bs ==> fst b <= v) } =
  match bs with
  | [] -> current
  | (x, t)::rest ->
    let current = if x < current then current else x in
    max rest current
val max (bs: list (var & typ)) (current: var)
    : v: var{current <= v /\ (forall (b: var & typ). List.Tot.memP b bs ==> fst b <= v)}
let rec max (bs: list (var & typ)) (current: var)
    : v: var{current <= v /\ (forall (b: var & typ). List.Tot.memP b bs ==> fst b <= v)} =
match bs with
| [] -> current
| (x, t) :: rest ->
  let current = if x < current then current else x in
  max rest current
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
Prims.list FStar.Pervasives.Native.tuple2 Pulse.Syntax.Base.var Pulse.Syntax.Base.typ Pulse.Typing.Env.max Prims.l_or Prims.precedes Prims.l_and Prims.op_Equals_Equals_Equals Prims.op_LessThan Prims.bool Prims.b2t Prims.op_LessThanOrEqual Prims.l_Forall Prims.l_imp FStar.List.Tot.Base.memP FStar.Pervasives.Native.fst
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)

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 }

let push_binding_bs _ _ _ _ = ()

let push_binding_as_map _ _ _ _ = ()

let rec max (bs:list (var & typ)) (current:var)
val max (bs: list (var & typ)) (current: var)
    : v: var{current <= v /\ (forall (b: var & typ). List.Tot.memP b bs ==> fst b <= v)}
bs: Prims.list (Pulse.Syntax.Base.var * Pulse.Syntax.Base.typ) -> current: Pulse.Syntax.Base.var
  -> v:
    Pulse.Syntax.Base.var
      { current <= v /\
        (forall (b: (Pulse.Syntax.Base.var * Pulse.Syntax.Base.typ)).
            FStar.List.Tot.Base.memP b bs ==> FStar.Pervasives.Native.fst b <= v) }