Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add the command lambdapi depend to compute dependencies quickly #1212

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion src/cli/lambdapi.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 ]
Expand Down
9 changes: 9 additions & 0 deletions src/lplib/string.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
7 changes: 7 additions & 0 deletions src/parsing/package.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
51 changes: 51 additions & 0 deletions src/tool/depend.ml
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion src/tool/dune
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading