diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-06-30 18:05:39 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-08-26 17:48:50 +0200 |
| commit | bcfd854d7a6e012ac6bf116487a59a0f997725ee (patch) | |
| tree | 08c36946a8d0587fe450b2ec897eaaf09145d166 | |
| parent | 3ffdcc7183b2cfbf6c53dd4f1dd6e48da416f07d (diff) | |
Debug RAKAM
| -rw-r--r-- | dev/db | 1 | ||||
| -rw-r--r-- | dev/include | 3 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 20 |
4 files changed, 24 insertions, 1 deletions
@@ -33,6 +33,7 @@ install_printer Top_printers.pptype install_printer Top_printers.ppj install_printer Top_printers.ppenv install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_cst_stack_t install_printer Top_printers.ppmetas install_printer Top_printers.ppevm diff --git a/dev/include b/dev/include index 7c63f5443..941fa3383 100644 --- a/dev/include +++ b/dev/include @@ -53,7 +53,8 @@ #install_printer (* type_judgement *) pptype;; #install_printer (* judgement *) ppj;; -#install_printer (* judgement *) pp_cst_stack_t;; +#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; +#install_printer (* Reductionops machine stack *) pp_stack_t;; (*#install_printer (* hint_db *) print_hint_db;;*) (*#install_printer (* hints_path *) pphintspath;;*) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index fccf580a5..15f35b775 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -141,6 +141,7 @@ let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n) let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) +let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 383066405..e9f84391b 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 |