Sanity Checker

[SchrodingerZhu]

Let's have sth like:

use std::collections::HashMap;
use crate::theory::abs::data::{MetaKind, Term};
use crate::theory::{Name, Var};

pub struct UnusedParamAnalyzer<'a> {
    parameters: HashMap<Name, (&'a Term, bool)>,
    unused: Vec<(Name, &'a Term)>,
}

impl<'a> UnusedParamAnalyzer<'a> {
    pub fn new() -> Self {
        UnusedParamAnalyzer {
            parameters: HashMap::new(),
            unused: Vec::new(),
        }
    }

    pub fn with_binding<F>(&mut self, name: Name, term: &'a Term, mut continuation: F) where F: FnMut(&mut Self) {
        let backup = self.parameters.insert(name.clone(), (term, false));
        continuation(self);
        let released = if let Some(backup) = backup {
            self.parameters.insert(name.clone(), backup)
        } else {
            self.parameters.remove(&name)
        };
        match released {
            Some((term, flag)) => {
                if !flag {
                    self.unused.push((name, term));
                }
            },
            _ => unreachable!("must have been inserted in this scope"),
        }
    }

    pub fn mark_used(&mut self, name: Name) {
        if let Some((_, flag)) = self.parameters.get_mut(&name) {
            *flag = true;
        }
    }
    // term is the term that binds the variable
    pub fn analyze(&mut self, term: &'a Term) {
        match term {
            Term::Ref(var) => {
                self.mark_used(var.name.clone());
            }
            Term::Qualified(_, _) => {
                // qualified does not contribute to local used variables
            }
            Term::Extern(_) => {}
            Term::MetaRef(kind, y, z) => {
                // TODO: check if this is correct
                if let MetaKind::UserMeta = kind {
                    self.mark_used(y.name.clone());
                }
                for (_, t) in z {
                    self.analyze(t);
                }
            }
            Term::Undef(_var) => {
                // undef does not contribute to used variables
            }
            Term::Let(param, val, body) => {
                self.analyze(&param.typ);
                self.analyze(val);
                self.with_binding(param.var.name.clone(), term, |this| {
                    this.analyze(body);
                });
            }
            Term::Univ => {}
            Term::Pi(param, body) => {
                self.analyze(&param.typ);
                self.with_binding(param.var.name.clone(), term, |this| {
                    this.analyze(body);
                });
            }
            Term::Lam(param, body) => {
                self.analyze(&param.typ);
                self.with_binding(param.var.name.clone(), term, |this| {
                    this.analyze(body);
                });
            }
            Term::App(x, _, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::Sigma(param, body) => {
                self.analyze(&param.typ);
                self.with_binding(param.var.name.clone(), term, |this| {
                    this.analyze(body);
                });
            }
            Term::Tuple(x, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::TupleLet(x, y, expr, body) => {
                self.analyze(&x.typ);
                self.analyze(&y.typ);
                self.analyze(expr);
                // can be dependent tuple
                self.with_binding(x.var.name.clone(), term, |this| {
                    this.with_binding(y.var.name.clone(), term, |this| {
                        this.analyze(body);
                    });
                });
            }
            Term::Unit => {}
            Term::TT => {}
            Term::UnitLet(_, body) => {
                self.analyze(body);
            }
            Term::Boolean => {}
            Term::False => {}
            Term::True => {}
            Term::If(x, y, z) => {
                self.analyze(x);
                self.analyze(y);
                self.analyze(z);
            }
            Term::String => {
            }
            Term::Str(_) => {}
            Term::Number => {}
            Term::Num(_) => {}
            Term::NumAdd(x, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::NumSub(x, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::BigInt => {}
            Term::Big(_) => {}
            Term::Row => {}
            Term::Fields(x) => {
                for (_, t) in x {
                    self.analyze(t);
                }
            }
            Term::Combine(x, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::RowOrd(x, _, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::RowSat => {}
            Term::RowEq(x, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::RowRefl => {}
            Term::Object(x) => {
                self.analyze(x);
            }
            Term::Obj(x) => {
                self.analyze(x);
            }
            Term::Concat(x, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::Access(x, _) => {
                self.analyze(x);
            }
            Term::Downcast(x, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::Enum(x) => {
                self.analyze(x);
            }
            Term::Variant(x) => {
                self.analyze(x);
            }
            Term::Upcast(x, y) => {
                self.analyze(x);
                self.analyze(y);
            }
            Term::Switch(x, map) => {
                self.analyze(x);
                for (_, (var, body)) in map {
                    self.with_binding(var.name.clone(), term, |this| {
                        this.analyze(body);
                    });
                }
            }
            Term::Vptr(var, terms) => {
                self.mark_used(var.name.clone());
                for t in terms {
                    self.analyze(t);
                }
            }
            Term::Vp(_, terms) => {
                for t in terms {
                    self.analyze(t);
                }
            }
            Term::Lookup(x) => {
                self.analyze(x);
            }
            Term::Find(x, a, b) => {
                self.mark_used(a.name.clone());
                self.mark_used(b.name.clone());
                self.analyze(x);
            }
            Term::ImplementsOf(x, var) => {
                self.mark_used(var.name.clone());
                self.analyze(x);
            }
            Term::ImplementsSat => {
            }
        }
    }
    pub fn finalize(self) -> Vec<(Name, &'a Term)> {
        self.unused
    }
}

[SchrodingerZhu]

@QuarticCat @anqurvanillapy

I am struggling to decide if analyzer can be designed in a less ad-hoc way.

[anqurvanillapy]

I guess our elaborator could expose some hooks for analysis passes so some extra checks could be done via only looking at the self.gamma 🤔️? Or even we just extend the gamma values with some extra flags?

Anyway you code looks legit here but yes I’m still not sure about some possible generalization, maybe we could generalize it in the future when more checks are necessary and clear, accepting this first.

[QuarticCat]

I am struggling to decide if analyzer can be designed in a less ad-hoc way.

I think you are saying: do we need another layer of IR?

[anqurvanillapy]

I think you are saying: do we need another layer of IR?

A new IR form is not needed I guess, but the extensibility of the analyzer/sanity checking/linter using the existing IR (here it's Expr) can be considered for a while 👀.

[SchrodingerZhu]

@QuarticCat as you may have already seen, the backend emits code solely based on the core concrete syntax tree (CST) without using 3AC or CFG. To my understanding, since our CST is simpler than CFG in term of graph analysis complexity, there is no need to have the Iterative Dataflow Analysis framework. Correct me if you think otherwise.