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.

Sign up for GitHub

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

Simplify the use of --cmi, towards making it the default #3592

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+57 −75
Open

Simplify the use of --cmi, towards making it the default #3592

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
90 changes: 38 additions & 52 deletions ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

42 changes: 19 additions & 23 deletions src/parser/FStarC.Parser.Dep.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -230,7 +230,6 @@ type deps = {
file_system_map:files_for_module_name; //an abstraction of the file system, keys are lowercase module names
cmd_line_files:list file_name; //all command-line files
all_files:list file_name; //all files
interfaces_with_inlining:list module_name; //interfaces that use `inline_for_extraction` require inlining
parse_results:smap parsing_data //map from filenames to parsing_data
//callers (Universal.fs) use this to get the parsing data for caching purposes
}
Expand All @@ -239,16 +238,15 @@ let deps_add_dep (Deps m) k v =
BU.smap_add m k v
let deps_keys (Deps m) = BU.smap_keys m
let deps_empty () = Deps (BU.smap_create 41)
let mk_deps dg fs c a i pr = {
let mk_deps dg fs c a pr = {
dep_graph=dg;
file_system_map=fs;
cmd_line_files=c;
all_files=a;
interfaces_with_inlining=i;
parse_results=pr;
}
(* In public interface *)
let empty_deps = mk_deps (deps_empty ()) (BU.smap_create 0) [] [] [] (BU.smap_create 0)
let empty_deps = mk_deps (deps_empty ()) (BU.smap_create 0) [] [] (BU.smap_create 0)
let module_name_of_dep = function
| UseInterface m
| PreferInterface m
Expand Down Expand Up @@ -284,7 +282,10 @@ let has_interface (file_system_map:files_for_module_name) (key:module_name)
let has_implementation (file_system_map:files_for_module_name) (key:module_name)
: bool =
Option.isSome (implementation_of_internal file_system_map key)

let interfaces_with_inlining deps m =
if Options.cmi()
then has_interface deps.file_system_map m
else false

(*
* Public interface
Expand Down Expand Up @@ -1241,15 +1242,15 @@ let dep_graph_copy dep_graph =
let (Deps g) = dep_graph in
Deps (BU.smap_copy g)

let widen_deps friends dep_graph file_system_map widened =
let widen_deps (friends:string -> bool) dep_graph file_system_map widened =
let widened = BU.mk_ref widened in
let (Deps dg) = dep_graph in
let (Deps dg') = deps_empty() in
let widen_one deps =
deps |> List.map (fun d ->
match d with
| PreferInterface m
when (List.contains m friends &&
when (friends m &&
has_implementation file_system_map m) ->
widened := true;
FriendImplementation m
Expand All @@ -1268,7 +1269,7 @@ let widen_deps friends dep_graph file_system_map widened =
let topological_dependences_of'
file_system_map
dep_graph
interfaces_needing_inlining
(interfaces_needing_inlining: string -> bool)
root_files
widened
: list file_name
Expand Down Expand Up @@ -1385,15 +1386,13 @@ let topological_dependences_of'
all_friend_deps dep_graph [] ([], []) root_files
in
if !dbg
then BU.print3 "Phase1 complete:\n\t\
then BU.print2 "Phase1 complete:\n\t\
all_files = %s\n\t\
all_friends=%s\n\t\
interfaces_with_inlining=%s\n"
all_friends=%s\n"
(String.concat ", " all_files_0)
(String.concat ", " (remove_dups (fun x y -> x=y) friends))
(String.concat ", " (interfaces_needing_inlining));
(String.concat ", " (remove_dups (fun x y -> x=y) friends));
let widened, dep_graph =
widen_deps friends dep_graph file_system_map widened
widen_deps (fun m -> List.contains m friends) dep_graph file_system_map widened
in
let _, all_files =
if !dbg
Expand All @@ -1408,7 +1407,7 @@ let topological_dependences_of'
let phase1
file_system_map
dep_graph
interfaces_needing_inlining
(interfaces_needing_inlining:string -> bool)
for_extraction
=
if !dbg
Expand All @@ -1422,7 +1421,7 @@ let phase1
let topological_dependences_of
file_system_map
dep_graph
interfaces_needing_inlining
(interfaces_needing_inlining:string -> bool)
root_files
for_extraction
: list file_name
Expand Down Expand Up @@ -1623,22 +1622,19 @@ let collect (all_cmd_line_files: list file_name)
let m = lowercase_module_name f in
Options.add_verify_module m);

let inlining_ifaces = !interfaces_needing_inlining in
let all_files, _ =
profile
(fun () ->
topological_dependences_of
file_system_map
dep_graph
inlining_ifaces
(has_interface file_system_map)
all_cmd_line_files
(Options.codegen()<>None))
"FStarC.Parser.Dep.topological_dependences_of"
in
if !dbg
then BU.print1 "Interfaces needing inlining: %s\n" (String.concat ", " inlining_ifaces);
all_files,
mk_deps dep_graph file_system_map all_cmd_line_files all_files inlining_ifaces parse_results
mk_deps dep_graph file_system_map all_cmd_line_files all_files parse_results

(* In public interface *)
let deps_of deps (f:file_name)
Expand Down Expand Up @@ -1786,7 +1782,7 @@ let print_full (outc : out_channel) (deps:deps) : unit =
let output_krml_file f = norm_path (output_file ".krml" f) in
let output_cmx_file f = norm_path (output_file ".cmx" f) in
let cache_file f = norm_path (cache_file_name f) in
let widened, dep_graph = phase1 deps.file_system_map deps.dep_graph deps.interfaces_with_inlining true in
let widened, dep_graph = phase1 deps.file_system_map deps.dep_graph (interfaces_with_inlining deps) true in
let all_checked_files =
keys |>
List.fold_left
Expand Down Expand Up @@ -1858,7 +1854,7 @@ let print_full (outc : out_channel) (deps:deps) : unit =
topological_dependences_of'
deps.file_system_map
(dep_graph_copy dep_graph)
deps.interfaces_with_inlining
(interfaces_with_inlining deps)
[file_name]
widened)
"FStarC.Parser.Dep.topological_dependences_of_2"
Expand Down
Loading