A header comment in .depend, some library tweaks

ocaml/fstar-lib/FStar_All.ml

@@ -1,9 +1,4 @@
 exception Failure = Failure
 let failwith x = raise (Failure x)
 let exit i = exit (Z.to_int i)
-let op_Bar_Greater (x : 'a) (f : ('a -> 'b)) : 'b = f x
-let op_Less_Bar  (f : ('a -> 'b)) (x : 'a) : 'b = f x
-let pipe_right a f = f a
-let pipe_left f a = f a
 let try_with f1 f2 = try f1 () with | e -> f2 e
-

ocaml/fstar-lib/FStar_Compiler_Util.ml

@@ -917,6 +917,7 @@ let geq (i:int) (j:int) = i >= j
 
 let exec_name = Sys.executable_name
 let get_exec_dir () = Filename.dirname (Sys.executable_name)
+let get_cmd_args () = Array.to_list Sys.argv
 let expand_environment_variable x = try Some (Sys.getenv x) with Not_found -> None
 
 let physical_equality (x:'a) (y:'a) = x == y

src/basic/FStar.Compiler.Util.fsti

@@ -309,6 +309,7 @@ val mk_ref: 'a -> ref 'a
 
 val exec_name : string
 val get_exec_dir: unit -> string
+val get_cmd_args : unit -> list string
 val expand_environment_variable: string -> option string
 
 val physical_equality: 'a -> 'a -> bool

src/parser/FStar.Parser.Dep.fst

@@ -2021,11 +2021,20 @@ let print_full (outc : out_channel) (deps:deps) : unit =
     FStar.StringBuffer.output_channel outc sb
 
 let do_print (outc : out_channel) (fn : string) deps : unit =
+  let pref () =
+    BU.fprint outc "# This was generated by F* version %s\n" [!Options._version];
+    BU.fprint outc "# Executable: %s\n" [show BU.exec_name];
+    BU.fprint outc "# Command line arguments: \"%s\"\n" [show (BU.get_cmd_args ())];
+    BU.fprint outc "#\n" [];
+    ()
+  in
   match Options.dep() with
   | Some "make" ->
+      pref ();
       print_make outc deps
   | Some "full" ->
-      profile (fun () -> print_full outc deps) "FStar.Parser.Deps.print_full_deps"
+      pref ();
+      profile (fun () -> print_full outc deps) "FStarC.Parser.Deps.print_full_deps"
   | Some "graph" ->
       print_graph outc fn deps.dep_graph
   | Some "raw" ->

ulib/FStar.All.fst → ulib/FStar.All.fsti

@@ -36,8 +36,8 @@ effect All (a:Type) (pre:all_pre) (post:(h:heap -> Tot (all_post' a (pre h)))) =
     (fun (p : all_post a) (h : heap) -> pre h /\ (forall ra h1. post h ra h1 ==> p ra h1))
 effect ML (a:Type) = ALL a (fun (p:all_post a) (_:heap) -> forall (a:result a) (h:heap). p a h)
 
-assume val exit : int -> ML 'a
-assume val try_with : (unit -> ML 'a) -> (exn -> ML 'a) -> ML 'a
+val exit : int -> ML 'a
+val try_with : (unit -> ML 'a) -> (exn -> ML 'a) -> ML 'a
 
-assume exception Failure of string
-assume val failwith : string -> All 'a (fun h -> True) (fun h a h' -> Err? a /\ h == h')
+exception Failure of string
+val failwith : string -> All 'a (fun h -> True) (fun h a h' -> Err? a /\ h == h')

ulib/FStar.IO.fsti

@@ -0,0 +1,82 @@
+(*
+   Copyright 2008-2018 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module FStar.IO
+
+open FStar.All
+
+exception EOF
+
+new
+val fd_read : Type0
+new
+val fd_write : Type0
+
+val stdin : fd_read
+val stdout : fd_write
+val stderr : fd_write
+
+val print_newline : unit -> ML unit
+val print_string : string -> ML unit
+
+(* assume val print_nat_hex : nat -> ML unit *)
+(* assume val print_nat_dec : nat -> ML unit *)
+
+(* Print as hexadecimal with a leading 0x *)
+val print_uint8 : FStar.UInt8.t -> ML unit
+val print_uint16 : FStar.UInt16.t -> ML unit
+val print_uint32 : FStar.UInt32.t -> ML unit
+val print_uint64 : FStar.UInt64.t -> ML unit
+
+(* Print as decimal *)
+val print_uint8_dec : FStar.UInt8.t -> ML unit
+val print_uint16_dec : FStar.UInt16.t -> ML unit
+val print_uint32_dec : FStar.UInt32.t -> ML unit
+val print_uint64_dec : FStar.UInt64.t -> ML unit
+
+(* Print as hex in fixed width, no leading 0x *)
+val print_uint8_hex_pad : FStar.UInt8.t -> ML unit
+val print_uint16_hex_pad : FStar.UInt16.t -> ML unit
+val print_uint32_hex_pad : FStar.UInt32.t -> ML unit
+val print_uint64_hex_pad : FStar.UInt64.t -> ML unit
+
+(* Print as decimal, zero padded to maximum possible length *)
+val print_uint8_dec_pad : FStar.UInt8.t -> ML unit
+val print_uint16_dec_pad : FStar.UInt16.t -> ML unit
+val print_uint32_dec_pad : FStar.UInt32.t -> ML unit
+val print_uint64_dec_pad : FStar.UInt64.t -> ML unit
+
+val print_any : 'a -> ML unit
+val input_line : unit -> ML string
+val input_int : unit -> ML int
+val input_float : unit -> ML FStar.Float.float
+val open_read_file : string -> ML fd_read
+val open_write_file : string -> ML fd_write
+val close_read_file : fd_read -> ML unit
+val close_write_file : fd_write -> ML unit
+val read_line : fd_read -> ML string
+val write_string : fd_write -> string -> ML unit
+
+(*
+   An UNSOUND escape hatch for printf-debugging;
+   Although it always returns false, we mark it
+   as returning a bool, so that extraction doesn't
+   erase this call.
+
+   Note: no guarantees are provided regarding the order
+   of assume valuation of this function; since it is marked as pure,
+   the compiler may re-order or replicate it.
+*)
+val debug_print_string : string -> Tot bool

ulib/ml/Makefile.realized

@@ -1,8 +1,8 @@
 # You should include this Makefile in your Makefile to make sure you remain
 # future-proof w.r.t. realized modules!
 
-FSTAR_REALIZED_MODULES=All Buffer Bytes Char CommonST Constructive Dyn Float Ghost Heap Monotonic.Heap \
-	HyperStack.All HyperStack.ST HyperStack.IO Int16 Int32 Int64 Int8 IO \
+FSTAR_REALIZED_MODULES=Buffer Bytes Char CommonST Constructive Dyn Float Ghost Heap Monotonic.Heap \
+	HyperStack.All HyperStack.ST HyperStack.IO Int16 Int32 Int64 Int8 \
 	List List.Tot.Base Mul Option Pervasives.Native ST Exn String \
 	UInt16 UInt32 UInt64 UInt8 \
 	Pointer.Derived1 Pointer.Derived2 \