val term_to_string' (level: string) (t: term) : T.Tac string
let rec term_to_string' (level:string) (t:term)
  : T.Tac string
  = match t.t with
    | Tm_Emp -> "emp"

    | Tm_Pure p ->
      sprintf "pure (\n%s%s)" 
        (indent level)
        (term_to_string' (indent level) p)
      
    | Tm_Star p1 p2 ->
      sprintf "%s ** \n%s%s" 
        (term_to_string' level p1)
        level
        (term_to_string' level p2)
                          
    | Tm_ExistsSL _ b body ->
      sprintf "(exists (%s:%s).\n%s%s)"
              (T.unseal b.binder_ppname.name)
              (term_to_string' (indent level) b.binder_ty)
              level
              (term_to_string' (indent level) body)

    | Tm_ForallSL u b body ->
      sprintf "(forall (%s:%s).\n%s%s)"
              (T.unseal b.binder_ppname.name)
              (term_to_string' (indent level) b.binder_ty)
              level
              (term_to_string' (indent level) body)
                          
    | Tm_VProp -> "vprop"
    | Tm_Inames -> "inames"
    | Tm_EmpInames -> "emp_inames"
    | Tm_Unknown -> "_"
    | Tm_FStar t ->
      T.term_to_string t
val term_to_string' (level: string) (t: term) : T.Tac string
let rec term_to_string' (level: string) (t: term) : T.Tac string =
match t.t with
| Tm_Emp -> "emp"
| Tm_Pure p -> sprintf "pure (\n%s%s)" (indent level) (term_to_string' (indent level) p)
| Tm_Star p1 p2 ->
  sprintf "%s ** \n%s%s" (term_to_string' level p1) level (term_to_string' level p2)
| Tm_ExistsSL _ b body ->
  sprintf "(exists (%s:%s).\n%s%s)"
    (T.unseal b.binder_ppname.name)
    (term_to_string' (indent level) b.binder_ty)
    level
    (term_to_string' (indent level) body)
| Tm_ForallSL u b body ->
  sprintf "(forall (%s:%s).\n%s%s)"
    (T.unseal b.binder_ppname.name)
    (term_to_string' (indent level) b.binder_ty)
    level
    (term_to_string' (indent level) body)
| Tm_VProp -> "vprop"
| Tm_Inames -> "inames"
| Tm_EmpInames -> "emp_inames"
| Tm_Unknown -> "_"
| Tm_FStar t -> T.term_to_string t
Pulse.Syntax.Printer.fst.checked
Pulse.Syntax.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.String.fsti.checked FStar.Sealed.fsti.checked FStar.Reflection.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Syntax.Printer.fst
Prims.string Pulse.Syntax.Base.term Pulse.Syntax.Base.__proj__Mkterm__item__t FStar.Printf.sprintf Pulse.Syntax.Printer.indent Pulse.Syntax.Printer.term_to_string' Pulse.Syntax.Base.universe Pulse.Syntax.Base.binder FStar.Tactics.Unseal.unseal Pulse.Syntax.Base.__proj__Mkppname__item__name Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ppname Pulse.Syntax.Base.__proj__Mkbinder__item__binder_ty Pulse.Syntax.Base.host_term FStar.Tactics.V2.Builtins.term_to_string
module Pulse.Syntax.Printer
open FStar.Printf
open Pulse.Syntax.Base

module L = FStar.List.Tot

module T = FStar.Tactics.V2
module Un = FStar.Sealed
module R = FStar.Reflection.V2

let tot_or_ghost_to_string = function
  | T.E_Total -> "total"
  | T.E_Ghost -> "ghost"


let name_to_string (f:R.name) = String.concat "." f

let dbg_printing : bool = true

// let constant_to_string = function
//   | Unit -> "()"
//   | Bool true -> "true"
//   | Bool false -> "false"
//   | Int i -> sprintf "%d" i

let rec universe_to_string (n:nat) (u:universe) 
  : Tot string (decreases u) =
  let open R in
  match inspect_universe u with
  | Uv_Unk -> "_"
  | Uv_Zero -> sprintf "%d" n
  | Uv_Succ u -> universe_to_string (n + 1) u
  | Uv_BVar x -> if n = 0 then sprintf "%d" x else sprintf "(%d + %d)" x n
  | Uv_Max us ->
    let r = "(max _)" in
    // sprintf "(max %s %s)" (universe_to_string 0 u0) (universe_to_string 0 u1) in
    if n = 0 then r else sprintf "%s + %d" r n
  | _ -> sprintf "<univ>"

let univ_to_string u = sprintf "u#%s" (universe_to_string 0 u)
let qual_to_string = function
  | None -> ""
  | Some Implicit -> "#"

let indent (level:string) = level ^ "\t"
    
let rec term_to_string' (level:string) (t:term)
val term_to_string' (level: string) (t: term) : T.Tac string
level: Prims.string -> t: Pulse.Syntax.Base.term -> FStar.Tactics.Effect.Tac Prims.string