<commit_before>(*
   Copyright 2008-2014 <NAME> and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
#light "off"
// (c) Microsoft Corporation. All rights reserved

module FStar.TypeChecker.Util
open FStar.ST
open FStar.Exn
open FStar.All
open FStar
open FStar.Util
open FStar.Errors
open FStar.TypeChecker
open FStar.Syntax
open FStar.TypeChecker.Env
open FStar.TypeChecker.Rel
open FStar.Syntax.Syntax
open FStar.Ident
open FStar.Syntax.Subst
open FStar.TypeChecker.Common

type lcomp_with_binder = option<bv> * lcomp



module SS = FStar.Syntax.Subst
module S = FStar.Syntax.Syntax
module BU = FStar.Util
module U = FStar.Syntax.Util
module N = FStar.TypeChecker.Normalize
module P = FStar.Syntax.Print
module C = FStar.Parser.Const

//Reporting errors
let report env errs =
    Errors.err (Env.get_range env)
               (Err.failed_to_prove_specification errs)

(************************************************************************)
(* Unification variables *)
(************************************************************************)
let is_type t = match (compress t).n with
    | Tm_type _ -> true
    | _ -> false

let t_binders env =
    Env.all_binders env |> List.filter (fun (x, _) -> is_type x.sort)

//new unification variable
let new_uvar_aux env k =
    let bs = if (Options.full_context_dependency())
             || Ident.lid_equals C.prims_lid (Env.current_module env)
             then Env.all_binders env
             else t_binders env in
    Rel.new_uvar (Env.get_range env) bs k

let new_uvar env k = fst (new_uvar_aux env k)

let as_uvar : typ -> uvar = function
    | {n=Tm_uvar(uv, _)} -> uv
    | _ -> failwith "Impossible"

let new_implicit_var reason r env k =
    match U.destruct k C.range_of_lid with
     | Some [_; (tm, _)] ->
       let t = S.mk (S.Tm_constant (FStar.Const.Const_range tm.pos)) None tm.pos in
       t, [], Rel.trivial_guard

     | _ ->
       let t, u = new_uvar_aux env k in
       let g = {Rel.trivial_guard with implicits=[(reason, env, as_uvar u, t, k, r)]} in
       t, [(as_uvar u, r)], g

let check_uvars r t =
  let uvs = Free.uvars t in
  if not (BU.set_is_empty uvs)
  then
    let us = List.map (fun (x, _) -> Print.uvar_to_string x) (BU.set_elements uvs) |> String.concat ", " in
    (* ignoring the hide_uvar_nums and print_implicits flags here *)
    Options.push();
    Options.set_option "hide_uvar_nums" (Options.Bool false);
    Options.set_option "print_implicits" (Options.Bool true);
    Errors.err r
      (BU.format2 "Unconstrained unification variables %s in type signature %s; \
       please add an annotation" us (Print.term_to_string t));
    Options.pop()

(************************************************************************)
(* Extracting annotations from a term *)
(************************************************************************)
//let force_sort' s = match !s.tk with
//    | None -> failwith (BU.format2 "(%s) Impossible: Forced tk not present on %s" (Range.string_of_range s.pos) (Print.term_to_string s))
//    | Some tk -> tk
//
//let force_sort s = mk (force_sort' s) None s.pos

let extract_let_rec_annotation env {lbname=lbname; lbunivs=univ_vars; lbtyp=t; lbdef=e} :
    list<univ_name>
   * typ
   * bool //true indicates that the type needs to be checked; false indicates that it is already checked
   =
  let rng = S.range_of_lbname lbname in
  let t = SS.compress t in
  match t.n with
   | Tm_unknown ->
     if univ_vars <> [] then failwith "Impossible: non-empty universe variables but the type is unknown";
     let r = Env.get_range env in
     let mk_binder scope a =
        match (SS.compress a.sort).n with
        | Tm_unknown ->
          let k, _ = U.type_u() in
          let t =  Rel.new_uvar e.pos scope k |> fst in
          {a with sort=t}, false
        | _ -> a, true in

    let rec aux must_check_ty vars e : either<typ,comp> * bool =
      let e = SS.compress e in
      match e.n with
      | Tm_meta(e, _) -> aux must_check_ty vars e
      | Tm_ascribed(e, t, _) -> fst t, true

      | Tm_abs(bs, body, _) ->
        let scope, bs, must_check_ty = bs |> List.fold_left (fun (scope, bs, must_check_ty) (a, imp) ->
              let tb, must_check_ty =
                if must_check_ty
                then a, true
                else mk_binder scope a in
              let b = (tb, imp) in
              let bs = bs@[b] in
              let scope = scope@[b] in
              scope, bs, must_check_ty)
           (vars,[], must_check_ty) in

        let res, must_check_ty = aux must_check_ty scope body in
        let c = match res with
            | Inl t ->
              if Options.ml_ish()
              then U.ml_comp t r
              else S.mk_Total t //let rec without annotations default to Tot, except if --MLish
            | Inr c -> c in
        let t = U.arrow bs c in
        if debug env Options.High
        then BU.print3 "(%s) Using type %s .... must check = %s\n"
                (Range.string_of_range r) (Print.term_to_string t) (BU.string_of_bool must_check_ty);
        Inl t, must_check_ty

      | _ ->
        if must_check_ty
        then Inl S.tun, true
        else Inl (Rel.new_uvar r vars U.ktype0 |> fst), false
    in

    let t, b = aux false (t_binders env) e in
    let t =
       match t with
       | Inr c ->
             if U.is_tot_or_gtot_comp c
             then U.comp_result c
             else raise (Error(BU.format1 "Expected a 'let rec' to be annotated with a value type; got a computation type %s"
                                                        (Print.comp_to_string c),
                           rng))
       | Inl t -> t in
    [], t, b

  | _ ->
    let univ_vars, t = open_univ_vars univ_vars t in
    univ_vars, t, false

(************************************************************************)
(* Utilities on patterns  *)
(************************************************************************)

(*
  pat_as_exps allow_implicits env p:
    Turns a pattern p into a triple:
*)
let pat_as_exp (allow_implicits:bool)
               (env:Env.env)
               (p:pat)
               (tc_annot : Env.env -> term -> term * guard_t)
    : (list<bv>          (* pattern-bound variables (which may appear in the branch of match) *)
     * term              (* expressions corresponding to the pattern *)
     * guard_t           (* guard for the annotations on the pattern bound variables *)  //AR: earlier tc_annot was forcing it to be trivial without assuming the equality of the scrutinee with the pattern
                                                                                         //see the comment in tc_pat in TcTerm.fs
     * pat)   =          (* decorated pattern, with all the missing implicit args in p filled in *)
    let check_bv (env:Env.env) (x:bv) :(bv * guard_t) =
          let t_x, guard =
              match (SS.compress x.sort) with
              | {n=Tm_unknown} ->
                let t, _ = U.type_u() in
                new_uvar env t, Rel.trivial_guard
              | t -> //user-decorated type
                tc_annot env t
          in
          {x with sort=t_x}, guard
    in
    let rec pat_as_arg_with_env allow_wc_dependence env (p:pat) :
                                    (list<bv>    //all pattern-bound vars including wild-cards, in proper order
                                    * list<bv>   //just the accessible vars, for the disjunctive pattern test
                                    * list<bv>   //just the wildcards
                                    * Env.env    //env extending with the pattern-bound variables
                                    * term       //the pattern as a term/typ
                                    * guard_t    //guard for the type annotations on the pattern bvs
                                    * pat) =     //the elaborated pattern itself
        match p.v with
           | Pat_constant c ->
             let e =
                match c with
                | FStar.Const.Const_int(repr, Some sw) ->
                  FStar.ToSyntax.ToSyntax.desugar_machine_integer env.dsenv repr sw p.p
                | _ ->
                  mk (Tm_constant c) None p.p
             in
             ([], [], [], env, e, Rel.trivial_guard, p)

           | Pat_dot_term(x, _) ->
             let k, _ = U.type_u () in
             let t = new_uvar env k in
             let x = {x with sort=t} in
             let e, u = Rel.new_uvar p.p (Env.all_binders env) t in
             let p = {p with v=Pat_dot_term(x, e)} in
             ([], [], [], env, e, Rel.trivial_guard, p)

           | Pat_wild x ->
             let x, g = check_bv env x in
             let env = if allow_wc_dependence then Env.push_bv env x else env in
             let e = mk (Tm_name x) None p.p in
             ([x], [], [x], env, e, g, p)

           | Pat_var x ->
             let x, g = check_bv env x in
             let env = Env.push_bv env x in
             let e = mk (Tm_name x) None p.p in
             ([x], [x], [], env, e, g, p)

           | Pat_cons(fv, pats) ->
             let (b, a, w, env, args, guard, pats) =
               pats |>
               List.fold_left
                 (fun (b, a, w, env, args, guard, pats) (p, imp) ->
                    let (b', a', w', env, te, guard', pat) = pat_as_arg_with_env allow_wc_dependence env p in
                    let arg = if imp then iarg te else as_arg te in
                    (b'::b, a'::a, w'::w, env, arg::args, Rel.conj_guard guard guard', (pat, imp)::pats))
               ([], [], [], env, [], Rel.trivial_guard, [])
             in
             let e = mk (Tm_meta(mk_Tm_app (Syntax.fv_to_tm fv)
                                           (args |> List.rev) None p.p,
                                 Meta_desugared Data_app))
                     None
                     p.p in
             (List.rev b |> List.flatten,
              List.rev a |> List.flatten,
              List.rev w |> List.flatten,
              env,
              e,
              guard,
              {p with v=Pat_cons(fv, List.rev pats)})
    in

    let rec elaborate_pat env p = //Adds missing implicit patterns to constructor patterns
        let maybe_dot inaccessible a r =
            if allow_implicits && inaccessible
            then withinfo (Pat_dot_term(a, tun)) r
            else withinfo (Pat_var a) r
        in
        match p.v with
        | Pat_cons(fv, pats) ->
          let pats = List.map (fun (p, imp) -> elaborate_pat env p, imp) pats in
          let _, t = Env.lookup_datacon env fv.fv_name.v in
          let f, _ = U.arrow_formals t in
          let rec aux formals pats =
              match formals, pats with
              | [], [] -> []
              | [], _::_ -> raise (Error("Too many pattern arguments", range_of_lid fv.fv_name.v))
              | _::_, [] -> //fill the rest with dot patterns (if allowed), if all the remaining formals are implicit
                formals |>
                List.map (fun (t, imp) ->
                            match imp with
                            | Some (Implicit inaccessible) ->
                            let a = Syntax.new_bv (Some (Syntax.range_of_bv t)) tun in
                            let r = range_of_lid fv.fv_name.v in
                            maybe_dot inaccessible a r, true

                            | _ ->
                              raise (Error(BU.format1 "Insufficient pattern arguments (%s)"
                                                      (Print.pat_to_string p),
                                           range_of_lid fv.fv_name.v)))

              | f::formals', (p, p_imp)::pats' ->
                begin
                match f with
                | (_, Some (Implicit _)) when p_imp ->
                  (p, true)::aux formals' pats'

                | (_, Some (Implicit inaccessible)) ->
                  let a = Syntax.new_bv (Some p.p) tun in
                  let p = maybe_dot inaccessible a (range_of_lid fv.fv_name.v) in
                  (p, true)::aux formals' pats

                | (_, imp) ->
                  (p, S.is_implicit imp)::aux formals' pats'
                end
         in
         {p with v=Pat_cons(fv, aux f pats)}
        | _ -> p in

    let one_pat allow_wc_dependence env p =
        let p = elaborate_pat env p in
        let b, a, w, env, arg, guard, p = pat_as_arg_with_env allow_wc_dependence env p in
        match b |> BU.find_dup bv_eq with
            | Some x -> raise (Error(Err.nonlinear_pattern_variable x, p.p))
            | _ -> b, a, w, arg, guard, p
    in
    let b, _, _, tm, guard, p = one_pat true env p in
    b, tm, guard, p

let decorate_pattern env p exp =
    let qq = p in
    let rec aux p e : pat  =
        let pkg q = withinfo q p.p in
        let e = U.unmeta e in
        match p.v, e.n with
            | _, Tm_uinst(e, _) -> aux p e

            | Pat_constant _, _ ->
              pkg p.v

            | Pat_var x, Tm_name y ->
              if not (bv_eq x y)
              then failwith (BU.format2 "Expected pattern variable %s; got %s" (Print.bv_to_string x) (Print.bv_to_string y));
              if Env.debug env <| Options.Other "Pat"
              then BU.print2 "Pattern variable %s introduced at type %s\n" (Print.bv_to_string x) (Normalize.term_to_string env y.sort);
              let s = Normalize.normalize [Normalize.Beta] env y.sort in
              let x = {x with sort=s} in
              pkg (Pat_var x)

            | Pat_wild x, Tm_name y ->
              if bv_eq x y |> not
              then failwith (BU.format2 "Expected pattern variable %s; got %s" (Print.bv_to_string x) (Print.bv_to_string y));
              let s = Normalize.normalize [Normalize.Beta] env y.sort in
              let x = {x with sort=s} in
              pkg (Pat_wild x)

            | Pat_dot_term(x, _), _ ->
              pkg (Pat_dot_term(x, e))

            | Pat_cons(fv, []), Tm_fvar fv' ->
              if not (Syntax.fv_eq fv fv')
              then failwith (BU.format2 "Expected pattern constructor %s; got %s" fv.fv_name.v.str fv'.fv_name.v.str);
              pkg (Pat_cons(fv', []))

            | Pat_cons(fv, argpats), Tm_app({n=Tm_fvar(fv')}, args)
            | Pat_cons(fv, argpats), Tm_app({n=Tm_uinst({n=Tm_fvar(fv')}, _)}, args) ->

              if fv_eq fv fv' |> not
              then failwith (BU.format2 "Expected pattern constructor %s; got %s" fv.fv_name.v.str fv'.fv_name.v.str);

              let fv = fv' in
              let rec match_args matched_pats args argpats = match args, argpats with
                | [], [] -> pkg (Pat_cons(fv, List.rev matched_pats))
                | arg::args, (argpat, _)::argpats ->
                  begin match arg, argpat.v with
                        | (e, Some (Implicit true)), Pat_dot_term _ ->
                          let x = Syntax.new_bv (Some p.p) S.tun in
                          let q = withinfo (Pat_dot_term(x, e)) p.p in
                          match_args ((q, true)::matched_pats) args argpats

                        | (e, imp), _ ->
                          let pat = aux argpat e, S.is_implicit imp in
                          match_args (pat::matched_pats) args argpats
                 end

                | _ -> failwith (BU.format2 "Unexpected number of pattern arguments: \n\t%s\n\t%s\n" (Print.pat_to_string p) (Print.term_to_string e)) in

              match_args [] args argpats

           | _ ->
            failwith (BU.format3
                            "(%s) Impossible: pattern to decorate is %s; expression is %s\n"
                            (Range.string_of_range qq.p)
                            (Print.pat_to_string qq)
                            (Print.term_to_string exp))
    in
    aux p exp

 let rec decorated_pattern_as_term (pat:pat) : list<bv> * term =
    let mk f : term = mk f None pat.p in

    let pat_as_arg (p, i) =
        let vars, te = decorated_pattern_as_term p in
        vars, (te, as_implicit i) in
    match pat.v with
    | Pat_constant c ->
        [], mk (Tm_constant c)

    | Pat_wild x
    | Pat_var x  ->
        [x], mk (Tm_name x)

    | Pat_cons(fv, pats) ->
        let vars, args = pats |> List.map pat_as_arg |> List.unzip in
        let vars = List.flatten vars in
        vars,  mk (Tm_app(Syntax.fv_to_tm fv, args))

    | Pat_dot_term(x, e) ->
        [], e


(*********************************************************************************************)
(* Utils related to monadic computations *)
(*********************************************************************************************)
let destruct_comp c : (universe * typ * typ) =
  let wp = match c.effect_args with
    | [(wp, _)] -> wp
    | _ -> failwith (BU.format2 "Impossible: Got a computation %s with effect args [%s]" c.effect_name.str
      (List.map (fun (x, _) -> Print.term_to_string x) c.effect_args |> String.concat ", ")) in
  List.hd c.comp_univs, c.result_typ, wp

let lift_comp c m lift =
  let u, _, wp = destruct_comp c in
  {comp_univs=[u];
   effect_name=m;
   result_typ=c.result_typ;
   effect_args=[as_arg (lift.mlift_wp u c.result_typ wp)];
   flags=[]}

let join_effects env l1 l2 =
  let m, _, _ = Env.join env (norm_eff_name env l1) (norm_eff_name env l2) in
  m

let join_lcomp env c1 c2 =
  if U.is_total_lcomp c1
  && U.is_total_lcomp c2
  then C.effect_Tot_lid
  else join_effects env c1.eff_name c2.eff_name

let lift_and_destruct env c1 c2 =
  let c1 = Env.unfold_effect_abbrev env c1 in
  let c2 = Env.unfold_effect_abbrev env c2 in
  let m, lift1, lift2 = Env.join env c1.effect_name c2.effect_name in
  let m1 = lift_comp c1 m lift1 in
  let m2 = lift_comp c2 m lift2 in
  let md = Env.get_effect_decl env m in
  let a, kwp = Env.wp_signature env md.mname in
  (md, a, kwp), destruct_comp m1, destruct_comp m2

let is_pure_effect env l =
  let l = norm_eff_name env l in
  lid_equals l C.effect_PURE_lid

let is_pure_or_ghost_effect env l =
  let l = norm_eff_name env l in
  lid_equals l C.effect_PURE_lid
  || lid_equals l C.effect_GHOST_lid

let mk_comp_l mname u_result result wp flags =
  mk_Comp ({ comp_univs=[u_result];
             effect_name=mname;
             result_typ=result;
             effect_args=[S.as_arg wp];
             flags=flags})

let mk_comp md = mk_comp_l md.mname

let lax_mk_tot_or_comp_l mname u_result result flags =
    if Ident.lid_equals mname C.effect_Tot_lid
    then S.mk_Total' result (Some u_result)
    else mk_comp_l mname u_result result S.tun flags

let subst_lcomp subst lc =
    {lc with res_typ=SS.subst subst lc.res_typ;
             comp=fun () -> SS.subst_comp subst (lc.comp())}

let is_function t = match (compress t).n with
    | Tm_arrow _ -> true
    | _ -> false

let label reason r f : term =
    mk (Tm_meta(f, Meta_labeled(reason, r, false))) None f.pos

let label_opt env reason r f = match reason with
    | None -> f
    | Some reason ->
        if not <| Env.should_verify env
        then f
        else label (reason()) r f

let label_guard r reason (g:guard_t) = match g.guard_f with
    | Trivial -> g
    | NonTrivial f -> {g with guard_f=NonTrivial (label reason r f)}

let close_comp env bvs (c:comp) =
    if U.is_ml_comp c then c
    else if env.lax
    && Options.ml_ish() //NS: disabling this optimization temporarily
    then c
    else begin
            let close_wp u_res md res_t bvs wp0 =
              List.fold_right (fun x wp ->
                  let bs = [mk_binder x] in
                  let us = u_res::[env.universe_of env x.sort] in
                  let wp = U.abs bs wp (Some (U.mk_residual_comp C.effect_Tot_lid None [TOTAL])) in
                  mk_Tm_app (inst_effect_fun_with us env md md.close_wp) [S.as_arg res_t; S.as_arg x.sort; S.as_arg wp] None wp0.pos)
              bvs wp0 in
            let c = Env.unfold_effect_abbrev env c in
            let u_res_t, res_t, wp = destruct_comp c in
            let md = Env.get_effect_decl env c.effect_name in
            let wp = close_wp u_res_t md res_t bvs wp in
            mk_comp md u_res_t c.result_typ wp c.flags
        end

let close_lcomp env bvs (lc:lcomp) =
  let close () = close_comp env bvs (lc.comp()) in
  {lc with comp=close}

let return_value env t v =
  let c =
    if not <| Env.lid_exists env C.effect_GTot_lid //we're still in prims, not yet having fully defined the primitive effects
    then mk_Total t
    else if U.is_unit t
    then S.mk_Total' t (Some U_zero)
    else let m = Env.get_effect_decl env C.effect_PURE_lid in //if Tot isn't fully defined in prims yet, then just return (Total t)
         let u_t = env.universe_of env t in
         let wp =
            if env.lax
            && Options.ml_ish() //NS: Disabling this optimization temporarily
            then S.tun
            else let a, kwp = Env.wp_signature env C.effect_PURE_lid in
                 let k = SS.subst [NT(a, t)] kwp in
                 N.normalize [N.Beta; N.NoFullNorm] env (mk_Tm_app (inst_effect_fun_with [u_t] env m m.ret_wp) [S.as_arg t; S.as_arg v] None v.pos) in
         mk_comp m u_t t wp [RETURN] in
  if debug env <| Options.Other "Return"
  then BU.print3 "(%s) returning %s at comp type %s\n"
                    (Range.string_of_range v.pos)
                    (P.term_to_string v)
                    (N.comp_to_string env c);
  c

let bind r1 env e1opt (lc1:lcomp) ((b, lc2):lcomp_with_binder) : lcomp =
  let lc1 = N.ghost_to_pure_lcomp env lc1 in //downgrade from ghost to pure, if possible
  let lc2 = N.ghost_to_pure_lcomp env lc2 in
  let joined_eff = join_lcomp env lc1 lc2 in
  if debug env Options.Extreme
  || debug env <| Options.Other "bind"
  then
    (let bstr = match b with
      | None -> "none"
      | Some x -> Print.bv_to_string x in
    BU.print4 "Before lift: Making bind (e1=%s)@c1=%s\nb=%s\t\tc2=%s\n"
        (match e1opt with | None -> "None" | Some e -> Print.term_to_string e)
        (Print.lcomp_to_string lc1) bstr (Print.lcomp_to_string lc2));
  let bind_it () =
      if env.lax
      && Options.ml_ish() //NS: disabling this optimization temporarily
      then
         let u_t = env.universe_of env lc2.res_typ in
         lax_mk_tot_or_comp_l joined_eff u_t lc2.res_typ []
      else begin
          let c1 = lc1.comp () in
          let c2 = lc2.comp () in
          if debug env Options.Extreme
          || debug env <| Options.Other "bind"
          then BU.print5 "b=%s,Evaluated %s to %s\n And %s to %s\n"
                (match b with
                  | None -> "none"
                  | Some x -> Print.bv_to_string x)
                (Print.lcomp_to_string lc1)
                (Print.comp_to_string c1)
                (Print.lcomp_to_string lc2)
                (Print.comp_to_string c2);
          let try_simplify () =
            let aux () =
                if U.is_trivial_wp c1
                then match b with
                     | None ->
                       Inl (c2, "trivial no binder")
                     | Some _ ->
                       if U.is_ml_comp c2 //|| not (U.is_free [Inr x] (U.freevars_comp c2))
                       then Inl (c2, "trivial ml")
                       else Inr "c1 trivial; but c2 is not ML"
                else if U.is_ml_comp c1 && U.is_ml_comp c2
                then Inl (c2, "both ml")
                else Inr "c1 not trivial, and both are not ML"
            in
            let subst_c2 reason =
                match e1opt, b with
                | Some e, Some x ->
                  Inl (SS.subst_comp [NT(x,e)] c2, reason)
                | _ -> aux()
            in
            let inline_c1_as_guarded_pure_return () :bool * comp =
              let c1_is_guarded_pure_return () :bool * list<term> =
                let pure_return_p = FStar.Parser.Const.pconst "pure_return" in
                let pure_assert_p = FStar.Parser.Const.pconst "pure_assert_p" in
              
                let rec collect_guards (t:term) (accum:list<term>) :bool * list<term> =
                  match (SS.compress t).n with
                  | Tm_app (head, args) ->
                    (match (SS.compress head).n with
                     | Tm_uinst ({ n = Tm_fvar fv }, _) when fv_eq_lid fv pure_return_p -> true, accum
                     | Tm_uinst ({ n = Tm_fvar fv }, _) when fv_eq_lid fv pure_assert_p ->
                       (match args with
                        | _::p::wp::_ -> collect_guards (fst wp) ((fst p)::accum)
                        | _           -> failwith "Impossible, pure_assert_p should have at least 3 args!")
                     | _ -> false, accum)
                  | _ -> false, accum
                in
                match c1.n with
                | Comp { effect_args = [ (wp, _) ] } -> collect_guards wp []
                | _                                  -> false, []
              in

              let c1_is_guarded, guards = c1_is_guarded_pure_return () in
              if c1_is_guarded && List.length guards > 0 then
                match subst_c2 "c1 is guarded tot" with
                | Inl (c2, _) ->
                  let c2 = Env.unfold_effect_abbrev env c2 in
                  let u_res_t, res_t, wp = destruct_comp c2 in
                  let md = Env.get_effect_decl env c2.effect_name in
                  let wp =
                    List.fold_left (fun wp guard ->
                                    mk_Tm_app (inst_effect_fun_with [u_res_t] env md md.assert_p)
                                              [S.as_arg res_t; S.as_arg <| label_opt env None (Env.get_range env) guard; S.as_arg wp] None wp.pos
                                   ) wp guards in
                  let c2 = mk_comp md u_res_t res_t wp [] in  //AR: dropping the flags?
                  true, c2
                | Inr _  -> false, c2
              else false, c2
            in
            let rec maybe_close t x c =
                match (N.unfold_whnf env t).n with
                | Tm_refine(y, _) ->
                  maybe_close y.sort x c
                | Tm_fvar fv
                    when S.fv_eq_lid fv C.unit_lid ->
                  close_comp env [x] c
                | _ -> c
            in
            if Option.isNone (Env.try_lookup_effect_lid env C.effect_GTot_lid) //if we're very early in prims
            then if U.is_tot_or_gtot_comp c1
                 && U.is_tot_or_gtot_comp c2
                 then Inl (c2, "Early in prims; we don't have bind yet")
                 else raise (Error("Non-trivial pre-conditions very early in prims, even before we have defined the PURE monad", Env.get_range env))
            else if U.is_total_comp c1
                 && U.is_total_comp c2
            then subst_c2 "both total"
            else if U.is_tot_or_gtot_comp c1
                 && U.is_tot_or_gtot_comp c2
            then Inl (S.mk_GTotal (U.comp_result c2), "both gtot")
            else
              let c1_is_guarded_tot, ret_c2 = inline_c1_as_guarded_pure_return () in
              if c1_is_guarded_tot then Inl (ret_c2, "c1 is guarded tot")
              else
                match e1opt, b with
                   | Some e, Some x ->
                     if U.is_total_comp c1
                     && not (Syntax.is_null_bv x)
                     then let c2 = SS.subst_comp [NT(x,e)] c2 in
                          let x = {x with sort = U.comp_result c1} in
                          Inl (maybe_close x.sort x c2, "c1 Tot")
                          //forall (_:t). c2[e/x]
                          //It's important to have that (forall (_:t)) since
                          //if x does not appear free in e,
                          //then it may still be important to know that t is inhabited
                     else aux ()
                   | _ -> aux ()
          in
          match try_simplify () with
          | Inl (c, reason) ->
            if debug env Options.Extreme
            || debug env <| Options.Other "bind"
            then BU.print5 "Simplified (because %s) bind c1: %s\n\nc2: %s\n\nto c: %s\n\nWith effect lid: %s\n\n"
                            reason (Print.comp_to_string c1) (Print.comp_to_string c2) (Print.comp_to_string c) (Print.lid_to_string joined_eff);
            c
          | Inr reason ->
            let (md, a, kwp), (u_t1, t1, wp1), (u_t2, t2, wp2) = lift_and_destruct env c1 c2 in
            let bs =
                match b with
                | None -> [null_binder t1]<commit_msg>inlining pure and ghost wps<commit_after>(*
   Copyright 2008-2014 <NAME> and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
#light "off"
// (c) Microsoft Corporation. All rights reserved

module FStar.TypeChecker.Util
open FStar.ST
open FStar.Exn
open FStar.All
open FStar
open FStar.Util
open FStar.Errors
open FStar.TypeChecker
open FStar.Syntax
open FStar.TypeChecker.Env
open FStar.TypeChecker.Rel
open FStar.Syntax.Syntax
open FStar.Ident
open FStar.Syntax.Subst
open FStar.TypeChecker.Common

type lcomp_with_binder = option<bv> * lcomp



module SS = FStar.Syntax.Subst
module S = FStar.Syntax.Syntax
module BU = FStar.Util
module U = FStar.Syntax.Util
module N = FStar.TypeChecker.Normalize
module P = FStar.Syntax.Print
module C = FStar.Parser.Const

//Reporting errors
let report env errs =
    Errors.err (Env.get_range env)
               (Err.failed_to_prove_specification errs)

(************************************************************************)
(* Unification variables *)
(************************************************************************)
let is_type t = match (compress t).n with
    | Tm_type _ -> true
    | _ -> false

let t_binders env =
    Env.all_binders env |> List.filter (fun (x, _) -> is_type x.sort)

//new unification variable
let new_uvar_aux env k =
    let bs = if (Options.full_context_dependency())
             || Ident.lid_equals C.prims_lid (Env.current_module env)
             then Env.all_binders env
             else t_binders env in
    Rel.new_uvar (Env.get_range env) bs k

let new_uvar env k = fst (new_uvar_aux env k)

let as_uvar : typ -> uvar = function
    | {n=Tm_uvar(uv, _)} -> uv
    | _ -> failwith "Impossible"

let new_implicit_var reason r env k =
    match U.destruct k C.range_of_lid with
     | Some [_; (tm, _)] ->
       let t = S.mk (S.Tm_constant (FStar.Const.Const_range tm.pos)) None tm.pos in
       t, [], Rel.trivial_guard

     | _ ->
       let t, u = new_uvar_aux env k in
       let g = {Rel.trivial_guard with implicits=[(reason, env, as_uvar u, t, k, r)]} in
       t, [(as_uvar u, r)], g

let check_uvars r t =
  let uvs = Free.uvars t in
  if not (BU.set_is_empty uvs)
  then
    let us = List.map (fun (x, _) -> Print.uvar_to_string x) (BU.set_elements uvs) |> String.concat ", " in
    (* ignoring the hide_uvar_nums and print_implicits flags here *)
    Options.push();
    Options.set_option "hide_uvar_nums" (Options.Bool false);
    Options.set_option "print_implicits" (Options.Bool true);
    Errors.err r
      (BU.format2 "Unconstrained unification variables %s in type signature %s; \
       please add an annotation" us (Print.term_to_string t));
    Options.pop()

(************************************************************************)
(* Extracting annotations from a term *)
(************************************************************************)
//let force_sort' s = match !s.tk with
//    | None -> failwith (BU.format2 "(%s) Impossible: Forced tk not present on %s" (Range.string_of_range s.pos) (Print.term_to_string s))
//    | Some tk -> tk
//
//let force_sort s = mk (force_sort' s) None s.pos

let extract_let_rec_annotation env {lbname=lbname; lbunivs=univ_vars; lbtyp=t; lbdef=e} :
    list<univ_name>
   * typ
   * bool //true indicates that the type needs to be checked; false indicates that it is already checked
   =
  let rng = S.range_of_lbname lbname in
  let t = SS.compress t in
  match t.n with
   | Tm_unknown ->
     if univ_vars <> [] then failwith "Impossible: non-empty universe variables but the type is unknown";
     let r = Env.get_range env in
     let mk_binder scope a =
        match (SS.compress a.sort).n with
        | Tm_unknown ->
          let k, _ = U.type_u() in
          let t =  Rel.new_uvar e.pos scope k |> fst in
          {a with sort=t}, false
        | _ -> a, true in

    let rec aux must_check_ty vars e : either<typ,comp> * bool =
      let e = SS.compress e in
      match e.n with
      | Tm_meta(e, _) -> aux must_check_ty vars e
      | Tm_ascribed(e, t, _) -> fst t, true

      | Tm_abs(bs, body, _) ->
        let scope, bs, must_check_ty = bs |> List.fold_left (fun (scope, bs, must_check_ty) (a, imp) ->
              let tb, must_check_ty =
                if must_check_ty
                then a, true
                else mk_binder scope a in
              let b = (tb, imp) in
              let bs = bs@[b] in
              let scope = scope@[b] in
              scope, bs, must_check_ty)
           (vars,[], must_check_ty) in

        let res, must_check_ty = aux must_check_ty scope body in
        let c = match res with
            | Inl t ->
              if Options.ml_ish()
              then U.ml_comp t r
              else S.mk_Total t //let rec without annotations default to Tot, except if --MLish
            | Inr c -> c in
        let t = U.arrow bs c in
        if debug env Options.High
        then BU.print3 "(%s) Using type %s .... must check = %s\n"
                (Range.string_of_range r) (Print.term_to_string t) (BU.string_of_bool must_check_ty);
        Inl t, must_check_ty

      | _ ->
        if must_check_ty
        then Inl S.tun, true
        else Inl (Rel.new_uvar r vars U.ktype0 |> fst), false
    in

    let t, b = aux false (t_binders env) e in
    let t =
       match t with
       | Inr c ->
             if U.is_tot_or_gtot_comp c
             then U.comp_result c
             else raise (Error(BU.format1 "Expected a 'let rec' to be annotated with a value type; got a computation type %s"
                                                        (Print.comp_to_string c),
                           rng))
       | Inl t -> t in
    [], t, b

  | _ ->
    let univ_vars, t = open_univ_vars univ_vars t in
    univ_vars, t, false

(************************************************************************)
(* Utilities on patterns  *)
(************************************************************************)

(*
  pat_as_exps allow_implicits env p:
    Turns a pattern p into a triple:
*)
let pat_as_exp (allow_implicits:bool)
               (env:Env.env)
               (p:pat)
               (tc_annot : Env.env -> term -> term * guard_t)
    : (list<bv>          (* pattern-bound variables (which may appear in the branch of match) *)
     * term              (* expressions corresponding to the pattern *)
     * guard_t           (* guard for the annotations on the pattern bound variables *)  //AR: earlier tc_annot was forcing it to be trivial without assuming the equality of the scrutinee with the pattern
                                                                                         //see the comment in tc_pat in TcTerm.fs
     * pat)   =          (* decorated pattern, with all the missing implicit args in p filled in *)
    let check_bv (env:Env.env) (x:bv) :(bv * guard_t) =
          let t_x, guard =
              match (SS.compress x.sort) with
              | {n=Tm_unknown} ->
                let t, _ = U.type_u() in
                new_uvar env t, Rel.trivial_guard
              | t -> //user-decorated type
                tc_annot env t
          in
          {x with sort=t_x}, guard
    in
    let rec pat_as_arg_with_env allow_wc_dependence env (p:pat) :
                                    (list<bv>    //all pattern-bound vars including wild-cards, in proper order
                                    * list<bv>   //just the accessible vars, for the disjunctive pattern test
                                    * list<bv>   //just the wildcards
                                    * Env.env    //env extending with the pattern-bound variables
                                    * term       //the pattern as a term/typ
                                    * guard_t    //guard for the type annotations on the pattern bvs
                                    * pat) =     //the elaborated pattern itself
        match p.v with
           | Pat_constant c ->
             let e =
                match c with
                | FStar.Const.Const_int(repr, Some sw) ->
                  FStar.ToSyntax.ToSyntax.desugar_machine_integer env.dsenv repr sw p.p
                | _ ->
                  mk (Tm_constant c) None p.p
             in
             ([], [], [], env, e, Rel.trivial_guard, p)

           | Pat_dot_term(x, _) ->
             let k, _ = U.type_u () in
             let t = new_uvar env k in
             let x = {x with sort=t} in
             let e, u = Rel.new_uvar p.p (Env.all_binders env) t in
             let p = {p with v=Pat_dot_term(x, e)} in
             ([], [], [], env, e, Rel.trivial_guard, p)

           | Pat_wild x ->
             let x, g = check_bv env x in
             let env = if allow_wc_dependence then Env.push_bv env x else env in
             let e = mk (Tm_name x) None p.p in
             ([x], [], [x], env, e, g, p)

           | Pat_var x ->
             let x, g = check_bv env x in
             let env = Env.push_bv env x in
             let e = mk (Tm_name x) None p.p in
             ([x], [x], [], env, e, g, p)

           | Pat_cons(fv, pats) ->
             let (b, a, w, env, args, guard, pats) =
               pats |>
               List.fold_left
                 (fun (b, a, w, env, args, guard, pats) (p, imp) ->
                    let (b', a', w', env, te, guard', pat) = pat_as_arg_with_env allow_wc_dependence env p in
                    let arg = if imp then iarg te else as_arg te in
                    (b'::b, a'::a, w'::w, env, arg::args, Rel.conj_guard guard guard', (pat, imp)::pats))
               ([], [], [], env, [], Rel.trivial_guard, [])
             in
             let e = mk (Tm_meta(mk_Tm_app (Syntax.fv_to_tm fv)
                                           (args |> List.rev) None p.p,
                                 Meta_desugared Data_app))
                     None
                     p.p in
             (List.rev b |> List.flatten,
              List.rev a |> List.flatten,
              List.rev w |> List.flatten,
              env,
              e,
              guard,
              {p with v=Pat_cons(fv, List.rev pats)})
    in

    let rec elaborate_pat env p = //Adds missing implicit patterns to constructor patterns
        let maybe_dot inaccessible a r =
            if allow_implicits && inaccessible
            then withinfo (Pat_dot_term(a, tun)) r
            else withinfo (Pat_var a) r
        in
        match p.v with
        | Pat_cons(fv, pats) ->
          let pats = List.map (fun (p, imp) -> elaborate_pat env p, imp) pats in
          let _, t = Env.lookup_datacon env fv.fv_name.v in
          let f, _ = U.arrow_formals t in
          let rec aux formals pats =
              match formals, pats with
              | [], [] -> []
              | [], _::_ -> raise (Error("Too many pattern arguments", range_of_lid fv.fv_name.v))
              | _::_, [] -> //fill the rest with dot patterns (if allowed), if all the remaining formals are implicit
                formals |>
                List.map (fun (t, imp) ->
                            match imp with
                            | Some (Implicit inaccessible) ->
                            let a = Syntax.new_bv (Some (Syntax.range_of_bv t)) tun in
                            let r = range_of_lid fv.fv_name.v in
                            maybe_dot inaccessible a r, true

                            | _ ->
                              raise (Error(BU.format1 "Insufficient pattern arguments (%s)"
                                                      (Print.pat_to_string p),
                                           range_of_lid fv.fv_name.v)))

              | f::formals', (p, p_imp)::pats' ->
                begin
                match f with
                | (_, Some (Implicit _)) when p_imp ->
                  (p, true)::aux formals' pats'

                | (_, Some (Implicit inaccessible)) ->
                  let a = Syntax.new_bv (Some p.p) tun in
                  let p = maybe_dot inaccessible a (range_of_lid fv.fv_name.v) in
                  (p, true)::aux formals' pats

                | (_, imp) ->
                  (p, S.is_implicit imp)::aux formals' pats'
                end
         in
         {p with v=Pat_cons(fv, aux f pats)}
        | _ -> p in

    let one_pat allow_wc_dependence env p =
        let p = elaborate_pat env p in
        let b, a, w, env, arg, guard, p = pat_as_arg_with_env allow_wc_dependence env p in
        match b |> BU.find_dup bv_eq with
            | Some x -> raise (Error(Err.nonlinear_pattern_variable x, p.p))
            | _ -> b, a, w, arg, guard, p
    in
    let b, _, _, tm, guard, p = one_pat true env p in
    b, tm, guard, p

let decorate_pattern env p exp =
    let qq = p in
    let rec aux p e : pat  =
        let pkg q = withinfo q p.p in
        let e = U.unmeta e in
        match p.v, e.n with
            | _, Tm_uinst(e, _) -> aux p e

            | Pat_constant _, _ ->
              pkg p.v

            | Pat_var x, Tm_name y ->
              if not (bv_eq x y)
              then failwith (BU.format2 "Expected pattern variable %s; got %s" (Print.bv_to_string x) (Print.bv_to_string y));
              if Env.debug env <| Options.Other "Pat"
              then BU.print2 "Pattern variable %s introduced at type %s\n" (Print.bv_to_string x) (Normalize.term_to_string env y.sort);
              let s = Normalize.normalize [Normalize.Beta] env y.sort in
              let x = {x with sort=s} in
              pkg (Pat_var x)

            | Pat_wild x, Tm_name y ->
              if bv_eq x y |> not
              then failwith (BU.format2 "Expected pattern variable %s; got %s" (Print.bv_to_string x) (Print.bv_to_string y));
              let s = Normalize.normalize [Normalize.Beta] env y.sort in
              let x = {x with sort=s} in
              pkg (Pat_wild x)

            | Pat_dot_term(x, _), _ ->
              pkg (Pat_dot_term(x, e))

            | Pat_cons(fv, []), Tm_fvar fv' ->
              if not (Syntax.fv_eq fv fv')
              then failwith (BU.format2 "Expected pattern constructor %s; got %s" fv.fv_name.v.str fv'.fv_name.v.str);
              pkg (Pat_cons(fv', []))

            | Pat_cons(fv, argpats), Tm_app({n=Tm_fvar(fv')}, args)
            | Pat_cons(fv, argpats), Tm_app({n=Tm_uinst({n=Tm_fvar(fv')}, _)}, args) ->

              if fv_eq fv fv' |> not
              then failwith (BU.format2 "Expected pattern constructor %s; got %s" fv.fv_name.v.str fv'.fv_name.v.str);

              let fv = fv' in
              let rec match_args matched_pats args argpats = match args, argpats with
                | [], [] -> pkg (Pat_cons(fv, List.rev matched_pats))
                | arg::args, (argpat, _)::argpats ->
                  begin match arg, argpat.v with
                        | (e, Some (Implicit true)), Pat_dot_term _ ->
                          let x = Syntax.new_bv (Some p.p) S.tun in
                          let q = withinfo (Pat_dot_term(x, e)) p.p in
                          match_args ((q, true)::matched_pats) args argpats

                        | (e, imp), _ ->
                          let pat = aux argpat e, S.is_implicit imp in
                          match_args (pat::matched_pats) args argpats
                 end

                | _ -> failwith (BU.format2 "Unexpected number of pattern arguments: \n\t%s\n\t%s\n" (Print.pat_to_string p) (Print.term_to_string e)) in

              match_args [] args argpats

           | _ ->
            failwith (BU.format3
                            "(%s) Impossible: pattern to decorate is %s; expression is %s\n"
                            (Range.string_of_range qq.p)
                            (Print.pat_to_string qq)
                            (Print.term_to_string exp))
    in
    aux p exp

 let rec decorated_pattern_as_term (pat:pat) : list<bv> * term =
    let mk f : term = mk f None pat.p in

    let pat_as_arg (p, i) =
        let vars, te = decorated_pattern_as_term p in
        vars, (te, as_implicit i) in
    match pat.v with
    | Pat_constant c ->
        [], mk (Tm_constant c)

    | Pat_wild x
    | Pat_var x  ->
        [x], mk (Tm_name x)

    | Pat_cons(fv, pats) ->
        let vars, args = pats |> List.map pat_as_arg |> List.unzip in
        let vars = List.flatten vars in
        vars,  mk (Tm_app(Syntax.fv_to_tm fv, args))

    | Pat_dot_term(x, e) ->
        [], e


(*********************************************************************************************)
(* Utils related to monadic computations *)
(*********************************************************************************************)
let destruct_comp c : (universe * typ * typ) =
  let wp = match c.effect_args with
    | [(wp, _)] -> wp
    | _ -> failwith (BU.format2 "Impossible: Got a computation %s with effect args [%s]" c.effect_name.str
      (List.map (fun (x, _) -> Print.term_to_string x) c.effect_args |> String.concat ", ")) in
  List.hd c.comp_univs, c.result_typ, wp

let lift_comp c m lift =
  let u, _, wp = destruct_comp c in
  {comp_univs=[u];
   effect_name=m;
   result_typ=c.result_typ;
   effect_args=[as_arg (lift.mlift_wp u c.result_typ wp)];
   flags=[]}

let join_effects env l1 l2 =
  let m, _, _ = Env.join env (norm_eff_name env l1) (norm_eff_name env l2) in
  m

let join_lcomp env c1 c2 =
  if U.is_total_lcomp c1
  && U.is_total_lcomp c2
  then C.effect_Tot_lid
  else join_effects env c1.eff_name c2.eff_name

let lift_and_destruct env c1 c2 =
  let c1 = Env.unfold_effect_abbrev env c1 in
  let c2 = Env.unfold_effect_abbrev env c2 in
  let m, lift1, lift2 = Env.join env c1.effect_name c2.effect_name in
  let m1 = lift_comp c1 m lift1 in
  let m2 = lift_comp c2 m lift2 in
  let md = Env.get_effect_decl env m in
  let a, kwp = Env.wp_signature env md.mname in
  (md, a, kwp), destruct_comp m1, destruct_comp m2

let is_pure_effect env l =
  let l = norm_eff_name env l in
  lid_equals l C.effect_PURE_lid

let is_pure_or_ghost_effect env l =
  let l = norm_eff_name env l in
  lid_equals l C.effect_PURE_lid
  || lid_equals l C.effect_GHOST_lid

let mk_comp_l mname u_result result wp flags =
  mk_Comp ({ comp_univs=[u_result];
             effect_name=mname;
             result_typ=result;
             effect_args=[S.as_arg wp];
             flags=flags})

let mk_comp md = mk_comp_l md.mname

let lax_mk_tot_or_comp_l mname u_result result flags =
    if Ident.lid_equals mname C.effect_Tot_lid
    then S.mk_Total' result (Some u_result)
    else mk_comp_l mname u_result result S.tun flags

let subst_lcomp subst lc =
    {lc with res_typ=SS.subst subst lc.res_typ;
             comp=fun () -> SS.subst_comp subst (lc.comp())}

let is_function t = match (compress t).n with
    | Tm_arrow _ -> true
    | _ -> false

let label reason r f : term =
    mk (Tm_meta(f, Meta_labeled(reason, r, false))) None f.pos

let label_opt env reason r f = match reason with
    | None -> f
    | Some reason ->
        if not <| Env.should_verify env
        then f
        else label (reason()) r f

let label_guard r reason (g:guard_t) = match g.guard_f with
    | Trivial -> g
    | NonTrivial f -> {g with guard_f=NonTrivial (label reason r f)}

let close_comp env bvs (c:comp) =
    if U.is_ml_comp c then c
    else if env.lax
    && Options.ml_ish() //NS: disabling this optimization temporarily
    then c
    else begin
            let close_wp u_res md res_t bvs wp0 =
              List.fold_right (fun x wp ->
                  let bs = [mk_binder x] in
                  let us = u_res::[env.universe_of env x.sort] in
                  let wp = U.abs bs wp (Some (U.mk_residual_comp C.effect_Tot_lid None [TOTAL])) in
                  mk_Tm_app (inst_effect_fun_with us env md md.close_wp) [S.as_arg res_t; S.as_arg x.sort; S.as_arg wp] None wp0.pos)
              bvs wp0 in
            let c = Env.unfold_effect_abbrev env c in
            let u_res_t, res_t, wp = destruct_comp c in
            let md = Env.get_effect_decl env c.effect_name in
            let wp = close_wp u_res_t md res_t bvs wp in
            mk_comp md u_res_t c.result_typ wp c.flags
        end

let close_lcomp env bvs (lc:lcomp) =
  let close () = close_comp env bvs (lc.comp()) in
  {lc with comp=close}

let return_value env t v =
  let c =
    if not <| Env.lid_exists env C.effect_GTot_lid //we're still in prims, not yet having fully defined the primitive effects
    then mk_Total t
    else if U.is_unit t
    then S.mk_Total' t (Some U_zero)
    else let m = Env.get_effect_decl env C.effect_PURE_lid in //if Tot isn't fully defined in prims yet, then just return (Total t)
         let u_t = env.universe_of env t in
         let wp =
            if env.lax
            && Options.ml_ish() //NS: Disabling this optimization temporarily
            then S.tun
            else let a, kwp = Env.wp_signature env C.effect_PURE_lid in
                 let k = SS.subst [NT(a, t)] kwp in
                 N.normalize [N.Beta; N.NoFullNorm] env (mk_Tm_app (inst_effect_fun_with [u_t] env m m.ret_wp) [S.as_arg t; S.as_arg v] None v.pos) in
         mk_comp m u_t t wp [RETURN] in
  if debug env <| Options.Other "Return"
  then BU.print3 "(%s) returning %s at comp type %s\n"
                    (Range.string_of_range v.pos)
                    (P.term_to_string v)
                    (N.comp_to_string env c);
  c

let bind r1 env e1opt (lc1:lcomp) ((b, lc2):lcomp_with_binder) : lcomp =
  let lc1 = N.ghost_to_pure_lcomp env lc1 in //downgrade from ghost to pure, if possible
  let lc2 = N.ghost_to_pure_lcomp env lc2 in
  let joined_eff = join_lcomp env lc1 lc2 in
  if debug env Options.Extreme
  || debug env <| Options.Other "bind"
  then
    (let bstr = match b with
      | None -> "none"
      | Some x -> Print.bv_to_string x in
    BU.print4 "Before lift: Making bind (e1=%s)@c1=%s\nb=%s\t\tc2=%s\n"
        (match e1opt with | None -> "None" | Some e -> Print.term_to_string e)
        (Print.lcomp_to_string lc1) bstr (Print.lcomp_to_string lc2));
  let bind_it () =
      if env.lax
      && Options.ml_ish() //NS: disabling this optimization temporarily
      then
         let u_t = env.universe_of env lc2.res_typ in
         lax_mk_tot_or_comp_l joined_eff u_t lc2.res_typ []
      else begin
          let c1 = lc1.comp () in
          let c2 = lc2.comp () in
          if debug env Options.Extreme
          || debug env <| Options.Other "bind"
          then BU.print5 "b=%s,Evaluated %s to %s\n And %s to %s\n"
                (match b with
                  | None -> "none"
                  | Some x -> Print.bv_to_string x)
                (Print.lcomp_to_string lc1)
                (Print.comp_to_string c1)
                (Print.lcomp_to_string lc2)
                (Print.comp_to_string c2);
          let aux () =
            if U.is_trivial_wp c1
            then match b with
                 | None ->
                   Inl (c2, "trivial no binder")
                 | Some _ ->
                   if U.is_ml_comp c2 //|| not (U.is_free [Inr x] (U.freevars_comp c2))
                   then Inl (c2, "trivial ml")
                   else Inr "c1 trivial; but c2 is not ML"
            else if U.is_ml_comp c1 && U.is_ml_comp c2
            then Inl (c2, "both ml")
            else Inr "c1 not trivial, and both are not ML"
          in
          let subst_c2 reason =
            match e1opt, b with
            | Some e, Some x ->
                Inl (SS.subst_comp [NT(x,e)] c2, reason)
            | _ -> aux()
          in
          let try_simplify () =
            let rec maybe_close t x c =
                match (N.unfold_whnf env t).n with
                | Tm_refine(y, _) ->
                  maybe_close y.sort x c
                | Tm_fvar fv
                    when S.fv_eq_lid fv C.unit_lid ->
                  close_comp env [x] c
                | _ -> c
            in
            if Option.isNone (Env.try_lookup_effect_lid env C.effect_GTot_lid) //if we're very early in prims
            then if U.is_tot_or_gtot_comp c1
                 && U.is_tot_or_gtot_comp c2
                 then Inl (c2, "Early in prims; we don't have bind yet")
                 else raise (Error("Non-trivial pre-conditions very early in prims, even before we have defined the PURE monad", Env.get_range env))
            else if U.is_total_comp c1
                 && U.is_total_comp c2
            then subst_c2 "both total"
            else if U.is_tot_or_gtot_comp c1
                 && U.is_tot_or_gtot_comp c2
            then Inl (S.mk_GTotal (U.comp_result c2), "both gtot")
            else match e1opt, b with
                   | Some e, Some x ->
                     if U.is_total_comp c1
                     && not (Syntax.is_null_bv x)
                     then let c2 = SS.subst_comp [NT(x,e)] c2 in
                          let x = {x with sort = U.comp_result c1} in
                          Inl (maybe_close x.sort x c2, "c1 Tot")
                          //forall (_:t). c2[e/x]
                          //It's important to have that (forall (_:t)) since
                          //if x does not appear free in e,
                          //then it may still be important to know that t is inhabited
                     else aux ()
                   | _ -> aux ()
          in
          match try_simplify () with
          | Inl (c, reason) ->
            if debug env Options.Extreme
            || debug env <| Options.Other "bind"
            then BU.print5 "Simplified (because %s) bind c1: %s\n\nc2: %s\n\nto c: %s\n\nWith effect lid: %s\n\n"
                            reason (Print.comp_to_string c1) (Print.comp_to_string c2) (Print.comp_to_string c) (Print.lid_to_string joined_eff);
            c
          | Inr reason ->
            //c1 and c2 are the two comps
            let c2 =
              if U.is_pure_or_ghost_comp c1 then
                match subst_c2 "inline all pure" with
                | Inl (c2, _) -> c2
                  //we have inlined
//                  let c2 = Env.unfold_effect_abbrev env c2 in
//                  let u_res_t, res_t, wp = destruct_comp c2 in
//                  let md = Env.get_effect_decl env c2.effect_name in
//                  let wp =
//                    match e1opt, b with
//                    | Some e, Some bv ->
//                      let c1 = Env.unfold_effect_abbrev env c1 in
//                      let u_res_t1, res_t1, _ = destruct_comp c1 in
//                      U.mk_imp (U.mk_eq2 u_res_t1 res_t1 (bv_to_name bv) e) wp
//                    | _, _ -> wp
//                  in
//                  mk_comp md u_res_t res_t wp c2.flags
                | Inr _       -> c2
              else c2
            in
            let (md, a, kwp), (u_t1, t1, wp1), (u_t2, t2, wp2) = lift_and_destruct env c1 c2 in
            let bs =
                match b with
                | None -> [null_binder t1]
{'fraction_non_alphanumeric': 0.11426389900030186, 'fraction_numerical': 0.005504554574995117, 'mean_word_length': 1.6646794416844097, 'pattern_counts': {'":': 0, '<': 41, '<?xml version=': 0, '>': 271, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 64, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2389301', 'n_tokens_mistral': 18483, 'n_tokens_neox': 17820, 'n_words': 5640}