rust: add references to egraph
This commit is contained in:
parent
465af72b1a
commit
a49f930eb1
1 changed files with 38 additions and 1 deletions
|
@ -45,6 +45,10 @@ pub enum ExprKind {
|
|||
/// a reference to the call stack (which naturally can't be inlined into the expression).
|
||||
CallStackRef(Rc<Var>),
|
||||
|
||||
/// a value which is a read-only reference in the core language
|
||||
RefOf(Expr),
|
||||
RefTy(Rc<Var>, Expr),
|
||||
|
||||
Lambda(Rc<Var>, Expr),
|
||||
|
||||
TyLambda {
|
||||
|
@ -114,6 +118,11 @@ impl Expr {
|
|||
// we don't need to deep-clone call stack references (they are immutable)
|
||||
Ek::CallStackRef(csr) => Ek::CallStackRef(Rc::clone(csr)),
|
||||
|
||||
Ek::RefOf(inner) => Ek::RefOf(inner.deep_clone_intern(hmexpr)),
|
||||
// RefTy is also a CSR consumer
|
||||
Ek::RefTy(csr, inner) => Ek::RefTy(Rc::clone(csr), inner.deep_clone_intern(hmexpr)),
|
||||
|
||||
// lambdas and their dependent types are CSR introducers
|
||||
Ek::Lambda(csr, inner) => Ek::Lambda(Rc::clone(csr), inner.deep_clone_intern(hmexpr)),
|
||||
|
||||
Ek::TyLambda { argty, arg, exp } => Ek::TyLambda {
|
||||
|
@ -199,6 +208,18 @@ impl Expr {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
(Ek::RefOf(lhs), Ek::RefOf(rhs)) => lhs.deep_eq_intern(rhs, hsv, hscsrs),
|
||||
(Ek::RefTy(cslhs, exlhs), Ek::RefTy(csrhs, exrhs)) => {
|
||||
match hscsrs.entry((Rc::as_ptr(cslhs), Rc::as_ptr(csrhs))) {
|
||||
Entry::Occupied(occ) => *occ.get() && exlhs.deep_eq_intern(exrhs, hsv, hscsrs),
|
||||
Entry::Vacant(vac) => {
|
||||
vac.insert(false);
|
||||
false
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
(Ek::Lambda(cslhs, exlhs), Ek::Lambda(csrhs, exrhs)) => {
|
||||
Self::deep_eq_mark_var(hscsrs, cslhs, csrhs);
|
||||
exlhs.deep_eq_intern(exrhs, hsv, hscsrs)
|
||||
|
@ -283,7 +304,7 @@ impl Expr {
|
|||
|
||||
match &mut *this {
|
||||
Ek::Poison | Ek::NoArgsCross(_) | Ek::Literal(_) => {}
|
||||
Ek::Weak(w) => Expr(w.upgrade().expect("tried to force dropped weak pointer"))
|
||||
Ek::Weak(w) => Expr(w.upgrade().expect("tried to subst dropped weak pointer"))
|
||||
.subst_intern(hsx, hsvars),
|
||||
Ek::CallStackRef(csr) => {
|
||||
if let Some(Expr(x)) = hsvars.get(&(Rc::as_ptr(&csr) as usize)) {
|
||||
|
@ -292,6 +313,11 @@ impl Expr {
|
|||
*this = Ek::NoArgsCross(Expr(Rc::clone(x)));
|
||||
}
|
||||
}
|
||||
Ek::RefOf(inner) => inner.subst_intern(hsx, hsvars),
|
||||
Ek::RefTy(_, inner) => {
|
||||
// this is a bit special (and I don't know if it is really correct)
|
||||
inner.subst_intern(hsx, hsvars)
|
||||
}
|
||||
Ek::Lambda(csr, inner) => {
|
||||
if let Some(hsvars2) = subst_prune_csr(hsvars, &csr) {
|
||||
inner.subst_intern(hsx, &*hsvars2)
|
||||
|
@ -375,6 +401,7 @@ impl Expr {
|
|||
n.0 = tmp;
|
||||
}
|
||||
n.force_intern(hsx)?;
|
||||
n.strip_nac_heads();
|
||||
// handle NAC -> Weak -> NAC -> Weak => NAC -> Weak
|
||||
// because indirection just slows us down too much
|
||||
loop {
|
||||
|
@ -399,6 +426,10 @@ impl Expr {
|
|||
// we don't have hsvars here because they would mess with lazyness
|
||||
// if you need this normalized, use `subst` instead
|
||||
}
|
||||
Ek::RefOf(inner) => {
|
||||
inner.force_intern(hsx)?;
|
||||
}
|
||||
Ek::RefTy(_, inner) => inner.force_intern(hsx)?,
|
||||
Ek::Lambda(_, inner) => inner.force_intern(hsx)?,
|
||||
Ek::TyLambda { argty, arg: _, exp } => {
|
||||
argty.force_intern(hsx)?;
|
||||
|
@ -423,6 +454,12 @@ impl Expr {
|
|||
self.subst(hsvars);
|
||||
continue;
|
||||
}
|
||||
Ek::RefOf(Expr(n)) => {
|
||||
// references around lambdas get dropped here for simplicity
|
||||
// (they mostly matter for its interaction with linearity checks)
|
||||
*this = (*n.borrow()).clone();
|
||||
continue;
|
||||
}
|
||||
Ek::NoArgsCross(Expr(n)) => {
|
||||
// NOTE: the forcing above would've flattened all potentially present stacks.
|
||||
// here we simply lift the NAC to the outside of the apply
|
||||
|
|
Loading…
Reference in a new issue