let check_effect_annotation g r (c_annot c_computed:comp) =
  match c_annot, c_computed with
  | C_Tot _, C_Tot _ -> ()
  | C_ST _, C_ST _ -> ()
  | C_STAtomic i _, C_STAtomic j _
  | C_STGhost i _, C_STGhost j _ ->
    if eq_tm i j
    then ()
    else fail g (Some i.range)
                (Printf.sprintf "Annotated effect expects only invariants in %s to be opened; but computed effect claims that invariants %s are opened"
                  (P.term_to_string i)
                  (P.term_to_string j))
  | _, _ ->
    fail g (Some r)
           (Printf.sprintf "Expected effect %s but this function body has effect %s"
                  (P.tag_of_comp c_annot)
                  (P.tag_of_comp c_computed))
let check_effect_annotation g r (c_annot: comp) (c_computed: comp) =
match c_annot, c_computed with
| C_Tot _, C_Tot _ -> ()
| C_ST _, C_ST _ -> ()
| C_STAtomic i _, C_STAtomic j _
| C_STGhost i _, C_STGhost j _ ->
  if eq_tm i j
  then ()
  else
    fail g
      (Some i.range)
      (Printf.sprintf "Annotated effect expects only invariants in %s to be opened; but computed effect claims that invariants %s are opened"
          (P.term_to_string i)
          (P.term_to_string j))
| _, _ ->
  fail g
    (Some r)
    (Printf.sprintf "Expected effect %s but this function body has effect %s"
        (P.tag_of_comp c_annot)
        (P.tag_of_comp c_computed))
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.range Pulse.Syntax.Base.comp FStar.Pervasives.Native.Mktuple2 Pulse.Syntax.Base.term Prims.unit Pulse.Syntax.Base.st_comp Pulse.Syntax.Base.eq_tm Prims.bool Pulse.Typing.Env.fail FStar.Pervasives.Native.Some Pulse.Syntax.Base.__proj__Mkterm__item__range Prims.string FStar.Printf.sprintf Pulse.Syntax.Printer.term_to_string Pulse.Syntax.Printer.tag_of_comp
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})
  : 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 check_effect_annotation : g: Pulse.Typing.Env.env ->
    r: Pulse.Syntax.Base.range ->
    c_annot: Pulse.Syntax.Base.comp ->
    c_computed: Pulse.Syntax.Base.comp
  -> FStar.Tactics.Effect.Tac Prims.unit

    g: Pulse.Typing.Env.env ->
    r: Pulse.Syntax.Base.range ->
    c_annot: Pulse.Syntax.Base.comp ->
    c_computed: Pulse.Syntax.Base.comp
  -> FStar.Tactics.Effect.Tac Prims.unit