编译步骤/类型检查/函数应用隐式参数合成。豫
yuyan · 592 行 · 29534 字节 · UTF-8
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592
寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「模式合一」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「模式合一结构比较」之书。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「抽象语法树」之「总集」之书。
寻观「编译器核心」之「编译数据」之「抽象绑定树结构」之「命名环境术」之书。
寻观「编译器核心」之「编译数据」之「操作符」之「操作符数据结构」之书。
寻观「编译器核心」之「顺序标识符」之「顺序标识符」之书。
寻观「编译器核心」之「编译步骤」之「类型检查」之「类型检查基础」之书。
「函数应用接地信息」即「表达式」
合(「或可有」于「表达式」)
也。 「:含局部变量的类型、可直接读取的 ground 类型:」
「函数应用类型骨架」即
「匹配合一上下文」
合(「列」于「字符串」)
合(「列」于「表达式」)
合「表达式」
也。 「:上下文、按声明顺序的隐式变量名、显式参数类型、返回类型:」
「函数应用参数组」即
(「列」于「表达式」)
合(「列」于「表达式」)
合(「列」于(「参数形式」合「表达式」))
也。 「:已给隐式参数、当前函数的全部显式参数、剩余调用脊:」
「收集函数调用头脊」乃
化「表达式」而
「表达式」合(「列」于(「参数形式」合「表达式」))
也。
「收集函数调用头脊」者会「式」而
鉴「式」而
有(「式节点」于「函数调用」于(「缀」于「头」于「参数节点们」))则
「头」
与((「态射」)
于「参数节点们」
于(会「参数节点式」而
鉴「参数节点式」而
有(「式节点」于(「参数节点」于「形」)于((「列」【「参数」】)))则「形」与「参数」
或有「其他」则
「发生事故」于『函数调用脊必须是单参数节点』
)
)
或有「其他」则「式」与「罄」
也。
「读取函数应用实参类型」乃
化「命名环境」而
化「表达式」而
「或可有」于「表达式」
也。
「读取函数应用实参类型」者会「境」而会「参数」而
鉴「参数」而
有(「式节点」于(「源码范围标注节点」于「忽略范围」)于((「列」【「源码参数」】)))则
「读取函数应用实参类型」于「境」于「源码参数」
或有(「自由变量」于「名」)则(
鉴(「解析单个名称及物」于「境」于「名」)而
有(「可有」于(「参数类」与「忽略参数物」))则
「可有」于「参数类」
或有「可无」则
「可无」 「:模式中的新绑定尚不在环境中:」
)
或有(「式节点」于(「文件定义引用节点」于「文件名」于「定义名」于「忽略序数」)于「罄」)则(
鉴(「文件定义引用类及物」于「境」于「文件名」于「定义名」)而
有(「参数类」与「忽略参数物」)则
「可有」于「参数类」
)
或有「其他参数」则「可无」
也。
「函数应用期望类自由名」乃化(「或可有」于「表达式」)而「列」于「字符串」也。
「函数应用期望类自由名」者会「可能期望类」而
鉴「可能期望类」而
有「可无」则「罄」
或有(「可有」于「期望类」)则
「读取式自由变量」于「期望类」
也。
「实例化函数应用隐式参数」乃
化(「列」于「字符串」)而
化「匹配合一上下文」而
化「表达式」而
「字符串」合「表达式」合
「匹配合一上下文」
也。
「实例化函数应用隐式参数」者会「已用名」而会「上下文」而会「绑定值域」而
鉴「绑定值域」而
有(「绑定」于「忽略原名」于「下式」)
则(
虑「全已用名」者
(「附加」授以「字符串」)于「已用名」
于(「读取式自由变量」于「下式」)而
递归虑「新局部名」其化「有」而「字符串」者会「无」而
虑「候选名」者「下个字符序数」于『__函数应用隐式参数__』而
若(「存在吗」授以「字符串」)
于(会「已有名」而「串相等」于「候选名」于「已有名」)于「全已用名」则
「新局部名」于「元」
否则
「候选名」
而
虑「名」者「新局部名」于「元」
而
虑「值域」者「解构替换绑定名非重复」于「一」于「名」于「下式」
而
虑「后上下文」者「匹配合一上下文添加变量」于「上下文」于「名」而
「名」
与「值域」与「后上下文」
)
或有「其他值域」则
「发生事故」于『隐式派值域必须是绑定』
也。
「读取函数应用类型骨架」乃
化(「列」于「字符串」)而
化「表达式」而
「函数应用类型骨架」
也。
「读取函数应用类型骨架」者会「初已用名」而会「头类」而
虑「初上下文」者「空串典」授以(「或可有」于「表达式」)而
虑「完成」者
(化「匹配合一上下文」而化(「列」于「字符串」)而化「表达式」而「函数应用类型骨架」也
会「上下文」而会「隐式名们」而会「显式函数类」而
鉴(「拆分多参数函数类型」于「显式函数类」)而
有(「可有」于(「参数类型们」与「返回类型」))则
「上下文」与「隐式名们」与「参数类型们」与
「返回类型」
或有「可无」则
「上下文」与「隐式名们」与「罄」与「显式函数类」
)而
鉴「头类」而
有(「式节点」于(「隐式派类型节点」于「参数个数」)于((「列」【「绑定值域」】)))
则(
递归虑「读取隐式参数们」
其
化「整数」而化(「列」于「字符串」)而化「匹配合一上下文」而化(「列」于「字符串」)而化「表达式」而
「函数应用类型骨架」者
会「剩余个数」而会「已用名」而会「上下文」而会「反隐式名们」而会「当前绑定值域」而
若(「等」于「剩余个数」于「零」)
则
「完成」于「上下文」于(「反转」于「反隐式名们」)于「当前绑定值域」
否则
(
鉴(「实例化函数应用隐式参数」于「已用名」于「上下文」于「当前绑定值域」)而
有(「隐式名」与「后绑定值域」与「后上下文」)则
「读取隐式参数们」
于(「减」于「剩余个数」于「一」)
于(「缀」于「隐式名」于「已用名」)
于「后上下文」
于(「缀」于「隐式名」于「反隐式名们」)于「后绑定值域」
)
而
「读取隐式参数们」于
「参数个数」于
「初已用名」于
「初上下文」于「罄」于
「绑定值域」
)
或有(「式节点」于「箭头类型节点」于「忽略类型们」)则
「完成」于「初上下文」于「罄」于「头类」
或有「其他类」则
「完成」于「初上下文」于「罄」于「其他类」
也。
「拆分函数应用参数组」乃
化「整数」而
化「整数」而
化「爻」而
化(「列」于(「参数形式」合「表达式」))而
「函数应用参数组」
也。
「拆分函数应用参数组」者会「隐式参数个数」而
会「显式参数个数」而
会「要求饱和」而
会「脊」而
递归虑「读取显式参数们」其化「整数」而化(「列」于「表达式」)而化(「列」于「表达式」)而化(「列」
于(「参数形式」合「表达式」))而「函数应用参数组」者
会「剩余个数」而会「隐式参数们」而会「反显式参数们」而会「剩余脊」而
若(「等」于「剩余个数」于「零」)
则
「隐式参数们」与(「反转」于「反显式参数们」)与「剩余脊」
否则
(
鉴「剩余脊」而
有(「缀」于(「显式」与「参数」)于「后脊」)则
「读取显式参数们」
于(「减」于「剩余个数」于「一」)
于「隐式参数们」
于(「缀」于「参数」于「反显式参数们」)
于
「后脊」
或有「罄」则
若「要求饱和」
则
「发生事故」于『函数应用缺少显式参数,不允许部分应用』
否则
「隐式参数们」与(「反转」于「反显式参数们」)
与「罄」
或有(「缀」于(「隐式」与「忽略参数」)于「忽略后脊」)则
「发生事故」于
『显式函数参数之间不可以出现隐式调用参数』
)
而
递归虑「读取隐式参数们」其化「整数」而化(「列」于「表达式」)而化(「列」于(「参数形式」合「表达式」))而
「函数应用参数组」者
会「剩余个数」而会「反隐式参数们」而会「剩余脊」而
若(「等」于「剩余个数」于「零」)
则
「读取显式参数们」
于「显式参数个数」
于(「反转」于「反隐式参数们」)于「罄」于「剩余脊」
否则
(
鉴「剩余脊」而
有(「缀」于(「隐式」与「参数」)于「后脊」)则
「读取隐式参数们」
于(「减」于「剩余个数」于「一」)
于(「缀」于「参数」于「反隐式参数们」)
于
「后脊」
或有「其他脊」则
「读取显式参数们」
于「显式参数个数」
于(「反转」于「反隐式参数们」)于「罄」于
「剩余脊」
)
而
「读取隐式参数们」于「隐式参数个数」于「罄」于「脊」
也。
「尝试接地函数应用类型」乃
化「匹配合一上下文」而
化「表达式」而
化「表达式」而
「匹配合一上下文」
也。
「尝试接地函数应用类型」者会「上下文」而会「含变量类」而会「ground类」而
鉴「ground类」而
有(「式节点」于(「隐式派类型节点」于「忽略参数个数」)于((「列」【「忽略值域」】)))则
「上下文」 「:直接读取的多态类型仍需实例化,不能作为 ground 类型:」
或有「其他ground类」则
「尝试匹配合一」于「上下文」于「含变量类」于「ground类」
也。
「接地函数应用隐式参数」乃
化「匹配合一上下文」而
化(「列」于「函数应用接地信息」)而
「匹配合一上下文」
也。
「接地函数应用隐式参数」者会「初上下文」而会「接地信息们」而
若(「等」于((「长度」授以「字符串」)于((「串典所有键」授以(「或可有」于「表达式」))于「初上下文」))
于
「零」)
则
「初上下文」
否则
(
虑「最终上下文」者
(「从左折叠」授以「函数应用接地信息」授以「匹配合一上下文」)
于(会「接地信息」而会
「上下文」而
鉴「接地信息」而
有(「含变量类」与「可无」)则
「上下文」
或有(「含变量类」与(「可有」于「ground类」))则
「尝试接地函数应用类型」于「上下文」于「含变量类」
于「ground类」
)于「初上下文」于「接地信息们」
而
虑「未解名」者「匹配合一上下文未解名」于「最终上下文」
而
若(「等」于(「长度」于「未解名」)于「零」)
则
「最终上下文」
否则
「发生事故」
于『函数应用的隐式参数无法完全确定:』附(「间合」于『,』于「未解名」)附
『;匹配合一上下文:』附(「匹配合一上下文表示」于「最终上下文」)
)
也。
「写入函数应用已给隐式参数」乃
化「匹配合一上下文」而
化(「列」于「字符串」)而
化(「列」于「表达式」)而
「匹配合一上下文」合(「列」于「字符串」)
也。
「写入函数应用已给隐式参数」者会「上下文」而会「剩余隐式名们」而会「剩余已给参数们」而
鉴「剩余已给参数们」而
有「罄」则「上下文」与「剩余隐式名们」
或有(「缀」于「参数」于「后参数们」)则(
鉴「剩余隐式名们」而
有(「缀」于「隐式名」于「后隐式名们」)
则(
虑「后上下文」者
(「串典更新」授以(「或可有」于「表达式」))
于
「上下文」于「隐式名」于(「可有」于「参数」)
而
「写入函数应用已给隐式参数」
于「后上下文」于「后隐式名们」于
「后参数们」
)
或有「罄」则「发生事故」于『函数应用提供了过多隐式参数』
)
也。
「求解函数应用隐式参数」乃
化「命名环境」而
化「函数应用类型骨架」而
化(「列」
于「表达式」 「:用户已给隐式参数:」
)而
化(「列」
于「表达式」 「:当前函数的全部显式参数:」
)而化(「或可有」于「表达式」)而
「列」
于「表达式」 「:只返回自动插入的隐式类型实参:」
也。
「求解函数应用隐式参数」者会「境」而会「骨架」而会「已给隐式参数们」而会「显式参数们」而会「可能期望类」而
鉴「骨架」而
有(「初上下文」与「隐式名们」与「参数类型们」与「返回类型」)
则(
虑「上下文及缺省名们」者
「写入函数应用已给隐式参数」于
「初上下文」于「隐式名们」于
「已给隐式参数们」而递归虑「读取显式接地信息们」其化(「列」于「表达式」)而化(「列」于「表达式」)而(「列」
于
「函数应用接地信息」)者会
「剩余参数类型们」而会
「剩余显式参数们」而鉴
「剩余参数类型们」与「剩余显式参数们」
而
有「罄」与「罄」则(「罄」授以「函数应用接地信息」)
或有(「缀」于「参数类型」于「后参数类型们」)与(「缀」于「参数」于「后显式参数们」)则
「缀」
于(「参数类型」与(「读取函数应用实参类型」于「境」于「参数」))
于(「读取显式接地信息们」于「后参数类型们」于「后显式参数们」)
或有「其他」则
「发生事故」
于
『函数应用骨架与显式实参数量不同:参数类型个数=』附(「整数表示」于(「长度」于「剩余参数类型们」))附
『,实参个数=』附(「整数表示」于(「长度」于「剩余显式参数们」))
而
虑「显式接地信息们」者
(
鉴「显式参数们」而
有「罄」则(「罄」授以「函数应用接地信息」) 「:裸多态函数由整个期望函数类型接地,没有显式实参信息:」
或有「非空显式参数们」则
「读取显式接地信息们」
于
「参数类型们」于「显式参数们」
)
而
虑「全部接地信息」者
(「附加」授以「函数应用接地信息」)
于
「显式接地信息们」
于((「列」【(「返回类型」与「可能期望类」)】))
而
虑「最终上下文」者
「接地函数应用隐式参数」
于(「上下文及缺省名们」中「零」)
于「全部接地信息」
而
(「态射」授以「字符串」授以「表达式」)
于(「上下文及缺省名们」中「一」)
于(会「隐式名」而(「获取可有内容」授以「表达式」)
于((「串典读取」授以(「或可有」于「表达式」))于「最终上下文」于「隐式名」))
)
也。
「添加当前函数应用组参数」乃
化「爻」而
化「表达式」而
化「参数形式」而
化「表达式」而
「表达式」
也。
「添加当前函数应用组参数」者会「已经开始」而会「函数」而会「形」而会「参数」而
若「已经开始」
则
「添加函数调用参数」于「函数」于「形」于「参数」
否则
「函数调用式」于「函数」于((「列」【(「参数节点式」于「形」于((「列」【「参数」】)))】))
也。
「检查函数应用参数组」乃
化「命名环境」而
化「表达式」而
化「表达式」而
化(「列」于「表达式」)而
化(「列」于「表达式」)而
化(「列」于「表达式」)而
「表达式」合「表达式」
也。
「检查函数应用参数组」者会「境」而会「头类」而会「头物」而会「已给隐式参数们」而会「显式参数们」而会「缺省隐式参数们」而
虑「全部隐式参数们」者
(「附加」授以「表达式」)于「已给隐式参数们」于「缺省隐式参数们」而
递归虑「检查隐式参数们」其化「表达式」而化「表达式」而化(「列」于「表达式」)而化「爻」而「表达式」合「表达式」合
「爻」者
会「当前类」而会「当前物」而会「剩余参数们」而会「已经开始」而
鉴「剩余参数们」而
有「罄」则「当前类」与「当前物」与「已经开始」
或有(「缀」于「参数」于「后参数们」)
则(
虑「后参数」者
(「读引用」于「进行类型类型检查引用」)于「境」于
「参数」而
虑「后类」者
「应用首隐式类型参数」于「当前类」于「后参数」而
虑「后物」者
「添加当前函数应用组参数」
于「已经开始」于「当前物」于
「隐式」于「后参数」
而
「检查隐式参数们」于「后类」于「后物」于
「后参数们」于「阳」
)
而
鉴(「检查隐式参数们」于「头类」于「头物」于「全部隐式参数们」于「阴」)而
有(「显式函数类」与「隐式后物」与「已经开始」)则(
鉴「显式参数们」而
有「罄」则「显式函数类」与「隐式后物」
或有「非空显式参数们」则(
鉴(「拆分多参数函数类型」于「显式函数类」)而
有(「可有」于(「参数类型们」与「返回类型」))
则(
虑「无」者
(
若(「等」于(「长度」于「参数类型们」)于(「长度」于「显式参数们」))则
「元」
否则
「发生事故」于『函数应用显式参数数量与函数类型不一致』
)
而
递归虑「检查显式参数们」其化「表达式」而化「爻」而化(「列」于「表达式」)而化(「列」于「表达式」)而
「表达式」者会「当前物」而
会「已有参数」而会「剩余参数们」而会「剩余类型们」而鉴
「剩余参数们」与「剩余类型们」而
有「罄」与「罄」则「当前物」
或有(「缀」于「参数」于「后参数们」)与(「缀」于「定义域」于「后类型们」)
则(
虑「后参数」者
(「读引用」于「进行对象类型检查引用」)
于
「境」于「参数」于「定义域」
而
虑「后物」者
「添加当前函数应用组参数」
于「已有参数」于
「当前物」于「显式」于「后参数」
而
「检查显式参数们」
于
「后物」于「阳」于「后参数们」于「后类型们」
)
或有「其他」则
「发生事故」于
『函数应用显式参数与参数类型没有一一对应』
而
虑「后物」者
「检查显式参数们」
于「隐式后物」于
「已经开始」于「显式参数们」于「参数类型们」
而
「返回类型」与「后物」
)
或有「可无」则
「发生事故」
于『函数调用的当前类型不是显式函数类型:』附(「表达式表示」于「显式函数类」)
)
)
也。
「进行已知头函数应用」乃
化「命名环境」而
化「表达式」而
化「表达式」而
化(「列」于(「参数形式」合「表达式」))而
化(「或可有」于「表达式」)而
「表达式」合「表达式」
也。
「进行已知头函数应用」者会「境」而会「头类」而会「头物」而会「脊」而会「可能期望类」而
虑「要求饱和」者(鉴「脊」而
有「罄」则「阴」
或有「非空脊」则「阳」)而
虑「初已用名」者
(「附加」授以「字符串」)
于(「读取式自由变量」于「头物」)
于((「附加」授以「字符串」)于(「函数应用期望类自由名」于「可能期望类」)于(「命名环境获取所有名称」于「境」))
而
鉴(「读取函数应用类型骨架」于「初已用名」于「头类」)而
有(「上下文」与「隐式名们」与「参数类型们」与「返回类型」)
则
若(「且」
于「要求饱和」
于(「且」于(「等」于(「长度」于「隐式名们」)于「零」)于(「等」于(「长度」于「参数类型们」)于「零」)))
则
「发生事故」于『函数调用的当前结果不是函数:』附(「表达式表示」于「头类」)
否则
(
鉴(「拆分函数应用参数组」于(「长度」于「隐式名们」)于(「长度」于「参数类型们」)于「要求饱和」于「脊」)
而
有(「已给隐式参数们」与「显式参数们」与「剩余脊」)
则(
虑「当前可能期望类」者
(鉴「剩余脊」而
有「罄」则「可能期望类」
或有「非空剩余脊」则「可无」授以「表达式」)
而
虑「接地返回类型」者
(
鉴「显式参数们」而
有「罄」则(
鉴「参数类型们」而
有「罄」则「返回类型」
或有「非空参数类型们」则
「多参数函数类型」于「参数类型们」于
「返回类型」
)
或有「非空显式参数们」则「返回类型」
)
而
虑「接地骨架」者「上下文」与「隐式名们」与「参数类型们」与
「接地返回类型」
而
虑「缺省隐式参数们」者
「求解函数应用隐式参数」
于「境」
于
「接地骨架」
于「已给隐式参数们」于「显式参数们」于
「当前可能期望类」
而
虑「当前结果」者
「检查函数应用参数组」
于「境」
于「头类」
于
「头物」
于「已给隐式参数们」于「显式参数们」于
「缺省隐式参数们」而鉴「剩余脊」而
有「罄」则「当前结果」
或有「非空剩余脊」则
「进行已知头函数应用」
于「境」
于(「当前结果」中「零」)
于(「当前结果」中「一」)于「剩余脊」于「可能期望类」
)
)
也。
「进行函数应用头脊类型合成」乃
化「命名环境」而
化「表达式」而
「表达式」合「表达式」
也。
「进行函数应用头脊类型合成」者会「境」而会「物」而
虑「头及脊」者「收集函数调用头脊」于「物」而
虑「头类及物」者
(「读引用」于「进行对象类型合成引用」)于「境」
于(「头及脊」中「零」)
而
「进行已知头函数应用」
于「境」
于(「头类及物」中「零」)
于(「头类及物」中「一」)
于(「头及脊」中「一」)
于(「可无」授以「表达式」)
也。
「进行函数应用头脊类型检查」乃
化「命名环境」而
化「表达式」而
化「表达式」而
「表达式」
也。
「进行函数应用头脊类型检查」者会「境」而会「物」而会「期望类」而
虑「头及脊」者「收集函数调用头脊」于「物」而
虑「头类及物」者
(「读引用」于「进行对象类型合成引用」)于「境」
于(「头及脊」中「零」)而
虑「结果类及物」者
「进行已知头函数应用」
于「境」
于(「头类及物」中「零」)
于(「头类及物」中「一」)
于(「头及脊」中「一」)
于(「可有」于「期望类」)而
虑「无」者
「断言类型相等」于(「结果类及物」中「零」)于「期望类」
而
「结果类及物」中「一」
也。