val diff_witness (#a: Type) (l1 l2: list a) (l3: G.erased (list a))
    : Pure (list a) (requires l1 == l2 @ G.reveal l3) (ensures fun w -> w == G.reveal l3)
let rec diff_witness (#a:Type) (l1 l2:list a) (l3:G.erased (list a))
  : Pure (list a)
         (requires l1 == l2 @ G.reveal l3)
         (ensures fun w -> w == G.reveal l3) =
  match l1, l2 with
  | [], _ -> []
  | _, [] -> l1
  | hd1::tl1, hd2::tl2 ->
    diff_witness tl1 tl2 l3
val diff_witness (#a: Type) (l1 l2: list a) (l3: G.erased (list a))
    : Pure (list a) (requires l1 == l2 @ G.reveal l3) (ensures fun w -> w == G.reveal l3)
let rec diff_witness (#a: Type) (l1 l2: list a) (l3: G.erased (list a))
    : Pure (list a) (requires l1 == l2 @ G.reveal l3) (ensures fun w -> w == G.reveal l3) =
match l1, l2 with
| [], _ -> []
| _, [] -> l1
| hd1 :: tl1, hd2 :: tl2 -> diff_witness tl1 tl2 l3
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.Ghost.erased FStar.Pervasives.Native.Mktuple2 Prims.Nil Pulse.Typing.Env.diff_witness Prims.eq2 FStar.List.Tot.Base.op_At FStar.Ghost.reveal
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)
  : 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

let fresh g =
  match g.bs with
  | [] -> 1
  | (x, _)::bs_rest ->
    let max = max bs_rest x in
    max + 1

//
// TODO: Move to ulib
//
let rec append_memP (#a:Type) (l1 l2:list a) (x:a)
  : Lemma (L.memP x (l1 @ l2) <==> (L.memP x l1 \/ L.memP x l2))
          [SMTPat (L.memP x (l1 @ l2))] =
  match l1 with
  | [] -> ()
  | _::tl -> append_memP tl l2 x

let push_env (g1:env) (g2:env { disjoint g1 g2 }) : env =
  { f = g1.f; bs = g2.bs @ g1.bs; names= g2.names @ g1.names;
    m = Map.concat g2.m g1.m; ctxt = g1.ctxt }

let push_env_fstar_env _ _ = ()

let push_env_bindings _ _ = ()

let push_env_as_map _ _ = ()

let push_env_assoc g1 g2 g3 =
  L.append_assoc g3.bs g2.bs g1.bs;
  assert (equal (push_env g1 (push_env g2 g3)) (push_env (push_env g1 g2) g3))

let check_disjoint g s =
  admit ();
  not (L.existsb (fun (x, _) -> Set.mem x s) g.bs)

let rec remove_binding_aux (g:env)
  (prefix:list (var & typ))
  (prefix_names:list ppname { List.length prefix == List.length prefix_names})
  (suffix:list (var & typ) { Cons? suffix })
  (suffix_names:list ppname { List.length suffix == List.length suffix_names })
  : Pure (var & typ & env)
         (requires bindings g == prefix @ suffix /\
                   g.names == prefix_names @ suffix_names)
         (ensures fun r ->
            let x, t, g' = r in
            fstar_env g' == fstar_env g /\
            (~ (x `Set.mem` dom g')) /\
            g == push_env (push_binding (mk_env (fstar_env g)) x ppname_default t) g')
         (decreases List.Tot.length suffix) =
  match suffix, suffix_names with
  | [x, t], _ ->
    let m = Map.restrict (Set.complement (Set.singleton x)) (Map.upd g.m x tm_unknown) in
    // we need uniqueness invariant in the representation
    assume (forall (b:var & typ). List.Tot.memP b prefix <==> (List.Tot.memP b g.bs /\
                                                               fst b =!= x));
    let g' = {g with bs = prefix; names=prefix_names; m} in
    assert (equal g (push_env (push_binding (mk_env (fstar_env g)) x ppname_default t) g'));
    x, t, g'
  | (x, t)::suffix_rest, n::suffix_names_rest ->
    assume (prefix @ suffix == (prefix @ [x,t]) @ suffix_rest);
    assume (prefix_names @ suffix_names == (prefix_names @ [n]) @ suffix_names_rest);
    remove_binding_aux g (prefix @ [x, t]) (prefix_names @ [n]) suffix_rest suffix_names_rest

let remove_binding g =
  remove_binding_aux g [] [] g.bs g.names

let remove_latest_binding g =
  match g.bs with
  | (x, t)::rest ->
    let m = Map.restrict (Set.complement (Set.singleton x)) (Map.upd g.m x tm_unknown) in
    // we need uniqueness invariant in the representation
    assume (forall (b:var & typ). List.Tot.memP b rest <==> (List.Tot.memP b g.bs /\
                                                             fst b =!= x));
    let g' = {g with bs = rest; names=L.tl g.names; m} in
    assert (equal g (push_binding g' x ppname_default t));
    x, t, g'    

let intro_env_extends (g1 g2 g3:env)
  : Lemma (requires extends_with g1 g2 g3)
          (ensures g1 `env_extends` g2) = ()

let elim_env_extends (g1:env) (g2:env { g1 `env_extends` g2 })
  : GTot (g3:env { extends_with g1 g2 g3 }) =
  FStar.IndefiniteDescription.indefinite_description_ghost
    env (fun g3 -> extends_with g1 g2 g3)

let elim_env_extends_tot (g1:env) (g2:env { g1 `env_extends` g2 })
  : g3:G.erased env { extends_with g1 g2 (Ghost.reveal g3)  }
  = G.hide (elim_env_extends g1 g2)

let rec diff_witness (#a:Type) (l1 l2:list a) (l3:G.erased (list a))
  : Pure (list a)
         (requires l1 == l2 @ G.reveal l3)
val diff_witness (#a: Type) (l1 l2: list a) (l3: G.erased (list a))
    : Pure (list a) (requires l1 == l2 @ G.reveal l3) (ensures fun w -> w == G.reveal l3)
l1: Prims.list a -> l2: Prims.list a -> l3: FStar.Ghost.erased (Prims.list a)
  -> Prims.Pure (Prims.list a)