Commit 5fed2f9e authored by zhenlei's avatar zhenlei

function "get" done

parent e7ef2dc2
Pipeline #69849715 passed with stage
in 5 minutes and 11 seconds
......@@ -64,22 +64,33 @@ Require List.
| Left
| Right.
Definition binary_tree (a b : Set) := (a , b).
(* Definition binary_tree (a b : Set) := (a , b). *)
(* Inductive binary_tree (elt: Set) := *)
(* | Node : (binary_tree elt) -> (binary_tree elt) -> (binary_tree elt) *)
(* | Leaf : elt -> binary_tree elt. *)
(* compile storage into binary_tree *)
(* Fixpoint binary_tree_of (storage : type) := *)
Inductive binary_tree : Type :=
| Node : binary_tree -> binary_tree -> binary_tree
| Leaf : Type -> binary_tree .
(* get a element in tree *)
Fixpoint get {a b : Set} (tree: (Set * Set) (* binary_tree a b*)) (index: list direction)
Fixpoint get (tree: binary_tree) (index: list direction)
: option binary_tree
:=
match index with
| nil => tree
| nil => Some tree
| cons h t => match h with
| Left => let '(l,_) := tree in get l t
| Right => let (_,r) := tree in get r t
end
end.
| Left => match tree with
| Node l _ => get l t
| Leaf _ => None (* no exist element in left of node *)
end
| Right => match tree with
| Node _ r => get r t
| Leaf _ => None (* no exist element in right of node *)
end
end
end
.
Fixpoint rm {a b : Set} (tree: binary_tree a b) (index: list direction)
: option (binary_tree a b)
......@@ -112,6 +123,7 @@ Definition rebuild_storage_code
| Left =>
(* let to_insert before left_elt; continue *)
rebuild_storage_code left_elt to_insert t
;; PAIR
| Right =>
(* move to_insert before left_right *)
SWAP;;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment