diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-11 21:17:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-03 18:49:14 +0200 |
| commit | 844bffb7d6c84a02dcef300dda9099487b23c09a (patch) | |
| tree | 0b95e9fdddf6ab2204434da3ff4729edfe34d2e8 /pretyping/cbv.ml | |
| parent | 3c795ba6b5728e8a0a699ab15c773c52c48f33e4 (diff) | |
Added an option Set Debug Cbv.
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index e18625c42..bd7350dc4 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -175,6 +175,19 @@ let cofixp_reducible flgs _ stk = else false +let debug_cbv = ref false +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = "cbv visited constants display"; + Goptions.optkey = ["Debug";"Cbv"]; + Goptions.optread = (fun () -> !debug_cbv); + Goptions.optwrite = (fun a -> debug_cbv:=a); +} + +let pr_key = function + | ConstKey (sp,_) -> Names.Constant.print sp + | VarKey id -> Names.Id.print id + | RelKey n -> Pp.(str "REL_" ++ int n) (* The main recursive functions * @@ -254,9 +267,17 @@ let rec norm_head info env t stack = and norm_head_ref k info env stack normt = if red_set_ref (info_flags info) normt then match ref_value_cache info normt with - | Some body -> strip_appl (shift_value k body) stack - | None -> (VAL(0,make_constr_ref k normt),stack) - else (VAL(0,make_constr_ref k normt),stack) + | Some body -> + if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); + strip_appl (shift_value k body) stack + | None -> + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + (VAL(0,make_constr_ref k normt),stack) + else + begin + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + (VAL(0,make_constr_ref k normt),stack) + end (* cbv_stack_term performs weak reduction on constr t under the subs * env, with context stack, i.e. ([env]t stack). First computes weak |