]> matita.cs.unibo.it Git - helm.git/commitdiff
probe
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 29 May 2021 12:18:10 +0000 (14:18 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 29 May 2021 12:18:10 +0000 (14:18 +0200)
+ improved error handling

matita/components/binaries/probe/engine.ml
matita/components/binaries/probe/engine.mli
matita/components/binaries/probe/error.ml [new file with mode: 0644]
matita/components/binaries/probe/error.mli [new file with mode: 0644]
matita/components/binaries/probe/matitaList.ml
matita/components/binaries/probe/nCicScan.ml
matita/components/binaries/probe/probe.ml
matita/matita/contribs/lambdadelta/Makefile

index 8a8a74ac545b644aedb95915d0271b222d764150..345f065fec977afc91fda19b548640d0cd5caf9c 100644 (file)
@@ -19,47 +19,38 @@ module B  = Librarian
 module H  = HExtlib
 
 module M = MacLexer
-
-let unsupported protocol =
-   failwith (P.sprintf "probe: unsupported protocol: %s" protocol)
-
-let missing path =
-   failwith (P.sprintf "probe: missing path: %s" path)
-
-let unrooted path roots =
-   failwith (P.sprintf "probe: missing root: %s (found roots: %u)" path (L.length roots))
+module X = Error
 
 let out_int i = P.printf "%u\n" i
 
 let out_length uris = out_int (US.cardinal uris)
 
 let out_uris uris =
-   let map uri = P.printf "%S\n" (U.string_of_uri uri) in
-   US.iter map uris
+  let map uri = P.printf "%S\n" (U.string_of_uri uri) in
+  US.iter map uris
 
 let is_registry str =
-   F.check_suffix str ".conf.xml"
+  F.check_suffix str ".conf.xml"
 
 let get_uri str =
   let str = H.normalize_path str in
   let dir, file =
-      if H.is_regular str && F.check_suffix str ".ma"
-      then F.dirname str, F.chop_extension (F.basename str)
-      else if H.is_dir str then str, ""
-      else missing str
-   in
-   let rec aux bdir file = match B.find_roots_in_dir bdir with
-      | [root] ->
-         let buri = L.assoc "baseuri" (B.load_root_file root) in
-        F.concat bdir file, F.concat buri file
-      | roots  ->
-         if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir roots else
-        aux (F.dirname bdir) (F.concat (F.basename bdir) file)
-   in
-   aux dir file
+    if H.is_regular str && F.check_suffix str ".ma"
+    then F.dirname str, F.chop_extension (F.basename str)
+    else if H.is_dir str then str, ""
+    else X.missing str
+  in
+  let rec aux bdir file = match B.find_roots_in_dir bdir with
+  | [root] ->
+    let buri = L.assoc "baseuri" (B.load_root_file root) in
+    F.concat bdir file, F.concat buri file
+  | roots  ->
+    if bdir = F.current_dir_name || bdir = F.dir_sep then X.unrooted dir roots else
+    aux (F.dirname bdir) (F.concat (F.basename bdir) file)
+  in
+  aux dir file
 
 let mac fname =
-   let ich = open_in fname in
-   let lexbuf = Lexing.from_channel ich in
-   M.token lexbuf; close_in ich
-
+  let ich = open_in fname in
+  let lexbuf = Lexing.from_channel ich in
+  M.token lexbuf; close_in ich
index 5aed039616e6cd94fc6ace6d91d623a6346573ee..432af34c71b84591b5f52b3b3c212f5f8d8b1f33 100644 (file)
@@ -20,7 +20,3 @@ val mac: string -> unit
 val is_registry: string -> bool
 
 val get_uri: string -> string * string
-
-val unsupported: string -> 'a
-
-val missing: string -> 'a
diff --git a/matita/components/binaries/probe/error.ml b/matita/components/binaries/probe/error.ml
new file mode 100644 (file)
index 0000000..598edb1
--- /dev/null
@@ -0,0 +1,30 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
+      V_______________________________________________________________ *)
+
+module L = List
+module P = Printf
+
+exception Error of string
+
+let error s =
+  raise (Error s)
+
+let unsupported protocol =
+  error (P.sprintf "unsupported protocol: %s" protocol)
+
+let missing path =
+  error (P.sprintf "missing path: %s" path)
+
+let unrooted path roots =
+  error (P.sprintf "missing root: %s (found roots: %u)" path (L.length roots))
+
+let malformed () =
+  error "malformed term"
diff --git a/matita/components/binaries/probe/error.mli b/matita/components/binaries/probe/error.mli
new file mode 100644 (file)
index 0000000..35bdf83
--- /dev/null
@@ -0,0 +1,20 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
+      V_______________________________________________________________ *)
+
+exception Error of string
+
+val unsupported: string -> 'a
+
+val missing: string -> 'a
+
+val unrooted: string -> 'b list -> 'a
+
+val malformed: unit -> 'a
index d4ea3e584e6c10d90e46ef17b644e071d835a842..95250b26c13a65888f4af69635227353b7afcd1c 100644 (file)
@@ -21,6 +21,7 @@ module H  = HExtlib
 
 module O = Options
 module E = Engine
