val instantiate_implicits (g: env) (t: st_term{Tm_STApp? t.term})
    : T.Tac (uvs: env & g': env{extends_with g' g uvs} & t': st_term{Tm_STApp? t'.term})
let instantiate_implicits (g:env) (t:st_term { Tm_STApp? t.term })
  : T.Tac (uvs : env &
           g' : env { extends_with g' g uvs } &
           t' : st_term { Tm_STApp? t'.term }) =

  let range = t.range in
  let Tm_STApp { head; arg_qual=qual; arg } = t.term in
  let pure_app = tm_pureapp head qual arg in
  let t, ty = instantiate_term_implicits g pure_app in
  match is_arrow ty with
  | Some (_, Some Implicit, _) ->
    //Some implicits to follow
    intro_uvars_for_logical_implicits g (mk_env (fstar_env g)) t ty
  | _ ->
    match is_pure_app t with
    | Some (head, q, arg) ->
      let uvs = mk_env (fstar_env g) in
      (| uvs, push_env g uvs, {term=Tm_STApp {head;arg_qual=q;arg}; range=t.range; effect_tag=default_effect_hint } |)
    | _ ->
      fail g (Some t.range)
        (Printf.sprintf "check_stapp.instantiate_implicits: expected an application term, found: %s"
           (P.term_to_string t))
val instantiate_implicits (g: env) (t: st_term{Tm_STApp? t.term})
    : T.Tac (uvs: env & g': env{extends_with g' g uvs} & t': st_term{Tm_STApp? t'.term})
let instantiate_implicits (g: env) (t: st_term{Tm_STApp? t.term})
    : T.Tac (uvs: env & g': env{extends_with g' g uvs} & t': st_term{Tm_STApp? t'.term}) =
let range = t.range in
let Tm_STApp { head = head ; arg_qual = qual ; arg = arg } = t.term in
let pure_app = tm_pureapp head qual arg in
let t, ty = instantiate_term_implicits g pure_app in
match is_arrow ty with
| Some (_, Some Implicit, _) -> intro_uvars_for_logical_implicits g (mk_env (fstar_env g)) t ty
| _ ->
  match is_pure_app t with
  | Some (head, q, arg) ->
    let uvs = mk_env (fstar_env g) in
    (|
      uvs,
      push_env g uvs,
      {
        term = Tm_STApp ({ head = head; arg_qual = q; arg = arg });
        range = t.range;
        effect_tag = default_effect_hint
      }
    |)
  | _ ->
    fail g
      (Some t.range)
      (Printf.sprintf "check_stapp.instantiate_implicits: expected an application term, found: %s"
          (P.term_to_string t))
Pulse.Checker.STApp.fst.checked
Pulse.Typing.FV.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.STApp.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.st_term Prims.b2t Pulse.Syntax.Base.uu___is_Tm_STApp Pulse.Syntax.Base.__proj__Mkst_term__item__term Pulse.Syntax.Base.term FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier Pulse.Syntax.Pure.is_arrow Pulse.Syntax.Base.binder Pulse.Syntax.Base.comp Pulse.Checker.STApp.intro_uvars_for_logical_implicits Pulse.Typing.Env.mk_env Pulse.Typing.Env.fstar_env FStar.Pervasives.dtuple3 Pulse.Typing.Env.extends_with FStar.Pervasives.Native.tuple3 Pulse.Syntax.Pure.is_pure_app FStar.Pervasives.Mkdtuple3 Pulse.Typing.Env.push_env Pulse.Syntax.Base.Mkst_term Pulse.Syntax.Base.Tm_STApp Pulse.Syntax.Base.Mkst_term'__Tm_STApp__payload Pulse.Syntax.Base.__proj__Mkterm__item__range Pulse.Syntax.Base.default_effect_hint Prims.eq2 FStar.Reflection.Typing.fstar_top_env Pulse.Typing.Env.fail FStar.Pervasives.Native.Some Pulse.Syntax.Base.range Prims.string FStar.Printf.sprintf Pulse.Syntax.Printer.term_to_string FStar.Pervasives.Native.tuple2 Pulse.Checker.Pure.instantiate_term_implicits Pulse.Syntax.Pure.tm_pureapp Pulse.Syntax.Base.st_term' Pulse.Syntax.Base.__proj__Mkst_term__item__range
module Pulse.Checker.STApp

