Layout: every item but a label is one word. Labels are recorded at the
offset of the word that follows them; a duplicate name is refused.
116def aarch64LayoutAssemblyFrom :
117 (pi unrestricted assembly : (family AArch64Assembly) .
118 (pi unrestricted offset : Nat . (family AArch64AssemblyLayoutResult))) =
119 (lambda unrestricted assembly : (family AArch64Assembly) .
120 (eliminate
121 AArch64Assembly
122 (lambda unrestricted current : (family AArch64Assembly) .
123 (pi unrestricted offset : Nat . (family AArch64AssemblyLayoutResult)))
124 assembly
125 (branch
126 AArch64AssemblyEnd
127 .
128 (lambda unrestricted offset : Nat .
129 (constructor
130 AArch64AssemblyLayoutResult
131 AArch64AssemblyLayoutSuccess
132 (constructor AArch64LabelTable AArch64LabelTableEmpty)
133 offset)))
134 (branch
135 AArch64AssemblyEmit
136 instruction
137 tail
138 layoutTail
139 .
140 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
141 (branch
142 AArch64AssemblyLabel
143 name
144 tail
145 layoutTail
146 .
147 (lambda unrestricted offset : Nat .
148 (eliminate
149 AArch64AssemblyLayoutResult
150 (lambda unrestricted current : (family AArch64AssemblyLayoutResult) .
151 (family AArch64AssemblyLayoutResult))
152 (layoutTail offset)
153 (branch
154 AArch64AssemblyLayoutSuccess
155 labels
156 finalSize
157 .
158 (eliminate
159 AArch64LabelLookupResult
160 (lambda unrestricted lookup : (family AArch64LabelLookupResult) .
161 (family AArch64AssemblyLayoutResult))
162 (aarch64LookupLabel name labels)
163 (branch
164 AArch64LabelFound
165 existing
166 .
167 (constructor AArch64AssemblyLayoutResult AArch64AssemblyDuplicateLabel name))
168 (branch
169 AArch64LabelMissing
170 .
171 (constructor
172 AArch64AssemblyLayoutResult
173 AArch64AssemblyLayoutSuccess
174 (constructor AArch64LabelTable AArch64LabelTableEntry name offset labels)
175 finalSize))))
176 (branch
177 AArch64AssemblyDuplicateLabel
178 duplicate
179 .
180 (constructor AArch64AssemblyLayoutResult AArch64AssemblyDuplicateLabel duplicate)))))
181 (branch
182 AArch64AssemblyBranch
183 target
184 tail
185 layoutTail
186 .
187 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
188 (branch
189 AArch64AssemblyBranchLink
190 target
191 tail
192 layoutTail
193 .
194 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
195 (branch
196 AArch64AssemblyBranchIf
197 condition
198 target
199 tail
200 layoutTail
201 .
202 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
203 (branch
204 AArch64AssemblyCompareBranchIfZero
205 register
206 target
207 tail
208 layoutTail
209 .
210 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
211 (branch
212 AArch64AssemblyCompareBranchIfNotZero
213 register
214 target
215 tail
216 layoutTail
217 .
218 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))
219 (branch
220 AArch64AssemblyAddressOf
221 destination
222 target
223 tail
224 layoutTail
225 .
226 (lambda unrestricted offset : Nat . (layoutTail (naturalAdd offset 4))))))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.