From f479cf0420e91c0389838cba478cc6a90622f84e Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 29 Nov 2023 20:54:43 -0600 Subject: [PATCH] id typechecks --- Cargo.lock | 12 ++ bidir/Cargo.toml | 1 + bidir/src/bidir.rs | 1 - bidir/src/bidir_debruijn.rs | 78 ++++++---- bidir/src/data_debruijn.rs | 283 ++++++++++++++++++++++-------------- bidir/src/lib.rs | 5 + bidir/src/tests.rs | 8 +- 7 files changed, 248 insertions(+), 140 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 58b35f8..108118e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -78,6 +78,7 @@ dependencies = [ "anyhow", "contracts", "dashmap", + "derivative", "env_logger", "im", "lalrpop", @@ -198,6 +199,17 @@ dependencies = [ "powerfmt", ] +[[package]] +name = "derivative" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b" +dependencies = [ + "proc-macro2", + "quote", + "syn 1.0.109", +] + [[package]] name = "diff" version = "0.1.13" diff --git a/bidir/Cargo.toml b/bidir/Cargo.toml index 80a2052..89890e2 100644 --- a/bidir/Cargo.toml +++ b/bidir/Cargo.toml @@ -9,6 +9,7 @@ edition = "2021" anyhow = { version = "1.0.75", features = ["backtrace"] } contracts = { version = "0.6.3" } dashmap = "5.5.3" +derivative = "2.2.0" env_logger = "0.10.0" im = "15.1.0" lalrpop-util = { version = "0.20.0", features = ["lexer", "regex", "unicode"] } diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs index 88543a1..b48dd15 100644 --- a/bidir/src/bidir.rs +++ b/bidir/src/bidir.rs @@ -3,7 +3,6 @@ use anyhow::{bail, Result}; use crate::data::{Context, ContextEntry, FreeVar, Monotype, Term, Type}; use crate::gensym::gensym_existential; - // Figure 8. Applying a context, as a substitution, to a type #[cfg_attr(feature = "trace_execution", trace)] diff --git a/bidir/src/bidir_debruijn.rs b/bidir/src/bidir_debruijn.rs index aade19b..34b2aa7 100644 --- a/bidir/src/bidir_debruijn.rs +++ b/bidir/src/bidir_debruijn.rs @@ -1,6 +1,8 @@ use anyhow::{bail, Result}; -use crate::data_debruijn::{Context, ContextIndex, ContextItem, Term, Type}; +use crate::data_debruijn::{ + Context, ContextEntry, ContextIndex, Monotype, Term, Type, +}; use crate::DEPTH; // Figure 8. Applying a context, as a substitution, to a type @@ -54,7 +56,7 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result { instantiate_left(ctx, a, ty_a) } - (Type::Unit, Type::Var(_)) => todo!(), + (Type::Unit, Type::Var(_)) => todo!("wtf? {left:?} {right:?}"), (Type::Unit, Type::Existential(_)) => todo!(), (Type::Unit, Type::Polytype(_)) => todo!(), (Type::Unit, Type::Arrow(_, _)) => todo!(), @@ -96,7 +98,19 @@ pub fn instantiate_left( if ctx.get_existential(a).is_some() && ctx.get_existential(b).is_some() => { - todo!() + let mut new_ctx = ctx.clone(); + { + let b_entry = new_ctx + .vector + .get_mut(b.debruijn_level) + .expect("should exist"); + + *b_entry = + ContextEntry::ExistentialSolved(Monotype::Existential(a.to_owned())); + } + + Ok(new_ctx) + // todo!("helloge: a={a:?} , b={b:?} // {ctx:?}") } Type::Existential(_b) => todo!(), @@ -125,7 +139,6 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result { // 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)?; @@ -145,7 +158,7 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { Term::Var(index) => { let ty = match ctx.get_type(index) { Some(v) => v, - None => bail!("invalid index {index:?}, context: {ctx:?}"), + None => bail!("no TermAnnot at index {index:?} of context: {ctx:?}"), }; Ok((ty, ctx.clone())) } @@ -160,23 +173,31 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { // →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 (aug_ctx, marker_idx) = ctx.add(ContextEntry::Marker); + let (aug_ctx_at_a, ex_a_idx) = aug_ctx.add(ContextEntry::ExistentialVar); + let (aug_ctx_at_b, ex_b_idx) = + aug_ctx_at_a.add(ContextEntry::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 (aug_ctx, _annot_idx) = + aug_ctx_at_b.add(ContextEntry::TermAnnot(ex_a.clone())); + + let ex_a_2 = ex_b.bump_indexes(&aug_ctx_at_a, &aug_ctx, 2); + let ex_b_2 = ex_b.bump_indexes(&aug_ctx_at_b, &aug_ctx, 1); + + // TODO: Rewrite all indexes in this term + let e_2 = e.bump_indexes(ctx, &aug_ctx, 0); + + let wtf_ctx = typecheck(&aug_ctx, &e_2, &ex_b_2)?; 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 tau = Type::Arrow(Box::new(ex_a_2), Box::new(ex_b)); + let mut tau = app_ctx(&after_marker, &tau)?; - let (final_ctx, gen_idx) = before_marker.add(ContextItem::ExistentialVar); + let (final_ctx, gen_idx) = + before_marker.add(ContextEntry::ExistentialVar); for index in after_marker.unsolved_existentials() { tau = tau.subst(&index, Type::Var(gen_idx.clone())); @@ -190,11 +211,26 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { } pub fn app_synthesize( - _ctx: &Context, + ctx: &Context, fun_ty: &Type, term: &Term, ) -> Result<(Type, Context)> { match (fun_ty, term) { + // →App rule + (Type::Arrow(ty_a, ty_c), e) => { + let out_ctx = typecheck(ctx, e, ty_a)?; + Ok((*ty_c.clone(), out_ctx)) + } + + // ∀App rule + (Type::Polytype(ty_a), e) => { + let (aug_ctx, a_idx) = ctx.add(ContextEntry::ExistentialVar); + let aug_ty = ty_a.subst(&a_idx, Type::Existential(a_idx.clone())); + let (ty, ctx_delta) = app_synthesize(&aug_ctx, &aug_ty, e)?; + + Ok((ty, ctx_delta)) + } + (Type::Unit, Term::Unit) => todo!(), (Type::Unit, Term::Var(_)) => todo!(), (Type::Unit, Term::Lam(_)) => todo!(), @@ -210,16 +246,6 @@ pub fn app_synthesize( (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"), } diff --git a/bidir/src/data_debruijn.rs b/bidir/src/data_debruijn.rs index 082052d..0110487 100644 --- a/bidir/src/data_debruijn.rs +++ b/bidir/src/data_debruijn.rs @@ -1,8 +1,4 @@ -use std::{ - cell::RefCell, - fmt::{self}, - rc::Rc, -}; +use std::fmt::{self}; use im::Vector; @@ -40,6 +36,40 @@ impl fmt::Debug for Term { } } +impl Term { + pub fn bump_indexes( + &self, + old_ctx: &Context, + new_ctx: &Context, + by: usize, + ) -> Term { + match self { + Term::Unit => Term::Unit, + Term::Var(index) => { + let debruijn_index = index.debruijn_index + by; + let debruijn_level = new_ctx.vector.len() - 1 - debruijn_index; + let new_index = ContextIndex { + debruijn_index, + debruijn_level, + }; + Term::Var(new_index) + } + Term::Lam(body) => { + Term::Lam(Box::new(body.bump_indexes(old_ctx, new_ctx, by))) + } + Term::App(e1, e2) => Term::App( + Box::new(e1.bump_indexes(old_ctx, new_ctx, by)), + Box::new(e2.bump_indexes(old_ctx, new_ctx, by)), + ), + Term::Annot(e, ty) => + // TODO: Should i bump indexes in the type too (PROBABLY) + { + Term::Annot(Box::new(e.bump_indexes(old_ctx, new_ctx, by)), ty.clone()) + } + } + } +} + #[derive(Clone)] pub enum Type { Unit, @@ -85,6 +115,29 @@ impl Type { pub fn is_mono(&self) -> bool { self.try_into_mono().is_some() } + + pub fn bump_indexes( + &self, + old_ctx: &Context, + new_ctx: &Context, + by: usize, + ) -> Type { + match self { + Type::Unit => Type::Unit, + Type::Var(_) => todo!(), + Type::Existential(index) => { + let debruijn_index = index.debruijn_index + by; + let debruijn_level = new_ctx.vector.len() - 1 - debruijn_index; + let new_index = ContextIndex { + debruijn_index, + debruijn_level, + }; + Type::Existential(new_index) + } + Type::Polytype(_) => todo!(), + Type::Arrow(_, _) => todo!(), + } + } } impl Type { @@ -130,18 +183,29 @@ impl Type { // } // } - pub fn subst(&self, _before: &ContextIndex, _after: Type) -> Type { + pub fn subst(&self, before: &ContextIndex, after: Type) -> Type { match self { Type::Unit => Type::Unit, - Type::Var(_) => todo!(), - Type::Existential(_) => todo!(), + Type::Var(index) if index.debruijn_level == before.debruijn_level => { + after + } + Type::Var(index) => Type::Var(index.clone()), + Type::Existential(index) + if index.debruijn_level == before.debruijn_level => + { + after + } + Type::Existential(index) => Type::Existential(index.clone()), Type::Polytype(_) => todo!(), - Type::Arrow(_, _) => todo!(), + Type::Arrow(a, b) => Type::Arrow( + Box::new(a.subst(before, after.clone())), + Box::new(b.subst(before, after.clone())), + ), } } } -#[derive(Clone)] +#[derive(Debug, Clone)] pub enum Monotype { Unit, Var(ContextIndex), @@ -149,17 +213,6 @@ pub enum Monotype { Arrow(Box, Box), } -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::Arrow(arg0, arg1) => write!(f, "({arg0:?} -> {arg1:?})"), - } - } -} - impl Monotype { pub fn into_poly(&self) -> Type { match self { @@ -174,7 +227,7 @@ impl Monotype { } #[derive(Debug, Clone)] -pub enum ContextItem { +pub enum ContextEntry { TypeVar, TermAnnot(Type), ExistentialVar, @@ -182,19 +235,6 @@ pub enum ContextItem { Marker, } -#[derive(Clone)] -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 { - write!(f, "{:?}", self.item) - } -} - #[derive(Debug, Clone)] pub enum CompleteContextEntry { TypeVar(String), @@ -205,10 +245,8 @@ pub enum CompleteContextEntry { #[derive(Debug, Clone)] pub struct Context { - vector: Vector>>, - len: Rc>, - // len: ReadSignal, - // set_len: WriteSignal, + // TODO: Make this not pub(crate) + pub(crate) vector: Vector, } // impl fmt::Debug for Context { @@ -225,48 +263,27 @@ pub struct Context { 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, - } + Context { vector } } } impl Context { - pub fn add(&self, item: ContextItem) -> (Context, ContextIndex) { - let context_level = self.vector.len(); - let mut new_ctx = self.clone(); - new_ctx.vector.push_back(Rc::new(RefCell::new(ContextEntry { - item, - index_from_end: 0, - index_from_start: self.vector.len(), - }))); + pub fn add(&self, item: ContextEntry) -> (Context, ContextIndex) { + let idx = self.vector.len(); + let mut new_ctx = self.bump_indexes(1); + new_ctx.vector.push_back(item); - 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, + debruijn_index: 0, + debruijn_level: idx, }; (new_ctx, idx) } - pub fn get<'a>(&'a self, index: &ContextIndex) -> Option { - let entry = self.vector.get(index.context_level)?; - let entry = entry.borrow(); - Some(entry.item.clone()) + pub fn get<'a>(&'a self, index: &ContextIndex) -> Option<&ContextEntry> { + let item = self.vector.get(index.debruijn_level)?; + Some(item) } pub fn get_existential( @@ -276,8 +293,8 @@ impl Context { let item = self.get(index)?; match item { - ContextItem::ExistentialSolved(t) => Some(Some(t.clone())), - ContextItem::ExistentialVar => Some(None), + ContextEntry::ExistentialSolved(t) => Some(Some(t.clone())), + ContextEntry::ExistentialVar => Some(None), _ => None, } } @@ -286,20 +303,19 @@ impl Context { let item = self.get(index)?; match item { - ContextItem::TermAnnot(t) => Some(t.clone()), + ContextEntry::TermAnnot(t) => Some(t.clone()), _ => None, } } pub fn unsolved_existentials(&self) -> Vec { 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 => { + for (idx, item) in self.vector.iter().enumerate() { + match item { + ContextEntry::ExistentialVar => { let index = ContextIndex { - context_length: context_length.clone(), - context_level, + debruijn_level: idx, + debruijn_index: self.vector.len() - idx, }; unsolved.push(index) } @@ -313,43 +329,95 @@ impl Context { pub fn split_at(&self, index: &ContextIndex) -> (Context, Context) { let (before, after) = { // let idx = self.vector.iter().position(p)?; - self.vector.clone().split_at(index.context_level) + self.vector.clone().split_at(index.debruijn_level) }; - let before_len = Rc::new(RefCell::new(before.len())); - let after_len = Rc::new(RefCell::new(after.len())); + (Context { vector: before }, Context { vector: after }) + } - ( - Context { - vector: before, - len: before_len, - }, - Context { - vector: after, - len: after_len, - }, - ) + pub fn is_valid(&self) -> bool { + for item in self.vector.iter() { + match item { + ContextEntry::TermAnnot(_) => todo!(), + ContextEntry::ExistentialSolved(_) => todo!(), + _ => {} + } + } + true + } + + pub fn ensure_validity(&self) -> bool { + fn ensure_item_validity(ctx: &Context, item: &ContextEntry) -> bool { + match item { + ContextEntry::TermAnnot(ty) => ensure_type_validity(ctx, ty), + ContextEntry::ExistentialSolved(ty) => { + ensure_monotype_validity(ctx, ty) + } + _ => true, + } + } + + fn ensure_type_validity(ctx: &Context, ty: &Type) -> bool { + match ty { + Type::Var(idx) => ensure_index_validity(ctx, idx), + Type::Existential(idx) => ensure_index_validity(ctx, idx), + Type::Polytype(ty) => ensure_type_validity(ctx, ty), + Type::Arrow(ty1, ty2) => { + ensure_type_validity(ctx, ty1) && ensure_type_validity(ctx, ty2) + } + _ => true, + } + } + + fn ensure_monotype_validity(ctx: &Context, ty: &Monotype) -> bool { + match ty { + Monotype::Var(idx) => ensure_index_validity(ctx, idx), + Monotype::Existential(idx) => ensure_index_validity(ctx, idx), + Monotype::Arrow(ty1, ty2) => { + ensure_monotype_validity(ctx, ty1) + && ensure_monotype_validity(ctx, ty2) + } + _ => true, + } + } + + fn ensure_index_validity(ctx: &Context, idx: &ContextIndex) -> bool { + idx.debruijn_index + idx.debruijn_level == ctx.vector.len() + } + + self + .vector + .iter() + .all(|item| ensure_item_validity(self, item)) + } + + pub fn bump_indexes(&self, by: usize) -> Context { + Context { + vector: self + .vector + .iter() + .map(|entry| match entry { + ContextEntry::TypeVar => ContextEntry::TypeVar, + ContextEntry::TermAnnot(_) => todo!(), + ContextEntry::ExistentialVar => ContextEntry::ExistentialVar, + ContextEntry::ExistentialSolved(_) => todo!(), + ContextEntry::Marker => ContextEntry::Marker, + }) + .collect(), + } } } /// An index into the context. #[derive(Clone, PartialEq, Eq)] pub struct ContextIndex { - context_length: Rc>, - // context_length: ReadSignal, - // context_index: Memo, - context_level: usize, + pub(crate) debruijn_index: usize, + pub(crate) debruijn_level: usize, } 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 + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "#{}/{}", self.debruijn_level, self.debruijn_index) } } @@ -367,12 +435,9 @@ pub fn convert_term(term: &data::Term) -> Term { 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, + debruijn_index: 0, + debruijn_level: ctx.0.len(), }; Term::Var(index) } diff --git a/bidir/src/lib.rs b/bidir/src/lib.rs index 0f7dbcb..6fd43c0 100644 --- a/bidir/src/lib.rs +++ b/bidir/src/lib.rs @@ -1,12 +1,17 @@ #[macro_use] extern crate contracts; #[macro_use] +extern crate derivative; +#[macro_use] extern crate tracing; #[macro_use] extern crate trace; use lalrpop_util::lalrpop_mod; +// #[macro_export] +// pub mod fmt; + pub mod abstract_data; pub mod bidir; pub mod data; diff --git a/bidir/src/tests.rs b/bidir/src/tests.rs index 94e0553..c66cfe0 100644 --- a/bidir/src/tests.rs +++ b/bidir/src/tests.rs @@ -19,7 +19,7 @@ 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); + bail!("[test] Synthesized: {:?} (context = {:?})", ty, out_ctx); Ok(()) } @@ -29,8 +29,8 @@ fn test_id_of_unit() -> Result<()> { let ctx = Context::default(); let (ty, out_ctx) = synthesize(&ctx, &id_of_unit)?; - let wtf = app_ctx(&out_ctx, &ty); - println!("WTF: {wtf:?}"); - bail!("Synthesized: {:?} (context = {:?})", ty, out_ctx); + // let wtf = app_ctx(&out_ctx, &ty); + // println!("WTF: {wtf:?}"); + bail!("[test] Synthesized: {:?} (context = {:?})", ty, out_ctx); Ok(()) }