let print_code c _ _ = ("<" ^ aux_print_code c ^ ">\n"), 0
let print_code c _ _ =
("<" ^ aux_print_code c ^ ">\n"), 0
Vale.Transformers.DebugPrint.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.String.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Char.fsti.checked
Vale.Transformers.DebugPrint.fst
Vale.X64.Machine_Semantics_s.code FStar.Pervasives.Native.Mktuple2 Prims.string Prims.int Prims.op_Hat Vale.Transformers.DebugPrint.aux_print_code FStar.Pervasives.Native.tuple2
(**

   This is a convenience module for making it easier to debug
   transformations by overriding some printers. You probably do not want
   to use this module unless you know exactly what you're doing.

*)
module Vale.Transformers.DebugPrint

open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.Def.PossiblyMonad
open Vale.X64.Decls
open Vale.X64.Print_s
open FStar.String

let rec get_non_space (x:list char) : string =
  match x with
  | [] -> "."
  | x :: xs ->
    if x = ' ' then get_non_space xs else string_of_list [x]

let print_ins i _ =
  get_non_space (list_of_string (print_ins i gcc))

let rec aux_print_code (c:code) : string =
  match c with
  | Ins i -> print_ins i gcc
  | Block l -> "(" ^ aux_print_codes l ^ ")"
  | IfElse _ t f -> "I" ^ aux_print_code t ^ aux_print_code f
  | While _ b -> "W" ^ aux_print_code b

and aux_print_codes (c:codes) : string =
  match c with
  | [] -> ""
  | x :: xs -> aux_print_code x ^ aux_print_codes xs
val print_code : c: Vale.X64.Machine_Semantics_s.code -> _: _ -> _: _ -> Prims.string * Prims.int
c: Vale.X64.Machine_Semantics_s.code -> _: _ -> _: _ -> Prims.string * Prims.int