From 9f47f7b4e9b99484b02b3b6f4d71a049b3389565 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 9 Nov 2012 18:56:55 +0000 Subject: [PATCH] - mac (ma count) small program to count the number of characters (not bytes) in a .ma file excluding (possibly nested) comments, repeated spaces, and escape characters in strings - lambda_delta: Makefile updated to use mac --- matita/components/binaries/mac/Makefile | 6 +++ matita/components/binaries/mac/lexer.mll | 29 ++++++++++++++ matita/components/binaries/mac/mac.ml | 41 ++++++++++++++++++++ matita/components/binaries/mac/options.ml | 11 ++++++ matita/matita/contribs/lambda_delta/Makefile | 38 +++++++++--------- 5 files changed, 107 insertions(+), 18 deletions(-) create mode 100644 matita/components/binaries/mac/Makefile create mode 100644 matita/components/binaries/mac/lexer.mll create mode 100644 matita/components/binaries/mac/mac.ml create mode 100644 matita/components/binaries/mac/options.ml diff --git a/matita/components/binaries/mac/Makefile b/matita/components/binaries/mac/Makefile new file mode 100644 index 000000000..2a738628f --- /dev/null +++ b/matita/components/binaries/mac/Makefile @@ -0,0 +1,6 @@ +EXEC = mac +VERSION=0.1.0 + +REQUIRES = + +include ../Makefile.common diff --git a/matita/components/binaries/mac/lexer.mll b/matita/components/binaries/mac/lexer.mll new file mode 100644 index 000000000..4068879ec --- /dev/null +++ b/matita/components/binaries/mac/lexer.mll @@ -0,0 +1,29 @@ +{ + 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 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"; token lexbuf } + | _ { out "CHR"; incr O.count; token lexbuf } + | eof { out "EOF" } +and str = parse + | QT { 2 } + | "\\\"" { succ (str lexbuf) } + | UNI { str lexbuf } + | _ { succ (str lexbuf) } +and block = parse + | CL { () } + | OL { block lexbuf; block lexbuf } + | QT { let _ = str lexbuf in block lexbuf } + | _ { block lexbuf } diff --git a/matita/components/binaries/mac/mac.ml b/matita/components/binaries/mac/mac.ml new file mode 100644 index 000000000..d5826e619 --- /dev/null +++ b/matita/components/binaries/mac/mac.ml @@ -0,0 +1,41 @@ +module A = Arg +module P = Printf + +module O = Options +module L = Lexer + +let help = "Usage: mac [ -LX ]* [ ]*" +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 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.0 M - November 2012\n" + +let process_stdin () = + process_channel stdin + +let process_file fname = + let ich = open_in fname in + process_channel ich; close_in ich + +let output_count () = + if !active then P.printf "%u\n" !O.count + +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 () diff --git a/matita/components/binaries/mac/options.ml b/matita/components/binaries/mac/options.ml new file mode 100644 index 000000000..937924671 --- /dev/null +++ b/matita/components/binaries/mac/options.ml @@ -0,0 +1,11 @@ +let debug_lexer_default = false + +let count_default = 0 + +let debug_lexer = ref debug_lexer_default + +let count = ref count_default + +let clear () = + debug_lexer := debug_lexer_default; + count := count_default diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index a1bea3529..7d2fee6bf 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -3,9 +3,11 @@ XOA_DIR = ../../../components/binaries/xoa XOA = xoa.native DEP_DIR = ../../../components/binaries/matitadep DEP = matitadep.native +MAC_DIR = ../../../components/binaries/mac +MAC = mac.native -CONF = ground_2/xoa.conf.xml -TARGETS = ground_2/xoa_natation.ma ground_2/xoa.ma +XOA_CONF = ground_2/xoa.conf.xml +XOA_TARGETS = ground_2/xoa_natation.ma ground_2/xoa.ma ORIG = . ./orig.sh @@ -19,9 +21,9 @@ all: xoa: $(TARGETS) -$(TARGETS): $(CONF) - @echo " EXEC $(XOA) $(CONF)" - $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(CONF) +$(XOA_TARGETS): $(XOA_CONF) + @echo " EXEC $(XOA) $(XOA_CONF)" + $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_CONF) # orig ####################################################################### @@ -43,39 +45,39 @@ stats: $(PACKAGES:%=%.stats) %.stats: MAS = $(shell find $* -name "*.ma") -%.stats: CHARS = $(shell cat $(MAS) | wc -c) +%.stats: CHARS = $(shell $(MAC_DIR)/$(MAC) $(MAS)) %.stats: @printf '\x1B[1;40;37m' - @printf '%-15s %-43s' 'Statistics for:' $* + @printf '%-15s %-40s' 'Statistics for:' $* @printf '\x1B[0m\n' @printf '\x1B[1;40;35m' @printf '%-8s %6i' Chars $(CHARS) - @printf ' %-8s %5i' Lines `cat $(MAS) | wc -l` - @printf ' %-6s %3i' Pages `echo $$(($(CHARS) / 5120))` - @printf ' %-11s' '' + @printf ' %-8s %3i' Pages `echo $$(($(CHARS) / 5120))` + @printf ' %-23s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;36m' @printf '%-8s %6i' Sources `ls $(MAS) | wc -l` - @printf ' %-41s' '' + @printf ' %-38s' '' # @printf ' %-8s %5i' Objs `ls *.vo | wc -l` # @printf ' %-6s %3i' Files `ls *.v | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;32m' @printf '%-8s %6i' Theorems `grep "theorem " $(MAS) | wc -l` - @printf ' %-8s %5i' Lemmas `grep "lemma " $(MAS) | wc -l` - @printf ' %-6s %3i' Facts `grep "fact " $(MAS) | wc -l` + @printf ' %-8s %3i' Lemmas `grep "lemma " $(MAS) | wc -l` + @printf ' %-5s %3i' Facts `grep "fact " $(MAS) | wc -l` @printf ' %-6s %4i' Proofs `grep qed $(MAS) | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;33m' - @printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l` - @printf ' %-41s' '' + @printf '%-8s %6i' Declared `grep "inductive \|record " $(MAS) | wc -l` + @printf ' %-8s %3i' Defined `grep "definition \|let rec " $(MAS) | wc -l` + @printf ' %-23s' '' # @printf ' %-8s %5i' Local `grep "Local" *.v | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;31m' @printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l` - @printf ' %-8s %5i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l` - @printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` + @printf ' %-8s %3i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l` + @printf ' %-5s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` @printf ' %-11s' '' @printf '\x1B[0m\n' @@ -87,7 +89,7 @@ define SUMMARY_TEMPLATE TBLS += $$(TBL_$(1)) $$(TBL_$(1)): V1 := $$(shell ls $$(MAS_$(1)) | wc -l) - $$(TBL_$(1)): V2 := $$(shell cat $$(MAS_$(1)) | wc -c) + $$(TBL_$(1)): V2 := $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1))) $$(TBL_$(1)): C1 := $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l) $$(TBL_$(1)): C2 := $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l) $$(TBL_$(1)): C3 := $$(shell grep "inductive \|record \|definition \|let rec " $$(MAS_$(1)) | wc -l) -- 2.39.2