1	# Shape and owner preservation for traversals with consumed cursor state.
2	import Base
3	import ../traversal_array.bend as Traversal
4	import ../traversal_loop.bend as Loop
5	import ./storage_witness.bend as Witness
6	import ./traversal_witness.bend as TraversalWitness
7	
8	type Sample<-Reader: Type,-Element: Data,-Context: Data,-reader: Reader,-result: Reader & Traversal.Visited<Context,Element>> is Data:
9	  Sample{context: Context,-value: Element,equation: {result == (reader,Traversal.Visited{context,value}) : Reader & Traversal.Visited<Context,Element>}}
10	
11	def store(~Reader: Type,~Element: Data,~Context: Data,+depth: Nat,-reader: Reader,+position: U32,-output: Array<Element>,
12	  -result: Reader & Traversal.Visited<Context,Element>,output_evidence: Witness.Witness(Element,depth,output),sample: Sample<Reader,Element,Context,reader,result>) ->
13	  TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_store(~Reader,~Element,~Context,position,output,result)>:
14	  match sample:
15	    case Sample{context,value,equation}:
16	      %Equal.sym(Reader & Traversal.Visited<Context,Element>,result,(reader,Traversal.Visited{context,value}),equation) :
17	        TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_store(~Reader,~Element,~Context,position,output,_)>
18	      TraversalWitness.StateEvidence{Array.set(Element,output,position,value),(position + 1 : U32),context,{==},Witness.write(Element,depth,output,position,value,output_evidence)}
19	
20	def step(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
21	  ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,
22	  ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
23	  +depth: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,reader_evidence: ReaderEvidence(reader),
24	  evidence: TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,state>) ->
25	  TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_step(~Reader,~Element,~Context,~read,state)>:
26	  match evidence:
27	    case TraversalWitness.StateEvidence{output,position,context,equation,output_evidence}:
28	      %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
29	        TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_step(~Reader,~Element,~Context,~read,_)>
30	      store(~Reader,~Element,~Context,depth,reader,position,output,read(reader,context),output_evidence,read_preserves(reader,context,reader_evidence))
31	
32	def spread_store(~Element: Data,~Context: Data,+depth: Nat,-input: Array<Element>,+position: U32,-output: Array<Element>,target: Traversal.Target<Context>,
33	  -result: Array<Element> & Element,output_evidence: Witness.Witness(Element,depth,output),observed: Witness.Read<Element,input,result>) ->
34	  TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_store(~Element,~Context,position,output,target,result)>:
35	  match target observed:
36	    case Traversal.Target{context,+address} Witness.Read{value,equation}:
37	      %Equal.sym(Array<Element> & Element,result,(input,value),equation) :
38	        TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_store(~Element,~Context,position,output,Traversal.Target{context,address},_)>
39	      TraversalWitness.StateEvidence{Array.set(Element,output,address,value),(position + 1 : U32),context,{==},Witness.write(Element,depth,output,address,value,output_evidence)}
40	
41	def spread_step(~Element: Data,~Context: Data,~target: Context -> Traversal.Target<Context>,
42	  +depth: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,input_evidence: Witness.ArrayWitness<Element,input>,
43	  evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,state>) ->
44	  TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_step(~Element,~Context,~target,state)>:
45	  match evidence:
46	    case TraversalWitness.StateEvidence{output,+position,context,equation,output_evidence}:
47	      %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,state,Traversal.State{input,output,position,context},equation) :
48	        TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_step(~Element,~Context,~target,_)>
49	      spread_store(~Element,~Context,depth,input,position,output,target(context),Array.get(Element,input,position),output_evidence,
50	        Witness.observed(Element,input,position,input_evidence))
51	
52	def update_sample(~Reader: Type,~Element: Data,~Context: Data,~combine: Element -> Element -> Element,
53	  +depth: Nat,-reader: Reader,+position: U32,-output: Array<Element>,-current: Element,-result: Reader & Traversal.Visited<Context,Element>,
54	  output_evidence: Witness.Witness(Element,depth,output),sample: Sample<Reader,Element,Context,reader,result>) ->
55	  TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_sample(~Reader,~Element,~Context,~combine,position,output,current,result)>:
56	  match sample:
57	    case Sample{context,value,equation}:
58	      %Equal.sym(Reader & Traversal.Visited<Context,Element>,result,(reader,Traversal.Visited{context,value}),equation) :
59	        TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_sample(~Reader,~Element,~Context,~combine,position,output,current,_)>
60	      TraversalWitness.StateEvidence{Array.set(Element,output,position,combine(current,value)),(position + 1 : U32),context,{==},
61	        Witness.write(Element,depth,output,position,combine(current,value),output_evidence)}
62	
63	def update_current(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,
64	  ~combine: Element -> Element -> Element,+depth: Nat,-reader: Reader,position: U32,context: Context,-output: Array<Element>,-result: Array<Element> & Element,
65	  output_evidence: Witness.Witness(Element,depth,output),observed: Witness.Read<Element,output,result>,sample: Sample<Reader,Element,Context,reader,read(reader,context)>) ->
66	  TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_current(~Reader,~Element,~Context,~read,~combine,position,context,reader,result)>:
67	  match observed:
68	    case Witness.Read{value,equation}:
69	      %Equal.sym(Array<Element> & Element,result,(output,value),equation) :
70	        TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_current(~Reader,~Element,~Context,~read,~combine,position,context,reader,_)>
71	      update_sample(~Reader,~Element,~Context,~combine,depth,reader,position,output,value,read(reader,context),output_evidence,sample)
72	
73	def update_step(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
74	  ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,~combine: Element -> Element -> Element,
75	  ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
76	  +depth: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,reader_evidence: ReaderEvidence(reader),
77	  evidence: TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,state>) ->
78	  TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_step(~Reader,~Element,~Context,~read,~combine,state)>:
79	  match evidence:
80	    case TraversalWitness.StateEvidence{output,+position,+context,equation,+output_evidence}:
81	      %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
82	        TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_step(~Reader,~Element,~Context,~read,~combine,_)>
83	      update_current(~Reader,~Element,~Context,~read,~combine,depth,reader,position,context,output,Array.get(Element,output,position),output_evidence,
84	        Witness.read(Element,depth,output,position,output_evidence),read_preserves(reader,context,reader_evidence))
85	
86	def update(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
87	  ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,~combine: Element -> Element -> Element,
88	  ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
89	  +depth: Nat,count: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,+reader_evidence: ReaderEvidence(reader),
90	  evidence: TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,state>) ->
91	  TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update(~Reader,~Element,~Context,~read,~combine,count,state)>:
92	  match count:
93	    case 0n: evidence
94	    case 1n+rest:
95	      update(~Reader,~Element,~Context,~ReaderEvidence,~read,~combine,~read_preserves,depth,rest,reader,
96	        Traversal.visit_update_step(~Reader,~Element,~Context,~read,~combine,state),reader_evidence,
97	        update_step(~Reader,~Element,~Context,~ReaderEvidence,~read,~combine,~read_preserves,depth,reader,state,reader_evidence,evidence))
98	
99	def fold_value(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~combine: Accumulator -> Element -> Accumulator,
100	  -reader: Reader,+position: U32,-accumulator: Accumulator,-result: Reader & Traversal.Visited<Context,Element>,sample: Sample<Reader,Element,Context,reader,result>) ->
101	  TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold_value(~Reader,~Element,~Accumulator,~Context,~combine,position,accumulator,result)>:
102	  match sample:
103	    case Sample{context,value,equation}:
104	      %Equal.sym(Reader & Traversal.Visited<Context,Element>,result,(reader,Traversal.Visited{context,value}),equation) :
105	        TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold_value(~Reader,~Element,~Accumulator,~Context,~combine,position,accumulator,_)>
106	      TraversalWitness.FoldEvidence{combine(accumulator,value),(position + 1 : U32),context,{==}}
107	
108	def fold_step(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
109	  ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,~combine: Accumulator -> Element -> Accumulator,
110	  ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
111	  -reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,reader_evidence: ReaderEvidence(reader),
112	  evidence: TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
113	  TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,state)>:
114	  match evidence:
115	    case TraversalWitness.FoldEvidence{accumulator,position,context,equation}:
116	      %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,state,Traversal.State{reader,accumulator,position,context},equation) :
117	        TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,_)>
118	      fold_value(~Reader,~Element,~Accumulator,~Context,~combine,reader,position,accumulator,read(reader,context),read_preserves(reader,context,reader_evidence))
119	
120	def fold_run(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
121	  ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,~combine: Accumulator -> Element -> Accumulator,
122	  ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
123	  count: Nat,-reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,+reader_evidence: ReaderEvidence(reader),
124	  evidence: TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
125	  TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold(~Reader,~Element,~Accumulator,~Context,~read,~combine,count,state)>:
126	  match count:
127	    case 0n: evidence
128	    case 1n+rest:
129	      fold_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,rest,reader,
130	        Traversal.visit_fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,state),reader_evidence,
131	        fold_step(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,reader,state,reader_evidence,evidence))