Merge pull request #3551 from mtzguido/tidy_fstar_all

Tidying up a bit of FStar.All and FStar.Compiler.Effect

ocaml/fstar-lib/FStar_All.ml

@@ -1,9 +1,7 @@
 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
-
+(* Not used: handled specially by extraction. If used,
+   you will get all sorts of weird failures (e.g. an incomplete match
+   on f2!). *)
+(* let try_with f1 f2 = try f1 () with | e -> f2 e *)

ocaml/fstar-lib/FStar_Compiler_Effect.ml

@@ -1,6 +1,3 @@
-let op_Bar_Greater (x : 'a) (f : ('a -> 'b)) : 'b = f x
-let op_Less_Bar  (f : ('a -> 'b)) (x : 'a) : 'b = f x
-
 type 'a ref' = 'a ref[@@deriving yojson,show]
 type 'a ref = 'a ref'[@@deriving yojson,show]
 
@@ -9,6 +6,9 @@ let op_Colon_Equals x y = x := y
 let alloc x = ref x
 let raise = raise
 let exit i = exit (Z.to_int i)
-let try_with f1 f2 = try f1 () with | e -> f2 e
 exception Failure = Failure
 let failwith x = raise (Failure x)
+(* Not used: handled specially by extraction. If used,
+   you will get all sorts of weird failures (e.g. an incomplete match
+   on f2!). *)
+(* let try_with f1 f2 = try f1 () with | e -> f2 e *)

src/Makefile.boot

@@ -52,8 +52,7 @@ EXTRACT_MODULES=FStar.Pervasives FStar.Common FStar.Thunk		\
 # And there are a few specific files that should not be extracted at
 # all, despite being in one of the EXTRACT_NAMESPACES
 NO_EXTRACT=FStar.Tactics.Native FStar.Tactics.Load	\
-	   FStar.Extraction.ML.PrintML FStar.Compiler.List \
-	   FStar.Compiler.Effect
+	   FStar.Extraction.ML.PrintML FStar.Compiler.List
 
 EXTRACT = $(addprefix --extract_module , $(EXTRACT_MODULES))		\
 	  $(addprefix --extract_namespace , $(EXTRACT_NAMESPACES))	\

src/basic/FStar.Compiler.Effect.fst → src/basic/FStar.Compiler.Effect.fsti

@@ -37,31 +37,24 @@ effect All (a:Type) (pre:all_pre) (post:(h:unit -> Tot (all_post' a (pre h)))) =
 
 effect ML (a:Type) = ALL a (fun (p:all_post a) (_:unit) -> forall (a:result a) (h:unit). p a h)
 
-assume
+new
 val ref (a:Type) : Type0
 
-assume
 val (!) (#a:Type) (r:ref a)
   : ML a
 
-assume
 val (:=) (#a:Type) (r:ref a) (x:a)
   : ML unit
 
-assume
 val alloc (#a:Type) (x:a)
   : ML (ref a)
 
-assume
 val raise (e: exn) : ML 'a
 
-assume
 val exit : int -> ML 'a
 
-assume
 val try_with : (unit -> ML 'a) -> (exn -> ML 'a) -> ML 'a
 
 exception Failure of string
 
-assume
 val failwith : string -> ML 'a

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/ml/Makefile.realized

@@ -1,7 +1,7 @@
 # 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 \
+FSTAR_REALIZED_MODULES=Buffer Bytes Char CommonST Constructive Dyn Float Ghost Heap Monotonic.Heap \
 	HyperStack.All HyperStack.ST HyperStack.IO Int16 Int32 Int64 Int8 IO \
 	List List.Tot.Base Mul Option Pervasives.Native ST Exn String \
 	UInt16 UInt32 UInt64 UInt8 \