+module X = Error
 
 let chop_extension file =
   try F.chop_extension file
@@ -88,8 +89,8 @@ let from_uri base devel uri =
     let file = mk_file path in
     if Y.file_exists (F.concat base file) then
       scan_entry (is_script devel) base devel file
-    else E.missing path
-  else E.unsupported protocol
+    else X.missing path
+  else X.unsupported protocol
 
 let from_string base devel s =
   from_uri base devel (U.uri_of_string s)
index 5b0a106051279fceb94563605f7726c1a37db811..736baafbcc4e67546d7ab09deab874a5473fa487 100644 (file)
@@ -19,6 +19,7 @@ module P  = NCicPp
 module E  = NCicEnvironment
 
 module O  = Options
+module X  = Error
 
 type status = {
 (* current complexity *)
@@ -29,9 +30,6 @@ type status = {
 
 let status = new P.status
 
-let malformed () =
-  failwith "probe: malformed term"
-
 let add_name str =
   let u = U.uri_of_string str in
   if US.mem u !O.names then Printf.eprintf "probe: name clash: %S\n" str;
@@ -86,7 +84,7 @@ let rec scan_term st = function
   | (_, C.Sort _)                :: tl -> scan_term (inc st) tl
   | (c, C.Rel i)                 :: tl -> scan_term (scan_lref st c i) tl
   | (_, C.Const p)               :: tl -> scan_term (scan_gref st p) tl
-  | (_, C.Appl [])               :: tl -> malformed ()
+  | (_, C.Appl [])               :: tl -> X.malformed ()
   | (c, C.Appl ts)               :: tl ->
     scan_term (add st (pred (L.length ts))) (set_list c ts tl)
   | (c, C.Match (_, t0, t1, ts)) :: tl ->
index d118fdab26fb81858a47288ac4e4b4ca011f7875..897148e97e8771c63a640e312fe0ad344d000c90 100644 (file)
@@ -22,27 +22,32 @@ module M = MatitaList
 module D = MatitaRemove
 module S = NCicScan
 module E = Engine
+module X = Error
 
 let trusted _ = true
 
 let no_log _ _ = ()
 
 let init registry =
-   R.load_from registry;
-   if !O.no_init then begin
-      B.init ();
-      C.set_trust trusted;
-      H.set_log_callback no_log;
-      O.no_init := false;
-   end
+  R.load_from registry;
+  if !O.no_init then begin
+    B.init ();
+    C.set_trust trusted;
+    H.set_log_callback no_log;
+    O.no_init := false;
+  end
 
 let scan_uri devel str =
-   M.from_string (R.get "matita.basedir") devel str;
-   S.scan ()
+  try 
+    M.from_string (R.get "matita.basedir") devel str;
+    S.scan ()
+  with
+  | X.Error s ->
+    Printf.eprintf "probe: %s\n%!" s
 
 let scan_from devel =
-   let devel, uri = E.get_uri devel in
-   scan_uri devel uri
+  let devel, uri = E.get_uri devel in
+  scan_uri devel uri
 
 let set_g () = O.exclude := `Generated :: !O.exclude
 
@@ -71,45 +76,45 @@ let out_ss () = E.out_uris !O.srcs
 let out_b file = O.out_deps file
 
 let process s =
-   if L.is_uri s then scan_uri "" s
-   else if E.is_registry s then init s
-   else scan_from s
+  if L.is_uri s then scan_uri "" s
+  else if E.is_registry s then init s
+  else scan_from s
 
 let clear () =
-   D.objects (); O.clear ()
+  D.objects (); O.clear ()
 
 let _ =
-   let help = "Usage: probe [ -LX | <configuration file> | -gip | <HELM (base)uri> | -f | -oc | -on | -os | -sc | -sn | -ss  ]*" in
-   let help_L  = " Activate lexer debugging" in
-   let help_X  = " Clear configuration, options and counters" in
-   let help_b  = "<file>  Print backward object dependences in this file" in
-   let help_f  = " Print the number of objects grouped by flavour" in
-   let help_g  = " Exclude generated objects" in
-   let help_i  = " Exclude implied objects" in
-   let help_nn = " Print the number of names" in
-   let help_ns = " Print the list of names" in
-   let help_oc = " Print the total intrinsic complexity (objects)" in
-   let help_on = " Print the number of objects" in
-   let help_os = " Print the list of objects" in
-   let help_p  = " Exclude provided objects" in
-   let help_sc = " Print the total extrinsic complexity (sources)" in
-   let help_sn = " Print the number of sources" in
-   let help_ss = " Print the list of sources" in
-   A.parse [
-      "-L" , A.Set O.debug_lexer, help_L;
-      "-X" , A.Unit clear , help_X;
-      "-b" , A.String out_b , help_b;
-      "-f" , A.Unit out_f , help_f;
-      "-g" , A.Unit set_g , help_g;
-      "-i" , A.Unit set_i , help_i;
-      "-nn", A.Unit out_nn, help_nn;
-      "-ns", A.Unit out_ns, help_ns;
-      "-oc", A.Unit out_oc, help_oc;
-      "-on", A.Unit out_on, help_on;
-      "-os", A.Unit out_os, help_os;
-      "-p" , A.Unit set_p , help_p;
-      "-sc", A.Unit out_sc, help_sc;
-      "-sn", A.Unit out_sn, help_sn;
-      "-ss", A.Unit out_ss, help_ss;
-   ] process help;
-   D.objects ()
+  let help = "Usage: probe [ -LX | <configuration file> | -gip | <HELM (base)uri> | -f | -oc | -on | -os | -sc | -sn | -ss  ]*" in
+  let help_L  = " Activate lexer debugging" in
+  let help_X  = " Clear configuration, options and counters" in
+  let help_b  = "<file>  Print backward object dependences in this file" in
+  let help_f  = " Print the number of objects grouped by flavour" in
+  let help_g  = " Exclude generated objects" in
+  let help_i  = " Exclude implied objects" in
+  let help_nn = " Print the number of names" in
+  let help_ns = " Print the list of names" in
+  let help_oc = " Print the total intrinsic complexity (objects)" in
+  let help_on = " Print the number of objects" in
+  let help_os = " Print the list of objects" in
+  let help_p  = " Exclude provided objects" in
+  let help_sc = " Print the total extrinsic complexity (sources)" in
+  let help_sn = " Print the number of sources" in
+  let help_ss = " Print the list of sources" in
+  A.parse [
+    "-L" , A.Set O.debug_lexer, help_L;
+    "-X" , A.Unit clear , help_X;
+    "-b" , A.String out_b , help_b;
+    "-f" , A.Unit out_f , help_f;
+    "-g" , A.Unit set_g , help_g;
+    "-i" , A.Unit set_i , help_i;
+    "-nn", A.Unit out_nn, help_nn;
+    "-ns", A.Unit out_ns, help_ns;
+    "-oc", A.Unit out_oc, help_oc;
+    "-on", A.Unit out_on, help_on;
+    "-os", A.Unit out_os, help_os;
+    "-p" , A.Unit set_p , help_p;
+    "-sc", A.Unit out_sc, help_sc;
+    "-sn", A.Unit out_sn, help_sn;
+    "-ss", A.Unit out_ss, help_ss;
+  ] process help;
+  D.objects ()
index 8d6f2ccd2f60da89d179693bdb6bc2a618e44407..dc13cc1561ad288013ab4681a6885f83578a5341 100644 (file)
@@ -186,7 +186,7 @@ define SUMMARY_TEMPLATE
   $$(SUM_$(1)): S2 = $$(word 2, $$(C0))
   $$(SUM_$(1)): S3 = $$(word 3, $$(C0))
   $$(SUM_$(1)): S4 = $$(word 4, $$(C0))
-  $$(SUM_$(1)): S5 = $$(shell printf "%.1f" `echo "scale=2;$$(S4)/$$(S2)"|bc`)
+  $$(SUM_$(1)): S5 = $$(shell printf "%.1f" `echo "scale=2;if($$(S2)!=0)$$(S4)/$$(S2) else 0"|bc`)
   $$(SUM_$(1)): C1 = $$(word 5, $$(C0))
   $$(SUM_$(1)): C2 = $$(word 7, $$(C0))
   $$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc)