81def planNativePhysicalMemory =
82 (lambda unrestricted state : Nat .
83 (lambda unrestricted slots : Nat .
84 (eliminate
85 StdBool
86 (lambda unrestricted flag : (family StdBool) .
87 (family
88 StdResult
89 (family NativePhysicalMemoryFailure)
90 (family NativePhysicalMemoryLayout)))
91 (stdBoolFromNatural (naturalNonzero state))
92 (branch
93 StdTrue
94 .
95 (eliminate
96 StdBool
97 (lambda unrestricted flag : (family StdBool) .
98 (family
99 StdResult
100 (family NativePhysicalMemoryFailure)
101 (family NativePhysicalMemoryLayout)))
102 (stdBoolFromNatural (nativePhysicalMemoryAdmitted state slots))
103 (branch
104 StdTrue
105 .
106 (let unrestricted slotBytes =
107 (naturalMultiply slots nativePhysicalMemoryWordBytes)
108 in
109 (let unrestricted scratch =
110 (naturalAdd state slotBytes)
111 in
112 (constructor
113 StdResult
114 StdSuccess
115 (family NativePhysicalMemoryFailure)
116 (family NativePhysicalMemoryLayout)
117 (constructor
118 NativePhysicalMemoryLayout
119 NativePhysicalMemoryLayoutOf
120 state
121 slotBytes
122 scratch
123 (naturalAdd scratch nativePhysicalMemoryScratchBytes))))))
124 (branch
125 StdFalse
126 .
127 (constructor
128 StdResult
129 StdFailure
130 (family NativePhysicalMemoryFailure)
131 (family NativePhysicalMemoryLayout)
132 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow)))))
133 (branch
134 StdFalse
135 .
136 (constructor
137 StdResult
138 StdFailure
139 (family NativePhysicalMemoryFailure)
140 (family NativePhysicalMemoryLayout)
141 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryEmpty))))))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.