nbp command: give number of useful steps (#155)

main.ml

@@ -134,7 +134,7 @@ hol2dk env
   print the values of $HOL2DK_DIR and $HOLLIGHT_DIR
 
 hol2dk nbp $base
-  print the number of proof steps in $base.prf
+  print the number of useful proof steps in $base.prf
 
 hol2dk proof $base $x $y
   print proof steps between theorem indexes $x and $y
@@ -578,7 +578,14 @@ and command = function
 
   | "stat"::_ -> wrong_nb_args()
 
-  | ["nbp";b] -> log "%#d proof steps\n" (read_val (b^".nbp")); 0
+  | ["nbp";b] ->
+     read_use b;
+     let n =
+       Array.fold_left (fun n k -> if k >= 0 then n+1 else n) 0 !last_use in
+     let nb_proofs = Array.length !last_use in
+     log "%#d / %#d = %2d%% useful proof steps\n"
+       n nb_proofs (percent n nb_proofs);
+     0
 
   | "nbp"::_ -> wrong_nb_args()