From bcfd854d7a6e012ac6bf116487a59a0f997725ee Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Mon, 30 Jun 2014 18:05:39 +0200
Subject: Debug RAKAM

---
 pretyping/reductionops.ml | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 383066405c..e9f84391b6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -749,9 +749,29 @@ let fix_recarg ((recindices,bodynum),_) stack =
     It substitutes fix and cofix by the constant they come from in
     contract_* in any case .
 *)
+
+let debug_RAKAM = ref (false)
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname =
+    "Print states of the Reductionops abstract machine";
+  Goptions.optkey = ["Debug";"RAKAM"];
+  Goptions.optread = (fun () -> !debug_RAKAM);
+  Goptions.optwrite = (fun a -> debug_RAKAM:=a);
+}
+
 let rec whd_state_gen ?csts tactic_mode flags env sigma =
   let rec whrec cst_l (x, stack as s) =
+    let () = if !debug_RAKAM then
+	let open Pp in
+	pp (h 0 (str "<<" ++ Termops.print_constr x ++
+		   str "|" ++ cut () ++ Cst_stack.pr cst_l ++
+		   str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
+		   str ">>") ++ fnl ())
+    in
     let fold () =
+      let () = if !debug_RAKAM then
+	  let open Pp in pp (str "<><><><><>" ++ fnl ()) in
       if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l)
     in
     match kind_of_term x with
-- 
cgit v1.2.3