val preprocess_abs (g: env) (t: st_term{Tm_Abs? t.term}) : T.Tac (t: st_term{Tm_Abs? t.term})
let preprocess_abs
      (g:env)
      (t:st_term{Tm_Abs? t.term})
  : T.Tac (t:st_term { Tm_Abs? t.term })
  = let annot = arrow_of_abs t in
    let annot, _ = Pulse.Checker.Pure.instantiate_term_implicits g annot in
    match annot.t with
    | Tm_FStar annot ->
      rebuild_abs g t annot
    | _ ->
      Env.fail g (Some t.range) 
                 (Printf.sprintf "Expected an arrow type as an annotation, got %s"
                          (P.term_to_string annot))
val preprocess_abs (g: env) (t: st_term{Tm_Abs? t.term}) : T.Tac (t: st_term{Tm_Abs? t.term})
let preprocess_abs (g: env) (t: st_term{Tm_Abs? t.term}) : T.Tac (t: st_term{Tm_Abs? t.term}) =
let annot = arrow_of_abs t in
let annot, _ = Pulse.Checker.Pure.instantiate_term_implicits g annot in
match annot.t with
| Tm_FStar annot -> rebuild_abs g t annot
| _ ->
  Env.fail g
    (Some t.range)
    (Printf.sprintf "Expected an arrow type as an annotation, got %s" (P.term_to_string annot))
Pulse.Checker.Abs.fst.checked
Pulse.Typing.FV.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.Abs.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.st_term Prims.b2t Pulse.Syntax.Base.uu___is_Tm_Abs Pulse.Syntax.Base.__proj__Mkst_term__item__term Pulse.Syntax.Base.term Pulse.Syntax.Base.__proj__Mkterm__item__t Pulse.Syntax.Base.host_term Pulse.Checker.Abs.rebuild_abs Pulse.Syntax.Base.term' Pulse.Typing.Env.fail FStar.Pervasives.Native.Some Pulse.Syntax.Base.range Pulse.Syntax.Base.__proj__Mkst_term__item__range Prims.string FStar.Printf.sprintf Pulse.Syntax.Printer.term_to_string FStar.Pervasives.Native.tuple2 Pulse.Checker.Pure.instantiate_term_implicits Pulse.Checker.Abs.arrow_of_abs
module Pulse.Checker.Abs

module T = FStar.Tactics.V2

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

module P = Pulse.Syntax.Printer
module FV = Pulse.Typing.FV
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
(* Infers the the type of the binders from the specification alone, not the body *)

let rec arrow_of_abs (t:st_term { Tm_Abs? t.term })
  : T.Tac term
  = let Tm_Abs { b; q; ascription; body } = t.term in
    if Tm_Abs? body.term
    then (
      let arr = arrow_of_abs body in
      tm_arrow b q (C_Tot arr)
    )
    else
      tm_arrow b q ascription
module Env = Pulse.Typing.Env

let rec rebuild_abs (g:env) (t:st_term) (annot:T.term)
  : T.Tac (t:st_term { Tm_Abs? t.term })
  = match t.term, R.inspect_ln annot with
    | Tm_Abs { b; q; ascription=C_Tot un; body }, R.Tv_Arrow b' c' -> (
      let ty = readback_ty (T.inspect_binder b').sort in
      let comp = R.inspect_comp c' in
      match ty, comp with
      | Some ty, T.C_Total res_ty ->
        let b = { binder_ty = ty ; binder_ppname = b.binder_ppname } in
        let body = rebuild_abs g body res_ty in
        { t with term = Tm_Abs { b; q; ascription=C_Tot un; body }}
      | _ ->
        Env.fail g (Some t.range) 
            (Printf.sprintf "Unexpected type of abstraction: %s"
                (T.term_to_string annot))
    )
    | Tm_Abs { b; q; ascription=_; body }, R.Tv_Arrow b' c' -> (
      let ty = readback_ty (T.inspect_binder b').sort in
      let comp = R.inspect_comp c' in
      match ty, comp with
      | Some ty, R.C_Total res -> (
        let c = readback_comp res in
        match c with
        | None -> 
          Env.fail g (Some t.range) 
                      (Printf.sprintf "Unexpected computation type in abstraction: %s"
                          (T.term_to_string res))
        | Some c ->
          let b = { binder_ty = ty ; binder_ppname = b.binder_ppname } in
          { t with term = Tm_Abs { b; q; ascription=c; body }}
      )
      | _ ->
        Env.fail g (Some t.range) 
                    (Printf.sprintf "Unexpected type of abstraction: %s"
                          (T.term_to_string annot))
    )
    | _ -> 
      Env.fail g (Some t.range) 
                (Printf.sprintf "Unexpected arity of abstraction: expected a term of type %s"
                      (T.term_to_string annot))

let preprocess_abs
      (g:env)
      (t:st_term{Tm_Abs? t.term})
val preprocess_abs (g: env) (t: st_term{Tm_Abs? t.term}) : T.Tac (t: st_term{Tm_Abs? t.term})
g: Pulse.Typing.Env.env -> t: Pulse.Syntax.Base.st_term{Tm_Abs? (Mkst_term?.term t)}
  -> FStar.Tactics.Effect.Tac (t: Pulse.Syntax.Base.st_term{Tm_Abs? (Mkst_term?.term t)})