From 63d6d890e727a78eabbb7add4c0347a8ca9eac11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 28 Feb 2025 17:55:41 +0100 Subject: [PATCH 1/4] add command lambdapi depend --- src/cli/lambdapi.ml | 11 ++++++++++- src/tool/depend.ml | 22 ++++++++++++++++++++++ src/tool/dune | 2 +- 3 files changed, 33 insertions(+), 2 deletions(-) create mode 100644 src/tool/depend.ml diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index f06916e2f..b3a92da33 100644 --- a/src/cli/lambdapi.ml +++ b/src/cli/lambdapi.ml @@ -114,6 +114,10 @@ let parse_cmd : Config.t -> string list -> unit = fun cfg files -> in Error.handle_exceptions run +(** Running the depend mode. *) +let depend_cmd : Config.t -> string list -> unit = fun _cfg files -> + Tool.Depend.print_deps files + (** Possible outputs for the export command. *) type output = Lp | Dk | RawDk | Hrs | Xtc | RawCoq | SttCoq @@ -384,6 +388,11 @@ let parse_cmd = Cmd.v (Cmd.info "parse" ~doc ~man:man_pkg_file) CLT.(const parse_cmd $ Config.full $ files) +let depend_cmd = + let doc = "Print dependencies of the given files." in + Cmd.v (Cmd.info "depend" ~doc ~man:man_pkg_file) + CLT.(const depend_cmd $ Config.full $ files) + let export_cmd = let doc = "Translate the given files to other formats." in Cmd.v (Cmd.info "export" ~doc ~man:man_pkg_file) @@ -452,7 +461,7 @@ let _ = Stdlib.at_exit (Debug.print_time t0); Printexc.record_backtrace true; let cmds = - [ check_cmd ; parse_cmd ; export_cmd ; lsp_server_cmd + [ check_cmd ; parse_cmd ; depend_cmd ; export_cmd ; lsp_server_cmd ; decision_tree_cmd ; help_cmd ; version_cmd ; Init.cmd ; Install.install_cmd ; Install.uninstall_cmd ; index_cmd ; search_cmd ; websearch_cmd ] diff --git a/src/tool/depend.ml b/src/tool/depend.ml new file mode 100644 index 000000000..ad243b339 --- /dev/null +++ b/src/tool/depend.ml @@ -0,0 +1,22 @@ + +let string_of_file (f:string) :string = + let ic = Stdlib.open_in f in + let n = Stdlib.in_channel_length ic in + let s = Bytes.create n in + Stdlib.really_input ic s 0 n; + Stdlib.close_in ic; + Bytes.to_string s + +let re = Str.regexp {|^require[ \n\t]+\(open[ \n\t]+\)?\([^;]+\);|} + +let search (content:string) = + let rec search (start:int) :unit = + try let _ = Str.search_forward re content start in + print_endline (Str.matched_group 2 content); + search (Str.match_end()) + with _ -> () + in search 0 + +let print_deps_file filename = search (string_of_file filename) + +let print_deps = List.iter print_deps_file diff --git a/src/tool/dune b/src/tool/dune index d3cc83495..7ecdfd036 100644 --- a/src/tool/dune +++ b/src/tool/dune @@ -2,7 +2,7 @@ (name tool) (public_name lambdapi.tool) (modules :standard) - (libraries lambdapi.parsing lambdapi.core dream unix) + (libraries lambdapi.parsing lambdapi.core dream unix str) (preprocess (pps lwt_ppx))) (rule From 458ce8481971796598111391bdcd20641add90f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 28 Feb 2025 18:42:54 +0100 Subject: [PATCH 2/4] wip --- src/parsing/package.ml | 7 ++++++ src/tool/depend.ml | 48 ++++++++++++++++++++++++++++++++++-------- 2 files changed, 46 insertions(+), 9 deletions(-) diff --git a/src/parsing/package.ml b/src/parsing/package.ml index 6e4ba5fd0..5d500e05d 100644 --- a/src/parsing/package.ml +++ b/src/parsing/package.ml @@ -88,3 +88,10 @@ let apply_config : string -> unit = fun fname -> let {root_path; _} = read cfg_file in let root = Filename.dirname cfg_file in Library.add_mapping (root_path, root) + +(** [root_path fname] tries to find a configuration file from [fname] and + return the root_path if any. *) +let root_path fname = + match find_config fname with + | None -> None + | Some cfg_file -> Some (read cfg_file).root_path diff --git a/src/tool/depend.ml b/src/tool/depend.ml index ad243b339..38324b811 100644 --- a/src/tool/depend.ml +++ b/src/tool/depend.ml @@ -1,22 +1,52 @@ +(** Fast extraction of the dependencies of a set of Lambdapi files without + parsing them. *) -let string_of_file (f:string) :string = - let ic = Stdlib.open_in f in +(* FIXME: extend to Dedukti files *) + +(** [string_of_file filename] returns the contents of [filename] as a + string *) +let string_of_file filename = + let ic = Stdlib.open_in filename in let n = Stdlib.in_channel_length ic in let s = Bytes.create n in Stdlib.really_input ic s 0 n; Stdlib.close_in ic; Bytes.to_string s -let re = Str.regexp {|^require[ \n\t]+\(open[ \n\t]+\)?\([^;]+\);|} +(* FIXME: does not handle escaped names {|...|}. *) +let re_mod = Str.regexp "\\([^ \n\t]+\\)" + +(* FIXME: do not print files starting with the root_path. *) +let search_mod root_path content = + print_endline ("search_mod: "^content); + let rec search start = + try let _ = Str.search_forward re_mod content start in + let s = Str.matched_group 1 content in + if String.starts_with ~prefix:root_path s then print_endline s; + search (Str.match_end()) + with _ -> () + in search 0 + +(* FIXME: does not handle comments /* ... */ between module names, or comments + // ... at the end of a line. *) +let re_req = + Str.regexp "\\(^\\|[ \t]\\)require\\([ \n\t]+open\\)?[ \n\t]+\\([^;]+\\);" -let search (content:string) = - let rec search (start:int) :unit = - try let _ = Str.search_forward re content start in - print_endline (Str.matched_group 2 content); +let search_req root_path content = + let rec search start = + try let _ = Str.search_forward re_req content start in + search_mod root_path (Str.matched_group 3 content); search (Str.match_end()) with _ -> () in search 0 -let print_deps_file filename = search (string_of_file filename) +let print_deps_file root_path filename = + search_req root_path (string_of_file filename) -let print_deps = List.iter print_deps_file +let print_deps = function + | [] -> () + | (f::_) as fs -> + match Parsing.Package.root_path f with + | None -> Common.Error.fatal_no_pos "No lambdapi.pkd found." + | Some root_path -> + List.iter (print_deps_file (String.concat "." root_path)) fs From e0ae9cd3b301e843358ad6a2c363d923b682fbfc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 28 Feb 2025 18:43:47 +0100 Subject: [PATCH 3/4] wip --- src/tool/depend.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/tool/depend.ml b/src/tool/depend.ml index 38324b811..41fbcb5f4 100644 --- a/src/tool/depend.ml +++ b/src/tool/depend.ml @@ -16,7 +16,6 @@ let string_of_file filename = (* FIXME: does not handle escaped names {|...|}. *) let re_mod = Str.regexp "\\([^ \n\t]+\\)" -(* FIXME: do not print files starting with the root_path. *) let search_mod root_path content = print_endline ("search_mod: "^content); let rec search start = @@ -47,6 +46,6 @@ let print_deps = function | [] -> () | (f::_) as fs -> match Parsing.Package.root_path f with - | None -> Common.Error.fatal_no_pos "No lambdapi.pkd found." + | None -> Common.Error.fatal_no_pos "No file lambdapi.pkg found." | Some root_path -> List.iter (print_deps_file (String.concat "." root_path)) fs From 13d98671d66bc3229bcd003dc52273ac7ed25407 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 3 Mar 2025 19:28:48 +0100 Subject: [PATCH 4/4] add starts_with in lplib --- src/lplib/string.ml | 9 +++++++++ src/tool/depend.ml | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/lplib/string.ml b/src/lplib/string.ml index 32e09711f..8d46ae91d 100644 --- a/src/lplib/string.ml +++ b/src/lplib/string.ml @@ -41,3 +41,12 @@ module B = Bytes let bos = B.unsafe_of_string let get_utf_8_uchar s i = B.get_utf_8_uchar (bos s) i let is_valid_utf_8 s = B.is_valid_utf_8 (bos s) + +let starts_with ~prefix s = + let len_s = length s + and len_pre = length prefix in + let rec aux i = + if i = len_pre then true + else if unsafe_get s i <> unsafe_get prefix i then false + else aux (i + 1) + in len_s >= len_pre && aux 0 diff --git a/src/tool/depend.ml b/src/tool/depend.ml index 41fbcb5f4..bf9a15768 100644 --- a/src/tool/depend.ml +++ b/src/tool/depend.ml @@ -21,7 +21,7 @@ let search_mod root_path content = let rec search start = try let _ = Str.search_forward re_mod content start in let s = Str.matched_group 1 content in - if String.starts_with ~prefix:root_path s then print_endline s; + if Lplib.String.starts_with ~prefix:root_path s then print_endline s; search (Str.match_end()) with _ -> () in search 0