From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
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 | <configuration file> | -gip | HELM (base)uri | -c | -on | os | -sn | -ss  ]*" in
+   let help = "Usage: probe [ -X | <configuration file> | -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;