val extend_env_alt : g: FStar.Stubs.Reflection.Types.env -> sg: BoolRefinement.src_env
  -> FStar.Stubs.Reflection.Types.env
let extend_env_alt (g:R.env) (sg:src_env) = 
  RT.extend_env_l g (as_bindings sg)
module BoolRefinement
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
module L = FStar.List.Tot
open FStar.List.Tot
#push-options "--z3cliopt 'smt.qi.eager_threshold=100' --z3cliopt 'smt.arith.nl=false'"

let var = nat
let index = nat

let tun = R.pack_ln R.Tv_Unknown

type src_exp =
  | EBVar : index -> src_exp
  | EVar  : var -> src_exp
  | EBool : bool -> src_exp
  | EIf   : src_exp -> src_exp -> src_exp -> src_exp
  | ELam  : src_ty -> src_exp -> src_exp
  | EApp  : src_exp -> src_exp -> src_exp

and src_ty =
  | TBool : src_ty
  | TRefineBool : src_exp -> src_ty
  | TArrow : src_ty -> src_ty -> src_ty

let rec size (e:src_exp)
  : nat
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> 1
    | EIf b e1 e2 -> size b + size e1 + size e2 + 1
    | ELam _ e -> 1 + size e
    | EApp e1 e2 -> 1 + size e1 + size e2

let rec freevars (e:src_exp) 
  : FStar.Set.set var
  = match e with
    | EVar v -> Set.singleton v
    | EBool _
    | EBVar _ -> Set.empty
    | EIf b e1 e2 -> Set.union (freevars b) (Set.union (freevars e1) (freevars e2))
    | ELam t e -> Set.union (freevars_ty t) (freevars e)
    | EApp e1 e2 -> Set.union (freevars e1) (freevars e2)
and freevars_ty (t:src_ty)
  : Set.set var
  = match t with
    | TBool -> Set.empty
    | TArrow t1 t2 -> freevars_ty t1 `Set.union` freevars_ty t2
    | TRefineBool e -> freevars e
  
let rec closed (e:src_exp) 
  : b:bool{ b <==> freevars e `Set.equal` Set.empty }
  = match e with
    | EVar v -> 
      assert (v `Set.mem` freevars e);
      false
    | EBool _
    | EBVar _ -> true
    | EIf b e1 e2 -> closed b && closed e1 && closed e2
    | ELam t e -> closed_ty t && closed e
    | EApp e1 e2 -> closed e1 && closed e2
and closed_ty (t:src_ty)
  : b:bool{ b <==> freevars_ty t `Set.equal` Set.empty }
  = match t with
    | TBool -> true
    | TRefineBool e -> closed e
    | TArrow t1 t2 -> closed_ty t1 && closed_ty t2
  
let rec ln' (e:src_exp) (n:int)
  : bool
  = match e with
    | EBool _
    | EVar _ -> true
    | EBVar m -> m <= n
    | EIf b e1 e2 -> ln' b n && ln' e1 n && ln' e2 n
    | ELam t e -> ln_ty t && ln' e (n + 1)
    | EApp e1 e2 -> ln' e1 n && ln' e2 n
and ln_ty (e:src_ty)
  : b:bool{ b ==> closed_ty e }
  = match e with
    | TBool -> true
    | TRefineBool e -> ln' e (- 1) && closed e
    | TArrow t1 t2 -> ln_ty t1 && ln_ty t2

