+++ /dev/null
-EXEC = mac
-VERSION=0.1.0
-
-REQUIRES =
-
-include ../Makefile.common
+++ /dev/null
-(*
- ||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 O = Options
-
- let out s = if !O.debug_lexer then prerr_endline s
-}
-
-let OL = "(*"
-let CL = "*)"
-let UNI = ['\x80'-'\xBF']+
-let SPC = ['\r' '\n' '\t' ' ']+
-let WRD = ['0'-'9' 'A'-'Z' 'a'-'z' '_']+
-let QT = '"'
-
-rule token = parse
- | OL { out "COM"; block lexbuf; token lexbuf }
- | QT { out "STR"; O.count := !O.count + str lexbuf; token lexbuf }
- | SPC { out "SPC"; incr O.count; token lexbuf }
- | UNI { out "UNI"; incr O.count; token lexbuf }
- | WRD { out "WRD"; incr O.count; token lexbuf }
- | _ { out "CHR"; incr O.count; token lexbuf }
- | eof { out "EOF" }
-and str = parse
- | QT { 2 }
- | "\\\"" { succ (str lexbuf) }
- | UNI { succ (str lexbuf) }
- | WRD { succ (str lexbuf) }
- | _ { succ (str lexbuf) }
-and block = parse
- | CL { () }
- | OL { block lexbuf; block lexbuf }
- | QT { let _ = str lexbuf in block lexbuf }
- | _ { block lexbuf }
+++ /dev/null
-(*
- ||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 A = Arg
-module P = Printf
-
-module O = Options
-module L = Lexer
-
-let help = "Usage: mac [ -LXQV | -p <int> ]* [ <file> ]*"
-let help_L = " Activate lexer debugging"
-let help_Q = " Read data from standard input"
-let help_V = " Show version information"
-let help_X = " Reset options and counters"
-let help_p = "<int> Assume <int> characters per page (default: 5120)"
-
-let active = ref false
-
-let process_channel ich =
- let lexbuf = Lexing.from_channel ich in
- L.token lexbuf; active := true
-
-let output_version () =
- P.printf "mac 0.1.1 M - July 2013\n"
-
-let process_stdin () =
- process_channel stdin
-
-let process_file fname =
- let ich = open_in fname in
- process_channel ich; close_in ich
-
-let set_page i =
- if i > 0 then O.page := i
-
-let output_count () =
- if !active then
- let pages = !O.count / !O.page in
- let pages = if !O.count mod !O.page = 0 then pages else succ pages in
- P.printf "%u %u\n" !O.count pages
-
-let main () =
- A.parse [
- "-L", A.Set O.debug_lexer, help_L;
- "-Q", Arg.Unit process_stdin, help_Q;
- "-V", Arg.Unit output_version, help_V;
- "-X", A.Unit O.clear, help_X;
- ] process_file help;
- output_count ()
-
-let _ = main ()
+++ /dev/null
-(*
- ||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_______________________________________________________________ *)
-
-let debug_lexer_default = false
-
-let count_default = 0
-
-let page_default = 5120
-
-let debug_lexer = ref debug_lexer_default
-
-let count = ref count_default
-
-let page = ref page_default
-
-let clear () =
- debug_lexer := debug_lexer_default;
- count := count_default;
- page := page_default
+++ /dev/null
-(*
- ||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_______________________________________________________________ *)
-
-val debug_lexer: bool ref
-
-val count: int ref
-
-val page: int ref
-
-val clear: unit -> unit
module B = Librarian
module H = HExtlib
+module M = MacLexer
+
let unsupported protocol =
failwith (P.sprintf "probe: unsupported protocol: %s" protocol)
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
+
val out_uris: NUri.UriSet.t -> unit
+val mac: string -> unit
+
val is_registry: string -> bool
val get_uri: string -> string * string
--- /dev/null
+(*
+ ||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 A = Arg
+module P = Printf
+
+module O = Options
+module L = Lexer
+
+let help = "Usage: mac [ -LXQV | -p <int> ]* [ <file> ]*"
+let help_L = " Activate lexer debugging"
+let help_Q = " Read data from standard input"
+let help_V = " Show version information"
+let help_X = " Reset options and counters"
+let help_p = "<int> Assume <int> characters per page (default: 5120)"
+
+let active = ref false
+
+let process_channel ich =
+ let lexbuf = Lexing.from_channel ich in
+ L.token lexbuf; active := true
+
+let output_version () =
+ P.printf "mac 0.1.1 M - July 2013\n"
+
+let process_stdin () =
+ process_channel stdin
+
+let process_file fname =
+ let ich = open_in fname in
+ process_channel ich; close_in ich
+
+let set_page i =
+ if i > 0 then O.page := i
+
+let output_count () =
+ if !active then
+ let pages = !O.count / !O.page in
+ let pages = if !O.count mod !O.page = 0 then pages else succ pages in
+ P.printf "%u %u\n" !O.count pages
+
+let main () =
+ A.parse [
+ "-L", A.Set O.debug_lexer, help_L;
+ "-Q", Arg.Unit process_stdin, help_Q;
+ "-V", Arg.Unit output_version, help_V;
+ "-X", A.Unit O.clear, help_X;
+ ] process_file help;
+ output_count ()
+
+let _ = main ()
--- /dev/null
+(*
+ ||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 O = Options
+
+ let out s = if !O.debug_lexer then prerr_endline s
+}
+
+let OL = "(*"
+let CL = "*)"
+let UNI = ['\x80'-'\xBF']+
+let SPC = ['\r' '\n' '\t' ' ']+
+let WRD = ['0'-'9' 'A'-'Z' 'a'-'z' '_']+
+let QT = '"'
+
+rule token = parse
+ | OL { out "COM"; block lexbuf; token lexbuf }
+ | QT { out "STR"; O.chars := !O.chars + str lexbuf; token lexbuf }
+ | SPC { out "SPC"; incr O.chars; token lexbuf }
+ | UNI { out "UNI"; incr O.chars; token lexbuf }
+ | WRD { out "WRD"; incr O.chars; token lexbuf }
+ | _ { out "CHR"; incr O.chars; token lexbuf }
+ | eof { out "EOF" }
+and str = parse
+ | QT { 2 }
+ | "\\\"" { succ (str lexbuf) }
+ | UNI { succ (str lexbuf) }
+ | WRD { succ (str lexbuf) }
+ | _ { succ (str lexbuf) }
+and block = parse
+ | CL { () }
+ | OL { block lexbuf; block lexbuf }
+ | QT { let _ = str lexbuf in block lexbuf }
+ | _ { block lexbuf }
try F.chop_extension file
with Invalid_argument("Filename.chop_extension") -> file
+let script devel = chop_extension devel ^ ".ma"
+
let src_exists path = !O.no_devel || Y.file_exists path
let is_obj base path =
H.is_dir (F.concat base path)
let is_script devel =
- src_exists (chop_extension devel ^ ".ma")
+ src_exists (script devel)
let mk_file path =
if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
let add_src devel path =
let path = F.chop_extension path in
let str = F.concat "cic:" path ^ "/" in
- O.srcs := US.add (U.uri_of_string str) !O.srcs
+ O.srcs := US.add (U.uri_of_string str) !O.srcs;
+ E.mac (script devel)
let add_remove base path =
O.remove := F.concat base path :: !O.remove
let default_net = 0
+let default_chars = 0
+
+let default_debug_lexer = false
+
let default_no_devel = true
let default_no_init = true
let net = ref default_net
+let chars = ref default_chars
+
+let debug_lexer = ref default_debug_lexer
+
let no_devel = ref default_no_devel
let no_init = ref default_no_init
R.clear (); A.iteri clear_slot slot;
objs := default_objs; srcs := default_srcs; remove := default_remove;
exclude := default_exclude; net := default_net;
+ chars := default_chars; debug_lexer := default_debug_lexer;
no_devel := default_no_devel; no_init := default_no_init
val net: int ref
+val chars: int ref
+
+val debug_lexer: bool ref
+
val no_devel: bool ref
val no_init: bool ref
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_oc () = E.out_int !O.net
+
let out_on () = E.out_length !O.objs
let out_os () = E.out_uris !O.objs
-let out_sn () = E.out_length !O.srcs
+let out_sc () = E.out_int !O.chars
+
+let out_sn () = E.out_length !O.srcs
let out_ss () = E.out_uris !O.srcs
D.objects (); O.clear ()
let _ =
- let help = "Usage: probe [ -X | <configuration file> | -gip | HELM (base)uri | -cf | -on | os | -sn | -ss ]*" in
+ 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_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_g = " Exclude generated objects" in
let help_i = " Exclude implied objects" in
- let help_p = " Exclude provided objects" 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 [
- "-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;
+ "-L" , A.Set O.debug_lexer, help_L;
+ "-X" , A.Unit clear , help_X;
+ "-f" , A.Unit out_f , help_f;
+ "-g" , A.Unit set_g , help_g;
+ "-i" , A.Unit set_i , help_i;
+ "-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;
+ "-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;
$(1)/$(1)_probe.txt: $$(MAS_$(1))
@echo " PROBE $(1)"
- $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -on -c > $$@
+ $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -sc -on -oc -f > $$@
$(1)/$(1)_mac.txt: $$(MAS_$(1))
@echo " MAC $(1)"
SUMS += $$(SUM_$(1))
$$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt)
- $$(SUM_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt)
- $$(SUM_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l)
- $$(SUM_$(1)): C1 = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l)
- $$(SUM_$(1)): C2 = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l)
- $$(SUM_$(1)): C3 = $$(shell grep "^inductive \|^record \|^definition \|^let rec " $$(MAS_$(1)) | wc -l)
- $$(SUM_$(1)): P1 = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l)
- $$(SUM_$(1)): P2 = $$(shell grep "^lemma " $$(MAS_$(1)) | wc -l)
- $$(SUM_$(1)): P3 = $$(shell grep "^lemma \|^theorem " $$(MAS_$(1)) | wc -l)
-
- $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt $(1)/$(1)_mac.txt
+ $$(SUM_$(1)): S1 = $$(word 1, $$(S0))
+ $$(SUM_$(1)): S2 = $$(word 2, $$(S0))
+ $$(SUM_$(1)): S4 = $$(word 4, $$(S0))
+ $$(SUM_$(1)): C1 = $$(word 5, $$(S0))
+ $$(SUM_$(1)): C2 = $$(word 7, $$(S0))
+ $$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc)
+ $$(SUM_$(1)): P1 = $$(word 10, $$(S0))
+ $$(SUM_$(1)): P2 = $$(word 9, $$(S0))
+ $$(SUM_$(1)): P3 = $$(shell echo "$$(P1)+$$(P2)"|bc)
+
+ $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt
@printf ' SUMMARY $(1)\n'
@printf 'name "$$(basename $$(@F))"\n\n' > $$@
@printf 'table {\n' >> $$@
@printf ' [ "objects" * ]\n' >> $$@
@printf ' ]\n' >> $$@
@printf ' class "cyan" [ "sizes"\n' >> $$@
- @printf ' [ "files" "$$(S4)" ]\n' >> $$@
- @printf ' [ "characters" "$$(word 1, $$(S1))" ]\n' >> $$@
- @printf ' [ "nodes" "$$(word 3, $$(S0))" ]\n' >> $$@
+ @printf ' [ "files" "$$(S1)" ]\n' >> $$@
+ @printf ' [ "characters" "$$(S2)" ]\n' >> $$@
+ @printf ' [ "nodes" "$$(S4)" ]\n' >> $$@
@printf ' ]\n' >> $$@
@printf ' class "green" [ "propositions"\n' >> $$@
@printf ' [ "theorems" "$$(P1)" ]\n' >> $$@
projects / helm.git / commitdiff