Introduce --read_checked_file option

src/basic/FStar.Options.fst

@@ -238,6 +238,7 @@ let defaults =
       ("quake_keep"                   , Bool false);
       ("query_cache"                  , Bool false);
       ("query_stats"                  , Bool false);
+      ("read_checked_file"            , Unset);
       ("record_hints"                 , Bool false);
       ("record_options"               , Bool false);
       ("report_assumes"               , Unset);
@@ -425,6 +426,7 @@ let get_quake_hi                ()      = lookup_opt "quake_hi"
 let get_quake_keep              ()      = lookup_opt "quake_keep"               as_bool
 let get_query_cache             ()      = lookup_opt "query_cache"              as_bool
 let get_query_stats             ()      = lookup_opt "query_stats"              as_bool
+let get_read_checked_file       ()      = lookup_opt "read_checked_file"        (as_option as_string)
 let get_record_hints            ()      = lookup_opt "record_hints"             as_bool
 let get_record_options          ()      = lookup_opt "record_options"           as_bool
 let get_retry                   ()      = lookup_opt "retry"                    as_bool
@@ -1152,6 +1154,11 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
     Const (Bool true),
     text "Print SMT query statistics");
 
+  ( noshort,
+    "read_checked_file",
+    PathStr "path",
+    text "Read a checked file and dump it to standard output.");
+
   ( noshort,
     "record_hints",
     Const (Bool true),
@@ -1937,6 +1944,7 @@ let quake_hi                     () = get_quake_hi                    ()
 let quake_keep                   () = get_quake_keep                  ()
 let query_cache                  () = get_query_cache                 ()
 let query_stats                  () = get_query_stats                 ()
+let read_checked_file            () = get_read_checked_file           ()
 let record_hints                 () = get_record_hints                ()
 let record_options               () = get_record_options              ()
 let retry                        () = get_retry                       ()

src/basic/FStar.Options.fsti

@@ -185,6 +185,7 @@ val quake_hi                    : unit    -> int
 val quake_keep                  : unit    -> bool
 val query_cache                 : unit    -> bool
 val query_stats                 : unit    -> bool
+val read_checked_file           : unit    -> option string
 val record_hints                : unit    -> bool
 val record_options              : unit    -> bool
 val retry                       : unit    -> bool

src/fstar/FStar.CheckedFiles.fst

@@ -233,36 +233,46 @@ let load_checked_file (fn:string) (checked_fn:string) :cache_t =
                 end
                 else add_and_return (Unknown, Inr x.parsing_data)
 
+let load_tc_result (checked_fn:string) : option (list (string & 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 ((_,s2)) -> Some (s2.deps_dig, s2.tc_res)
+  | _ -> None
+
 (*
  * Second step for loading checked files, validates the tc data
  * Either the reason why tc_result is invalid
  *   or tc_result
  *)
-let load_checked_file_with_tc_result (deps:Dep.deps) (fn:string) (checked_fn:string)
-  :either string tc_result =
+let load_checked_file_with_tc_result
+  (deps:Dep.deps)
+  (fn:string)
+  (checked_fn:string)
+  : either string tc_result
+=
   if !dbg then
     BU.print1 "Trying to load checked file with tc result %s\n" checked_fn;
 
-  let load_tc_result (fn:string) :list (string & 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 ((_,s2)) -> s2.deps_dig, s2.tc_res
-     | _ ->
-       failwith "Impossible! if first phase of loading was unknown, it should have succeeded"
+  let load_tc_result' (fn:string) :list (string & string) & tc_result =
+    match load_tc_result fn with
+    | Some x -> x
+    | None -> failwith "Impossible! if first phase of loading was unknown, it should have succeeded"
   in
 
   let elt = load_checked_file fn checked_fn in  //first step, in case some client calls it directly
   match elt with
   | Invalid msg, _ -> Inl msg
-  | Valid _, _ -> checked_fn |> load_tc_result |> snd |> Inr
+  | Valid _, _ -> checked_fn |> load_tc_result' |> snd |> Inr
   | Unknown, parsing_data ->
     match hash_dependences deps fn with
     | Inl msg ->
       let elt = (Invalid msg, parsing_data) in
       BU.smap_add mcache checked_fn elt;
       Inl msg
     | Inr deps_dig' ->
-      let deps_dig, tc_result = checked_fn |> load_tc_result in
+      let deps_dig, tc_result = checked_fn |> load_tc_result' in
       if deps_dig = deps_dig'
       then begin
         //mark the tc data of the file as valid

src/fstar/FStar.CheckedFiles.fsti

@@ -41,6 +41,14 @@ type tc_result = {
   extraction_time:int
 }
 
+val load_tc_result (checked_fn:string) : option (list (string & string) & tc_result)
+
+val load_checked_file_with_tc_result
+  (deps:Dep.deps)
+  (fn:string)
+  (checked_fn:string)
+  : either string tc_result
+
 (*
  * Read parsing data from the checked file
  * This function is passed as a callback to Parser.Dep

src/fstar/FStar.Main.fst

@@ -23,6 +23,8 @@ open FStar.CheckedFiles
 open FStar.Universal
 open FStar.Compiler
 
+open FStar.Class.Show
+
 module E = FStar.Errors
 module UF = FStar.Syntax.Unionfind
 module RE = FStar.Reflection.V2.Embeddings
@@ -160,6 +162,20 @@ let go _ =
           else failwith "You seem to be using the F#-generated version ofthe compiler ; \o
                          reindenting is not known to work yet with this version"
 
+        (* --read_checked: read and print a checked file *)
+        else if Some? (Options.read_checked_file ()) then
+          let path = Some?.v <| Options.read_checked_file () in
+          let env = Universal.init_env Parser.Dep.empty_deps in
+          let res = FStar.CheckedFiles.load_tc_result path in
+          match res with
+          | None ->
+            let open FStar.Pprint in
+            Errors.raise_err_doc (Errors.Fatal_ModuleOrFileNotFound, [
+                Errors.Msg.text "Could not read checked file:" ^/^ doc_of_string path
+              ])
+
+          | Some (_, tcr) ->
+            print1 "%s\n" (show tcr.checked_module)
         (* --lsp *)
         else if Options.lsp_server () then
           FStar.Interactive.Lsp.start_server ()