diff options
| author | Maxime Dénès | 2020-08-28 16:39:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-08-28 17:24:59 +0200 |
| commit | d1dc6347fb9aa0659f8a8e824c33937d6bfb6e3e (patch) | |
| tree | 18edfe7faf45f41a71845ee8d3f9ae90257e3a93 /engine | |
| parent | 911f33f0a0ff648082d329841388f59e8cecf231 (diff) | |
Enrich `evar_map` printer with future goals stack
This is a useful for debugging.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 14 | ||||
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 4 |
3 files changed, 19 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 62a818ee6f..555c3a150c 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -499,6 +499,8 @@ module FutureGoals : sig val put_shelf : Evar.t list -> stack -> stack + val pr_stack : stack -> Pp.t + end = struct type t = { @@ -588,6 +590,15 @@ end = struct let shelf = shelved @ hd.shelf in { hd with shelf } :: tl + let pr_stack stack = + let open Pp in + let pr_future_goals fgl = + prlist_with_sep spc Evar.print fgl.comb ++ + pr_opt (fun ev -> str"(principal: " ++ Evar.print ev ++ str")") fgl.principal + in + if List.is_empty stack then str"(empty stack)" + else prlist_with_sep (fun () -> str"||") pr_future_goals stack + end @@ -1197,6 +1208,9 @@ let shelve_on_future_goals shelved evd = let remove_future_goal evd evk = { evd with future_goals = FutureGoals.remove evk evd.future_goals } +let pr_future_goals_stack evd = + FutureGoals.pr_stack evd.future_goals + let give_up ev evd = { evd with given_up = Evar.Set.add ev evd.given_up } diff --git a/engine/evd.mli b/engine/evd.mli index db5265ca0a..5c7a529b9c 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -392,6 +392,8 @@ val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map val remove_future_goal : evar_map -> Evar.t -> evar_map +val pr_future_goals_stack : evar_map -> Pp.t + val give_up : Evar.t -> evar_map -> evar_map val given_up : evar_map -> Evar.Set.t diff --git a/engine/termops.ml b/engine/termops.ml index e5231ef9cd..7579631313 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -301,8 +301,10 @@ let pr_evar_map_gen with_univs pr_evars env sigma = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma + and future_goals = + str "FUTURE GOALS STACK:" ++ brk (0, 1) ++ Evd.pr_future_goals_stack sigma ++ fnl () in - evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ future_goals let pr_evar_list env sigma l = let open Evd in |