执行语义与编译实现

行一：求值之态

ρ 记局部值，σ 记可变位置，⟨e,ρ,σ⟩⇓⟨v,σ′⟩ 记求值；异常、退出、不终别列。静态验类不行一般用户术。

常量直得，名取词法绑定或已初始化全局。成函数则得代码与所捕之境，不行体。实参按值，引用传位置身份而非复制内容。

调用先函数，求首参而施之，得中间函数，乃求次参而施；源虽足参，不可先尽求实参而后行中间体；惟中间之施皆但新建闭包、无可见之效者（受调为已知顶层定义，其签名数内之参皆连续拉姆达），乃可依次先求诸参而一调直入，见编三；隐式类参已静定，不执行、不占槽。标准库「且」「或」诸普通函数先尽求实参，不短路；普通爻函之调不自得特殊条件之求。欲短路则用关键词且、或：甲且乙先求甲，甲阴即得阴，不求乙；甲或乙先求甲，甲阳即得阳，不求乙（提案 00022）。

虑先定义后尾；顺序存前作用而弃前值；元组依次求值；条件惟行所中；模式对象只求一次，不反算任意用户函数，惟选支行。附虽右结合，作用仍先左后右。

常源文（名。豫）之顶层惟有定义，无计算：顶层诸定义之值皆数据——函、字面、别名、构造器施于数据（含列与组）、以数据为初之「置匣」「置匣列」（静格，每程序之实一份），及以 令 绑数据于局部之名者。算、串之联与凡函之呼皆不得居顶层，验类报之；值须运行时算者，书为函 得「无」而 …，或以标准库之「一算」初取时算之一次。编译器书顶层数据为全局段之常初值，程序始时全局已备；串常逾一万字节者，限于引擎常数组之上限，启时自数据之段拷其字节。

试（名。测试。豫）、脚本（名。脚本。豫）、设计之源（名。设计。豫，提案〇〇〇一八）与金样（名其一。豫，号逐位书以汉字）之顶层即程序之体：顶层之语依次行之，所导之试与设计之源之体先于导之者行。设计之源凡源文皆可导之。

可执行之程序始于入口之函：入口之文（非试、脚本、金样）定「入口」，其类 化「有」为「有」，包述可以「入口函数」别指一名。程序启时依次行试与脚本之体，终呼入口之函一次。

行二：递归与状态

通用递归之法：分配一槽，初单位；自引用改读槽；求定义成闭包；写回槽；返闭包。捕获递归单元，不在未填时拷单位为自身。其余捕获依词法，引用保身份。

一般递归值若填前读自身，得占位或后误，不作惰性无限结构。无普遍终止检查，通过验类不谓必终。

引用新、读、写位置，写返单位，别名同观；迁堆保身份而可改裸址，故不作跨安全点稳定地址。数组与不安全原语边界非类型系统尽证。

行三：内建与异常

下名须在「」中，∀为承。原始尝试运行受一二元组，库可另包两参。有为单位类，元为其值，非顶类。

串异以 Wasm 原生之异为之。抛串即抛载其串之异（WasmGC throw $error），循调用之栈外传，最近未毕之尝试承之。尝试 (操作,处理)：于所承之域内行 操作(元)，常终则其果即尝试之果，不行处理；其间（并其所调之函）所抛之串异于此承之，抛处以后之句不复行；承之则先出所承之域，乃行 处理(s)，其果为尝试之果；处理自再抛，归外层。常途不分配，不书全局。

串异终无承者，至程序之入口，交顶层未承之术。其术之初值为标准库之「常处祸」：书“未捕捉的豫言异常：”并其辞于标准误，以退出码一终其程。程序不链「祸福」，则编译器所生之入口亦书“未捕捉的豫言异常：”并其辞于标准误，以退出码一终其程。

当前续延包装为可传之提前返回术，调用则向动态点送值。每入以当前续延调用，新立动态之标识；早返依标识寻其返点，途经之尝试不截之，入之次数无限。WasmGC 以异常标签及动态标识为之，不保证已毁栈可长存、反复恢复之多次续延。

模式缺支，抛与抛串同之可承之异，其辞定为“模式匹配错误，缺少分支：鉴表达式”，以保诸次编译之诊断常量相同。系统原语之退出与中止不经语言之处异。

编一：阶段与不变量

阶段可合，不得赖优化器使非法树可运行。跨模块优化可省；旧模块已引用直接公开入口，则必供之或桥接。

编二：ANF 之法

正规化取式与继续；直接值授继续，复杂式递归其子而以新鲜名绑定。先将显参脊左折为一参应用树，再逐节点正规函数、实参，令 r 为调用果而继续；惟已明分组之内部 IR 可一次授诸参。条件令继续为合流点，各生分支，毋先算两支。

尾位含函数末、条件支末及令 x=调用而返 x。ANF 临绑定不可失其尾位。WasmGC 以 return_call_indirect 保尾调用不增调用栈。

编三：闭包与直调桥

函数自由值 v1…vk 依固定私序，分配 [代码,v1,…,vk]；代码受 self 与显参，vi 改 self[i]，i 自一始。间接调用只求闭包一次，读零项而传 self。捕获序属自身，不窥他方。

源码嵌套 λ 保逐参链，不可擅合而替旧全局闭包。直接入口依明示内部参组，不受 self；作函数值则包闭包，包装丢 self 而施直入。反向桥读所存闭包、插 self 而施。值全局与直接函数两类符号皆须可用。

