Fixed-shape liveness compilation. The result is a checked arena plan, not a
runtime request to substitute a different tensor shape.
819def lifetimeComesBeforeOrEqual =
820 (lambda unrestricted left : (family Lifetime) .
821 (lambda unrestricted right : (family Lifetime) .
822 (eliminate
823 Lifetime
824 (lambda unrestricted current : (family Lifetime) . Nat)
825 left
826 (branch
827 LifetimeValue
828 leftTensor
829 leftFirst
830 leftLast
831 leftBytes
832 leftAlignment
833 .
834 (eliminate
835 Lifetime
836 (lambda unrestricted current : (family Lifetime) . Nat)
837 right
838 (branch
839 LifetimeValue
840 rightTensor
841 rightFirst
842 rightLast
843 rightBytes
844 rightAlignment
845 .
846 (naturalFlagOr
847 (nat-less-than (modelWord32ToNatural leftFirst) (modelWord32ToNatural rightFirst))
848 (naturalFlagAnd
849 (livenessNaturalEqual
850 (modelWord32ToNatural leftFirst)
851 (modelWord32ToNatural rightFirst))
852 (eliminate
853 TensorId
854 (lambda unrestricted current : (family TensorId) . Nat)
855 leftTensor
856 (branch
857 TensorIdValue
858 leftId
859 .
860 (eliminate
861 TensorId
862 (lambda unrestricted current : (family TensorId) . Nat)
863 rightTensor
864 (branch
865 TensorIdValue
866 rightId
867 .
868 (naturalLessThanOrEqual
869 (modelWord32ToNatural leftId)
870 (modelWord32ToNatural rightId))))))))))))))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.