wip
This commit is contained in:
parent
9e14894693
commit
9dd6779950
|
|
@ -65,17 +65,25 @@ dependencies = [
|
|||
"rustc-demangle",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "base64"
|
||||
version = "0.21.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "35636a1494ede3b646cc98f74f8e62c773a38a659ebc777a2cf26b9b74171df9"
|
||||
|
||||
[[package]]
|
||||
name = "bidir"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"anyhow",
|
||||
"contracts",
|
||||
"dashmap",
|
||||
"env_logger",
|
||||
"im",
|
||||
"lalrpop",
|
||||
"lalrpop-util",
|
||||
"lazy_static",
|
||||
"leptos_reactive",
|
||||
"rustyline",
|
||||
"test-log",
|
||||
"trace",
|
||||
|
|
@ -119,6 +127,12 @@ dependencies = [
|
|||
"typenum",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "bumpalo"
|
||||
version = "3.14.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7f30e7476521f6f8af1a1c4c0b8cc94f0bee37d91763d0ca2665f299b6cd8aec"
|
||||
|
||||
[[package]]
|
||||
name = "cc"
|
||||
version = "1.0.83"
|
||||
|
|
@ -145,6 +159,17 @@ dependencies = [
|
|||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "contracts"
|
||||
version = "0.6.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f1d1429e3bd78171c65aa010eabcdf8f863ba3254728dbfb0ad4b1545beac15c"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn 1.0.109",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "crunchy"
|
||||
version = "0.2.2"
|
||||
|
|
@ -277,6 +302,95 @@ version = "0.4.2"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80"
|
||||
|
||||
[[package]]
|
||||
name = "futures"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "da0290714b38af9b4a7b094b8a37086d1b4e61f2df9122c3cad2577669145335"
|
||||
dependencies = [
|
||||
"futures-channel",
|
||||
"futures-core",
|
||||
"futures-executor",
|
||||
"futures-io",
|
||||
"futures-sink",
|
||||
"futures-task",
|
||||
"futures-util",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "futures-channel"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ff4dd66668b557604244583e3e1e1eada8c5c2e96a6d0d6653ede395b78bbacb"
|
||||
dependencies = [
|
||||
"futures-core",
|
||||
"futures-sink",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "futures-core"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "eb1d22c66e66d9d72e1758f0bd7d4fd0bee04cad842ee34587d68c07e45d088c"
|
||||
|
||||
[[package]]
|
||||
name = "futures-executor"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0f4fb8693db0cf099eadcca0efe2a5a22e4550f98ed16aba6c48700da29597bc"
|
||||
dependencies = [
|
||||
"futures-core",
|
||||
"futures-task",
|
||||
"futures-util",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "futures-io"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8bf34a163b5c4c52d0478a4d757da8fb65cabef42ba90515efee0f6f9fa45aaa"
|
||||
|
||||
[[package]]
|
||||
name = "futures-macro"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "53b153fd91e4b0147f4aced87be237c98248656bb01050b96bf3ee89220a8ddb"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn 2.0.38",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "futures-sink"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e36d3378ee38c2a36ad710c5d30c2911d752cb941c00c72dbabfb786a7970817"
|
||||
|
||||
[[package]]
|
||||
name = "futures-task"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "efd193069b0ddadc69c46389b740bbccdd97203899b48d09c5f7969591d6bae2"
|
||||
|
||||
[[package]]
|
||||
name = "futures-util"
|
||||
version = "0.3.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a19526d624e703a3179b3d322efec918b6246ea0fa51d41124525f00f1cc8104"
|
||||
dependencies = [
|
||||
"futures-channel",
|
||||
"futures-core",
|
||||
"futures-io",
|
||||
"futures-macro",
|
||||
"futures-sink",
|
||||
"futures-task",
|
||||
"memchr",
|
||||
"pin-project-lite",
|
||||
"pin-utils",
|
||||
"slab",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "getrandom"
|
||||
version = "0.2.10"
|
||||
|
|
@ -371,6 +485,15 @@ version = "1.0.9"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38"
|
||||
|
||||
[[package]]
|
||||
name = "js-sys"
|
||||
version = "0.3.65"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "54c0c35952f67de54bb584e9fd912b3023117cbafc0a77d8f3dee1fb5f572fe8"
|
||||
dependencies = [
|
||||
"wasm-bindgen",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "lalrpop"
|
||||
version = "0.20.0"
|
||||
|
|
@ -409,6 +532,29 @@ version = "1.4.0"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
|
||||
|
||||
[[package]]
|
||||
name = "leptos_reactive"
|
||||
version = "0.5.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "282e84ae3e3eb30ab1eb1c881bfeea8a3cb6d6c683dc99f26f2f69ee240b148d"
|
||||
dependencies = [
|
||||
"base64",
|
||||
"cfg-if",
|
||||
"futures",
|
||||
"indexmap",
|
||||
"paste",
|
||||
"pin-project",
|
||||
"rustc-hash",
|
||||
"self_cell",
|
||||
"serde",
|
||||
"serde-wasm-bindgen",
|
||||
"serde_json",
|
||||
"slotmap",
|
||||
"thiserror",
|
||||
"tracing",
|
||||
"wasm-bindgen-futures",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.149"
|
||||
|
|
@ -552,6 +698,12 @@ dependencies = [
|
|||
"windows-targets",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "paste"
|
||||
version = "1.0.14"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "de3145af08024dea9fa9914f381a17b8fc6034dfb00f3a84013f7ff43f29ed4c"
|
||||
|
||||
[[package]]
|
||||
name = "petgraph"
|
||||
version = "0.6.4"
|
||||
|
|
@ -577,12 +729,38 @@ version = "0.5.0"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5be167a7af36ee22fe3115051bc51f6e6c7054c9348e28deb4f49bd6f705a315"
|
||||
|
||||
[[package]]
|
||||
name = "pin-project"
|
||||
version = "1.1.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fda4ed1c6c173e3fc7a83629421152e01d7b1f9b7f65fb301e490e8cfc656422"
|
||||
dependencies = [
|
||||
"pin-project-internal",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "pin-project-internal"
|
||||
version = "1.1.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4359fd9c9171ec6e8c62926d6faaf553a8dc3f64e1507e76da7911b4f6a04405"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn 2.0.38",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "pin-project-lite"
|
||||
version = "0.2.13"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8afb450f006bf6385ca15ef45d71d2288452bc3683ce2e2cacc0d18e4be60b58"
|
||||
|
||||
[[package]]
|
||||
name = "pin-utils"
|
||||
version = "0.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8b870d8c151b6f2fb93e84a13146138f05d02ed11c7e7c54f8826aaaf7c9f184"
|
||||
|
||||
[[package]]
|
||||
name = "powerfmt"
|
||||
version = "0.2.0"
|
||||
|
|
@ -714,6 +892,12 @@ version = "0.1.23"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76"
|
||||
|
||||
[[package]]
|
||||
name = "rustc-hash"
|
||||
version = "1.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2"
|
||||
|
||||
[[package]]
|
||||
name = "rustix"
|
||||
version = "0.38.21"
|
||||
|
|
@ -768,6 +952,12 @@ version = "1.2.0"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
|
||||
|
||||
[[package]]
|
||||
name = "self_cell"
|
||||
version = "1.0.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e388332cd64eb80cd595a00941baf513caffae8dce9cfd0467fc9c66397dade6"
|
||||
|
||||
[[package]]
|
||||
name = "serde"
|
||||
version = "1.0.192"
|
||||
|
|
@ -777,6 +967,17 @@ dependencies = [
|
|||
"serde_derive",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "serde-wasm-bindgen"
|
||||
version = "0.5.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f3b143e2833c57ab9ad3ea280d21fd34e285a42837aeb0ee301f4f41890fa00e"
|
||||
dependencies = [
|
||||
"js-sys",
|
||||
"serde",
|
||||
"wasm-bindgen",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "serde_derive"
|
||||
version = "1.0.192"
|
||||
|
|
@ -824,6 +1025,25 @@ dependencies = [
|
|||
"typenum",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "slab"
|
||||
version = "0.4.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8f92a496fb766b417c996b9c5e57daf2f7ad3b0bebe1ccfca4856390e3d3bb67"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "slotmap"
|
||||
version = "1.0.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e1e08e261d0e8f5c43123b7adf3e4ca1690d655377ac93a03b2c9d3e98de1342"
|
||||
dependencies = [
|
||||
"serde",
|
||||
"version_check",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "smallvec"
|
||||
version = "1.11.1"
|
||||
|
|
@ -1110,6 +1330,82 @@ version = "0.11.0+wasi-snapshot-preview1"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen"
|
||||
version = "0.2.88"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7daec296f25a1bae309c0cd5c29c4b260e510e6d813c286b19eaadf409d40fce"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"wasm-bindgen-macro",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-backend"
|
||||
version = "0.2.88"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e397f4664c0e4e428e8313a469aaa58310d302159845980fd23b0f22a847f217"
|
||||
dependencies = [
|
||||
"bumpalo",
|
||||
"log",
|
||||
"once_cell",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn 2.0.38",
|
||||
"wasm-bindgen-shared",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-futures"
|
||||
version = "0.4.38"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9afec9963e3d0994cac82455b2b3502b81a7f40f9a0d32181f7528d9f4b43e02"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"js-sys",
|
||||
"wasm-bindgen",
|
||||
"web-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-macro"
|
||||
version = "0.2.88"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5961017b3b08ad5f3fe39f1e79877f8ee7c23c5e5fd5eb80de95abc41f1f16b2"
|
||||
dependencies = [
|
||||
"quote",
|
||||
"wasm-bindgen-macro-support",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-macro-support"
|
||||
version = "0.2.88"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c5353b8dab669f5e10f5bd76df26a9360c748f054f862ff5f3f8aae0c7fb3907"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn 2.0.38",
|
||||
"wasm-bindgen-backend",
|
||||
"wasm-bindgen-shared",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-shared"
|
||||
version = "0.2.88"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0d046c5d029ba91a1ed14da14dca44b68bf2f124cfbaf741c54151fdb3e0750b"
|
||||
|
||||
[[package]]
|
||||
name = "web-sys"
|
||||
version = "0.3.65"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5db499c5f66323272151db0e666cd34f78617522fb0c1604d31a27c50c206a85"
|
||||
dependencies = [
|
||||
"js-sys",
|
||||
"wasm-bindgen",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "winapi"
|
||||
version = "0.3.9"
|
||||
|
|
|
|||
|
|
@ -7,11 +7,13 @@ edition = "2021"
|
|||
|
||||
[dependencies]
|
||||
anyhow = { version = "1.0.75", features = ["backtrace"] }
|
||||
contracts = { version = "0.6.3" }
|
||||
dashmap = "5.5.3"
|
||||
env_logger = "0.10.0"
|
||||
im = "15.1.0"
|
||||
lalrpop-util = { version = "0.20.0", features = ["lexer", "regex", "unicode"] }
|
||||
lazy_static = "1.4.0"
|
||||
leptos_reactive = "0.5.2"
|
||||
rustyline = "12.0.0"
|
||||
trace = "0.1.7"
|
||||
tracing = "0.1.40"
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@ use anyhow::{bail, Result};
|
|||
|
||||
use crate::data::{Context, ContextEntry, FreeVar, Monotype, Term, Type};
|
||||
use crate::gensym::gensym_existential;
|
||||
use crate::DEPTH;
|
||||
|
||||
|
||||
// Figure 8. Applying a context, as a substitution, to a type
|
||||
|
||||
|
|
@ -121,7 +121,7 @@ pub fn instantiate_left(
|
|||
Ok(new_ctx)
|
||||
}
|
||||
|
||||
Type::Existential(b) => todo!(),
|
||||
Type::Existential(_b) => todo!(),
|
||||
|
||||
Type::Unit => todo!(),
|
||||
Type::Var(_) => todo!(),
|
||||
|
|
@ -164,7 +164,7 @@ pub fn instantiate_right(
|
|||
let aug_b = ty_b.subst(beta, &Type::Existential(ex_b.to_owned()));
|
||||
let out_ctx = instantiate_right(&aug_ctx, &aug_b, a)?;
|
||||
|
||||
let (before, after) = out_ctx
|
||||
let (before, _after) = out_ctx
|
||||
.split_by(
|
||||
|entry| matches!(entry, ContextEntry::Marker(m) if *m == ex_b),
|
||||
)
|
||||
|
|
@ -208,11 +208,11 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
|
|||
(Term::Unit, Type::Unit) => Ok(ctx.clone()),
|
||||
|
||||
// ∀I rule
|
||||
(e, Type::Polytype(x, tyA)) => todo!(),
|
||||
(_e, Type::Polytype(_x, _tyA)) => todo!(),
|
||||
|
||||
// →I rule
|
||||
(Term::Lam(x, e), Type::Arrow(ty_a, ty_b)) => {
|
||||
let mut aug_ctx = ctx.clone();
|
||||
(Term::Lam(_x, _e), Type::Arrow(_ty_a, _ty_b)) => {
|
||||
let _aug_ctx = ctx.clone();
|
||||
todo!()
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,22 +1,25 @@
|
|||
use anyhow::{bail, Result};
|
||||
|
||||
use crate::data_debruijn::{Context, Term, Type};
|
||||
use crate::data_debruijn::{Context, ContextIndex, ContextItem, Term, Type};
|
||||
use crate::DEPTH;
|
||||
|
||||
// Figure 8. Applying a context, as a substitution, to a type
|
||||
|
||||
#[trace]
|
||||
pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
|
||||
match ty {
|
||||
Type::Unit => Ok(Type::Unit),
|
||||
Type::Var(s) => Ok(Type::Var(s.clone())),
|
||||
|
||||
Type::Existential(a) => match ctx.lookup_existential(a) {
|
||||
Some((_, Some(m))) => Ok(m.into_poly()),
|
||||
Some((_, None)) => Ok(Type::Existential(a.clone())),
|
||||
None => bail!("existential variable {a} doesn't exist in context"),
|
||||
Type::Existential(a) => match ctx.get_existential(a) {
|
||||
Some(Some(m)) => Ok(m.into_poly()),
|
||||
Some(None) => Ok(Type::Existential(a.clone())),
|
||||
None => bail!("existential variable {a:?} doesn't exist in context"),
|
||||
},
|
||||
|
||||
Type::Polytype(a, t) => {
|
||||
Ok(Type::Polytype(a.clone(), Box::new(app_ctx(ctx, t)?)))
|
||||
Type::Polytype(t) => {
|
||||
let t = app_ctx(ctx, t)?;
|
||||
Ok(Type::Polytype(Box::new(t)))
|
||||
}
|
||||
|
||||
Type::Arrow(a, b) => Ok(Type::Arrow(
|
||||
|
|
@ -26,14 +29,198 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
|
|||
}
|
||||
}
|
||||
|
||||
// Figure 9. Algorithmic subtyping
|
||||
|
||||
/// Under input context Γ , type A is a subtype of B, with output context ∆
|
||||
pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
|
||||
match (left, right) {
|
||||
// <:Unit rule
|
||||
(Type::Unit, Type::Unit) => Ok(ctx.clone()),
|
||||
|
||||
// <:Var rule
|
||||
(Type::Var(x), Type::Var(y)) if x == y && ctx.get_type(x).is_some() => {
|
||||
Ok(ctx.clone())
|
||||
}
|
||||
|
||||
// <:Exvar rule
|
||||
(Type::Existential(x), Type::Existential(y))
|
||||
if x == y && ctx.get_existential(x).is_some() =>
|
||||
{
|
||||
Ok(ctx.clone())
|
||||
}
|
||||
|
||||
// <:InstantiateL
|
||||
(Type::Existential(a) , ty_a) if ctx.get_existential(a).is_some() => {
|
||||
instantiate_left(ctx, a, ty_a)
|
||||
}
|
||||
|
||||
(Type::Unit, Type::Var(_)) => todo!(),
|
||||
(Type::Unit, Type::Existential(_)) => todo!(),
|
||||
(Type::Unit, Type::Polytype(_)) => todo!(),
|
||||
(Type::Unit, Type::Arrow(_, _)) => todo!(),
|
||||
(Type::Var(_), Type::Unit) => todo!(),
|
||||
(Type::Var(_), Type::Var(_)) => todo!(),
|
||||
(Type::Var(_), Type::Existential(_)) => todo!(),
|
||||
(Type::Var(_), Type::Polytype(_)) => todo!(),
|
||||
(Type::Var(_), Type::Arrow(_, _)) => todo!(),
|
||||
(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 between {left:?} and {right:?} (ctx = {ctx:?})"),
|
||||
}
|
||||
}
|
||||
|
||||
// Figure 10. Instantiation
|
||||
|
||||
pub fn instantiate_left(
|
||||
ctx: &Context,
|
||||
a: &ContextIndex,
|
||||
ty_a: &Type,
|
||||
) -> Result<Context> {
|
||||
match ty_a {
|
||||
// InstLReach rule
|
||||
Type::Existential(b)
|
||||
if ctx.get_existential(a).is_some()
|
||||
&& ctx.get_existential(b).is_some() =>
|
||||
{
|
||||
todo!()
|
||||
}
|
||||
|
||||
Type::Existential(_b) => todo!(),
|
||||
Type::Unit => todo!(),
|
||||
Type::Var(_) => todo!(),
|
||||
Type::Polytype(_) => todo!(),
|
||||
Type::Arrow(_, _) => todo!(),
|
||||
}
|
||||
}
|
||||
|
||||
// Figure 11. Algorithmic typing
|
||||
|
||||
#[trace]
|
||||
pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
|
||||
match (term, ty) {
|
||||
// 1I rule
|
||||
(Term::Unit, Type::Unit) => Ok(ctx.clone()),
|
||||
|
||||
// ∀I rule
|
||||
(_e, Type::Polytype(_t)) => todo!(),
|
||||
|
||||
// →I rule
|
||||
(Term::Lam(_e), Type::Arrow(_ty_a, _ty_b)) => {
|
||||
todo!()
|
||||
}
|
||||
|
||||
// Sub rule
|
||||
(term, ty) => {
|
||||
println!("SUB RULE: {term:?} || {ty:?} ({ctx:?})");
|
||||
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)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[trace]
|
||||
pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
|
||||
match term {
|
||||
// 1I⇒ rule
|
||||
Term::Unit => Ok((Type::Unit, ctx.clone())),
|
||||
|
||||
Term::Var(_) => todo!(),
|
||||
Term::Lam(_) => todo!(),
|
||||
Term::App(_, _) => todo!(),
|
||||
// Var rule
|
||||
Term::Var(index) => {
|
||||
let ty = match ctx.get_type(index) {
|
||||
Some(v) => v,
|
||||
None => bail!("invalid index {index:?}, context: {ctx:?}"),
|
||||
};
|
||||
Ok((ty, ctx.clone()))
|
||||
}
|
||||
|
||||
// →E rule
|
||||
Term::App(e1, e2) => {
|
||||
let (ty_a, ctx_theta) = synthesize(ctx, e1)?;
|
||||
let app_a = app_ctx(&ctx_theta, &ty_a)?;
|
||||
let (ty_c, ctx_delta) = app_synthesize(&ctx_theta, &app_a, &e2)?;
|
||||
Ok((ty_c, ctx_delta))
|
||||
}
|
||||
|
||||
// →I⇒' rule
|
||||
Term::Lam(e) => {
|
||||
let (aug_ctx, marker_idx) = ctx.add(ContextItem::Marker);
|
||||
let (aug_ctx, ex_a_idx) = aug_ctx.add(ContextItem::ExistentialVar);
|
||||
let (aug_ctx, ex_b_idx) = aug_ctx.add(ContextItem::ExistentialVar);
|
||||
|
||||
let ex_a = Type::Existential(ex_a_idx.clone());
|
||||
let ex_b = Type::Existential(ex_b_idx.clone());
|
||||
let (aug_ctx, _annot_idx) =
|
||||
aug_ctx.add(ContextItem::TermAnnot(ex_a.clone()));
|
||||
|
||||
let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?;
|
||||
|
||||
let (before_marker, after_marker) = wtf_ctx.split_at(&marker_idx);
|
||||
println!("Splitting: {:?}", wtf_ctx);
|
||||
let mut tau =
|
||||
app_ctx(&after_marker, &Type::Arrow(Box::new(ex_a), Box::new(ex_b)))?;
|
||||
|
||||
let (final_ctx, gen_idx) = before_marker.add(ContextItem::ExistentialVar);
|
||||
|
||||
for index in after_marker.unsolved_existentials() {
|
||||
tau = tau.subst(&index, Type::Var(gen_idx.clone()));
|
||||
}
|
||||
|
||||
Ok((Type::Polytype(Box::new(tau)), final_ctx))
|
||||
}
|
||||
|
||||
Term::Annot(_, _) => todo!(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn app_synthesize(
|
||||
_ctx: &Context,
|
||||
fun_ty: &Type,
|
||||
term: &Term,
|
||||
) -> Result<(Type, Context)> {
|
||||
match (fun_ty, term) {
|
||||
(Type::Unit, Term::Unit) => todo!(),
|
||||
(Type::Unit, Term::Var(_)) => todo!(),
|
||||
(Type::Unit, Term::Lam(_)) => todo!(),
|
||||
(Type::Unit, Term::App(_, _)) => todo!(),
|
||||
(Type::Unit, Term::Annot(_, _)) => todo!(),
|
||||
(Type::Var(_), Term::Unit) => todo!(),
|
||||
(Type::Var(_), Term::Var(_)) => todo!(),
|
||||
(Type::Var(_), Term::Lam(_)) => todo!(),
|
||||
(Type::Var(_), Term::App(_, _)) => todo!(),
|
||||
(Type::Var(_), Term::Annot(_, _)) => todo!(),
|
||||
(Type::Existential(_), Term::Unit) => todo!(),
|
||||
(Type::Existential(_), Term::Var(_)) => todo!(),
|
||||
(Type::Existential(_), Term::Lam(_)) => todo!(),
|
||||
(Type::Existential(_), Term::App(_, _)) => todo!(),
|
||||
(Type::Existential(_), Term::Annot(_, _)) => todo!(),
|
||||
(Type::Polytype(_), Term::Unit) => todo!(),
|
||||
(Type::Polytype(_), Term::Var(_)) => todo!(),
|
||||
(Type::Polytype(_), Term::Lam(_)) => todo!(),
|
||||
(Type::Polytype(_), Term::App(_, _)) => todo!(),
|
||||
(Type::Polytype(_), Term::Annot(_, _)) => todo!(),
|
||||
(Type::Arrow(_, _), Term::Unit) => todo!(),
|
||||
(Type::Arrow(_, _), Term::Var(_)) => todo!(),
|
||||
(Type::Arrow(_, _), Term::Lam(_)) => todo!(),
|
||||
(Type::Arrow(_, _), Term::App(_, _)) => todo!(),
|
||||
(Type::Arrow(_, _), Term::Annot(_, _)) => todo!(),
|
||||
|
||||
_ => bail!("trying to appSynthesize with a non-function type"),
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,57 +0,0 @@
|
|||
use crate::DEPTH;
|
||||
use crate::{data, data_debruijn, gensym::gensym_type};
|
||||
|
||||
pub fn convert_term(term: &data::Term) -> data_debruijn::Term {
|
||||
fn convert_term_with_context(
|
||||
ctx: &data::Context,
|
||||
term: &data::Term,
|
||||
) -> data_debruijn::Term {
|
||||
match term {
|
||||
data::Term::Unit => data_debruijn::Term::Unit,
|
||||
|
||||
data::Term::Var(name) => {
|
||||
let (idx, _) = ctx.lookup_type(name).unwrap();
|
||||
let ctx_len = ctx.0.len();
|
||||
data_debruijn::Term::Var(ctx_len - 1 - idx)
|
||||
}
|
||||
|
||||
data::Term::Lam(arg, body) => {
|
||||
let ty = gensym_type();
|
||||
let ctx2 = ctx.add(vec![data::ContextEntry::TermAnnot(
|
||||
arg.to_owned(),
|
||||
data::Type::Var(ty.clone()),
|
||||
)]);
|
||||
let body = convert_term_with_context(&ctx2, body);
|
||||
data_debruijn::Term::Lam(Box::new(body))
|
||||
}
|
||||
|
||||
data::Term::App(func, arg) => {
|
||||
let func = convert_term_with_context(ctx, &func);
|
||||
let arg = convert_term_with_context(ctx, &arg);
|
||||
data_debruijn::Term::App(Box::new(func), Box::new(arg))
|
||||
}
|
||||
|
||||
data::Term::Annot(term, ty) => {
|
||||
let term = convert_term_with_context(ctx, &term);
|
||||
let ty = convert_ty_with_context(ctx, &ty);
|
||||
data_debruijn::Term::Annot(Box::new(term), ty)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn convert_ty_with_context(
|
||||
ctx: &data::Context,
|
||||
ty: &data::Type,
|
||||
) -> data_debruijn::Type {
|
||||
match ty {
|
||||
data::Type::Unit => data_debruijn::Type::Unit,
|
||||
|
||||
data::Type::Var(_) => todo!(),
|
||||
data::Type::Existential(_) => todo!(),
|
||||
data::Type::Polytype(_, _) => todo!(),
|
||||
data::Type::Arrow(_, _) => todo!(),
|
||||
}
|
||||
}
|
||||
|
||||
convert_term_with_context(&data::Context::default(), term)
|
||||
}
|
||||
|
|
@ -1,9 +1,12 @@
|
|||
use std::{fmt, hash::Hash};
|
||||
use std::{
|
||||
cell::RefCell,
|
||||
fmt::{self},
|
||||
rc::Rc,
|
||||
};
|
||||
|
||||
use anyhow::{bail, Result};
|
||||
use im::{HashSet, Vector};
|
||||
use im::Vector;
|
||||
|
||||
use crate::gensym::gensym_existential;
|
||||
use crate::{data, gensym::gensym_type};
|
||||
|
||||
/// A lambda calculus term.
|
||||
#[derive(Clone)]
|
||||
|
|
@ -13,7 +16,7 @@ pub enum Term {
|
|||
|
||||
/// Variable, with a reference into the context.
|
||||
/// The entry pointed to by this index MUST be a TypeVar.
|
||||
Var(usize),
|
||||
Var(ContextIndex),
|
||||
|
||||
/// Lambda abstraction.
|
||||
Lam(Box<Term>),
|
||||
|
|
@ -29,7 +32,7 @@ impl fmt::Debug for Term {
|
|||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
match self {
|
||||
Self::Unit => write!(f, "unit"),
|
||||
Self::Var(arg0) => write!(f, "{}", arg0),
|
||||
Self::Var(arg0) => write!(f, "{:?}", arg0),
|
||||
Self::Lam(arg1) => write!(f, "(λ.{:?})", arg1),
|
||||
Self::App(arg0, arg1) => write!(f, "({:?} · {:?})", arg0, arg1),
|
||||
Self::Annot(arg0, arg1) => write!(f, "({:?} : {:?})", arg0, arg1),
|
||||
|
|
@ -40,8 +43,8 @@ impl fmt::Debug for Term {
|
|||
#[derive(Clone)]
|
||||
pub enum Type {
|
||||
Unit,
|
||||
Var(usize),
|
||||
Existential(usize),
|
||||
Var(ContextIndex),
|
||||
Existential(ContextIndex),
|
||||
Polytype(Box<Type>),
|
||||
Arrow(Box<Type>, Box<Type>),
|
||||
}
|
||||
|
|
@ -50,8 +53,8 @@ impl fmt::Debug for Type {
|
|||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
match self {
|
||||
Self::Unit => write!(f, "𝟙"),
|
||||
Self::Var(arg0) => write!(f, "{}", arg0),
|
||||
Self::Existential(arg0) => write!(f, "{}", arg0),
|
||||
Self::Var(arg0) => write!(f, "{:?}", arg0),
|
||||
Self::Existential(arg0) => write!(f, "{:?}", arg0),
|
||||
Self::Polytype(arg1) => write!(f, "(∀.{:?})", arg1),
|
||||
Self::Arrow(arg0, arg1) => write!(f, "({:?} -> {:?})", arg0, arg1),
|
||||
}
|
||||
|
|
@ -65,8 +68,8 @@ impl Type {
|
|||
pub fn try_into_mono(&self) -> Option<Monotype> {
|
||||
match self {
|
||||
Type::Unit => Some(Monotype::Unit),
|
||||
Type::Var(x) => Some(Monotype::Var(*x)),
|
||||
Type::Existential(x) => Some(Monotype::Existential(*x)),
|
||||
Type::Var(x) => Some(Monotype::Var(x.clone())),
|
||||
Type::Existential(x) => Some(Monotype::Existential(x.clone())),
|
||||
|
||||
// Polytypes cannot be converted to monotypes
|
||||
Type::Polytype(_) => None,
|
||||
|
|
@ -126,13 +129,23 @@ impl Type {
|
|||
// ),
|
||||
// }
|
||||
// }
|
||||
|
||||
pub fn subst(&self, _before: &ContextIndex, _after: Type) -> Type {
|
||||
match self {
|
||||
Type::Unit => Type::Unit,
|
||||
Type::Var(_) => todo!(),
|
||||
Type::Existential(_) => todo!(),
|
||||
Type::Polytype(_) => todo!(),
|
||||
Type::Arrow(_, _) => todo!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
pub enum Monotype {
|
||||
Unit,
|
||||
Var(usize),
|
||||
Existential(usize),
|
||||
Var(ContextIndex),
|
||||
Existential(ContextIndex),
|
||||
Arrow(Box<Monotype>, Box<Monotype>),
|
||||
}
|
||||
|
||||
|
|
@ -140,8 +153,8 @@ impl fmt::Debug for Monotype {
|
|||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
match self {
|
||||
Self::Unit => write!(f, "𝟙"),
|
||||
Self::Var(arg0) => write!(f, "{}", arg0),
|
||||
Self::Existential(arg0) => write!(f, "{}", arg0),
|
||||
Self::Var(arg0) => write!(f, "{:?}", arg0),
|
||||
Self::Existential(arg0) => write!(f, "{:?}", arg0),
|
||||
Self::Arrow(arg0, arg1) => write!(f, "({arg0:?} -> {arg1:?})"),
|
||||
}
|
||||
}
|
||||
|
|
@ -160,24 +173,25 @@ impl Monotype {
|
|||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum ContextItem {
|
||||
TypeVar,
|
||||
TermAnnot(Type),
|
||||
ExistentialVar,
|
||||
ExistentialSolved(Monotype),
|
||||
Marker,
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
pub enum ContextEntry {
|
||||
TypeVar(String),
|
||||
TermAnnot(String, Type),
|
||||
ExistentialVar(String),
|
||||
ExistentialSolved(String, Monotype),
|
||||
Marker(String),
|
||||
pub struct ContextEntry {
|
||||
item: ContextItem,
|
||||
index_from_start: usize,
|
||||
index_from_end: usize,
|
||||
}
|
||||
|
||||
impl fmt::Debug for ContextEntry {
|
||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
match self {
|
||||
Self::TypeVar(arg0) => write!(f, "{}", arg0),
|
||||
Self::TermAnnot(arg0, arg1) => write!(f, "{} : {:?}", arg0, arg1),
|
||||
Self::ExistentialVar(arg0) => write!(f, "{}", arg0),
|
||||
Self::ExistentialSolved(arg0, arg1) => write!(f, "{} ≔ {:?}", arg0, arg1),
|
||||
Self::Marker(arg0) => write!(f, "▶{}", arg0),
|
||||
}
|
||||
write!(f, "{:?}", self.item)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -189,159 +203,222 @@ pub enum CompleteContextEntry {
|
|||
Marker(String),
|
||||
}
|
||||
|
||||
#[derive(Clone, Default)]
|
||||
pub struct Context(pub(crate) Vector<ContextEntry>);
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct Context {
|
||||
vector: Vector<Rc<RefCell<ContextEntry>>>,
|
||||
len: Rc<RefCell<usize>>,
|
||||
// len: ReadSignal<usize>,
|
||||
// set_len: WriteSignal<usize>,
|
||||
}
|
||||
|
||||
impl fmt::Debug for Context {
|
||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
f.write_str("Γ")?;
|
||||
for rule in self.0.iter() {
|
||||
f.write_str(", ")?;
|
||||
rule.fmt(f)?;
|
||||
// impl fmt::Debug for Context {
|
||||
// fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
// f.write_str("Γ")?;
|
||||
// for rule in self.vector.iter() {
|
||||
// f.write_str(", ")?;
|
||||
// rule.fmt(f)?;
|
||||
// }
|
||||
// Ok(())
|
||||
// }
|
||||
// }
|
||||
|
||||
impl Default for Context {
|
||||
fn default() -> Self {
|
||||
let vector = Vector::default();
|
||||
// let (len, set_len) = create_signal(0);
|
||||
let len = Rc::new(RefCell::new(0));
|
||||
|
||||
Context {
|
||||
vector,
|
||||
len,
|
||||
// len,
|
||||
// set_len,
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Context {
|
||||
pub fn add(&self, entries: Vec<ContextEntry>) -> Context {
|
||||
pub fn add(&self, item: ContextItem) -> (Context, ContextIndex) {
|
||||
let context_level = self.vector.len();
|
||||
let mut new_ctx = self.clone();
|
||||
for entry in entries {
|
||||
new_ctx.0.push_back(entry);
|
||||
}
|
||||
new_ctx
|
||||
new_ctx.vector.push_back(Rc::new(RefCell::new(ContextEntry {
|
||||
item,
|
||||
index_from_end: 0,
|
||||
index_from_start: self.vector.len(),
|
||||
})));
|
||||
|
||||
let context_length = Rc::new(RefCell::new(new_ctx.vector.len()));
|
||||
// let context_length = self.len.clone();
|
||||
// {
|
||||
// *context_length.borrow_mut() += 1;
|
||||
// }
|
||||
|
||||
// let context_index =
|
||||
// create_memo(move |_| context_length.get() - context_level);
|
||||
let idx = ContextIndex {
|
||||
context_level,
|
||||
context_length,
|
||||
// context_index,
|
||||
};
|
||||
(new_ctx, idx)
|
||||
}
|
||||
|
||||
/// Looks up a polytype by name, also returning an index
|
||||
pub fn lookup_type(&self, name: impl AsRef<str>) -> Option<(usize, Type)> {
|
||||
self
|
||||
.0
|
||||
.iter()
|
||||
.enumerate()
|
||||
.find_map(|(i, entry)| match entry {
|
||||
ContextEntry::TermAnnot(n, t) if n == name.as_ref() => {
|
||||
Some((i, t.clone()))
|
||||
}
|
||||
_ => None,
|
||||
})
|
||||
pub fn get<'a>(&'a self, index: &ContextIndex) -> Option<ContextItem> {
|
||||
let entry = self.vector.get(index.context_level)?;
|
||||
let entry = entry.borrow();
|
||||
Some(entry.item.clone())
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn has_type(&self, name: impl AsRef<str>) -> bool {
|
||||
self.lookup_type(name).is_some()
|
||||
}
|
||||
|
||||
/// Looks up an existential variable by name
|
||||
/// - Returns Some(Some(t)) if solved
|
||||
/// - Returns Some(None) if exists but unsolved
|
||||
/// - Returns None if not found
|
||||
pub fn lookup_existential(
|
||||
pub fn get_existential(
|
||||
&self,
|
||||
name: impl AsRef<str>,
|
||||
) -> Option<(usize, Option<Monotype>)> {
|
||||
self
|
||||
.0
|
||||
.iter()
|
||||
.enumerate()
|
||||
.find_map(|(i, entry)| match entry {
|
||||
ContextEntry::ExistentialVar(n) if n == name.as_ref() => {
|
||||
Some((i, None))
|
||||
}
|
||||
ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => {
|
||||
Some((i, Some(t.clone())))
|
||||
}
|
||||
_ => None,
|
||||
})
|
||||
index: &ContextIndex,
|
||||
) -> Option<Option<Monotype>> {
|
||||
let item = self.get(index)?;
|
||||
|
||||
match item {
|
||||
ContextItem::ExistentialSolved(t) => Some(Some(t.clone())),
|
||||
ContextItem::ExistentialVar => Some(None),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn has_existential(&self, name: impl AsRef<str>) -> bool {
|
||||
self.lookup_existential(name).is_some()
|
||||
pub fn get_type(&self, index: &ContextIndex) -> Option<Type> {
|
||||
let item = self.get(index)?;
|
||||
|
||||
match item {
|
||||
ContextItem::TermAnnot(t) => Some(t.clone()),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
|
||||
/// Returns a list of names of unsolved existentials
|
||||
pub fn unsolved_existentials(&self) -> HashSet<String> {
|
||||
let mut unsolved = HashSet::new();
|
||||
|
||||
for entry in self.0.iter() {
|
||||
match entry {
|
||||
ContextEntry::ExistentialVar(n) => {
|
||||
unsolved.insert(n.clone());
|
||||
pub fn unsolved_existentials(&self) -> Vec<ContextIndex> {
|
||||
let mut unsolved = Vec::new();
|
||||
let context_length = self.len.clone();
|
||||
for (context_level, entry) in self.vector.iter().enumerate() {
|
||||
match entry.borrow().item {
|
||||
ContextItem::ExistentialVar => {
|
||||
let index = ContextIndex {
|
||||
context_length: context_length.clone(),
|
||||
context_level,
|
||||
};
|
||||
unsolved.push(index)
|
||||
}
|
||||
_ => {}
|
||||
}
|
||||
}
|
||||
|
||||
unsolved
|
||||
}
|
||||
|
||||
/// Returns (before, after)
|
||||
pub fn split_by<P>(&self, p: P) -> Option<(Context, Context)>
|
||||
where
|
||||
P: Fn(&ContextEntry) -> bool,
|
||||
{
|
||||
/// Splits the context
|
||||
pub fn split_at(&self, index: &ContextIndex) -> (Context, Context) {
|
||||
let (before, after) = {
|
||||
let idx = self.0.iter().position(p)?;
|
||||
self.0.clone().split_at(idx)
|
||||
// let idx = self.vector.iter().position(p)?;
|
||||
self.vector.clone().split_at(index.context_level)
|
||||
};
|
||||
|
||||
Some((Context(before), Context(after)))
|
||||
let before_len = Rc::new(RefCell::new(before.len()));
|
||||
let after_len = Rc::new(RefCell::new(after.len()));
|
||||
|
||||
(
|
||||
Context {
|
||||
vector: before,
|
||||
len: before_len,
|
||||
},
|
||||
Context {
|
||||
vector: after,
|
||||
len: after_len,
|
||||
},
|
||||
)
|
||||
}
|
||||
|
||||
pub fn unsplit(
|
||||
left: &Context,
|
||||
center: ContextEntry,
|
||||
right: &Context,
|
||||
) -> Context {
|
||||
let mut res = left.clone();
|
||||
res.0.push_back(center);
|
||||
res.0.extend(right.0.clone().into_iter());
|
||||
res
|
||||
}
|
||||
|
||||
// pub fn split_existential_function(&self, var: &str) -> Result<(String, String, Context)> {
|
||||
// let mut ctx = self.clone();
|
||||
// let idx = match ctx.lookup_existential(var) {
|
||||
// Some((idx, _)) => idx,
|
||||
// None => bail!("wtf?"),
|
||||
// };
|
||||
|
||||
// let ex_a1_s = gensym_existential();
|
||||
// let ex_a2_s = gensym_existential();
|
||||
// ctx.0[idx] = ContextEntry::ExistentialSolved(
|
||||
// var.to_owned(),
|
||||
// Monotype::Arrow(
|
||||
// Box::new(Monotype::Existential(ex_a1_s.to_owned())),
|
||||
// Box::new(Monotype::Existential(ex_a2_s.to_owned())),
|
||||
// ),
|
||||
// );
|
||||
// ctx
|
||||
// .0
|
||||
// .insert(idx, ContextEntry::ExistentialVar(ex_a1_s.to_owned()));
|
||||
// ctx
|
||||
// .0
|
||||
// .insert(idx, ContextEntry::ExistentialVar(ex_a2_s.to_owned()));
|
||||
|
||||
// Ok((ex_a1_s, ex_a2_s, ctx))
|
||||
// }
|
||||
}
|
||||
|
||||
/// An index into the context.
|
||||
#[derive(Clone, PartialEq, Eq)]
|
||||
pub struct ContextIndex {
|
||||
context_length: usize,
|
||||
context_index: usize,
|
||||
context_length: Rc<RefCell<usize>>,
|
||||
// context_length: ReadSignal<usize>,
|
||||
// context_index: Memo<usize>,
|
||||
context_level: usize,
|
||||
}
|
||||
|
||||
impl ContextIndex {
|
||||
/// Bump an index, creating a new one when entering a new context level
|
||||
///
|
||||
/// This should ensure the index is still referring to the same context entry.
|
||||
pub fn bump(&self) -> Self {
|
||||
ContextIndex {
|
||||
context_length: self.context_length + 1,
|
||||
context_index: self.context_index + 1,
|
||||
context_level: self.context_level,
|
||||
}
|
||||
impl fmt::Debug for ContextIndex {
|
||||
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
|
||||
write!(f, "#{}", self.context_index())
|
||||
}
|
||||
}
|
||||
|
||||
impl ContextIndex {
|
||||
pub fn context_index(&self) -> usize {
|
||||
*self.context_length.borrow() - self.context_level
|
||||
}
|
||||
}
|
||||
|
||||
/* Convert */
|
||||
|
||||
pub fn convert_term(term: &data::Term) -> Term {
|
||||
fn convert_term_with_context(
|
||||
ctx: &data::Context,
|
||||
ctx2: &Context,
|
||||
term: &data::Term,
|
||||
) -> Term {
|
||||
match term {
|
||||
data::Term::Unit => Term::Unit,
|
||||
|
||||
data::Term::Var(name) => {
|
||||
let (idx, _) = ctx.lookup_type(name).unwrap();
|
||||
|
||||
let _len = ctx2.len.clone();
|
||||
// let context_index = create_memo(move |_| len.get() - idx);
|
||||
let index = ContextIndex {
|
||||
context_length: ctx2.len.clone(),
|
||||
context_level: idx,
|
||||
// context_index,
|
||||
};
|
||||
Term::Var(index)
|
||||
}
|
||||
|
||||
data::Term::Lam(arg, body) => {
|
||||
let ty = gensym_type();
|
||||
let aug_ctx = ctx.add(vec![data::ContextEntry::TermAnnot(
|
||||
arg.to_owned(),
|
||||
data::Type::Var(ty.clone()),
|
||||
)]);
|
||||
let body = convert_term_with_context(&aug_ctx, ctx2, body);
|
||||
Term::Lam(Box::new(body))
|
||||
}
|
||||
|
||||
data::Term::App(func, arg) => {
|
||||
let func = convert_term_with_context(ctx, ctx2, &func);
|
||||
let arg = convert_term_with_context(ctx, ctx2, &arg);
|
||||
Term::App(Box::new(func), Box::new(arg))
|
||||
}
|
||||
|
||||
data::Term::Annot(term, ty) => {
|
||||
let term = convert_term_with_context(ctx, ctx2, &term);
|
||||
let ty = convert_ty_with_context(ctx, ctx2, &ty);
|
||||
Term::Annot(Box::new(term), ty)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn convert_ty_with_context(
|
||||
_ctx: &data::Context,
|
||||
_ctx2: &Context,
|
||||
ty: &data::Type,
|
||||
) -> Type {
|
||||
match ty {
|
||||
data::Type::Unit => Type::Unit,
|
||||
|
||||
data::Type::Var(_) => todo!(),
|
||||
data::Type::Existential(_) => todo!(),
|
||||
data::Type::Polytype(_, _) => todo!(),
|
||||
data::Type::Arrow(_, _) => todo!(),
|
||||
}
|
||||
}
|
||||
|
||||
convert_term_with_context(
|
||||
&data::Context::default(),
|
||||
&Context::default(),
|
||||
term,
|
||||
)
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
use dashmap::DashMap;
|
||||
use lazy_static::lazy_static;
|
||||
|
||||
|
||||
thread_local! {
|
||||
static CTRMAP: DashMap<&'static str, usize> = DashMap::new();
|
||||
|
|
|
|||
|
|
@ -1,4 +1,6 @@
|
|||
#[macro_use]
|
||||
extern crate contracts;
|
||||
#[macro_use]
|
||||
extern crate tracing;
|
||||
#[macro_use]
|
||||
extern crate trace;
|
||||
|
|
@ -9,8 +11,6 @@ pub mod abstract_data;
|
|||
pub mod bidir;
|
||||
pub mod data;
|
||||
|
||||
pub mod convert_data;
|
||||
|
||||
pub mod bidir_debruijn;
|
||||
pub mod data_debruijn;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
use anyhow::Result;
|
||||
use bidir::{
|
||||
bidir::{app_ctx, synthesize},
|
||||
convert_data::convert_term,
|
||||
data::Context,
|
||||
bidir_debruijn::{app_ctx, synthesize},
|
||||
data_debruijn::convert_term,
|
||||
data_debruijn::Context,
|
||||
parser::TermParser,
|
||||
};
|
||||
use rustyline::{Config, DefaultEditor};
|
||||
|
|
@ -30,11 +30,11 @@ fn main() -> Result<()> {
|
|||
};
|
||||
println!("parsed: {:?}", parsed_term);
|
||||
|
||||
let ctx = Context::default();
|
||||
let converted_term = convert_term(&parsed_term);
|
||||
println!("converted: {converted_term:?}");
|
||||
|
||||
let (ty, out_ctx) = match synthesize(&ctx, &parsed_term) {
|
||||
let ctx = Context::default();
|
||||
let (ty, out_ctx) = match synthesize(&ctx, &converted_term) {
|
||||
Ok(v) => v,
|
||||
Err(err) => {
|
||||
eprintln!("typecheck error: {err}");
|
||||
|
|
|
|||
|
|
@ -2,9 +2,8 @@ use anyhow::{bail, Result};
|
|||
|
||||
use crate::{
|
||||
bidir_debruijn::{app_ctx, synthesize},
|
||||
convert_data::convert_term,
|
||||
data_debruijn::Context,
|
||||
data_debruijn::Term,
|
||||
data_debruijn::{convert_term, Term},
|
||||
parser::TermParser,
|
||||
};
|
||||
|
||||
|
|
@ -16,12 +15,11 @@ fn term_of(str: &'static str) -> Result<Term> {
|
|||
}
|
||||
|
||||
#[test]
|
||||
fn test_id() -> Result<()> {
|
||||
fn test_id_only() -> Result<()> {
|
||||
let id = term_of(r"\x.x")?;
|
||||
let ctx = Context::default();
|
||||
let (ty, out_ctx) = synthesize(&ctx, &id)?;
|
||||
bail!("Synthesized: {:?} (context = {:?})", ty, out_ctx);
|
||||
|
||||
Ok(())
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue