From: Ferruccio Guidi Date: Thu, 24 Mar 2016 12:23:19 +0000 (+0000) Subject: support for printing the number of objects grouped by flavour X-Git-Tag: make_still_working~625 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c62bc0725203409f99fd10eaf0b670a406e311b3;p=helm.git support for printing the number of objects grouped by flavour --- diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml index e9c6a2448..fc6957292 100644 --- a/matita/components/binaries/probe/nCicScan.ml +++ b/matita/components/binaries/probe/nCicScan.ml @@ -25,6 +25,10 @@ let status = new P.status let malformed () = failwith "probe: malformed term" +let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour) + +let add_ind n = O.add_xflavour n `Inductive + let rec set_list c ts cts = let map cts t = (c, t) :: cts in L.fold_left map cts ts @@ -74,13 +78,17 @@ let rec scan_term a = function let scan_obj u a = let _, _, _, _, obj = E.get_checked_obj status u in match obj with - | C.Constant (_, _, None, t, _) -> + | C.Constant (_, _, None, t, m) -> + add_attr 1 m; scan_term (succ a) [[], t] - | C.Constant (_, _, Some t0, t1, _) -> + | C.Constant (_, _, Some t0, t1, m) -> + add_attr 1 m; scan_term (succ a) (set_list [] [t0; t1] []) - | C.Fixpoint (_, rfs, _) -> + | C.Fixpoint (_, rfs, m) -> + add_attr (L.length rfs) m; scan_term (a + L.length rfs) (set_funs [] rfs []) | C.Inductive (_, _, its, _) -> + add_ind (L.length its); let cts = L.fold_left (set_type []) [] its in scan_term (a + L.length cts) cts diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml index 4c3c51d12..655539d14 100644 --- a/matita/components/binaries/probe/options.ml +++ b/matita/components/binaries/probe/options.ml @@ -9,9 +9,17 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module A = Array +module P = Printf + +module C = NCic module R = Helm_registry module US = NUri.UriSet +type def_xflavour = [ C.def_flavour + | `Inductive + ] + let default_objs = US.empty let default_srcs = US.empty @@ -26,6 +34,10 @@ let default_no_devel = true let default_no_init = true +let xflavours = 8 + +let slot = A.make xflavours 0 + let objs = ref default_objs let srcs = ref default_srcs @@ -40,8 +52,26 @@ let no_devel = ref default_no_devel let no_init = ref default_no_init +let index_of_xflavour = function + | `Inductive -> 0 + | `Axiom -> 1 + | `Definition -> 2 + | `Fact -> 3 + | `Lemma -> 4 + | `Theorem -> 5 + | `Corollary -> 6 + | `Example -> 7 + +let add_xflavour n xf = + let i = index_of_xflavour xf in + slot.(i) <- slot.(i) + n + +let clear_slot i _ = slot.(i) <- 0 + +let iter_xflavours map = A.iteri (fun _ -> map) slot + let clear () = - R.clear (); + R.clear (); A.iteri clear_slot slot; objs := default_objs; srcs := default_srcs; remove := default_remove; exclude := default_exclude; net := default_net; no_devel := default_no_devel; no_init := default_no_init diff --git a/matita/components/binaries/probe/options.mli b/matita/components/binaries/probe/options.mli index a692c9013..7b99bf535 100644 --- a/matita/components/binaries/probe/options.mli +++ b/matita/components/binaries/probe/options.mli @@ -9,6 +9,14 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +type def_xflavour = [ NCic.def_flavour + | `Inductive + ] + +val add_xflavour: int -> def_xflavour -> unit + +val iter_xflavours: (int -> unit) -> unit + val objs: NUri.UriSet.t ref val srcs: NUri.UriSet.t ref diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml index 748826be1..e3d8f6cc9 100644 --- a/matita/components/binaries/probe/probe.ml +++ b/matita/components/binaries/probe/probe.ml @@ -52,6 +52,8 @@ let set_p () = O.exclude := `Provided :: !O.exclude let out_c () = E.out_int !O.net +let out_f () = O.iter_xflavours E.out_int + let out_on () = E.out_length !O.objs let out_os () = E.out_uris !O.objs @@ -69,10 +71,11 @@ let clear () = D.objects (); O.clear () let _ = - let help = "Usage: probe [ -X | | -gip | HELM (base)uri | -c | -on | os | -sn | -ss ]*" in + let help = "Usage: probe [ -X | | -gip | HELM (base)uri | -cf | -on | os | -sn | -ss ]*" in let help_X = " Clear configuration, options and counters" in let help_c = " Print the total intrinsic complexity" in let help_g = " Exclude generated objects" in + let help_f = " Print the number of objects grouped by flavour" in let help_i = " Exclude implied objects" in let help_p = " Exclude provided objects" in let help_on = " Print the number of objects" in @@ -82,6 +85,7 @@ let _ = A.parse [ "-X" , A.Unit clear, help_X; "-c" , A.Unit out_c, help_c; + "-f" , A.Unit out_f, help_f; "-g" , A.Unit set_g, help_g; "-i" , A.Unit set_i, help_i; "-on", A.Unit out_on, help_on;