From e7b1339790b63bbfc2c23ebb7f99ca6eea9d9a53 Mon Sep 17 00:00:00 2001 From: mehbark Date: Mon, 12 Jun 2023 21:11:30 -0400 Subject: [PATCH] i need to rewrite terms FASTER --- main.js | 44 ++++++++++++--- pi.slimp | 8 +++ src/main.rs | 151 ++++++++++++++++++++++++++++++++++++++++++++-------- 3 files changed, 175 insertions(+), 28 deletions(-) create mode 100644 pi.slimp diff --git a/main.js b/main.js index 1256702..6850ac2 100644 --- a/main.js +++ b/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 => - message.reply(mk_message(data.toString())) + let rules = ""; + 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) { - return "```lisp\n" + str.slice(0, 1975) + "```"; +function mk_message(str, stream = "", lang = "lisp") { + return `${stream}\n` + "```" + lang + "\n" + str.slice(0, 1975) + "```"; } diff --git a/pi.slimp b/pi.slimp new file mode 100644 index 0000000..ae9b7f6 --- /dev/null +++ b/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) diff --git a/src/main.rs b/src/main.rs index 04c35b1..306020a 100644 --- a/src/main.rs +++ b/src/main.rs @@ -14,8 +14,9 @@ static TABLE: Lazy> = Lazy::new(|| Mutex::new(SymbolTable::ne static FORALL: Lazy = 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 = Lazy::new(|| TABLE.lock().unwrap().intern("def").unwrap()); +static LET: Lazy = 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::(), } } + + #[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 { 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 { 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 { ')' => { 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 { 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 { } } + 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 { - vars: vars[1..].to_vec(), - lhs, - rhs: rw(&rule, rhs), + if vars.len() == 1 { + Rule::Concrete { lhs, rhs } + } else { + 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!( - f, - "∀{}, {lhs} ==> {rhs}", - vars.iter() + Rule::Forall { vars, lhs, rhs } => { + let vars = vars + .iter() .map(|v| TABLE.lock().unwrap().get(*v).unwrap().to_string()) - .join(" ") - ), - Rule::Concrete { lhs, rhs } => write!(f, "{lhs} ==> {rhs}"), + .join(" "); + let abs = format!("∀{vars},"); + 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>, 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 { + 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 { @@ -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(); - eprintln!("{}", rules.iter().map(ToString::to_string).join("\n")); - Some(simp(&rules, expr, step_limit, complexity_limit)) + let mut rules = parsed.iter().filter_map(make_rule).collect_vec(); + rules.sort_by_key(Rule::num_vars); + + 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)))