diff options
| -rw-r--r-- | dev/include | 4 | ||||
| -rw-r--r-- | dev/top_printers.ml | 3 | ||||
| -rw-r--r-- | plugins/subtac/subtac_utils.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.ml | 52 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 | ||||
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 3 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 |
10 files changed, 54 insertions, 22 deletions
diff --git a/dev/include b/dev/include index 243f9ea5f..1648d5791 100644 --- a/dev/include +++ b/dev/include @@ -24,11 +24,7 @@ #install_printer (* judgement *) ppj;; #install_printer (* hint_db *) print_hint_db;; -#install_printer (* goal *) ppgoal;; -#install_printer (* sigma goal *) ppsigmagoal;; -#install_printer (* proof *) pproof;; #install_printer (* Goal.goal *) ppgoalgoal;; -#install_printer (* pftreestate *) pppftreestate;; #install_printer (* metaset.t *) ppmetas;; #install_printer (* evar_map *) ppevm;; #install_printer (* clenv *) ppclenv;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 547ca0475..333cf1a67 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -112,7 +112,8 @@ let pp_transparent_state s = pp (pr_transparent_state s) (* proof printers *) let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_map evd) +let ppevm evd = pp(pr_evar_map (Some 2) evd) +let ppevmall evd = pp(pr_evar_map None evd) let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) (* spiwack: deactivated until a replacement is found diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 7fba23dc2..cd9028fe8 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -119,7 +119,7 @@ let my_print_context = Termops.print_rel_context let my_print_named_context = Termops.print_named_context let my_print_env = Termops.print_env let my_print_glob_constr = Printer.pr_glob_constr_env -let my_print_evardefs = Evd.pr_evar_map +let my_print_evardefs = Evd.pr_evar_map None let my_print_tycon_type = Evarutil.pr_tycon_type diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5125b21cc..5f08a0e8a 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -766,21 +766,55 @@ let pr_evar_info evi = in hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") -let pr_evar_map_t (evars,(uvs,univs) as sigma) = +let compute_evar_dependency_graph (sigma:evar_map) = + (* Compute the map binding ev to the evars whose body depends on ev *) + fold (fun evk evi acc -> + let deps = + match evar_body evi with + | Evar_empty -> ExistentialSet.empty + | Evar_defined c -> collect_evars c in + ExistentialSet.fold (fun evk' acc -> + let tab = try ExistentialMap.find evk' acc with Not_found -> [] in + ExistentialMap.add evk' ((evk,evi)::tab) acc) deps acc) + sigma ExistentialMap.empty + +let evar_dependency_closure n sigma = + let graph = compute_evar_dependency_graph sigma in + let order a b = fst a < fst b in + let rec aux n l = + if n=0 then l + else + let l' = + list_map_append (fun (evk,_) -> ExistentialMap.find evk graph) l in + aux (n-1) (list_uniquize (Sort.list order (l@l'))) in + aux n (undefined_list sigma) + +let pr_evar_map_t depth sigma = + let (evars,(uvs,univs)) = sigma.evars in + let pr_evar_list l = + h 0 (prlist_with_sep pr_fnl + (fun (ev,evi) -> + h 0 (str(string_of_existential ev) ++ + str"==" ++ pr_evar_info evi)) l) in let evs = if evars = EvarInfoMap.empty then mt () else - str"EVARS:"++brk(0,1)++ - h 0 (prlist_with_sep pr_fnl - (fun (ev,evi) -> - h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) - (EvarMap.to_list sigma))++fnl() + match depth with + | None -> + (* Print all evars *) + str"EVARS:"++brk(0,1)++pr_evar_list (to_list sigma)++fnl() + | Some n -> + (* Print all evars *) + str"UNDEFINED EVARS"++ + (if n=0 then mt() else str" (+level "++int n++str" closure):")++ + brk(0,1)++ + pr_evar_list (evar_dependency_closure n sigma)++fnl() and svs = if Univ.UniverseLSet.is_empty uvs then mt () else str"UNIVERSE VARIABLES:"++brk(0,1)++ h 0 (prlist_with_sep pr_fnl (fun u -> Univ.pr_uni_level u) (Univ.UniverseLSet.elements uvs))++fnl() - and cs = + and cs = if univs = Univ.initial_universes then mt () else str"UNIVERSES:"++brk(0,1)++ h 0 (Univ.pr_universes univs)++fnl() @@ -810,10 +844,10 @@ let pr_evar_map_constraints evd = if evd.conv_pbs = [] then mt() else pr_constraints evd.conv_pbs++fnl() -let pr_evar_map evd = +let pr_evar_map allevars evd = let pp_evm = if evd.evars = EvarMap.empty then mt() else - pr_evar_map_t evd.evars++fnl() in + pr_evar_map_t allevars evd++fnl() in let cstrs = if evd.conv_pbs = [] then mt() else str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in let pp_met = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 8131837d8..0ba752de7 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -280,7 +280,7 @@ type unsolvability_explanation = SeveralInstancesFound of int val pr_evar_info : evar_info -> Pp.std_ppcmds val pr_evar_map_constraints : evar_map -> Pp.std_ppcmds -val pr_evar_map : evar_map -> Pp.std_ppcmds +val pr_evar_map : int option -> evar_map -> Pp.std_ppcmds val pr_metaset : Metaset.t -> Pp.std_ppcmds diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 8c05499a2..6e6fff96d 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -519,4 +519,4 @@ let pr_clenv clenv = h 0 (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ - pr_evar_map clenv.evd) + pr_evar_map (Some 2) clenv.evd) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index b685f5041..abd67236a 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -134,6 +134,6 @@ val clenv_conv_leq : exception NotExtensibleClause val clenv_push_prod : clausenv -> clausenv -(** {6 Pretty-print } *) +(** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.std_ppcmds diff --git a/proofs/goal.ml b/proofs/goal.ml index 9be2d028a..0f10c7f84 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Term (* This module implements the abstract interface to goals *) @@ -22,7 +23,7 @@ type goal = { (* spiwack: I don't deal with the tags, yet. It is a worthy discussion whether we do want some tags displayed besides the goal or not. *) -let pr_goal {content = e} = Pp.int e +let pr_goal {content = e} = str "GOAL:" ++ Pp.int e (* access primitive *) (* invariant : [e] must exist in [em] *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5bfdba8a4..5475daa89 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -213,9 +213,9 @@ let db_pr_goal sigma g = str" " ++ pc) ++ fnl () let pr_gls gls = - hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) + hov 0 (pr_evar_map (Some 2) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls)) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b3f4395cf..f3df77379 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -711,7 +711,7 @@ let pr_constraints printenv env evm = str " : " ++ pr_lconstr evi.evar_concl) l ++ fnl() ++ pr_evar_map_constraints evm else - pr_evar_map evm + pr_evar_map None evm let explain_unsatisfiable_constraints env evd constr = let evm = Evarutil.nf_evar_map evd in |