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/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/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 new file mode 100644 index 000000000..bf9a15768 --- /dev/null +++ b/src/tool/depend.ml @@ -0,0 +1,51 @@ +(** Fast extraction of the dependencies of a set of Lambdapi files without + parsing them. *) + +(* 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 + +(* FIXME: does not handle escaped names {|...|}. *) +let re_mod = Str.regexp "\\([^ \n\t]+\\)" + +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 Lplib.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_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 root_path filename = + search_req root_path (string_of_file filename) + +let print_deps = function + | [] -> () + | (f::_) as fs -> + match Parsing.Package.root_path f with + | None -> Common.Error.fatal_no_pos "No file lambdapi.pkg found." + | Some root_path -> + List.iter (print_deps_file (String.concat "." root_path)) fs 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