From 809c25c8bca80826fb18cdbb34ad070aacfb2801 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 1 Nov 2023 23:46:22 -0500 Subject: [PATCH] ok we're back to rust --- .gitignore | 3 +- Cargo.lock | 220 ++++++++++++ Cargo.toml | 3 + Makefile | 4 + bidir/.gitignore | 1 + bidir/Cargo.lock | 220 ++++++++++++ bidir/Cargo.toml | 12 + bidir/bidir.ts | 57 ---- bidir/contexts.ts | 18 - bidir/data.ts | 42 --- bidir/src/bidir.rs | 134 ++++++++ bidir/src/data.rs | 53 +++ bidir/src/gensym.rs | 18 + bidir/src/lib.rs | 6 + bidir/src/tests.rs | 13 + bidir/tarpaulin-report.html | 660 ++++++++++++++++++++++++++++++++++++ rustfmt.toml | 1 + 17 files changed, 1347 insertions(+), 118 deletions(-) create mode 100644 Cargo.lock create mode 100644 Cargo.toml create mode 100644 Makefile create mode 100644 bidir/.gitignore create mode 100644 bidir/Cargo.lock create mode 100644 bidir/Cargo.toml delete mode 100644 bidir/bidir.ts delete mode 100644 bidir/contexts.ts delete mode 100644 bidir/data.ts create mode 100644 bidir/src/bidir.rs create mode 100644 bidir/src/data.rs create mode 100644 bidir/src/gensym.rs create mode 100644 bidir/src/lib.rs create mode 100644 bidir/src/tests.rs create mode 100644 bidir/tarpaulin-report.html create mode 100644 rustfmt.toml diff --git a/.gitignore b/.gitignore index 1454376..0726eb1 100644 --- a/.gitignore +++ b/.gitignore @@ -9,4 +9,5 @@ node_modules lib/bs __tests__/**/*.mjs -src/**/*.mjs \ No newline at end of file +src/**/*.mjs +target \ No newline at end of file diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 0000000..b099ccc --- /dev/null +++ b/Cargo.lock @@ -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" diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..1d7c0ed --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,3 @@ +[workspace] +resolver = "2" +members = ["bidir"] diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..365febb --- /dev/null +++ b/Makefile @@ -0,0 +1,4 @@ +.PHONY: doc + +doc: + cargo doc --workspace --no-deps --document-private-items \ No newline at end of file diff --git a/bidir/.gitignore b/bidir/.gitignore new file mode 100644 index 0000000..1de5659 --- /dev/null +++ b/bidir/.gitignore @@ -0,0 +1 @@ +target \ No newline at end of file diff --git a/bidir/Cargo.lock b/bidir/Cargo.lock new file mode 100644 index 0000000..b099ccc --- /dev/null +++ b/bidir/Cargo.lock @@ -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" diff --git a/bidir/Cargo.toml b/bidir/Cargo.toml new file mode 100644 index 0000000..44c1c6e --- /dev/null +++ b/bidir/Cargo.toml @@ -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" diff --git a/bidir/bidir.ts b/bidir/bidir.ts deleted file mode 100644 index 07a0319..0000000 --- a/bidir/bidir.ts +++ /dev/null @@ -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[]] {} diff --git a/bidir/contexts.ts b/bidir/contexts.ts deleted file mode 100644 index aa57188..0000000 --- a/bidir/contexts.ts +++ /dev/null @@ -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; -} diff --git a/bidir/data.ts b/bidir/data.ts deleted file mode 100644 index 276a26d..0000000 --- a/bidir/data.ts +++ /dev/null @@ -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 }; diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs new file mode 100644 index 0000000..5d6fe9e --- /dev/null +++ b/bidir/src/bidir.rs @@ -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 { + 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 { + 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!() + } + } +} diff --git a/bidir/src/data.rs b/bidir/src/data.rs new file mode 100644 index 0000000..1dfb5b0 --- /dev/null +++ b/bidir/src/data.rs @@ -0,0 +1,53 @@ +use im::Vector; + +#[derive(Debug, Clone)] +pub enum Term { + Unit, + Var(String), + Lam(String, Box), + App(Box, Box), + Annot(Box, Type), +} + +#[derive(Debug, Clone)] +pub enum Type { + Unit, + Var(String), + Existential(String), + Polytype(String, Box), + Arrow(Box, Box), +} + +#[derive(Debug, Clone)] +pub enum Monotype { + Unit, + Var(String), + Existential(String), + Arrow(Box, Box), +} + +pub type Context = Vector; + +#[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) -> Option { + ctx.iter().find_map(|entry| match entry { + ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some(t.clone()), + _ => None, + }) +} diff --git a/bidir/src/gensym.rs b/bidir/src/gensym.rs new file mode 100644 index 0000000..738ff46 --- /dev/null +++ b/bidir/src/gensym.rs @@ -0,0 +1,18 @@ +use lazy_static::lazy_static; +use parking_lot::Mutex; + +lazy_static! { + static ref CTR: Mutex = Mutex::new(0); +} + +pub fn gensym() -> String { + gensym_prefix("var") +} + +pub fn gensym_prefix(prefix: impl AsRef) -> String { + let mut g = CTR.lock(); + let ctr = *g; + *g += 1; + drop(g); + format!("{}{}", prefix.as_ref(), ctr) +} diff --git a/bidir/src/lib.rs b/bidir/src/lib.rs new file mode 100644 index 0000000..9802e1a --- /dev/null +++ b/bidir/src/lib.rs @@ -0,0 +1,6 @@ +mod bidir; +mod data; + +mod gensym; +#[cfg(test)] +mod tests; diff --git a/bidir/src/tests.rs b/bidir/src/tests.rs new file mode 100644 index 0000000..f176c3e --- /dev/null +++ b/bidir/src/tests.rs @@ -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(()) +} diff --git a/bidir/tarpaulin-report.html b/bidir/tarpaulin-report.html new file mode 100644 index 0000000..6aa70e7 --- /dev/null +++ b/bidir/tarpaulin-report.html @@ -0,0 +1,660 @@ + + + + + + + +
+ + + + + + \ No newline at end of file diff --git a/rustfmt.toml b/rustfmt.toml new file mode 100644 index 0000000..b196eaa --- /dev/null +++ b/rustfmt.toml @@ -0,0 +1 @@ +tab_spaces = 2