From ffcd2eea75760a679980ae50d9897c8ed0a2f057 Mon Sep 17 00:00:00 2001 From: Xie Yuheng Date: Fri, 1 Nov 2024 15:28:27 +0800 Subject: [PATCH] up --- README.md | 4 ++-- docs/articles/programming-with-interaction-nets.md | 10 +++++----- ...345\272\224\347\275\221\347\274\226\347\250\213.md" | 10 +++++----- src/command-line/commands/Run.ts | 2 +- 4 files changed, 13 insertions(+), 13 deletions(-) diff --git a/README.md b/README.md index 7e5dc16f..be361cdf 100644 --- a/README.md +++ b/README.md @@ -138,7 +138,7 @@ eval @inspect(sixSoles()) [ [Goto The Playground](https://inet.xieyuheng.com/playground/aW1wb3J0IHsgTGlzdCB9IGZyb20gImh0dHBzOi8vY29kZS1vZi1pbmV0LWpzLmZpZGIuYXBwL3N0ZC9kYXRhdHlwZS9MaXN0LmkiCgovLyBDb25jYXRlbmF0aW9uIG9mIGxpc3RzIGlzIHBlcmZvcm1lZCBpbiBsaW5lYXIgdGltZQovLyB3aXRoIHJlc3BlY3QgdG8gaXRzIGZpcnN0IGFyZ3VtZW50LgovLyBDb25zdGFudCB0aW1lIGNvbmNhdGVuYXRpb24gaXMgcG9zc2libGUKLy8gd2l0aCBkaWZmZXJlbmNlLWxpc3RzOiB0aGUgaWRlYSBjb25zaXN0cyBpbgovLyBwbHVnZ2luZyB0aGUgZnJvbnQgb2YgdGhlIHNlY29uZCBhcmd1bWVudAovLyBhdCB0aGUgYmFjayBvZiB0aGUgZmlyc3Qgb25lLgoKdHlwZSBEaWZmTGlzdChFbGVtZW50OiBAVHlwZSkKCm5vZGUgZGlmZigKICBmcm9udDogTGlzdCgnQSksCiAgLS0tLS0tLQogIGJhY2s6IExpc3QoJ0EpLAogIHZhbHVlITogRGlmZkxpc3QoJ0EpLAopCgpub2RlIGRpZmZBcHBlbmQoCiAgdGFyZ2V0ITogRGlmZkxpc3QoJ0EpLAogIHJlc3Q6IERpZmZMaXN0KCdBKQogIC0tLS0tLS0tCiAgcmVzdWx0OiBEaWZmTGlzdCgnQSkKKQoKbm9kZSBkaWZmT3BlbigKICB0YXJnZXQhOiBEaWZmTGlzdCgnQSksCiAgbmV3QmFjazogTGlzdCgnQSkKICAtLS0tLS0tLS0tCiAgb2xkQmFjazogTGlzdCgnQSkKKQoKcnVsZSBkaWZmQXBwZW5kKHRhcmdldCEsIHJlc3QsIHJlc3VsdCkKICAgICBkaWZmKGZyb250LCBiYWNrLCB2YWx1ZSEpIHsKICBsZXQgbmV3QmFjaywgdmFsdWUgPSBkaWZmKGZyb250KQogIEBjb25uZWN0KHZhbHVlLCByZXN1bHQpCiAgZGlmZk9wZW4ocmVzdCwgbmV3QmFjaywgYmFjaykKfQoKcnVsZSBkaWZmT3Blbih0YXJnZXQhLCBuZXdCYWNrLCBvbGRCYWNrKQogICAgIGRpZmYoZnJvbnQsIGJhY2ssIHZhbHVlISkgewogIEBjb25uZWN0KGJhY2ssIG5ld0JhY2spCiAgQGNvbm5lY3QoZnJvbnQsIG9sZEJhY2spCn0KCi8vIFRFU1QKCmltcG9ydCB7IGNvbnMgfSBmcm9tICJodHRwczovL2NvZGUtb2YtaW5ldC1qcy5maWRiLmFwcC9zdGQvZGF0YXR5cGUvTGlzdC5pIgoKdHlwZSBUcml2aWFsCgpub2RlIHNvbGUoLS0gdmFsdWUhOiBUcml2aWFsKQoKZnVuY3Rpb24gdHdvVHdvU29sZXMoKTogRGlmZkxpc3QoVHJpdmlhbCkgewogIGxldCBmcm9udCwgYmFjaywgdmFsdWUxID0gZGlmZigpCiAgQGNvbm5lY3QoZnJvbnQsIGNvbnMoc29sZSgpLCBjb25zKHNvbGUoKSwgYmFjaykpKQogIGxldCBmcm9udCwgYmFjaywgdmFsdWUyID0gZGlmZigpCiAgQGNvbm5lY3QoZnJvbnQsIGNvbnMoc29sZSgpLCBjb25zKHNvbGUoKSwgYmFjaykpKQogIHJldHVybiBkaWZmQXBwZW5kKHZhbHVlMSwgdmFsdWUyKQp9CgpldmFsIEBpbnNwZWN0KEBydW4odHdvVHdvU29sZXMoKSkpCmV2YWwgQGluc3BlY3QodHdvVHdvU29sZXMoKSk) ] ```inet -import { List } from "https://code-of-inet-js.fidb.app/std/datatype/List.i" +import { List } from "https://code-of-inet-js.xieyuheng.com/std/datatype/List.i" // Concatenation of lists is performed in linear time // with respect to its first argument. @@ -185,7 +185,7 @@ rule diffOpen(target!, newBack, oldBack) // TEST -import { cons } from "https://code-of-inet-js.fidb.app/std/datatype/List.i" +import { cons } from "https://code-of-inet-js.xieyuheng.com/std/datatype/List.i" type Trivial diff --git a/docs/articles/programming-with-interaction-nets.md b/docs/articles/programming-with-interaction-nets.md index 04737dcb..25f5395f 100644 --- a/docs/articles/programming-with-interaction-nets.md +++ b/docs/articles/programming-with-interaction-nets.md @@ -683,7 +683,7 @@ to import definitions from other module. import { Nat, zero, add1, add, one, two, three, -} from "https://code-of-inet-js.fidb.app/std/datatype/Nat.i" +} from "https://code-of-inet-js.xieyuheng.com/std/datatype/Nat.i" node natErase( target!: Nat @@ -794,7 +794,7 @@ rule append(target!, rest, result) cons(head, tail, value!) { cons(head, append(tail, rest), result) } -import { Nat, zero } from "https://code-of-inet-js.fidb.app/std/datatype/Nat.i" +import { Nat, zero } from "https://code-of-inet-js.xieyuheng.com/std/datatype/Nat.i" function sixZeros(): List(Nat) { return append( @@ -836,7 +836,7 @@ the relationship between all nodes is symmetric. [Goto the playground of `DiffList` and `(diffAppend)`](https://inet.xieyuheng.com/playground/aW1wb3J0IHsgTGlzdCB9IGZyb20gImh0dHBzOi8vY29kZS1vZi1pbmV0LWpzLmZpZGIuYXBwL3N0ZC9kYXRhdHlwZS9MaXN0LmkiCgp0eXBlIERpZmZMaXN0KEVsZW1lbnQ6IEBUeXBlKQoKbm9kZSBkaWZmKAogIGZyb250OiBMaXN0KCdBKSwKICAtLS0tLS0tCiAgYmFjazogTGlzdCgnQSksCiAgdmFsdWUhOiBEaWZmTGlzdCgnQSksCikKCm5vZGUgZGlmZkFwcGVuZCgKICB0YXJnZXQhOiBEaWZmTGlzdCgnQSksCiAgcmVzdDogRGlmZkxpc3QoJ0EpCiAgLS0tLS0tLS0KICByZXN1bHQ6IERpZmZMaXN0KCdBKQopCgpub2RlIGRpZmZPcGVuKAogIHRhcmdldCE6IERpZmZMaXN0KCdBKSwKICBuZXdCYWNrOiBMaXN0KCdBKQogIC0tLS0tLS0tLS0KICBvbGRCYWNrOiBMaXN0KCdBKQopCgpydWxlIGRpZmZBcHBlbmQodGFyZ2V0ISwgcmVzdCwgcmVzdWx0KQogICAgIGRpZmYoZnJvbnQsIGJhY2ssIHZhbHVlISkgewogIGxldCBuZXdCYWNrLCB2YWx1ZSA9IGRpZmYoZnJvbnQpCiAgQGNvbm5lY3QodmFsdWUsIHJlc3VsdCkKICBkaWZmT3BlbihyZXN0LCBuZXdCYWNrLCBiYWNrKQp9CgpydWxlIGRpZmZPcGVuKHRhcmdldCEsIG5ld0JhY2ssIG9sZEJhY2spCiAgICAgZGlmZihmcm9udCwgYmFjaywgdmFsdWUhKSB7CiAgQGNvbm5lY3QoYmFjaywgbmV3QmFjaykKICBAY29ubmVjdChmcm9udCwgb2xkQmFjaykKfQoKaW1wb3J0IHsgTmF0LCB6ZXJvIH0gZnJvbSAiaHR0cHM6Ly9jb2RlLW9mLWluZXQtanMuZmlkYi5hcHAvc3RkL2RhdGF0eXBlL05hdC5pIgppbXBvcnQgeyBjb25zIH0gZnJvbSAiaHR0cHM6Ly9jb2RlLW9mLWluZXQtanMuZmlkYi5hcHAvc3RkL2RhdGF0eXBlL0xpc3QuaSIKCmZ1bmN0aW9uIHR3b1R3b1plcm9zKCk6IERpZmZMaXN0KE5hdCkgewogIGxldCBmcm9udCwgYmFjaywgdmFsdWUxID0gZGlmZigpCiAgQGNvbm5lY3QoZnJvbnQsIGNvbnMoemVybygpLCBjb25zKHplcm8oKSwgYmFjaykpKQogIGxldCBmcm9udCwgYmFjaywgdmFsdWUyID0gZGlmZigpCiAgQGNvbm5lY3QoZnJvbnQsIGNvbnMoemVybygpLCBjb25zKHplcm8oKSwgYmFjaykpKQogIHJldHVybiBkaWZmQXBwZW5kKHZhbHVlMSwgdmFsdWUyKQp9CgpldmFsIHR3b1R3b1plcm9zKCk) ``` -import { List } from "https://code-of-inet-js.fidb.app/std/datatype/List.i" +import { List } from "https://code-of-inet-js.xieyuheng.com/std/datatype/List.i" type DiffList(Element: @Type) @@ -874,8 +874,8 @@ rule diffOpen(target!, newBack, oldBack) @connect(front, oldBack) } -import { Nat, zero } from "https://code-of-inet-js.fidb.app/std/datatype/Nat.i" -import { cons } from "https://code-of-inet-js.fidb.app/std/datatype/List.i" +import { Nat, zero } from "https://code-of-inet-js.xieyuheng.com/std/datatype/Nat.i" +import { cons } from "https://code-of-inet-js.xieyuheng.com/std/datatype/List.i" function twoTwoZeros(): DiffList(Nat) { let front, back, value1 = diff() 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 5905d63a..200db4fd 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" @@ -659,7 +659,7 @@ eval max(two(), three()) import { Nat, zero, add1, add, one, two, three, -} from "https://code-of-inet-js.fidb.app/std/datatype/Nat.i" +} from "https://code-of-inet-js.xieyuheng.com/std/datatype/Nat.i" node natErase( target!: Nat @@ -768,7 +768,7 @@ rule append(target!, rest, result) cons(head, tail, value!) { cons(head, append(tail, rest), result) } -import { Nat, zero } from "https://code-of-inet-js.fidb.app/std/datatype/Nat.i" +import { Nat, zero } from "https://code-of-inet-js.xieyuheng.com/std/datatype/Nat.i" function sixZeros(): List(Nat) { return append( @@ -806,7 +806,7 @@ eval sixZeros() [去 `DiffList` 与 `(diffAppend)` 的演算场](https://inet.xieyuheng.com/playground/aW1wb3J0IHsgTGlzdCB9IGZyb20gImh0dHBzOi8vY29kZS1vZi1pbmV0LWpzLmZpZGIuYXBwL3N0ZC9kYXRhdHlwZS9MaXN0LmkiCgp0eXBlIERpZmZMaXN0KEVsZW1lbnQ6IEBUeXBlKQoKbm9kZSBkaWZmKAogIGZyb250OiBMaXN0KCdBKSwKICAtLS0tLS0tCiAgYmFjazogTGlzdCgnQSksCiAgdmFsdWUhOiBEaWZmTGlzdCgnQSksCikKCm5vZGUgZGlmZkFwcGVuZCgKICB0YXJnZXQhOiBEaWZmTGlzdCgnQSksCiAgcmVzdDogRGlmZkxpc3QoJ0EpCiAgLS0tLS0tLS0KICByZXN1bHQ6IERpZmZMaXN0KCdBKQopCgpub2RlIGRpZmZPcGVuKAogIHRhcmdldCE6IERpZmZMaXN0KCdBKSwKICBuZXdCYWNrOiBMaXN0KCdBKQogIC0tLS0tLS0tLS0KICBvbGRCYWNrOiBMaXN0KCdBKQopCgpydWxlIGRpZmZBcHBlbmQodGFyZ2V0ISwgcmVzdCwgcmVzdWx0KQogICAgIGRpZmYoZnJvbnQsIGJhY2ssIHZhbHVlISkgewogIGxldCBuZXdCYWNrLCB2YWx1ZSA9IGRpZmYoZnJvbnQpCiAgQGNvbm5lY3QodmFsdWUsIHJlc3VsdCkKICBkaWZmT3BlbihyZXN0LCBuZXdCYWNrLCBiYWNrKQp9CgpydWxlIGRpZmZPcGVuKHRhcmdldCEsIG5ld0JhY2ssIG9sZEJhY2spCiAgICAgZGlmZihmcm9udCwgYmFjaywgdmFsdWUhKSB7CiAgQGNvbm5lY3QoYmFjaywgbmV3QmFjaykKICBAY29ubmVjdChmcm9udCwgb2xkQmFjaykKfQoKaW1wb3J0IHsgTmF0LCB6ZXJvIH0gZnJvbSAiaHR0cHM6Ly9jb2RlLW9mLWluZXQtanMuZmlkYi5hcHAvc3RkL2RhdGF0eXBlL05hdC5pIgppbXBvcnQgeyBjb25zIH0gZnJvbSAiaHR0cHM6Ly9jb2RlLW9mLWluZXQtanMuZmlkYi5hcHAvc3RkL2RhdGF0eXBlL0xpc3QuaSIKCmZ1bmN0aW9uIHR3b1R3b1plcm9zKCk6IERpZmZMaXN0KE5hdCkgewogIGxldCBmcm9udCwgYmFjaywgdmFsdWUxID0gZGlmZigpCiAgQGNvbm5lY3QoZnJvbnQsIGNvbnMoemVybygpLCBjb25zKHplcm8oKSwgYmFjaykpKQogIGxldCBmcm9udCwgYmFjaywgdmFsdWUyID0gZGlmZigpCiAgQGNvbm5lY3QoZnJvbnQsIGNvbnMoemVybygpLCBjb25zKHplcm8oKSwgYmFjaykpKQogIHJldHVybiBkaWZmQXBwZW5kKHZhbHVlMSwgdmFsdWUyKQp9CgpldmFsIHR3b1R3b1plcm9zKCk) ``` -import { List } from "https://code-of-inet-js.fidb.app/std/datatype/List.i" +import { List } from "https://code-of-inet-js.xieyuheng.com/std/datatype/List.i" type DiffList(Element: @Type) @@ -844,8 +844,8 @@ rule diffOpen(target!, newBack, oldBack) @connect(front, oldBack) } -import { Nat, zero } from "https://code-of-inet-js.fidb.app/std/datatype/Nat.i" -import { cons } from "https://code-of-inet-js.fidb.app/std/datatype/List.i" +import { Nat, zero } from "https://code-of-inet-js.xieyuheng.com/std/datatype/Nat.i" +import { cons } from "https://code-of-inet-js.xieyuheng.com/std/datatype/List.i" function twoTwoZeros(): DiffList(Nat) { let front, back, value1 = diff() diff --git a/src/command-line/commands/Run.ts b/src/command-line/commands/Run.ts index 0f165533..8f10cf5e 100644 --- a/src/command-line/commands/Run.ts +++ b/src/command-line/commands/Run.ts @@ -30,7 +30,7 @@ export class Run extends Command { ``, `Run a URL:`, ``, - blue(` ${runner.name} ${this.name} https://code-of-inet.fidb.app/std/datatype/Nat.test.i`), + blue(` ${runner.name} ${this.name} https://code-of-inet.xieyuheng.com/std/datatype/Nat.test.i`), ``, ].join("\n")