matita/components/binaries/probe/probe.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module A = Arg
  13
  14 module R = Helm_registry
  15 module L = Librarian
  16 module B = NCicLibrary
  17 module C = NCicTypeChecker
  18 module H = HLog
  19
  20 module O = Options
  21 module M = MatitaList
  22 module D = MatitaRemove
  23 module S = NCicScan
  24 module E = Engine
  25 module X = Error
  26
  27 let trusted _ = true
  28
  29 let no_log _ _ = ()
  30
  31 let init registry =
  32   R.load_from registry;
  33   if !O.no_init then begin
  34     B.init ();
  35     C.set_trust trusted;
  36     H.set_log_callback no_log;
  37     O.no_init := false;
  38   end
  39
  40 let scan_uri devel str =
  41   try
  42     M.from_string (R.get "matita.basedir") devel str;
  43     S.scan ()
  44   with
  45   | X.Error s ->
  46     Printf.eprintf "probe: %s\n%!" s
  47
  48 let scan_from devel =
  49   let devel, uri = E.get_uri devel in
  50   scan_uri devel uri
  51
  52 let set_g () = O.exclude := `Generated :: !O.exclude
  53
  54 let set_i () = O.exclude := `Implied :: !O.exclude
  55
  56 let set_p () = O.exclude := `Provided :: !O.exclude
  57
  58 let out_f () = O.iter_xflavours E.out_int
  59
  60 let out_nn () = E.out_length !O.names
  61
  62 let out_ns () = E.out_uris !O.names
  63
  64 let out_oc () = E.out_int !O.net
  65
  66 let out_on () = E.out_length !O.objs
  67
  68 let out_os () = E.out_uris !O.objs
  69
  70 let out_sc () = E.out_int !O.chars
  71
  72 let out_sn () = E.out_length !O.srcs
  73
  74 let out_ss () = E.out_uris !O.srcs
  75
  76 let out_b file = O.out_deps file
  77
  78 let process s =
  79   if L.is_uri s then scan_uri "" s
  80   else if E.is_registry s then init s
  81   else scan_from s
  82
  83 let clear () =
  84   D.objects (); O.clear ()
  85
  86 let _ =
  87   let help = "Usage: probe [ -LX | <configuration file> | -gip | <HELM (base)uri> | -f | -oc | -on | -os | -sc | -sn | -ss  ]*" in
  88   let help_L  = " Activate lexer debugging" in
  89   let help_X  = " Clear configuration, options and counters" in
  90   let help_b  = "<file>  Print backward object dependences in this file" in
  91   let help_f  = " Print the number of objects grouped by flavour" in
  92   let help_g  = " Exclude generated objects" in
  93   let help_i  = " Exclude implied objects" in
  94   let help_nn = " Print the number of names" in
  95   let help_ns = " Print the list of names" in
  96   let help_oc = " Print the total intrinsic complexity (objects)" in
  97   let help_on = " Print the number of objects" in
  98   let help_os = " Print the list of objects" in
  99   let help_p  = " Exclude provided objects" in
 100   let help_sc = " Print the total extrinsic complexity (sources)" in
 101   let help_sn = " Print the number of sources" in
 102   let help_ss = " Print the list of sources" in
 103   A.parse [
 104     "-L" , A.Set O.debug_lexer, help_L;
 105     "-X" , A.Unit clear , help_X;
 106     "-b" , A.String out_b , help_b;
 107     "-f" , A.Unit out_f , help_f;
 108     "-g" , A.Unit set_g , help_g;
 109     "-i" , A.Unit set_i , help_i;
 110     "-nn", A.Unit out_nn, help_nn;
 111     "-ns", A.Unit out_ns, help_ns;
 112     "-oc", A.Unit out_oc, help_oc;
 113     "-on", A.Unit out_on, help_on;
 114     "-os", A.Unit out_os, help_os;
 115     "-p" , A.Unit set_p , help_p;
 116     "-sc", A.Unit out_sc, help_sc;
 117     "-sn", A.Unit out_sn, help_sn;
 118     "-ss", A.Unit out_ss, help_ss;
 119   ] process help;
 120   D.objects ()