val term_opt_to_string (t: option term) : T.Tac string
let term_opt_to_string (t:option term)
  : T.Tac string
  = match t with
    | None -> ""
    | Some t -> term_to_string t
val term_opt_to_string (t: option term) : T.Tac string
let term_opt_to_string (t: option term) : T.Tac string =
match t with
| None -> ""
| Some 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
FStar.Pervasives.Native.option Pulse.Syntax.Base.term Prims.string Pulse.Syntax.Printer.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)
  : 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
let term_to_string t = term_to_string' "" t

let rec term_to_doc t
  : T.Tac document
  = match t.t with
    | Tm_Emp -> doc_of_string "emp"

    | Tm_Pure p -> doc_of_string "pure" ^/^ parens (term_to_doc p)
    | Tm_Star p1 p2 ->
      infix 2 1 (doc_of_string "**")
                (term_to_doc p1)
                (term_to_doc p2)

    | Tm_ExistsSL _ b body ->
      parens (doc_of_string "exists" ^/^ parens (doc_of_string (T.unseal b.binder_ppname.name)
                                                  ^^ doc_of_string ":"
                                                  ^^ term_to_doc b.binder_ty)
              ^^ doc_of_string "."
              ^/^ term_to_doc body)

    | Tm_ForallSL u b body ->
      parens (doc_of_string "forall" ^/^ parens (doc_of_string (T.unseal b.binder_ppname.name)
                                                  ^^ doc_of_string ":"
                                                  ^^ term_to_doc b.binder_ty)
              ^^ doc_of_string "."
              ^/^ term_to_doc body)

    | Tm_VProp -> doc_of_string "vprop"
    | Tm_Inames -> doc_of_string "inames"
    | Tm_EmpInames -> doc_of_string "emp_inames"
    | Tm_Unknown -> doc_of_string "_"
    | Tm_FStar t ->
      // Should call term_to_doc when available
      doc_of_string (T.term_to_string t)

let binder_to_string (b:binder)
  : T.Tac string
  = sprintf "%s:%s" 
            (T.unseal b.binder_ppname.name)
            (term_to_string b.binder_ty)

let ctag_to_string = function
  | STT -> "ST"
  | STT_Atomic -> "STAtomic"
  | STT_Ghost -> "STGhost"

let comp_to_string (c:comp)
  : T.Tac string
  = match c with
    | C_Tot t -> 
      sprintf "Tot %s" (term_to_string t)
      
    | C_ST s ->
      sprintf "stt %s (requires\n%s) (ensures\n%s)"
              (term_to_string s.res)
              (term_to_string s.pre)
              (term_to_string s.post)

    | C_STAtomic inames s ->
      sprintf "stt_atomic %s %s (requires\n%s) (ensures\n%s)"
              (term_to_string inames)
              (term_to_string s.res)
              (term_to_string s.pre)
              (term_to_string s.post)

    | C_STGhost inames s ->
      sprintf "stt_atomic %s %s (requires\n%s) (ensures\n%s)"
              (term_to_string inames)
              (term_to_string s.res)
              (term_to_string s.pre)
              (term_to_string s.post)

let term_opt_to_string (t:option term)
val term_opt_to_string (t: option term) : T.Tac string
t: FStar.Pervasives.Native.option Pulse.Syntax.Base.term -> FStar.Tactics.Effect.Tac Prims.string