i need to rewrite terms FASTER

main.js

@@ -20,21 +20,53 @@ client.once(Events.ClientReady, c => {
 client.login(token);
 
 client.on("messageCreate", message => {
-    if (message.author.id == id || !message.mentions.has(id)) return;
+    if (
+        message.author.id == id ||
+        message.author.id == "1117299835855450163" ||
+        !message.mentions.has(id)
+    )
+        return;
     try {
+        let [so, se] = [false, false];
+
+        function done() {
+            if (!so || !se) return;
+
+            rules.length > 0 &&
+                message.reply(mk_message(rules, "`stderr:`", "ansi"));
+
+            message.reply(
+                out.length > 0
+                    ? mk_message(out, "`stdout:`")
+                    : "no output. weird."
+            );
+        }
+
         let process = spawn("./target/release/slimp", [message.content], {
             stdio: "pipe",
         });
-        process.stdout.on("data", data =>
+        let rules = "";
-            message.reply(mk_message(data.toString()))
+        process.stderr.on("data", data => (rules += data.toString()));
+        process.stderr.on("close", () => ((se = true), done()));
+
+        let out = "";
+        process.stdout.on("data", data => (out += data.toString()));
+        process.stdout.on("close", () => ((so = true), done()));
+
+        let timeout = 1 * 60 * 1000;
+        setTimeout(
+            () => (
+                (out += `took more than ${timeout}ms so killed. sorry`),
+                process.kill()
+            ),
+            timeout
         );
-        process.stderr.on("data", data => console.error(data.toString()));
     } catch (e) {
         console.error(e);
         message.reply(":(");
     }
 });
 
-function mk_message(str) {
+function mk_message(str, stream = "", lang = "lisp") {
-    return "```lisp\n" + str.slice(0, 1975) + "```";
+    return `${stream}\n` + "```" + lang + "\n" + str.slice(0, 1975) + "```";
 }

pi.slimp

@@ -0,0 +1,8 @@
+(forall (name arg type out f) ((the (Pi name type out) f) (the type arg)) (let name arg (the out (f arg))))
+(forall (name arg body) ((lambda name body) arg) (let name arg body))
+(def id-type (Pi a U (Pi x a a)))
+(def id      (lambda _ (lambda x x)))
+(forall (in out) (-> in out) (Pi _ in out))
+(forall (expr expected got) (assert-type expected (the got expr)) (= expected got))
+(forall (a) (= a a) t)
+(forall (name-a name-b in out) (= (Pi name-a in out) (Pi name-b in out)) t)

src/main.rs

@@ -14,8 +14,9 @@ static TABLE: Lazy<Mutex<SymbolTable>> = Lazy::new(|| Mutex::new(SymbolTable::ne
 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 = 10_000;
+const DEFAULT_COMPLEXITY_LIMIT: usize = 20_000;
 const DEFAULT_STEP_LIMIT: usize = 2_000;
 
 fn main() {
@@ -67,6 +68,22 @@ impl Sexp {
         matches!(self, Self::List(..))
     }
 
+    #[must_use]
+    fn atom(&self) -> Option<&Symbol> {
+        match self {
+            Sexp::Atom(at) => Some(at),
+            Sexp::List(_) => None,
+        }
+    }
+
+    #[must_use]
+    fn list(&self) -> Option<&[Sexp]> {
+        match self {
+            Sexp::Atom(_) => None,
+            Sexp::List(xs) => Some(&xs),
+        }
+    }
+
     #[must_use]
     fn unwrap_atom(&self) -> Symbol {
         match self {
@@ -113,6 +130,7 @@ impl Sexp {
             }
             Sexp::List(xs) => {
                 let mut out = HashSet::from_iter(xs);
+                out.insert(self);
                 out.extend(xs.iter().flat_map(Sexp::concretion_targets));
                 out
             }
@@ -134,6 +152,17 @@ impl Sexp {
             Sexp::List(xs) => 10 + xs.iter().map(Sexp::complexity).sum::<usize>(),
         }
     }
+
+    #[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()),
+            },
+        }
+    }
 }
 
 impl fmt::Display for Sexp {
@@ -159,6 +188,12 @@ fn lex(src: &str) -> Vec<Token> {
     let mut atom = None;
     let mut in_comment = false;
 
+    let indices: Vec<_> = src.char_indices().map(|(a, _)| a).collect();
+    let slice_src = |start: usize, end: usize| -> &str {
+        let end = indices.get(end + 1).unwrap_or(&src.len()) - 1;
+        &src[indices[start]..=end]
+    };
+
     for (i, c) in src.chars().enumerate() {
         match c {
             ';' | '`' => {
@@ -173,7 +208,7 @@ fn lex(src: &str) -> Vec<Token> {
             match c {
                 '(' => {
                     if let Some((start, end)) = atom {
-                        out.push(Token::Atom(&src[start..=end]));
+                        out.push(Token::Atom(slice_src(start, end)));
                         atom = None;
                     }
                     out.push(Token::LParen);
@@ -181,7 +216,7 @@ fn lex(src: &str) -> Vec<Token> {
 
                 ')' => {
                     if let Some((start, end)) = atom {
-                        out.push(Token::Atom(&src[start..=end]));
+                        out.push(Token::Atom(slice_src(start, end)));
                         atom = None;
                     }
                     out.push(Token::RParen);
@@ -189,7 +224,7 @@ fn lex(src: &str) -> Vec<Token> {
 
                 c if c.is_whitespace() => {
                     if let Some((start, end)) = atom {
-                        out.push(Token::Atom(&src[start..=end]));
+                        out.push(Token::Atom(slice_src(start, end)));
                         atom = None;
                     }
                 }
@@ -204,6 +239,10 @@ fn lex(src: &str) -> Vec<Token> {
         }
     }
 
+    if let Some((start, end)) = atom {
+        out.push(Token::Atom(slice_src(start, end)));
+    }
+
     out
 }
 
@@ -280,11 +319,16 @@ impl Rule {
                 } else {
                     let rule = Rule::var_replace(vars[0], sexp);
                     let lhs = rw(&rule, lhs);
+                    let rhs = rw(&rule, rhs);
 
-                    Rule::Forall {
+                    if vars.len() == 1 {
-                        vars: vars[1..].to_vec(),
+                        Rule::Concrete { lhs, rhs }
-                        lhs,
+                    } else {
-                        rhs: rw(&rule, rhs),
+                        Rule::Forall {
+                            vars: vars[1..].to_vec(),
+                            lhs,
+                            rhs,
+                        }
                     }
                 }
             }
@@ -382,14 +426,16 @@ impl Rule {
 impl fmt::Display for Rule {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            Rule::Forall { vars, lhs, rhs } => write!(
+            Rule::Forall { vars, lhs, rhs } => {
-                f,
+                let vars = vars
-                "∀{}, {lhs} ==> {rhs}",
+                    .iter()
-                vars.iter()
                     .map(|v| TABLE.lock().unwrap().get(*v).unwrap().to_string())
-                    .join(" ")
+                    .join(" ");
-            ),
+                let abs = format!("∀{vars},");
-            Rule::Concrete { lhs, rhs } => write!(f, "{lhs} ==> {rhs}"),
+                let lhs = format!("{abs:>15} {lhs}");
+                write!(f, "{lhs:<50} ==> {rhs}")
+            }
+            Rule::Concrete { lhs, rhs } => write!(f, "{:>50} ==> {rhs}", lhs.to_string()),
         }
     }
 }
@@ -413,13 +459,21 @@ fn matches(vars: Option<&Vec<Symbol>>, lhs: &Sexp, expr: &Sexp) -> bool {
 }
 
 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();
                 let mut out = sexp.clone();
                 for rule in rule.concretions(&targets) {
-                    out = rw(&rule, &out);
+                    let rwed = rw(&rule, &out);
+                    if rwed != out {
+                        out = rwed;
+                        break;
+                    }
                 }
                 out
             } else {
@@ -442,10 +496,18 @@ fn rw(rule: &Rule, sexp: &Sexp) -> Sexp {
     }
 }
 
-fn simp(rules: &[Rule], mut expr: Sexp, step_limit: usize, complexity_limit: usize) -> Sexp {
+fn simp(
+    rules: &[Rule],
+    mut expr: Sexp,
+    step_limit: usize,
+    complexity_limit: usize,
+) -> (Sexp, usize) {
+    let mut max = 0;
+    let mut grace = step_limit / 4;
     for i in 0..step_limit {
+        expr = expr.apply_lets();
         let complexity = expr.complexity();
-        eprintln!("{}/{step_limit} {complexity}", i + 1);
+        // eprintln!("{}/{step_limit} {complexity}", i + 1);
         if complexity > complexity_limit {
             break;
         }
@@ -457,11 +519,46 @@ fn simp(rules: &[Rule], mut expr: Sexp, step_limit: usize, complexity_limit: usi
         }
 
         if expr == last {
+            grace -= 1;
+        }
+
+        if grace == 0 {
             break;
         }
+
+        max = i;
+    }
+
+    (expr, max)
+}
+
+#[derive(Debug, Clone)]
+struct Let<'src> {
+    from: Symbol,
+    to: &'src Sexp,
+    body: &'src Sexp,
+}
+
+impl<'src> Let<'src> {
+    fn from_sexp(sexp: &'src Sexp) -> Option<Self> {
+        match sexp {
+            Sexp::Atom(_) => None,
+            Sexp::List(xs) => match &xs[..] {
+                [Sexp::Atom(let_), Sexp::Atom(from), to, body] if *let_ == *LET => Some(Self {
+                    from: *from,
+                    to,
+                    body,
+                }),
+                _ => None,
+            },
+        }
     }
 
-    expr
+    fn eval(self) -> Sexp {
+        let Self { from, to, body } = self;
+
+        rw(&Rule::var_replace(from, to), body)
+    }
 }
 
 fn make_rule(sexp: &Sexp) -> Option<Rule> {
@@ -489,9 +586,19 @@ fn run_program(src: &str, step_limit: usize, complexity_limit: usize) -> Option<
     let mut parsed = parse(&lex(src))?;
 
     let expr = parsed.pop()?;
-    let rules = parsed.iter().filter_map(make_rule).collect_vec();
+    let mut rules = parsed.iter().filter_map(make_rule).collect_vec();
-    eprintln!("{}", rules.iter().map(ToString::to_string).join("\n"));
+    rules.sort_by_key(Rule::num_vars);
-    Some(simp(&rules, expr, step_limit, complexity_limit))
+
+    for (i, rule) in rules.iter().enumerate() {
+        eprintln!("{}{rule}", if i % 2 == 0 { "\x1b[0m" } else { "\x1b[1m" });
+    }
+    //eprintln!("{:<50}\n{:<50}\n{:^50}", "|", "▾", expr.to_string());
+
+    let (simped, steps) = simp(&rules, expr, step_limit, complexity_limit);
+    eprintln!("\x1b[0m");
+    eprintln!("Complexity: {}", simped.complexity());
+    eprintln!("Steps:      {}", steps + 1);
+    Some(simped)
 }
 
 // (forall (a b) (+ a (succ b)) (succ (+ a b))) (forall (a) (+ a 0) a) (forall (a) (= a a) true) (= (+ (succ 0) (succ 0)) (succ (succ 0)))