Skip to content

Commit f51670f

Browse files
mtzguidomtzguido
authored
Merge pull request #490 from mtzguido/update-ml
Update expected ML output
2 parents 5b3e515 + 6e70820 commit f51670f

File tree

5 files changed

+142
-172
lines changed

5 files changed

+142
-172
lines changed

‎test/Example_Unreachable.ml.expected‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
open Prims
2-
let rec (test : Prims.bool FStar_Pervasives_Native.option -> Prims.bool) =
3-
fun x ->
4-
match x with
5-
| FStar_Pervasives_Native.Some b -> b
6-
| FStar_Pervasives_Native.None -> Pulse_Lib_Dv.unreachable ()
2+
let rec test (x : Prims.bool FStar_Pervasives_Native.option) : Prims.bool=
3+
match x with
4+
| FStar_Pervasives_Native.Some b -> b
5+
| FStar_Pervasives_Native.None -> Pulse_Lib_Dv.unreachable ()

‎test/ExtractionTest.ml.expected‎

Lines changed: 93 additions & 113 deletions
Original file line numberDiff line numberDiff line change
@@ -1,121 +1,101 @@
11
open Prims
2-
let (zero : unit -> FStar_UInt32.t) = fun uu___ -> Stdint.Uint32.zero
3-
let rec (test_invariants_and_later : unit -> unit) = fun uu___ -> ()
4-
let rec (test_read_write :
5-
FStar_UInt32.t Pulse_Lib_HigherReference.ref -> unit -> unit) =
6-
fun x ->
7-
fun _'n ->
8-
let n = Pulse_Lib_HigherReference.read x () () in
9-
Pulse_Lib_HigherReference.write x
10-
(FStar_UInt32.add n Stdint.Uint32.zero) ()
11-
let rec (test_write_10 :
12-
FStar_UInt32.t Pulse_Lib_HigherReference.ref -> unit -> unit) =
13-
fun x ->
14-
fun _'n ->
15-
Pulse_Lib_HigherReference.write x (Stdint.Uint32.of_int (2)) ();
16-
test_read_write x ();
17-
Pulse_Lib_HigherReference.write x Stdint.Uint32.zero ()
18-
let rec (test_inner_ghost_fun : unit -> unit) = fun uu___ -> ()
19-
let rec (write10 :
20-
FStar_UInt32.t Pulse_Lib_HigherReference.ref -> unit -> unit) =
21-
fun x ->
22-
fun _'n ->
23-
let ctr =
24-
Pulse_Lib_HigherReference.alloc () (Stdint.Uint32.of_int (10)) in
25-
Pulse_Lib_Dv.while_
26-
(fun while_cond ->
27-
let __anf0 = Pulse_Lib_HigherReference.read ctr () () in
28-
FStar_UInt32.gt __anf0 Stdint.Uint32.zero)
29-
(fun while_body ->
30-
test_write_10 x ();
31-
(let __anf0 = Pulse_Lib_HigherReference.read ctr () () in
32-
Pulse_Lib_HigherReference.write ctr
33-
(FStar_UInt32.sub __anf0 Stdint.Uint32.one) ()))
34-
let rec (fill_array :
35-
FStar_UInt32.t Pulse_Lib_HigherArray_Core.array ->
36-
FStar_SizeT.t -> FStar_UInt32.t -> unit -> unit)
37-
=
38-
fun x ->
39-
fun n ->
40-
fun v ->
41-
fun _'s ->
42-
let i = Pulse_Lib_HigherReference.alloc () Stdint.Uint64.zero in
43-
Pulse_Lib_Dv.while_
44-
(fun while_cond ->
45-
let __anf0 = Pulse_Lib_HigherReference.read i () () in
46-
FStar_SizeT.lt __anf0 n)
47-
(fun while_body ->
48-
let __anf0 = Pulse_Lib_HigherReference.read i () () in
49-
Pulse_Lib_HigherArray_Core.mask_write x __anf0 v () ();
50-
(let __anf01 = Pulse_Lib_HigherReference.read i () () in
51-
Pulse_Lib_HigherReference.write i
52-
(FStar_SizeT.add __anf01 Stdint.Uint64.one) ()))
53-
let rec (sub_array : FStar_UInt32.t Pulse_Lib_HigherArray_Core.array -> unit)
54-
=
55-
fun x ->
56-
let __anf0 =
57-
Pulse_Lib_HigherArray_Core.sub x () () Stdint.Uint64.one () () in
58-
Pulse_Lib_HigherArray_Core.mask_write __anf0 Stdint.Uint64.zero
59-
(Stdint.Uint32.of_int (42)) () ()
60-
let (test0 : FStar_SizeT.t -> FStar_SizeT.t -> FStar_SizeT.t) =
61-
fun x -> fun y -> FStar_SizeT.rem x y
2+
let zero (uu___ : unit) : FStar_UInt32.t= Stdint.Uint32.zero
3+
let rec test_invariants_and_later (uu___ : unit) : unit= ()
4+
let rec test_read_write (x : FStar_UInt32.t Pulse_Lib_HigherReference.ref)
5+
(_'n : unit) : unit=
6+
let n = Pulse_Lib_HigherReference.read x () () in
7+
Pulse_Lib_HigherReference.write x (FStar_UInt32.add n Stdint.Uint32.zero)
8+
()
9+
let rec test_write_10 (x : FStar_UInt32.t Pulse_Lib_HigherReference.ref)
10+
(_'n : unit) : unit=
11+
Pulse_Lib_HigherReference.write x (Stdint.Uint32.of_int (2)) ();
12+
test_read_write x ();
13+
Pulse_Lib_HigherReference.write x Stdint.Uint32.zero ()
14+
let rec test_inner_ghost_fun (uu___ : unit) : unit= ()
15+
let rec write10 (x : FStar_UInt32.t Pulse_Lib_HigherReference.ref)
16+
(_'n : unit) : unit=
17+
let ctr = Pulse_Lib_HigherReference.alloc () (Stdint.Uint32.of_int (10)) in
18+
Pulse_Lib_Dv.while_
19+
(fun while_cond ->
20+
let __anf0 = Pulse_Lib_HigherReference.read ctr () () in
21+
FStar_UInt32.gt __anf0 Stdint.Uint32.zero)
22+
(fun while_body ->
23+
test_write_10 x ();
24+
(let __anf0 = Pulse_Lib_HigherReference.read ctr () () in
25+
Pulse_Lib_HigherReference.write ctr
26+
(FStar_UInt32.sub __anf0 Stdint.Uint32.one) ()))
27+
let rec fill_array (x : FStar_UInt32.t Pulse_Lib_HigherArray_Core.array)
28+
(n : FStar_SizeT.t) (v : FStar_UInt32.t) (_'s : unit) : unit=
29+
let i = Pulse_Lib_HigherReference.alloc () Stdint.Uint64.zero in
30+
Pulse_Lib_Dv.while_
31+
(fun while_cond ->
32+
let __anf0 = Pulse_Lib_HigherReference.read i () () in
33+
FStar_SizeT.lt __anf0 n)
34+
(fun while_body ->
35+
let __anf0 = Pulse_Lib_HigherReference.read i () () in
36+
Pulse_Lib_HigherArray_Core.mask_write x __anf0 v () ();
37+
(let __anf01 = Pulse_Lib_HigherReference.read i () () in
38+
Pulse_Lib_HigherReference.write i
39+
(FStar_SizeT.add __anf01 Stdint.Uint64.one) ()))
40+
let rec sub_array (x : FStar_UInt32.t Pulse_Lib_HigherArray_Core.array) :
41+
unit=
42+
let __anf0 = Pulse_Lib_HigherArray_Core.sub x () () Stdint.Uint64.one () () in
43+
Pulse_Lib_HigherArray_Core.mask_write __anf0 Stdint.Uint64.zero
44+
(Stdint.Uint32.of_int (42)) () ()
45+
let test0 (x : FStar_SizeT.t) (y : FStar_SizeT.t) : FStar_SizeT.t=
46+
FStar_SizeT.rem x y
6247
type 'a opt =
6348
| None
6449
| Some of 'a
65-
let uu___is_None : 'a . 'a opt -> Prims.bool =
66-
fun projectee -> match projectee with | None -> true | uu___ -> false
67-
let uu___is_Some : 'a . 'a opt -> Prims.bool =
68-
fun projectee -> match projectee with | Some v -> true | uu___ -> false
69-
let __proj__Some__item__v : 'a . 'a opt -> 'a =
70-
fun projectee -> match projectee with | Some v -> v
71-
let (my_safe_add : FStar_SizeT.t -> FStar_SizeT.t -> FStar_SizeT.t opt) =
72-
fun x ->
73-
fun y ->
74-
if FStar_SizeT.lte x (Stdint.Uint64.of_string "0xffff")
75-
then
76-
(if
77-
FStar_SizeT.lte y
78-
(FStar_SizeT.sub (Stdint.Uint64.of_string "0xffff") x)
79-
then Some (FStar_SizeT.add x y)
80-
else None)
81-
else None
82-
let rec (testbi : FStar_SizeT.t -> FStar_SizeT.t -> FStar_SizeT.t) =
83-
fun x -> fun y -> FStar_SizeT.rem x y
84-
let rec (testbi2 : FStar_SizeT.t -> FStar_SizeT.t -> FStar_SizeT.t opt) =
85-
fun x -> fun y -> my_safe_add x y
86-
let rec (extract_match : Prims.bool opt -> Prims.bool) =
87-
fun x -> match x with | None -> false | Some b -> Prims.op_Negation b
88-
let rec (fib : Prims.nat -> Prims.nat) =
89-
fun x ->
90-
if x <= Prims.int_one
91-
then Prims.int_one
92-
else
93-
(let x1 = fib (x - Prims.int_one) in
94-
let x2 = fib (x - (Prims.of_int (2))) in x1 + x2)
95-
let rec (fib2 : Prims.nat -> Prims.nat) =
96-
fun x -> let n = fib x in let m = fib (x + Prims.int_one) in m + n
50+
let uu___is_None (projectee : 'a opt) : Prims.bool=
51+
match projectee with | None -> true | uu___ -> false
52+
let uu___is_Some (projectee : 'a opt) : Prims.bool=
53+
match projectee with | Some v -> true | uu___ -> false
54+
let __proj__Some__item__v (projectee : 'a opt) : 'a=
55+
match projectee with | Some v -> v
56+
let my_safe_add (x : FStar_SizeT.t) (y : FStar_SizeT.t) : FStar_SizeT.t opt=
57+
if FStar_SizeT.lte x (Stdint.Uint64.of_string "0xffff")
58+
then
59+
(if
60+
FStar_SizeT.lte y
61+
(FStar_SizeT.sub (Stdint.Uint64.of_string "0xffff") x)
62+
then Some (FStar_SizeT.add x y)
63+
else None)
64+
else None
65+
let rec testbi (x : FStar_SizeT.t) (y : FStar_SizeT.t) : FStar_SizeT.t=
66+
FStar_SizeT.rem x y
67+
let rec testbi2 (x : FStar_SizeT.t) (y : FStar_SizeT.t) : FStar_SizeT.t opt=
68+
my_safe_add x y
69+
let rec extract_match (x : Prims.bool opt) : Prims.bool=
70+
match x with | None -> false | Some b -> Prims.op_Negation b
71+
let rec fib (x : Prims.nat) : Prims.nat=
72+
if x <= Prims.int_one
73+
then Prims.int_one
74+
else
75+
(let x1 = fib (x - Prims.int_one) in
76+
let x2 = fib (x - (Prims.of_int (2))) in x1 + x2)
77+
let rec fib2 (x : Prims.nat) : Prims.nat=
78+
let n = fib x in let m = fib (x + Prims.int_one) in m + n
9779
type ('a, 'b) data =
9880
| One of 'a * 'b
9981
| Two of 'a
10082
| Three of 'b * 'a
101-
let uu___is_One : 'a 'b . ('a, 'b) data -> Prims.bool =
102-
fun projectee ->
103-
match projectee with | One (_0, _1) -> true | uu___ -> false
104-
let __proj__One__item___0 : 'a 'b . ('a, 'b) data -> 'a =
105-
fun projectee -> match projectee with | One (_0, _1) -> _0
106-
let __proj__One__item___1 : 'a 'b . ('a, 'b) data -> 'b =
107-
fun projectee -> match projectee with | One (_0, _1) -> _1
108-
let uu___is_Two : 'a 'b . ('a, 'b) data -> Prims.bool =
109-
fun projectee -> match projectee with | Two _0 -> true | uu___ -> false
110-
let __proj__Two__item___0 : 'a 'b . ('a, 'b) data -> 'a =
111-
fun projectee -> match projectee with | Two _0 -> _0
112-
let uu___is_Three : 'a 'b . ('a, 'b) data -> Prims.bool =
113-
fun projectee ->
114-
match projectee with | Three (_0, _1) -> true | uu___ -> false
115-
let __proj__Three__item___0 : 'a 'b . ('a, 'b) data -> 'b =
116-
fun projectee -> match projectee with | Three (_0, _1) -> _0
117-
let __proj__Three__item___1 : 'a 'b . ('a, 'b) data -> 'a =
118-
fun projectee -> match projectee with | Three (_0, _1) -> _1
119-
let rec (test_that_we_access_the_right_field_in_matches :
120-
(Prims.nat, Prims.bool) data -> Prims.nat) =
121-
fun x -> match x with | One (y, z) -> y | Two y -> y | Three (z, y) -> y
83+
let uu___is_One (projectee : ('a, 'b) data) : Prims.bool=
84+
match projectee with | One (_0, _1) -> true | uu___ -> false
85+
let __proj__One__item___0 (projectee : ('a, 'b) data) : 'a=
86+
match projectee with | One (_0, _1) -> _0
87+
let __proj__One__item___1 (projectee : ('a, 'b) data) : 'b=
88+
match projectee with | One (_0, _1) -> _1
89+
let uu___is_Two (projectee : ('a, 'b) data) : Prims.bool=
90+
match projectee with | Two _0 -> true | uu___ -> false
91+
let __proj__Two__item___0 (projectee : ('a, 'b) data) : 'a=
92+
match projectee with | Two _0 -> _0
93+
let uu___is_Three (projectee : ('a, 'b) data) : Prims.bool=
94+
match projectee with | Three (_0, _1) -> true | uu___ -> false
95+
let __proj__Three__item___0 (projectee : ('a, 'b) data) : 'b=
96+
match projectee with | Three (_0, _1) -> _0
97+
let __proj__Three__item___1 (projectee : ('a, 'b) data) : 'a=
98+
match projectee with | Three (_0, _1) -> _1
99+
let rec test_that_we_access_the_right_field_in_matches
100+
(x : (Prims.nat, Prims.bool) data) : Prims.nat=
101+
match x with | One (y, z) -> y | Two y -> y | Three (z, y) -> y

‎test/InlineArrayLen.ml.expected‎

Lines changed: 34 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,35 @@
11
open Prims
2-
let rec (basic : unit -> FStar_Int32.t) =
3-
fun uu___ ->
4-
let arr =
5-
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
6-
(Stdint.Uint64.of_int (2)) in
7-
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
8-
let rec (use : unit -> FStar_Int32.t) =
9-
fun uu___ ->
10-
let arr =
11-
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
12-
(Stdint.Uint64.of_int (2)) in
13-
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
14-
let rec (use_gen_init : unit -> FStar_Int32.t) =
15-
fun uu___ ->
16-
let arr =
17-
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
18-
(Stdint.Uint64.of_int (2)) in
19-
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
20-
let rec (use_gen_init_st : unit -> FStar_Int32.t) =
21-
fun uu___ ->
22-
let init uu___1 = fun uu___2 -> (Stdint.Int32.of_int (123)) in
23-
let __anf0 = init () () in
24-
let arr =
25-
Pulse_Lib_HigherArray_Core.mask_alloc () __anf0
26-
(Stdint.Uint64.of_int (2)) in
27-
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
28-
let rec (use_gen_len : unit -> FStar_Int32.t) =
29-
fun uu___ ->
30-
let arr =
31-
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
32-
(Stdint.Uint64.of_int (2)) in
33-
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
34-
let rec (use_gen_len_st : unit -> FStar_Int32.t) =
35-
fun uu___ ->
36-
let len uu___1 = fun uu___2 -> (Stdint.Uint64.of_int (42)) in
37-
let __anf0 = len () () in
38-
let arr =
39-
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
40-
__anf0 in
41-
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
2+
let rec basic (uu___ : unit) : FStar_Int32.t=
3+
let arr =
4+
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
5+
(Stdint.Uint64.of_int (2)) in
6+
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
7+
let rec use (uu___ : unit) : FStar_Int32.t=
8+
let arr =
9+
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
10+
(Stdint.Uint64.of_int (2)) in
11+
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
12+
let rec use_gen_init (uu___ : unit) : FStar_Int32.t=
13+
let arr =
14+
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
15+
(Stdint.Uint64.of_int (2)) in
16+
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
17+
let rec use_gen_init_st (uu___ : unit) : FStar_Int32.t=
18+
let init uu___1 uu___2 = (Stdint.Int32.of_int (123)) in
19+
let __anf0 = init () () in
20+
let arr =
21+
Pulse_Lib_HigherArray_Core.mask_alloc () __anf0
22+
(Stdint.Uint64.of_int (2)) in
23+
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
24+
let rec use_gen_len (uu___ : unit) : FStar_Int32.t=
25+
let arr =
26+
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
27+
(Stdint.Uint64.of_int (2)) in
28+
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()
29+
let rec use_gen_len_st (uu___ : unit) : FStar_Int32.t=
30+
let len uu___1 uu___2 = (Stdint.Uint64.of_int (42)) in
31+
let __anf0 = len () () in
32+
let arr =
33+
Pulse_Lib_HigherArray_Core.mask_alloc () (Stdint.Int32.of_int (123))
34+
__anf0 in
35+
Pulse_Lib_HigherArray_Core.mask_read arr Stdint.Uint64.zero () () ()

‎test/Null.ml.expected‎

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,10 @@
11
open Prims
2-
let (x : Prims.int Pulse_Lib_HigherReference.ref) =
2+
let x : Prims.int Pulse_Lib_HigherReference.ref=
33
Pulse_Lib_HigherReference.null ()
4-
let (y : unit -> Prims.int Pulse_Lib_Box.box) =
5-
fun uu___ -> Pulse_Lib_Box.null ()
6-
let rec (foo : unit -> Prims.int Pulse_Lib_Box.box) =
7-
fun uu___ -> Pulse_Lib_Box.null ()
8-
let rec (test : Prims.int Pulse_Lib_HigherReference.ref -> Prims.int) =
9-
fun x1 ->
10-
if Pulse_Lib_HigherReference.is_null x1
11-
then Prims.int_zero
12-
else Pulse_Lib_HigherReference.read x1 () ()
4+
let y (uu___ : unit) : Prims.int Pulse_Lib_Box.box= Pulse_Lib_Box.null ()
5+
let rec foo (uu___ : unit) : Prims.int Pulse_Lib_Box.box=
6+
Pulse_Lib_Box.null ()
7+
let rec test (x1 : Prims.int Pulse_Lib_HigherReference.ref) : Prims.int=
8+
if Pulse_Lib_HigherReference.is_null x1
9+
then Prims.int_zero
10+
else Pulse_Lib_HigherReference.read x1 () ()

‎test/Unobservable.ml.expected‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
open Prims
2-
let rec (incr : Prims.int -> Prims.int) = fun x -> x + Prims.int_one
3-
let rec (test : unit -> Prims.int) =
4-
fun uu___ -> let x = incr Prims.int_one in incr x
5-
let rec (test2 : unit -> Prims.int) = fun uu___ -> incr Prims.int_one
2+
let rec incr (x : Prims.int) : Prims.int= x + Prims.int_one
3+
let rec test (uu___ : unit) : Prims.int= let x = incr Prims.int_one in incr x
4+
let rec test2 (uu___ : unit) : Prims.int= incr Prims.int_one

0 commit comments

Comments
 (0)