let rec ln_weaker (e:src_exp) (n:int) (m:int{n <= m})
  : Lemma 
    (requires ln' e n)
    (ensures ln' e m)
  = match e with
    | EBool _
    | EVar _
    | EBVar _ -> ()
    | EIf b e1 e2 -> 
      ln_weaker b n m;
      ln_weaker e1 n m;
      ln_weaker e2 n m
    | ELam t e ->
      ln_weaker e (n + 1) (m + 1)
    | EApp e1 e2 ->
      ln_weaker e1 n m;
      ln_weaker e2 n m    

let ln e = ln' e (-1)

let rec open_exp' (e:src_exp) (v:var) (n:index)
  : e':src_exp { size e == size e'}
    = match e with
    | EBool _ -> e
    | EVar m -> EVar m
    | EBVar m -> if m = n then EVar v else EBVar m
    | EIf b e1 e2 -> EIf (open_exp' b v n) (open_exp' e1 v n) (open_exp' e2 v n)
    | ELam t e -> ELam t (open_exp' e v (n + 1))
    | EApp e1 e2 -> EApp (open_exp' e1 v n) (open_exp' e2 v n)

let rec close_exp' (e:src_exp) (v:var) (n:nat)
  : e':src_exp { size e == size e'}
  = match e with
    | EBool _ -> e
    | EVar m -> if m = v then EBVar n else EVar m
    | EBVar m -> EBVar m
    | EIf b e1 e2 -> EIf (close_exp' b v n) (close_exp' e1 v n) (close_exp' e2 v n)
    | ELam t e -> ELam t (close_exp' e v (n + 1))
    | EApp e1 e2 -> EApp (close_exp' e1 v n) (close_exp' e2 v n)

let open_exp e v = open_exp' e v 0
let close_exp e v = close_exp' e v 0

let rec open_close' (e:src_exp) (x:var) (n:nat { ln' e (n - 1) })
  : Lemma (open_exp' (close_exp' e x n) x n == e)
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar m -> ()
    | EIf b e1 e2 -> 
      open_close' b x n;
      open_close' e1 x n;
      open_close' e2 x n
    | ELam _ e -> open_close' e x (n + 1)
    | EApp e1 e2 -> 
      open_close' e1 x n; 
      open_close' e2 x n

let open_close (e:src_exp) (x:var)
  : Lemma 
    (requires ln e)
    (ensures open_exp (close_exp e x) x == e)
    [SMTPat (open_exp (close_exp e x) x)]
  = open_close' e x 0

let rec open_exp_ln (e:src_exp) (v:var) (n:index) (m:int)
  : Lemma 
    (requires ln' e n /\
              m == n - 1)
    (ensures ln' (open_exp' e v n) m)
    [SMTPat (ln' e n);
     SMTPat (ln' (open_exp' e v n) m)]
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar m -> ()
    | EIf b e1 e2 ->
      open_exp_ln b v n m;
      open_exp_ln e1 v n m;
      open_exp_ln e2 v n m
    | ELam _ e -> open_exp_ln e v (n + 1) (m + 1)
    | EApp e1 e2 -> open_exp_ln e1 v n m; open_exp_ln e2 v n m

let rec close_exp_ln (e:src_exp) (v:var) (n:nat)
  : Lemma 
    (requires ln' e (n - 1))
    (ensures ln' (close_exp' e v n) n)
    [SMTPat (ln' (close_exp' e v n) n)]
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar m -> ()
    | EIf b e1 e2 ->
      close_exp_ln b v n;
      close_exp_ln e1 v n;
      close_exp_ln e2 v n
    | ELam _ e -> close_exp_ln e v (n + 1)
    | EApp e1 e2 -> close_exp_ln e1 v n; close_exp_ln e2 v n

