Compare commits
2 commits
| Author | SHA1 | Date | |
|---|---|---|---|
| 54928688cd | |||
| 18fe764992 |
19 changed files with 815 additions and 769 deletions
4
.gitignore
vendored
4
.gitignore
vendored
|
|
@ -1,3 +1 @@
|
|||
.stack-work/
|
||||
*~
|
||||
client_session_key.aes
|
||||
/target
|
||||
|
|
|
|||
792
Cargo.lock
generated
Normal file
792
Cargo.lock
generated
Normal file
|
|
@ -0,0 +1,792 @@
|
|||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
[[package]]
|
||||
name = "aead"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4cf01b9b56e767bb57b94ebf91a58b338002963785cdd7013e21c0d4679471e4"
|
||||
dependencies = [
|
||||
"generic-array",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "aes"
|
||||
version = "0.3.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "54eb1d8fe354e5fc611daf4f2ea97dd45a765f4f1e4512306ec183ae2e8f20c9"
|
||||
dependencies = [
|
||||
"aes-soft",
|
||||
"aesni",
|
||||
"block-cipher-trait",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "aes-gcm"
|
||||
version = "0.5.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "834a6bda386024dbb7c8fc51322856c10ffe69559f972261c868485f5759c638"
|
||||
dependencies = [
|
||||
"aead",
|
||||
"aes",
|
||||
"block-cipher-trait",
|
||||
"ghash",
|
||||
"subtle 2.3.0",
|
||||
"zeroize",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "aes-soft"
|
||||
version = "0.3.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cfd7e7ae3f9a1fb5c03b389fc6bb9a51400d0c13053f0dca698c832bfd893a0d"
|
||||
dependencies = [
|
||||
"block-cipher-trait",
|
||||
"byteorder",
|
||||
"opaque-debug",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "aesni"
|
||||
version = "0.6.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2f70a6b5f971e473091ab7cfb5ffac6cde81666c4556751d8d5620ead8abf100"
|
||||
dependencies = [
|
||||
"block-cipher-trait",
|
||||
"opaque-debug",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "atty"
|
||||
version = "0.2.14"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8"
|
||||
dependencies = [
|
||||
"hermit-abi",
|
||||
"libc",
|
||||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "autocfg"
|
||||
version = "1.0.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a"
|
||||
|
||||
[[package]]
|
||||
name = "base64"
|
||||
version = "0.9.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "489d6c0ed21b11d038c31b6ceccca973e65d73ba3bd8ecb9a2babf5546164643"
|
||||
dependencies = [
|
||||
"byteorder",
|
||||
"safemem",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "base64"
|
||||
version = "0.12.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3441f0f7b02788e948e47f457ca01f1d7e6d92c693bc132c22b087d3141c03ff"
|
||||
|
||||
[[package]]
|
||||
name = "bitflags"
|
||||
version = "1.2.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693"
|
||||
|
||||
[[package]]
|
||||
name = "block-buffer"
|
||||
version = "0.7.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c0940dc441f31689269e10ac70eb1002a3a1d3ad1390e030043662eb7fe4688b"
|
||||
dependencies = [
|
||||
"block-padding",
|
||||
"byte-tools",
|
||||
"byteorder",
|
||||
"generic-array",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "block-cipher-trait"
|
||||
version = "0.6.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1c924d49bd09e7c06003acda26cd9742e796e34282ec6c1189404dee0c1f4774"
|
||||
dependencies = [
|
||||
"generic-array",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "block-padding"
|
||||
version = "0.1.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fa79dedbb091f449f1f39e53edf88d5dbe95f895dae6135a8d7b881fb5af73f5"
|
||||
dependencies = [
|
||||
"byte-tools",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "byte-tools"
|
||||
version = "0.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e3b5ca7a04898ad4bcd41c90c5285445ff5b791899bb1b0abdd2a2aa791211d7"
|
||||
|
||||
[[package]]
|
||||
name = "byteorder"
|
||||
version = "1.3.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "08c48aae112d48ed9f069b33538ea9e3e90aa263cfa3d1c24309612b1f7472de"
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
version = "0.1.10"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4785bdd1c96b2a846b2bd7cc02e86b6b3dbf14e7e53446c4f54c92a361040822"
|
||||
|
||||
[[package]]
|
||||
name = "cookie"
|
||||
version = "0.11.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5795cda0897252e34380a27baf884c53aa7ad9990329cdad96d4c5d027015d44"
|
||||
dependencies = [
|
||||
"aes-gcm",
|
||||
"base64 0.12.3",
|
||||
"hkdf",
|
||||
"hmac",
|
||||
"percent-encoding 2.1.0",
|
||||
"rand",
|
||||
"sha2",
|
||||
"time",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "crypto-mac"
|
||||
version = "0.7.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4434400df11d95d556bac068ddfedd482915eb18fe8bea89bc80b6e4b1c179e5"
|
||||
dependencies = [
|
||||
"generic-array",
|
||||
"subtle 1.0.0",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "devise"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "74e04ba2d03c5fa0d954c061fc8c9c288badadffc272ebb87679a89846de3ed3"
|
||||
dependencies = [
|
||||
"devise_codegen",
|
||||
"devise_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "devise_codegen"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "066ceb7928ca93a9bedc6d0e612a8a0424048b0ab1f75971b203d01420c055d7"
|
||||
dependencies = [
|
||||
"devise_core",
|
||||
"quote",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "devise_core"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cf41c59b22b5e3ec0ea55c7847e5f358d340f3a8d6d53a5cf4f1564967f96487"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "digest"
|
||||
version = "0.8.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f3d0c8c8752312f9713efd397ff63acb9f85585afbf179282e720e7704954dd5"
|
||||
dependencies = [
|
||||
"generic-array",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "fake-simd"
|
||||
version = "0.1.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e88a8acf291dafb59c2d96e8f59828f3838bb1a70398823ade51a84de6a6deed"
|
||||
|
||||
[[package]]
|
||||
name = "generic-array"
|
||||
version = "0.12.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c68f0274ae0e023facc3c97b2e00f076be70e254bc851d972503b328db79b2ec"
|
||||
dependencies = [
|
||||
"typenum",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "getrandom"
|
||||
version = "0.1.15"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fc587bc0ec293155d5bfa6b9891ec18a1e330c234f896ea47fbada4cadbe47e6"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"libc",
|
||||
"wasi 0.9.0+wasi-snapshot-preview1",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ghash"
|
||||
version = "0.2.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9f0930ed19a7184089ea46d2fedead2f6dc2b674c5db4276b7da336c7cd83252"
|
||||
dependencies = [
|
||||
"polyval",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "glob"
|
||||
version = "0.3.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9b919933a397b79c37e33b77bb2aa3dc8eb6e165ad809e58ff75bc7db2e34574"
|
||||
|
||||
[[package]]
|
||||
name = "hashbrown"
|
||||
version = "0.9.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d7afe4a420e3fe79967a00898cc1f4db7c8a49a9333a29f8a4bd76a253d5cd04"
|
||||
|
||||
[[package]]
|
||||
name = "hermit-abi"
|
||||
version = "0.1.17"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5aca5565f760fb5b220e499d72710ed156fdb74e631659e99377d9ebfbd13ae8"
|
||||
dependencies = [
|
||||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "hkdf"
|
||||
version = "0.8.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3fa08a006102488bd9cd5b8013aabe84955cf5ae22e304c2caf655b633aefae3"
|
||||
dependencies = [
|
||||
"digest",
|
||||
"hmac",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "hmac"
|
||||
version = "0.7.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5dcb5e64cda4c23119ab41ba960d1e170a774c8e4b9d9e6a9bc18aabf5e59695"
|
||||
dependencies = [
|
||||
"crypto-mac",
|
||||
"digest",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "httparse"
|
||||
version = "1.3.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cd179ae861f0c2e53da70d892f5f3029f9594be0c41dc5269cd371691b1dc2f9"
|
||||
|
||||
[[package]]
|
||||
name = "hyper"
|
||||
version = "0.10.16"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0a0652d9a2609a968c14be1a9ea00bf4b1d64e2e1f53a1b51b6fff3a6e829273"
|
||||
dependencies = [
|
||||
"base64 0.9.3",
|
||||
"httparse",
|
||||
"language-tags",
|
||||
"log 0.3.9",
|
||||
"mime",
|
||||
"num_cpus",
|
||||
"time",
|
||||
"traitobject",
|
||||
"typeable",
|
||||
"unicase",
|
||||
"url",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "idna"
|
||||
version = "0.1.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "38f09e0f0b1fb55fdee1f17470ad800da77af5186a1a76c026b679358b7e844e"
|
||||
dependencies = [
|
||||
"matches",
|
||||
"unicode-bidi",
|
||||
"unicode-normalization",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "indexmap"
|
||||
version = "1.6.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "55e2e4c765aa53a0424761bf9f41aa7a6ac1efa87238f59560640e27fca028f2"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"hashbrown",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "language-tags"
|
||||
version = "0.2.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a91d884b6667cd606bb5a69aa0c99ba811a115fc68915e7056ec08a46e93199a"
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.80"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4d58d1b70b004888f764dfbf6a26a3b0342a1632d33968e4a179d8011c760614"
|
||||
|
||||
[[package]]
|
||||
name = "log"
|
||||
version = "0.3.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e19e8d5c34a3e0e2223db8e060f9e8264aeeb5c5fc64a4ee9965c062211c024b"
|
||||
dependencies = [
|
||||
"log 0.4.11",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "log"
|
||||
version = "0.4.11"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4fabed175da42fed1fa0746b0ea71f412aa9d35e76e95e59b192c64b9dc2bf8b"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "matches"
|
||||
version = "0.1.8"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7ffc5c5338469d4d3ea17d269fa8ea3512ad247247c30bd2df69e68309ed0a08"
|
||||
|
||||
[[package]]
|
||||
name = "memchr"
|
||||
version = "2.3.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0ee1c47aaa256ecabcaea351eae4a9b01ef39ed810004e298d2511ed284b1525"
|
||||
|
||||
[[package]]
|
||||
name = "mime"
|
||||
version = "0.2.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ba626b8a6de5da682e1caa06bdb42a335aee5a84db8e5046a3e8ab17ba0a3ae0"
|
||||
dependencies = [
|
||||
"log 0.3.9",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num_cpus"
|
||||
version = "1.13.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "05499f3756671c15885fee9034446956fff3f243d6077b91e5767df161f766b3"
|
||||
dependencies = [
|
||||
"hermit-abi",
|
||||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "opaque-debug"
|
||||
version = "0.2.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2839e79665f131bdb5782e51f2c6c9599c133c6098982a54c794358bf432529c"
|
||||
|
||||
[[package]]
|
||||
name = "pear"
|
||||
version = "0.1.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5320f212db967792b67cfe12bd469d08afd6318a249bd917d5c19bc92200ab8a"
|
||||
dependencies = [
|
||||
"pear_codegen",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "pear_codegen"
|
||||
version = "0.1.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bfc1c836fdc3d1ef87c348b237b5b5c4dff922156fb2d968f57734f9669768ca"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
"version_check 0.9.2",
|
||||
"yansi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "percent-encoding"
|
||||
version = "1.0.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "31010dd2e1ac33d5b46a5b413495239882813e0369f8ed8a5e266f173602f831"
|
||||
|
||||
[[package]]
|
||||
name = "percent-encoding"
|
||||
version = "2.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d4fd5641d01c8f18a23da7b6fe29298ff4b55afcccdf78973b24cf3175fee32e"
|
||||
|
||||
[[package]]
|
||||
name = "polyval"
|
||||
version = "0.3.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7ec3341498978de3bfd12d1b22f1af1de22818f5473a11e8a6ef997989e3a212"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"universal-hash",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ppv-lite86"
|
||||
version = "0.2.10"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ac74c624d6b2d21f425f752262f42188365d7b8ff1aff74c82e45136510a4857"
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro2"
|
||||
version = "0.4.30"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759"
|
||||
dependencies = [
|
||||
"unicode-xid",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "props"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"rocket",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "quote"
|
||||
version = "0.6.13"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand"
|
||||
version = "0.7.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6a6b1679d49b24bbfe0c803429aa1874472f50d9b363131f0e89fc356b544d03"
|
||||
dependencies = [
|
||||
"getrandom",
|
||||
"libc",
|
||||
"rand_chacha",
|
||||
"rand_core",
|
||||
"rand_hc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_chacha"
|
||||
version = "0.2.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f4c8ed856279c9737206bf725bf36935d8666ead7aa69b52be55af369d193402"
|
||||
dependencies = [
|
||||
"ppv-lite86",
|
||||
"rand_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_core"
|
||||
version = "0.5.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "90bde5296fc891b0cef12a6d03ddccc162ce7b2aff54160af9338f8d40df6d19"
|
||||
dependencies = [
|
||||
"getrandom",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_hc"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ca3129af7b92a17112d59ad498c6f81eaf463253766b90396d39ea7a39d6613c"
|
||||
dependencies = [
|
||||
"rand_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rocket"
|
||||
version = "0.4.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4fc7e5d6aaa32ace6893ae8a1875688ca7b07d6c2428ae88e704c3623c8866e9"
|
||||
dependencies = [
|
||||
"atty",
|
||||
"base64 0.12.3",
|
||||
"log 0.4.11",
|
||||
"memchr",
|
||||
"num_cpus",
|
||||
"pear",
|
||||
"rocket_codegen",
|
||||
"rocket_http",
|
||||
"state",
|
||||
"time",
|
||||
"toml",
|
||||
"version_check 0.9.2",
|
||||
"yansi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rocket_codegen"
|
||||
version = "0.4.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "519154b16df5fe552a8f9cd76a97793a9f5d58e34f186ab79c7b29ce1d009358"
|
||||
dependencies = [
|
||||
"devise",
|
||||
"glob",
|
||||
"indexmap",
|
||||
"quote",
|
||||
"rocket_http",
|
||||
"version_check 0.9.2",
|
||||
"yansi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rocket_http"
|
||||
version = "0.4.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a9d087de7203c7a60a0ed5cd3a135b552dbfbed9932c52d49d083e8629935257"
|
||||
dependencies = [
|
||||
"cookie",
|
||||
"hyper",
|
||||
"indexmap",
|
||||
"pear",
|
||||
"percent-encoding 1.0.1",
|
||||
"smallvec",
|
||||
"state",
|
||||
"time",
|
||||
"unicode-xid",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "safemem"
|
||||
version = "0.3.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ef703b7cb59335eae2eb93ceb664c0eb7ea6bf567079d843e09420219668e072"
|
||||
|
||||
[[package]]
|
||||
name = "serde"
|
||||
version = "1.0.117"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b88fa983de7720629c9387e9f517353ed404164b1e482c970a90c1a4aaf7dc1a"
|
||||
|
||||
[[package]]
|
||||
name = "sha2"
|
||||
version = "0.8.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a256f46ea78a0c0d9ff00077504903ac881a1dafdc20da66545699e7776b3e69"
|
||||
dependencies = [
|
||||
"block-buffer",
|
||||
"digest",
|
||||
"fake-simd",
|
||||
"opaque-debug",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "smallvec"
|
||||
version = "1.5.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7acad6f34eb9e8a259d3283d1e8c1d34d7415943d4895f65cc73813c7396fc85"
|
||||
|
||||
[[package]]
|
||||
name = "state"
|
||||
version = "0.4.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3015a7d0a5fd5105c91c3710d42f9ccf0abfb287d62206484dcc67f9569a6483"
|
||||
|
||||
[[package]]
|
||||
name = "subtle"
|
||||
version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2d67a5a62ba6e01cb2192ff309324cb4875d0c451d55fe2319433abe7a05a8ee"
|
||||
|
||||
[[package]]
|
||||
name = "subtle"
|
||||
version = "2.3.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "343f3f510c2915908f155e94f17220b19ccfacf2a64a2a5d8004f2c3e311e7fd"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "0.15.44"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"unicode-xid",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "time"
|
||||
version = "0.1.44"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6db9e6914ab8b1ae1c260a4ae7a49b6c5611b40328a735b21862567685e73255"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"wasi 0.10.0+wasi-snapshot-preview1",
|
||||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "tinyvec"
|
||||
version = "1.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ccf8dbc19eb42fba10e8feaaec282fb50e2c14b2726d6301dbfeed0f73306a6f"
|
||||
dependencies = [
|
||||
"tinyvec_macros",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "tinyvec_macros"
|
||||
version = "0.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cda74da7e1a664f795bb1f8a87ec406fb89a02522cf6e50620d016add6dbbf5c"
|
||||
|
||||
[[package]]
|
||||
name = "toml"
|
||||
version = "0.4.10"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "758664fc71a3a69038656bee8b6be6477d2a6c315a6b81f7081f591bffa4111f"
|
||||
dependencies = [
|
||||
"serde",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "traitobject"
|
||||
version = "0.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "efd1f82c56340fdf16f2a953d7bda4f8fdffba13d93b00844c25572110b26079"
|
||||
|
||||
[[package]]
|
||||
name = "typeable"
|
||||
version = "0.1.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1410f6f91f21d1612654e7cc69193b0334f909dcf2c790c4826254fbb86f8887"
|
||||
|
||||
[[package]]
|
||||
name = "typenum"
|
||||
version = "1.12.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "373c8a200f9e67a0c95e62a4f52fbf80c23b4381c05a17845531982fa99e6b33"
|
||||
|
||||
[[package]]
|
||||
name = "unicase"
|
||||
version = "1.4.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7f4765f83163b74f957c797ad9253caf97f103fb064d3999aea9568d09fc8a33"
|
||||
dependencies = [
|
||||
"version_check 0.1.5",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "unicode-bidi"
|
||||
version = "0.3.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "49f2bd0c6468a8230e1db229cff8029217cf623c767ea5d60bfbd42729ea54d5"
|
||||
dependencies = [
|
||||
"matches",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "unicode-normalization"
|
||||
version = "0.1.16"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a13e63ab62dbe32aeee58d1c5408d35c36c392bba5d9d3142287219721afe606"
|
||||
dependencies = [
|
||||
"tinyvec",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "unicode-xid"
|
||||
version = "0.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc"
|
||||
|
||||
[[package]]
|
||||
name = "universal-hash"
|
||||
version = "0.3.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "df0c900f2f9b4116803415878ff48b63da9edb268668e08cf9292d7503114a01"
|
||||
dependencies = [
|
||||
"generic-array",
|
||||
"subtle 2.3.0",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "url"
|
||||
version = "1.7.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "dd4e7c0d531266369519a4aa4f399d748bd37043b00bde1e4ff1f60a120b355a"
|
||||
dependencies = [
|
||||
"idna",
|
||||
"matches",
|
||||
"percent-encoding 1.0.1",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "version_check"
|
||||
version = "0.1.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "914b1a6776c4c929a602fafd8bc742e06365d4bcbe48c30f9cca5824f70dc9dd"
|
||||
|
||||
[[package]]
|
||||
name = "version_check"
|
||||
version = "0.9.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b5a972e5669d67ba988ce3dc826706fb0a8b01471c088cb0b6110b805cc36aed"
|
||||
|
||||
[[package]]
|
||||
name = "wasi"
|
||||
version = "0.9.0+wasi-snapshot-preview1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cccddf32554fecc6acb585f82a32a72e28b48f8c4c1883ddfeeeaa96f7d8e519"
|
||||
|
||||
[[package]]
|
||||
name = "wasi"
|
||||
version = "0.10.0+wasi-snapshot-preview1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1a143597ca7c7793eff794def352d41792a93c481eb1042423ff7ff72ba2c31f"
|
||||
|
||||
[[package]]
|
||||
name = "winapi"
|
||||
version = "0.3.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
|
||||
dependencies = [
|
||||
"winapi-i686-pc-windows-gnu",
|
||||
"winapi-x86_64-pc-windows-gnu",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "winapi-i686-pc-windows-gnu"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
|
||||
|
||||
[[package]]
|
||||
name = "winapi-x86_64-pc-windows-gnu"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
|
||||
|
||||
[[package]]
|
||||
name = "yansi"
|
||||
version = "0.5.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9fc79f4a1e39857fc00c3f662cbf2651c771f00e9c15fe2abc341806bd46bd71"
|
||||
|
||||
[[package]]
|
||||
name = "zeroize"
|
||||
version = "1.1.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "05f33972566adbd2d3588b0491eb94b98b43695c4ef897903470ede4f3f5a28a"
|
||||
8
Cargo.toml
Normal file
8
Cargo.toml
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
[package]
|
||||
name = "props"
|
||||
version = "0.1.0"
|
||||
authors = ["Joscha <joscha@plugh.de>"]
|
||||
edition = "2018"
|
||||
|
||||
[dependencies]
|
||||
rocket = "0.4.6"
|
||||
18
LICENSE
18
LICENSE
|
|
@ -1,18 +0,0 @@
|
|||
Copyright (c) 2020 Garmelon
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of
|
||||
this software and associated documentation files (the "Software"), to deal in
|
||||
the Software without restriction, including without limitation the rights to
|
||||
use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
|
||||
the Software, and to permit persons to whom the Software is furnished to do so,
|
||||
subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all
|
||||
copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
|
||||
FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
|
||||
COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
|
||||
IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
|
||||
CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
|
|
@ -1,4 +1,3 @@
|
|||
# propa-tools
|
||||
# props
|
||||
|
||||
Various programming paradigm related bits and bobs. May not contain any actual
|
||||
executables.
|
||||
Propa tools
|
||||
|
|
|
|||
2
Setup.hs
2
Setup.hs
|
|
@ -1,2 +0,0 @@
|
|||
import Distribution.Simple
|
||||
main = defaultMain
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
module Main where
|
||||
|
||||
main :: IO ()
|
||||
main = putStrLn "Hello world!"
|
||||
34
package.yaml
34
package.yaml
|
|
@ -1,34 +0,0 @@
|
|||
name: propa-tools
|
||||
version: 0.1.0.0
|
||||
license: MIT
|
||||
author: Garmelon <joscha@plugh.de>
|
||||
copyright: 2020 Garmelon
|
||||
|
||||
extra-source-files:
|
||||
- README.md
|
||||
- LICENSE
|
||||
|
||||
extra-doc-files:
|
||||
- README.md
|
||||
|
||||
dependencies:
|
||||
- base >= 4.7 && < 5
|
||||
- containers
|
||||
- megaparsec
|
||||
- parser-combinators
|
||||
- text
|
||||
- transformers
|
||||
|
||||
library:
|
||||
source-dirs: src
|
||||
|
||||
executables:
|
||||
propa-tools-exe:
|
||||
main: Main.hs
|
||||
source-dirs: app
|
||||
ghc-options:
|
||||
- -threaded
|
||||
- -rtsopts
|
||||
- -with-rtsopts=-N
|
||||
dependencies:
|
||||
- propa-tools
|
||||
|
|
@ -1,58 +0,0 @@
|
|||
cabal-version: 1.18
|
||||
|
||||
-- This file has been generated from package.yaml by hpack version 0.34.2.
|
||||
--
|
||||
-- see: https://github.com/sol/hpack
|
||||
|
||||
name: propa-tools
|
||||
version: 0.1.0.0
|
||||
author: Garmelon <joscha@plugh.de>
|
||||
maintainer: Garmelon <joscha@plugh.de>
|
||||
copyright: 2020 Garmelon
|
||||
license: MIT
|
||||
license-file: LICENSE
|
||||
build-type: Simple
|
||||
extra-source-files:
|
||||
README.md
|
||||
LICENSE
|
||||
extra-doc-files:
|
||||
README.md
|
||||
|
||||
library
|
||||
exposed-modules:
|
||||
Propa.Lambda.Display
|
||||
Propa.Lambda.Term
|
||||
Propa.Prolog.Debug
|
||||
Propa.Prolog.Display
|
||||
Propa.Prolog.Parse
|
||||
Propa.Prolog.Types
|
||||
Propa.Prolog.Unify
|
||||
other-modules:
|
||||
Paths_propa_tools
|
||||
hs-source-dirs:
|
||||
src
|
||||
build-depends:
|
||||
base >=4.7 && <5
|
||||
, containers
|
||||
, megaparsec
|
||||
, parser-combinators
|
||||
, text
|
||||
, transformers
|
||||
default-language: Haskell2010
|
||||
|
||||
executable propa-tools-exe
|
||||
main-is: Main.hs
|
||||
other-modules:
|
||||
Paths_propa_tools
|
||||
hs-source-dirs:
|
||||
app
|
||||
ghc-options: -threaded -rtsopts -with-rtsopts=-N
|
||||
build-depends:
|
||||
base >=4.7 && <5
|
||||
, containers
|
||||
, megaparsec
|
||||
, parser-combinators
|
||||
, propa-tools
|
||||
, text
|
||||
, transformers
|
||||
default-language: Haskell2010
|
||||
|
|
@ -1,127 +0,0 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
-- | This module contains functions useful for displaying 'Term's.
|
||||
|
||||
module Propa.Lambda.Display
|
||||
( Name
|
||||
, findConstNames
|
||||
, makeVarNamesUnique
|
||||
, findVarNames
|
||||
, displayTerm
|
||||
, displayTerm'
|
||||
) where
|
||||
|
||||
import Data.Maybe
|
||||
import Numeric.Natural
|
||||
|
||||
import Control.Monad.Trans.State
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Text as T
|
||||
|
||||
import Propa.Lambda.Term
|
||||
|
||||
-- | The name of a variable or a constant.
|
||||
type Name = T.Text
|
||||
|
||||
varNames :: [Name]
|
||||
varNames = chars ++ (mappend <$> constNames <*> chars)
|
||||
where
|
||||
chars = map T.singleton ['a'..'z']
|
||||
|
||||
constNames :: [Name]
|
||||
constNames = chars ++ (mappend <$> constNames <*> chars)
|
||||
where
|
||||
chars = map T.singleton ['A'..'Z']
|
||||
|
||||
chooseUnique :: (Ord a) => Set.Set a -> [a] -> a
|
||||
chooseUnique taken = head . dropWhile (`Set.member` taken)
|
||||
|
||||
makeNameUnique :: Set.Set Name -> Name -> Name
|
||||
makeNameUnique taken name
|
||||
= chooseUnique taken
|
||||
$ zipWith (<>) (repeat name)
|
||||
$ "" : map (T.pack . show) [(2::Integer) ..]
|
||||
|
||||
-- | Find names for constants that don't overlap with existing constants. Every
|
||||
-- unnamed constant is assumed to be a different constant. This means that every
|
||||
-- unnamed constant will be assigned a unique name.
|
||||
--
|
||||
-- Names for constants follow the schema @A@, @B@, ... @AA@, @AB@, ...
|
||||
findConstNames :: Term e (Maybe Name) v -> Term e Name v
|
||||
findConstNames term = evalState (helper term) (Set.fromList $ catMaybes $ consts term)
|
||||
where
|
||||
helper (Var i) = pure $ Var i
|
||||
helper (Const c) = do
|
||||
taken <- get
|
||||
let name = fromMaybe (chooseUnique taken constNames) c
|
||||
put $ Set.insert name taken
|
||||
pure $ Const name
|
||||
helper (Lambda v t) = Lambda v <$> helper t
|
||||
helper (App l r) = App <$> helper l <*> helper r
|
||||
helper (Ext e) = pure $ Ext e
|
||||
|
||||
-- | Make names of existing variables unique. If the name is not already unique
|
||||
-- in the current scope, tries to make it unique by appending a number from
|
||||
-- @[2..]@.
|
||||
makeVarNamesUnique :: Term e Name (Maybe Name) -> Term e Name (Maybe Name)
|
||||
makeVarNamesUnique term = helper (Set.fromList $ consts term) term
|
||||
where
|
||||
helper _ (Var i) = Var i
|
||||
helper _ (Const c) = Const c
|
||||
helper taken (Lambda v t) = case v of
|
||||
Nothing -> Lambda Nothing $ helper taken t
|
||||
Just name ->
|
||||
let newName = makeNameUnique taken name
|
||||
in Lambda (Just newName) $ helper (Set.insert name taken) t
|
||||
helper taken (App l r) = App (helper taken l) (helper taken r)
|
||||
helper _ (Ext e) = Ext e
|
||||
|
||||
-- | Find names for unnamed variables that are unique in the current scope.
|
||||
--
|
||||
-- Names for variables follow the schema @a@, @b@, ..., @aa@, @ab@, ...
|
||||
findVarNames :: Term e Name (Maybe Name) -> Term e Name Name
|
||||
findVarNames term = helper (Set.fromList $ consts term) term
|
||||
where
|
||||
helper _ (Var i) = Var i
|
||||
helper _ (Const c) = Const c
|
||||
helper taken (Lambda v t) =
|
||||
let name = fromMaybe (chooseUnique taken varNames) v
|
||||
in Lambda name $ helper (Set.insert name taken) t
|
||||
helper taken (App l r) = App (helper taken l) (helper taken r)
|
||||
helper _ (Ext e) = Ext e
|
||||
|
||||
-- | Display a term using the variable and constant names provided. Does not
|
||||
-- attempt to resolve name collisions.
|
||||
displayTerm :: (e -> T.Text) -> Term e Name Name -> T.Text
|
||||
displayTerm f = dTerm f []
|
||||
|
||||
-- | Display a term. Tries to use the provided variable names where possible.
|
||||
-- Resolves name collisions.
|
||||
displayTerm' :: (e -> T.Text) -> Term e (Maybe Name) (Maybe Name) -> T.Text
|
||||
displayTerm' f = displayTerm f . findVarNames . makeVarNamesUnique . findConstNames
|
||||
|
||||
nth :: [a] -> Natural -> Maybe a
|
||||
nth [] _ = Nothing
|
||||
nth (x:_) 0 = Just x
|
||||
nth (_:xs) n = nth xs $ n - 1
|
||||
|
||||
varName :: [Name] -> Natural -> Name
|
||||
varName vs i = fromMaybe e $ nth vs i
|
||||
where
|
||||
e = "[" <> T.pack (show i) <> "]"
|
||||
|
||||
dTerm :: (e -> T.Text) -> [Name] -> Term e Name Name -> T.Text
|
||||
dTerm _ vs (Var i) = varName vs i
|
||||
dTerm _ _ (Const c) = c
|
||||
dTerm f vs (Lambda v t) = "λ" <> v <> dLambda (v:vs) t
|
||||
where
|
||||
dLambda ws (Lambda w u) = " " <> w <> dLambda (w:ws) u
|
||||
dLambda ws u = ". " <> dTerm f ws u
|
||||
dTerm f vs (App l r) = dLeft l <> " " <> dRight r
|
||||
where
|
||||
dLeft t@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
|
||||
dLeft t = dTerm f vs t
|
||||
dRight t@(Lambda _ _) = "(" <> dTerm f vs t <> ")"
|
||||
dRight t@(App _ _) = "(" <> dTerm f vs t <> ")"
|
||||
dRight t = dTerm f vs t
|
||||
dTerm f _ (Ext e) = f e
|
||||
|
|
@ -1,56 +0,0 @@
|
|||
-- | This module contains 'Term', the base type for lambda expressions. It also
|
||||
-- contains a few utility functions for operating on it.
|
||||
|
||||
module Propa.Lambda.Term
|
||||
( Term(..)
|
||||
, vars
|
||||
, mapVars
|
||||
, consts
|
||||
, mapConsts
|
||||
) where
|
||||
|
||||
import Numeric.Natural
|
||||
|
||||
-- | Lambda calculus term using De Bruijn indexing and expanded to deal with
|
||||
-- naming complexity and extensions.
|
||||
data Term e c v
|
||||
= Var Natural
|
||||
-- ^ Variable using a De Bruijn index
|
||||
| Const c
|
||||
-- ^ Constant living outside the variable namespace
|
||||
| Lambda v (Term e c v)
|
||||
-- ^ Lambda definition
|
||||
| App (Term e c v) (Term e c v)
|
||||
-- ^ Lambda application
|
||||
| Ext e
|
||||
-- ^ Term extension (set @e@ to 'Data.Void' if you don't need this)
|
||||
deriving (Show)
|
||||
|
||||
-- | All of a term's variable names in order from left to right.
|
||||
vars :: Term e c v -> [v]
|
||||
vars (Lambda v t) = v : vars t
|
||||
vars (App l r) = vars l <> vars r
|
||||
vars _ = []
|
||||
|
||||
-- | Map over the variable names.
|
||||
mapVars :: (a -> b) -> Term e c a -> Term e c b
|
||||
mapVars _ (Var i) = Var i
|
||||
mapVars _ (Const c) = Const c
|
||||
mapVars f (Lambda a t) = Lambda (f a) (mapVars f t)
|
||||
mapVars f (App l r) = App (mapVars f l) (mapVars f r)
|
||||
mapVars _ (Ext e) = Ext e
|
||||
|
||||
-- | All of a term's constant names in order from left to right.
|
||||
consts :: Term e c v -> [c]
|
||||
consts (Const c) = [c]
|
||||
consts (Lambda _ t) = consts t
|
||||
consts (App l r) = consts l <> consts r
|
||||
consts _ = []
|
||||
|
||||
-- | Map over the constant names.
|
||||
mapConsts :: (a -> b) -> Term e a v -> Term e b v
|
||||
mapConsts _ (Var i) = Var i
|
||||
mapConsts f (Const c) = Const (f c)
|
||||
mapConsts f (Lambda v t) = Lambda v (mapConsts f t)
|
||||
mapConsts f (App l r) = App (mapConsts f l) (mapConsts f r)
|
||||
mapConsts _ (Ext e) = Ext e
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Propa.Prolog.Debug
|
||||
( parseAndRun
|
||||
) where
|
||||
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Text.IO as T
|
||||
|
||||
import Propa.Prolog.Display
|
||||
import Propa.Prolog.Parse
|
||||
import Propa.Prolog.Unify
|
||||
|
||||
parseAndRun :: String -> String -> IO ()
|
||||
parseAndRun dbStr statsStr = T.putStrLn $ case results of
|
||||
Left e -> e
|
||||
Right [] -> "No."
|
||||
Right rs -> T.intercalate "\n" rs
|
||||
where
|
||||
results = do
|
||||
db <- parseDb "<db>" $ T.pack dbStr
|
||||
stats <- parseStats "<query>" $ T.pack statsStr
|
||||
pure $ map displayResult $ run db stats
|
||||
|
|
@ -1,71 +0,0 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Propa.Prolog.Display
|
||||
( displayTerm
|
||||
, displayTerms
|
||||
, displayDef
|
||||
, displayDefs
|
||||
, displayResult
|
||||
) where
|
||||
|
||||
import Data.Char
|
||||
import Data.List
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Text as T
|
||||
|
||||
import Propa.Prolog.Types
|
||||
|
||||
displayName :: T.Text -> T.Text
|
||||
displayName name
|
||||
| T.all isLower name = name
|
||||
| otherwise = "\"" <> escaped <> "\""
|
||||
where
|
||||
escaped = foldl' (\s (a, b) -> T.replace a b s) name
|
||||
[ ("\\", "\\\\")
|
||||
, ("\n", "\\n")
|
||||
, ("\r", "\\r")
|
||||
, ("\t", "\\t")
|
||||
]
|
||||
|
||||
displayStat :: Stat T.Text -> T.Text
|
||||
displayStat (Stat "[]" []) = "[]"
|
||||
displayStat (Stat "[|]" [a, b]) = "[" <> displayTerm a <> displayList b
|
||||
displayStat (Stat name []) = displayName name
|
||||
displayStat (Stat name args)
|
||||
= displayName name
|
||||
<> "("
|
||||
<> T.intercalate ", " (map displayTerm args)
|
||||
<> ")"
|
||||
|
||||
displayList :: Term T.Text -> T.Text
|
||||
displayList (TStat (Stat "[|]" [a, b])) = "," <> displayTerm a <> displayList b
|
||||
displayList (TStat (Stat "[]" [])) = "]"
|
||||
displayList t = "|" <> displayTerm t <> "]"
|
||||
|
||||
displayTerm :: Term T.Text -> T.Text
|
||||
displayTerm (TVar v) = v
|
||||
displayTerm (TInt i) = T.pack $ show i
|
||||
displayTerm (TStat s) = displayStat s
|
||||
|
||||
displayTerms :: [Term T.Text] -> T.Text
|
||||
displayTerms terms = T.intercalate ",\n" (map displayTerm terms) <> "."
|
||||
|
||||
displayDef :: Def T.Text -> T.Text
|
||||
displayDef (Def stat []) = displayStat stat <> "."
|
||||
displayDef (Def stat stats)
|
||||
= displayStat stat
|
||||
<> " :-\n"
|
||||
<> T.intercalate ",\n" (map (\t -> " " <> displayStat t) stats)
|
||||
<> "."
|
||||
|
||||
displayDefs :: [Def T.Text] -> T.Text
|
||||
displayDefs = T.intercalate "\n" . map displayDef
|
||||
|
||||
displayResult :: Map.Map T.Text (Term T.Text) -> T.Text
|
||||
displayResult m
|
||||
| null termsToDisplay = "Yes."
|
||||
| otherwise = T.intercalate "\n" termsAsStrings
|
||||
where
|
||||
termsToDisplay = filter (\(k, v) -> v /= TVar k) $ Map.assocs m
|
||||
termsAsStrings = map (\(k, v) -> k <> " = " <> displayTerm v) termsToDisplay
|
||||
|
|
@ -1,128 +0,0 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Propa.Prolog.Parse
|
||||
( parseStats
|
||||
, parseDb
|
||||
) where
|
||||
|
||||
import Control.Monad
|
||||
import Data.Bifunctor
|
||||
import Data.Char
|
||||
import Data.Void
|
||||
|
||||
import Control.Monad.Combinators.Expr
|
||||
import qualified Data.Text as T
|
||||
import Text.Megaparsec
|
||||
import qualified Text.Megaparsec.Char as C
|
||||
import qualified Text.Megaparsec.Char.Lexer as L
|
||||
|
||||
import Propa.Prolog.Types
|
||||
|
||||
type Parser = Parsec Void T.Text
|
||||
|
||||
-- Lexeme stuff
|
||||
|
||||
space :: Parser ()
|
||||
space = L.space C.space1 (L.skipLineComment "%") (L.skipBlockComment "/*" "*/")
|
||||
|
||||
lexeme :: Parser a -> Parser a
|
||||
lexeme = L.lexeme space
|
||||
|
||||
symbol :: T.Text -> Parser T.Text
|
||||
symbol = L.symbol space
|
||||
|
||||
parens :: Parser a -> Parser a
|
||||
parens = between (symbol "(") (symbol ")")
|
||||
|
||||
brackets :: Parser a -> Parser a
|
||||
brackets = between (symbol "[") (symbol "]")
|
||||
|
||||
-- Names
|
||||
|
||||
pName :: Parser T.Text
|
||||
pName = lexeme $ unquotedName <|> quotedName
|
||||
where
|
||||
unquotedName = takeWhile1P (Just "lowercase character") isLower
|
||||
quotedName = fmap T.pack $ C.char '\'' *> manyTill L.charLiteral (C.char '\'')
|
||||
|
||||
pVarName :: Parser T.Text
|
||||
pVarName = lexeme $ takeWhile1P (Just "uppercase character") isUpper
|
||||
|
||||
-- Statements
|
||||
|
||||
pTermToStat :: Parser (Term T.Text) -> Parser (Stat T.Text)
|
||||
pTermToStat p = do
|
||||
term <- p
|
||||
case term of
|
||||
(TVar _) -> fail "expected statement, not variable"
|
||||
(TInt _) -> fail "expected statement, not integer"
|
||||
(TStat s) -> pure s
|
||||
|
||||
-- | Parse a statement of the form @name(args)@.
|
||||
pPlainStat :: Parser (Stat T.Text)
|
||||
pPlainStat = do
|
||||
name <- pName
|
||||
terms <- parens (pTerm `sepBy1` symbol ",") <|> pure []
|
||||
pure $ Stat name terms
|
||||
|
||||
pStat :: Parser (Stat T.Text)
|
||||
pStat = pPlainStat <|> pTermToStat pTerm
|
||||
|
||||
pStats :: Parser [Stat T.Text]
|
||||
pStats = (pStat `sepBy1` symbol ",") <* symbol "."
|
||||
|
||||
-- Terms
|
||||
|
||||
pCons :: Parser (Term T.Text)
|
||||
pCons = brackets $ do
|
||||
elems <- pTerm `sepBy1` symbol ","
|
||||
void $ symbol "|"
|
||||
rest <- pTerm
|
||||
pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) rest elems
|
||||
|
||||
pList :: Parser (Term T.Text)
|
||||
pList = do
|
||||
elems <- brackets $ pTerm `sepBy` symbol ","
|
||||
pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) (TStat $ Stat "[]" []) elems
|
||||
|
||||
-- | Parse a term that is not an expression.
|
||||
pPlainTerm :: Parser (Term T.Text)
|
||||
pPlainTerm
|
||||
= (TVar <$> pVarName)
|
||||
<|> (TInt <$> L.signed (pure ()) L.decimal)
|
||||
<|> (TStat <$> pPlainStat)
|
||||
<|> try pCons
|
||||
<|> pList
|
||||
<|> parens pTerm
|
||||
|
||||
pTerm :: Parser (Term T.Text)
|
||||
pTerm = makeExprParser pPlainTerm
|
||||
[ [ binary "=" ]
|
||||
]
|
||||
where
|
||||
binary name = InfixL $ (\a b -> TStat $ Stat name [a, b]) <$ symbol name
|
||||
|
||||
-- Definitions
|
||||
|
||||
pDef :: Parser (Def T.Text)
|
||||
pDef = do
|
||||
stat <- pStat
|
||||
stats <- (symbol ":-" *> (pStat `sepBy1` symbol ",")) <|> pure []
|
||||
void $ symbol "."
|
||||
pure $ Def stat stats
|
||||
|
||||
pDefs :: Parser [Def T.Text]
|
||||
pDefs = many pDef
|
||||
|
||||
-- And finally, our nice parsers
|
||||
|
||||
parseHelper :: Parser a -> FilePath -> T.Text -> Either T.Text a
|
||||
parseHelper p path input
|
||||
= first (T.pack . errorBundlePretty)
|
||||
$ parse (space *> p <* eof) path input
|
||||
|
||||
parseStats :: FilePath -> T.Text -> Either T.Text [Stat T.Text]
|
||||
parseStats = parseHelper pStats
|
||||
|
||||
parseDb :: FilePath -> T.Text -> Either T.Text (Db T.Text)
|
||||
parseDb = parseHelper pDefs
|
||||
|
|
@ -1,60 +0,0 @@
|
|||
module Propa.Prolog.Types
|
||||
( Stat(..)
|
||||
, Term(..)
|
||||
, tVar
|
||||
, Def(..)
|
||||
, Db
|
||||
) where
|
||||
|
||||
import qualified Data.Text as T
|
||||
|
||||
data Stat a = Stat T.Text [Term a]
|
||||
deriving (Show, Eq)
|
||||
|
||||
instance Functor Stat where
|
||||
fmap f (Stat name terms) = Stat name $ fmap (fmap f) terms
|
||||
|
||||
instance Foldable Stat where
|
||||
foldMap f (Stat _ terms) = foldMap (foldMap f) terms
|
||||
|
||||
instance Traversable Stat where
|
||||
traverse f (Stat name terms) = Stat name <$> traverse (traverse f) terms
|
||||
|
||||
data Term a
|
||||
= TVar a
|
||||
| TInt Integer
|
||||
| TStat (Stat a)
|
||||
deriving (Show, Eq)
|
||||
|
||||
instance Functor Term where
|
||||
fmap f (TVar a) = TVar $ f a
|
||||
fmap _ (TInt i) = TInt i
|
||||
fmap f (TStat s) = TStat $ fmap f s
|
||||
|
||||
instance Foldable Term where
|
||||
foldMap f (TVar a) = f a
|
||||
foldMap _ (TInt _) = mempty
|
||||
foldMap f (TStat s) = foldMap f s
|
||||
|
||||
instance Traversable Term where
|
||||
traverse f (TVar a) = TVar <$> f a
|
||||
traverse _ (TInt i) = pure $ TInt i
|
||||
traverse f (TStat s) = TStat <$> traverse f s
|
||||
|
||||
tVar :: Term a -> Maybe a
|
||||
tVar (TVar v) = Just v
|
||||
tVar _ = Nothing
|
||||
|
||||
data Def a = Def (Stat a) [Stat a]
|
||||
deriving (Show)
|
||||
|
||||
instance Functor Def where
|
||||
fmap f (Def stat stats) = Def (fmap f stat) (fmap f <$> stats)
|
||||
|
||||
instance Foldable Def where
|
||||
foldMap f (Def stat stats) = foldMap f stat <> foldMap (foldMap f) stats
|
||||
|
||||
instance Traversable Def where
|
||||
traverse f (Def stat stats) = Def <$> traverse f stat <*> traverse (traverse f) stats
|
||||
|
||||
type Db a = [Def a]
|
||||
|
|
@ -1,164 +0,0 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Propa.Prolog.Unify
|
||||
( run
|
||||
) where
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad
|
||||
import Data.Foldable
|
||||
import Data.List
|
||||
import Data.Tuple
|
||||
|
||||
import Control.Monad.Trans.Class
|
||||
import Control.Monad.Trans.State
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Text as T
|
||||
|
||||
import Propa.Prolog.Types
|
||||
|
||||
-- General utility functions
|
||||
|
||||
-- | Start at a value and follow the map's entries until the end of the chain of
|
||||
-- references.
|
||||
follow :: (Ord a) => (b -> Maybe a) -> Map.Map a b -> b -> b
|
||||
follow f m b = maybe b (follow f m) $ (m Map.!?) =<< f b
|
||||
|
||||
-- | Deduplicates the elements of a finite list. Doesn't preserve the order of
|
||||
-- the elements. Doesn't work on infinite lists.
|
||||
deduplicate :: (Ord a) => [a] -> [a]
|
||||
deduplicate = Set.toList . Set.fromList
|
||||
|
||||
-- Now the fun begins...
|
||||
|
||||
data Context = Context
|
||||
{ cDb :: Db T.Text
|
||||
, cVarIdx :: Int
|
||||
, cTerms :: Map.Map Int (Term Int)
|
||||
} deriving (Show)
|
||||
|
||||
newContext :: [Def T.Text] -> Context
|
||||
newContext db = Context db 0 Map.empty
|
||||
|
||||
bindTerm :: Int -> Term Int -> UniM ()
|
||||
bindTerm k v = modify $ \c -> c{cTerms = Map.insert k v $ cTerms c}
|
||||
|
||||
-- | Look up a variable, first repeatedly in the var map and then the term map.
|
||||
-- Returns statements unchanged.
|
||||
--
|
||||
-- If this returns a variable, then that variable is not bound.
|
||||
lookupTerm :: Term Int -> UniM (Term Int)
|
||||
lookupTerm t = do
|
||||
c <- get
|
||||
pure $ follow tVar (cTerms c) t
|
||||
|
||||
-- | A simple state monad transformer over the list monad for easy backtracking.
|
||||
-- Needs to be changed when implementing cuts.
|
||||
type UniM = StateT Context []
|
||||
|
||||
varMap :: (Foldable a) => a T.Text -> UniM (Map.Map T.Text Int)
|
||||
varMap a = do
|
||||
c <- get
|
||||
let i = cVarIdx c
|
||||
vars = deduplicate $ toList a
|
||||
vmap = Map.fromList $ zip vars [i..]
|
||||
put c{cVarIdx = i + Map.size vmap}
|
||||
pure vmap
|
||||
|
||||
-- | Convert a definition's variables to unique integers that are not already in
|
||||
-- use in the current context.
|
||||
understand :: (Functor a, Foldable a) => a T.Text -> UniM (a Int, Map.Map T.Text Int)
|
||||
understand a = do
|
||||
vmap <- varMap a
|
||||
pure (fmap (vmap Map.!) a, vmap)
|
||||
|
||||
satisfyStat :: Stat Int -> UniM ()
|
||||
satisfyStat stat = do
|
||||
c <- get
|
||||
(Def dStat dStats, _) <- understand =<< lift (cDb c)
|
||||
unifyStat stat dStat
|
||||
satisfyStats dStats
|
||||
|
||||
satisfyStats :: [Stat Int] -> UniM ()
|
||||
satisfyStats = traverse_ satisfyStat
|
||||
|
||||
unifyStat :: Stat Int -> Stat Int -> UniM ()
|
||||
unifyStat (Stat name1 args1) (Stat name2 args2) = do
|
||||
guard $ name1 == name2
|
||||
unifyTerms args1 args2
|
||||
|
||||
unifyTerm :: Term Int -> Term Int -> UniM ()
|
||||
unifyTerm t1 t2 = do
|
||||
t1' <- lookupTerm t1
|
||||
t2' <- lookupTerm t2
|
||||
case (t1', t2') of
|
||||
(TStat s1, TStat s2) -> unifyStat s1 s2
|
||||
(TInt i1, TInt i2) -> guard $ i1 == i2
|
||||
(TVar v, TVar w) | v == w -> pure ()
|
||||
(TVar v, t) -> bindTerm v t
|
||||
(t, TVar v) -> bindTerm v t
|
||||
(_, _) -> empty
|
||||
|
||||
unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
|
||||
unifyTerms t1 t2 = do
|
||||
guard $ length t1 == length t2
|
||||
sequenceA_ $ zipWith unifyTerm t1 t2
|
||||
|
||||
-- Figuring out how to display the result of the unification
|
||||
|
||||
-- | An infinite list of possible variable names: @A@, @B@, ..., @A1@, @B1@,
|
||||
-- ..., @A2@, ...
|
||||
varNames :: [T.Text]
|
||||
varNames = do
|
||||
num <- "" : map (T.pack . show) [(1::Integer)..]
|
||||
char <- alphabet
|
||||
pure $ char <> num
|
||||
where
|
||||
alphabet = map T.singleton ['A'..'Z']
|
||||
|
||||
-- | Find a naming (Map from integer to name) for all variables in a list of
|
||||
-- terms based on the original variable names and the variable mapping. Attempts
|
||||
-- to map variables to known variables instead of a common unknown variable.
|
||||
findVarNaming :: Map.Map T.Text Int -> Map.Map Int (Term Int) -> [Term Int] -> Map.Map Int T.Text
|
||||
findVarNaming known vars terms =
|
||||
let knownLookedUp :: Map.Map T.Text Int
|
||||
knownLookedUp = Map.mapMaybe (tVar . follow tVar vars . TVar) known
|
||||
knownNaming = Map.fromList $ reverse $ map swap $ Map.toList knownLookedUp
|
||||
knownNames = Map.keysSet known
|
||||
knownVars = Map.keysSet knownNaming
|
||||
termVars = Set.fromList $ concatMap toList terms
|
||||
unknownVars = termVars Set.\\ knownVars
|
||||
availVarNames = filter (not . (`Set.member` knownNames)) varNames
|
||||
unknownNaming = Map.fromList $ zip (sort $ Set.toList unknownVars) availVarNames
|
||||
in knownNaming <> unknownNaming
|
||||
|
||||
-- | Recursively set variables to their most resolved term.
|
||||
resolveVars :: Term Int -> UniM (Term Int)
|
||||
resolveVars t = do
|
||||
t2 <- lookupTerm t
|
||||
case t2 of
|
||||
(TVar v) -> pure $ TVar v
|
||||
(TInt i) -> pure $ TInt i
|
||||
(TStat (Stat name args)) -> TStat . Stat name <$> traverse resolveVars args
|
||||
|
||||
-- | Helper type so I can resolve variables in multiple statements
|
||||
-- simultaneously.
|
||||
newtype Stats a = Stats { unStats :: [Stat a] }
|
||||
|
||||
instance Functor Stats where
|
||||
fmap f (Stats ts) = Stats $ fmap (fmap f) ts
|
||||
|
||||
instance Foldable Stats where
|
||||
foldMap f (Stats ts) = foldMap (foldMap f) ts
|
||||
|
||||
run :: Db T.Text -> [Stat T.Text] -> [Map.Map T.Text (Term T.Text)]
|
||||
run db stats = map fst $ runStateT helper $ newContext db
|
||||
where
|
||||
helper = do
|
||||
(stats2, vmap) <- understand $ Stats stats
|
||||
satisfyStats $ unStats stats2
|
||||
tmap <- traverse (resolveVars . TVar) vmap
|
||||
c <- get
|
||||
let naming = findVarNaming vmap (cTerms c) $ Map.elems tmap
|
||||
pure $ fmap (naming Map.!) <$> tmap
|
||||
12
src/main.rs
Normal file
12
src/main.rs
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
#![feature(proc_macro_hygiene, decl_macro)]
|
||||
|
||||
#[macro_use] extern crate rocket;
|
||||
|
||||
#[get("/")]
|
||||
fn index() -> &'static str {
|
||||
"Hello, world!"
|
||||
}
|
||||
|
||||
fn main() {
|
||||
rocket::ignite().mount("/", routes![index]).launch();
|
||||
}
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
resolver:
|
||||
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/16/23.yaml
|
||||
|
||||
packages:
|
||||
- .
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
# This file was autogenerated by Stack.
|
||||
# You should not edit this file by hand.
|
||||
# For more information, please see the documentation at:
|
||||
# https://docs.haskellstack.org/en/stable/lock_files
|
||||
|
||||
packages: []
|
||||
snapshots:
|
||||
- completed:
|
||||
size: 532832
|
||||
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/16/23.yaml
|
||||
sha256: fbb2a0519008533924c7753bd7164ddd1009f09504eb06674acad6049b46db09
|
||||
original:
|
||||
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/16/23.yaml
|
||||
Loading…
Add table
Add a link
Reference in a new issue