val term_as_mlexpr (g: env) (t: term) : T.Tac mlexpr
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
val term_as_mlexpr (g: env) (t: term) : T.Tac mlexpr
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
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
Pulse.Extract.Main.env Pulse.Syntax.Base.term Pulse.Extract.CompilerLib.mlexpr Pulse.Extract.CompilerLib.e_tag Pulse.Extract.CompilerLib.mlty FStar.Pervasives.Native.tuple3 Pulse.Extract.CompilerLib.term_as_mlexpr FStar.Tactics.NamedView.term Pulse.Extract.CompilerLib.normalize_for_extraction Pulse.Extract.CompilerLib.uenv Pulse.Extract.Main.uenv_of_env FStar.Reflection.Types.term Pulse.Elaborate.Pure.elab_term
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)
val term_as_mlexpr (g: env) (t: term) : T.Tac mlexpr
g: Pulse.Extract.Main.env -> t: Pulse.Syntax.Base.term
  -> FStar.Tactics.Effect.Tac Pulse.Extract.CompilerLib.mlexpr