今之实现：顶层定义依类型检查所得之签名定其数 N（右嵌之箭既展，显参之数，隐参不计）；定义首有不少于 N 层单参拉姆达者，生 N 参之直入（工函数），全局槽存逐参之门，门受满参则调直入。直入之名、定义之序与其数书于阶段产物“顶层元数”，他模据之于满参之调径调，余参逐一而施；拉姆达不足 N 层者不生直入，仍经全局槽。详见 库/译场/文档/函数应用形状分析.文言.md。

优化可删废值、合包装、直调；跨模块之试须保被验入口。已内联而无跨界调用，不作接口成功之证。

编四：数与平台

整数为六十四位补码。内建之减依六十四位环绕，比较为六十四位有符号之比，结果为爻。运行时所实现之加减乘除，溢出、除零、最小整除负一无统一稳定约；内建与运行时二途须分，不悉称环绕。

小数 binary64，常量依位模式精确生之。普通打印与中间产物之精确表示（十七位有效数字）不同，不以打印往返生常量。串依 UTF-8 原字节生之；源长度、码点数、字节数各别。

今之实（WasmGC 后端）：标准库之整数加、减、乘、除，与小数加、减、乘、除、整转小、小转整，皆编译器就地生 Wasm 之令。整数加减乘依六十四位环绕；整数除向零截之，除数为零或最小整除负一则陷。小数四则依 IEEE binary64，就近取偶，非数之号与载不约；整转小就近取偶；小转整向零截之，遇非数、无穷，或截后逾六十四位整数之域，则陷。陷即止其程序，尝试运行不能接，退码由宿主定。旧编译器所出之产物犹经宿主算此诸术，逾界者其果或异（如诺驿宿主之小转整依二之六十四次方环绕）。

数值原语之第二批（其目见网页汇编接口）亦就地生之。整数取余为截断之余，号随被除数，除数为零则陷，最小整余负一得零；无符号除与无符号余以二数皆为 u64，除数为零则陷；左移、右移、无符号右移、循环移位，位数模六十四，右移补其号位；前导零数、末尾零数、置位数得零至六十四；小等、大等依有符号较之，无符号小于、大于依 u64 较之。小数之较依 IEEE，遇非数唯“不等”为真，负零等于正零；最小、最大传非数，负零小于正零；绝对值、取负、复号惟改号位；向上取整、向下取整、截断、就近取整（取偶），其果仍为小数；开方正确舍入。小数饱和转整数向零截之，非数得零，越界取六十四位整数之最大或最小；无符号整数转小数以整数为 u64，就近取偶；小数位、位转小数按位重释，不易一位。

标准库之理解整数（原语字符串转整数）亦成于客内：越首之空白（空格及制表、换行、纵制表、换页、回车），识可有之正负号及其后之十进之数，遇他字则止，不验其尾；逾六十四位则依二之六十四次方回绕，无数则零。

编五：中间文件

ABI 兼容不须同缓存。若读旧阶段，则另守 ["豫言中间单元一",阶段名,有序定义数组]，项为 [名,公开性,表达式]，依阶段释索引、形状、身份、版本。文本为数据，不执行任意术。

模块互通依 Wasm 模块之导入、导出与类型身份。语言服务、排版、网站、缓存命中、调试注释及私有临名不入 ABI；异之不否已验互调，同之亦不足代互调。

编六：脚本之行

豫言之程有二行法（提案〇〇〇〇三）。

• 编而行：全程先过前端，无误乃生而行之；行时之序依行一。
• 脚本之行：诸模各编为装载单元（一模之豫汇与机器码，见《文件后缀》与《豫行格式》“装载单元”），装入方行之豫构进程，链接而后行。所导之模以单元装入，装时惟书顶层之数：常模之顶惟有定义（提案〇〇〇〇六），顶层之数由单元之 _start 书之，诸单元依装序行其 _start，后装者得读先装者之顶数；「一算」之值初取乃算，同编而行。具入口函数之常源，装毕复调入口一次。
• 豫构 运行 路径 参数… 编全脚本及其所依之模为单元，乃装而行之；前端之误先行而报，同编而行。
• 豫构 交互 逐组治之：一组者一句，或「乃」并其后同名之定义。每组过前端、编为组单元、装而行之，一组之效先于次组而成。有误之组（编有误，或行时有未接之异常）不录，其定义后不可见，先前之定义仍可用。末句为裸式，则依类型印其值。
• 二者之系：所受所拒之程同，求值之迹与输出同（《总纲》总〇）；所异者，报误之时（交互行至其组乃报）、优化之域（内联与全程之析惟行于单元之内）与速。
• 同名再定：依编译器之规，后定蔽前定，已编之引仍中早定（《类型与模块》）；欲随行而变者，用「置匣」「写匣」。
• 首行 #!：源文首行以 #! 起者，二行法皆以此行为空白（《词法与语法》）。
• 链接：单元导他模之函与全局，字段名与位无涉，全进程唯一；诸单元共一零号表与异常之标，闭包、客体与异常通行于单元之间。原生宿主依结构规范单元之类型，并入主程之实例，机器码依重定位装之（执行器之侧见客体二号说明“装载单元”）；诺驿宿主依网页汇编之导入导出逐一实例诸单元。
• 俟后之版：豫构 运行 改于豫构进程内编之（今以编译器子进程治前端）；交互中同类之构造器分数组而定。