豫言源码浏览器 / Source Browser

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

寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则数据」之书。

「：文言：入参之约既定，诸返皆整，递参守约，乃许私门裸返。汉语：对已验证局部编号与作用域的统一正则函数，在给定整数参数前提下，证明所有正常返回都是整数；递归调用用归纳假设，但每次递归必须保持这些参数前提。未知结果、混合返回和复杂退出保守拒绝。算术只有在原位置成功执行后才产生整数事实；证明不允许改变公开入口或提前检查参数。：」
「验整数返回」乃化「正则函数」而化（「列」于「整数」）而「爻」也。
「验整数返回」者会「函」而会「整数参」而
  虑「参数」者「函」中「二」而
  虑「含」者
    （化「整数」而化（「列」于「整数」）而「爻」也会「号」而会「列值」而「存在吗」授以「整数」
      于（会「前」而「等于」于「前」于「号」）于「列值」
    ）而
  若「非」于（「全部符合」授以「整数」于（会「号」而「含」于「号」于「参数」）于「整数参」）则
    「阴」
  否则
    虑「表」者「新数组引用」授以「爻」于「阴」于（「函」中「四」）
    而
    虑「可」者「新引用」授以「爻」于「阳」而
    虑「无」者
      「态射」授以「整数」授以「有」
      于「整数参」
      于（会「号」而「写数组引用」授以「爻」于「表」于「号」于「阳」）
    而
    虑「已整」者
      （化「正则原子」而「爻」也会「值」而鉴「值」而
          有（「正则整数」于「常」）则「阳」
          或有（「正则爻」于「真」）则「阳」
          或有（「正则局部」于「号」）则
            「读数组引用」授以「爻」于「表」于「号」
          或有「其他」则「阴」
      ）而
    递归虑「守参」其化（「列」于「整数」）而化（「列」于「正则原子」）而「爻」者会「诸号」而
      会「诸参」而
        鉴「诸号」而
          有「罄」则（鉴「诸参」而
          有「罄」则「阳」
          或有「其他」则「阴」）
          或有（「缀」于「号」于「余号」）则（
            鉴「诸参」而
              有（「缀」于「值」于「余参」）则
                若「含」于「号」于「整数参」则
                  若「已整」于「值」则
                    「守参」于「余号」于「余参」
                  否则
                    「阴」
                否则
                  「守参」于「余号」于「余参」
              或有「罄」则「阴」
          ）
    而
    递归虑「扫段」其化「正则区域」而「爻」者会「段」而
      鉴「段」而
        有（「正则段」于「诸令」于「终」）则
          虑「无」者
            「态射」授以「正则指令」授以「有」
            于「诸令」
            于（会「令」而鉴「令」而
              有（「正则运算」于「号」于「类」于「术」于「参」）则（
                虑「整」者鉴「术」而
                  有（「正则原语」于「名」）则（
                    鉴「名」而
                      有『豫言_整数加』则「阳」
                      或有『豫言_整数减』则「阳」
                      或有『豫言_整数乘』则「阳」
                      或有『豫言_整数除』则「阳」
                      或有『豫言_整数相等』则「阳」
                      或有『豫言_整数大于』则「阳」
                      或有「其他」则「阴」
                  ）
                  或有「正则调用」则（
                    鉴「参」而
                      有（「缀」于（「正则函数引用」于「名」）于「余」）则
                        若「串相等」于「名」于（「函」中「零」）则
                          若「守参」于「参数」于「余」则
                            「阳」
                          否则
                            （「写引用」于「可」于「阴」；
                              「阴」）
                        否则
                          「阴」
                      或有「其他」则「阴」
                  ）
                  或有「其他」则
                    「阴」
                而
                「写数组引用」授以「爻」于「表」于「号」于「整」
              ）
              或有（「正则如果」于「号」于「类」于「条件」于「阳体」于「阴体」）则（
                虑「阳整」者「扫段」于「阳体」
                而
                虑「阴整」者「扫段」于「阴体」而
                「写数组引用」授以「爻」
                于「表」于「号」
                于（「且」于「阳整」于「阴整」）
              ）
              或有「其他」则
                「写引用」于「可」于「阴」）
          而
          鉴「终」而
            有（「正则产出」于「值」）则「已整」于「值」
            或有「其他」则
              （「写引用」于「可」于「阴」；
                「阴」）
    而
    虑「果」者「扫段」于（「函」中「三」）而
    「且」于「果」于（「读引用」于「可」）
也。