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
  26 let trusted _ = true
  27
  28 let no_log _ _ = ()
  29
  30 let init registry =
  31    R.load_from registry;
  32    if !O.no_init then begin
  33       B.init ();
  34       C.set_trust trusted;
  35       H.set_log_callback no_log;
  36       O.no_init := false;
  37    end
  38
  39 let scan_uri devel str =
  40    M.from_string (R.get "matita.basedir") devel str;
  41    S.scan ()
  42
  43 let scan_from devel =
  44    let devel, uri = E.get_uri devel in
  45    scan_uri devel uri
  46
  47 let set_g () = O.exclude := `Generated :: !O.exclude
  48
  49 let set_i () = O.exclude := `Implied :: !O.exclude
  50
  51 let set_p () = O.exclude := `Provided :: !O.exclude
  52
  53 let out_c () = E.out_int !O.net
  54
  55 let out_on () = E.out_length !O.objs
  56
  57 let out_os () = E.out_uris !O.objs
  58
  59 let out_sn () = E.out_length !O.srcs
  60
  61 let out_ss () = E.out_uris !O.srcs
  62
  63 let process s =
  64    if L.is_uri s then scan_uri "" s
  65    else if E.is_registry s then init s
  66    else scan_from s
  67
  68 let clear () =
  69    D.objects (); O.clear ()
  70
  71 let _ =
  72    let help = "Usage: probe [ -X | <configuration file> | -gip | HELM (base)uri | -c | -on | os | -sn | -ss  ]*" in
  73    let help_X  = " Clear configuration, options and counters" in
  74    let help_c  = " Print the total intrinsic complexity" in
  75    let help_g  = " Exclude generated objects" in
  76    let help_i  = " Exclude implied objects" in
  77    let help_p  = " Exclude provided objects" in
  78    let help_on = " Print the number of objects" in
  79    let help_os = " Print the list of objects" in
  80    let help_sn = " Print the number of sources" in
  81    let help_ss = " Print the list of sources" in
  82    A.parse [
  83       "-X" , A.Unit clear, help_X;
  84       "-c" , A.Unit out_c, help_c;
  85       "-g" , A.Unit set_g, help_g;
  86       "-i" , A.Unit set_i, help_i;
  87       "-on", A.Unit out_on, help_on;
  88       "-os", A.Unit out_os, help_os;
  89       "-p" , A.Unit set_p, help_p;
  90       "-sn", A.Unit out_sn, help_sn;
  91       "-ss", A.Unit out_ss, help_ss;
  92    ] process help;
  93    D.objects ()