A Ruby interpreter for propositional logic

logical.rb

# frozen_string_literal: true

require "bundler/inline"

gemfile(true) do
  source "https://rubygems.org"

  git_source(:github) { |repo| "https://github.com/#{repo}.git" }

  gem "minitest"
end

require "minitest/autorun"

# simple propositional logic

class Token
  attr_reader :type, :value

  def initialize(type, value)
    @type = type
    @value = value
  end
end

class Lexer
  def initialize(input)
    @input = input
  end

  def tokens
    @input.split('').map do |char|
      # for each `char`, there are only 6 possible things to do
      case char
      when ' '
        next
      when '~'
        Token.new(:NOT, '~')
      when '&'
        Token.new(:AND, '&')
      when 'v'
        Token.new(:OR, 'v')
      when '>'
        Token.new(:IFSO, '>')
      when '('
        Token.new(:LPAREN, '(')
      when ')'
        Token.new(:RPAREN, ')')
      when 'T'
        Token.new(:TRUE, 'T')
      when 'F'
        Token.new(:FALSE, 'F')
      end
    end.compact
  end
end

module AST
  class Atom
    attr_reader :value

    def initialize(value)
      @value = value
    end
  end

  class UnaryOperation
    attr_reader :operand

    def initialize(operand)
      @operand = operand
    end
  end

  class BinaryOperation
    attr_reader :left, :right

    def initialize(left, right)
      @left = left
      @right = right
    end
  end

  class Negation < UnaryOperation
  end

  class Conjunction < BinaryOperation
  end

  class Disjunction < BinaryOperation
  end

  class Implication < BinaryOperation
  end
end

class Parser
  def initialize(tokens)
    @tokens = tokens
    @stream = @tokens.to_enum
    @current_token = @stream.next
  end

  def parse
    expression
  end

  # expression :: disjunction (IFSO expression)*
  def expression
    result = disjunction
    token = @current_token

    if token.type == :IFSO
      eat(:IFSO)
      result = AST::Implication.new(result, expression)
    end

    result
  end

  # disjunction :: conjunction (OR disjunction)* 
  def disjunction
    result = conjunction
    token = @current_token

    if token.type == :OR
      eat(:OR)
      result = AST::Disjunction.new(result, disjunction)
    end

    result
  end

  # conjunction :: formula (AND conjunction)* 
  def conjunction
    result = formula
    token = @current_token

    if token.type == :AND
      eat(:AND)
      result = AST::Conjunction.new(result, conjunction)
    end

    result
  end

  # formula :: (NOT)* formula | LPAREN expression RPAREN | term
  def formula
    token = @current_token

    if token.type == :NOT
      eat(:NOT)
      return AST::Negation.new(formula)
    elsif token.type == :LPAREN
      eat(:LPAREN)
      result = expression
      eat(:RPAREN)
      return result
    else
      return term
    end
  end

  # term :: TRUE | FALSE
  def term
    token = @current_token

    if token.type == :TRUE
      eat(:TRUE)
      return AST::Atom.new(true)
    elsif token.type == :FALSE
      eat(:FALSE)
      return AST::Atom.new(false)
    else
      raise "#{token.value} is an invalid term"
    end
  end

  def eat(token_type)
    raise 'ERROR' unless @current_token.type == token_type

    begin
      @current_token = @stream.next
    rescue StopIteration
    end
  end
end

class Interpreter
  def initialize(ast)
    @ast = ast
  end

  def interpret
    visit(@ast)
  end

  def visit(node)
    if node.is_a? AST::Atom
      visit_atom(node)
    elsif node.is_a? AST::Negation
      visit_negation(node)
    elsif node.is_a? AST::Conjunction
      visit_conjunction(node)
    elsif node.is_a? AST::Disjunction
      visit_disjunction(node)
    elsif node.is_a? AST::Implication
      visit_implication(node)
    end
  end

  def visit_atom(node)
    node.value
  end

  def visit_negation(node)
    case visit(node.operand)
    when true
      false
    when false
      true
    end
  end

  def visit_conjunction(node)
    case [visit(node.left), visit(node.right)]
    when [false, false]
      false
    when [false, true]
      false
    when [true, false]
      false
    when [true, true]
      true
    end
  end

  def visit_disjunction(node)
    case [visit(node.left), visit(node.right)]
    when [false, false]
      false
    when [false, true]
      true
    when [true, false]
      true
    when [true, true]
      true
    end
  end

  def visit_implication(node)
    case [visit(node.left), visit(node.right)]
    when [false, false]
      true
    when [false, true]
      true
    when [true, false]
      false
    when [true, true]
      true
    end
  end
end

def interpret(string)
  tokens = Lexer.new(string).tokens
  ast = Parser.new(tokens).parse
  Interpreter.new(ast).interpret
end

# -----------------------------------------------------------------------------

class LogicInterpreterTest < Minitest::Test
  def test_tokens
    assert_equal true, interpret('T')
    assert_equal false, interpret('F')
  end
  
  def test_negation
    assert_equal false, interpret('~T')
    assert_equal true, interpret('~F')
  end
  
  def test_conjunction
    assert_equal true, interpret('T & T')
    assert_equal false, interpret('T & F')
    assert_equal false, interpret('F & T')
    assert_equal false, interpret('F & F')
  end
  
  def test_disjunction
    assert_equal true, interpret('T v T')
    assert_equal true, interpret('T v F')
    assert_equal true, interpret('F v T')
    assert_equal false, interpret('F v F')
  end
  
  def test_implication
    assert_equal true, interpret('T > T')
    assert_equal false, interpret('T > F')
    assert_equal true, interpret('F > T')
    assert_equal true, interpret('F > F')
  end
  
  def test_simple_expressions
    assert_equal false, interpret('~F & F')
    assert_equal false, interpret('F v ~T')
  end
  
  def test_stacked_negations
    assert_equal true, interpret('~~T')
    assert_equal true, interpret('~~~F')
    assert_equal false, interpret('~~F & F')
    assert_equal true, interpret('F v ~~T')
  end
  
  def test_parenthetical_grouping
    assert_equal true, interpret('T & (F v T)')
    assert_equal false, interpret('~(T & (F v T))')
    assert_equal true, interpret('~(T & (F v T)) > T')
  end
  
  def test_operator_precedence
    assert_equal true, interpret('T & F v T')
    assert_equal false, interpret('T & F v ~T')
    assert_equal true, interpret('F & T v T')
    assert_equal true, interpret('~F & T v T')
  end
end