1 # One owned read/transform/write traversal. Reader and address mapping are static 2 # templates, so composition does not create a closure for each element. 3 import Base 4 import ./traversal_loop.bend as Loop 5 6 type Collected is Kind(ownership): 7 Collected{context: Context,value: Element} 8 9 def collect_prepend(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),value: Element,result: Reader & List) -> Reader & List: 10 (reader,values) = result 11 (reader,value <> values) 12 13 def collect_next(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Context: Data, 14 result: Reader & Collected,tail: Reader -> Context -> Reader & List) -> Reader & List: 15 (reader,Collected{context,value}) = result 16 collect_prepend(~ownership,~Reader,~Element,value,tail(reader,context)) 17 18 # Values may own arrays; a context transition supplies the next read without 19 # indexing a second list or allocating an array of affine elements. 20 def collect(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Context: Data, 21 ~read: Reader -> Context -> Reader & Collected,count: Nat,reader: Reader,context: Context) -> Reader & List: 22 match count: 23 case 0n: (reader,[]) 24 case 1n+rest: collect_next(~ownership,~Reader,~Element,~Context,read(reader,context),reader => context => collect(~ownership,~Reader,~Element,~Context,~read,rest,reader,context)) 25 26 def collect_list_next(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),result: Reader & Element, 27 tail: Reader -> Reader & List) -> Reader & List: 28 (reader,value) = result 29 collect_prepend(~ownership,~Reader,~Element,value,tail(reader)) 30 31 def collect_list(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Key: Data,~Context: Data, 32 ~read: Reader -> Context -> Key -> Reader & Element,keys: List<&2,Key>,reader: Reader,+context: Context) -> Reader & List: 33 match keys: 34 case Nil{}: (reader,[]) 35 case key <> rest: collect_list_next(~ownership,~Reader,~Element,read(reader,context,key),reader => collect_list(~ownership,~Reader,~Element,~Key,~Context,~read,rest,reader,context)) 36 37 # The same collections as one loop: the values so far, newest first, beside 38 # the reader and the next context, reversed once at the end. No closure is 39 # called, so a leaf task that collects stays fork-free. 40 type Gathering is Kind(reader_kind <&> ownership): 41 Gathering{reader: Reader,context: Context,values: List} 42 43 def reversed_onto(~ownership: Quant,~Element: Kind(ownership),values: List,tail: List) -> List: 44 match values: 45 case []: tail 46 case head <> rest: reversed_onto(~ownership,~Element,rest,head <> tail) 47 48 def gathered(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Context: Data, 49 result: Reader & Collected,values: List) -> Gathering<&1,ownership,Reader,Element,Context>: 50 (reader,Collected{context,value}) = result 51 Gathering{reader,context,value <> values} 52 53 def gather_step(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Context: Data, 54 ~read: Reader -> Context -> Reader & Collected,state: Gathering<&1,ownership,Reader,Element,Context>) -> 55 Gathering<&1,ownership,Reader,Element,Context>: 56 Gathering{reader,context,values} = state 57 gathered(~ownership,~Reader,~Element,~Context,read(reader,context),values) 58 59 def gathering_result(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Context: Data,state: Gathering<&1,ownership,Reader,Element,Context>) -> 60 Reader & List: 61 Gathering{reader,context,values} = state 62 (reader,reversed_onto(~ownership,~Element,values,[])) 63 64 def collect_loop(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Context: Data, 65 ~read: Reader -> Context -> Reader & Collected,count: Nat,reader: Reader,context: Context) -> Reader & List: 66 gathering_result(~ownership,~Reader,~Element,~Context, 67 Loop.run(~Gathering<&1,ownership,Reader,Element,Context>,~gather_step(~ownership,~Reader,~Element,~Context,~read),count,Gathering{reader,context,[]})) 68 69 # The keys not read yet travel in the context. 70 type Keyed<-Key: Data,-Context: Data> is Data: 71 Keyed{keys: List<&2,Key>,context: Context} 72 73 def gathered_key(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Key: Data,~Context: Data, 74 result: Reader & Element,rest: List<&2,Key>,context: Context,values: List) -> Gathering<&1,ownership,Reader,Element,Keyed>: 75 (reader,value) = result 76 Gathering{reader,Keyed{rest,context},value <> values} 77 78 def key_step(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Key: Data,~Context: Data, 79 ~read: Reader -> Context -> Key -> Reader & Element,keys: List<&2,Key>,reader: Reader,+context: Context,values: List) -> 80 Gathering<&1,ownership,Reader,Element,Keyed>: 81 match keys: 82 case []: Gathering{reader,Keyed{[],context},values} 83 case key <> rest: gathered_key(~ownership,~Reader,~Element,~Key,~Context,read(reader,context,key),rest,context,values) 84 85 def gather_key_step(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Key: Data,~Context: Data, 86 ~read: Reader -> Context -> Key -> Reader & Element,state: Gathering<&1,ownership,Reader,Element,Keyed>) -> 87 Gathering<&1,ownership,Reader,Element,Keyed>: 88 Gathering{reader,Keyed{keys,context},values} = state 89 key_step(~ownership,~Reader,~Element,~Key,~Context,~read,keys,reader,context,values) 90 91 def collect_list_loop(~ownership: Quant,~Reader: Type,~Element: Kind(ownership),~Key: Data,~Context: Data, 92 ~read: Reader -> Context -> Key -> Reader & Element,+keys: List<&2,Key>,reader: Reader,context: Context) -> Reader & List: 93 gathering_result(~ownership,~Reader,~Element,~Keyed, 94 Loop.run(~Gathering<&1,ownership,Reader,Element,Keyed>,~gather_key_step(~ownership,~Reader,~Element,~Key,~Context,~read), 95 List.length(&2,Key,keys),Gathering{reader,Keyed{keys,context},[]})) 96 97 def write_list(~Element: Data,values: List<&2,Element>,+offset: U32,storage: Array) -> Array: 98 match values: 99 case []: storage 100 case head <> tail: 101 write_list(~Element,tail,(offset + 1 : U32),Array.set(Element,storage,offset,head)) 102 103 type State is Kind(reader_kind <&> output_kind): 104 State{reader: Reader,output: Output,position: U32,context: Context} 105 106 # Indexed state updates share the traversal counter without requiring an array 107 # destination. The caller establishes any no-wrap bound on the U32 position. 108 def indexed_step(~Value: Type,~Context: Data,~update: U32 -> Context -> Value -> Value, 109 state: State<&2,&1,Unit,Value,Context>) -> State<&2,&1,Unit,Value,Context>: 110 State{Unit{},value,+position,+context} = state 111 State{Unit{},update(position,context,value),(position + 1 : U32),context} 112 113 def indexed_output(~Value: Type,~Context: Data,state: State<&2,&1,Unit,Value,Context>) -> Value: 114 State{Unit{},value,position,context} = state 115 value 116 117 def indexed_fold(~Value: Type,~Context: Data,~update: U32 -> Context -> Value -> Value, 118 count: Nat,position: U32,context: Context,value: Value) -> Value: 119 indexed_output(~Value,~Context, 120 Loop.run(~State<&2,&1,Unit,Value,Context>,~indexed_step(~Value,~Context,~update),count, 121 State{Unit{},value,position,context})) 122 123 def write_state(~Reader: Type,~Element: Data,~Context: Data,reader: Reader,output: Array,position: U32,context: Context, 124 destination: U32,value: Element) -> State<&1,&1,Reader,Array,Context>: 125 State{reader,Array.set(Element,output,destination,value),(position + 1 : U32),context} 126 127 def store(~Reader: Type,~Element: Data,~Context: Data,~destination: Context -> U32 -> U32, 128 +position: U32,+context: Context,output: Array,result: Reader & Element) -> State<&1,&1,Reader,Array,Context>: 129 (reader,value) = result 130 write_state(~Reader,~Element,~Context,reader,output,position,context,destination(context,position),value) 131 132 def step(~Reader: Type,~Element: Data,~Context: Data, 133 ~read: Reader -> Context -> U32 -> Reader & Element,~destination: Context -> U32 -> U32, 134 state: State<&1,&1,Reader,Array,Context>) -> State<&1,&1,Reader,Array,Context>: 135 State{reader,output,+position,+context} = state 136 store(~Reader,~Element,~Context,~destination,position,context,output,read(reader,context,position)) 137 138 def run(~Reader: Type,~Element: Data,~Context: Data, 139 ~read: Reader -> Context -> U32 -> Reader & Element,~destination: Context -> U32 -> U32, 140 count: Nat,state: State<&1,&1,Reader,Array,Context>) -> State<&1,&1,Reader,Array,Context>: 141 Loop.run(~State<&1,&1,Reader,Array,Context>,~step(~Reader,~Element,~Context,~read,~destination),count,state) 142 143 # Return both owners when the caller can reuse the source allocation later. 144 def finish(~Reader: Type,~Element: Data,~Context: Data,state: State<&1,&1,Reader,Array,Context>) -> Reader & Array: 145 State{reader,output,position,context} = state 146 (reader,output) 147 148 def index(context: Unit,position: U32) -> U32: 149 position 150 151 def read_index(~Element: Data,storage: Array,context: Unit,position: U32) -> Array & Element: 152 Array.get(Element,storage,position) 153 154 type Offsets is Data: 155 Offsets{source: U32,destination: U32} 156 157 def destination_offset(context: Offsets,position: U32) -> U32: 158 Offsets{source,destination} = context 159 (destination + position : U32) 160 161 def source_offset(~Element: Data,input: Array,context: Offsets,position: U32) -> Array & Element: 162 Offsets{source,destination} = context 163 Array.get(Element,input,(source + position : U32)) 164 165 # The values base, base + stride, base + 2 * stride, ... of one line. 166 type Strided is Data: 167 Strided{base: U32,stride: U32} 168 169 def strided(~Element: Data,input: Array,context: Strided,position: U32) -> Array & Element: 170 Strided{base,stride} = context 171 Array.get(Element,input,(base + position * stride : U32)) 172 173 def copy(~Element: Data,count: Nat,source: U32,destination: U32,input: Array,target: Array) -> Array & Array: 174 finish(~Array,~Element,~Offsets, 175 run(~Array,~Element,~Offsets,~source_offset(~Element),~destination_offset,count, 176 State{input,target,0,Offsets{source,destination}})) 177 178 # Ordered folds share the same state/counter and preserve the combine order. 179 # Element and Accumulator can differ; no associativity assumption is required. 180 def fold_value(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data, 181 ~combine: Accumulator -> Element -> Accumulator,accumulator: Accumulator, 182 position: U32,context: Context,result: Reader & Element) -> State<&1,&2,Reader,Accumulator,Context>: 183 (reader,value) = result 184 State{reader,combine(accumulator,value),(position + 1 : U32),context} 185 186 def fold_step(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data, 187 ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator, 188 state: State<&1,&2,Reader,Accumulator,Context>) -> State<&1,&2,Reader,Accumulator,Context>: 189 State{reader,accumulator,+position,+context} = state 190 fold_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,read(reader,context,position)) 191 192 def finish_fold(~Reader: Type,~Accumulator: Data,~Context: Data,state: State<&1,&2,Reader,Accumulator,Context>) -> Reader & Accumulator: 193 State{reader,accumulator,position,context} = state 194 (reader,accumulator) 195 196 def fold(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data, 197 ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator, 198 count: Nat,position: U32,reader: Reader,initial: Accumulator,context: Context) -> Reader & Accumulator: 199 finish_fold(~Reader,~Accumulator,~Context, 200 Loop.run(~State<&1,&2,Reader,Accumulator,Context>,~fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine), 201 count,State{reader,initial,position,context})) 202 203 # Eight values read one after another, before any of them is combined. 204 type Eight<-Element: Data> is Data: 205 Eight{a: Element,b: Element,c: Element,d: Element,e: Element,f: Element,g: Element,h: Element} 206 207 def read_last(~Reader: Type,~Element: Data,+a: Element,+b: Element,+c: Element,+d: Element,+e: Element,+f: Element,+g: Element, 208 result: Reader & Element) -> Reader & Eight: 209 (reader,h) = result 210 (reader,Eight{a,b,c,d,e,f,g,h}) 211 212 def read_seventh(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> U32 -> Reader & Element,+position: U32,+context: Context, 213 +a: Element,+b: Element,+c: Element,+d: Element,+e: Element,+f: Element,result: Reader & Element) -> Reader & Eight: 214 (reader,g) = result 215 read_last(~Reader,~Element,a,b,c,d,e,f,g,read(reader,context,(position + 1 : U32))) 216 217 def read_sixth(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> U32 -> Reader & Element,+position: U32,+context: Context, 218 +a: Element,+b: Element,+c: Element,+d: Element,+e: Element,result: Reader & Element) -> Reader & Eight: 219 (reader,f) = result 220 read_seventh(~Reader,~Element,~Context,~read,(position + 1 : U32),context,a,b,c,d,e,f,read(reader,context,(position + 1 : U32))) 221 222 def read_fifth(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> U32 -> Reader & Element,+position: U32,+context: Context, 223 +a: Element,+b: Element,+c: Element,+d: Element,result: Reader & Element) -> Reader & Eight: 224 (reader,e) = result 225 read_sixth(~Reader,~Element,~Context,~read,(position + 1 : U32),context,a,b,c,d,e,read(reader,context,(position + 1 : U32))) 226 227 def read_fourth(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> U32 -> Reader & Element,+position: U32,+context: Context, 228 +a: Element,+b: Element,+c: Element,result: Reader & Element) -> Reader & Eight: 229 (reader,d) = result 230 read_fifth(~Reader,~Element,~Context,~read,(position + 1 : U32),context,a,b,c,d,read(reader,context,(position + 1 : U32))) 231 232 def read_third(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> U32 -> Reader & Element,+position: U32,+context: Context, 233 +a: Element,+b: Element,result: Reader & Element) -> Reader & Eight: 234 (reader,c) = result 235 read_fourth(~Reader,~Element,~Context,~read,(position + 1 : U32),context,a,b,c,read(reader,context,(position + 1 : U32))) 236 237 def read_second(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> U32 -> Reader & Element,+position: U32,+context: Context, 238 +a: Element,result: Reader & Element) -> Reader & Eight: 239 (reader,b) = result 240 read_third(~Reader,~Element,~Context,~read,(position + 1 : U32),context,a,b,read(reader,context,(position + 1 : U32))) 241 242 # The values at position, position + 1, ..., position + 7. 243 def read_eight(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> U32 -> Reader & Element,+position: U32,+context: Context, 244 result: Reader & Element) -> Reader & Eight: 245 (reader,a) = result 246 read_second(~Reader,~Element,~Context,~read,(position + 1 : U32),context,a,read(reader,context,(position + 1 : U32))) 247 248 # The position after eight steps of one. 249 def after_eight(+position: U32) -> U32: 250 ((((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) 251 252 def combine_eight(~Element: Data,~Accumulator: Data,~combine: Accumulator -> Element -> Accumulator,accumulator: Accumulator,values: Eight) -> Accumulator: 253 Eight{+a,+b,+c,+d,+e,+f,+g,+h} = values 254 combine(combine(combine(combine(combine(combine(combine(combine(accumulator,a),b),c),d),e),f),g),h) 255 256 def round_value(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~combine: Accumulator -> Element -> Accumulator, 257 accumulator: Accumulator,+position: U32,+context: Context,result: Reader & Eight) -> State<&1,&2,Reader,Accumulator,Context>: 258 (reader,values) = result 259 State{reader,combine_eight(~Element,~Accumulator,~combine,accumulator,values),after_eight(position),context} 260 261 # Eight fold steps: the same reads and combines, the reads first. 262 def fold_round(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data, 263 ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator, 264 state: State<&1,&2,Reader,Accumulator,Context>) -> State<&1,&2,Reader,Accumulator,Context>: 265 State{reader,accumulator,+position,+context} = state 266 round_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context, 267 read_eight(~Reader,~Element,~Context,~read,position,context,read(reader,context,position))) 268 269 # fold with the steps after the first count % 8 taken eight at a time: the 270 # same result for every combine. The eight reads of a round come first, so an 271 # accumulator of several lanes keeps them in registers. 272 def fold_rounds(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data, 273 ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator, 274 count: Nat,position: U32,reader: Reader,initial: Accumulator,context: Context) -> Reader & Accumulator: 275 +count = count 276 finish_fold(~Reader,~Accumulator,~Context, 277 Loop.run(~State<&1,&2,Reader,Accumulator,Context>,~fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n), 278 Loop.run(~State<&1,&2,Reader,Accumulator,Context>,~fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n), 279 State{reader,initial,position,context}))) 280 281 # Reuse the output owner for each read/write; no second array or clone. 282 def mapped_value(~Element: Data,~Context: Data,~map: Context -> Element -> Element, 283 +position: U32,+context: Context,result: Array & Element) -> State<&2,&1,Unit,Array,Context>: 284 (output,value) = result 285 State{Unit{},Array.set(Element,output,position,map(context,value)),(position + 1 : U32),context} 286 287 def map_step(~Element: Data,~Context: Data,~map: Context -> Element -> Element, 288 state: State<&2,&1,Unit,Array,Context>) -> State<&2,&1,Unit,Array,Context>: 289 State{Unit{},output,+position,context} = state 290 mapped_value(~Element,~Context,~map,position,context,Array.get(Element,output,position)) 291 292 def mapped_output(~Element: Data,~Context: Data,state: State<&2,&1,Unit,Array,Context>) -> Array: 293 State{Unit{},output,position,context} = state 294 output 295 296 def map_in_place(~Element: Data,~Context: Data,~map: Context -> Element -> Element, 297 count: Nat,position: U32,context: Context,output: Array) -> Array: 298 mapped_output(~Element,~Context,Loop.run(~State<&2,&1,Unit,Array,Context>, 299 ~map_step(~Element,~Context,~map),count,State{Unit{},output,position,context})) 300 301 # Read the destination's current element, combine it with an owned reader, then 302 # store through the same traversal state. Distinct Array owners cannot alias. 303 def update_sample(~Reader: Type,~Element: Data,~Sample: Data,~Context: Data, 304 ~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32, 305 position: U32,context: Context,output: Array,current: Element,result: Reader & Sample) -> State<&1,&1,Reader,Array,Context>: 306 (reader,sample) = result 307 store(~Reader,~Element,~Context,~destination,position,context,output,(reader,combine(current,sample))) 308 309 def update_current(~Reader: Type,~Element: Data,~Sample: Data,~Context: Data, 310 ~read: Reader -> Context -> U32 -> Reader & Sample,~combine: Element -> Sample -> Element, 311 ~destination: Context -> U32 -> U32,reader: Reader,+position: U32,+context: Context,result: Array & Element) -> State<&1,&1,Reader,Array,Context>: 312 (output,current) = result 313 update_sample(~Reader,~Element,~Sample,~Context,~combine,~destination,position,context,output,current,read(reader,context,position)) 314 315 def update_step(~Reader: Type,~Element: Data,~Sample: Data,~Context: Data, 316 ~read: Reader -> Context -> U32 -> Reader & Sample,~combine: Element -> Sample -> Element, 317 ~destination: Context -> U32 -> U32,state: State<&1,&1,Reader,Array,Context>) -> State<&1,&1,Reader,Array,Context>: 318 State{reader,output,+position,+context} = state 319 update_current(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,reader,position,context, 320 Array.get(Element,output,destination(context,position))) 321 322 def update(~Reader: Type,~Element: Data,~Sample: Data,~Context: Data, 323 ~read: Reader -> Context -> U32 -> Reader & Sample,~combine: Element -> Sample -> Element, 324 ~destination: Context -> U32 -> U32,count: Nat,state: State<&1,&1,Reader,Array,Context>) -> State<&1,&1,Reader,Array,Context>: 325 Loop.run(~State<&1,&1,Reader,Array,Context>, 326 ~update_step(~Reader,~Element,~Sample,~Context,~read,~combine,~destination),count,state) 327 328 # A cursor is consumed by read and returned advanced. The state position is the 329 # absolute contiguous destination, so it need not retain a second cursor copy. 330 type Visited<-Context: Data,-Element: Data> is Data: 331 Visited{context: Context,value: Element} 332 333 def visit_store(~Reader: Type,~Element: Data,~Context: Data,+position: U32,output: Array,result: Reader & Visited) -> 334 State<&1,&1,Reader,Array,Context>: 335 (reader,Visited{context,value}) = result 336 write_state(~Reader,~Element,~Context,reader,output,position,context,position,value) 337 338 def visit_step(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> Reader & Visited, 339 state: State<&1,&1,Reader,Array,Context>) -> State<&1,&1,Reader,Array,Context>: 340 State{reader,output,position,context} = state 341 visit_store(~Reader,~Element,~Context,position,output,read(reader,context)) 342 343 def visit(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> Reader & Visited, 344 count: Nat,state: State<&1,&1,Reader,Array,Context>) -> State<&1,&1,Reader,Array,Context>: 345 Loop.run(~State<&1,&1,Reader,Array,Context>,~visit_step(~Reader,~Element,~Context,~read),count,state) 346 347 # A scatter reads the source at the state position, which counts up, and 348 # stores at the address its context names; target yields that address with 349 # the context of the next element. 350 type Target<-Context: Data> is Data: 351 Target{context: Context,address: U32} 352 353 def spread_store(~Element: Data,~Context: Data,position: U32,output: Array,target: Target,result: Array & Element) -> 354 State<&1,&1,Array,Array,Context>: 355 Target{context,address} = target 356 (input,value) = result 357 State{input,Array.set(Element,output,address,value),(position + 1 : U32),context} 358 359 def spread_step(~Element: Data,~Context: Data,~target: Context -> Target, 360 state: State<&1,&1,Array,Array,Context>) -> State<&1,&1,Array,Array,Context>: 361 State{input,output,+position,context} = state 362 spread_store(~Element,~Context,position,output,target(context),Array.get(Element,input,position)) 363 364 def visit_update_sample(~Reader: Type,~Element: Data,~Context: Data,~combine: Element -> Element -> Element, 365 +position: U32,output: Array,current: Element,result: Reader & Visited) -> State<&1,&1,Reader,Array,Context>: 366 (reader,Visited{context,value}) = result 367 write_state(~Reader,~Element,~Context,reader,output,position,context,position,combine(current,value)) 368 369 def visit_update_current(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> Reader & Visited, 370 ~combine: Element -> Element -> Element,position: U32,context: Context,reader: Reader,result: Array & Element) -> State<&1,&1,Reader,Array,Context>: 371 (output,current) = result 372 visit_update_sample(~Reader,~Element,~Context,~combine,position,output,current,read(reader,context)) 373 374 def visit_update_step(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> Reader & Visited, 375 ~combine: Element -> Element -> Element,state: State<&1,&1,Reader,Array,Context>) -> State<&1,&1,Reader,Array,Context>: 376 State{reader,output,+position,context} = state 377 visit_update_current(~Reader,~Element,~Context,~read,~combine,position,context,reader,Array.get(Element,output,position)) 378 379 def visit_update(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> Reader & Visited, 380 ~combine: Element -> Element -> Element,count: Nat,state: State<&1,&1,Reader,Array,Context>) -> State<&1,&1,Reader,Array,Context>: 381 Loop.run(~State<&1,&1,Reader,Array,Context>,~visit_update_step(~Reader,~Element,~Context,~read,~combine),count,state) 382 383 def visit_fold_value(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~combine: Accumulator -> Element -> Accumulator, 384 position: U32,accumulator: Accumulator,result: Reader & Visited) -> State<&1,&2,Reader,Accumulator,Context>: 385 (reader,Visited{context,value}) = result 386 State{reader,combine(accumulator,value),(position + 1 : U32),context} 387 388 def visit_fold_step(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~read: Reader -> Context -> Reader & Visited, 389 ~combine: Accumulator -> Element -> Accumulator,state: State<&1,&2,Reader,Accumulator,Context>) -> State<&1,&2,Reader,Accumulator,Context>: 390 State{reader,accumulator,position,context} = state 391 visit_fold_value(~Reader,~Element,~Accumulator,~Context,~combine,position,accumulator,read(reader,context)) 392 393 def visit_fold(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~read: Reader -> Context -> Reader & Visited, 394 ~combine: Accumulator -> Element -> Accumulator,count: Nat,state: State<&1,&2,Reader,Accumulator,Context>) -> State<&1,&2,Reader,Accumulator,Context>: 395 Loop.run(~State<&1,&2,Reader,Accumulator,Context>,~visit_fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),count,state)