diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-21 16:54:38 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-21 16:54:38 +0000 |
commit | d09af1d5ca8bb610cec40918b23be67ba6f9673f (patch) | |
tree | a0ffa9b6df25e44b7ce51aa6017781f9bac2f84a /checker/check_stat.ml | |
parent | 2407beea26ae531431db3123ecba6a08acd4e3e2 (diff) |
added the .vo checker (with independent Makefile)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/check_stat.ml')
-rw-r--r-- | checker/check_stat.ml | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml new file mode 100644 index 000000000..963665946 --- /dev/null +++ b/checker/check_stat.ml @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open System +open Flags +open Names +open Term +open Declarations +open Environ + +let memory_stat = ref false + +let print_memory_stat () = + if !memory_stat then begin + Format.printf "total heap size = %d kbytes\n" (heap_size_kb ()); + Format.print_newline(); + flush_all() + end + +let output_context = ref false + +let pr_engt = function + Some ImpredicativeSet -> + str "Theory: Set is impredicative" + | None -> + str "Theory: Set is predicative" + +let cst_filter f csts = + Cmap.fold + (fun c ce acc -> if f c ce then c::acc else acc) + csts [] + +let is_ax _ cb = cb.const_body = None + +let pr_ax csts = + let axs = cst_filter is_ax csts in + if axs = [] then + str "Axioms: <none>" + else + hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Indtypes.prcon axs) + +let print_context env = + if !output_context then begin + let + {env_globals= + {env_constants=csts; env_inductives=inds; + env_modules=mods; env_modtypes=mtys}; + env_stratification= + {env_universes=univ; env_engagement=engt}} = env in + msgnl(hov 0 + (str"CONTEXT SUMMARY" ++ fnl() ++ + str"===============" ++ fnl() ++ fnl() ++ + str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_ax csts) ++ + fnl())) + end + +let stats () = + print_context (Safe_typing.get_env()); + print_memory_stat () + +let _ = at_exit stats |