proofs/containers/intrusive_doubly_linked_list/frames.bend
bend-collections-laws-containers@1.0.0.0 · 75 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as G
3import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/shape.bend as S
4
5
6def separated(~N: Data, ~eq: N -> N -> Bool, at: Maybe<&2,N>, xs: List<&2,N>) -> Data:
7 match at:
8 case None{}: Unit
9 case Some{n}: G.away(~N,~eq,n,xs)
10
11def optional_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +at: Maybe<&2,N>, +v: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, sep: separated(~N,~eq,at,xs), good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,g,at,v),p,xs,q):
12 match at:
13 case None{}: good
14 case Some{n}: S.segment_sp_frame(~N, ~R, ~P, ~eq,g,n,v,xs,p,q,sep,good)
15
16# Any other chain disjoint from the edited node and its two neighbours keeps
17# every next/prev link. It may be another root in the same association.
18def remove_segment_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +before: Maybe<&2,N>, +after: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, +an: G.away(~N,~eq,n,xs), ap: separated(~N,~eq,before,xs), aq: separated(~N,~eq,after,xs), good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.cut(~N, ~R, ~P,g,r,n,before,after),p,xs,q):
19 match before:
20 case None{}:
21 S.segment_sn_frame(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,after,None{}),r,after),n,None{},xs,p,q,an,S.segment_sh_frame(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,g,after,None{}),r,after,xs,p,q,optional_frame(~N, ~R, ~P, ~eq,g,after,None{},xs,p,q,aq,good)))
22 case Some{+prev}:
23 S.segment_sn_frame(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,after,Some{prev}),prev,after),n,None{}),n,None{},xs,p,q,an,
24 S.segment_sp_frame(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,after,Some{prev}),prev,after),n,None{},xs,p,q,an,
25 S.segment_sn_frame(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,g,after,Some{prev}),prev,after,xs,p,q,ap,optional_frame(~N, ~R, ~P, ~eq,g,after,Some{prev},xs,p,q,aq,good))))
26
27def prepend_segment_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +head: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, an: G.away(~N,~eq,n,xs), ah: separated(~N,~eq,head,xs), good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.attach(~N, ~R, ~P,g,r,n,head),p,xs,q):
28 S.segment_sh_frame(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,head),head,Some{n}),r,Some{n},xs,p,q,optional_frame(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,head),head,Some{n},xs,p,q,ah,S.segment_sn_frame(~N, ~R, ~P, ~eq,g,n,head,xs,p,q,an,good)))
29
30def root_effect(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, p: Maybe<&2,N>, q: Maybe<&2,N>, +x: R) -> Maybe<&2,N>:
31 match p:
32 case None{}: G.choose(~Maybe<&2,N>,req(r,x),q,G.head(~N, ~R, ~P,~req,g,x))
33 case Some{n}: G.head(~N, ~R, ~P,~req,g,x)
34
35def remove_root_effect(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>, +x: R) -> {G.head(~N, ~R, ~P,~req,G.cut(~N, ~R, ~P,g,r,n,p,q),x) == root_effect(~N, ~R, ~P,~req,g,r,p,q,x) : Maybe<&2,N>}:
36 match g p q:
37 case G.Graph{ns,ps,rs,f} None{} None{}: {==}
38 case G.Graph{ns,ps,rs,f} None{} Some{a}: {==}
39 case G.Graph{ns,ps,rs,f} Some{a} None{}: {==}
40 case G.Graph{ns,ps,rs,f} Some{a} Some{b}: {==}
41
42def root_effect_other(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +p: Maybe<&2,N>, +q: Maybe<&2,N>, +x: R, neq: {req(r,x) == False{} : Bool}) -> {root_effect(~N, ~R, ~P,~req,g,r,p,q,x) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}:
43 match p:
44 case None{}:
45 %Equal.sym(Bool,req(r,x),False{},neq) : {G.choose(~Maybe<&2,N>,_,q,G.head(~N, ~R, ~P,~req,g,x)) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}
46 {==}
47 case Some{n}: {==}
48
49def remove_other_root(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>, +x: R, neq: {req(r,x) == False{} : Bool}) -> {G.head(~N, ~R, ~P,~req,G.cut(~N, ~R, ~P,g,r,n,p,q),x) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}:
50 Equal.trans(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.cut(~N, ~R, ~P,g,r,n,p,q),x),root_effect(~N, ~R, ~P,~req,g,r,p,q,x),G.head(~N, ~R, ~P,~req,g,x),remove_root_effect(~N, ~R, ~P,~req,g,r,n,p,q,x),root_effect_other(~N, ~R, ~P,~req,g,r,p,q,x,neq))
51
52def prepend_root_effect(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +h: Maybe<&2,N>, +x: R) -> {G.head(~N, ~R, ~P,~req,G.attach(~N, ~R, ~P,g,r,n,h),x) == G.choose(~Maybe<&2,N>,req(r,x),Some{n},G.head(~N, ~R, ~P,~req,g,x)) : Maybe<&2,N>}:
53 match g h:
54 case G.Graph{ns,ps,rs,f} None{}: {==}
55 case G.Graph{ns,ps,rs,f} Some{a}: {==}
56
57def prepend_other_root(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +h: Maybe<&2,N>, +x: R, neq: {req(r,x) == False{} : Bool}) -> {G.head(~N, ~R, ~P,~req,G.attach(~N, ~R, ~P,g,r,n,h),x) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}:
58 %Equal.sym(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.attach(~N, ~R, ~P,g,r,n,h),x),G.choose(~Maybe<&2,N>,req(r,x),Some{n},G.head(~N, ~R, ~P,~req,g,x)),prepend_root_effect(~N, ~R, ~P,~req,g,r,n,h,x)) : {_ == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}
59 %Equal.sym(Bool,req(r,x),False{},neq) : {G.choose(~Maybe<&2,N>,_,Some{n},G.head(~N, ~R, ~P,~req,g,x)) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}
60 {==}
61
62def removed_next(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>, same: {eq(n,n) == True{} : Bool}) -> {G.next(~N, ~R, ~P, ~eq,G.cut(~N, ~R, ~P,g,r,n,p,q),n) == None{} : Maybe<&2,N>}:
63 match p:
64 case None{}: S.next_sn_self(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,q,None{}),r,q),n,None{},same)
65 case Some{prev}: S.next_sn_self(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,q,Some{prev}),prev,q),n,None{}),n,None{},same)
66
67def removed_nonhead_prev(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +p: N, +q: Maybe<&2,N>, same: {eq(n,n) == True{} : Bool}) -> {G.prev(~N, ~R, ~P, ~eq,G.cut(~N, ~R, ~P,g,r,n,Some{p},q),n) == None{} : Maybe<&2,N>}:
68 Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.cut(~N, ~R, ~P,g,r,n,Some{p},q),n),G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,q,Some{p}),p,q),n,None{}),n),None{},S.prev_sn(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,q,Some{p}),p,q),n,None{}),n,None{},n),S.prev_sp_self(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,q,Some{p}),p,q),n,None{},same))
69
70def removed_head_prev(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +q: Maybe<&2,N>, hp: {G.prev(~N, ~R, ~P, ~eq,g,n) == None{} : Maybe<&2,N>}, aq: separated(~N,~eq,q,Con{n,Nil{}})) -> {G.prev(~N, ~R, ~P, ~eq,G.cut(~N, ~R, ~P,g,r,n,None{},q),n) == None{} : Maybe<&2,N>}:
71 match q aq:
72 case None{} _:
73 Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.cut(~N, ~R, ~P,g,r,n,None{},None{}),n),G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,None{}),n),None{},S.prev_sn(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,None{}),n,None{},n),Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,None{}),n),G.prev(~N, ~R, ~P, ~eq,g,n),None{},S.prev_sh(~N, ~R, ~P, ~eq,g,r,None{},n),hp))
74 case Some{+x} Tuple{Tuple{neq,rev},rest}:
75 Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.cut(~N, ~R, ~P,g,r,n,None{},Some{x}),n),G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.sp(~N, ~R, ~P,g,x,None{}),r,Some{x}),n),None{},S.prev_sn(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.sp(~N, ~R, ~P,g,x,None{}),r,Some{x}),n,None{},n),Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.sp(~N, ~R, ~P,g,x,None{}),r,Some{x}),n),G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,x,None{}),n),None{},S.prev_sh(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,x,None{}),r,Some{x},n),Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,x,None{}),n),G.prev(~N, ~R, ~P, ~eq,g,n),None{},S.prev_sp_other(~N, ~R, ~P, ~eq,g,x,None{},n,neq),hp)))