Skip to content

Commit

Permalink
update docs -- zh -- for renaming from return to result
Browse files Browse the repository at this point in the history
  • Loading branch information
@xieyuheng
xieyuheng committed Sep 18, 2023
1 parent 9f8398d commit f859a12
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 48 deletions.
2 changes: 1 addition & 1 deletion TODO.md
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
update docs -- for renaming from `return` to `result`
update docs -- en -- for renaming from `return` to `result`
94 changes: 47 additions & 47 deletions docs/articles/反应网编程.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ year: 2023
(add)-target // 被加数
(add)-addend // 加数
(add)-return // 得数
(add)-result // 得数
```

接口分为两类，一类是输入接口，一类是输出接口。
Expand All @@ -176,7 +176,7 @@ year: 2023
(add)-target // 输入接口
(add)-addend // 输入接口
-------------
(add)-return // 输出接口
(add)-result // 输出接口
```

节点和节点之间可以通过接口相连，并且输入接口只能与输出接口相连。
Expand Down Expand Up @@ -210,7 +210,7 @@ year: 2023
(add)-target! // 主接口
(add)-addend
-------------
(add)-return
(add)-result
```

另外我们要求每个接口都有固定的类型，
Expand Down Expand Up @@ -245,7 +245,7 @@ node add
Nat :target!
Nat :prev
--------
Nat :return
Nat :result
end
```

Expand Down Expand Up @@ -289,7 +289,7 @@ type List @Type -- @Type end
`(add1)` 和 `(add)` 之间的反应规则：

```
return value
result value
| |
(add) => (add1)
/ \ |
Expand Down Expand Up @@ -325,7 +325,7 @@ prev target addend
rule add1 add
(add)-addend
(add1)-prev add
add1 return-(add)
add1 result-(add)
end
```

