wip: not sure
This commit is contained in:
parent
6012067fa5
commit
4ff88c0ca9
2 changed files with 275 additions and 87 deletions
|
|
@ -1,7 +1,7 @@
|
|||
use anyhow::{bail, Result};
|
||||
use anyhow::{bail, ensure, Result};
|
||||
|
||||
use crate::data_debruijn::{
|
||||
Context, ContextEntry, ContextIndex, Monotype, Term, Type,
|
||||
Context, ContextEntry, ContextIndex, Monotype, Term, Type, Visitor,
|
||||
};
|
||||
use crate::DEPTH;
|
||||
|
||||
|
|
@ -105,6 +105,11 @@ pub fn instantiate_left(
|
|||
.get_mut(b.debruijn_level)
|
||||
.expect("should exist");
|
||||
|
||||
ensure!(
|
||||
matches!(b_entry, ContextEntry::ExistentialVar),
|
||||
"not an existential variable"
|
||||
);
|
||||
|
||||
*b_entry =
|
||||
ContextEntry::ExistentialSolved(Monotype::Existential(a.to_owned()));
|
||||
}
|
||||
|
|
@ -173,37 +178,59 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
|
|||
|
||||
// →I⇒' rule
|
||||
Term::Lam(e) => {
|
||||
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, 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);
|
||||
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_at_b.add(ContextEntry::TermAnnot(ex_a.clone()));
|
||||
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);
|
||||
struct V(usize, usize);
|
||||
impl Visitor for V {
|
||||
fn visit_index(&self, index: &mut ContextIndex) -> Result<()> {
|
||||
index.debruijn_index += self.0;
|
||||
index.debruijn_level = self.1 - 1 - index.debruijn_index;
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
// TODO: Rewrite all indexes in this term
|
||||
let e_2 = e.bump_indexes(ctx, &aug_ctx, 0);
|
||||
let ex_a_2 = ex_b.transform_with_visitor(&V(2, aug_ctx.size()))?;
|
||||
let ex_b_2 = ex_b.transform_with_visitor(&V(1, aug_ctx.size()))?;
|
||||
let e_2 = e.transform_with_visitor(&V(0, aug_ctx.size()))?;
|
||||
|
||||
println!("---");
|
||||
let wtf_ctx = typecheck(&aug_ctx, &e_2, &ex_b_2)?;
|
||||
|
||||
let (before_marker, after_marker) = wtf_ctx.split_at(&marker_idx);
|
||||
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(ContextEntry::ExistentialVar);
|
||||
|
||||
for index in after_marker.unsolved_existentials() {
|
||||
tau = tau.subst(&index, Type::Var(gen_idx.clone()));
|
||||
// Bump the levels down since we're splitting teh array
|
||||
struct V2(usize);
|
||||
impl Visitor for V2 {
|
||||
fn visit_index(&self, index: &mut ContextIndex) -> Result<()> {
|
||||
index.debruijn_level -= 1;
|
||||
index.debruijn_index = self.0 - 1 - index.debruijn_level;
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
let after_marker =
|
||||
after_marker.transform_with_visitor(&V2(after_marker.size()))?;
|
||||
|
||||
Ok((Type::Polytype(Box::new(tau)), final_ctx))
|
||||
let tau = Type::Arrow(Box::new(ex_a_2), Box::new(ex_b));
|
||||
println!("pre-tau: {tau:?} (in {after_marker:?})");
|
||||
let tau = app_ctx(&after_marker, &tau)?;
|
||||
|
||||
// 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))
|
||||
}
|
||||
|
||||
Term::Annot(_, _) => todo!(),
|
||||
|
|
@ -224,7 +251,7 @@ pub fn app_synthesize(
|
|||
|
||||
// ∀App rule
|
||||
(Type::Polytype(ty_a), e) => {
|
||||
let (aug_ctx, a_idx) = ctx.add(ContextEntry::ExistentialVar);
|
||||
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)?;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
use std::fmt::{self};
|
||||
|
||||
use anyhow::Result;
|
||||
use im::Vector;
|
||||
|
||||
use crate::{data, gensym::gensym_type};
|
||||
|
|
@ -37,36 +38,57 @@ impl fmt::Debug for Term {
|
|||
}
|
||||
|
||||
impl Term {
|
||||
pub fn bump_indexes(
|
||||
// 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<V: Visitor>(
|
||||
&self,
|
||||
old_ctx: &Context,
|
||||
new_ctx: &Context,
|
||||
by: usize,
|
||||
) -> Term {
|
||||
match self {
|
||||
Term::Unit => Term::Unit,
|
||||
visitor: &V,
|
||||
) -> Result<Term> {
|
||||
let mut expr = self.clone();
|
||||
visitor.visit_term_before(&mut expr)?;
|
||||
let mut expr = match expr {
|
||||
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,
|
||||
let mut index = index.clone();
|
||||
visitor.visit_index(&mut index)?;
|
||||
Term::Var(index)
|
||||
}
|
||||
Term::Lam(_) => todo!(),
|
||||
Term::App(_, _) => todo!(),
|
||||
Term::Annot(_, _) => todo!(),
|
||||
_ => expr,
|
||||
};
|
||||
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())
|
||||
}
|
||||
}
|
||||
visitor.visit_term_after(&mut expr)?;
|
||||
Ok(expr)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -116,31 +138,23 @@ impl Type {
|
|||
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!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
// 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!(),
|
||||
// }
|
||||
// }
|
||||
|
||||
impl Type {
|
||||
// pub fn free_vars(&self) -> HashSet<FreeVar> {
|
||||
// fn free_vars_with_context(ctx: &Context, ty: &Type) -> HashSet<FreeVar> {
|
||||
// match ty {
|
||||
|
|
@ -203,6 +217,27 @@ impl Type {
|
|||
),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn transform_with_visitor<V: Visitor>(
|
||||
&self,
|
||||
visitor: &V,
|
||||
) -> Result<Type> {
|
||||
let mut ty = self.clone();
|
||||
visitor.visit_type_before(&mut ty)?;
|
||||
let mut ty = match ty {
|
||||
Type::Var(_) => todo!(),
|
||||
Type::Existential(index) => {
|
||||
let mut index = index.clone();
|
||||
visitor.visit_index(&mut index)?;
|
||||
Type::Existential(index)
|
||||
}
|
||||
Type::Polytype(_) => todo!(),
|
||||
Type::Arrow(_, _) => todo!(),
|
||||
_ => ty,
|
||||
};
|
||||
visitor.visit_type_after(&mut ty)?;
|
||||
Ok(ty)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
|
|
@ -224,6 +259,54 @@ 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<V: Visitor>(
|
||||
&self,
|
||||
visitor: &V,
|
||||
) -> Result<Monotype> {
|
||||
let mut ty = self.clone();
|
||||
visitor.visit_monotype_before(&mut ty)?;
|
||||
let mut ty = match ty {
|
||||
Monotype::Var(_) => todo!(),
|
||||
Monotype::Existential(index) => {
|
||||
let mut index = index.clone();
|
||||
visitor.visit_index(&mut index)?;
|
||||
Monotype::Existential(index)
|
||||
}
|
||||
Monotype::Arrow(_, _) => todo!(),
|
||||
_ => ty,
|
||||
};
|
||||
visitor.visit_monotype_after(&mut ty)?;
|
||||
Ok(ty)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
|
|
@ -289,18 +372,34 @@ impl Default for Context {
|
|||
}
|
||||
|
||||
impl Context {
|
||||
pub fn add(&self, item: ContextEntry) -> (Context, ContextIndex) {
|
||||
#[inline]
|
||||
pub fn size(&self) -> usize {
|
||||
self.vector.len()
|
||||
}
|
||||
|
||||
pub fn add(&self, item: ContextEntry) -> Result<(Context, ContextIndex)> {
|
||||
let idx = self.vector.len();
|
||||
let mut new_ctx = self.bump_indexes(1);
|
||||
struct V;
|
||||
impl Visitor for V {
|
||||
fn visit_index(&self, index: &mut ContextIndex) -> Result<()> {
|
||||
index.debruijn_index += 1;
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
let mut new_ctx = self.transform_with_visitor(&V)?;
|
||||
new_ctx.vector.push_back(item);
|
||||
|
||||
let idx = ContextIndex {
|
||||
debruijn_index: 0,
|
||||
debruijn_level: idx,
|
||||
};
|
||||
(new_ctx, idx)
|
||||
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)
|
||||
|
|
@ -347,10 +446,7 @@ impl Context {
|
|||
|
||||
/// Splits the 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.debruijn_level)
|
||||
};
|
||||
let (before, after) = self.vector.clone().split_at(index.debruijn_level);
|
||||
|
||||
(Context { vector: before }, Context { vector: after })
|
||||
}
|
||||
|
|
@ -411,21 +507,56 @@ impl Context {
|
|||
.all(|item| ensure_item_validity(self, item))
|
||||
}
|
||||
|
||||
pub fn bump_indexes(&self, by: usize) -> Context {
|
||||
Context {
|
||||
pub fn transform_with_visitor<V: Visitor>(
|
||||
&self,
|
||||
visitor: &V,
|
||||
) -> Result<Context> {
|
||||
Ok(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,
|
||||
.map(|entry| {
|
||||
let mut entry = entry.clone();
|
||||
visitor.visit_context_entry_before(&mut entry)?;
|
||||
let mut entry = match entry {
|
||||
ContextEntry::TermAnnot(ty) => {
|
||||
ContextEntry::TermAnnot(ty.transform_with_visitor(visitor)?)
|
||||
}
|
||||
ContextEntry::ExistentialSolved(ty) => {
|
||||
ContextEntry::ExistentialSolved(
|
||||
ty.transform_with_visitor(visitor)?,
|
||||
)
|
||||
}
|
||||
_ => entry,
|
||||
};
|
||||
visitor.visit_context_entry_after(&mut entry)?;
|
||||
Ok(entry)
|
||||
})
|
||||
.collect::<Result<_>>()?,
|
||||
})
|
||||
.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.
|
||||
|
|
@ -507,3 +638,33 @@ pub fn convert_term(term: &data::Term) -> Term {
|
|||
term,
|
||||
)
|
||||
}
|
||||
|
||||
pub trait Visitor {
|
||||
fn visit_context_entry_before(&self, expr: &mut ContextEntry) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
fn visit_context_entry_after(&self, expr: &mut ContextEntry) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
fn visit_type_before(&self, expr: &mut Type) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
fn visit_type_after(&self, expr: &mut Type) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
fn visit_monotype_before(&self, expr: &mut Monotype) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
fn visit_monotype_after(&self, expr: &mut Monotype) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
fn visit_term_before(&self, expr: &mut Term) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
fn visit_term_after(&self, expr: &mut Term) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
fn visit_index(&self, index: &mut ContextIndex) -> Result<()> {
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue