75def makeSM86Control =
76 (lambda unrestricted stall : Byte .
77 (lambda unrestricted yieldMode : (family SM86YieldMode) .
78 (lambda unrestricted writeBarrier : (family SM86Barrier) .
79 (lambda unrestricted readBarrier : (family SM86Barrier) .
80 (lambda unrestricted waitMask : Byte .
81 (lambda unrestricted reuseMask : Byte .
82 (sm86ControlCheck
83 (nat-less-than (byte-to-nat stall) (byte-to-nat (byte 16)))
84 sm86ControlStallCode
85 (lambda unrestricted stallWitness : Nat .
86 (sm86ControlCheck
87 (nat-less-than (byte-to-nat waitMask) (byte-to-nat (byte 64)))
88 sm86ControlWaitMaskCode
89 (lambda unrestricted waitWitness : Nat .
90 (sm86ControlCheck
91 (nat-less-than (byte-to-nat reuseMask) (byte-to-nat (byte 16)))
92 sm86ControlReuseMaskCode
93 (lambda unrestricted reuseWitness : Nat .
94 (constructor
95 SM86ControlResult
96 SM86ControlValidated
97 (constructor
98 SM86Control
99 SM86ControlValue
100 stall
101 yieldMode
102 writeBarrier
103 readBarrier
104 waitMask
105 reuseMask))))))))))))))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.