Expand Down Expand Up @@ -358,18 +358,18 @@ add
(add1)-prev target-(add₂)
(add)-addend addend-(add₂)
栈：[ (add₂)-return ]
栈：[ (add₂)-result ]
add1
新节点：(add1₂)
新连接：
(add₂)-return prev-(add1₂)
(add₂)-result prev-(add1₂)
栈：[ (add1₂)-value ]
return-(add)
result-(add)
栈：[ ]
```
Expand All @@ -381,7 +381,7 @@ return-(add)
```
rule zero add
(add)-addend
return-(add)
result-(add)
end
```

Expand All @@ -394,7 +394,7 @@ end

我们还有一个线上的演算场，可以用来方便地分享代码。

[去 `Nat` 与 `(add)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gQFR5cGUgZW5kCgpub2RlIHplcm8KICAtLS0tLS0tLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgYWRkMQogIE5hdCA6cHJldgogIC0tLS0tLS0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKbm9kZSBhZGQKICBOYXQgOnRhcmdldCEKICBOYXQgOmFkZGVuZAogIC0tLS0tLS0tLS0tLQogIE5hdCA6cmV0dXJuCmVuZAoKcnVsZSB6ZXJvIGFkZAogIChhZGQpLWFkZGVuZAogIHJldHVybi0oYWRkKQplbmQKCnJ1bGUgYWRkMSBhZGQKICAoYWRkKS1hZGRlbmQKICAoYWRkMSktcHJldiBhZGQKICBhZGQxIHJldHVybi0oYWRkKQplbmQKCmNsYWltIG9uZSAtLSBOYXQgZW5kCgpkZWZpbmUgb25lCiAgemVybyBhZGQxCmVuZAoKY2xhaW0gdHdvIC0tIE5hdCBlbmQKCmRlZmluZSB0d28KICBvbmUgYWRkMQplbmQKCmNsYWltIGFkZDIgTmF0IC0tIE5hdCBlbmQKCmRlZmluZSBhZGQyCiAgdHdvIGFkZAplbmQKCm9uZSBhZGQyCm9uZSBhZGQyCmFkZA)
[去 `Nat` 与 `(add)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gQFR5cGUgZW5kCgpub2RlIHplcm8KICAtLS0tLS0tLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgYWRkMQogIE5hdCA6cHJldgogIC0tLS0tLS0tLS0tLQogIE5hdCA6dmFsdWUhCmVuZAoKbm9kZSBhZGQKICBOYXQgOnRhcmdldCEKICBOYXQgOmFkZGVuZAogIC0tLS0tLS0tLS0tLQogIE5hdCA6cmVzdWx0CmVuZAoKcnVsZSB6ZXJvIGFkZAogIChhZGQpLWFkZGVuZAogIHJlc3VsdC0oYWRkKQplbmQKCnJ1bGUgYWRkMSBhZGQKICAoYWRkKS1hZGRlbmQKICAoYWRkMSktcHJldiBhZGQKICBhZGQxIHJlc3VsdC0oYWRkKQplbmQKCmNsYWltIG9uZSAtLSBOYXQgZW5kCgpkZWZpbmUgb25lCiAgemVybyBhZGQxCmVuZAoKY2xhaW0gdHdvIC0tIE5hdCBlbmQKCmRlZmluZSB0d28KICBvbmUgYWRkMQplbmQKCmNsYWltIGFkZDIgTmF0IC0tIE5hdCBlbmQKCmRlZmluZSBhZGQyCiAgdHdvIGFkZAplbmQKCm9uZSBhZGQyCm9uZSBhZGQyCmFkZA)

```
type Nat -- @Type end
Expand All @@ -414,18 +414,18 @@ node add
Nat :target!
Nat :addend
------------
Nat :return
Nat :result
end
rule zero add
(add)-addend
return-(add)
result-(add)
end
rule add1 add
(add)-addend
(add1)-prev add
add1 return-(add)
add1 result-(add)
end
claim one -- Nat end
Expand Down Expand Up @@ -513,7 +513,7 @@ add
我们称代表这个函数的节点为 `(max)`。

```
return
result
|
(max)
/ \
Expand All @@ -527,14 +527,14 @@ node max
Nat :first!
Nat :second
----------
Nat :return
Nat :result
end
```

`(zero)` 与 `(zero)` 的反应很简单：

```
return return
result result
| |
(max) => |
/ \ \
Expand All @@ -545,7 +545,7 @@ end

```
rule zero max
(max)-second return-(max)
(max)-second result-(max)
end
```

Expand All @@ -554,7 +554,7 @@ end
我们完全可以想象下面的反应规则：

```
return return
result result
| |
(max) => (add1)
/ \ |
Expand All @@ -571,7 +571,7 @@ end
其中 `aux` 是 auxiliary 的所写。

```
return
result
|
(maxAux)
/ \
Expand All @@ -585,14 +585,14 @@ node maxAux
Nat :first
Nat :second!
--------
Nat :return
Nat :result
end
```

利用辅助节点定义 `(add1)` 和 `(max)` 之间的规则：

```
return return
result result
| |
(max) => (maxAux)
/ \ / \
Expand All @@ -607,14 +607,14 @@ end
rule add1 max
(max)-second
(add1)-prev maxAux
return-(max)
result-(max)
end
```

`(zero)` 与 `(maxAux)` 之间的规则：

```
return return
result result
| |
(maxAux) => (add1)
/ \ |
Expand All @@ -626,14 +626,14 @@ end
```
rule zero maxAux
(maxAux)-first add1
return-(maxAux)
result-(maxAux)
end
```

`(add1)` 与 `(maxAux)` 之间的规则：

```
return return
result result
| |
(maxAux) => (add1)
/ \ |
Expand All @@ -648,11 +648,11 @@ end
rule add1 maxAux
(add1)-prev
(maxAux)-first max
add1 return-(maxAux)
add1 result-(maxAux)
end
```

[去 `Nat` 与 `(max)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gQFR5cGUgZW5kCgpub2RlIHplcm8KICAtLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgYWRkMQogIE5hdCA6cHJldgogIC0tLS0tLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgbWF4QXV4CiAgTmF0IDpmaXJzdAogIE5hdCA6c2Vjb25kIQogIC0tLS0tLS0tCiAgTmF0IDpyZXR1cm4KZW5kCgpub2RlIG1heAogIE5hdCA6Zmlyc3QhCiAgTmF0IDpzZWNvbmQKICAtLS0tLS0tLS0tCiAgTmF0IDpyZXR1cm4KZW5kCgpydWxlIHplcm8gbWF4CiAgKG1heCktc2Vjb25kIHJldHVybi0obWF4KQplbmQKCnJ1bGUgYWRkMSBtYXgKICAobWF4KS1zZWNvbmQgKGFkZDEpLXByZXYgbWF4QXV4CiAgcmV0dXJuLShtYXgpCmVuZAoKcnVsZSB6ZXJvIG1heEF1eAogIChtYXhBdXgpLWZpcnN0IGFkZDEKICByZXR1cm4tKG1heEF1eCkKZW5kCgpydWxlIGFkZDEgbWF4QXV4CiAgKGFkZDEpLXByZXYgKG1heEF1eCktZmlyc3QgbWF4CiAgYWRkMSByZXR1cm4tKG1heEF1eCkKZW5kCgpjbGFpbSBvbmUgLS0gTmF0IGVuZApkZWZpbmUgb25lIHplcm8gYWRkMSBlbmQKCmNsYWltIHR3byAtLSBOYXQgZW5kCmRlZmluZSB0d28gb25lIGFkZDEgZW5kCgpjbGFpbSB0aHJlZSAtLSBOYXQgZW5kCmRlZmluZSB0aHJlZSB0d28gYWRkMSBlbmQKCmNsYWltIGZvdXIgLS0gTmF0IGVuZApkZWZpbmUgZm91ciB0aHJlZSBhZGQxIGVuZAoKemVybyB0d28gbWF4Cgp0aHJlZSB0d28gbWF4)
[去 `Nat` 与 `(max)` 的演算场](https://inet.run/playground/dHlwZSBOYXQgLS0gQFR5cGUgZW5kCgpub2RlIHplcm8KICAtLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgYWRkMQogIE5hdCA6cHJldgogIC0tLS0tLS0tLS0KICBOYXQgOnZhbHVlIQplbmQKCm5vZGUgbWF4QXV4CiAgTmF0IDpmaXJzdAogIE5hdCA6c2Vjb25kIQogIC0tLS0tLS0tCiAgTmF0IDpyZXN1bHQKZW5kCgpub2RlIG1heAogIE5hdCA6Zmlyc3QhCiAgTmF0IDpzZWNvbmQKICAtLS0tLS0tLS0tCiAgTmF0IDpyZXN1bHQKZW5kCgpydWxlIHplcm8gbWF4CiAgKG1heCktc2Vjb25kIHJlc3VsdC0obWF4KQplbmQKCnJ1bGUgYWRkMSBtYXgKICAobWF4KS1zZWNvbmQgKGFkZDEpLXByZXYgbWF4QXV4CiAgcmVzdWx0LShtYXgpCmVuZAoKcnVsZSB6ZXJvIG1heEF1eAogIChtYXhBdXgpLWZpcnN0IGFkZDEKICByZXN1bHQtKG1heEF1eCkKZW5kCgpydWxlIGFkZDEgbWF4QXV4CiAgKGFkZDEpLXByZXYgKG1heEF1eCktZmlyc3QgbWF4CiAgYWRkMSByZXN1bHQtKG1heEF1eCkKZW5kCgpjbGFpbSBvbmUgLS0gTmF0IGVuZApkZWZpbmUgb25lIHplcm8gYWRkMSBlbmQKCmNsYWltIHR3byAtLSBOYXQgZW5kCmRlZmluZSB0d28gb25lIGFkZDEgZW5kCgpjbGFpbSB0aHJlZSAtLSBOYXQgZW5kCmRlZmluZSB0aHJlZSB0d28gYWRkMSBlbmQKCmNsYWltIGZvdXIgLS0gTmF0IGVuZApkZWZpbmUgZm91ciB0aHJlZSBhZGQxIGVuZAoKemVybyB0d28gbWF4Cgp0aHJlZSB0d28gbWF4)

```
type Nat -- @Type end
Expand All @@ -672,33 +672,33 @@ node maxAux
Nat :first
Nat :second!
--------
Nat :return
Nat :result
end
node max
Nat :first!
Nat :second
----------
Nat :return
Nat :result
end
rule zero max
(max)-second return-(max)
(max)-second result-(max)
end
rule add1 max
(max)-second (add1)-prev maxAux
return-(max)
result-(max)
end
rule zero maxAux
(maxAux)-first add1
return-(maxAux)
result-(maxAux)
end
rule add1 maxAux
(add1)-prev (maxAux)-first max
add1 return-(maxAux)
add1 result-(maxAux)
end
claim one -- Nat end
Expand Down Expand Up @@ -763,7 +763,7 @@ three two max
- 用 `$local` 保存一个值之后，可以通过调用 `local` 来取出这个值。
- 取出之后，`$local` 就空了，就又可以用于保存新的值了。

[去 `Nat` 与 `(mul)` 的演算场](https://inet.run/playground/aW1wb3J0CiAgTmF0LCB6ZXJvLCBhZGQxLCBhZGQsCiAgb25lLCB0d28sIHRocmVlLApmcm9tICJodHRwczovL2NvZGUtb2YtaW5ldC5maWRiLmFwcC90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKCm5vZGUgbmF0RXJhc2UKICBOYXQgOnRhcmdldCEKICAtLS0tLS0tLQplbmQKCnJ1bGUgemVybyBuYXRFcmFzZSBlbmQKCnJ1bGUgYWRkMSBuYXRFcmFzZQogIChhZGQxKS1wcmV2IG5hdEVyYXNlCmVuZAoKbm9kZSBuYXREdXAKICBOYXQgOnRhcmdldCEKICAtLS0tLS0tLQogIE5hdCA6c2Vjb25kCiAgTmF0IDpmaXJzdAplbmQKCnJ1bGUgemVybyBuYXREdXAKICB6ZXJvIGZpcnN0LShuYXREdXApCiAgemVybyBzZWNvbmQtKG5hdER1cCkKZW5kCgpydWxlIGFkZDEgbmF0RHVwCiAgKGFkZDEpLXByZXYgbmF0RHVwICRmaXJzdCAkc2Vjb25kCiAgZmlyc3QgYWRkMSBmaXJzdC0obmF0RHVwKQogIHNlY29uZCBhZGQxIHNlY29uZC0obmF0RHVwKQplbmQKCm5vZGUgbXVsCiAgTmF0IDp0YXJnZXQhCiAgTmF0IDptdWxlbmQKICAtLS0tLS0tLQogIE5hdCA6cmV0dXJuCmVuZAoKcnVsZSB6ZXJvIG11bAogIChtdWwpLW11bGVuZCBuYXRFcmFzZQogIHplcm8gcmV0dXJuLShtdWwpCmVuZAoKcnVsZSBhZGQxIG11bAogIChtdWwpLW11bGVuZCBuYXREdXAgJGZpcnN0ICRzZWNvbmQKICAoYWRkMSktcHJldiBmaXJzdCBtdWwgc2Vjb25kIGFkZAogIHJldHVybi0obXVsKQplbmQKCnR3byBuYXREdXAgJGZpcnN0ICRzZWNvbmQKCnR3byB0d28gbXVsCgp0aHJlZSB0aHJlZSBtdWw)
[去 `Nat` 与 `(mul)` 的演算场](https://inet.run/playground/aW1wb3J0CiAgTmF0LCB6ZXJvLCBhZGQxLCBhZGQsCiAgb25lLCB0d28sIHRocmVlLApmcm9tICJodHRwczovL2NvZGUtb2YtaW5ldC5maWRiLmFwcC90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKCm5vZGUgbmF0RXJhc2UKICBOYXQgOnRhcmdldCEKICAtLS0tLS0tLQplbmQKCnJ1bGUgemVybyBuYXRFcmFzZSBlbmQKCnJ1bGUgYWRkMSBuYXRFcmFzZQogIChhZGQxKS1wcmV2IG5hdEVyYXNlCmVuZAoKbm9kZSBuYXREdXAKICBOYXQgOnRhcmdldCEKICAtLS0tLS0tLQogIE5hdCA6c2Vjb25kCiAgTmF0IDpmaXJzdAplbmQKCnJ1bGUgemVybyBuYXREdXAKICB6ZXJvIGZpcnN0LShuYXREdXApCiAgemVybyBzZWNvbmQtKG5hdER1cCkKZW5kCgpydWxlIGFkZDEgbmF0RHVwCiAgKGFkZDEpLXByZXYgbmF0RHVwICRmaXJzdCAkc2Vjb25kCiAgZmlyc3QgYWRkMSBmaXJzdC0obmF0RHVwKQogIHNlY29uZCBhZGQxIHNlY29uZC0obmF0RHVwKQplbmQKCm5vZGUgbXVsCiAgTmF0IDp0YXJnZXQhCiAgTmF0IDptdWxlbmQKICAtLS0tLS0tLQogIE5hdCA6cmVzdWx0CmVuZAoKcnVsZSB6ZXJvIG11bAogIChtdWwpLW11bGVuZCBuYXRFcmFzZQogIHplcm8gcmVzdWx0LShtdWwpCmVuZAoKcnVsZSBhZGQxIG11bAogIChtdWwpLW11bGVuZCBuYXREdXAgJGZpcnN0ICRzZWNvbmQKICAoYWRkMSktcHJldiBmaXJzdCBtdWwgc2Vjb25kIGFkZAogIHJlc3VsdC0obXVsKQplbmQKCnR3byBuYXREdXAgJGZpcnN0ICRzZWNvbmQKCnR3byB0d28gbXVsCgp0aHJlZSB0aHJlZSBtdWw)

```
import
Expand Down Expand Up @@ -804,18 +804,18 @@ node mul
Nat :target!
Nat :mulend
--------
Nat :return
Nat :result
end
rule zero mul
(mul)-mulend natErase
zero return-(mul)
zero result-(mul)
end
rule add1 mul
(mul)-mulend natDup $first $second
(add1)-prev first mul second add
return-(mul)
result-(mul)
end
two natDup $first $second
Expand Down Expand Up @@ -848,7 +848,7 @@ three three mul
在定义 `(cons)` 和 `(append)` 时，代表类型变元的相同的符号 `'A`，出现了多次。
这意味着在连接这些节点的接口时，这个类型变元必须匹配到相同的类型。

[去 `List` 与 `(append)` 的演算场](https://inet.run/playground/dHlwZSBMaXN0IEBUeXBlIC0tIEBUeXBlIGVuZAoKbm9kZSBudWxsCiAgLS0tLS0tLS0KICAnQSBMaXN0IDp2YWx1ZSEKZW5kCgpub2RlIGNvbnMKICAnQSA6aGVhZAogICdBIExpc3QgOnRhaWwKICAtLS0tLS0tLQogICdBIExpc3QgOnZhbHVlIQplbmQKCm5vZGUgYXBwZW5kCiAgJ0EgTGlzdCA6dGFyZ2V0IQogICdBIExpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIExpc3QgOnJldHVybgplbmQKCnJ1bGUgbnVsbCBhcHBlbmQKICAoYXBwZW5kKS1yZXN0CiAgcmV0dXJuLShhcHBlbmQpCmVuZAoKcnVsZSBjb25zIGFwcGVuZAogIChhcHBlbmQpLXJlc3QgKGNvbnMpLXRhaWwgYXBwZW5kCiAgKGNvbnMpLWhlYWQgY29ucwogIHJldHVybi0oYXBwZW5kKQplbmQKCmltcG9ydCB6ZXJvIGZyb20gImh0dHBzOi8vY2RuLmluZXQucnVuL3Rlc3RzL2RhdGF0eXBlL05hdC5pIgoKbnVsbCB6ZXJvIGNvbnMgemVybyBjb25zCm51bGwgemVybyBjb25zIHplcm8gY29ucwphcHBlbmQKCm51bGwgemVybyBjb25zIHplcm8gY29ucwpudWxsIHplcm8gY29ucyB6ZXJvIGNvbnMKYXBwZW5kIEBydW4gJHJlc3VsdA)
[去 `List` 与 `(append)` 的演算场](https://inet.run/playground/dHlwZSBMaXN0IEBUeXBlIC0tIEBUeXBlIGVuZAoKbm9kZSBudWxsCiAgLS0tLS0tLS0KICAnQSBMaXN0IDp2YWx1ZSEKZW5kCgpub2RlIGNvbnMKICAnQSA6aGVhZAogICdBIExpc3QgOnRhaWwKICAtLS0tLS0tLQogICdBIExpc3QgOnZhbHVlIQplbmQKCm5vZGUgYXBwZW5kCiAgJ0EgTGlzdCA6dGFyZ2V0IQogICdBIExpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIExpc3QgOnJlc3VsdAplbmQKCnJ1bGUgbnVsbCBhcHBlbmQKICAoYXBwZW5kKS1yZXN0CiAgcmVzdWx0LShhcHBlbmQpCmVuZAoKcnVsZSBjb25zIGFwcGVuZAogIChhcHBlbmQpLXJlc3QgKGNvbnMpLXRhaWwgYXBwZW5kCiAgKGNvbnMpLWhlYWQgY29ucwogIHJlc3VsdC0oYXBwZW5kKQplbmQKCmltcG9ydCB6ZXJvIGZyb20gImh0dHBzOi8vY29kZS1vZi1pbmV0LmZpZGIuYXBwL3Rlc3RzL2RhdGF0eXBlL05hdC5pIgoKbnVsbCB6ZXJvIGNvbnMgemVybyBjb25zCm51bGwgemVybyBjb25zIHplcm8gY29ucwphcHBlbmQKCm51bGwgemVybyBjb25zIHplcm8gY29ucwpudWxsIHplcm8gY29ucyB6ZXJvIGNvbnMKYXBwZW5kIEBydW4gJHJlc3VsdA)

```
type List @Type -- @Type end
Expand All @@ -869,18 +869,18 @@ node append
'A List :target!
'A List :rest
--------
'A List :return
'A List :result
end
rule null append
(append)-rest
return-(append)
result-(append)
end
rule cons append
(append)-rest (cons)-tail append
(cons)-head cons
return-(append)
result-(append)
end
import zero from "https://code-of-inet.fidb.app/tests/datatype/Nat.i"
Expand Down Expand Up @@ -921,7 +921,7 @@ append @run $result
后面跟着的 `@spread` 可以将其所有接口按定义中相反的顺序返回到栈中，
然后我们把这些接口保存到了一些局部变量中。

[去 `DiffList` 与 `(diffAppend)` 的演算场](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jb2RlLW9mLWluZXQuZmlkYi5hcHAvdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmQXBwZW5kCiAgJ0EgRGlmZkxpc3QgOnRhcmdldCEKICAnQSBEaWZmTGlzdCA6cmVzdAogIC0tLS0tLS0tCiAgJ0EgRGlmZkxpc3QgOnJldHVybgplbmQKCm5vZGUgZGlmZk9wZW4KICAnQSBEaWZmTGlzdCA6dGFyZ2V0IQogICdBIExpc3QgOmxpc3QKICAtLS0tLS0tLS0tCiAgJ0EgTGlzdCA6cmV0dXJuCmVuZAoKcnVsZSBkaWZmIGRpZmZBcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZBcHBlbmQpCiAgKGRpZmZBcHBlbmQpLXJlc3QgZGlmZk9wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZk9wZW4KICAoZGlmZiktYmFjayBsaXN0LShkaWZmT3BlbikKICAoZGlmZiktZnJvbnQgcmV0dXJuLShkaWZmT3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2NvZGUtb2YtaW5ldC5maWRiLmFwcC90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jb2RlLW9mLWluZXQuZmlkYi5hcHAvdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKZGlmZkFwcGVuZAoKLy8g5LiK6Z2i55qE5Luj56CB5Y-v5Lul5bCR55So5LiA5Liq5bGA6YOo5Y-Y6YePIGAkdmFsdWVgIO-8jOiAjOeugOWMluWmguS4i--8mgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgJGJhY2sKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZBcHBlbmQKCi8vIOWGjeWwkeeUqOS4gOS4quWxgOmDqOWPmOmHjyBgJGJhY2tg77yM6L-b5LiA5q2l566A5YyW77yaCgooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmQXBwZW5kCgpAcnVuICRyZXN1bHQ)
[去 `DiffList` 与 `(diffAppend)` 的演算场](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jb2RlLW9mLWluZXQuZmlkYi5hcHAvdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmQXBwZW5kCiAgJ0EgRGlmZkxpc3QgOnRhcmdldCEKICAnQSBEaWZmTGlzdCA6cmVzdAogIC0tLS0tLS0tCiAgJ0EgRGlmZkxpc3QgOnJlc3VsdAplbmQKCm5vZGUgZGlmZk9wZW4KICAnQSBEaWZmTGlzdCA6dGFyZ2V0IQogICdBIExpc3QgOmxpc3QKICAtLS0tLS0tLS0tCiAgJ0EgTGlzdCA6cmVzdWx0CmVuZAoKcnVsZSBkaWZmIGRpZmZBcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXN1bHQtKGRpZmZBcHBlbmQpCiAgKGRpZmZBcHBlbmQpLXJlc3QgZGlmZk9wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZk9wZW4KICAoZGlmZiktYmFjayBsaXN0LShkaWZmT3BlbikKICAoZGlmZiktZnJvbnQgcmVzdWx0LShkaWZmT3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2NvZGUtb2YtaW5ldC5maWRiLmFwcC90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jb2RlLW9mLWluZXQuZmlkYi5hcHAvdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKZGlmZkFwcGVuZAoKLy8g5LiK6Z2i55qE5Luj56CB5Y-v5Lul5bCR55So5LiA5Liq5bGA6YOo5Y-Y6YePIGAkdmFsdWVgIO-8jOiAjOeugOWMluWmguS4i--8mgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgJGJhY2sKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZBcHBlbmQKCi8vIOWGjeWwkeeUqOS4gOS4quWxgOmDqOWPmOmHjyBgJGJhY2tg77yM6L-b5LiA5q2l566A5YyW77yaCgooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmQXBwZW5kCgpAcnVuICRyZXN1bHQ)

```
import List from "https://code-of-inet.fidb.app/tests/datatype/List.i"
Expand All @@ -939,24 +939,24 @@ node diffAppend
'A DiffList :target!
'A DiffList :rest
--------
'A DiffList :return
'A DiffList :result
end
node diffOpen
'A DiffList :target!
'A List :list
----------
'A List :return
'A List :result
end
rule diff diffAppend
(diff)-front diff return-(diffAppend)
(diff)-front diff result-(diffAppend)
(diffAppend)-rest diffOpen back-(diff)
end
rule diff diffOpen
(diff)-back list-(diffOpen)
(diff)-front return-(diffOpen)
(diff)-front result-(diffOpen)
end
import zero from "https://code-of-inet.fidb.app/tests/datatype/Nat.i"
Expand Down

0 comments on commit f859a12

Please sign in to comment.