René's URL Explorer Experiment

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"Sanity Checker","articleBody":"Let's have sth like:\r\n```rust\r\nuse std::collections::HashMap;\r\nuse crate::theory::abs::data::{MetaKind, Term};\r\nuse crate::theory::{Name, Var};\r\n\r\npub struct UnusedParamAnalyzer\u003c'a> {\r\n    parameters: HashMap\u003cName, (&'a Term, bool)>,\r\n    unused: Vec\u003c(Name, &'a Term)>,\r\n}\r\n\r\nimpl\u003c'a> UnusedParamAnalyzer\u003c'a> {\r\n    pub fn new() -> Self {\r\n        UnusedParamAnalyzer {\r\n            parameters: HashMap::new(),\r\n            unused: Vec::new(),\r\n        }\r\n    }\r\n\r\n    pub fn with_binding\u003cF>(&mut self, name: Name, term: &'a Term, mut continuation: F) where F: FnMut(&mut Self) {\r\n        let backup = self.parameters.insert(name.clone(), (term, false));\r\n        continuation(self);\r\n        let released = if let Some(backup) = backup {\r\n            self.parameters.insert(name.clone(), backup)\r\n        } else {\r\n            self.parameters.remove(&name)\r\n        };\r\n        match released {\r\n            Some((term, flag)) => {\r\n                if !flag {\r\n                    self.unused.push((name, term));\r\n                }\r\n            },\r\n            _ => unreachable!(\"must have been inserted in this scope\"),\r\n        }\r\n    }\r\n\r\n    pub fn mark_used(&mut self, name: Name) {\r\n        if let Some((_, flag)) = self.parameters.get_mut(&name) {\r\n            *flag = true;\r\n        }\r\n    }\r\n    // term is the term that binds the variable\r\n    pub fn analyze(&mut self, term: &'a Term) {\r\n        match term {\r\n            Term::Ref(var) => {\r\n                self.mark_used(var.name.clone());\r\n            }\r\n            Term::Qualified(_, _) => {\r\n                // qualified does not contribute to local used variables\r\n            }\r\n            Term::Extern(_) => {}\r\n            Term::MetaRef(kind, y, z) => {\r\n                // TODO: check if this is correct\r\n                if let MetaKind::UserMeta = kind {\r\n                    self.mark_used(y.name.clone());\r\n                }\r\n                for (_, t) in z {\r\n                    self.analyze(t);\r\n                }\r\n            }\r\n            Term::Undef(_var) => {\r\n                // undef does not contribute to used variables\r\n            }\r\n            Term::Let(param, val, body) => {\r\n                self.analyze(¶m.typ);\r\n                self.analyze(val);\r\n                self.with_binding(param.var.name.clone(), term, |this| {\r\n                    this.analyze(body);\r\n                });\r\n            }\r\n            Term::Univ => {}\r\n            Term::Pi(param, body) => {\r\n                self.analyze(¶m.typ);\r\n                self.with_binding(param.var.name.clone(), term, |this| {\r\n                    this.analyze(body);\r\n                });\r\n            }\r\n            Term::Lam(param, body) => {\r\n                self.analyze(¶m.typ);\r\n                self.with_binding(param.var.name.clone(), term, |this| {\r\n                    this.analyze(body);\r\n                });\r\n            }\r\n            Term::App(x, _, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::Sigma(param, body) => {\r\n                self.analyze(¶m.typ);\r\n                self.with_binding(param.var.name.clone(), term, |this| {\r\n                    this.analyze(body);\r\n                });\r\n            }\r\n            Term::Tuple(x, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::TupleLet(x, y, expr, body) => {\r\n                self.analyze(&x.typ);\r\n                self.analyze(&y.typ);\r\n                self.analyze(expr);\r\n                // can be dependent tuple\r\n                self.with_binding(x.var.name.clone(), term, |this| {\r\n                    this.with_binding(y.var.name.clone(), term, |this| {\r\n                        this.analyze(body);\r\n                    });\r\n                });\r\n            }\r\n            Term::Unit => {}\r\n            Term::TT => {}\r\n            Term::UnitLet(_, body) => {\r\n                self.analyze(body);\r\n            }\r\n            Term::Boolean => {}\r\n            Term::False => {}\r\n            Term::True => {}\r\n            Term::If(x, y, z) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n                self.analyze(z);\r\n            }\r\n            Term::String => {\r\n            }\r\n            Term::Str(_) => {}\r\n            Term::Number => {}\r\n            Term::Num(_) => {}\r\n            Term::NumAdd(x, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::NumSub(x, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::BigInt => {}\r\n            Term::Big(_) => {}\r\n            Term::Row => {}\r\n            Term::Fields(x) => {\r\n                for (_, t) in x {\r\n                    self.analyze(t);\r\n                }\r\n            }\r\n            Term::Combine(x, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::RowOrd(x, _, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::RowSat => {}\r\n            Term::RowEq(x, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::RowRefl => {}\r\n            Term::Object(x) => {\r\n                self.analyze(x);\r\n            }\r\n            Term::Obj(x) => {\r\n                self.analyze(x);\r\n            }\r\n            Term::Concat(x, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::Access(x, _) => {\r\n                self.analyze(x);\r\n            }\r\n            Term::Downcast(x, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::Enum(x) => {\r\n                self.analyze(x);\r\n            }\r\n            Term::Variant(x) => {\r\n                self.analyze(x);\r\n            }\r\n            Term::Upcast(x, y) => {\r\n                self.analyze(x);\r\n                self.analyze(y);\r\n            }\r\n            Term::Switch(x, map) => {\r\n                self.analyze(x);\r\n                for (_, (var, body)) in map {\r\n                    self.with_binding(var.name.clone(), term, |this| {\r\n                        this.analyze(body);\r\n                    });\r\n                }\r\n            }\r\n            Term::Vptr(var, terms) => {\r\n                self.mark_used(var.name.clone());\r\n                for t in terms {\r\n                    self.analyze(t);\r\n                }\r\n            }\r\n            Term::Vp(_, terms) => {\r\n                for t in terms {\r\n                    self.analyze(t);\r\n                }\r\n            }\r\n            Term::Lookup(x) => {\r\n                self.analyze(x);\r\n            }\r\n            Term::Find(x, a, b) => {\r\n                self.mark_used(a.name.clone());\r\n                self.mark_used(b.name.clone());\r\n                self.analyze(x);\r\n            }\r\n            Term::ImplementsOf(x, var) => {\r\n                self.mark_used(var.name.clone());\r\n                self.analyze(x);\r\n            }\r\n            Term::ImplementsSat => {\r\n            }\r\n        }\r\n    }\r\n    pub fn finalize(self) -> Vec\u003c(Name, &'a Term)> {\r\n        self.unused\r\n    }\r\n}\r\n```","author":{"url":"https://github.com/SchrodingerZhu","@type":"Person","name":"SchrodingerZhu"},"datePublished":"2023-04-30T01:56:52Z","url":"https://github.com/rowscript/rowscript/issues/73"}