let rec abs_body (n_args:nat) (t:st_term) =
  if n_args = 0 then Some t
  else (
    match t.term with 
    | Tm_Abs { body } -> abs_body (n_args - 1) body
    | _ -> None
  )
let rec abs_body (n_args: nat) (t: st_term) =
if n_args = 0
then Some t
else
  (match t.term with
    | Tm_Abs { body = body } -> abs_body (n_args - 1) body
    | _ -> None)
Pulse.Extract.Main.fst.checked
Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.Naming.fsti.checked Pulse.Syntax.Base.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Reflection.Util.fst.checked Pulse.Readback.fsti.checked Pulse.Extract.CompilerLib.fsti.checked Pulse.Elaborate.Pure.fst.checked Pulse.Checker.Match.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Sealed.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Reflection.fst.checked FStar.Range.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Pulse.Extract.Main.fst
Prims.nat Pulse.Syntax.Base.st_term Prims.op_Equality Prims.int FStar.Pervasives.Native.Some Prims.bool Pulse.Syntax.Base.__proj__Mkst_term__item__term Pulse.Syntax.Base.binder FStar.Pervasives.Native.option Pulse.Syntax.Base.qualifier Pulse.Syntax.Base.comp Pulse.Extract.Main.abs_body Prims.op_Subtraction Pulse.Syntax.Base.st_term' FStar.Pervasives.Native.None
module Pulse.Extract.Main

open Pulse.Syntax.Base
open Pulse.Extract.CompilerLib
open Pulse.Syntax.Printer
open FStar.List.Tot

module L = FStar.List.Tot
module R = FStar.Reflection
module RT = FStar.Reflection.Typing
module T = FStar.Tactics.V2
module RB = Pulse.Readback
module Elab = Pulse.Elaborate.Pure
module E = Pulse.Typing.Env
module LN = Pulse.Syntax.Naming
module RU = Pulse.RuntimeUtils
module ECL = Pulse.Extract.CompilerLib

exception Extraction_failure of string

noeq
type env = { 
  uenv_inner: uenv;
  coreenv: Pulse.Typing.Env.env
}

let name = ppname & nat

let topenv_of_env (g:env) = E.fstar_env g.coreenv
let tcenv_of_env (g:env) = Pulse.Typing.elab_env g.coreenv
let uenv_of_env (g:env) = set_tcenv g.uenv_inner (tcenv_of_env g)
  
let debug (g:env) (f: unit -> T.Tac string)
  : T.Tac unit
  = if RU.debug_at_level (E.fstar_env g.coreenv) "pulse_extraction"
    then T.print (f())


let term_as_mlexpr (g:env) (t:term)
  : T.Tac mlexpr
  = let t = Elab.elab_term t in
    let uenv = uenv_of_env g in
    let t = normalize_for_extraction uenv t in
    let mlt, _, _ = term_as_mlexpr uenv t in
    mlt

let term_as_mlty (g:env) (t:term)
  : T.Tac mlty
  = let t = Elab.elab_term t in
    term_as_mlty (uenv_of_env g) t

let extend_env (g:env) (b:binder)
  : T.Tac (env & mlident & mlty & name)
  = let mlty = term_as_mlty g b.binder_ty in
    let x = E.fresh g.coreenv in
    let coreenv = E.push_binding g.coreenv x b.binder_ppname b.binder_ty in
    debug g (fun _ -> Printf.sprintf "Extending environment with %s : %s\n"
                                      (binder_to_string b)
                                      (term_to_string b.binder_ty));
    let uenv_inner, mlident = extend_bv g.uenv_inner b.binder_ppname x mlty in
    { uenv_inner; coreenv }, mlident, mlty, (b.binder_ppname, x)

let rec name_as_mlpath (x:T.name) 
  : T.Tac mlpath 
  = match x with
    | [] -> T.fail "Unexpected empty name"
    | [x] -> [], x
    | x :: xs ->
      let xs, x = name_as_mlpath xs in
      x :: xs, x

module R = FStar.Reflection.V2
let extract_constant (g:env) (c:T.vconst)
  : T.Tac mlconstant
  = let e = T.pack_ln (R.Tv_Const c) in
    let mle, _, _ = CompilerLib.term_as_mlexpr (uenv_of_env g) e in
    match mlconstant_of_mlexpr mle with
    | None -> T.raise (Extraction_failure "Failed to extract constant")
    | Some c -> c

let rec extend_env_pat_core (g:env) (p:pattern)
  : T.Tac (env & list mlpattern & list Pulse.Typing.Env.binding)
  = match p with
    | Pat_Dot_Term _ -> g, [], []
    | Pat_Var pp sort -> 
      let x = E.fresh g.coreenv in
      let pp = mk_ppname pp FStar.Range.range_0 in
      let ty = T.unseal sort in
      assume (not_tv_unknown ty);
      let ty = tm_fstar ty (T.range_of_term ty) in
      debug g (fun _ -> Printf.sprintf "Pushing pat_var %s : %s\n" (T.unseal pp.name) (term_to_string ty));
      let coreenv = E.push_binding g.coreenv x pp ty in
      let uenv_inner, mlident = extend_bv g.uenv_inner pp x mlty_top in
      { uenv_inner; coreenv },
      [ mlp_var mlident ],
      [ (x, tm_unknown) ]

    | Pat_Cons f pats ->
      let g, pats, bindings = 
        T.fold_left
          (fun (g, pats, bindings) (p, _) ->
            let g, pats', bindings' = extend_env_pat_core g p in
            g, pats @ pats', bindings@bindings')
          (g, [], [])
          pats
      in
      g, [mlp_constructor (name_as_mlpath f.fv_name) pats], bindings
    | Pat_Constant c ->
      let c = extract_constant g c in
      g, [mlp_const c], []
let extend_env_pat g p = 
  let g, pats, bs = extend_env_pat_core g p in
  match pats with
  | [p] -> g, p, bs
  | _ -> T.raise (Extraction_failure "Unexpected extraction of pattern")

let unit_val : term = tm_fstar Pulse.Reflection.Util.unit_tm Range.range_0
let is_erasable (p:st_term) : T.Tac bool = 
  let tag = T.unseal p.effect_tag in
  match tag with
  | Some STT_Ghost -> true
  | _ -> false
    
let head_and_args (t:term)
  : option (R.term & list R.argv) =
  match t.t with
  | Tm_FStar t0 -> Some (R.collect_app_ln t0)
  | _ -> None

let term_eq_string (s:string) (t:R.term) : bool =
  match R.inspect_ln t with
  | R.Tv_Const (R.C_String s') -> s=s'
  | _ -> false

let maybe_unfold_head (g:env) (f:R.term) 
  : option st_term
  = match R.inspect_ln f with
    | R.Tv_FVar f -> (
      let name = R.inspect_fv f in
      match R.lookup_typ (topenv_of_env g) name with
      | None -> None
      | Some se ->
        let attrs = R.sigelt_attrs se in
        if List.Tot.existsb (term_eq_string "inline") attrs
        then sigelt_extension_data se
        else None
    )
    | R.Tv_UInst f _ ->
      //No universe-polymorphic inlining ... yet
      None
    | _ -> None
val abs_body : n_args: Prims.nat -> t: Pulse.Syntax.Base.st_term
  -> FStar.Pervasives.Native.option Pulse.Syntax.Base.st_term
n_args: Prims.nat -> t: Pulse.Syntax.Base.st_term
  -> FStar.Pervasives.Native.option Pulse.Syntax.Base.st_term