diff --git a/README.md b/README.md index f989531f..497d337a 100644 --- a/README.md +++ b/README.md @@ -154,28 +154,28 @@ node diff 'A DiffList :value! end -node diff_append +node diffAppend 'A DiffList :target! 'A DiffList :rest -------- 'A DiffList :return end -node diff_open +node diffOpen 'A DiffList :target! 'A List :list ---------- 'A List :return end -rule diff diff_append - (diff)-front diff return-(diff_append) - (diff_append)-rest diff_open back-(diff) +rule diff diffAppend + (diff)-front diff return-(diffAppend) + (diffAppend)-rest diffOpen back-(diff) end -rule diff diff_open - (diff)-back list-(diff_open) - (diff)-front return-(diff_open) +rule diff diffOpen + (diff)-back list-(diffOpen) + (diff)-front return-(diffOpen) end import zero from "https://code-of-inet.fidb.app/tests/datatype/Nat.i" @@ -185,7 +185,7 @@ import cons from "https://code-of-inet.fidb.app/tests/datatype/List.i" back zero cons zero cons front @connect value (diff) @spread $front $back $value back zero cons zero cons front @connect value -diff_append +diffAppend // By using one less local variable `$value`, // we can simplify the above code: @@ -194,14 +194,14 @@ diff_append back zero cons zero cons front @connect (diff) @spread $front $back back zero cons zero cons front @connect -diff_append +diffAppend // 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 +diffAppend @run $result ``` diff --git a/docs/articles/programming-with-interaction-nets.md b/docs/articles/programming-with-interaction-nets.md index cb58b563..d0e1ea19 100644 --- a/docs/articles/programming-with-interaction-nets.md +++ b/docs/articles/programming-with-interaction-nets.md @@ -588,12 +588,12 @@ But because of single-principal-port constraint, we have to introduce an auxiliary node and some auxiliary rules, to explicitly choose between two interactable edges. -We call the auxiliary node `(max_aux)`. +We call the auxiliary node `(maxAux)`. ``` return | - (max_aux) + (maxAux) / \ first second! ``` @@ -601,7 +601,7 @@ first second! Node definition: ``` -node max_aux +node maxAux Nat :first Nat :second! -------- @@ -615,7 +615,7 @@ the rule between `(add1)` and `(max)`: ``` return return | | - (max) => (max_aux) + (max) => (maxAux) / \ / \ (add1) second prev second | @@ -627,17 +627,17 @@ Rule definition: ``` rule add1 max (max)-second - (add1)-prev max_aux + (add1)-prev maxAux return-(max) end ``` -The rule between `(zero)` and `(max_aux)`: +The rule between `(zero)` and `(maxAux)`: ``` return return | | - (max_aux) => (add1) + (maxAux) => (add1) / \ | first (zero) first ``` @@ -645,18 +645,18 @@ The rule between `(zero)` and `(max_aux)`: Rule definition: ``` -rule zero max_aux - (max_aux)-first add1 - return-(max_aux) +rule zero maxAux + (maxAux)-first add1 + return-(maxAux) end ``` -The rule between `(add1)` and `(max_aux)`: +The rule between `(add1)` and `(maxAux)`: ``` return return | | - (max_aux) => (add1) + (maxAux) => (add1) / \ | first (add1) (max) | / \ @@ -666,10 +666,10 @@ The rule between `(add1)` and `(max_aux)`: Rule definition: ``` -rule add1 max_aux +rule add1 maxAux (add1)-prev - (max_aux)-first max - add1 return-(max_aux) + (maxAux)-first max + add1 return-(maxAux) end ``` @@ -689,7 +689,7 @@ node add1 Nat :value! end -node max_aux +node maxAux Nat :first Nat :second! -------- @@ -708,18 +708,18 @@ rule zero max end rule add1 max - (max)-second (add1)-prev max_aux + (max)-second (add1)-prev maxAux return-(max) end -rule zero max_aux - (max_aux)-first add1 - return-(max_aux) +rule zero maxAux + (maxAux)-first add1 + return-(maxAux) end -rule add1 max_aux - (add1)-prev (max_aux)-first max - add1 return-(max_aux) +rule add1 maxAux + (add1)-prev (maxAux)-first max + add1 return-(maxAux) end claim one -- Nat end @@ -748,15 +748,15 @@ We will find that, to define the interaction rule between `(mul)` and `(zero)` or `(mul)` and `(add1)`, we need to introduce auxiliary nodes again: -- `(nat_erase)` to erase a natural number. -- `(nat_dup)` to duplicate a natural number. +- `(natErase)` to erase a natural number. +- `(natDup)` to duplicate a natural number. These two nodes are different from all aforementioned nodes, because all aforementioned nodes has one output port, but: -- `(nat_erase)` has zero output ports. -- `(nat_dup)` has two output ports. +- `(natErase)` has zero output ports. +- `(natDup)` has two output ports. This is the main reason why we use stack to build net. @@ -799,33 +799,33 @@ import one, two, three, from "https://code-of-inet.fidb.app/tests/datatype/Nat.i" -node nat_erase +node natErase Nat :target! -------- end -rule zero nat_erase end +rule zero natErase end -rule add1 nat_erase - (add1)-prev nat_erase +rule add1 natErase + (add1)-prev natErase end -node nat_dup +node natDup Nat :target! -------- Nat :second Nat :first end -rule zero nat_dup - zero first-(nat_dup) - zero second-(nat_dup) +rule zero natDup + zero first-(natDup) + zero second-(natDup) end -rule add1 nat_dup - (add1)-prev nat_dup $first $second - first add1 first-(nat_dup) - second add1 second-(nat_dup) +rule add1 natDup + (add1)-prev natDup $first $second + first add1 first-(natDup) + second add1 second-(natDup) end node mul @@ -836,17 +836,17 @@ node mul end rule zero mul - (mul)-mulend nat_erase + (mul)-mulend natErase zero return-(mul) end rule add1 mul - (mul)-mulend nat_dup $first $second + (mul)-mulend natDup $first $second (add1)-prev first mul second add return-(mul) end -two nat_dup $first $second +two natDup $first $second two two mul @@ -957,7 +957,7 @@ 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. -[Goto the playground of `DiffList` and `(diff_append)`](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKZGlmZl9hcHBlbmQKCi8vIFVzZSBvbmUgbGVzcyBsb2NhbCB2YXJpYWJsZSBgJHZhbHVlYCwKLy8gd2UgY2FuIHNpbXBsaWZ5IHRoZSBhYm92ZSBjb2RlOgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgJGJhY2sKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZfYXBwZW5kCgovLyBVc2Ugb25lIGxlc3MgbG9jYWwgdmFyaWFibGUgYCRiYWNrYCwKLy8gd2UgY2FuIGZ1cnRoZXIgc2ltcGxpZnkgdGhlIGFib3ZlIGNvZGU6CgooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmX2FwcGVuZAoKQHJ1biAkcmVzdWx0) +[Goto the playground of `DiffList` and `(diffAppend)`](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKZGlmZl9hcHBlbmQKCi8vIFVzZSBvbmUgbGVzcyBsb2NhbCB2YXJpYWJsZSBgJHZhbHVlYCwKLy8gd2UgY2FuIHNpbXBsaWZ5IHRoZSBhYm92ZSBjb2RlOgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgJGJhY2sKYmFjayB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZfYXBwZW5kCgovLyBVc2Ugb25lIGxlc3MgbG9jYWwgdmFyaWFibGUgYCRiYWNrYCwKLy8gd2UgY2FuIGZ1cnRoZXIgc2ltcGxpZnkgdGhlIGFib3ZlIGNvZGU6CgooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdAooZGlmZikgQHNwcmVhZCAkZnJvbnQgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmX2FwcGVuZAoKQHJ1biAkcmVzdWx0) ``` import List from "https://code-of-inet.fidb.app/tests/datatype/List.i" @@ -971,28 +971,28 @@ node diff 'A DiffList :value! end -node diff_append +node diffAppend 'A DiffList :target! 'A DiffList :rest -------- 'A DiffList :return end -node diff_open +node diffOpen 'A DiffList :target! 'A List :list ---------- 'A List :return end -rule diff diff_append - (diff)-front diff return-(diff_append) - (diff_append)-rest diff_open back-(diff) +rule diff diffAppend + (diff)-front diff return-(diffAppend) + (diffAppend)-rest diffOpen back-(diff) end -rule diff diff_open - (diff)-back list-(diff_open) - (diff)-front return-(diff_open) +rule diff diffOpen + (diff)-back list-(diffOpen) + (diff)-front return-(diffOpen) end import zero from "https://code-of-inet.fidb.app/tests/datatype/Nat.i" @@ -1002,7 +1002,7 @@ import cons from "https://code-of-inet.fidb.app/tests/datatype/List.i" back zero cons zero cons front @connect value (diff) @spread $front $back $value back zero cons zero cons front @connect value -diff_append +diffAppend // By using one less local variable `$value`, // we can simplify the above code: @@ -1011,14 +1011,14 @@ diff_append back zero cons zero cons front @connect (diff) @spread $front $back back zero cons zero cons front @connect -diff_append +diffAppend // 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 +diffAppend @run $result ``` 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 5b29e717..49c880b1 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" @@ -567,13 +567,13 @@ end 我们不得不增加一个辅助节点以及相关的规则， 来明显地在两个可反应的边中做出选择。 -我们称辅助节点为 `(max_aux)`， +我们称辅助节点为 `(maxAux)`， 其中 `aux` 是 auxiliary 的所写。 ``` return | - (max_aux) + (maxAux) / \ first second! ``` @@ -581,7 +581,7 @@ first second! 定义如下： ``` -node max_aux +node maxAux Nat :first Nat :second! -------- @@ -594,7 +594,7 @@ end ``` return return | | - (max) => (max_aux) + (max) => (maxAux) / \ / \ (add1) second prev second | @@ -606,17 +606,17 @@ end ``` rule add1 max (max)-second - (add1)-prev max_aux + (add1)-prev maxAux return-(max) end ``` -`(zero)` 与 `(max_aux)` 之间的规则： +`(zero)` 与 `(maxAux)` 之间的规则： ``` return return | | - (max_aux) => (add1) + (maxAux) => (add1) / \ | first (zero) first ``` @@ -624,18 +624,18 @@ end 定义如下： ``` -rule zero max_aux - (max_aux)-first add1 - return-(max_aux) +rule zero maxAux + (maxAux)-first add1 + return-(maxAux) end ``` -`(add1)` 与 `(max_aux)` 之间的规则： +`(add1)` 与 `(maxAux)` 之间的规则： ``` return return | | - (max_aux) => (add1) + (maxAux) => (add1) / \ | first (add1) (max) | / \ @@ -645,10 +645,10 @@ end 定义如下： ``` -rule add1 max_aux +rule add1 maxAux (add1)-prev - (max_aux)-first max - add1 return-(max_aux) + (maxAux)-first max + add1 return-(maxAux) end ``` @@ -668,7 +668,7 @@ node add1 Nat :value! end -node max_aux +node maxAux Nat :first Nat :second! -------- @@ -687,18 +687,18 @@ rule zero max end rule add1 max - (max)-second (add1)-prev max_aux + (max)-second (add1)-prev maxAux return-(max) end -rule zero max_aux - (max_aux)-first add1 - return-(max_aux) +rule zero maxAux + (maxAux)-first add1 + return-(maxAux) end -rule add1 max_aux - (add1)-prev (max_aux)-first max - add1 return-(max_aux) +rule add1 maxAux + (add1)-prev (maxAux)-first max + add1 return-(maxAux) end claim one -- Nat end @@ -726,15 +726,15 @@ three two max 我们将会发现，为了定义 `(mul)` 与 `(zero)` 和 `(add1)` 之间的反应规则， 我们又要引入两个新的辅助节点： -- `(nat_erase)` 删除一个自然数。 -- `(nat_dup)` 复制一个自然数。 +- `(natErase)` 删除一个自然数。 +- `(natDup)` 复制一个自然数。 这两个节点与之前的所有节点都不一样， 之前的所有节点都有一个输出节点， 然而： -- `(nat_erase)` 有零个输出节点。 -- `(nat_dup)` 有两个输出节点。 +- `(natErase)` 有零个输出节点。 +- `(natDup)` 有两个输出节点。 这其实是我们使用栈来构造网的主要原因。 @@ -771,33 +771,33 @@ import one, two, three, from "https://code-of-inet.fidb.app/tests/datatype/Nat.i" -node nat_erase +node natErase Nat :target! -------- end -rule zero nat_erase end +rule zero natErase end -rule add1 nat_erase - (add1)-prev nat_erase +rule add1 natErase + (add1)-prev natErase end -node nat_dup +node natDup Nat :target! -------- Nat :second Nat :first end -rule zero nat_dup - zero first-(nat_dup) - zero second-(nat_dup) +rule zero natDup + zero first-(natDup) + zero second-(natDup) end -rule add1 nat_dup - (add1)-prev nat_dup $first $second - first add1 first-(nat_dup) - second add1 second-(nat_dup) +rule add1 natDup + (add1)-prev natDup $first $second + first add1 first-(natDup) + second add1 second-(natDup) end node mul @@ -808,17 +808,17 @@ node mul end rule zero mul - (mul)-mulend nat_erase + (mul)-mulend natErase zero return-(mul) end rule add1 mul - (mul)-mulend nat_dup $first $second + (mul)-mulend natDup $first $second (add1)-prev first mul second add return-(mul) end -two nat_dup $first $second +two natDup $first $second two two mul @@ -921,7 +921,7 @@ append @run $result 后面跟着的 `@spread` 可以将其所有接口按定义中相反的顺序返回到栈中， 然后我们把这些接口保存到了一些局部变量中。 -[去 `DiffList` 与 `(diff_append)` 的演算场](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKZGlmZl9hcHBlbmQKCi8vIOS4iumdoueahOS7o-eggeWPr-S7peWwkeeUqOS4gOS4quWxgOmDqOWPmOmHjyBgJHZhbHVlYCDvvIzogIznroDljJblpoLkuIvvvJoKCihkaWZmKSBAc3ByZWFkICRmcm9udCAkYmFjawpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmX2FwcGVuZAoKLy8g5YaN5bCR55So5LiA5Liq5bGA6YOo5Y-Y6YePIGAkYmFja2DvvIzov5vkuIDmraXnroDljJbvvJoKCihkaWZmKSBAc3ByZWFkICRmcm9udCB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CihkaWZmKSBAc3ByZWFkICRmcm9udCB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZfYXBwZW5kCgpAcnVuICRyZXN1bHQ) +[去 `DiffList` 与 `(diffAppend)` 的演算场](https://inet.run/playground/aW1wb3J0IExpc3QgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBEaWZmTGlzdCBAVHlwZSAtLSBAVHlwZSBlbmQKCm5vZGUgZGlmZgogICdBIExpc3QgOmZyb250CiAgLS0tLS0tLQogICdBIExpc3QgOmJhY2sKICAnQSBEaWZmTGlzdCA6dmFsdWUhCmVuZAoKbm9kZSBkaWZmX2FwcGVuZAogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgRGlmZkxpc3QgOnJlc3QKICAtLS0tLS0tLQogICdBIERpZmZMaXN0IDpyZXR1cm4KZW5kCgpub2RlIGRpZmZfb3BlbgogICdBIERpZmZMaXN0IDp0YXJnZXQhCiAgJ0EgTGlzdCA6bGlzdAogIC0tLS0tLS0tLS0KICAnQSBMaXN0IDpyZXR1cm4KZW5kCgpydWxlIGRpZmYgZGlmZl9hcHBlbmQKICAoZGlmZiktZnJvbnQgZGlmZiByZXR1cm4tKGRpZmZfYXBwZW5kKQogIChkaWZmX2FwcGVuZCktcmVzdCBkaWZmX29wZW4gYmFjay0oZGlmZikKZW5kCgpydWxlIGRpZmYgZGlmZl9vcGVuCiAgKGRpZmYpLWJhY2sgbGlzdC0oZGlmZl9vcGVuKQogIChkaWZmKS1mcm9udCByZXR1cm4tKGRpZmZfb3BlbikKZW5kCgppbXBvcnQgemVybyBmcm9tICJodHRwczovL2Nkbi5pbmV0LnJ1bi90ZXN0cy9kYXRhdHlwZS9OYXQuaSIKaW1wb3J0IGNvbnMgZnJvbSAiaHR0cHM6Ly9jZG4uaW5ldC5ydW4vdGVzdHMvZGF0YXR5cGUvTGlzdC5pIgoKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrICR2YWx1ZQpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QgdmFsdWUKZGlmZl9hcHBlbmQKCi8vIOS4iumdoueahOS7o-eggeWPr-S7peWwkeeUqOS4gOS4quWxgOmDqOWPmOmHjyBgJHZhbHVlYCDvvIzogIznroDljJblpoLkuIvvvJoKCihkaWZmKSBAc3ByZWFkICRmcm9udCAkYmFjawpiYWNrIHplcm8gY29ucyB6ZXJvIGNvbnMgZnJvbnQgQGNvbm5lY3QKKGRpZmYpIEBzcHJlYWQgJGZyb250ICRiYWNrCmJhY2sgemVybyBjb25zIHplcm8gY29ucyBmcm9udCBAY29ubmVjdApkaWZmX2FwcGVuZAoKLy8g5YaN5bCR55So5LiA5Liq5bGA6YOo5Y-Y6YePIGAkYmFja2DvvIzov5vkuIDmraXnroDljJbvvJoKCihkaWZmKSBAc3ByZWFkICRmcm9udCB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CihkaWZmKSBAc3ByZWFkICRmcm9udCB6ZXJvIGNvbnMgemVybyBjb25zIGZyb250IEBjb25uZWN0CmRpZmZfYXBwZW5kCgpAcnVuICRyZXN1bHQ) ``` import List from "https://code-of-inet.fidb.app/tests/datatype/List.i" @@ -935,28 +935,28 @@ node diff 'A DiffList :value! end -node diff_append +node diffAppend 'A DiffList :target! 'A DiffList :rest -------- 'A DiffList :return end -node diff_open +node diffOpen 'A DiffList :target! 'A List :list ---------- 'A List :return end -rule diff diff_append - (diff)-front diff return-(diff_append) - (diff_append)-rest diff_open back-(diff) +rule diff diffAppend + (diff)-front diff return-(diffAppend) + (diffAppend)-rest diffOpen back-(diff) end -rule diff diff_open - (diff)-back list-(diff_open) - (diff)-front return-(diff_open) +rule diff diffOpen + (diff)-back list-(diffOpen) + (diff)-front return-(diffOpen) end import zero from "https://code-of-inet.fidb.app/tests/datatype/Nat.i" @@ -966,7 +966,7 @@ import cons from "https://code-of-inet.fidb.app/tests/datatype/List.i" back zero cons zero cons front @connect value (diff) @spread $front $back $value back zero cons zero cons front @connect value -diff_append +diffAppend // 上面的代码可以少用一个局部变量 `$value` ，而简化如下： @@ -974,13 +974,13 @@ diff_append back zero cons zero cons front @connect (diff) @spread $front $back back zero cons zero cons front @connect -diff_append +diffAppend // 再少用一个局部变量 `$back`，进一步简化： (diff) @spread $front zero cons zero cons front @connect (diff) @spread $front zero cons zero cons front @connect -diff_append +diffAppend @run $result ``` diff --git a/docs/diary/2023-07-27-design-of-new-syntax.md b/docs/diary/2023-07-27-design-of-new-syntax.md index 52ba9f9a..67016f9f 100644 --- a/docs/diary/2023-07-27-design-of-new-syntax.md +++ b/docs/diary/2023-07-27-design-of-new-syntax.md @@ -109,7 +109,7 @@ defru cons append append cons end -defn six_soles +defn sixSoles null sole cons sole cons sole cons null sole cons sole cons sole cons append @@ -125,35 +125,35 @@ defnode diff -- DiffList('A)! end -defnode diff_append +defnode diffAppend left: DiffList('A)! right: DiffList('A) -- DiffList('A) end -defnode diff_open +defnode diffOpen DiffList('A)! list: List('A) -- List('A) end -defrule diff diff_append - (diff)-right (diff_append)-right diff_open +defrule diff diffAppend + (diff)-right (diffAppend)-right diffOpen (diff)-left diff end -defrule diff diff_open - (diff)-right list-(diff_open) - (diff)-left return-(diff_open) +defrule diff diffOpen + (diff)-right list-(diffOpen) + (diff)-left return-(diffOpen) end -defru diff diff_append +defru diff diffAppend - diff_open diff + diffOpen diff end -defru diff diff_open +defru diff diffOpen connect @@ -166,15 +166,15 @@ If a wire's two ports are connected with port `A` and `B`, after building a net, we remove the wire, and connect `A` with `B`. ```inet -defn one_two_soles +defn oneTwoSoles wire sole cons diff wire sole cons sole cons diff - diff_append + diffAppend end -defn two_two_soles +defn twoTwoSoles wire sole cons sole cons diff wire sole cons sole cons diff - diff_append + diffAppend end ``` diff --git a/docs/diary/2023-09-13-refactor-the-syntax-of-rearrange-to-literal-node-and-spread.md b/docs/diary/2023-09-13-refactor-the-syntax-of-rearrange-to-literal-node-and-spread.md index a70e5c41..9efa8ab3 100644 --- a/docs/diary/2023-09-13-refactor-the-syntax-of-rearrange-to-literal-node-and-spread.md +++ b/docs/diary/2023-09-13-refactor-the-syntax-of-rearrange-to-literal-node-and-spread.md @@ -35,7 +35,7 @@ Example usage to construct `DiffList`: ``` zero (cons :tail) zero cons diff $value @connect value zero (cons :tail) zero cons diff $value @connect value -diff_append +diffAppend ``` Now the syntax of rearrange is removed, @@ -47,7 +47,7 @@ and `@spread` to get all it's ports. back zero cons zero cons front @connect value (diff) @spread $front $back $value back zero cons zero cons front @connect value -diff_append +diffAppend // use less variables: @@ -55,11 +55,11 @@ diff_append back zero cons zero cons front @connect (diff) @spread $front $back back zero cons zero cons front @connect -diff_append +diffAppend // use less variables: (diff) @spread $front zero cons zero cons front @connect (diff) @spread $front zero cons zero cons front @connect -diff_append +diffAppend ``` diff --git a/src/lang/builtins/inspect.ts b/src/lang/builtins/inspect.ts index d17c195a..29793786 100644 --- a/src/lang/builtins/inspect.ts +++ b/src/lang/builtins/inspect.ts @@ -14,9 +14,9 @@ export function compose(env: Env): void { const connectedcomponent = findConnectedComponent(env.net, value.node) const netText = formatNet(connectedcomponent) if (netText.length === 0) { - env.mod.loader.onOutput(`net_from_port ${formatValue(value)} end`) + env.mod.loader.onOutput(`netFromPort ${formatValue(value)} end`) } else { - env.mod.loader.onOutput(`net_from_port ${formatValue(value)}`) + env.mod.loader.onOutput(`netFromPort ${formatValue(value)}`) env.mod.loader.onOutput(indent(netText)) env.mod.loader.onOutput("end") } diff --git a/src/lang/cap/capInputPort.ts b/src/lang/cap/capInputPort.ts index 6a0585a8..2d467a1f 100644 --- a/src/lang/cap/capInputPort.ts +++ b/src/lang/cap/capInputPort.ts @@ -15,7 +15,7 @@ export function capInputPort(mod: Mod, net: Net, port: Port): Port { isPrincipal: false, } - const node = addNode(net, mod, "@input_port_cap", [], [portExp]) + const node = addNode(net, mod, "@inputPortCap", [], [portExp]) const nodeEntry = findNodeEntryOrFail(net, node) nodeEntry.asPortCap = { nodeName: port.node.name, diff --git a/src/lang/cap/capOutputPort.ts b/src/lang/cap/capOutputPort.ts index 5343bfdf..e43c9be8 100644 --- a/src/lang/cap/capOutputPort.ts +++ b/src/lang/cap/capOutputPort.ts @@ -15,7 +15,7 @@ export function capOutputPort(mod: Mod, net: Net, port: Port): Port { isPrincipal: false, } - const node = addNode(net, mod, "@ouput_port_cap", [portExp], []) + const node = addNode(net, mod, "@ouputPortCap", [portExp], []) const nodeEntry = findNodeEntryOrFail(net, node) nodeEntry.asPortCap = { nodeName: port.node.name, diff --git a/src/lang/cap/capType.ts b/src/lang/cap/capType.ts index 5e7af138..54cd5fb9 100644 --- a/src/lang/cap/capType.ts +++ b/src/lang/cap/capType.ts @@ -15,7 +15,7 @@ export function capType(mod: Mod, net: Net, t: Value): Port { isPrincipal: false, } - const node = addNode(net, mod, "@type_cap", [], [portExp]) + const node = addNode(net, mod, "@typeCap", [], [portExp]) const nodeEntry = findNodeEntryOrFail(net, node) nodeEntry.asTypeCap = {} diff --git a/src/lang/present/presentNodeAsNet.test.ts b/src/lang/present/presentNodeAsNet.test.ts index ae7c21f8..b28d0b44 100644 --- a/src/lang/present/presentNodeAsNet.test.ts +++ b/src/lang/present/presentNodeAsNet.test.ts @@ -25,8 +25,8 @@ end const net = presentNodeAsNet(mod, "add") expect(formatNet(net)).toMatchInlineSnapshot(` - "(add₀)-target covering-(@input_port_cap₀) - (add₀)-addend covering-(@input_port_cap₁) - (add₀)-return covering-(@ouput_port_cap₀)" + "(add₀)-target covering-(@inputPortCap₀) + (add₀)-addend covering-(@inputPortCap₁) + (add₀)-return covering-(@ouputPortCap₀)" `) }) diff --git a/src/lang/present/presentRuleAsNets.test.ts b/src/lang/present/presentRuleAsNets.test.ts index 28c9907a..358d0349 100644 --- a/src/lang/present/presentRuleAsNets.test.ts +++ b/src/lang/present/presentRuleAsNets.test.ts @@ -47,16 +47,16 @@ end const [initial, final] = presentRuleAsNets(mod, "add1 add") expect(formatNet(initial)).toMatchInlineSnapshot(` - "(add1₂)-prev covering-(@input_port_cap₃) + "(add1₂)-prev covering-(@inputPortCap₃) (add1₂)-value!target-(add₃) - (add₃)-addend covering-(@input_port_cap₄) - (add₃)-return covering-(@ouput_port_cap₂)" + (add₃)-addend covering-(@inputPortCap₄) + (add₃)-return covering-(@ouputPortCap₂)" `) expect(formatNet(final)).toMatchInlineSnapshot(` - "(@input_port_cap₃)-covering target-(add₄) - (@input_port_cap₄)-covering addend-(add₄) - (@ouput_port_cap₂)-covering value-(add1₃) + "(@inputPortCap₃)-covering target-(add₄) + (@inputPortCap₄)-covering addend-(add₄) + (@ouputPortCap₂)-covering value-(add1₃) (add₄)-return prev-(add1₃)" `) }) diff --git a/src/lang/present/presentWordAsEnv.test.ts b/src/lang/present/presentWordAsEnv.test.ts index c23063e9..a7b08e95 100644 --- a/src/lang/present/presentWordAsEnv.test.ts +++ b/src/lang/present/presentWordAsEnv.test.ts @@ -73,9 +73,9 @@ define addadd add add end expect(formatEnv(presentWordAsEnv(mod, "addadd"))).toMatchInlineSnapshot(` "env net - (@type_cap₃)-covering addend-(add₈) - (@type_cap₄)-covering addend-(add₇) - (@type_cap₅)-covering target-(add₇) + (@typeCap₃)-covering addend-(add₈) + (@typeCap₄)-covering addend-(add₇) + (@typeCap₅)-covering target-(add₇) (add₇)-return target-(add₈) end stack diff --git a/tests/builtin/apply.i.out b/tests/builtin/apply.i.out index f5805841..2f16ef5a 100644 --- a/tests/builtin/apply.i.out +++ b/tests/builtin/apply.i.out @@ -1,4 +1,4 @@ -net_from_port (zero₀)-value! end -net_from_port (add1₀)-value! +netFromPort (zero₀)-value! end +netFromPort (add1₀)-value! (add1₀)-prev value-(zero₀) end diff --git a/tests/builtin/run-only-top-port.i.out b/tests/builtin/run-only-top-port.i.out index 3610fdf0..f6b64bcd 100644 --- a/tests/builtin/run-only-top-port.i.out +++ b/tests/builtin/run-only-top-port.i.out @@ -1,14 +1,14 @@ -net_from_port (add1₂₅)-value! +netFromPort (add1₂₅)-value! (add1₂₅)-prev value-(add1₂₃) (add1₂₃)-prev value-(zero₂₁) end -net_from_port (add₁₀)-return +netFromPort (add₁₀)-return (add₁₀)-target!value-(add1₂₂) (add₁₀)-addend value-(add1₂₁) (add1₂₂)-prev value-(zero₂₀) (add1₂₁)-prev value-(zero₁₉) end -net_from_port (add1₂₆)-value! +netFromPort (add1₂₆)-value! (add1₂₆)-prev value-(add1₂₁) (add1₂₁)-prev value-(zero₁₉) end diff --git a/tests/builtin/spread.i.out b/tests/builtin/spread.i.out index d506d143..68bc6b7e 100644 --- a/tests/builtin/spread.i.out +++ b/tests/builtin/spread.i.out @@ -1,3 +1,3 @@ -net_from_port (add₀)-target! end -net_from_port (add₀)-addend end -net_from_port (add₀)-return end +netFromPort (add₀)-target! end +netFromPort (add₀)-addend end +netFromPort (add₀)-return end diff --git a/tests/checking/claim-input-arity-extra.error.i.err b/tests/checking/claim-input-arity-extra.error.i.err index 0f0685d9..42ed59d6 100644 --- a/tests/checking/claim-input-arity-extra.error.i.err +++ b/tests/checking/claim-input-arity-extra.error.i.err @@ -1,7 +1,7 @@ [checkWords] I expect the stack to be empty after checking. stack length: 1 - stack: [(@type_cap₀)-covering] + stack: [(@typeCap₀)-covering] Maybe this is due to extra input arity, or lack of output arity. diff --git a/tests/checking/claim-output-arity-lack.error.i.err b/tests/checking/claim-output-arity-lack.error.i.err index af73bf49..790c2ea2 100644 --- a/tests/checking/claim-output-arity-lack.error.i.err +++ b/tests/checking/claim-output-arity-lack.error.i.err @@ -1,7 +1,7 @@ [checkWords] I expect the stack to be empty after checking. stack length: 1 - stack: [(@type_cap₀)-covering] + stack: [(@typeCap₀)-covering] Maybe this is due to extra input arity, or lack of output arity. diff --git a/tests/checking/locals-not-used-in-define.error.i b/tests/checking/locals-not-used-in-define.error.i index 61df71db..47f9a046 100644 --- a/tests/checking/locals-not-used-in-define.error.i +++ b/tests/checking/locals-not-used-in-define.error.i @@ -1,2 +1,2 @@ -claim my_drop 'A -- end -define my_drop $a end +claim myDrop 'A -- end +define myDrop $a end diff --git a/tests/checking/locals-not-used-in-define.error.i.err b/tests/checking/locals-not-used-in-define.error.i.err index 67cc5207..e2124234 100644 --- a/tests/checking/locals-not-used-in-define.error.i.err +++ b/tests/checking/locals-not-used-in-define.error.i.err @@ -4,8 +4,8 @@ [Define.execute] I fail to define word. - word: my_drop + word: myDrop - 1 |claim my_drop 'A -- end - 2 |define my_drop $a end + 1 |claim myDrop 'A -- end + 2 |define myDrop $a end 3 | diff --git a/tests/checking/rule-sign.error.i.err b/tests/checking/rule-sign.error.i.err index c1be4c13..b1b33503 100644 --- a/tests/checking/rule-sign.error.i.err +++ b/tests/checking/rule-sign.error.i.err @@ -1,8 +1,8 @@ [checkSigns] I expect the two ports to have opposite signs, but they all have positive sign. - first port: (@input_port_cap₂)-covering - second port: (@input_port_cap₁)-covering + first port: (@inputPortCap₂)-covering + second port: (@inputPortCap₁)-covering [compose] I fail compose word. diff --git a/tests/datatype/Bin.i b/tests/datatype/Bin.i index 0abdfb10..3a7ee784 100644 --- a/tests/datatype/Bin.i +++ b/tests/datatype/Bin.i @@ -21,39 +21,39 @@ end // Utilities -node bin_dup +node binDup Bin :value! ------------ Bin :result1 Bin :result2 end -rule b1 bin_dup - (b1)-higherbits bin_dup $d b1 result1-(bin_dup) d b1 result2-(bin_dup) +rule b1 binDup + (b1)-higherbits binDup $d b1 result1-(binDup) d b1 result2-(binDup) end -rule b0 bin_dup - (b0)-higherbits bin_dup $d b0 result1-(bin_dup) d b0 result2-(bin_dup) +rule b0 binDup + (b0)-higherbits binDup $d b0 result1-(binDup) d b0 result2-(binDup) end -rule bend bin_dup - bend result1-(bin_dup) bend result2-(bin_dup) +rule bend binDup + bend result1-(binDup) bend result2-(binDup) end -node bin_erase +node binErase Bin :value! ------------ end -rule b1 bin_erase - (b1)-higherbits bin_erase +rule b1 binErase + (b1)-higherbits binErase end -rule b0 bin_erase - (b0)-higherbits bin_erase +rule b0 binErase + (b0)-higherbits binErase end -rule bend bin_erase +rule bend binErase end // b0q -- b0 when in the middle of a number, replaced by bend elsewhere - used to avoid unnecessary leading zeroes @@ -150,33 +150,33 @@ rule b0 bmul end rule b1 bmul - (b1)-higherbits (bmul)-left bin_dup $d bmul b0q d badd result-(bmul) + (b1)-higherbits (bmul)-left binDup $d bmul b0q d badd result-(bmul) end rule bend bmul bend result-(bmul) - (bmul)-left bin_erase + (bmul)-left binErase end // Conversion to and from Nat import Nat, zero, add1, - nat_erase, nat_dup + natErase, natDup from "./Nat.i" -node nat_double +node natDouble Nat :target! ------------ Nat :return end -rule zero nat_double - zero return-(nat_double) +rule zero natDouble + zero return-(natDouble) end -rule add1 nat_double - (add1)-prev nat_double add1 add1 return-(nat_double) +rule add1 natDouble + (add1)-prev natDouble add1 add1 return-(natDouble) end node ntob @@ -202,11 +202,11 @@ node bton end rule b0 bton - (b0)-higherbits bton nat_double result-(bton) + (b0)-higherbits bton natDouble result-(bton) end rule b1 bton - (b1)-higherbits bton nat_double add1 result-(bton) + (b1)-higherbits bton natDouble add1 result-(bton) end rule bend bton diff --git a/tests/datatype/Bin.test.i.out b/tests/datatype/Bin.test.i.out index 6a793e8e..b65233f7 100644 --- a/tests/datatype/Bin.test.i.out +++ b/tests/datatype/Bin.test.i.out @@ -1,4 +1,4 @@ -net_from_port (bmul₅)-result +netFromPort (bmul₅)-result (bmul₅)-left result-(ntob₃) (bmul₅)-right!value-(b0₁₆) (ntob₃)-nat!value-(add1₃₂) @@ -13,7 +13,7 @@ net_from_port (bmul₅)-result (b1₁₅)-higherbits value-(b1₁₄) (b1₁₄)-higherbits value-(bend₁₅) end -net_from_port (b0₁₇)-value! +netFromPort (b0₁₇)-value! (b0₁₇)-higherbits value-(b1₂₆) (b1₂₆)-higherbits value-(b0₂₃) (b0₂₃)-higherbits value-(b1₃₉) diff --git a/tests/datatype/DiffList.i b/tests/datatype/DiffList.i index b04edf81..e2917079 100644 --- a/tests/datatype/DiffList.i +++ b/tests/datatype/DiffList.i @@ -16,26 +16,26 @@ node diff 'A DiffList :value! end -node diff_append +node diffAppend 'A DiffList :target! 'A DiffList :rest -------- 'A DiffList :return end -node diff_open +node diffOpen 'A DiffList :target! 'A List :list ---------- 'A List :return end -rule diff diff_append - (diff)-front diff return-(diff_append) - (diff_append)-rest diff_open back-(diff) +rule diff diffAppend + (diff)-front diff return-(diffAppend) + (diffAppend)-rest diffOpen back-(diff) end -rule diff diff_open - (diff)-back list-(diff_open) - (diff)-front return-(diff_open) +rule diff diffOpen + (diff)-back list-(diffOpen) + (diff)-front return-(diffOpen) end diff --git a/tests/datatype/DiffList.test.i b/tests/datatype/DiffList.test.i index 800f462b..70a480cf 100644 --- a/tests/datatype/DiffList.test.i +++ b/tests/datatype/DiffList.test.i @@ -1,22 +1,22 @@ require "DiffList.i" require "Trivial.i" -claim one_two_soles -- Trivial DiffList end +claim oneTwoSoles -- Trivial DiffList end -define one_two_soles +define oneTwoSoles (diff) @spread $front sole cons front @connect (diff) @spread $front sole cons sole cons front @connect - diff_append + diffAppend end -one_two_soles @inspect @run @inspect +oneTwoSoles @inspect @run @inspect -claim two_two_soles -- Trivial DiffList end +claim twoTwoSoles -- Trivial DiffList end -define two_two_soles +define twoTwoSoles (diff) @spread $front sole cons sole cons front @connect (diff) @spread $front sole cons sole cons front @connect - diff_append + diffAppend end -two_two_soles @inspect @run @inspect +twoTwoSoles @inspect @run @inspect diff --git a/tests/datatype/DiffList.test.i.out b/tests/datatype/DiffList.test.i.out index dd33eb93..055b32c7 100644 --- a/tests/datatype/DiffList.test.i.out +++ b/tests/datatype/DiffList.test.i.out @@ -1,6 +1,6 @@ -net_from_port (diff_append₂)-return - (diff_append₂)-target!value-(diff₆) - (diff_append₂)-rest value-(diff₅) +netFromPort (diffAppend₂)-return + (diffAppend₂)-target!value-(diff₆) + (diffAppend₂)-rest value-(diff₅) (diff₆)-front value-(cons₇) (diff₆)-back tail-(cons₆) (cons₇)-head value-(sole₅) @@ -10,7 +10,7 @@ net_from_port (diff_append₂)-return (diff₅)-back tail-(cons₅) (cons₅)-head value-(sole₃) end -net_from_port (diff₇)-value! +netFromPort (diff₇)-value! (diff₇)-front value-(cons₇) (diff₇)-back tail-(cons₅) (cons₇)-head value-(sole₅) @@ -19,9 +19,9 @@ net_from_port (diff₇)-value! (cons₆)-tail value-(cons₅) (cons₅)-head value-(sole₃) end -net_from_port (diff_append₄)-return - (diff_append₄)-target!value-(diff₁₁) - (diff_append₄)-rest value-(diff₁₀) +netFromPort (diffAppend₄)-return + (diffAppend₄)-target!value-(diff₁₁) + (diffAppend₄)-rest value-(diff₁₀) (diff₁₁)-front value-(cons₁₅) (diff₁₁)-back tail-(cons₁₄) (cons₁₅)-head value-(sole₁₃) @@ -33,7 +33,7 @@ net_from_port (diff_append₄)-return (cons₁₃)-tail value-(cons₁₂) (cons₁₂)-head value-(sole₁₀) end -net_from_port (diff₁₂)-value! +netFromPort (diff₁₂)-value! (diff₁₂)-front value-(cons₁₅) (diff₁₂)-back tail-(cons₁₂) (cons₁₅)-head value-(sole₁₃) diff --git a/tests/datatype/List.test.i b/tests/datatype/List.test.i index dd2a7472..12ce8b10 100644 --- a/tests/datatype/List.test.i +++ b/tests/datatype/List.test.i @@ -1,12 +1,12 @@ require "List.i" require "Trivial.i" -claim six_soles -- Trivial List end +claim sixSoles -- Trivial List end -define six_soles +define sixSoles null sole cons sole cons sole cons null sole cons sole cons sole cons append end -six_soles @inspect @run @inspect +sixSoles @inspect @run @inspect diff --git a/tests/datatype/List.test.i.out b/tests/datatype/List.test.i.out index 76d86492..81f03701 100644 --- a/tests/datatype/List.test.i.out +++ b/tests/datatype/List.test.i.out @@ -1,4 +1,4 @@ -net_from_port (append₄)-return +netFromPort (append₄)-return (append₄)-target!value-(cons₁₃) (append₄)-rest value-(cons₁₀) (cons₁₃)-head value-(sole₁₁) @@ -14,7 +14,7 @@ net_from_port (append₄)-return (cons₈)-head value-(sole₆) (cons₈)-tail value-(null₃) end -net_from_port (cons₁₄)-value! +netFromPort (cons₁₄)-value! (cons₁₄)-head value-(sole₁₁) (cons₁₄)-tail value-(cons₁₅) (cons₁₅)-head value-(sole₁₀) diff --git a/tests/datatype/Nat.i b/tests/datatype/Nat.i index e6930bf3..a7486919 100644 --- a/tests/datatype/Nat.i +++ b/tests/datatype/Nat.i @@ -42,35 +42,35 @@ define three two one add end claim four -- Nat end define four two two add end -// To define `mul`, we first need `nat_erase` and `nat_dup`. +// To define `mul`, we first need `natErase` and `natDup`. -node nat_erase +node natErase Nat :target! -------- end -rule zero nat_erase end +rule zero natErase end -rule add1 nat_erase - (add1)-prev nat_erase +rule add1 natErase + (add1)-prev natErase end -node nat_dup +node natDup Nat :target! -------- Nat :second Nat :first end -rule zero nat_dup - zero first-(nat_dup) - zero second-(nat_dup) +rule zero natDup + zero first-(natDup) + zero second-(natDup) end -rule add1 nat_dup - (add1)-prev nat_dup $first $second - first add1 first-(nat_dup) - second add1 second-(nat_dup) +rule add1 natDup + (add1)-prev natDup $first $second + first add1 first-(natDup) + second add1 second-(natDup) end node mul @@ -81,19 +81,19 @@ node mul end rule zero mul - (mul)-mulend nat_erase + (mul)-mulend natErase zero return-(mul) end rule add1 mul - (mul)-mulend nat_dup $first $second + (mul)-mulend natDup $first $second (add1)-prev first mul second add return-(mul) end -// To define `max`, we need `max_aux`. +// To define `max`, we need `maxAux`. -node max_aux +node maxAux Nat :first Nat :second! -------- @@ -112,16 +112,16 @@ rule zero max end rule add1 max - (max)-second (add1)-prev max_aux + (max)-second (add1)-prev maxAux return-(max) end -rule zero max_aux - (max_aux)-first add1 - return-(max_aux) +rule zero maxAux + (maxAux)-first add1 + return-(maxAux) end -rule add1 max_aux - (add1)-prev (max_aux)-first max - add1 return-(max_aux) +rule add1 maxAux + (add1)-prev (maxAux)-first max + add1 return-(maxAux) end diff --git a/tests/datatype/Nat.test.i b/tests/datatype/Nat.test.i index 3f743cf7..eef5afb4 100644 --- a/tests/datatype/Nat.test.i +++ b/tests/datatype/Nat.test.i @@ -14,8 +14,8 @@ define addadd add add end one one one addadd @run @inspect -two nat_erase zero @inspect @run @inspect -two nat_dup @inspect @run @inspect +two natErase zero @inspect @run @inspect +two natDup @inspect @run @inspect two two mul @inspect @run @inspect three three mul @inspect @run @inspect diff --git a/tests/datatype/Nat.test.i.out b/tests/datatype/Nat.test.i.out index 72b2d31d..9049e308 100644 --- a/tests/datatype/Nat.test.i.out +++ b/tests/datatype/Nat.test.i.out @@ -1,19 +1,19 @@ -net_from_port (add₁₀)-return +netFromPort (add₁₀)-return (add₁₀)-target!value-(zero₂₀) (add₁₀)-addend value-(zero₁₉) end -net_from_port (zero₁₉)-value! end -net_from_port (add₁₁)-return +netFromPort (zero₁₉)-value! end +netFromPort (add₁₁)-return (add₁₁)-target!value-(add1₂₂) (add₁₁)-addend value-(add1₂₁) (add1₂₂)-prev value-(zero₂₂) (add1₂₁)-prev value-(zero₂₁) end -net_from_port (add1₂₃)-value! +netFromPort (add1₂₃)-value! (add1₂₃)-prev value-(add1₂₁) (add1₂₁)-prev value-(zero₂₁) end -net_from_port (add₁₅)-return +netFromPort (add₁₅)-return (add₁₅)-target return-(add₁₄) (add₁₅)-addend return-(add₁₃) (add₁₄)-target!value-(add1₂₇) @@ -25,39 +25,39 @@ net_from_port (add₁₅)-return (add1₂₅)-prev value-(zero₂₄) (add1₂₄)-prev value-(zero₂₃) end -net_from_port (add1₃₀)-value! +netFromPort (add1₃₀)-value! (add1₃₀)-prev value-(add1₃₁) (add1₃₁)-prev value-(add1₂₈) (add1₂₈)-prev value-(add1₂₄) (add1₂₄)-prev value-(zero₂₃) end -net_from_port (add₂₀)-return +netFromPort (add₂₀)-return (add₂₀)-target!value-(add1₃₂) (add₂₀)-addend value-(zero₂₇) (add1₃₂)-prev value-(zero₂₈) end -net_from_port (add1₃₃)-value! +netFromPort (add1₃₃)-value! (add1₃₃)-prev value-(zero₂₇) end -net_from_port (add1₃₈)-value! +netFromPort (add1₃₈)-value! (add1₃₈)-prev value-(add1₃₉) (add1₃₉)-prev value-(add1₃₄) (add1₃₄)-prev value-(zero₂₉) end -net_from_port (zero₃₄)-value! end -net_from_port (zero₃₄)-value! end -net_from_port (nat_dup₄)-first - (nat_dup₄)-target return-(add₃₀) +netFromPort (zero₃₄)-value! end +netFromPort (zero₃₄)-value! end +netFromPort (natDup₄)-first + (natDup₄)-target return-(add₃₀) (add₃₀)-target!value-(add1₄₃) (add₃₀)-addend value-(add1₄₂) (add1₄₃)-prev value-(zero₃₆) (add1₄₂)-prev value-(zero₃₅) end -net_from_port (add1₄₅)-value! +netFromPort (add1₄₅)-value! (add1₄₅)-prev value-(add1₄₇) (add1₄₇)-prev value-(zero₃₇) end -net_from_port (mul₃)-return +netFromPort (mul₃)-return (mul₃)-target return-(add₃₃) (mul₃)-mulend return-(add₃₂) (add₃₃)-target!value-(add1₅₂) @@ -69,13 +69,13 @@ net_from_port (mul₃)-return (add1₅₀)-prev value-(zero₄₀) (add1₄₉)-prev value-(zero₃₉) end -net_from_port (add1₅₇)-value! +netFromPort (add1₅₇)-value! (add1₅₇)-prev value-(add1₆₀) (add1₆₀)-prev value-(add1₆₃) (add1₆₃)-prev value-(add1₆₆) (add1₆₆)-prev value-(zero₅₁) end -net_from_port (mul₈)-return +netFromPort (mul₈)-return (mul₈)-target return-(add₄₇) (mul₈)-mulend return-(add₄₅) (add₄₇)-target!value-(add1₇₂) @@ -93,7 +93,7 @@ net_from_port (mul₈)-return (add1₆₈)-prev value-(zero₅₃) (add1₆₇)-prev value-(zero₅₂) end -net_from_port (add1₇₉)-value! +netFromPort (add1₇₉)-value! (add1₇₉)-prev value-(add1₈₂) (add1₈₂)-prev value-(add1₈₅) (add1₈₅)-prev value-(add1₈₈) @@ -104,15 +104,15 @@ net_from_port (add1₇₉)-value! (add1₁₀₀)-prev value-(add1₁₀₃) (add1₁₀₃)-prev value-(zero₇₀) end -net_from_port (add1₁₀₇)-value! +netFromPort (add1₁₀₇)-value! (add1₁₀₇)-prev value-(add1₁₀₄) (add1₁₀₄)-prev value-(zero₇₂) end -net_from_port (add1₁₁₂)-value! +netFromPort (add1₁₁₂)-value! (add1₁₁₂)-prev value-(add1₁₁₃) (add1₁₁₃)-prev value-(zero₇₅) end -net_from_port (add1₁₂₂)-value! +netFromPort (add1₁₂₂)-value! (add1₁₂₂)-prev value-(add1₁₂₃) (add1₁₂₃)-prev value-(add1₁₁₄) (add1₁₁₄)-prev value-(zero₇₇) diff --git a/tests/module/import.i.out b/tests/module/import.i.out index c127b782..a115079b 100644 --- a/tests/module/import.i.out +++ b/tests/module/import.i.out @@ -1,8 +1,8 @@ -net_from_port (add₁₀)-return +netFromPort (add₁₀)-return (add₁₀)-target!value-(add1₂₁) (add₁₀)-addend value-(zero₁₉) (add1₂₁)-prev value-(zero₂₀) end -net_from_port (add1₂₂)-value! +netFromPort (add1₂₂)-value! (add1₂₂)-prev value-(zero₁₉) end diff --git a/tests/module/require.i.out b/tests/module/require.i.out index c127b782..a115079b 100644 --- a/tests/module/require.i.out +++ b/tests/module/require.i.out @@ -1,8 +1,8 @@ -net_from_port (add₁₀)-return +netFromPort (add₁₀)-return (add₁₀)-target!value-(add1₂₁) (add₁₀)-addend value-(zero₁₉) (add1₂₁)-prev value-(zero₂₀) end -net_from_port (add1₂₂)-value! +netFromPort (add1₂₂)-value! (add1₂₂)-prev value-(zero₁₉) end diff --git a/tests/module/reuqire-more-rules-3.i.out b/tests/module/reuqire-more-rules-3.i.out index a3871425..4831088c 100644 --- a/tests/module/reuqire-more-rules-3.i.out +++ b/tests/module/reuqire-more-rules-3.i.out @@ -1,9 +1,9 @@ -net_from_port (zero₁)-value! end -net_from_port (add1₄)-value! +netFromPort (zero₁)-value! end +netFromPort (add1₄)-value! (add1₄)-prev value-(add1₂) (add1₂)-prev value-(zero₃) end -net_from_port (add1₉)-value! +netFromPort (add1₉)-value! (add1₉)-prev value-(add1₁₀) (add1₁₀)-prev value-(add1₆) (add1₆)-prev value-(add1₅) diff --git a/tests/statement/compose.i.out b/tests/statement/compose.i.out index 232d5709..46a27661 100644 --- a/tests/statement/compose.i.out +++ b/tests/statement/compose.i.out @@ -1,8 +1,8 @@ -net_from_port (add1₃)-value! +netFromPort (add1₃)-value! (add1₃)-prev value-(add1₂) (add1₂)-prev value-(zero₁) end -net_from_port (add1₃)-value! +netFromPort (add1₃)-value! (add1₃)-prev value-(add1₂) (add1₂)-prev value-(zero₁) end diff --git a/tests/value/input-and-output-placeholders.i.out b/tests/value/input-and-output-placeholders.i.out index 1bb40d2f..638b6918 100644 --- a/tests/value/input-and-output-placeholders.i.out +++ b/tests/value/input-and-output-placeholders.i.out @@ -1,6 +1,6 @@ -net_from_port (@input_port_cap₂)-covering end -net_from_port (@ouput_port_cap₁)-covering end -net_from_port (add₃)-return +netFromPort (@inputPortCap₂)-covering end +netFromPort (@ouputPortCap₁)-covering end +netFromPort (add₃)-return (add₃)-target!value-(add1₃) (add₃)-addend value-(add1₂) (add1₃)-prev value-(zero₂)