better matching

Cargo.lock

@@ -2,12 +2,29 @@
 # It is not intended for manual editing.
 version = 3
 
+[[package]]
+name = "cfg-if"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
+
 [[package]]
 name = "either"
 version = "1.8.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7fcaabb2fef8c910e7f4c7ce9f67a1283a1715879a7c230ca9d6d1ae31f16d91"
 
+[[package]]
+name = "getrandom"
+version = "0.2.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "wasi",
+]
+
 [[package]]
 name = "intaglio"
 version = "1.8.0"
@@ -23,12 +40,54 @@ dependencies = [
  "either",
 ]
 
+[[package]]
+name = "libc"
+version = "0.2.146"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f92be4933c13fd498862a9e02a3055f8a8d9c039ce33db97306fd5a6caa7f29b"
+
 [[package]]
 name = "once_cell"
 version = "1.18.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d"
 
+[[package]]
+name = "ppv-lite86"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de"
+
+[[package]]
+name = "rand"
+version = "0.8.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
+dependencies = [
+ "libc",
+ "rand_chacha",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
+dependencies = [
+ "ppv-lite86",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.6.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
+dependencies = [
+ "getrandom",
+]
+
 [[package]]
 name = "slimp"
 version = "0.1.0"
@@ -36,4 +95,11 @@ dependencies = [
  "intaglio",
  "itertools",
  "once_cell",
+ "rand",
 ]
+
+[[package]]
+name = "wasi"
+version = "0.11.0+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"

Cargo.toml

@@ -9,3 +9,4 @@ edition = "2021"
 intaglio = "1.8.0"
 itertools = "0.10.5"
 once_cell = "1.18.0"
+rand = "0.8.5"

main.js

@@ -23,6 +23,7 @@ client.on("messageCreate", message => {
     if (
         message.author.id == id ||
         message.author.id == "1117299835855450163" ||
+        message.author.id == "1115433649010114670" ||
         !message.mentions.has(id)
     )
         return;

pi-pair.slimp

@@ -0,0 +1,11 @@
+(forall (name arg type out f) ((the (Pi name type out) f) (the type arg)) (let name arg (the out (f arg))))
+(forall (in out) (-> in out) (Pi _ in out))
+(forall (var body arg) ((lambda var body) arg) (let var arg body))
+
+(def succ (the (-> nat nat) +1))
+(def cons (the (Pi A U (Pi B U (-> A (-> B (Pair A B))))) (lambda _ (lambda _ (lambda a (lambda b (pair a b)))))))
+(def car (the (Pi A U (Pi B U (-> (Pair A B) A))) (lambda _ (lambda _ (lambda p (car' p))))))
+(forall (a b) (car' (pair a b)) a)
+
+(def our-car ((car (the U nat)) (the U symbol)))
+(((((cons (the U nat)) (the U symbol)) (the nat 0)) (the symbol hi)))

src/main.rs

@@ -3,18 +3,19 @@ use std::{
     collections::HashSet,
     env,
     io::{self, Read},
+    iter,
     sync::Mutex,
 };
 
 use intaglio::{Symbol, SymbolTable};
 use itertools::Itertools;
 use once_cell::sync::Lazy;
+use rand::{distributions::Alphanumeric, Rng};
 
 static TABLE: Lazy<Mutex<SymbolTable>> = Lazy::new(|| Mutex::new(SymbolTable::new()));
 static FORALL: Lazy<Symbol> = Lazy::new(|| TABLE.lock().unwrap().intern("forall").unwrap());
 /// Note that it is actually the string "def". This is for the user's convenience.
 static CONCRETE: Lazy<Symbol> = Lazy::new(|| TABLE.lock().unwrap().intern("def").unwrap());
-static LET: Lazy<Symbol> = Lazy::new(|| TABLE.lock().unwrap().intern("let").unwrap());
 
 const DEFAULT_COMPLEXITY_LIMIT: usize = 20_000;
 const DEFAULT_STEP_LIMIT: usize = 2_000;
@@ -153,13 +154,27 @@ impl Sexp {
         }
     }
 
+    // #[must_use]
+    // fn apply_lets(&self) -> Sexp {
+    //     match self {
+    //         Sexp::Atom(_) => self.clone(),
+    //         Sexp::List(xs) => match Let::from_sexp(self) {
+    //             Some(let_) => let_.eval(),
+    //             None => Sexp::List(xs.iter().map(Sexp::apply_lets).collect()),
+    //         },
+    //     }
+    // }
+
     #[must_use]
-    fn apply_lets(&self) -> Sexp {
+    fn apply_special_form<'src, F: SpecialForm<'src>>(&'src self) -> Sexp {
         match self {
-            Sexp::Atom(_) => self.clone(),
-            Sexp::List(xs) => match Let::from_sexp(self) {
-                Some(let_) => let_.eval(),
-                None => Sexp::List(xs.iter().map(Sexp::apply_lets).collect()),
+            Sexp::Atom(_) => match F::from_sexp(self) {
+                Some(form) => form.eval(),
+                None => self.clone(),
+            },
+            Sexp::List(xs) => match F::from_sexp(self) {
+                Some(form) => form.eval(),
+                None => Sexp::List(xs.iter().map(Sexp::apply_special_form::<F>).collect()),
             },
         }
     }
@@ -360,9 +375,9 @@ impl Rule {
         }
     }
 
-    fn matches(&self, expr: &Sexp) -> bool {
-        matches(self.vars(), self.lhs(), expr)
-    }
+    // fn matches(&self, expr: &Sexp) -> bool {
+    //     could_match(self.vars(), self.lhs(), expr)
+    // }
 
     #[must_use]
     fn lhs(&self) -> &Sexp {
@@ -440,7 +455,7 @@ impl fmt::Display for Rule {
     }
 }
 
-fn matches(vars: Option<&Vec<Symbol>>, lhs: &Sexp, expr: &Sexp) -> bool {
+fn could_match(vars: Option<&[Symbol]>, lhs: &Sexp, expr: &Sexp) -> bool {
     let is_var = |var: &Symbol| -> bool {
         match vars {
             Some(vars) => vars.contains(var),
@@ -452,21 +467,69 @@ fn matches(vars: Option<&Vec<Symbol>>, lhs: &Sexp, expr: &Sexp) -> bool {
         (Sexp::Atom(a), Sexp::Atom(b)) => a == b || is_var(a),
         (Sexp::Atom(a), Sexp::List(_)) => is_var(a),
         (Sexp::List(a), Sexp::List(b)) => {
-            a.len() == b.len() && a.iter().zip(b).all(|(a, b)| matches(vars, a, b))
+            a.len() == b.len() && a.iter().zip(b).all(|(a, b)| could_match(vars, a, b))
         }
-        _ => false,
+        (Sexp::List(_), Sexp::Atom(_)) => false,
     }
 }
 
+// type Matches<'src> = HashMap<Symbol, HashSet<&'src Sexp>>;
+
+// i'm happy that this is faster, but it might be worth going back to the per-variable thing
+fn matches<'src>(vars: &HashSet<Symbol>, lhs: &Sexp, expr: &'src Sexp) -> HashSet<&'src Sexp> {
+    match (lhs, expr) {
+        (Sexp::Atom(a), Sexp::Atom(b)) => {
+            if a == b || vars.contains(a) {
+                let mut out = HashSet::with_capacity(1);
+                out.insert(expr);
+                out
+            } else {
+                HashSet::with_capacity(0)
+            }
+        }
+        (Sexp::Atom(a), Sexp::List(_)) => {
+            if vars.contains(a) {
+                let mut out = HashSet::with_capacity(1);
+                out.insert(expr);
+                out
+            } else {
+                HashSet::with_capacity(0)
+            }
+        }
+        (Sexp::List(_), Sexp::Atom(_)) => HashSet::with_capacity(0),
+        (Sexp::List(xs), Sexp::List(ys)) => {
+            if xs.len() == ys.len() {
+                xs.iter()
+                    .zip(ys)
+                    .map(|(lhs, expr)| matches(vars, lhs, expr))
+                    .reduce(|a, b| a.union(&b).copied().collect())
+                    .unwrap_or(HashSet::with_capacity(0))
+            } else {
+                HashSet::with_capacity(0)
+            }
+        }
+    }
+}
+
+// fn absorb_matches<'src>(from: Matches<'src>, into: &mut Matches<'src>) {
+//     for (var, matches) in from {
+//         let insert_into = into.entry(var).or_default();
+//         for matc in matches {
+//             insert_into.insert(matc);
+//         }
+//     }
+// }
+
 fn rw(rule: &Rule, sexp: &Sexp) -> Sexp {
     if rule.lhs() == rule.rhs() {
         return sexp.clone();
     }
 
     match rule {
-        rule @ Rule::Forall { vars, lhs, rhs } => {
-            if matches(Some(vars), lhs, sexp) {
-                let targets = sexp.concretion_targets();
+        rule @ Rule::Forall { vars, lhs, .. } => {
+            if could_match(Some(vars), lhs, sexp) {
+                // let targets = sexp.concretion_targets();
+                let targets = matches(&vars.iter().copied().collect(), lhs, sexp);
                 let mut out = sexp.clone();
                 for rule in rule.concretions(&targets) {
                     let rwed = rw(&rule, &out);
@@ -505,7 +568,11 @@ fn simp(
     let mut max = 0;
     let mut grace = step_limit / 4;
     for i in 0..step_limit {
-        expr = expr.apply_lets();
+        expr = expr
+            .apply_special_form::<Genslop>()
+            .apply_special_form::<Let>()
+            .apply_special_form::<Eq>();
+
         let complexity = expr.complexity();
         // eprintln!("{}/{step_limit} {complexity}", i + 1);
         if complexity > complexity_limit {
@@ -532,6 +599,13 @@ fn simp(
     (expr, max)
 }
 
+trait SpecialForm<'src>: Sized {
+    fn from_sexp(sexp: &'src Sexp) -> Option<Self>;
+
+    fn eval(self) -> Sexp;
+}
+
+static LET: Lazy<Symbol> = Lazy::new(|| TABLE.lock().unwrap().intern("let").unwrap());
 #[derive(Debug, Clone)]
 struct Let<'src> {
     from: Symbol,
@@ -539,7 +613,7 @@ struct Let<'src> {
     body: &'src Sexp,
 }
 
-impl<'src> Let<'src> {
+impl<'src> SpecialForm<'src> for Let<'src> {
     fn from_sexp(sexp: &'src Sexp) -> Option<Self> {
         match sexp {
             Sexp::Atom(_) => None,
@@ -561,6 +635,75 @@ impl<'src> Let<'src> {
     }
 }
 
+static EQ: Lazy<Symbol> = Lazy::new(|| TABLE.lock().unwrap().intern("eq").unwrap());
+#[derive(Debug, Clone)]
+struct Eq<'src> {
+    a: &'src Sexp,
+    b: &'src Sexp,
+    then: &'src Sexp,
+    els: &'src Sexp,
+}
+
+impl<'src> SpecialForm<'src> for Eq<'src> {
+    fn from_sexp(sexp: &'src Sexp) -> Option<Self> {
+        match sexp {
+            Sexp::Atom(_) => None,
+            Sexp::List(xs) => match &xs[..] {
+                [Sexp::Atom(eq), a, b, then, els] if *eq == *EQ => Some(Self { a, b, then, els }),
+                _ => None,
+            },
+        }
+    }
+
+    fn eval(self) -> Sexp {
+        let Self { a, b, then, els } = self;
+
+        if a == b {
+            then.clone()
+        } else {
+            els.clone()
+        }
+    }
+}
+
+static GENSLOP: Lazy<Symbol> = Lazy::new(|| TABLE.lock().unwrap().intern("genslop").unwrap());
+
+#[derive(Debug, Clone)]
+struct Genslop;
+
+impl Genslop {
+    fn gen() -> String {
+        format!(
+            "slop-{}",
+            rand::thread_rng()
+                .sample_iter(&Alphanumeric)
+                .take(8)
+                .map(char::from)
+                .collect::<String>()
+        )
+    }
+}
+
+impl SpecialForm<'_> for Genslop {
+    fn from_sexp(sexp: &Sexp) -> Option<Self> {
+        if let Some(genslop) = sexp.atom() {
+            if *genslop == *GENSLOP {
+                Some(Genslop)
+            } else {
+                None
+            }
+        } else {
+            None
+        }
+    }
+
+    fn eval(self) -> Sexp {
+        let ident = Genslop::gen();
+        let symbol = TABLE.lock().unwrap().intern(ident).unwrap();
+        Sexp::Atom(symbol)
+    }
+}
+
 fn make_rule(sexp: &Sexp) -> Option<Rule> {
     match sexp {
         Sexp::List(xs) => match &xs[..] {