Period p: its steps; in the last, the final forward; the checkpoint's
temporary (the first period's the train operation made); the gathers;
in the last, the report put back; the checkpoint published, counting the
steps (and the contexts) taken so far.
384def coppeliusPeriod =
385 (lambda unrestricted entries : Bytes .
386 (lambda unrestricted adamW : (family NativePhysicalCommands) .
387 (lambda unrestricted period : Nat .
388 (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
389 (let unrestricted first = (coppeliusPeriodFirst period) in
390 (let unrestricted last = (naturalEqual period coppeliusLastPeriod) in
391 (let unrestricted gathered = (naturalAdd (naturalAdd first coppeliusRunCheckpointInterval) last) in
392 (let unrestricted taken = (naturalMultiply (succ period) coppeliusRunCheckpointInterval) in
393 (let unrestricted publish =
394 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublish taken taken tail) in
395 (let unrestricted gathers =
396 (coppeliusGathers entries gathered
397 (coppeliusStepsWhen last
398 (coppeliusReissue entries (naturalAdd gathered cgChunks) coppeliusRestorePiece publish)
399 publish)) in
400 (let unrestricted begun =
401 (coppeliusStepsWhen period
402 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointBegin gathers)
403 gathers) in
404 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeat coppeliusRunCheckpointInterval
405 (coppeliusStepBody entries adamW first)
406 (coppeliusStepsWhen last
407 (coppeliusReissue entries (naturalAdd first coppeliusRunCheckpointInterval) coppeliusFinalPiece begun)
408 begun)))))))))))))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.