Simplify tracing for the x64 spec function.

HOL-Theorem-Prover · Mar 18, 2014 · d90a46f · d90a46f
1 parent 93ac68d
commit d90a46f
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 6 deletions.
diff --git a/examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml b/examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml
@@ -36,7 +36,7 @@ val (decomp_cert,decomp_def) = x64_decompLib.x64_decompile "decomp" `
 
 val _ = save_thm("decomp_cert",decomp_cert);
 
-val () = x64_progLib.x64_spec_trace := SOME (fn s => print (" " ^ s))
+val () = Feedback.set_trace "x64 spec" 2
 
 val (decomp1_cert,decomp1_def) = x64_decompLib.x64_decompile "decomp1" `
   (*  0: *) 55              (* push   %rbp *)
@@ -66,4 +66,4 @@ val (decomp1_cert,decomp1_def) = x64_decompLib.x64_decompile "decomp1" `
 
 val _ = save_thm("decomp1_cert",decomp1_cert);
 
-val _ = export_theory();
+val _ = export_theory()
diff --git a/examples/l3-machine-code/x64/prog/x64_progLib.sig b/examples/l3-machine-code/x64/prog/x64_progLib.sig
@@ -2,5 +2,4 @@ signature x64_progLib =
 sig
    val x64_spec: string -> Thm.thm
    val x64_spec_code: string quotation -> Thm.thm list
-   val x64_spec_trace: (string -> unit) option ref
 end
diff --git a/examples/l3-machine-code/x64/prog/x64_progLib.sml b/examples/l3-machine-code/x64/prog/x64_progLib.sml
@@ -258,16 +258,20 @@ local
            NO_TAC STATE_TAC
    val disassemble1 =
       hd o x64AssemblerLib.x64_disassemble o Lib.list_of_singleton o QUOTE
+   val x64_spec_trace = ref 0
+   val () = Feedback.register_trace ("x64 spec", x64_spec_trace, 2)
 in
-   val x64_spec_trace = ref NONE
    val x64_spec =
       (* utilsLib.cache 2000 String.compare *)
          (fn s =>
              let
                 val thm = x64_stepLib.x64_step s
                 val t = x64_mk_pre_post thm
              in
-                case !x64_spec_trace of SOME f => f (disassemble1 s) | _ => ()
+                case !x64_spec_trace of
+                   1 => assemblerLib.printn (s ^ " ; " ^ disassemble1 s)
+                 | 2 => print (" " ^ disassemble1 s)
+                 | _ => ()
               ; spec (thm, t)
              end)
 end
@@ -280,7 +284,7 @@ val x64_spec_code = List.map x64_spec o x64AssemblerLib.x64_code_no_spaces
 
 open x64_progLib
 
-val () = x64_spec_trace := SOME assemblerLib.printn
+val () = Feedback.set_trace "x64 spec" 1
 
 val thms = x64_spec_code
   `ret                          ; c3