diff --git a/bidir/src/bidir_debruijn.rs b/bidir/src/bidir_debruijn.rs index 0d32627..615feec 100644 --- a/bidir/src/bidir_debruijn.rs +++ b/bidir/src/bidir_debruijn.rs @@ -115,7 +115,6 @@ pub fn instantiate_left( } Ok(new_ctx) - // todo!("helloge: a={a:?} , b={b:?} // {ctx:?}") } Type::Existential(_b) => todo!(), @@ -223,12 +222,6 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { let tau = app_ctx(&after_marker, &tau)?; let tau = tau.transform_with_visitor(&V2(1, after_marker.size()))?; - // 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())); - // } - Ok((Type::Polytype(Box::new(tau)), before_marker)) } diff --git a/bidir/src/data_debruijn.rs b/bidir/src/data_debruijn.rs index 02de997..3441e2a 100644 --- a/bidir/src/data_debruijn.rs +++ b/bidir/src/data_debruijn.rs @@ -38,38 +38,6 @@ 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()) - // } - // } - // } - pub fn transform_with_visitor( &self, visitor: &V, @@ -138,65 +106,6 @@ impl Type { self.try_into_mono().is_some() } - // pub fn bump_indexes(&self, by: usize) -> Type { - // match self { - // Type::Unit => Type::Unit, - // Type::Var(_) => todo!(), - // Type::Existential(index) => { - // let debruijn_index = index.debruijn_index + by; - // let new_index = ContextIndex { - // debruijn_index, - // debruijn_level: index.debruijn_level, - // }; - // Type::Existential(new_index) - // } - // Type::Polytype(_) => todo!(), - // Type::Arrow(_, _) => todo!(), - // } - // } - - // pub fn free_vars(&self) -> HashSet { - // fn free_vars_with_context(ctx: &Context, ty: &Type) -> HashSet { - // match ty { - // Type::Unit => HashSet::default(), - // Type::Var(x) if ctx.lookup_type(x).is_some() => HashSet::default(), - // Type::Var(x) => [FreeVar::Var(x.to_owned())].into_iter().collect(), - // Type::Existential(x) if ctx.lookup_existential(x).is_some() => HashSet::default(), - // Type::Existential(x) => [FreeVar::Existential(x.to_owned())].into_iter().collect(), - // Type::Polytype(x, ty_a) => { - // let new_ctx = ctx.add(vec![ContextEntry::ExistentialVar(x.to_owned())]); - // free_vars_with_context(&new_ctx, &ty_a) - // } - // Type::Arrow(ty_a, ty_b) => { - // let a_vars = free_vars_with_context(&ctx, &ty_a); - // let b_vars = free_vars_with_context(&ctx, &ty_b); - // a_vars.union(b_vars) - // } - // } - // } - - // free_vars_with_context(&Context::default(), self) - // } - - // /// Substitute all variables with this variable with the replacement type. - // pub fn subst(&self, var: &str, replacement: &Type) -> Type { - // match self { - // Type::Unit => Type::Unit, - // Type::Var(n) if n == var => replacement.clone(), - // Type::Var(n) => Type::Var(n.clone()), - // Type::Existential(s) if s == var => replacement.clone(), - // Type::Existential(s) => Type::Existential(s.clone()), - // Type::Polytype(t) => { - // // Type::Polytype(a.clone(), Box::new(t.subst(var, replacement))), - // todo!() - // } - // Type::Arrow(a, b) => Type::Arrow( - // Box::new(a.subst(var, replacement)), - // Box::new(b.subst(var, replacement)), - // ), - // } - // } - pub fn subst(&self, before: &ContextIndex, after: Type) -> Type { match self { Type::Unit => Type::Unit, @@ -264,34 +173,6 @@ impl Monotype { } } - // pub fn bump_indexes(&self, by: isize) -> Monotype { - // match self { - // Monotype::Unit => Monotype::Unit, - // Monotype::Var(index) => { - // let debruijn_index = (index.debruijn_index as isize + by) as usize; - // // let debruijn_level = new_ctx.vector.len() - 1 - debruijn_index; - // let new_index = ContextIndex { - // debruijn_index, - // debruijn_level: index.debruijn_level, - // }; - // Monotype::Var(new_index) - // } - // Monotype::Existential(index) => { - // let debruijn_index = (index.debruijn_index as isize + by) as usize; - // // let debruijn_level = new_ctx.vector.len() - 1 - debruijn_index; - // let new_index = ContextIndex { - // debruijn_index, - // debruijn_level: index.debruijn_level, - // }; - // Monotype::Var(new_index) - // } - // Monotype::Arrow(a, b) => Monotype::Arrow( - // Box::new(a.bump_indexes(by)), - // Box::new(b.bump_indexes(by)), - // ), - // } - // } - pub fn transform_with_visitor( &self, visitor: &V, @@ -356,17 +237,6 @@ impl fmt::Debug for Context { } } -// 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(); @@ -400,10 +270,6 @@ impl Context { Ok((new_ctx, idx)) } - // /// Pops items from the end of the context, changing all of the indexes in the - // /// process - // pub fn pop(&self) -> Context {} - pub fn get<'a>(&'a self, index: &ContextIndex) -> Option<&ContextEntry> { let item = self.vector.get(index.debruijn_level)?; Some(item) @@ -539,28 +405,6 @@ impl Context { .collect::>()?, }) } - - // pub fn bump_indexes(&self, by: isize) -> Context { - // Context { - // vector: self - // .vector - // .iter() - // .map(|entry| match entry { - // ContextEntry::TypeVar => ContextEntry::TypeVar, - // ContextEntry::TermAnnot(ty) => { - // todo!() - // // ContextEntry::TermAnnot(ty.bump_indexes(by)) - // } - // ContextEntry::ExistentialVar => ContextEntry::ExistentialVar, - // ContextEntry::ExistentialSolved(ty) => { - // todo!() - // // ContextEntry::ExistentialSolved(ty.bump_indexes(-1)) - // } - // ContextEntry::Marker => ContextEntry::Marker, - // }) - // .collect(), - // } - // } } /// An index into the context.