From cbbbc763dc971b43fe74f1d08b797de5d1dc4f17 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 1 Jan 2013 23:01:20 +0000 Subject: [PATCH] - probe: new application to compute some data on the proof objects of a development, such as their net size (aka intrinsinc complexity) - lambdadelta: Makefile now asks "probe" fore some data --- matita/components/binaries/probe/Makefile | 6 ++ matita/components/binaries/probe/engine.ml | 23 +++++ matita/components/binaries/probe/engine.mli | 16 +++ .../components/binaries/probe/matitaList.ml | 63 ++++++++++++ .../components/binaries/probe/matitaList.mli | 14 +++ matita/components/binaries/probe/nCicScan.ml | 98 +++++++++++++++++++ matita/components/binaries/probe/nCicScan.mli | 12 +++ matita/components/binaries/probe/options.ml | 30 ++++++ matita/components/binaries/probe/options.mli | 20 ++++ matita/components/binaries/probe/probe.ml | 75 ++++++++++++++ matita/matita/contribs/lambdadelta/Makefile | 98 ++++++++++++------- 11 files changed, 420 insertions(+), 35 deletions(-) create mode 100644 matita/components/binaries/probe/Makefile create mode 100644 matita/components/binaries/probe/engine.ml create mode 100644 matita/components/binaries/probe/engine.mli create mode 100644 matita/components/binaries/probe/matitaList.ml create mode 100644 matita/components/binaries/probe/matitaList.mli create mode 100644 matita/components/binaries/probe/nCicScan.ml create mode 100644 matita/components/binaries/probe/nCicScan.mli create mode 100644 matita/components/binaries/probe/options.ml create mode 100644 matita/components/binaries/probe/options.mli create mode 100644 matita/components/binaries/probe/probe.ml diff --git a/matita/components/binaries/probe/Makefile b/matita/components/binaries/probe/Makefile new file mode 100644 index 000000000..24daac41d --- /dev/null +++ b/matita/components/binaries/probe/Makefile @@ -0,0 +1,6 @@ +EXEC = probe +VERSION=0.1.0 + +REQUIRES = helm-ng_library + +include ../Makefile.common diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml new file mode 100644 index 000000000..e79f000f9 --- /dev/null +++ b/matita/components/binaries/probe/engine.ml @@ -0,0 +1,23 @@ +(* + ||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 + +module U = NUri + +let out_uris uris = + let map uri = P.printf "%s\n" (U.string_of_uri uri) in + L.iter map uris + +let out_int i = P.printf "%u\n" i + +let out_length l = out_int (L.length l) diff --git a/matita/components/binaries/probe/engine.mli b/matita/components/binaries/probe/engine.mli new file mode 100644 index 000000000..7f3b5a2ca --- /dev/null +++ b/matita/components/binaries/probe/engine.mli @@ -0,0 +1,16 @@ +(* + ||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 out_uris: NUri.uri list -> unit + +val out_int: int -> unit + +val out_length: 'a list -> unit diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml new file mode 100644 index 000000000..a2ce7d908 --- /dev/null +++ b/matita/components/binaries/probe/matitaList.ml @@ -0,0 +1,63 @@ +(* + ||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 = Array +module F = Filename +module P = Printf +module S = String +module Y = Sys + +module U = NUri + +module O = Options + +let unsupported protocol = + failwith (P.sprintf "probe: unsupported protocol: %s" protocol) + +let missing path = + failwith (P.sprintf "probe: missing path: %s" path) + +let mk_file path = + if F.check_suffix path "/" then S.sub path 0 (pred (S.length path)) + else path ^ ".ng" + +let add_obj path = + let path = F.chop_extension path in + let str = F.concat "cic:" path in + O.objs := U.uri_of_string str :: !O.objs + +let add_src path = + let path = F.chop_extension path in + let str = F.concat "cic:" path ^ "/" in + O.srcs := U.uri_of_string str :: !O.srcs + +let rec scan_entry base path = + if F.check_suffix path ".con.ng" then add_obj path else + if F.check_suffix path ".ind.ng" then add_obj path else + if F.check_suffix path ".var.ng" then add_obj path else + if F.check_suffix path ".ng" then add_src path else + let files = Y.readdir (F.concat base path) in + let map base file = scan_entry base (F.concat path file) in + A.iter (map base) files + +let from_uri base uri = + let str = U.string_of_uri uri in + let i = S.index str '/' in + let protocol = S.sub str 0 i in + if protocol = "cic:" then + let path = S.sub str (succ i) (S.length str - succ i) in + let file = mk_file path in + if Y.file_exists (F.concat base file) then scan_entry base file + else missing path + else unsupported protocol + +let from_string base s = + from_uri base (U.uri_of_string s) diff --git a/matita/components/binaries/probe/matitaList.mli b/matita/components/binaries/probe/matitaList.mli new file mode 100644 index 000000000..92c28cd9d --- /dev/null +++ b/matita/components/binaries/probe/matitaList.mli @@ -0,0 +1,14 @@ +(* + ||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 from_uri: string -> NUri.uri -> unit + +val from_string: string -> string -> unit diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml new file mode 100644 index 000000000..a289af829 --- /dev/null +++ b/matita/components/binaries/probe/nCicScan.ml @@ -0,0 +1,98 @@ +(* + ||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 U = NUri +module R = NReference +module C = NCic +module P = NCicPp +module E = NCicEnvironment + +module O = Options + +let status = new P.status + +let malformed () = + failwith "probe: malformed term" + +let rec set_list c ts cts = + let map cts t = (c, t) :: cts in + L.fold_left map cts ts + +let set_funs c rfs cts = + let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in + L.fold_left map cts rfs + +let set_type c cts (_, _, t, css) = + let map cts (_, _, t) = (c, t) :: cts in + (c, t) :: L.fold_left map cts css + +let scan_lref a c i = + try match List.nth c (pred i) with + | _, C.Decl _ -> succ a + | _, C.Def _ -> a + with + | Failure _ -> succ a + +let scan_gref a = function + | R.Ref (_, R.Decl) + | R.Ref (_, R.Ind _) + | R.Ref (_, R.Con _) -> succ a + | R.Ref (u, R.Def _) + | R.Ref (u, R.Fix _) + | R.Ref (u, R.CoFix _) -> + if L.exists (U.eq u) !O.objs then a else succ a + +let rec scan_term a = function + | [] -> a + | (_, C.Meta _) :: tl + | (_, C.Implicit _) :: tl -> scan_term a tl + | (_, C.Sort _) :: tl -> scan_term (succ a) tl + | (c, C.Rel i) :: tl -> scan_term (scan_lref a c i) tl + | (_, C.Const p) :: tl -> scan_term (scan_gref a p) tl + | (_, C.Appl []) :: tl -> malformed () + | (c, C.Appl ts) :: tl -> + scan_term (L.length ts + pred a) (set_list c ts tl) + | (c, C.Match (_, t0, t1, ts)) :: tl -> + scan_term a (set_list c (t0::t1::ts) tl) + | (c, C.Prod (s, t0, t1)) :: tl + | (c, C.Lambda (s, t0, t1)) :: tl -> + scan_term (succ a) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl) + | (c, C.LetIn (s, t0, t1, t2)) :: tl -> + scan_term a ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl) + +let scan_obj a u = + let _, _, _, _, obj = E.get_checked_obj status u in + match obj with + | C.Constant (_, _, None, t, _) -> + scan_term (succ a) [[], t] + | C.Constant (_, _, Some t0, t1, _) -> + scan_term (succ a) (set_list [] [t0; t1] []) + | C.Fixpoint (_, rfs, _) -> + scan_term (a + L.length rfs) (set_funs [] rfs []) + | C.Inductive (_, _, its, _) -> + let cts = L.fold_left (set_type []) [] its in + scan_term (a + L.length cts) cts + +let accept_obj u = + let _, _, _, _, obj = E.get_checked_obj status u in + let g = match obj with + | C.Constant (_, _, _, _, (g, _, _)) + | C.Fixpoint (_, _, (g, _, _)) + | C.Inductive (_, _, _, (g, _)) -> g + in + if L.mem g !O.exclude then false else true + +let scan () = + if !O.exclude <> [] then + O.objs := L.filter accept_obj !O.objs; + O.net := L.fold_left scan_obj !O.net !O.objs diff --git a/matita/components/binaries/probe/nCicScan.mli b/matita/components/binaries/probe/nCicScan.mli new file mode 100644 index 000000000..be5404956 --- /dev/null +++ b/matita/components/binaries/probe/nCicScan.mli @@ -0,0 +1,12 @@ +(* + ||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 scan: unit -> unit diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml new file mode 100644 index 000000000..e243241d0 --- /dev/null +++ b/matita/components/binaries/probe/options.ml @@ -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_______________________________________________________________ *) + +let default_objs = [] + +let default_srcs = [] + +let default_exclude = [] + +let default_net = 0 + +let objs = ref default_objs + +let srcs = ref default_srcs + +let exclude = ref default_exclude + +let net = ref default_net + +let clear () = + objs := default_objs; srcs := default_srcs; + exclude := default_exclude; net := default_net diff --git a/matita/components/binaries/probe/options.mli b/matita/components/binaries/probe/options.mli new file mode 100644 index 000000000..e9e51e04e --- /dev/null +++ b/matita/components/binaries/probe/options.mli @@ -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_______________________________________________________________ *) + +val objs: NUri.uri list ref + +val srcs: NUri.uri list ref + +val exclude: NCic.generated list ref + +val net: int ref + +val clear: unit -> unit diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml new file mode 100644 index 000000000..375255838 --- /dev/null +++ b/matita/components/binaries/probe/probe.ml @@ -0,0 +1,75 @@ +(* + ||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 R = Helm_registry +module L = Librarian +module B = NCicLibrary +module C = NCicTypeChecker +module H = HLog + +module O = Options +module M = MatitaList +module S = NCicScan +module E = Engine + +let trusted _ = true + +let no_log _ _ = () + +let init registry = + R.load_from registry; + B.init (); + C.set_trust trusted; + H.set_log_callback no_log + +let scan str = + M.from_string (R.get "matita.basedir") str; + S.scan () + +let set_g () = O.exclude := `Generated :: !O.exclude + +let set_p () = O.exclude := `Provided :: !O.exclude + +let out_i () = 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_ss () = E.out_uris !O.srcs + +let process s = + if L.is_uri s then scan s else init s + +let _ = + let help = "Usage: probe [ -X | | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in + let help_X = " Reset options and counters" in + let help_g = " Exclude generated objects" in + let help_i = " Print the total intrinsic size" in + let help_p = " Exclude provided objects" in + let help_on = " Print the number of objects" in + let help_os = " Print the list of objects" in + let help_sn = " Print the number of sources" in + let help_ss = " Print the list of sources" in + A.parse [ + "-X" , A.Unit O.clear, help_X; + "-g" , A.Unit set_g, help_g; + "-i" , A.Unit out_i, help_i; + "-p" , A.Unit set_p, help_p; + "-on", A.Unit out_on, help_on; + "-os", A.Unit out_os, help_os; + "-sn", A.Unit out_sn, help_sn; + "-ss", A.Unit out_ss, help_ss; + ] process help diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 38f1c3076..5b8fd2863 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -1,3 +1,5 @@ +OPEN = ( + H = @ XOA_DIR = ../../../components/binaries/xoa XOA = xoa.native @@ -5,6 +7,9 @@ DEP_DIR = ../../../components/binaries/matitadep DEP = matitadep.native MAC_DIR = ../../../components/binaries/mac MAC = mac.native +PRB_DIR = ../../../components/binaries/probe +PRB = probe.native +PRB_OPTS = ../../matita.conf.xml -g cic:/matita/lambdadelta/ XOA_CONF = ground_2/xoa.conf.xml XOA_TARGETS = ground_2/xoa_notation.ma ground_2/xoa.ma @@ -18,6 +23,15 @@ PACKAGES = ground_2 basic_2 apps_2 all: ../../matitac.opt +# MAS ######################################################################## + +define MAS_TEMPLATE + MAS_$(1) := $$(shell find $(1) -name "*.ma") + MAS += $$(MAS_$(1)) +endef + +$(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG)))) + # xoa ######################################################################## xoa: $(XOA_TARGETS) @@ -34,63 +48,77 @@ orig: $(ORIGS) # dep ######################################################################## -deps: MAS = $(shell find $* -name "*.ma") - deps: $(DEP_DIR)/$(DEP) @echo " MATITADEP" $(H)grep "include \"" $(MAS) | $< # stats ###################################################################### -stats: $(PACKAGES:%=%.stats) - -%.stats: MAS = $(shell find $* -name "*.ma") - -%.stats: CHARS = $(shell $(MAC_DIR)/$(MAC) $(MAS)) - -%.stats: +define STATS_TEMPLATE + STT_$(1) := $(1).stats + STTS += $$(STT_$(1)) + + $$(STT_$(1)): S1 = $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1))) + $$(STT_$(1)): S2 := $$(shell echo $$$$(($$(S1) / 5120))) + $$(STT_$(1)): S4 := $$(shell ls $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): S5 := $$(shell $$(PRB_DIR)/$$(PRB) $$(PRB_OPTS)$(1)/ -sn -on) + $$(STT_$(1)): P1 := $$(shell grep "theorem " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): P2 := $$(shell grep "lemma " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): P3 := $$(shell grep "fact " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): P4 := $$(shell grep qed $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): C1 := $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): C2 := $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): M1 := $$(shell grep "axiom " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): M2 := $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): M3 := $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l) + +$$(STT_$(1)): @printf '\x1B[1;40;37m' - @printf '%-15s %-40s' 'Statistics for:' $* - @printf '\x1B[0m\n' + @printf '%-15s %-43s' 'Statistics for:' $(1) + @printf '\x1B[0m\n' @printf '\x1B[1;40;35m' - @printf '%-8s %6i' Chars $(CHARS) - @printf ' %-8s %3i' Pages `echo $$(($(CHARS) / 5120))` - @printf ' %-23s' '' + @printf '%-8s %6i' Chars $$(S1) + @printf ' %-8s %3i' Pages $$(S2) + @printf ' %-26s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;36m' - @printf '%-8s %6i' Sources `ls $(MAS) | wc -l` - @printf ' %-38s' '' -# @printf ' %-8s %5i' Objs `ls *.vo | wc -l` -# @printf ' %-6s %3i' Files `ls *.v | wc -l` + @printf '%-8s %6i' Files $$(S4) + @printf ' %-8s %3i' Sources $$(word 1, $$(S5)) + @printf ' %-7s %4i' Objects $$(word 2, $$(S5)) + @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;32m' - @printf '%-8s %6i' Theorems `grep "theorem " $(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 '%-8s %6i' Theorems $$(P1) + @printf ' %-8s %3i' Lemmas $$(P2) + @printf ' %-7s %4i' Facts $$(P3) + @printf ' %-6s %4i' Proofs $$(P4) @printf '\x1B[0m\n' @printf '\x1B[1;40;33m' - @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 '%-8s %6i' Declared $$(C1) + @printf ' %-8s %3i' Defined $$(C2) + @printf ' %-26s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;31m' - @printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l` - @printf ' %-8s %3i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l` - @printf ' %-5s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` + @printf '%-8s %6i' Axioms $$(M1) + @printf ' %-8s %3i' Comments $$(M2) + @printf ' %-7s %4i' Marks $$(M3) @printf ' %-11s' '' @printf '\x1B[0m\n' +endef + +$(foreach PKG, $(PACKAGES), $(eval $(call STATS_TEMPLATE,$(PKG)))) + +stats: $(STTS) # summary #################################################################### define SUMMARY_TEMPLATE TBL_$(1) := $(1)/$(1)_sum.tbl - MAS_$(1) := $$(shell find $(1) -name "*.ma") TBLS += $$(TBL_$(1)) - $$(TBL_$(1)): V1 := $$(shell ls $$(MAS_$(1)) | wc -l) - $$(TBL_$(1)): V2 := $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1))) + $$(TBL_$(1)): S1 := $$(shell ls $$(MAS_$(1)) | wc -l) + $$(TBL_$(1)): S2 := $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1))) + $$(TBL_$(1)): S3 := $$(shell $$(PRB_DIR)/$$(PRB) $$(PRB_OPTS)$(1)/ -i) $$(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) @@ -106,9 +134,9 @@ define SUMMARY_TEMPLATE @printf ' [ "objects" * ]\n' >> $$@ @printf ' ]\n' >> $$@ @printf ' class "cyan" [ "sizes"\n' >> $$@ - @printf ' [ "files" "$$(V1)" ]\n' >> $$@ - @printf ' [ "characters" "$$(V2)" ]\n' >> $$@ - @printf ' [ * ]\n' >> $$@ + @printf ' [ "files" "$$(S1)" ]\n' >> $$@ + @printf ' [ "characters" "$$(S2)" ]\n' >> $$@ + @printf ' [ "nodes" "$$(S3)" ]\n' >> $$@ @printf ' ]\n' >> $$@ @printf ' class "green" [ "propositions"\n' >> $$@ @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ -- 2.39.2