From 243d091f23f8338e155cdde14969a6043b8c89af Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 24 Feb 2013 16:20:34 +0000 Subject: [PATCH] - nUri : added Sets of uris for use in "probe" - probe: now we can exclude the objects of dismissed sources (those in .matita/ but not in the development as .ma) - lambdadelta: Makefile now uses the new feature of "probe" --- matita/components/binaries/probe/engine.ml | 47 +++++++++++++++++-- matita/components/binaries/probe/engine.mli | 14 ++++-- .../components/binaries/probe/matitaList.ml | 45 +++++++++--------- .../components/binaries/probe/matitaList.mli | 4 +- matita/components/binaries/probe/nCicScan.ml | 23 ++++----- matita/components/binaries/probe/options.ml | 8 +++- matita/components/binaries/probe/options.mli | 6 ++- matita/components/binaries/probe/probe.ml | 16 +++++-- matita/components/ng_kernel/nUri.ml | 1 + matita/components/ng_kernel/nUri.mli | 1 + matita/matita/contribs/lambdadelta/Makefile | 6 +-- 11 files changed, 117 insertions(+), 54 deletions(-) diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index e79f000f9..55936e542 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -9,15 +9,54 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module F = Filename module L = List module P = Printf -module U = NUri +module U = NUri +module US = U.UriSet +module B = Librarian +module H = HExtlib + +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 = + failwith (P.sprintf "probe: missing root: %s" path) + +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 - L.iter map uris + US.iter map uris -let out_int i = P.printf "%u\n" i +let is_registry str = + F.check_suffix str ".conf.xml" -let out_length l = out_int (L.length l) +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 + | _ -> + if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir else + aux (F.dirname bdir) (F.concat (F.basename bdir) file) + in + aux dir file +(* + + let bpath = F.dirname str ^ "/" in + bpath, buri +*) diff --git a/matita/components/binaries/probe/engine.mli b/matita/components/binaries/probe/engine.mli index 7f3b5a2ca..808315971 100644 --- a/matita/components/binaries/probe/engine.mli +++ b/matita/components/binaries/probe/engine.mli @@ -9,8 +9,16 @@ \ / 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 +val out_length: NUri.UriSet.t -> unit + +val out_uris: NUri.UriSet.t -> 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/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index a2ce7d908..7af98d59c 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -15,15 +15,13 @@ module P = Printf module S = String module Y = Sys -module U = NUri +module U = NUri +module US = U.UriSet module O = Options +module E = Engine -let unsupported protocol = - failwith (P.sprintf "probe: unsupported protocol: %s" protocol) - -let missing path = - failwith (P.sprintf "probe: missing path: %s" path) +let src_exists path = !O.no_devel || Y.file_exists path let mk_file path = if F.check_suffix path "/" then S.sub path 0 (pred (S.length path)) @@ -32,32 +30,35 @@ let mk_file path = 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 + O.objs := US.add (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 add_src devel path = + if src_exists (F.chop_extension devel ^ ".ma") then + 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 -let rec scan_entry base path = +let rec scan_entry base devel 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 + if F.check_suffix path ".ng" then add_src devel path else + if src_exists devel || src_exists (devel ^ ".ma") then + let files = Y.readdir (F.concat base path) in + let map base file = scan_entry base (F.concat devel file) (F.concat path file) in + A.iter (map base) files -let from_uri base uri = +let from_uri base devel uri = + O.no_devel := devel = ""; 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 + if Y.file_exists (F.concat base file) then scan_entry base devel file + else E.missing path + else E.unsupported protocol -let from_string base s = - from_uri base (U.uri_of_string s) +let from_string base devel s = + from_uri base devel (U.uri_of_string s) diff --git a/matita/components/binaries/probe/matitaList.mli b/matita/components/binaries/probe/matitaList.mli index 92c28cd9d..200c90158 100644 --- a/matita/components/binaries/probe/matitaList.mli +++ b/matita/components/binaries/probe/matitaList.mli @@ -9,6 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val from_uri: string -> NUri.uri -> unit +val from_uri: string -> string -> NUri.uri -> unit -val from_string: string -> string -> unit +val from_string: string -> string -> string -> unit diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml index a289af829..e9c6a2448 100644 --- a/matita/components/binaries/probe/nCicScan.ml +++ b/matita/components/binaries/probe/nCicScan.ml @@ -9,15 +9,16 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module L = List +module L = List -module U = NUri -module R = NReference -module C = NCic -module P = NCicPp -module E = NCicEnvironment +module U = NUri +module US = U.UriSet +module R = NReference +module C = NCic +module P = NCicPp +module E = NCicEnvironment -module O = Options +module O = Options let status = new P.status @@ -50,7 +51,7 @@ let scan_gref a = function | 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 + if US.mem u !O.objs then a else succ a let rec scan_term a = function | [] -> a @@ -70,7 +71,7 @@ let rec scan_term a = function | (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 scan_obj u a = let _, _, _, _, obj = E.get_checked_obj status u in match obj with | C.Constant (_, _, None, t, _) -> @@ -94,5 +95,5 @@ let accept_obj u = 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 + O.objs := US.filter accept_obj !O.objs; + O.net := US.fold scan_obj !O.objs !O.net diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml index e243241d0..246088727 100644 --- a/matita/components/binaries/probe/options.ml +++ b/matita/components/binaries/probe/options.ml @@ -9,9 +9,11 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -let default_objs = [] +module US = NUri.UriSet -let default_srcs = [] +let default_objs = US.empty + +let default_srcs = US.empty let default_exclude = [] @@ -25,6 +27,8 @@ let exclude = ref default_exclude let net = ref default_net +let no_devel = ref true + 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 index e9e51e04e..31b22307a 100644 --- a/matita/components/binaries/probe/options.mli +++ b/matita/components/binaries/probe/options.mli @@ -9,12 +9,14 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val objs: NUri.uri list ref +val objs: NUri.UriSet.t ref -val srcs: NUri.uri list ref +val srcs: NUri.UriSet.t ref val exclude: NCic.generated list ref val net: int ref val clear: unit -> unit + +val no_devel: bool ref diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml index 375255838..fb7b4eab9 100644 --- a/matita/components/binaries/probe/probe.ml +++ b/matita/components/binaries/probe/probe.ml @@ -32,10 +32,14 @@ let init registry = C.set_trust trusted; H.set_log_callback no_log -let scan str = - M.from_string (R.get "matita.basedir") str; +let scan_uri devel str = + M.from_string (R.get "matita.basedir") devel str; S.scan () +let scan_from devel = + let devel, uri = E.get_uri devel in + scan_uri devel uri + let set_g () = O.exclude := `Generated :: !O.exclude let set_p () = O.exclude := `Provided :: !O.exclude @@ -46,12 +50,14 @@ 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_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 + if L.is_uri s then scan_uri "" s + else if E.is_registry s then init s + else scan_from s let _ = let help = "Usage: probe [ -X | | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in @@ -67,9 +73,9 @@ let _ = "-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; + "-p" , A.Unit set_p, help_p; "-sn", A.Unit out_sn, help_sn; "-ss", A.Unit out_ss, help_ss; ] process help diff --git a/matita/components/ng_kernel/nUri.ml b/matita/components/ng_kernel/nUri.ml index b3c877768..ba87b2e28 100644 --- a/matita/components/ng_kernel/nUri.ml +++ b/matita/components/ng_kernel/nUri.ml @@ -59,3 +59,4 @@ end;; module UriHash = Hashtbl.Make(HT);; module UriMap = Map.Make(HT);; +module UriSet = Set.Make(HT);; diff --git a/matita/components/ng_kernel/nUri.mli b/matita/components/ng_kernel/nUri.mli index 25d319eb4..e3ad120f3 100644 --- a/matita/components/ng_kernel/nUri.mli +++ b/matita/components/ng_kernel/nUri.mli @@ -23,3 +23,4 @@ val hash: uri -> int module UriHash: Hashtbl.S with type key = uri module UriMap: Map.S with type key = uri +module UriSet: Set.S with type elt = uri diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 69fca343b..f13eb7e21 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -9,7 +9,7 @@ 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/ +PRB_OPTS = ../../matita.conf.xml -g XOA_CONF = ground_2/xoa.conf.xml XOA_TARGETS = ground_2/xoa_notation.ma ground_2/xoa.ma @@ -61,7 +61,7 @@ define STATS_TEMPLATE $$(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)): 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) @@ -120,7 +120,7 @@ define SUMMARY_TEMPLATE $$(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)): 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) -- 2.39.2