initial

cas.rb

@@ -0,0 +1,68 @@
+# frozen_string_literal: true
+
+require 'simp_rules'
+
+# TODO: natural numbers :)
+# TODO: little lang that transpiles to ruby
+
+# unnecessary if i standardize on parenthezing every binary op anyway!
+def lispify(bla)
+  if bla.is_a? Array
+    l  = bla[0]
+    op = bla[1]
+    r  = bla[2]
+    [op, [lispify(l), lispify(r)]]
+  else
+    bla
+  end
+end
+
+# doesn't account for actually important stuff, gonna need to do equal'
+def simp_rule(); end
+
+def simp(expr, rules = SIMP_RULES, limit: 413)
+  expr = expr.dup
+
+  limit.times do
+    rules.each do |rule|
+      expr = simp_single(expr, rule)
+    end
+  end
+
+  expr
+end
+
+def simp_single(expr, rule)
+  if rule.concrete?
+    expr = simp_applied_rule(expr, rule)
+  else
+    targets = potential_rule_targets(expr)
+    targets.each do |target|
+      concrete_rule = rule.clone.concrete(target)
+      expr = simp_single(expr, concrete_rule)
+    end
+  end
+
+  expr
+end
+
+def simp_applied_rule(expr, rule)
+  lhs = rule.lhs
+  rhs = rule.rhs
+
+  if expr == lhs
+    rhs
+  elsif expr.is_a? Array
+    expr.map { |expr| simp_applied_rule(expr, rule) }
+  else
+    expr
+  end
+end
+
+def potential_rule_targets(expr)
+  if expr.is_a? Array
+    (expr + expr.flatten).uniq
+  else
+    [expr]
+  end
+end

messing_with_eq.rb

@@ -0,0 +1,11 @@
+# frozen_string_literal: true
+
+require 'cas'
+require 'rule'
+require 'simp_rules'
+require 'rw_rules'
+
+def add_right_cancel
+  rule([%i[a + c], :==, %i[b + c]] => %i[a == b]).forall(:a, :b, :c)
+end
+

rule.rb

@@ -0,0 +1,99 @@
+class Rule
+  def forall(*syms)
+    syms.each do |sym|
+      forall_single(sym)
+    end
+
+    self
+  end
+
+  def forall_single(sym)
+    @generality ||= 0
+    @generality += 1
+    @syms ||= []
+    @syms += [sym]
+
+    self
+  end
+
+  def initialize(name, hash)
+    @name = name
+    @lhs = hash.keys.last
+    @rhs = hash.values.last
+    @syms ||= []
+    @generality ||= 0
+  end
+
+  def general?
+    @generality.positive?
+  end
+
+  def concrete?
+    !general?
+  end
+
+  # concrete is a verb :]
+  def concrete(*xs)
+    xs.each { |x| concrete_single(x) }
+    self
+  end
+
+  def concrete_single(x)
+    unless concrete?
+      sym = @syms.delete_at 0
+      replace_rule = Rule.new(sym => x)
+      @lhs = simp_single(@lhs, replace_rule)
+      @rhs = simp_single(@rhs, replace_rule)
+
+      @generality -= 1
+      @sym = nil
+    end
+
+    self
+  end
+
+  def apply(expr)
+    simp_single(expr, self)
+  end
+
+  def swap
+    rule = dup
+    rule.lhs = @rhs
+    rule.rhs = @lhs
+    rule
+  end
+
+  def inspect
+    "#<Rule \"#{@name}\": #{forall_display}#{pretty_side @lhs} <=> #{pretty_side @rhs}>"
+  end
+
+  def forall_display
+    if concrete?
+      ''
+    else
+      "∀#{@syms.join ' '}, "
+    end
+  end
+
+  attr_accessor :lhs, :rhs, :generality, :name
+
+  def ==(other)
+    other.is_a? Rule and
+      @lhs == other.lhs and
+      @rhs == other.rhs and
+      @generality == other.generality
+  end
+end
+
+def pretty_side(side)
+  if side.is_a? Array
+    "(#{side.map { |side_| pretty_side side_ }.join ' '})"
+  else
+    side.to_s
+  end
+end
+
+def rule(*syms)
+  Rule.new(*syms)
+end
+

rw_rules.rb

@@ -0,0 +1,19 @@
+# frozen_string_literal: true
+
+require 'rule'
+
+def rule(*args)
+  Rule.new(*args)
+end
+
+# not a simp rule! (loops)
+def add_assoc
+  rule(
+    [%i[a + b], :+, :c] => [:a, :+, %i[b + c]]
+  ).forall(:a, :b, :c)
+end
+
+RW_RULES = [
+  add_assoc,
+  rule(%i[a + b] => %i[b + a]).forall(:a, :b)
+].freeze

simp_rules.rb

@@ -0,0 +1,23 @@
+# frozen_string_literal: true
+
+require 'rule'
+
+class SimpRules
+  @@simp_rules = []
+
+  def self.register(rule)
+    @@simp_rules.push(rule)
+  end
+
+  def self.register_new(*args)
+    register(rule(*args))
+  end
+end
+
+SimpRules.register_new('one_plus_one', [1, :+, 1] => 2)
+SimpRules.register_new('add_zero', [:x, :+, 0] => :x).forall(:x)
+SimpRules.register_new('zero_add', [0, :+, :x] => :x).forall(:x)
+SimpRules.register_new('mul_one', [:x, :*, 1] => :x).forall(:x)
+SimpRules.register_new('one_mul', [1, :*, :x] => :x).forall(:x)
+SimpRules.register_new('mul_zero', [:x, :*, 0] => 0).forall(:x)
+SimpRules.register_new('zero_mul', [0, :*, :x] => 0).forall(:x)

tree_solve.rb

@@ -0,0 +1,49 @@
+# frozen_string_literal: true
+
+require 'cas'
+require 'rule'
+require 'rw_rules'
+require 'simp_rules'
+
+# sucks
+class Solver
+  def initialize(solve_for: :x, given: [])
+    @solve_for = solve_for
+    @visited = MySet.new([given])
+  end
+
+  def winner
+    found = @visited.find { |g| g.lhs == @solve_for || g.rhs == @solve_for && g.lhs != g.rhs }
+    return unless found
+
+    simp(if found.lhs == @solve_for
+      found.rhs
+    else
+      found.lhs
+    end)
+  end
+
+  def elaborate!
+    @visited.each do |t|
+      (SIMP_RULES + RW_RULES).each do |rule|
+        @visited.add(rule.apply(t))
+      end
+    end
+
+    simp!
+  end
+
+  def simp!
+    @visited.map! { |g| g.simp }
+
+    self
+  end
+end
+
+class MySet < Set
+  def add(item)
+    super.add(item) unless any? { |i| item == i }
+
+    self
+  end
+end