1	import Base
2	
3	def both(-A: Data, -B: Data) -> Data:
4	  Sigma<&2,&2,A,_ => B>
5	
6	def left(-A: Data, -B: Data, p: both(A,B)) -> A:
7	  (a,b) = p
8	  a
9	
10	def right(-A: Data, -B: Data, p: both(A,B)) -> B:
11	  (a,b) = p
12	  b
13	
14	# Proof-only finite maps. New bindings shadow old ones; no storage layout,
15	# allocation strategy, machine integer width or payload type is assumed.
16	type Binding<-K: Data, -V: Data> is Data:
17	  Binding{key: K, value: V}
18	
19	def choose(~V: Data, b: Bool, yes: V, no: V) -> V:
20	  match b:
21	    case True{}: yes
22	    case False{}: no
23	
24	def lookup(~K: Data, ~V: Data, ~eq: K -> K -> Bool, +key: K, xs: List<&2, Binding<K, V>>, +default: V) -> V:
25	  match xs:
26	    case Nil{}: default
27	    case Con{Binding{k, v}, rest}: choose(~V, eq(k, key), v, lookup(~K, ~V, ~eq, key, rest, default))
28	
29	type Graph<-N: Data, -R: Data, -P: Data> is Data:
30	  Graph{nexts: List<&2, Binding<N, Maybe<&2, N>>>, prevs: List<&2, Binding<N, Maybe<&2, N>>>, roots: List<&2, Binding<R, Maybe<&2, N>>>, frame: P}
31	
32	def next(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, g: Graph<N,R,P>, n: N) -> Maybe<&2,N>:
33	  Graph{ns, ps, rs, f} = g
34	  lookup(~N, ~Maybe<&2,N>, ~eq, n, ns, None{})
35	
36	def prev(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, g: Graph<N,R,P>, n: N) -> Maybe<&2,N>:
37	  Graph{ns, ps, rs, f} = g
38	  lookup(~N, ~Maybe<&2,N>, ~eq, n, ps, None{})
39	
40	def head(~N: Data, ~R: Data, ~P: Data, ~eq: R -> R -> Bool, g: Graph<N,R,P>, r: R) -> Maybe<&2,N>:
41	  Graph{ns, ps, rs, f} = g
42	  lookup(~R, ~Maybe<&2,N>, ~eq, r, rs, None{})
43	
44	def frame(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>) -> P:
45	  Graph{ns, ps, rs, f} = g
46	  f
47	
48	def sn(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, n: N, v: Maybe<&2,N>) -> Graph<N,R,P>:
49	  Graph{ns, ps, rs, f} = g
50	  Graph{Con{Binding{n,v},ns}, ps, rs, f}
51	
52	def sp(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, n: N, v: Maybe<&2,N>) -> Graph<N,R,P>:
53	  Graph{ns, ps, rs, f} = g
54	  Graph{ns, Con{Binding{n,v},ps}, rs, f}
55	
56	def sh(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, r: R, v: Maybe<&2,N>) -> Graph<N,R,P>:
57	  Graph{ns, ps, rs, f} = g
58	  Graph{ns, ps, Con{Binding{r,v},rs}, f}
59	
60	def first(~N: Data, xs: List<&2,N>, d: Maybe<&2,N>) -> Maybe<&2,N>:
61	  match xs:
62	    case Nil{}: d
63	    case Con{x, rest}: Some{x}
64	
65	def last(~N: Data, xs: List<&2,N>, d: Maybe<&2,N>) -> Maybe<&2,N>:
66	  match xs:
67	    case Nil{}: d
68	    case Con{x, rest}: last(~N, rest, Some{x})
69	
70	def append(~N: Data, xs: List<&2,N>, +ys: List<&2,N>) -> List<&2,N>:
71	  match xs:
72	    case Nil{}: ys
73	    case Con{x, rest}: Con{x, append(~N, rest, ys)}
74	
75	# Away records disjoint identities in both directions. A lawful equality is
76	# reflexive and agrees with identity; the algorithm does not execute it.
77	def away(~N: Data, ~eq: N -> N -> Bool, +n: N, xs: List<&2,N>) -> Data:
78	  match xs:
79	    case Nil{}: Unit
80	    case Con{x, rest}: both(both({eq(n,x) == False{} : Bool}, {eq(x,n) == False{} : Bool}), away(~N, ~eq, n, rest))
81	
82	def unique(~N: Data, ~eq: N -> N -> Bool, xs: List<&2,N>) -> Data:
83	  match xs:
84	    case Nil{}: Unit
85	    case Con{+x, +rest}: both(away(~N, ~eq, x, rest), unique(~N, ~eq, rest))
86	
87	# A segment states BOTH links of EVERY member, with explicit external ends.
88	# With unique(xs), segment(g,None,xs,None) describes an acyclic reciprocal
89	# chain, rather than merely an ordered write trace.
90	def segment(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: Graph<N,R,P>, p: Maybe<&2,N>, xs: List<&2,N>, +q: Maybe<&2,N>) -> Data:
91	  match xs:
92	    case Nil{}: Unit
93	    case Con{+x, +rest}: both({prev(~N,~R,~P,~eq,g,x) == p : Maybe<&2,N>}, both({next(~N,~R,~P,~eq,g,x) == first(~N,rest,q) : Maybe<&2,N>}, segment(~N,~R,~P,~eq,g,Some{x},rest,q)))
94	
95	def valid(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, +g: Graph<N,R,P>, r: R, +xs: List<&2,N>) -> Data:
96	  both(unique(~N,~eq,xs), both({head(~N,~R,~P,~req,g,r) == first(~N,xs,None{}) : Maybe<&2,N>}, segment(~N,~R,~P,~eq,g,None{},xs,None{})))
97	
98	def disjoint(~N: Data, ~eq: N -> N -> Bool, xs: List<&2,N>, +ys: List<&2,N>) -> Data:
99	  match xs:
100	    case Nil{}: Unit
101	    case Con{x,rest}: both(away(~N,~eq,x,ys),disjoint(~N,~eq,rest,ys))
102	
103	def optional_prev(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, at: Maybe<&2,N>, v: Maybe<&2,N>) -> Graph<N,R,P>:
104	  match at:
105	    case None{}: g
106	    case Some{n}: sp(~N,~R,~P,g,n,v)
107	
108	def attach(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, r: R, +n: N, +h: Maybe<&2,N>) -> Graph<N,R,P>:
109	  sh(~N,~R,~P,optional_prev(~N,~R,~P,sn(~N,~R,~P,g,n,h),h,Some{n}),r,Some{n})
110	
111	def cut_left(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, r: R, +n: N, p: Maybe<&2,N>, q: Maybe<&2,N>) -> Graph<N,R,P>:
112	  match p:
113	    case None{}: sn(~N,~R,~P,sh(~N,~R,~P,g,r,q),n,None{})
114	    case Some{p}: sn(~N,~R,~P,sp(~N,~R,~P,sn(~N,~R,~P,g,p,q),n,None{}),n,None{})
115	
116	def cut(~N: Data, ~R: Data, ~P: Data, g: Graph<N,R,P>, r: R, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>) -> Graph<N,R,P>:
117	  cut_left(~N,~R,~P,optional_prev(~N,~R,~P,g,q,p),r,n,p,q)
118	
119	def prepend(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: Graph<N,R,P>, +r: R, n: N) -> Graph<N,R,P>:
120	  attach(~N,~R,~P,g,r,n,head(~N,~R,~P,~req,g,r))
121	
122	def remove(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: Graph<N,R,P>, r: R, +n: N) -> Graph<N,R,P>:
123	  cut(~N,~R,~P,g,r,n,prev(~N,~R,~P,~eq,g,n),next(~N,~R,~P,~eq,g,n))