#push-options "--z3rlimit 15"
let rec open_exp_freevars (e:src_exp) (v:var) (n:nat)
  : Lemma ((freevars e `Set.subset` freevars (open_exp' e v n))  /\
           (freevars (open_exp' e v n) `Set.subset` (freevars e `Set.union` Set.singleton v)))
          [SMTPat (freevars (open_exp' e v n))]
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> ()
    | EApp e1 e2 ->
      open_exp_freevars e1 v n;
      open_exp_freevars e2 v n
    | EIf b e1 e2 ->
      open_exp_freevars b v n;    
      open_exp_freevars e1 v n;
      open_exp_freevars e2 v n
    | ELam t e ->
      open_exp_freevars e v (n + 1)
#pop-options

let minus (s:Set.set 'a) (x:'a) = Set.intersect s (Set.complement (Set.singleton x))

let rec close_exp_freevars (m:int) (e:src_exp { ln' e m } ) (v:var) (n:nat)
  : Lemma 
    (ensures freevars (close_exp' e v n) `Set.equal`
             (freevars e `minus` v))
    (decreases e)
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> ()
    | EApp e1 e2 ->
      close_exp_freevars m e1 v n;
      close_exp_freevars m e2 v n
    | EIf b e1 e2 ->
      close_exp_freevars m b v n;    
      close_exp_freevars m e1 v n;
      close_exp_freevars m e2 v n
    | ELam t body ->
      close_exp_freevars (m + 1) body v (n + 1)

let s_exp = e:src_exp { ln e }
let src_eqn = s_exp & s_exp

let s_ty = t:src_ty { ln_ty t }
//environment binds types or equations
let src_env = list (var & either s_ty src_eqn) 

let rec lookup (e:list (var & 'a)) (x:var)
  : option 'a
  = match e with
    | [] -> None
    | (y, v) :: tl -> if x = y then Some v else lookup tl x

let rec src_env_ok (s:src_env)
  : bool
  = match s with
    | [] -> true
    | (x, _)::tl -> None? (lookup tl x) && src_env_ok tl

let lookup_ty (e:src_env) (x:var)
  : option src_ty
  = match lookup e x with
    | Some (Inl t) -> Some t
    | _ -> None
    
let max (n1 n2:nat) = if n1 < n2 then n2 else n1

let rec fresh (e:list (var & 'a))
  : var
  = match e with
    | [] -> 0
    | (y, _) :: tl ->  max (fresh tl) y + 1
    | _ :: tl -> fresh tl

let rec fresh_not_mem (e:list (var & 'a)) (elt: (var & 'a))
  : Lemma (ensures L.memP elt e ==> fresh e > fst elt)
  = match e with
    | [] -> ()
    | hd :: tl -> fresh_not_mem tl elt
  
let rec lookup_mem (e:list (var & 'a)) (x:var)
  : Lemma
    (requires Some? (lookup e x))
    (ensures exists elt. L.memP elt e /\ fst elt == x)
  = match e with
    | [] -> ()
    | hd :: tl -> 
      match lookup tl x with
      | None -> assert (L.memP hd e)
      | _ -> 
        lookup_mem tl x;
        eliminate exists elt. L.memP elt tl /\ fst elt == x
        returns _
        with _ . ( 
          introduce exists elt. L.memP elt e /\ fst elt == x
          with elt
          and ()
        )

let fresh_is_fresh (e:src_env)
  : Lemma (None? (lookup e (fresh e)))
  =  match lookup e (fresh e) with
     | None -> ()
     | Some _ ->
       lookup_mem e (fresh e);
       FStar.Classical.forall_intro (fresh_not_mem e)

module RT = FStar.Reflection.Typing

let r_b2t (t:R.term) 
  : R.term 
  = R.(pack_ln (Tv_App (pack_ln (Tv_FVar RT.b2t_fv)) (t, Q_Explicit)))

let rec elab_exp (e:src_exp)
  : Tot R.term
  = let open R in
    match e with
    | EBool true ->
      pack_ln (Tv_Const R.C_True)

    | EBool false ->
      pack_ln (Tv_Const R.C_False)

    | EBVar n -> 
      let bv = R.pack_bv (RT.make_bv n) in
      R.pack_ln (Tv_BVar bv)
      
    | EVar n ->
      let namedv = R.pack_namedv (RT.make_namedv n) in
      R.pack_ln (Tv_Var namedv)

    | ELam t e ->
      let t = elab_ty t in
      let e = elab_exp e in
      R.pack_ln (Tv_Abs (RT.mk_simple_binder RT.pp_name_default t) e)
             
    | EApp e1 e2 ->
      let e1 = elab_exp e1 in
      let e2 = elab_exp e2 in
      R.pack_ln (Tv_App e1 (e2, Q_Explicit))

    | EIf b e1 e2 ->
      let b = elab_exp b in
      let e1 = elab_exp e1 in
      let e2 = elab_exp e2 in
      R.pack_ln (Tv_Match b None [(Pat_Constant C_True, e1); (Pat_Constant C_False, e2)])
      
and elab_ty (t:src_ty) 
  : R.term  
  = let open R in
    match t with
    | TBool -> 
      RT.bool_ty
      
    | TArrow t1 t2 ->
      let t1 = elab_ty t1 in
      let t2 = elab_ty t2 in
      R.pack_ln 
        (R.Tv_Arrow 
          (RT.mk_simple_binder RT.pp_name_default t1)
          (RT.mk_total t2)) //.pack_comp (C_Total t2 u_unk [])))
          
    | TRefineBool e ->
      let e = elab_exp e in
      let b : R.simple_binder = RT.mk_simple_binder RT.pp_name_default RT.bool_ty in
      let bv = R.pack_bv (RT.make_bv 0) in
      let refinement = r_b2t (R.pack_ln (Tv_App e (R.pack_ln (Tv_BVar bv), Q_Explicit))) in
      R.pack_ln (Tv_Refine b refinement)

let elab_eqn (e1 e2:src_exp)
  : R.term
  = RT.eq2 RT.u_zero RT.bool_ty (elab_exp e1) (elab_exp e2)

let binding = either s_ty src_eqn
let elab_binding (b:binding)
  : R.term 
  = match b with
    | Inl t -> elab_ty t
    | Inr (e1, e2) -> elab_eqn e1 e2
    
let extend_env_l (g:R.env) (sg:src_env) = 
  L.fold_right 
    (fun (x, b) g ->  RT.extend_env g x (elab_binding b))
     sg
     g

let as_bindings (sg:src_env) 
  : RT.bindings
  = L.map (fun (x, b) -> x, elab_binding b) sg
/
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Stubs.Tactics.V2.Builtins.fsti.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
BoolRefinement.fst
g: FStar.Stubs.Reflection.Types.env -> sg: BoolRefinement.src_env
  -> FStar.Stubs.Reflection.Types.env
FStar.Stubs.Reflection.Types.env BoolRefinement.src_env FStar.Reflection.Typing.extend_env_l BoolRefinement.as_bindings
let extend_env_alt (g: R.env) (sg: src_env) =
  
RT.extend_env_l g (as_bindings sg)