ok we're back to rust
This commit is contained in:
parent
f85b5d6785
commit
809c25c8bc
|
|
@ -9,4 +9,5 @@ node_modules
|
|||
lib/bs
|
||||
|
||||
__tests__/**/*.mjs
|
||||
src/**/*.mjs
|
||||
src/**/*.mjs
|
||||
target
|
||||
|
|
@ -0,0 +1,220 @@
|
|||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "anyhow"
|
||||
version = "1.0.75"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a4668cab20f66d8d020e1fbc0ebe47217433c1b6c8f2040faf858554e394ace6"
|
||||
|
||||
[[package]]
|
||||
name = "autocfg"
|
||||
version = "1.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
|
||||
|
||||
[[package]]
|
||||
name = "bidir"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"anyhow",
|
||||
"im",
|
||||
"lazy_static",
|
||||
"parking_lot",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "bitflags"
|
||||
version = "1.3.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
|
||||
|
||||
[[package]]
|
||||
name = "bitmaps"
|
||||
version = "2.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2"
|
||||
dependencies = [
|
||||
"typenum",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "im"
|
||||
version = "15.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9"
|
||||
dependencies = [
|
||||
"bitmaps",
|
||||
"rand_core",
|
||||
"rand_xoshiro",
|
||||
"sized-chunks",
|
||||
"typenum",
|
||||
"version_check",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "lazy_static"
|
||||
version = "1.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.149"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a08173bc88b7955d1b3145aa561539096c421ac8debde8cbc3612ec635fee29b"
|
||||
|
||||
[[package]]
|
||||
name = "lock_api"
|
||||
version = "0.4.11"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"scopeguard",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "parking_lot"
|
||||
version = "0.12.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3742b2c103b9f06bc9fff0a37ff4912935851bee6d36f3c02bcc755bcfec228f"
|
||||
dependencies = [
|
||||
"lock_api",
|
||||
"parking_lot_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "parking_lot_core"
|
||||
version = "0.9.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4c42a9226546d68acdd9c0a280d17ce19bfe27a46bf68784e4066115788d008e"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"libc",
|
||||
"redox_syscall",
|
||||
"smallvec",
|
||||
"windows-targets",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_core"
|
||||
version = "0.6.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
|
||||
|
||||
[[package]]
|
||||
name = "rand_xoshiro"
|
||||
version = "0.6.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa"
|
||||
dependencies = [
|
||||
"rand_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "redox_syscall"
|
||||
version = "0.4.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "scopeguard"
|
||||
version = "1.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
|
||||
|
||||
[[package]]
|
||||
name = "sized-chunks"
|
||||
version = "0.6.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e"
|
||||
dependencies = [
|
||||
"bitmaps",
|
||||
"typenum",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "smallvec"
|
||||
version = "1.11.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "942b4a808e05215192e39f4ab80813e599068285906cc91aa64f923db842bd5a"
|
||||
|
||||
[[package]]
|
||||
name = "typenum"
|
||||
version = "1.17.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
|
||||
|
||||
[[package]]
|
||||
name = "version_check"
|
||||
version = "0.9.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
|
||||
|
||||
[[package]]
|
||||
name = "windows-targets"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c"
|
||||
dependencies = [
|
||||
"windows_aarch64_gnullvm",
|
||||
"windows_aarch64_msvc",
|
||||
"windows_i686_gnu",
|
||||
"windows_i686_msvc",
|
||||
"windows_x86_64_gnu",
|
||||
"windows_x86_64_gnullvm",
|
||||
"windows_x86_64_msvc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_gnullvm"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_msvc"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_gnu"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_msvc"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnu"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnullvm"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_msvc"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
[workspace]
|
||||
resolver = "2"
|
||||
members = ["bidir"]
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
.PHONY: doc
|
||||
|
||||
doc:
|
||||
cargo doc --workspace --no-deps --document-private-items
|
||||
|
|
@ -0,0 +1 @@
|
|||
target
|
||||
|
|
@ -0,0 +1,220 @@
|
|||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "anyhow"
|
||||
version = "1.0.75"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a4668cab20f66d8d020e1fbc0ebe47217433c1b6c8f2040faf858554e394ace6"
|
||||
|
||||
[[package]]
|
||||
name = "autocfg"
|
||||
version = "1.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
|
||||
|
||||
[[package]]
|
||||
name = "bidir"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"anyhow",
|
||||
"im",
|
||||
"lazy_static",
|
||||
"parking_lot",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "bitflags"
|
||||
version = "1.3.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
|
||||
|
||||
[[package]]
|
||||
name = "bitmaps"
|
||||
version = "2.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2"
|
||||
dependencies = [
|
||||
"typenum",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "im"
|
||||
version = "15.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9"
|
||||
dependencies = [
|
||||
"bitmaps",
|
||||
"rand_core",
|
||||
"rand_xoshiro",
|
||||
"sized-chunks",
|
||||
"typenum",
|
||||
"version_check",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "lazy_static"
|
||||
version = "1.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.149"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a08173bc88b7955d1b3145aa561539096c421ac8debde8cbc3612ec635fee29b"
|
||||
|
||||
[[package]]
|
||||
name = "lock_api"
|
||||
version = "0.4.11"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"scopeguard",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "parking_lot"
|
||||
version = "0.12.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3742b2c103b9f06bc9fff0a37ff4912935851bee6d36f3c02bcc755bcfec228f"
|
||||
dependencies = [
|
||||
"lock_api",
|
||||
"parking_lot_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "parking_lot_core"
|
||||
version = "0.9.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4c42a9226546d68acdd9c0a280d17ce19bfe27a46bf68784e4066115788d008e"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"libc",
|
||||
"redox_syscall",
|
||||
"smallvec",
|
||||
"windows-targets",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_core"
|
||||
version = "0.6.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
|
||||
|
||||
[[package]]
|
||||
name = "rand_xoshiro"
|
||||
version = "0.6.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa"
|
||||
dependencies = [
|
||||
"rand_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "redox_syscall"
|
||||
version = "0.4.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "scopeguard"
|
||||
version = "1.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
|
||||
|
||||
[[package]]
|
||||
name = "sized-chunks"
|
||||
version = "0.6.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e"
|
||||
dependencies = [
|
||||
"bitmaps",
|
||||
"typenum",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "smallvec"
|
||||
version = "1.11.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "942b4a808e05215192e39f4ab80813e599068285906cc91aa64f923db842bd5a"
|
||||
|
||||
[[package]]
|
||||
name = "typenum"
|
||||
version = "1.17.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
|
||||
|
||||
[[package]]
|
||||
name = "version_check"
|
||||
version = "0.9.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
|
||||
|
||||
[[package]]
|
||||
name = "windows-targets"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c"
|
||||
dependencies = [
|
||||
"windows_aarch64_gnullvm",
|
||||
"windows_aarch64_msvc",
|
||||
"windows_i686_gnu",
|
||||
"windows_i686_msvc",
|
||||
"windows_x86_64_gnu",
|
||||
"windows_x86_64_gnullvm",
|
||||
"windows_x86_64_msvc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_gnullvm"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_msvc"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_gnu"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_msvc"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnu"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnullvm"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_msvc"
|
||||
version = "0.48.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
[package]
|
||||
name = "bidir"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
anyhow = "1.0.75"
|
||||
im = "15.1.0"
|
||||
lazy_static = "1.4.0"
|
||||
parking_lot = "0.12.1"
|
||||
|
|
@ -1,57 +0,0 @@
|
|||
import { isTypeInContext } from "./contexts";
|
||||
import { ContextEntry, Term, Type } from "./data";
|
||||
|
||||
function check(
|
||||
ctx: ContextEntry[],
|
||||
term: Term,
|
||||
type: Type
|
||||
): [boolean, ContextEntry[]] {
|
||||
switch (term.kind) {
|
||||
case "var":
|
||||
break;
|
||||
case "unit":
|
||||
return [type.kind === "unit", ctx];
|
||||
case "lambda": {
|
||||
// Get A and B first
|
||||
if (type.kind !== "arrow") return [false, ctx];
|
||||
const { input: A, output: B } = type;
|
||||
}
|
||||
case "app":
|
||||
break;
|
||||
case "annot":
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
function synthesize(ctx: ContextEntry[], term: Term): [Type, ContextEntry[]] {
|
||||
switch (term.kind) {
|
||||
case "var": {
|
||||
const res = lookupTypeVariable(ctx, term.name);
|
||||
if (!res) throw new Error("wtf?");
|
||||
return [res, ctx];
|
||||
}
|
||||
case "unit":
|
||||
return [{ kind: "unit" }, ctx];
|
||||
case "lambda": {
|
||||
}
|
||||
case "app":
|
||||
break;
|
||||
case "annot": {
|
||||
// Require that the type exists
|
||||
if (!isTypeInContext(term.type, ctx))
|
||||
throw new Error("type doesn't exist");
|
||||
|
||||
// Require that the term checks against the type
|
||||
const [result, outputCtx] = check(ctx, term.term, term.type);
|
||||
if (!result) throw new Error("invalid annotation: term doesn't check");
|
||||
|
||||
return [term.type, outputCtx];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
function synthesizeApp(
|
||||
ctx: ContextEntry[],
|
||||
funcType: Type,
|
||||
term: Term
|
||||
): [Type, ContextEntry[]] {}
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
// Helper functions for dealing with contexts
|
||||
|
||||
import { ContextEntry, Type } from "./data";
|
||||
import { isEqual } from "lodash";
|
||||
|
||||
/** Γ |- A (is the given type in this context?) */
|
||||
export function isTypeInContext(type: Type, ctx: ContextEntry[]): boolean {
|
||||
for (const entry of ctx) {
|
||||
switch (entry.kind) {
|
||||
case "termAnnot":
|
||||
if (isEqual(entry.type, type)) return true;
|
||||
break;
|
||||
default:
|
||||
continue;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
|
@ -1,42 +0,0 @@
|
|||
/**
|
||||
* Terms e ::= x | () | λx. e | e e | (e : A)
|
||||
* Types A, B, C ::= 1 | α | ^α | ∀α. A | A → B
|
||||
* Monotypes τ, σ ::= 1 | α | ^α | τ → σ
|
||||
* Contexts Γ, ∆, Θ ::= · | Γ, α | Γ, x : A
|
||||
* | Γ, ^α | Γ, ^α = τ | Γ, I^α
|
||||
* Complete Contexts Ω ::= · | Ω, α | Ω, x : A
|
||||
* | Ω, ^α = τ | Ω, I^
|
||||
*/
|
||||
|
||||
export type Term =
|
||||
| { kind: "var"; name: string }
|
||||
| { kind: "unit" }
|
||||
| { kind: "lambda"; name: string; body: Term }
|
||||
| { kind: "app"; func: Term; arg: Term }
|
||||
| { kind: "annot"; term: Term; type: Type };
|
||||
|
||||
export type Type =
|
||||
| { kind: "unit" }
|
||||
| { kind: "var"; name: string }
|
||||
| { kind: "existential"; name: string }
|
||||
| { kind: "poly"; name: string; type: Type }
|
||||
| { kind: "arrow"; input: Type; output: Type };
|
||||
|
||||
export type Monotype =
|
||||
| { kind: "unit" }
|
||||
| { kind: "var"; name: string }
|
||||
| { kind: "existential"; name: string }
|
||||
| { kind: "arrow"; input: Monotype; output: Monotype };
|
||||
|
||||
export type ContextEntry =
|
||||
| { kind: "typeVar"; name: string }
|
||||
| { kind: "termAnnot"; name: string; type: Type }
|
||||
| { kind: "existentialVar"; name: string }
|
||||
| { kind: "existentialSolved"; name: string; type: Monotype }
|
||||
| { kind: "marker"; name: string };
|
||||
|
||||
export type CompleteContextEntry =
|
||||
| { kind: "typeVar"; name: string }
|
||||
| { kind: "termAnnot"; name: string; type: Type }
|
||||
| { kind: "existentialSolved"; name: string; type: Monotype }
|
||||
| { kind: "marker"; name: string };
|
||||
|
|
@ -0,0 +1,134 @@
|
|||
use anyhow::{bail, Result};
|
||||
|
||||
use crate::{
|
||||
data::{ctx_lookup_type, Context, ContextEntry, Term, Type},
|
||||
gensym::gensym_prefix,
|
||||
};
|
||||
|
||||
// Figure 8. Applying a context, as a substitution, to a type
|
||||
|
||||
pub fn app_ctx(ctx: &Context, ty: &Type) -> Type {
|
||||
match ty {
|
||||
Type::Existential(_) => todo!(),
|
||||
Type::Polytype(_, _) => todo!(),
|
||||
Type::Arrow(a, b) => Type::Arrow(Box::new(app_ctx(ctx, a)), Box::new(app_ctx(ctx, b))),
|
||||
_ => ty.clone(),
|
||||
}
|
||||
}
|
||||
|
||||
// Figure 9. Algorithmic subtyping
|
||||
|
||||
/// Under input context Γ , type A is a subtype of B, with output context ∆
|
||||
pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result<Context> {
|
||||
println!("subtype(ctx = {ctx:?}, a = {a:?}, b = {b:?})");
|
||||
match (a, b) {
|
||||
// <:Unit rule
|
||||
(Type::Unit, Type::Unit) => Ok(ctx.clone()),
|
||||
|
||||
// <:Var rule
|
||||
(Type::Var(x), Type::Var(y)) if x == y => {
|
||||
// Ensure that the name exists in the context
|
||||
if !ctx.iter().any(|entry| match entry {
|
||||
ContextEntry::ExistentialVar(z) if x == z => true,
|
||||
_ => false,
|
||||
}) {
|
||||
bail!("name {x} not in context");
|
||||
}
|
||||
|
||||
Ok(ctx.clone())
|
||||
}
|
||||
|
||||
(Type::Existential(_), Type::Unit) => todo!(),
|
||||
(Type::Existential(_), Type::Var(_)) => todo!(),
|
||||
(Type::Existential(_), Type::Existential(_)) => todo!(),
|
||||
(Type::Existential(_), Type::Polytype(_, _)) => todo!(),
|
||||
(Type::Existential(_), Type::Arrow(_, _)) => todo!(),
|
||||
(Type::Polytype(_, _), Type::Unit) => todo!(),
|
||||
(Type::Polytype(_, _), Type::Var(_)) => todo!(),
|
||||
(Type::Polytype(_, _), Type::Existential(_)) => todo!(),
|
||||
(Type::Polytype(_, _), Type::Polytype(_, _)) => todo!(),
|
||||
(Type::Polytype(_, _), Type::Arrow(_, _)) => todo!(),
|
||||
(Type::Arrow(_, _), Type::Unit) => todo!(),
|
||||
(Type::Arrow(_, _), Type::Var(_)) => todo!(),
|
||||
(Type::Arrow(_, _), Type::Existential(_)) => todo!(),
|
||||
(Type::Arrow(_, _), Type::Polytype(_, _)) => todo!(),
|
||||
(Type::Arrow(_, _), Type::Arrow(_, _)) => todo!(),
|
||||
|
||||
_ => bail!("subtyping relation failed"),
|
||||
}
|
||||
}
|
||||
|
||||
// Figure 10. Instantiation
|
||||
|
||||
// Figure 11. Algorithmic typing
|
||||
|
||||
pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
|
||||
println!("typecheck(ctx = {ctx:?}, term = {term:?}, ty = {ty:?})");
|
||||
match (term, ty) {
|
||||
// 1I rule
|
||||
(Term::Unit, Type::Unit) => Ok(ctx.clone()),
|
||||
|
||||
// ∀I rule
|
||||
(e, Type::Polytype(x, tyA)) => todo!(),
|
||||
|
||||
// →I rule
|
||||
(Term::Lam(x, e), Type::Arrow(ty_a, ty_b)) => {
|
||||
let mut aug_ctx = ctx.clone();
|
||||
todo!()
|
||||
}
|
||||
|
||||
// Sub rule
|
||||
(term, ty) => {
|
||||
let (ty_a, ctx_theta) = synthesize(ctx, term)?;
|
||||
let a = app_ctx(&ctx_theta, &ty_a);
|
||||
let b = app_ctx(&ctx_theta, ty);
|
||||
let ctx_delta = subtype(&ctx_theta, &a, &b)?;
|
||||
Ok(ctx_delta)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
|
||||
println!("synthesize(ctx = {ctx:?}, term = {term:?}");
|
||||
match term {
|
||||
// Var rule
|
||||
Term::Var(name) => {
|
||||
let ty = match ctx_lookup_type(ctx, name) {
|
||||
Some(v) => v,
|
||||
None => bail!("could not find name {name}"),
|
||||
};
|
||||
Ok((ty, ctx.clone()))
|
||||
}
|
||||
|
||||
// 1I⇒ rule
|
||||
Term::Unit => Ok((Type::Unit, ctx.clone())),
|
||||
|
||||
// Anno rule
|
||||
Term::Annot(_, _) => todo!(),
|
||||
|
||||
// →I⇒ rule
|
||||
Term::Lam(x, e) => {
|
||||
let mut aug_ctx = ctx.clone();
|
||||
let ex_a = gensym_prefix("ex");
|
||||
let ex_b = gensym_prefix("ex");
|
||||
aug_ctx.push_back(ContextEntry::TypeVar(ex_a.clone()));
|
||||
aug_ctx.push_back(ContextEntry::TypeVar(ex_b.clone()));
|
||||
aug_ctx.push_back(ContextEntry::TermAnnot(x.clone(), Type::Var(ex_a.clone())));
|
||||
|
||||
let res = typecheck(&aug_ctx, &e, &Type::Var(ex_b.clone()));
|
||||
Ok((
|
||||
Type::Arrow(
|
||||
Box::new(Type::Existential(ex_a)),
|
||||
Box::new(Type::Existential(ex_b)),
|
||||
),
|
||||
ctx.clone(),
|
||||
))
|
||||
}
|
||||
|
||||
// →E rule
|
||||
Term::App(e1, e2) => {
|
||||
let (tyA, out_ctx) = synthesize(ctx, e1)?;
|
||||
todo!()
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,53 @@
|
|||
use im::Vector;
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum Term {
|
||||
Unit,
|
||||
Var(String),
|
||||
Lam(String, Box<Term>),
|
||||
App(Box<Term>, Box<Term>),
|
||||
Annot(Box<Term>, Type),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum Type {
|
||||
Unit,
|
||||
Var(String),
|
||||
Existential(String),
|
||||
Polytype(String, Box<Type>),
|
||||
Arrow(Box<Type>, Box<Type>),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum Monotype {
|
||||
Unit,
|
||||
Var(String),
|
||||
Existential(String),
|
||||
Arrow(Box<Monotype>, Box<Monotype>),
|
||||
}
|
||||
|
||||
pub type Context = Vector<ContextEntry>;
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum ContextEntry {
|
||||
TypeVar(String),
|
||||
TermAnnot(String, Type),
|
||||
ExistentialVar(String),
|
||||
ExistentialSolved(String, Monotype),
|
||||
Marker(String),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum CompleteContextEntry {
|
||||
TypeVar(String),
|
||||
TermAnnot(String, Type),
|
||||
ExistentialSolved(String, Monotype),
|
||||
Marker(String),
|
||||
}
|
||||
|
||||
pub fn ctx_lookup_type(ctx: &Context, name: impl AsRef<str>) -> Option<Type> {
|
||||
ctx.iter().find_map(|entry| match entry {
|
||||
ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some(t.clone()),
|
||||
_ => None,
|
||||
})
|
||||
}
|
||||
|
|
@ -0,0 +1,18 @@
|
|||
use lazy_static::lazy_static;
|
||||
use parking_lot::Mutex;
|
||||
|
||||
lazy_static! {
|
||||
static ref CTR: Mutex<usize> = Mutex::new(0);
|
||||
}
|
||||
|
||||
pub fn gensym() -> String {
|
||||
gensym_prefix("var")
|
||||
}
|
||||
|
||||
pub fn gensym_prefix(prefix: impl AsRef<str>) -> String {
|
||||
let mut g = CTR.lock();
|
||||
let ctr = *g;
|
||||
*g += 1;
|
||||
drop(g);
|
||||
format!("{}{}", prefix.as_ref(), ctr)
|
||||
}
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
mod bidir;
|
||||
mod data;
|
||||
|
||||
mod gensym;
|
||||
#[cfg(test)]
|
||||
mod tests;
|
||||
|
|
@ -0,0 +1,13 @@
|
|||
use anyhow::{bail, Result};
|
||||
use im::Vector;
|
||||
|
||||
use crate::{bidir::synthesize, data::Term};
|
||||
|
||||
#[test]
|
||||
fn test_id() -> Result<()> {
|
||||
let id = Term::Lam("x".to_owned(), Box::new(Term::Var("x".to_owned())));
|
||||
let ctx = Vector::new();
|
||||
let (ty, out_ctx) = synthesize(&ctx, &id)?;
|
||||
// bail!("Output: {ty:?} in context {out_ctx:?}");
|
||||
Ok(())
|
||||
}
|
||||
File diff suppressed because one or more lines are too long
|
|
@ -0,0 +1 @@
|
|||
tab_spaces = 2
|
||||
Loading…
Reference in New Issue