From 0e5fe45132b67b8f5a585e8a3c5e07a715ebf651 Mon Sep 17 00:00:00 2001 From: Xie Yuheng Date: Wed, 13 Sep 2023 11:05:14 +0800 Subject: [PATCH] update article -- for `@spread` --- README.md | 15 ++++-- TODO.md | 2 - .../programming-with-interaction-nets.md | 50 ++++++++++--------- ...24\347\275\221\347\274\226\347\250\213.md" | 45 +++++++++-------- 4 files changed, 62 insertions(+), 50 deletions(-) diff --git a/README.md b/README.md index a9f3dce3..09fc6533 100644 --- a/README.md +++ b/README.md @@ -133,7 +133,7 @@ append @run $result #### DiffList -[ [Goto The Playground](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKLy8gQ29uY2F0ZW5hdGlvbiBvZiBsaXN0cyBpcyBwZXJmb3JtZWQgaW4gbGluZWFyIHRpbWUKLy8gd2l0aCByZXNwZWN0IHRvIGl0cyBmaXJzdCBhcmd1bWVudC4KLy8gQ29uc3RhbnQgdGltZSBjb25jYXRlbmF0aW9uIGlzIHBvc3NpYmxlCi8vIHdpdGggZGlmZmVyZW5jZS1saXN0czogdGhlIGlkZWEgY29uc2lzdHMgaW4KLy8gcGx1Z2dpbmcgdGhlIGZyb250IG9mIHRoZSBzZWNvbmQgYXJndW1lbnQKLy8gYXQgdGhlIGJhY2sgb2YgdGhlIGZpcnN0IG9uZS4KCnR5cGUgRGlmZkxpc3QgQFR5cGUgLS0gQFR5cGUgZW5kCgpub2RlIGRpZmYKICAnQSBMaXN0IDpmcm9udAogIC0tLS0tLS0KICAnQSBMaXN0IDpiYWNrCiAgJ0EgRGlmZkxpc3QgOnZhbHVlIQplbmQKCm5vZGUgZGlmZl9hcHBlbmQKICAnQSBEaWZmTGlzdCA6dGFyZ2V0IQogICdBIERpZmZMaXN0IDpyZXN0CiAgLS0tLS0tLS0KICAnQSBEaWZmTGlzdCA6cmV0dXJuCmVuZAoKbm9kZSBkaWZmX29wZW4KICAnQSBEaWZmTGlzdCA6dGFyZ2V0IQogICdBIExpc3QgOmxpc3QKICAtLS0tLS0tLS0tCiAgJ0EgTGlzdCA6cmV0dXJuCmVuZAoKcnVsZSBkaWZmIGRpZmZfYXBwZW5kCiAgKGRpZmYpLWZyb250IGRpZmYgcmV0dXJuLShkaWZmX2FwcGVuZCkKICAoZGlmZl9hcHBlbmQpLXJlc3QgZGlmZl9vcGVuIGJhY2stKGRpZmYpCmVuZAoKcnVsZSBkaWZmIGRpZmZfb3BlbgogIChkaWZmKS1iYWNrIGxpc3QtKGRpZmZfb3BlbikKICAoZGlmZiktZnJvbnQgcmV0dXJuLShkaWZmX29wZW4pCmVuZAoKaW1wb3J0IHplcm8gZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTmF0LmkiCmltcG9ydCBjb25zIGZyb20gImh0dHBzOi8vY2RuLmluZXQucnVuL3Rlc3RzL2RhdGF0eXBlL0xpc3QuaSIKCihkaWZmKSBAc3ByZWFkICRmcm9udCAkYmFjayAkdmFsdWUKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0IHZhbHVlCihkaWZmKSBAc3ByZWFkICRmcm9udCAkYmFjayAkdmFsdWUKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0IHZhbHVlCmRpZmZfYXBwZW5kCgovLyBUaGUgY29kZSBhYm92ZSBjYW4gYmUgc2ltcGxpZmllZAovLyBieSB1c2luZyBsZXNzIG5hbWVkIGxvY2FsIHZhcmlhYmxlcy4KCihkaWZmKSBAc3ByZWFkICRmcm9udCB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CihkaWZmKSBAc3ByZWFkICRmcm9udCB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZfYXBwZW5kCgpAcnVuICRyZXN1bHQ) ] +[ [Goto The Playground](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKLy8gQ29uY2F0ZW5hdGlvbiBvZiBsaXN0cyBpcyBwZXJmb3JtZWQgaW4gbGluZWFyIHRpbWUKLy8gd2l0aCByZXNwZWN0IHRvIGl0cyBmaXJzdCBhcmd1bWVudC4KLy8gQ29uc3RhbnQgdGltZSBjb25jYXRlbmF0aW9uIGlzIHBvc3NpYmxlCi8vIHdpdGggZGlmZmVyZW5jZS1saXN0czogdGhlIGlkZWEgY29uc2lzdHMgaW4KLy8gcGx1Z2dpbmcgdGhlIGZyb250IG9mIHRoZSBzZWNvbmQgYXJndW1lbnQKLy8gYXQgdGhlIGJhY2sgb2YgdGhlIGZpcnN0IG9uZS4KCnR5cGUgRGlmZkxpc3QgQFR5cGUgLS0gQFR5cGUgZW5kCgpub2RlIGRpZmYKICAnQSBMaXN0IDpmcm9udAogIC0tLS0tLS0KICAnQSBMaXN0IDpiYWNrCiAgJ0EgRGlmZkxpc3QgOnZhbHVlIQplbmQKCm5vZGUgZGlmZl9hcHBlbmQKICAnQSBEaWZmTGlzdCA6dGFyZ2V0IQogICdBIERpZmZMaXN0IDpyZXN0CiAgLS0tLS0tLS0KICAnQSBEaWZmTGlzdCA6cmV0dXJuCmVuZAoKbm9kZSBkaWZmX29wZW4KICAnQSBEaWZmTGlzdCA6dGFyZ2V0IQogICdBIExpc3QgOmxpc3QKICAtLS0tLS0tLS0tCiAgJ0EgTGlzdCA6cmV0dXJuCmVuZAoKcnVsZSBkaWZmIGRpZmZfYXBwZW5kCiAgKGRpZmYpLWZyb250IGRpZmYgcmV0dXJuLShkaWZmX2FwcGVuZCkKICAoZGlmZl9hcHBlbmQpLXJlc3QgZGlmZl9vcGVuIGJhY2stKGRpZmYpCmVuZAoKcnVsZSBkaWZmIGRpZmZfb3BlbgogIChkaWZmKS1iYWNrIGxpc3QtKGRpZmZfb3BlbikKICAoZGlmZiktZnJvbnQgcmV0dXJuLShkaWZmX29wZW4pCmVuZAoKaW1wb3J0IHplcm8gZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTmF0LmkiCmltcG9ydCBjb25zIGZyb20gImh0dHBzOi8vY2RuLmluZXQucnVuL3Rlc3RzL2RhdGF0eXBlL0xpc3QuaSIKCihkaWZmKSBAc3ByZWFkICRmcm9udCAkYmFjayAkdmFsdWUKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0IHZhbHVlCihkaWZmKSBAc3ByZWFkICRmcm9udCAkYmFjayAkdmFsdWUKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0IHZhbHVlCmRpZmZfYXBwZW5kCgovLyBVc2Ugb25lIGxlc3MgbG9jYWwgdmFyaWFibGUgYCR2YWx1ZWAsCi8vIHdlIGNhbiBzaW1wbGlmeSB0aGUgYWJvdmUgY29kZToKCihkaWZmKSBAc3ByZWFkICRmcm9udCAkYmFjawpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmX2FwcGVuZAoKLy8gVXNlIG9uZSBsZXNzIGxvY2FsIHZhcmlhYmxlIGAkYmFja2AsCi8vIHdlIGNhbiBmdXJ0aGVyIHNpbXBsaWZ5IHRoZSBhYm92ZSBjb2RlOgoKKGRpZmYpIEBzcHJlYWQgJGZyb250IHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QKKGRpZmYpIEBzcHJlYWQgJGZyb250IHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QKZGlmZl9hcHBlbmQKCkBydW4gJHJlc3VsdA) ] ```inet import List from "https://cdn.inet.run/tests/datatype/List.i" @@ -187,8 +187,17 @@ back zero cons zero cons front @connect value back zero cons zero cons front @connect value diff_append -// The code above can be simplified -// by using less named local variables. +// By using one less local variable `$value`, +// we can simplify the above code: + +(diff) @spread $front $back +back zero cons zero cons front @connect +(diff) @spread $front $back +back zero cons zero cons front @connect +diff_append + +// By using one less local variable `$back`, +// we can further simplify the above code: (diff) @spread $front zero cons zero cons front @connect (diff) @spread $front zero cons zero cons front @connect diff --git a/TODO.md b/TODO.md index 6caccef2..180c4dda 100644 --- a/TODO.md +++ b/TODO.md @@ -1,5 +1,3 @@ -update article -- for `@spread` - [note] about spread vs rearrange `(cons)` -- unconnected node as value -- redesign syntax of rearrange diff --git a/docs/articles/programming-with-interaction-nets.md b/docs/articles/programming-with-interaction-nets.md index 116ae43f..ff19aa72 100644 --- a/docs/articles/programming-with-interaction-nets.md +++ b/docs/articles/programming-with-interaction-nets.md @@ -951,25 +951,13 @@ while the reverse is not true. But in interaction nets, the relationship between all nodes is symmetric. -In the following code, in one calling of `cons`, -we will write `(cons :tail)` instead of `cons`, -this means before calling this node, -we need to rearrange it's ports, -view the input port `:tail` as an output port, -not connect it to the ports in the stack -but return it directly to the stack. +In the following code, +we use `(diff)` to create a new node and return it to the stack, +follows `@spread` to put all it's ports to the stack +in reverse order of the definition, +then we save the ports to local variables for later use. -In the following code, we also used a phrase: - -``` -... $value @connect value ... -``` - -Which means firstly save the top value in the stack to `$value`, -then connect the top two ports in the stack, -finally return the value saved in `$value` back to the stack. - -[Goto the playground of `DiffList` and `(diff_append)`](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKemVybyAoY29ucyA6dGFpbCkgemVybyBjb25zIGRpZmYgJHZhbHVlIEBjb25uZWN0IHZhbHVlCnplcm8gKGNvbnMgOnRhaWwpIHplcm8gY29ucyBkaWZmICR2YWx1ZSBAY29ubmVjdCB2YWx1ZQpkaWZmX2FwcGVuZAoKemVybyAoY29ucyA6dGFpbCkgemVybyBjb25zIGRpZmYgJHZhbHVlIEBjb25uZWN0IHZhbHVlCnplcm8gKGNvbnMgOnRhaWwpIHplcm8gY29ucyBkaWZmICR2YWx1ZSBAY29ubmVjdCB2YWx1ZQpkaWZmX2FwcGVuZCBAcnVuICRyZXN1bHQ) +[Goto the playground of `DiffList` and `(diff_append)`](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKZGlmZl9hcHBlbmQKCi8vIFVzZSBvbmUgbGVzcyBsb2NhbCB2YXJpYWJsZSBgJHZhbHVlYCwKLy8gd2UgY2FuIHNpbXBsaWZ5IHRoZSBhYm92ZSBjb2RlOgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgJGJhY2sKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZfYXBwZW5kCgovLyBVc2Ugb25lIGxlc3MgbG9jYWwgdmFyaWFibGUgYCRiYWNrYCwKLy8gd2UgY2FuIGZ1cnRoZXIgc2ltcGxpZnkgdGhlIGFib3ZlIGNvZGU6CgooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmX2FwcGVuZAoKQHJ1biAkcmVzdWx0) ``` import List from "https://cdn.inet.run/tests/datatype/List.i" @@ -1010,13 +998,29 @@ end import zero from "https://cdn.inet.run/tests/datatype/Nat.i" import cons from "https://cdn.inet.run/tests/datatype/List.i" -zero (cons :tail) zero cons diff $value @connect value -zero (cons :tail) zero cons diff $value @connect value +(diff) @spread $front $back $value +back zero cons zero cons front @connect value +(diff) @spread $front $back $value +back zero cons zero cons front @connect value +diff_append + +// By using one less local variable `$value`, +// we can simplify the above code: + +(diff) @spread $front $back +back zero cons zero cons front @connect +(diff) @spread $front $back +back zero cons zero cons front @connect +diff_append + +// By using one less local variable `$back`, +// we can further simplify the above code: + +(diff) @spread $front zero cons zero cons front @connect +(diff) @spread $front zero cons zero cons front @connect diff_append -zero (cons :tail) zero cons diff $value @connect value -zero (cons :tail) zero cons diff $value @connect value -diff_append @run $result +@run $result ``` # 13 diff --git "a/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" "b/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" index bd5fc2cb..23aac42d 100644 --- "a/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" +++ "b/docs/articles/\345\217\215\345\272\224\347\275\221\347\274\226\347\250\213.md" @@ -917,24 +917,11 @@ append @run $result 从树的父节点可以找到子节点,但是反之不行。 而在反应网中,所有节点之间的关系是对称的。 -在下面的代码中,在一次调用 `cons` 时, -我们写成了 `(cons :tail)` 而不是直接写 `cons`, -这代表在调用这个节点之前,重新排列这个节点的接口, -将原本是输入接口的 `:tail` 看成是输出接口一样, -不是与栈中的接口相连,而是直接返回到栈中。 +在下面的代码中,我们用 `(diff)` 来构造一个新节点返回到栈中, +后面跟着的 `@spread` 可以将其所有接口按定义中相反的顺序返回到栈中, +然后我们把这些接口保存到了一些局部变量中。 -在下面的代码中我们还使用了一个短语: - -``` -... $value @connect value ... -``` - -它的意思是,先把栈顶的值保存在 `$value` 中, -然后将栈顶的两个接口相连, -最后再把保存在 `$value` 中的值放回栈中。 - - -[去 `DiffList` 与 `(diff_append)` 的演算场](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKemVybyAoY29ucyA6dGFpbCkgemVybyBjb25zIGRpZmYgJHZhbHVlIEBjb25uZWN0IHZhbHVlCnplcm8gKGNvbnMgOnRhaWwpIHplcm8gY29ucyBkaWZmICR2YWx1ZSBAY29ubmVjdCB2YWx1ZQpkaWZmX2FwcGVuZAoKemVybyAoY29ucyA6dGFpbCkgemVybyBjb25zIGRpZmYgJHZhbHVlIEBjb25uZWN0IHZhbHVlCnplcm8gKGNvbnMgOnRhaWwpIHplcm8gY29ucyBkaWZmICR2YWx1ZSBAY29ubmVjdCB2YWx1ZQpkaWZmX2FwcGVuZCBAcnVuICRyZXN1bHQ) +[去 `DiffList` 与 `(diff_append)` 的演算场](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKZGlmZl9hcHBlbmQKCi8vIOS4iumdoueahOS7o-eggeWPr-S7peWwkeeUqOS4gOS4quWxgOmDqOWPmOmHjyBgJHZhbHVlYCDvvIzogIznroDljJblpoLkuIvvvJoKCihkaWZmKSBAc3ByZWFkICRmcm9udCAkYmFjawpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmX2FwcGVuZAoKLy8g5YaN5bCR55So5LiA5Liq5bGA6YOo5Y-Y6YePIGAkYmFja2DvvIzov5vkuIDmraXnroDljJbvvJoKCihkaWZmKSBAc3ByZWFkICRmcm9udCB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CihkaWZmKSBAc3ByZWFkICRmcm9udCB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZfYXBwZW5kCgpAcnVuICRyZXN1bHQ) ``` import List from "https://cdn.inet.run/tests/datatype/List.i" @@ -975,13 +962,27 @@ end import zero from "https://cdn.inet.run/tests/datatype/Nat.i" import cons from "https://cdn.inet.run/tests/datatype/List.i" -zero (cons :tail) zero cons diff $value @connect value -zero (cons :tail) zero cons diff $value @connect value +(diff) @spread $front $back $value +back zero cons zero cons front @connect value +(diff) @spread $front $back $value +back zero cons zero cons front @connect value +diff_append + +// 上面的代码可以少用一个局部变量 `$value` ,而简化如下: + +(diff) @spread $front $back +back zero cons zero cons front @connect +(diff) @spread $front $back +back zero cons zero cons front @connect +diff_append + +// 再少用一个局部变量 `$back`,进一步简化: + +(diff) @spread $front zero cons zero cons front @connect +(diff) @spread $front zero cons zero cons front @connect diff_append -zero (cons :tail) zero cons diff $value @connect value -zero (cons :tail) zero cons diff $value @connect value -diff_append @run $result +@run $result ``` # 13