open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Pure
open Pulse.Checker.Base

module T = FStar.Tactics.V2
module RT = FStar.Reflection.Typing
module FV = Pulse.Typing.FV
module RU = Pulse.RuntimeUtils
module P = Pulse.Syntax.Printer
module Prover = Pulse.Checker.Prover

let debug_log (g:env) (f:unit -> T.Tac unit) : T.Tac unit = if RU.debug_at_level (fstar_env g) "st_app" then f () else ()

let canon_comp (c:comp_st) : comp_st = 
  match readback_comp (elab_comp c) with
  | None -> c
  | Some (C_Tot _) -> c //should be impossible
  | Some c' -> c'

#push-options "--admit_smt_queries true"
let canon_comp_eq_res (g:env) (c:comp_st)
  : RT.equiv (elab_env g) (elab_term (comp_res c)) (elab_term (comp_res (canon_comp c)))
  = RT.Rel_refl _ _ _ 
#pop-options

let canonicalize_st_typing (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
  : st_typing g t (canon_comp c)
  = let c' = canon_comp c in
    let x = fresh g in
    assume ( ~(x `Set.mem` freevars (comp_post c)) /\
            ~(x `Set.mem` freevars (comp_post c')) );
    assume (st_equiv_pre c c');
    let st_eq 
      : st_equiv g c c'
      = ST_VPropEquiv g c c' x (magic ()) (magic()) (magic()) (canon_comp_eq_res g c) (magic()) (magic())
    in
    T_Equiv _ _ _ _ d st_eq

let coerce_eq (#a #b:Type) (x:a) (_:squash (a === b)) : y:b { y == x } = x

let rec intro_uvars_for_logical_implicits (g:env) (uvs:env { disjoint uvs g }) (t:term) (ty:term)
  : T.Tac (uvs':env &
           g':env { extends_with g' g uvs' } &
           t':st_term { Tm_STApp? t'.term }) =
  
  let ropt = is_arrow ty in
  match ropt with
  | Some (b, Some Implicit, c_rest) ->
    let x = fresh (push_env g uvs) in
    let uvs' = push_binding uvs x ppname_default b.binder_ty in
    begin
      match c_rest with
       | C_ST _
       | C_STAtomic _ _
       | C_STGhost _ _ ->
         (| uvs', push_env g uvs', {term=Tm_STApp {head=t;arg_qual=Some Implicit;arg=null_var x};
                                    range=t.range;
                                    effect_tag=as_effect_hint (ctag_of_comp_st c_rest) } |)
       | C_Tot ty ->
         intro_uvars_for_logical_implicits g uvs' (tm_pureapp t (Some Implicit) (null_var x)) ty
    end
  | _ ->
    fail g None
      (Printf.sprintf "check_stapp.intro_uvars_for_logical_implicits: expected an arrow type,\
                       with an implicit parameter, found: %s"
         (P.term_to_string ty))


let instantiate_implicits (g:env) (t:st_term { Tm_STApp? t.term })
  : T.Tac (uvs : env &
val instantiate_implicits (g: env) (t: st_term{Tm_STApp? t.term})
    : T.Tac (uvs: env & g': env{extends_with g' g uvs} & t': st_term{Tm_STApp? t'.term})
g: Pulse.Typing.Env.env -> t: Pulse.Syntax.Base.st_term{Tm_STApp? (Mkst_term?.term t)}
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.dtuple3 Pulse.Typing.Env.env
        (fun uvs -> g': Pulse.Typing.Env.env{Pulse.Typing.Env.extends_with g' g uvs})
        (fun _ _ -> t': Pulse.Syntax.Base.st_term{Tm_STApp? (Mkst_term?.term t')}))