diff options
author | Son Ho | 2023-05-16 11:45:43 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | df4d60b71bcabf9897656d6d74157a4c7d8d539c (patch) | |
tree | 3cbf4a825484f962339e78313646cd1f1724192e /tests/coq/betree | |
parent | b1dd8274d7a1cff2b9427e4356b66c4e63fe498c (diff) |
Make good progress on generating code for HOL4
Diffstat (limited to '')
-rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index dc97a9e9..940b8650 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -56,7 +56,7 @@ Definition betree_fresh_node_id_back (counter : u64) : result u64 := (** [betree_main::betree::NodeIdCounter::{0}::new] *) Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t := - Return {| Betree_node_id_counter_next_node_id := (0%u64) |} + Return {| Betree_node_id_counter_next_node_id := 0%u64 |} . (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *) @@ -75,7 +75,7 @@ Definition betree_node_id_counter_fresh_id_back (** [core::num::u64::{10}::MAX] *) Definition core_num_u64_max_body : result u64 := - Return (18446744073709551615%u64) + Return 18446744073709551615%u64 . Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global. @@ -86,7 +86,7 @@ Definition betree_upsert_update_fwd | None => match st with | BetreeUpsertFunStateAdd v => Return v - | BetreeUpsertFunStateSub i => Return (0%u64) + | BetreeUpsertFunStateSub i => Return 0%u64 end | Some prev0 => match st with @@ -94,7 +94,7 @@ Definition betree_upsert_update_fwd margin <- u64_sub core_num_u64_max_c prev0; if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c | BetreeUpsertFunStateSub v => - if prev0 s>= v then u64_sub prev0 v else Return (0%u64) + if prev0 s>= v then u64_sub prev0 v else Return 0%u64 end end . @@ -107,7 +107,7 @@ Fixpoint betree_list_len_fwd | S n0 => match self with | BetreeListCons t tl => i <- betree_list_len_fwd T n0 tl; u64_add 1%u64 i - | BetreeListNil => Return (0%u64) + | BetreeListNil => Return 0%u64 end end . @@ -1061,8 +1061,7 @@ Definition betree_be_tree_new_fwd |}; Betree_be_tree_node_id_cnt := node_id_cnt0; Betree_be_tree_root := - (BetreeNodeLeaf - {| Betree_leaf_id := id; Betree_leaf_size := (0%u64) |}) + (BetreeNodeLeaf {| Betree_leaf_id := id; Betree_leaf_size := 0%u64 |}) |}) . |