val extend_env (g: env) (b: binder) : T.Tac (env & mlident & mlty & name)
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)
val extend_env (g: env) (b: binder) : T.Tac (env & mlident & mlty & name)
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 = uenv_inner; coreenv = coreenv }, mlident, mlty, (b.binder_ppname, x)
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.binder Pulse.Extract.CompilerLib.uenv Pulse.Extract.CompilerLib.mlident FStar.Pervasives.Native.Mktuple4 Pulse.Extract.CompilerLib.mlty Pulse.Extract.Main.name Pulse.Extract.Main.Mkenv FStar.Pervasives.Native.Mktuple2 Pulse.Syntax.Base.ppname Prims.nat Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ppname FStar.Pervasives.Native.tuple4 FStar.Pervasives.Native.tuple2 Pulse.Extract.CompilerLib.extend_bv Pulse.Extract.Main.__proj__Mkenv__item__uenv_inner Prims.unit Pulse.Extract.Main.debug Prims.string FStar.Printf.sprintf Pulse.Syntax.Printer.binder_to_string Pulse.Syntax.Printer.term_to_string Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ty Pulse.Typing.Env.env Prims.eq2 FStar.Reflection.Typing.fstar_top_env Pulse.Typing.Env.fstar_env Pulse.Extract.Main.__proj__Mkenv__item__coreenv Pulse.Typing.Env.push_binding Pulse.Syntax.Base.var Prims.l_not Prims.b2t FStar.Set.mem Pulse.Typing.Env.dom Pulse.Typing.Env.fresh Pulse.Extract.Main.term_as_mlty
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)
val extend_env (g: env) (b: binder) : T.Tac (env & mlident & mlty & name)
g: Pulse.Extract.Main.env -> b: Pulse.Syntax.Base.binder
  -> FStar.Tactics.Effect.Tac
    (((Pulse.Extract.Main.env * Pulse.Extract.CompilerLib.mlident) * Pulse.Extract.CompilerLib.mlty) *
      Pulse.Extract.Main.name)