Lift reusable local semantics into a system operation type. Transfers,
choices and repetition retain their identities and order unchanged.
291def mapGlobalProtocolOperations =
292 (lambda erased source : Type 0 .
293 (lambda erased target : Type 0 .
294 (lambda erased payload : Type 0 .
295 (lambda erased decision : Type 0 .
296 (lambda unrestricted transform : (pi unrestricted value : source . target) .
297 (lambda unrestricted program : (family GlobalProtocol source payload decision) .
298 (eliminate
299 GlobalProtocol
300 (lambda unrestricted current : (family GlobalProtocol source payload decision) .
301 (family GlobalProtocol target payload decision))
302 program
303 (branch
304 GlobalProtocolEnd
305 .
306 (constructor GlobalProtocol GlobalProtocolEnd target payload decision))
307 (branch
308 GlobalProtocolLocal
309 role
310 value
311 rest
312 induction
313 .
314 (constructor
315 GlobalProtocol
316 GlobalProtocolLocal
317 target
318 payload
319 decision
320 role
321 (transform value)
322 induction))
323 (branch
324 GlobalProtocolTransfer
325 identity
326 value
327 rest
328 induction
329 .
330 (constructor
331 GlobalProtocol
332 GlobalProtocolTransfer
333 target
334 payload
335 decision
336 identity
337 value
338 induction))
339 (branch
340 GlobalProtocolRepeat
341 count
342 body
343 rest
344 bodyResult
345 restResult
346 .
347 (constructor
348 GlobalProtocol
349 GlobalProtocolRepeat
350 target
351 payload
352 decision
353 count
354 bodyResult
355 restResult))
356 (branch
357 GlobalProtocolChoice
358 identity
359 selector
360 announcements
361 zeroBody
362 oneBody
363 rest
364 zeroResult
365 oneResult
366 restResult
367 .
368 (constructor
369 GlobalProtocol
370 GlobalProtocolChoice
371 target
372 payload
373 decision
374 identity
375 selector
376 announcements
377 zeroResult
378 oneResult
379 restResult)))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.