Merge pull request #3018 from FStarLang/_nik_parsing_data

Exposing parsing_data in the unsafe_raw_read_checked_file

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

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)

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

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