Skip to content

Commit

Permalink
FStar_All.ml, FStar_Compiler_Effect.ml: Remove some footguns and unus…
Browse files Browse the repository at this point in the history
…ed code
  • Loading branch information
mtzguido committed Oct 10, 2024
1 parent f9969ba commit af3cd9c
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 10 deletions.
10 changes: 4 additions & 6 deletions ocaml/fstar-lib/FStar_All.ml
Original file line number Diff line number Diff line change
@@ -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 *)
8 changes: 4 additions & 4 deletions ocaml/fstar-lib/FStar_Compiler_Effect.ml
Original file line number Diff line number Diff line change
@@ -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]

Expand All @@ -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 *)

0 comments on commit af3cd9c

Please sign in to comment.