100 lines
1.5 KiB
Ruby
100 lines
1.5 KiB
Ruby
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
|
|
|