编译步骤/代码生成/网页汇编栈表示证明。豫
yuyan · 180 行 · 9533 字节 · 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
寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则数据」之书。
「:文言:先定诸值之形,乃可去装;不以整数冒爻,不以引用入栈。汉语:零表示未证明,一为完整整数,二为布尔,三为单元,四为栈数组地址。该分析只消费合法 SSA;签名是待组合的调用约定,调用者仍须完成闭合、逃逸、入口类型守卫及分配容量证明。返回成功时给出每个局部值的表示,失败不产生可用证书。:」
「栈表示签」即(「列」于「整数」)
合「整数」
也。
「栈值表示」乃化(「数组引用类」于「整数」)而化「正则原子」而「整数」也。
「栈值表示」者会「表」而会「值」而
鉴「值」而
有(「正则局部」于「号」)则
「读数组引用」授以「整数」于「表」于「号」
或有(「正则整数」于「数」)则「一」
或有(「正则爻」于「真」)则「二」
或有「正则单元」则「三」
或有「其他」则「零」
也。
「栈诸值合签」乃
化(「数组引用类」于「整数」)而
化(「列」于「正则原子」)而
化(「列」于「整数」)而
「爻」
也。
「栈诸值合签」者会「表」而会「参」而会「签」而
鉴「参」而
有「罄」则(鉴「签」而
有「罄」则「阳」
或有「余签」则「阴」)
或有(「缀」于「值」于「余」)则(
鉴「签」而
有「罄」则「阴」
或有(「缀」于「类」于「余签」)则
「且」
于(「且」于(「大于」于「类」于「零」)于(「等于」于「类」于(「栈值表示」于「表」于「值」)))
于(「栈诸值合签」于「表」于「余」于「余签」)
)
也。
「栈原语签」乃化「字符串」而「栈表示签」也。
「栈原语签」者会「名」而
虑「双整」者(「列」于「整数」也(「列」【「一」,「一」】))而鉴「名」而
有『豫言_整数加』则「双整」与「一」
或有『豫言_整数减』则「双整」与「一」
或有『豫言_整数乘』则「双整」与「一」
或有『豫言_整数除』则「双整」与「一」
或有『豫言_整数相等』则「双整」与「二」
或有『豫言_整数大于』则「双整」与「二」
或有『豫言_读取引用数组』则(「列」【「四」,「一」】)与「一」
或有『豫言_写入引用数组』则(「列」【「一」,「一」,「四」】)与「三」
或有『豫言_新建引用数组』则「双整」与「四」
或有「其他」则(「罄」授以「整数」)与「零」
也。
「验栈表示」乃
化(化「字符串」而「栈表示签」)而
化「栈表示签」而
化「整数」而
化「正则函数」而
「或可有」于(「数组引用类」于「整数」)
也。
「验栈表示」者会「查签」而会「本签」而会「根号」而会「函」而
若「大于」于(「函」中「四」)于「二五六」则
「可无」
否则
若「非」于(「等于」于(「长度」授以「整数」于(「本签」中「零」))于(「长度」授以「整数」于(「函」中「二」)))
则
「可无」
否则
若「非」于(「或者」于(「等于」于(「本签」中「一」)于「一」)于(「等于」于(「本签」中「一」)于「三」))则
「可无」
否则
虑「表」者
「新数组引用」授以「整数」于「零」于(「函」中「四」)
而
虑「好」者「新引用」授以「爻」于「阳」
而
虑「记」者
(化「整数」而化「整数」而「有」也会「号」而会「类」而「写数组引用」授以「整数」于「表」于「号」于「类」)
而
虑「拒」者
(化「有」而「有」也会「无」而「写引用」于「好」于「阴」)
而
虑「无」者
「态射」授以「整数」授以「有」
于(「整数范围」于「零」于(「长度」授以「整数」于(「函」中「二」)))
于(会「位」
而
虑「类」者「第N个」授以「整数」于「位」于(「本签」中「零」)而
若「或者」于(「等于」于「类」于「一」)于(「等于」于「类」于「四」)则
「记」于(「第N个」授以「整数」于「位」于(「函」中「二」))于「类」
否则
「拒」于「元」)而
递归虑「扫」其化「正则区域」而「整数」者会「段」而
鉴「段」而
有(「正则段」于「诸令」于「终」)则(
虑「无」者
「态射」授以「正则指令」授以「有」
于「诸令」
于(会「令」而鉴「令」而
有(「正则运算」于「号」于「类」于「术」于「参」)则(
虑「约」者鉴「术」而
有(「正则原语」于「名」)则(
虑「无」者
若「串相等」于「名」于『豫言_新建引用数组』则
若「且」
于(「非」于(「小于」于「根号」于「零」))
于(「等于」于「号」于「根号」)则
「元」
否则
「拒」于「元」
否则
「元」
而
「栈原语签」于「名」
)
或有「正则调用」则(
鉴「参」而
有(「缀」于(「正则函数引用」于「名」)于「余」)则(
虑「签」者「查签」于「名」
而
若「且」
于(「或者」
于(「等于」于(「签」中「一」)于「一」)
于(「等于」于(「签」中「一」)于「三」))
于(「全部符合」授以「整数」
于(会「类」而「或者」于(「等于」于「类」于「一」)于(「等于」于「类」于「四」))
于(「签」中「零」))则
「签」
否则
(「罄」授以「整数」)与「零」
)
或有「其他」则(「罄」授以「整数」)与「零」
)
或有「其他」则(「罄」授以「整数」)与「零」
而
虑「实参」者鉴「术」而
有「正则调用」则(鉴「参」而
有(「缀」于「头」于「余」)则「余」
或有「罄」则「罄」)
或有「其他」则
「参」
而
若「且」
于(「大于」于(「约」中「一」)于「零」)
于(「栈诸值合签」于「表」于「实参」于(「约」中「零」))则
「记」于「号」于(「约」中「一」)
否则
「拒」于「元」
)
或有(「正则如果」于「号」于「类」于「条件」于「阳体」于「阴体」)则(
虑「真类」者「扫」于「阳体」
而
虑「假类」者「扫」于「阴体」
而
若「且」
于(「等于」于(「栈值表示」于「表」于「条件」)于「二」)
于(「且」
于(「大于」于「真类」于「零」)
于(「且」于(「非」于(「等于」于「真类」于「四」))于(「等于」于「真类」于「假类」)))则
「记」于「号」于「真类」
否则
「拒」于「元」
)
或有「其他」则「拒」于「元」)
而
鉴「终」而
有(「正则产出」于「值」)则
「栈值表示」于「表」于「值」
或有「其他」则(虑「无」者「拒」于「元」而「零」)
)
而
虑「果」者「扫」于(「函」中「三」)
而
若「且」于(「读引用」于「好」)于(「等于」于「果」于(「本签」中「一」))则
「可有」于「表」
否则
「可无」
也。