--- /dev/null
+EXEC = probe
+VERSION=0.1.0
+
+REQUIRES = helm-ng_library
+
+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 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)
--- /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 out_uris: NUri.uri list -> unit
+
+val out_int: int -> unit
+
+val out_length: 'a list -> unit
--- /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 = 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)
--- /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 from_uri: string -> NUri.uri -> unit
+
+val from_string: string -> string -> unit
--- /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 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
--- /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 scan: unit -> unit
--- /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 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
--- /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 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
--- /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 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 | <configuration file> | -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
+OPEN = (
+
H = @
XOA_DIR = ../../../components/binaries/xoa
XOA = xoa.native
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
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)
# 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)
@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' >> $$@
projects / helm.git / commitdiff