\ / 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
+*)
\ / 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
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))
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)
\ / 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
\ / 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
| 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
| (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, _) ->
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
\ / 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 = []
let net = ref default_net
+let no_devel = ref true
+
let clear () =
objs := default_objs; srcs := default_srcs;
exclude := default_exclude; net := default_net
\ / 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
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
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 | <configuration file> | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in
"-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
module UriHash = Hashtbl.Make(HT);;
module UriMap = Map.Make(HT);;
+module UriSet = Set.Make(HT);;
module UriHash: Hashtbl.S with type key = uri
module UriMap: Map.S with type key = uri
+module UriSet: Set.S with type elt = uri
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
$$(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)
$$(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)
projects / helm.git / commitdiff