diff options
| -rw-r--r-- | compiler/PureMicroPasses.ml | 8 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 81 | ||||
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 22 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 38 |
5 files changed, 66 insertions, 85 deletions
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 25d760fe..b9441397 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -828,6 +828,14 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx) let dont_filter () = let re, used_re = self#visit_texpression env re in let used = VarId.Set.union used (used_re ()) in + (* Simplify the left pattern if it only contains dummy variables *) + let lv = + if all_dummies then + let ty = lv.ty in + let value = PatDummy in + { value; ty } + else lv + in (Let (monadic, lv, re, e), fun _ -> used) in (* Potentially filter the let-binding *) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 81d81789..49b696b2 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2314,6 +2314,8 @@ and translate_forward_end (ectx : C.eval_ctx) let call = mk_apps func args in call in + + (* Create the let expression with the loop call *) mk_let effect_info.can_fail out_pat loop_call next_e and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 004db30e..10cdedd1 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -46,7 +46,7 @@ Definition betree_store_leaf_node_fwd (** [betree_main::betree::fresh_node_id] *) Definition betree_fresh_node_id_fwd (counter : u64) : result u64 := - i <- u64_add counter 1%u64; let _ := i in Return counter + _ <- u64_add counter 1%u64; Return counter . (** [betree_main::betree::fresh_node_id] *) @@ -62,8 +62,7 @@ Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t := (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) Definition betree_node_id_counter_fresh_id_fwd (self : Betree_node_id_counter_t) : result u64 := - i <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64; - let _ := i in + _ <- u64_add self.(Betree_node_id_counter_next_node_id) 1%u64; Return self.(Betree_node_id_counter_next_node_id) . @@ -242,15 +241,13 @@ Definition betree_leaf_split_back betree_list_split_at_fwd (u64 * u64) n content params.(Betree_params_split_size); let (content0, content1) := p in - p0 <- betree_list_hd_fwd (u64 * u64) content1; - let _ := p0 in + _ <- betree_list_hd_fwd (u64 * u64) content1; id0 <- betree_node_id_counter_fresh_id_fwd node_id_cnt; node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt; id1 <- betree_node_id_counter_fresh_id_fwd node_id_cnt0; - p1 <- betree_store_leaf_node_fwd id0 content0 st; - let (st0, _) := p1 in - p2 <- betree_store_leaf_node_fwd id1 content1 st0; - let (_, _) := p2 in + p0 <- betree_store_leaf_node_fwd id0 content0 st; + let (st0, _) := p0 in + _ <- betree_store_leaf_node_fwd id1 content1 st0; betree_node_id_counter_fresh_id_back node_id_cnt0 . @@ -343,10 +340,9 @@ Fixpoint betree_node_apply_upserts_fwd else ( p <- core_option_option_unwrap_fwd u64 prev st; let (st0, v) := p in - l <- + _ <- betree_list_push_front_fwd_back (u64 * Betree_message_t) msgs (key, BetreeMessageInsert v); - let _ := l in Return (st0, v)) end . @@ -401,24 +397,21 @@ Fixpoint betree_node_lookup_fwd then ( p1 <- betree_internal_lookup_in_children_fwd n0 node key st0; let (st1, opt) := p1 in - l0 <- + _ <- betree_node_lookup_first_message_for_key_back n0 key msgs (BetreeListCons (k, msg) l); - let _ := l0 in Return (st1, opt)) else match msg with | BetreeMessageInsert v => - l0 <- + _ <- betree_node_lookup_first_message_for_key_back n0 key msgs (BetreeListCons (k, BetreeMessageInsert v) l); - let _ := l0 in Return (st0, Some v) | BetreeMessageDelete => - l0 <- + _ <- betree_node_lookup_first_message_for_key_back n0 key msgs (BetreeListCons (k, BetreeMessageDelete) l); - let _ := l0 in Return (st0, None) | BetreeMessageUpsert ufs => p1 <- betree_internal_lookup_in_children_fwd n0 node key st0; @@ -443,10 +436,9 @@ Fixpoint betree_node_lookup_fwd | BetreeListNil => p0 <- betree_internal_lookup_in_children_fwd n0 node key st0; let (st1, opt) := p0 in - l <- + _ <- betree_node_lookup_first_message_for_key_back n0 key msgs BetreeListNil; - let _ := l in Return (st1, opt) end | BetreeNodeLeaf node => @@ -475,25 +467,22 @@ with betree_node_lookup_back let (k, msg) := p0 in if k s<> key then ( - l0 <- + _ <- betree_node_lookup_first_message_for_key_back n0 key msgs (BetreeListCons (k, msg) l); - let _ := l0 in node0 <- betree_internal_lookup_in_children_back n0 node key st0; Return (BetreeNodeInternal node0)) else match msg with | BetreeMessageInsert v => - l0 <- + _ <- betree_node_lookup_first_message_for_key_back n0 key msgs (BetreeListCons (k, BetreeMessageInsert v) l); - let _ := l0 in Return (BetreeNodeInternal node) | BetreeMessageDelete => - l0 <- + _ <- betree_node_lookup_first_message_for_key_back n0 key msgs (BetreeListCons (k, BetreeMessageDelete) l); - let _ := l0 in Return (BetreeNodeInternal node) | BetreeMessageUpsert ufs => p1 <- betree_internal_lookup_in_children_fwd n0 node key st0; @@ -509,25 +498,22 @@ with betree_node_lookup_back msgs0 <- betree_node_lookup_first_message_for_key_back n0 key msgs pending0; - p3 <- + _ <- betree_store_internal_node_fwd node0.(Betree_internal_id) msgs0 st2; - let (_, _) := p3 in Return (BetreeNodeInternal node0) end | BetreeListNil => - l <- + _ <- betree_node_lookup_first_message_for_key_back n0 key msgs BetreeListNil; - let _ := l in node0 <- betree_internal_lookup_in_children_back n0 node key st0; Return (BetreeNodeInternal node0) end | BetreeNodeLeaf node => p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st; let (_, bindings) := p in - opt <- betree_node_lookup_in_bindings_fwd n0 key bindings; - let _ := opt in + _ <- betree_node_lookup_in_bindings_fwd n0 key bindings; Return (BetreeNodeLeaf node) end end @@ -892,15 +878,13 @@ with betree_node_apply_messages_back p1 <- betree_internal_flush_back n0 node params node_id_cnt content0 st0; let (node0, node_id_cnt0) := p1 in - p2 <- + _ <- betree_store_internal_node_fwd node0.(Betree_internal_id) content1 st1; - let (_, _) := p2 in Return (BetreeNodeInternal node0, node_id_cnt0)) else ( - p0 <- + _ <- betree_store_internal_node_fwd node.(Betree_internal_id) content0 st0; - let (_, _) := p0 in Return (BetreeNodeInternal node, node_id_cnt)) | BetreeNodeLeaf node => p <- betree_load_leaf_node_fwd node.(Betree_leaf_id) st; @@ -912,15 +896,13 @@ with betree_node_apply_messages_back then ( p0 <- betree_leaf_split_fwd n0 node content0 params node_id_cnt st0; let (st1, new_node) := p0 in - p1 <- + _ <- betree_store_leaf_node_fwd node.(Betree_leaf_id) BetreeListNil st1; - let (_, _) := p1 in node_id_cnt0 <- betree_leaf_split_back n0 node content0 params node_id_cnt st0; Return (BetreeNodeInternal new_node, node_id_cnt0)) else ( - p0 <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0; - let (_, _) := p0 in + _ <- betree_store_leaf_node_fwd node.(Betree_leaf_id) content0 st0; Return (BetreeNodeLeaf (mkBetree_leaf_t node.(Betree_leaf_id) len), node_id_cnt)) end @@ -958,10 +940,9 @@ with betree_internal_flush_fwd betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params node_id_cnt0 msgs_right st0; let (st1, _) := p2 in - p3 <- + _ <- betree_node_apply_messages_back n0 self.(Betree_internal_right) params node_id_cnt0 msgs_right st0; - let (_, _) := p3 in Return (st1, BetreeListNil)) else Return (st0, msgs_right)) else ( @@ -969,10 +950,9 @@ with betree_internal_flush_fwd betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params node_id_cnt msgs_right st; let (st0, _) := p0 in - p1 <- + _ <- betree_node_apply_messages_back n0 self.(Betree_internal_right) params node_id_cnt msgs_right st; - let (_, _) := p1 in Return (st0, msgs_left)) end @@ -1037,10 +1017,9 @@ Definition betree_node_apply_fwd betree_node_apply_messages_fwd n self params node_id_cnt (BetreeListCons (key, new_msg) l) st; let (st0, _) := p in - p0 <- + _ <- betree_node_apply_messages_back n self params node_id_cnt (BetreeListCons (key, new_msg) l) st; - let (_, _) := p0 in Return (st0, tt) . @@ -1080,10 +1059,9 @@ Definition betree_be_tree_apply_fwd betree_node_apply_fwd n self.(Betree_be_tree_root) self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st; let (st0, _) := p in - p0 <- + _ <- betree_node_apply_back n self.(Betree_be_tree_root) self.(Betree_be_tree_params) self.(Betree_be_tree_node_id_cnt) key msg st; - let (_, _) := p0 in Return (st0, tt) . @@ -1107,8 +1085,7 @@ Definition betree_be_tree_insert_fwd := p <- betree_be_tree_apply_fwd n self key (BetreeMessageInsert value) st; let (st0, _) := p in - bt <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st; - let _ := bt in + _ <- betree_be_tree_apply_back n self key (BetreeMessageInsert value) st; Return (st0, tt) . @@ -1127,8 +1104,7 @@ Definition betree_be_tree_delete_fwd := p <- betree_be_tree_apply_fwd n self key BetreeMessageDelete st; let (st0, _) := p in - bt <- betree_be_tree_apply_back n self key BetreeMessageDelete st; - let _ := bt in + _ <- betree_be_tree_apply_back n self key BetreeMessageDelete st; Return (st0, tt) . @@ -1148,8 +1124,7 @@ Definition betree_be_tree_upsert_fwd := p <- betree_be_tree_apply_fwd n self key (BetreeMessageUpsert upd) st; let (st0, _) := p in - bt <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st; - let _ := bt in + _ <- betree_be_tree_apply_back n self key (BetreeMessageUpsert upd) st; Return (st0, tt) . diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 628eb2c3..854862b2 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -272,8 +272,7 @@ let betree_leaf_split_back | Return (st0, _) -> begin match betree_store_leaf_node_fwd id1 content1 st0 with | Fail e -> Fail e - | Return (_, _) -> - betree_node_id_counter_fresh_id_back node_id_cnt0 + | Return _ -> betree_node_id_counter_fresh_id_back node_id_cnt0 end end end @@ -603,7 +602,7 @@ and betree_node_lookup_back betree_store_internal_node_fwd node0.betree_internal_id msgs0 st2 with | Fail e -> Fail e - | Return (_, _) -> Return (BetreeNodeInternal node0) + | Return _ -> Return (BetreeNodeInternal node0) end end end @@ -1126,8 +1125,7 @@ and betree_node_apply_messages_back betree_store_internal_node_fwd node0.betree_internal_id content1 st1 with | Fail e -> Fail e - | Return (_, _) -> - Return (BetreeNodeInternal node0, node_id_cnt0) + | Return _ -> Return (BetreeNodeInternal node0, node_id_cnt0) end end end @@ -1136,7 +1134,7 @@ and betree_node_apply_messages_back betree_store_internal_node_fwd node.betree_internal_id content0 st0 with | Fail e -> Fail e - | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt) + | Return _ -> Return (BetreeNodeInternal node, node_id_cnt) end end end @@ -1164,7 +1162,7 @@ and betree_node_apply_messages_back betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 with | Fail e -> Fail e - | Return (_, _) -> + | Return _ -> begin match betree_leaf_split_back node content0 params node_id_cnt st0 with @@ -1179,7 +1177,7 @@ and betree_node_apply_messages_back betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 with | Fail e -> Fail e - | Return (_, _) -> + | Return _ -> Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len), node_id_cnt) end @@ -1234,7 +1232,7 @@ and betree_internal_flush_fwd betree_node_apply_messages_back self.betree_internal_right params node_id_cnt0 msgs_right st0 with | Fail e -> Fail e - | Return (_, _) -> Return (st1, BetreeListNil) + | Return _ -> Return (st1, BetreeListNil) end end else Return (st0, msgs_right) @@ -1251,7 +1249,7 @@ and betree_internal_flush_fwd betree_node_apply_messages_back self.betree_internal_right params node_id_cnt msgs_right st with | Fail e -> Fail e - | Return (_, _) -> Return (st0, msgs_left) + | Return _ -> Return (st0, msgs_left) end end end @@ -1338,7 +1336,7 @@ let betree_node_apply_fwd betree_node_apply_messages_back self params node_id_cnt (BetreeListCons (key, new_msg) l) st with | Fail e -> Fail e - | Return (_, _) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end @@ -1392,7 +1390,7 @@ let betree_be_tree_apply_fwd self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st with | Fail e -> Fail e - | Return (_, _) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 01fc457e..2a336271 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -311,7 +311,7 @@ let betree_leaf_split_back1 | Return (st1, _) -> begin match betree_store_leaf_node_fwd id1 content1 st1 with | Fail e -> Fail e - | Return (_, _) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end end @@ -350,7 +350,7 @@ let betree_leaf_split_back2 | Return (st1, _) -> begin match betree_store_leaf_node_fwd id1 content1 st1 with | Fail e -> Fail e - | Return (_, _) -> + | Return _ -> begin match betree_node_id_counter_fresh_id_back node_id_cnt0 with | Fail e -> Fail e @@ -691,8 +691,7 @@ and betree_node_lookup_back betree_store_internal_node_fwd node0.betree_internal_id msgs0 st5 with | Fail e -> Fail e - | Return (_, _) -> - Return (st0, BetreeNodeInternal node0) + | Return _ -> Return (st0, BetreeNodeInternal node0) end end end @@ -1219,7 +1218,7 @@ and betree_node_apply_messages_back'a betree_store_internal_node_fwd node0.betree_internal_id content1 st3 with | Fail e -> Fail e - | Return (_, _) -> + | Return _ -> Return (st0, (BetreeNodeInternal node0, node_id_cnt0)) end end @@ -1229,8 +1228,7 @@ and betree_node_apply_messages_back'a betree_store_internal_node_fwd node.betree_internal_id content0 st1 with | Fail e -> Fail e - | Return (_, _) -> - Return (st0, (BetreeNodeInternal node, node_id_cnt)) + | Return _ -> Return (st0, (BetreeNodeInternal node, node_id_cnt)) end end end @@ -1263,7 +1261,7 @@ and betree_node_apply_messages_back'a betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 with | Fail e -> Fail e - | Return (_, ()) -> + | Return _ -> begin match betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 with @@ -1279,7 +1277,7 @@ and betree_node_apply_messages_back'a betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 with | Fail e -> Fail e - | Return (_, _) -> + | Return _ -> Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id len), node_id_cnt)) end @@ -1326,7 +1324,7 @@ and betree_node_apply_messages_back1 betree_store_internal_node_fwd node0.betree_internal_id content1 st3 with | Fail e -> Fail e - | Return (_, _) -> + | Return _ -> betree_internal_flush_back1 node params node_id_cnt content0 st1 st0 end @@ -1337,7 +1335,7 @@ and betree_node_apply_messages_back1 betree_store_internal_node_fwd node.betree_internal_id content0 st1 with | Fail e -> Fail e - | Return (_, _) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end end @@ -1370,7 +1368,7 @@ and betree_node_apply_messages_back1 betree_leaf_split_back0 node content0 params node_id_cnt st1 st3 with | Fail e -> Fail e - | Return (_, ()) -> + | Return _ -> betree_leaf_split_back1 node content0 params node_id_cnt st1 st0 end @@ -1381,7 +1379,7 @@ and betree_node_apply_messages_back1 betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 with | Fail e -> Fail e - | Return (_, _) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end end @@ -1535,7 +1533,7 @@ and betree_internal_flush_back'a self.betree_internal_right params node_id_cnt0 msgs_right st3 st5 with | Fail e -> Fail e - | Return (_, ()) -> + | Return _ -> Return (st0, (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot n n0, node_id_cnt1)) @@ -1565,7 +1563,7 @@ and betree_internal_flush_back'a betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt msgs_right st st2 with | Fail e -> Fail e - | Return (_, ()) -> + | Return _ -> Return (st0, (Mkbetree_internal_t self.betree_internal_id self.betree_internal_pivot self.betree_internal_left n, node_id_cnt0)) @@ -1633,7 +1631,7 @@ and betree_internal_flush_back1 self.betree_internal_right params node_id_cnt0 msgs_right st3 st5 with | Fail e -> Fail e - | Return (_, ()) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end end @@ -1657,7 +1655,7 @@ and betree_internal_flush_back1 betree_node_apply_messages_back1 self.betree_internal_right params node_id_cnt msgs_right st st2 with | Fail e -> Fail e - | Return (_, ()) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end end @@ -1709,7 +1707,7 @@ let betree_node_apply_back'a betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons (key, new_msg) l) st st2 with | Fail e -> Fail e - | Return (_, ()) -> Return (st0, (self0, node_id_cnt0)) + | Return _ -> Return (st0, (self0, node_id_cnt0)) end end end @@ -1736,7 +1734,7 @@ let betree_node_apply_back1 betree_node_apply_messages_back1 self params node_id_cnt (BetreeListCons (key, new_msg) l) st st2 with | Fail e -> Fail e - | Return (_, ()) -> Return (st0, ()) + | Return _ -> Return (st0, ()) end end end @@ -1809,7 +1807,7 @@ let betree_be_tree_apply_back self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st st2 with | Fail e -> Fail e - | Return (_, ()) -> + | Return _ -> Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n) end end |