diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml index 625b00d480c..d9d063f32f2 100644 --- a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml +++ b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml @@ -591,7 +591,8 @@ let (store_module_to_cache : else () let (unsafe_raw_load_checked_file : Prims.string -> - (Prims.string Prims.list * tc_result) FStar_Pervasives_Native.option) + (FStar_Parser_Dep.parsing_data * Prims.string Prims.list * tc_result) + FStar_Pervasives_Native.option) = fun checked_fn -> let entry = FStar_Compiler_Util.load_2values_from_file checked_fn in @@ -600,6 +601,6 @@ let (unsafe_raw_load_checked_file : let uu___ = let uu___1 = FStar_Compiler_List.map FStar_Pervasives_Native.fst s2.deps_dig in - (uu___1, (s2.tc_res)) in + ((s1.parsing_data), uu___1, (s2.tc_res)) in FStar_Pervasives_Native.Some uu___ | uu___ -> FStar_Pervasives_Native.None \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml index dc572246ccd..7c126911b68 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml @@ -325,6 +325,14 @@ let (str_of_parsing_data : parsing_data -> Prims.string) = str_of_parsing_data_elt in FStar_String.op_Hat "; " uu___2 in FStar_String.op_Hat s uu___1) "") +let (friends : parsing_data -> FStar_Ident.lident Prims.list) = + fun p -> + let uu___ = p in + match uu___ with + | Mk_pd p1 -> + FStar_Compiler_List.collect + (fun uu___1 -> + match uu___1 with | P_dep (true, l) -> [l] | uu___2 -> []) p1 let (parsing_data_elt_eq : parsing_data_elt -> parsing_data_elt -> Prims.bool) = fun e1 -> @@ -1174,23 +1182,27 @@ let (collect_one : FStar_Compiler_Util.is_some in if uu___ then - ((let uu___2 = - FStar_Options.debug_at_level_no_module - (FStar_Options.Other "Dep") in - if uu___2 - then - FStar_Compiler_Util.print1 - "Reading the parsing data for %s from its checked file\n" - filename - else ()); - (let uu___2 = - let uu___3 = - FStar_Compiler_Effect.op_Bar_Greater data_from_cache - FStar_Compiler_Util.must in - from_parsing_data uu___3 original_map filename in - match uu___2 with - | (deps1, has_inline_for_extraction, mo_roots) -> - let uu___3 = + let uu___1 = + let uu___2 = + FStar_Compiler_Effect.op_Bar_Greater data_from_cache + FStar_Compiler_Util.must in + from_parsing_data uu___2 original_map filename in + match uu___1 with + | (deps1, has_inline_for_extraction, mo_roots) -> + ((let uu___3 = + FStar_Options.debug_at_level_no_module + (FStar_Options.Other "Dep") in + if uu___3 + then + let uu___4 = + let uu___5 = FStar_Compiler_List.map dep_to_string deps1 in + FStar_Compiler_Effect.op_Bar_Greater uu___5 + (FStar_String.concat ", ") in + FStar_Compiler_Util.print2 + "Reading the parsing data for %s from its checked file .. found [%s]\n" + filename uu___4 + else ()); + (let uu___3 = FStar_Compiler_Effect.op_Bar_Greater data_from_cache FStar_Compiler_Util.must in (uu___3, deps1, has_inline_for_extraction, mo_roots))) @@ -1823,7 +1835,7 @@ let (widen_deps : dependence_graph -> files_for_module_name -> Prims.bool -> (Prims.bool * dependence_graph)) = - fun friends -> + fun friends1 -> fun dep_graph -> fun file_system_map -> fun widened -> @@ -1840,7 +1852,7 @@ let (widen_deps : (fun d -> match d with | PreferInterface m when - (FStar_Compiler_List.contains m friends) && + (FStar_Compiler_List.contains m friends1) && (has_implementation file_system_map m) -> (FStar_Compiler_Effect.op_Colon_Equals @@ -1934,7 +1946,7 @@ let (topological_dependences_of' : all_friends filenames in let uu___ = all_friend_deps dep_graph [] ([], []) root_files in match uu___ with - | (friends, all_files_0) -> + | (friends1, all_files_0) -> ((let uu___2 = FStar_Options.debug_at_level_no_module (FStar_Options.Other "Dep") in @@ -1943,7 +1955,7 @@ let (topological_dependences_of' : let uu___3 = let uu___4 = FStar_Compiler_Util.remove_dups - (fun x -> fun y -> x = y) friends in + (fun x -> fun y -> x = y) friends1 in FStar_String.concat ", " uu___4 in FStar_Compiler_Util.print3 "Phase1 complete:\n\tall_files = %s\n\tall_friends=%s\n\tinterfaces_with_inlining=%s\n" @@ -1951,7 +1963,7 @@ let (topological_dependences_of' : (FStar_String.concat ", " interfaces_needing_inlining) else ()); (let uu___2 = - widen_deps friends dep_graph file_system_map widened in + widen_deps friends1 dep_graph file_system_map widened in match uu___2 with | (widened1, dep_graph1) -> let uu___3 = diff --git a/src/fstar/FStar.CheckedFiles.fst b/src/fstar/FStar.CheckedFiles.fst index ee0247e7132..cbd2356706b 100644 --- a/src/fstar/FStar.CheckedFiles.fst +++ b/src/fstar/FStar.CheckedFiles.fst @@ -472,8 +472,7 @@ let store_module_to_cache env fn parsing_data tc_result = end let unsafe_raw_load_checked_file (checked_fn:string) - : option (list string & tc_result) = let entry : option (checked_file_entry_stage1 * checked_file_entry_stage2) = BU.load_2values_from_file checked_fn in match entry with - | Some ((s1,s2)) -> Some (List.map fst s2.deps_dig, s2.tc_res) + | Some ((s1,s2)) -> Some (s1.parsing_data, List.map fst s2.deps_dig, s2.tc_res) | _ -> None diff --git a/src/fstar/FStar.CheckedFiles.fsti b/src/fstar/FStar.CheckedFiles.fsti index 4ffaf2fc970..1f4a560baa0 100644 --- a/src/fstar/FStar.CheckedFiles.fsti +++ b/src/fstar/FStar.CheckedFiles.fsti @@ -58,4 +58,4 @@ val load_module_from_cache: (uenv -> string -> option tc_result) val store_module_to_cache: uenv -> file_name:string -> Dep.parsing_data -> tc_result -> unit val unsafe_raw_load_checked_file (checked_file_name:string) - : option (list string & tc_result) + : option (FStar.Parser.Dep.parsing_data & list string & tc_result) diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst index 1830065ddc3..3ba4423a8a7 100644 --- a/src/parser/FStar.Parser.Dep.fst +++ b/src/parser/FStar.Parser.Dep.fst @@ -190,6 +190,15 @@ let str_of_parsing_data = function | Mk_pd l -> l |> List.fold_left (fun s elt -> s ^ "; " ^ (elt |> str_of_parsing_data_elt)) "" +let friends (p:parsing_data) : list lident = + let Mk_pd p = p in + List.collect + (function + | P_dep (true, l) -> [l] + | _ -> []) + p + + let parsing_data_elt_eq (e1:parsing_data_elt) (e2:parsing_data_elt) = match e1, e2 with | P_begin_module l1, P_begin_module l2 -> lid_equals l1 l2 @@ -751,9 +760,9 @@ let collect_one let data_from_cache = filename |> get_parsing_data_from_cache in if data_from_cache |> is_some then begin //we found the parsing data in the checked file - if Options.debug_at_level_no_module (Options.Other "Dep") then - BU.print1 "Reading the parsing data for %s from its checked file\n" filename; let deps, has_inline_for_extraction, mo_roots = from_parsing_data (data_from_cache |> must) original_map filename in + if Options.debug_at_level_no_module (Options.Other "Dep") then + BU.print2 "Reading the parsing data for %s from its checked file .. found [%s]\n" filename (List.map dep_to_string deps |> String.concat ", "); data_from_cache |> must, deps, has_inline_for_extraction, mo_roots end diff --git a/src/parser/FStar.Parser.Dep.fsti b/src/parser/FStar.Parser.Dep.fsti index dc435a1d34a..1bef7c515fc 100644 --- a/src/parser/FStar.Parser.Dep.fsti +++ b/src/parser/FStar.Parser.Dep.fsti @@ -44,9 +44,9 @@ val is_interface: string -> bool val is_implementation: string -> bool val parsing_data : Type0 //cached in the checked files - +val str_of_parsing_data (p:parsing_data) : string val empty_parsing_data: parsing_data //for legacy ide - +val friends (p:parsing_data) : list lident val deps : Type0 val empty_deps : deps