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 S = NCicScan
  23 module E = Engine
  24
  25 let trusted _ = true
  26
  27 let no_log _ _ = ()
  28
  29 let init registry =
  30    R.load_from registry;
  31    B.init ();
  32    C.set_trust trusted;
  33    H.set_log_callback no_log
  34
  35 let scan str =
  36    M.from_string (R.get "matita.basedir") str;
  37    S.scan ()
  38
  39 let set_g () = O.exclude := `Generated :: !O.exclude
  40
  41 let set_p () = O.exclude := `Provided :: !O.exclude
  42
  43 let out_i () = E.out_int !O.net
  44
  45 let out_on () = E.out_length !O.objs
  46
  47 let out_os () = E.out_uris !O.objs
  48
  49 let out_sn () = E.out_length !O.srcs
  50
  51 let out_ss () = E.out_uris !O.srcs
  52
  53 let process s =
  54    if L.is_uri s then scan s else init s
  55
  56 let _ =
  57    let help = "Usage: probe [ -X | <configuration file> | -gp | HELM (base)uri | -i | -on | os | -sn | -ss  ]*" in
  58    let help_X  = " Reset options and counters" in
  59    let help_g  = " Exclude generated objects" in
  60    let help_i  = " Print the total intrinsic size" in
  61    let help_p  = " Exclude provided objects" in
  62    let help_on = " Print the number of objects" in
  63    let help_os = " Print the list of objects" in
  64    let help_sn = " Print the number of sources" in
  65    let help_ss = " Print the list of sources" in
  66    A.parse [
  67       "-X" , A.Unit O.clear, help_X;
  68       "-g" , A.Unit set_g, help_g;
  69       "-i" , A.Unit out_i, help_i;
  70       "-p" , A.Unit set_p, help_p;
  71       "-on", A.Unit out_on, help_on;
  72       "-os", A.Unit out_os, help_os;
  73       "-sn", A.Unit out_sn, help_sn;
  74       "-ss", A.Unit out_ss, help_ss;
  75    ] process help