Source/Systems

PartitionedRegression.CoordinateHost

systems/partitioned-regression/src/PartitionedRegression/CoordinateHost.alpha

1,739 lines132 declarations69.0 KiBSHA-256 b43df3e170d7

def · lines 621–656

chCombineAddress

Full file
These are locations already owned by the coordinate host layout. The planner admits each logical reference against this exact tree before use. An unknown reference maps outside the arena and is rejected by admission.
621def chCombineAddress =
622  (lambda unrestricted layout : (family CoordinateHostLayout) .
623    (lambda unrestricted reference : (family CombineReference) .
624      (nat-eliminate
625        (lambda unrestricted flag : Nat . Nat)
626        (nat-eliminate
627          (lambda unrestricted flag : Nat . Nat)
628          (nat-eliminate
629            (lambda unrestricted flag : Nat . Nat)
630            (nat-eliminate
631              (lambda unrestricted flag : Nat . Nat)
632              (nat-eliminate
633                (lambda unrestricted flag : Nat . Nat)
634                (chExtent layout)
635                (lambda unrestricted prior : Nat .
636                  (lambda unrestricted ignored : Nat . (framePayloadAt (chPrediction layout))))
637                (naturalEqual
638                  (combineReferenceSlot reference)
639                  (combineReferenceSlot chCombineRightInput)))
640              (lambda unrestricted prior : Nat .
641                (lambda unrestricted ignored : Nat . (chScratch layout)))
642              (naturalEqual
643                (combineReferenceSlot reference)
644                (combineReferenceSlot chCombineLeftInput)))
645            (lambda unrestricted prior : Nat .
646              (lambda unrestricted ignored : Nat . (chError layout)))
647            (naturalEqual (combineReferenceSlot reference) (combineReferenceSlot chCombineResult)))
648          (lambda unrestricted prior : Nat .
649            (lambda unrestricted ignored : Nat . (chPartial layout)))
650          (naturalEqual
651            (combineReferenceSlot reference)
652            (combineReferenceSlot chCombineRightReference)))
653        (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (chPartial layout)))
654        (naturalEqual
655          (combineReferenceSlot reference)
656          (combineReferenceSlot chCombineLeftReference)))))

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.