diff --git a/ocaml/fstar-lib/FStar_All.ml b/ocaml/fstar-lib/FStar_All.ml index 4c16c33988e..4d8ce7492ff 100644 --- a/ocaml/fstar-lib/FStar_All.ml +++ b/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 - diff --git a/ocaml/fstar-lib/FStar_Compiler_Util.ml b/ocaml/fstar-lib/FStar_Compiler_Util.ml index 77d4e2989c7..3910c68f776 100644 --- a/ocaml/fstar-lib/FStar_Compiler_Util.ml +++ b/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 diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml index c4a863519e3..739f513fc6d 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml @@ -2898,12 +2898,40 @@ let (do_print : fun outc -> fun fn -> fun deps1 -> + let pref uu___ = + (let uu___2 = + let uu___3 = + FStar_Compiler_Effect.op_Bang FStar_Options._version in + [uu___3] in + FStar_Compiler_Util.fprint outc + "# This was generated by F* version %s\n" uu___2); + (let uu___3 = + let uu___4 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_string) + FStar_Compiler_Util.exec_name in + [uu___4] in + FStar_Compiler_Util.fprint outc "# Executable: %s\n" uu___3); + (let uu___4 = + let uu___5 = + let uu___6 = FStar_Compiler_Util.get_cmd_args () in + FStar_Class_Show.show + (FStar_Class_Show.show_list + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_string)) uu___6 in + [uu___5] in + FStar_Compiler_Util.fprint outc + "# Command line arguments: \"%s\"\n" uu___4); + FStar_Compiler_Util.fprint outc "#\n" [] in let uu___ = FStar_Options.dep () in match uu___ with - | FStar_Pervasives_Native.Some "make" -> print_make outc deps1 + | FStar_Pervasives_Native.Some "make" -> + (pref (); print_make outc deps1) | FStar_Pervasives_Native.Some "full" -> - profile (fun uu___1 -> print_full outc deps1) - "FStar.Parser.Deps.print_full_deps" + (pref (); + profile (fun uu___2 -> print_full outc deps1) + "FStarC.Parser.Deps.print_full_deps") | FStar_Pervasives_Native.Some "graph" -> print_graph outc fn deps1.dep_graph | FStar_Pervasives_Native.Some "raw" -> print_raw outc deps1 diff --git a/src/basic/FStar.Compiler.Util.fsti b/src/basic/FStar.Compiler.Util.fsti index 3221954c332..0e40c16d8c9 100644 --- a/src/basic/FStar.Compiler.Util.fsti +++ b/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 diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst index f1735a0b45d..f51a6fc4e81 100644 --- a/src/parser/FStar.Parser.Dep.fst +++ b/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" -> diff --git a/ulib/FStar.All.fst b/ulib/FStar.All.fsti similarity index 86% rename from ulib/FStar.All.fst rename to ulib/FStar.All.fsti index c3e6e5469f7..750653d6651 100644 --- a/ulib/FStar.All.fst +++ b/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') diff --git a/ulib/FStar.IO.fst b/ulib/FStar.IO.fst deleted file mode 100644 index 3f1326ea30b..00000000000 --- a/ulib/FStar.IO.fst +++ /dev/null @@ -1,79 +0,0 @@ -(* - 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 -assume new type fd_read : Type0 -assume new type fd_write : Type0 - -assume val stdin : fd_read -assume val stdout : fd_write -assume val stderr : fd_write - -assume val print_newline : unit -> ML unit -assume 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 *) -assume val print_uint8 : FStar.UInt8.t -> ML unit -assume val print_uint16 : FStar.UInt16.t -> ML unit -assume val print_uint32 : FStar.UInt32.t -> ML unit -assume val print_uint64 : FStar.UInt64.t -> ML unit - -(* Print as decimal *) -assume val print_uint8_dec : FStar.UInt8.t -> ML unit -assume val print_uint16_dec : FStar.UInt16.t -> ML unit -assume val print_uint32_dec : FStar.UInt32.t -> ML unit -assume val print_uint64_dec : FStar.UInt64.t -> ML unit - -(* Print as hex in fixed width, no leading 0x *) -assume val print_uint8_hex_pad : FStar.UInt8.t -> ML unit -assume val print_uint16_hex_pad : FStar.UInt16.t -> ML unit -assume val print_uint32_hex_pad : FStar.UInt32.t -> ML unit -assume val print_uint64_hex_pad : FStar.UInt64.t -> ML unit - -(* Print as decimal, zero padded to maximum possible length *) -assume val print_uint8_dec_pad : FStar.UInt8.t -> ML unit -assume val print_uint16_dec_pad : FStar.UInt16.t -> ML unit -assume val print_uint32_dec_pad : FStar.UInt32.t -> ML unit -assume val print_uint64_dec_pad : FStar.UInt64.t -> ML unit - -assume val print_any : 'a -> ML unit -assume val input_line : unit -> ML string -assume val input_int : unit -> ML int -assume val input_float : unit -> ML FStar.Float.float -assume val open_read_file : string -> ML fd_read -assume val open_write_file : string -> ML fd_write -assume val close_read_file : fd_read -> ML unit -assume val close_write_file : fd_write -> ML unit -assume val read_line : fd_read -> ML string -assume 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. -*) -assume val debug_print_string : string -> Tot bool diff --git a/ulib/FStar.IO.fsti b/ulib/FStar.IO.fsti new file mode 100644 index 00000000000..4a65a0b20dd --- /dev/null +++ b/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 diff --git a/ulib/ml/Makefile.realized b/ulib/ml/Makefile.realized index 47018067fbd..c996d62113e 100644 --- a/ulib/ml/Makefile.realized +++ b/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 \