class Korekto::Statement

Attributes

code[R]
regexp[R]
section[R]
statement_number[R]
title[R]

Public Class Methods

new(statement,code,title,section,statement_number,context) click to toggle source
# File lib/korekto/statement.rb, line 4
def initialize(statement,code,title,section,statement_number,context)
  @statement,@code,@title,@section,@statement_number,@context =
    statement,code,title,section,statement_number,context
  @statement.freeze; @section.freeze; @statement_number.freeze
  syntax_check unless @statement[0]=='/' and @statement[-1]=='/' and ['A','L','M','E','I'].include?(@code[0])
  @regexp = nil
  set_acceptance_code
  @code.freeze; @title.freeze; @regexp.freeze
end

Public Instance Methods

conclusion() click to toggle source
# File lib/korekto/statement.rb, line 185
def conclusion
  expected_instantiations(n:0)
  inference,s1,s2 = heap_combos_search('I')
  set_statement(support(inference,s1,s2), inference.title)
end
definition() click to toggle source
# File lib/korekto/statement.rb, line 191
def definition
  expected_instantiations(@title)
  set_statement
end
detect_statement(type) click to toggle source

Searches

# File lib/korekto/statement.rb, line 102
def detect_statement(type)
  statement = @context.type(type).detect do |statement|
    statement.match? @statement
  end
  raise Error, "does not match any '#{type}' statement" unless statement
  return statement
end
expected_instantiations(title=nil, n:nil) click to toggle source

Defined/Undefined

# File lib/korekto/statement.rb, line 132
def expected_instantiations(title=nil, n:nil)
  undefined = @context.symbols.undefined(self)
  if n ||= title&.match(/[1-9]\d*/)&.to_s&.to_i
    raise Error, "expected #{n} undefined: #{undefined.join(' ')}" unless n==undefined.length
  else
    raise Error, 'nothing was undefined' if undefined.empty?
  end
end
instantiation() click to toggle source
# File lib/korekto/statement.rb, line 179
def instantiation
  existential,s1 = heap_search('E')
  expected_instantiations(existential.title)
  set_statement(support(existential,s1), existential.title)
end
literal_regexp?(= @statement[0]=='/' && @statement[-1]=='/') click to toggle source
# File lib/korekto/statement.rb, line 20
  def literal_regexp?   = @statement[0]=='/' && @statement[-1]=='/'

  private

  def syntax_check
    @context.syntax.each do |rule|
      raise Error, "syntax: #{rule}" unless @statement.instance_eval(rule)
    rescue # other than Korekto::Error < Exception
      raise Error, "#{$!.class}: #{rule}"
    end
  end

  def set_acceptance_code
    case @code[0] # type
    when 'P'
      postulate
    when 'D'
      definition
    when 'C'
      conclusion
    when 'X'
      instantiation
    when 'R'
      result
    when 'S'
      set
    when 'T'
      tautology
    when 'A', 'L'
      # Axiom=>Tautoloty, Let=>Set,
      pattern_type(0)
    when 'M', 'E'
      # Map=>Result, Existential=>Instantiation(X)
      pattern_type(1)
    when 'I'
      # Inference=>Conclusion
      pattern_type(2)
    when 'W'
      ['T','S','R','X','C'].any? do |code|
        begin
          @code[0]=code
          set_acceptance_code
          true
        rescue Error
          false
        end
      end or raise Error, 'did not match any statement pattern'
    else
      raise Error, "statement type #{@code[0]} not implemented"
    end
  end

  # Common helper

  def set_statement(support=nil, title=nil)
    @code = "#{@code[0]}#{@statement_number}"
    @code += '.' + @section unless @section=='-'
    @code += "/#{support}" if support
    @title = title if (title=title&.split(':',2)&.first) and not title.empty?
  end

  def support(*s)
    support = []
    s.each do |s|
      c = s.code.split('/',2)[0]
      support.push(c)
    end
    return support.join(',')
  end

  # Pattern helpers

  def newlines_count(n)
    raise Error, "expected #{n} newlines" unless n==@regexp.inspect.gsub('\\\\','').scan('\\n').length
  end

  def set_regexp
    @regexp = @context.symbols.s2r(@statement)
  end

  # Searches

  def detect_statement(type)
    statement = @context.type(type).detect do |statement|
      statement.match? @statement
    end
    raise Error, "does not match any '#{type}' statement" unless statement
    return statement
  end

  def heap_combos_search(type)
    @context.heap.combos do |s1, s2|
      compound = [s1,s2,@statement].join("\n")
      @context.type(type).each do |inference|
        return inference,s1,s2 if inference.match?(compound)
      end
    end
    raise Error, "does not match any '#{type}' statement"
  end

  def heap_search(type)
    @context.heap.each do |s1|
      compound = [s1,@statement].join("\n")
      @context.type(type).each do |s0|
        return s0,s1 if s0.match?(compound)
      end
    end
    raise Error, "does not match any '#{type}' statement"
  end

  # Defined/Undefined

  def expected_instantiations(title=nil, n:nil)
    undefined = @context.symbols.undefined(self)
    if n ||= title&.match(/[1-9]\d*/)&.to_s&.to_i
      raise Error, "expected #{n} undefined: #{undefined.join(' ')}" unless n==undefined.length
    else
      raise Error, 'nothing was undefined' if undefined.empty?
    end
  end

  def undefined_in_pattern
    @title = @title.split(':',2).first if @title
    undefined = @context.symbols.undefined(self)
    @title = "#{@title}: #{undefined.join(' ')}" unless undefined.empty?
  end

  # Statement type processing

  def pattern_type(nl)
    set_regexp
    newlines_count(nl)
    undefined_in_pattern
    follows = @context.heap.to_a[0..nl].reverse
    if @regexp.match? follows.map{_1.to_s}.join("\n")
      set_statement(support(*follows))
    else
      set_statement
    end
  end

  def tautology
    expected_instantiations(n:0)
    axiom = detect_statement('A')
    set_statement(support(axiom), axiom.title)
  end

  def set
    let = detect_statement('L')
    expected_instantiations(let.title)
    set_statement(support(let), let.title)
  end

  def result
    expected_instantiations(n:0)
    mapping,s1 = heap_search('M')
    set_statement(support(mapping,s1), mapping.title)
  end

  def instantiation
    existential,s1 = heap_search('E')
    expected_instantiations(existential.title)
    set_statement(support(existential,s1), existential.title)
  end

  def conclusion
    expected_instantiations(n:0)
    inference,s1,s2 = heap_combos_search('I')
    set_statement(support(inference,s1,s2), inference.title)
  end

  def definition
    expected_instantiations(@title)
    set_statement
  end

  def postulate
    expected_instantiations(n:0)
    set_statement
  end
end
match?(statement) click to toggle source
# File lib/korekto/statement.rb, line 17
def match?(statement) = @regexp.match?(statement)
def scan(regex, &blk) = @statement.scan(regex, &blk)
def pattern?          = !@regexp.nil?
def literal_regexp?   = @statement[0]=='/' && @statement[-1]=='/'

private

def syntax_check
  @context.syntax.each do |rule|
    raise Error, "syntax: #{rule}" unless @statement.instance_eval(rule)
  rescue # other than Korekto::Error < Exception
    raise Error, "#{$!.class}: #{rule}"
  end
end

def set_acceptance_code
  case @code[0] # type
  when 'P'
    postulate
  when 'D'
    definition
  when 'C'
    conclusion
  when 'X'
    instantiation
  when 'R'
    result
  when 'S'
    set
  when 'T'
    tautology
  when 'A', 'L'
    # Axiom=>Tautoloty, Let=>Set,
    pattern_type(0)
  when 'M', 'E'
    # Map=>Result, Existential=>Instantiation(X)
    pattern_type(1)
  when 'I'
    # Inference=>Conclusion
    pattern_type(2)
  when 'W'
    ['T','S','R','X','C'].any? do |code|
      begin
        @code[0]=code
        set_acceptance_code
        true
      rescue Error
        false
      end
    end or raise Error, 'did not match any statement pattern'
  else
    raise Error, "statement type #{@code[0]} not implemented"
  end
end

# Common helper

def set_statement(support=nil, title=nil)
  @code = "#{@code[0]}#{@statement_number}"
  @code += '.' + @section unless @section=='-'
  @code += "/#{support}" if support
  @title = title if (title=title&.split(':',2)&.first) and not title.empty?
end

def support(*s)
  support = []
  s.each do |s|
    c = s.code.split('/',2)[0]
    support.push(c)
  end
  return support.join(',')
end

# Pattern helpers

def newlines_count(n)
  raise Error, "expected #{n} newlines" unless n==@regexp.inspect.gsub('\\\\','').scan('\\n').length
end

def set_regexp
  @regexp = @context.symbols.s2r(@statement)
end

# Searches

def detect_statement(type)
  statement = @context.type(type).detect do |statement|
    statement.match? @statement
  end
  raise Error, "does not match any '#{type}' statement" unless statement
  return statement
end

def heap_combos_search(type)
  @context.heap.combos do |s1, s2|
    compound = [s1,s2,@statement].join("\n")
    @context.type(type).each do |inference|
      return inference,s1,s2 if inference.match?(compound)
    end
  end
  raise Error, "does not match any '#{type}' statement"
end

def heap_search(type)
  @context.heap.each do |s1|
    compound = [s1,@statement].join("\n")
    @context.type(type).each do |s0|
      return s0,s1 if s0.match?(compound)
    end
  end
  raise Error, "does not match any '#{type}' statement"
end

# Defined/Undefined

def expected_instantiations(title=nil, n:nil)
  undefined = @context.symbols.undefined(self)
  if n ||= title&.match(/[1-9]\d*/)&.to_s&.to_i
    raise Error, "expected #{n} undefined: #{undefined.join(' ')}" unless n==undefined.length
  else
    raise Error, 'nothing was undefined' if undefined.empty?
  end
end

def undefined_in_pattern
  @title = @title.split(':',2).first if @title
  undefined = @context.symbols.undefined(self)
  @title = "#{@title}: #{undefined.join(' ')}" unless undefined.empty?
end

# Statement type processing

def pattern_type(nl)
  set_regexp
  newlines_count(nl)
  undefined_in_pattern
  follows = @context.heap.to_a[0..nl].reverse
  if @regexp.match? follows.map{_1.to_s}.join("\n")
    set_statement(support(*follows))
  else
    set_statement
  end
end

def tautology
  expected_instantiations(n:0)
  axiom = detect_statement('A')
  set_statement(support(axiom), axiom.title)
end

def set
  let = detect_statement('L')
  expected_instantiations(let.title)
  set_statement(support(let), let.title)
end

def result
  expected_instantiations(n:0)
  mapping,s1 = heap_search('M')
  set_statement(support(mapping,s1), mapping.title)
end

def instantiation
  existential,s1 = heap_search('E')
  expected_instantiations(existential.title)
  set_statement(support(existential,s1), existential.title)
end

def conclusion
  expected_instantiations(n:0)
  inference,s1,s2 = heap_combos_search('I')
  set_statement(support(inference,s1,s2), inference.title)
end

def definition
  expected_instantiations(@title)
  set_statement
end

def postulate
  expected_instantiations(n:0)
  set_statement
end
newlines_count(n) click to toggle source

Pattern helpers

# File lib/korekto/statement.rb, line 92
def newlines_count(n)
  raise Error, "expected #{n} newlines" unless n==@regexp.inspect.gsub('\\\\','').scan('\\n').length
end
pattern?(= !@regexp.nil?) click to toggle source
# File lib/korekto/statement.rb, line 19
  def pattern?          = !@regexp.nil?
  def literal_regexp?   = @statement[0]=='/' && @statement[-1]=='/'

  private

  def syntax_check
    @context.syntax.each do |rule|
      raise Error, "syntax: #{rule}" unless @statement.instance_eval(rule)
    rescue # other than Korekto::Error < Exception
      raise Error, "#{$!.class}: #{rule}"
    end
  end

  def set_acceptance_code
    case @code[0] # type
    when 'P'
      postulate
    when 'D'
      definition
    when 'C'
      conclusion
    when 'X'
      instantiation
    when 'R'
      result
    when 'S'
      set
    when 'T'
      tautology
    when 'A', 'L'
      # Axiom=>Tautoloty, Let=>Set,
      pattern_type(0)
    when 'M', 'E'
      # Map=>Result, Existential=>Instantiation(X)
      pattern_type(1)
    when 'I'
      # Inference=>Conclusion
      pattern_type(2)
    when 'W'
      ['T','S','R','X','C'].any? do |code|
        begin
          @code[0]=code
          set_acceptance_code
          true
        rescue Error
          false
        end
      end or raise Error, 'did not match any statement pattern'
    else
      raise Error, "statement type #{@code[0]} not implemented"
    end
  end

  # Common helper

  def set_statement(support=nil, title=nil)
    @code = "#{@code[0]}#{@statement_number}"
    @code += '.' + @section unless @section=='-'
    @code += "/#{support}" if support
    @title = title if (title=title&.split(':',2)&.first) and not title.empty?
  end

  def support(*s)
    support = []
    s.each do |s|
      c = s.code.split('/',2)[0]
      support.push(c)
    end
    return support.join(',')
  end

  # Pattern helpers

  def newlines_count(n)
    raise Error, "expected #{n} newlines" unless n==@regexp.inspect.gsub('\\\\','').scan('\\n').length
  end

  def set_regexp
    @regexp = @context.symbols.s2r(@statement)
  end

  # Searches

  def detect_statement(type)
    statement = @context.type(type).detect do |statement|
      statement.match? @statement
    end
    raise Error, "does not match any '#{type}' statement" unless statement
    return statement
  end

  def heap_combos_search(type)
    @context.heap.combos do |s1, s2|
      compound = [s1,s2,@statement].join("\n")
      @context.type(type).each do |inference|
        return inference,s1,s2 if inference.match?(compound)
      end
    end
    raise Error, "does not match any '#{type}' statement"
  end

  def heap_search(type)
    @context.heap.each do |s1|
      compound = [s1,@statement].join("\n")
      @context.type(type).each do |s0|
        return s0,s1 if s0.match?(compound)
      end
    end
    raise Error, "does not match any '#{type}' statement"
  end

  # Defined/Undefined

  def expected_instantiations(title=nil, n:nil)
    undefined = @context.symbols.undefined(self)
    if n ||= title&.match(/[1-9]\d*/)&.to_s&.to_i
      raise Error, "expected #{n} undefined: #{undefined.join(' ')}" unless n==undefined.length
    else
      raise Error, 'nothing was undefined' if undefined.empty?
    end
  end

  def undefined_in_pattern
    @title = @title.split(':',2).first if @title
    undefined = @context.symbols.undefined(self)
    @title = "#{@title}: #{undefined.join(' ')}" unless undefined.empty?
  end

  # Statement type processing

  def pattern_type(nl)
    set_regexp
    newlines_count(nl)
    undefined_in_pattern
    follows = @context.heap.to_a[0..nl].reverse
    if @regexp.match? follows.map{_1.to_s}.join("\n")
      set_statement(support(*follows))
    else
      set_statement
    end
  end

  def tautology
    expected_instantiations(n:0)
    axiom = detect_statement('A')
    set_statement(support(axiom), axiom.title)
  end

  def set
    let = detect_statement('L')
    expected_instantiations(let.title)
    set_statement(support(let), let.title)
  end

  def result
    expected_instantiations(n:0)
    mapping,s1 = heap_search('M')
    set_statement(support(mapping,s1), mapping.title)
  end

  def instantiation
    existential,s1 = heap_search('E')
    expected_instantiations(existential.title)
    set_statement(support(existential,s1), existential.title)
  end

  def conclusion
    expected_instantiations(n:0)
    inference,s1,s2 = heap_combos_search('I')
    set_statement(support(inference,s1,s2), inference.title)
  end

  def definition
    expected_instantiations(@title)
    set_statement
  end

  def postulate
    expected_instantiations(n:0)
    set_statement
  end
end
end
pattern_type(nl) click to toggle source

Statement type processing

# File lib/korekto/statement.rb, line 149
def pattern_type(nl)
  set_regexp
  newlines_count(nl)
  undefined_in_pattern
  follows = @context.heap.to_a[0..nl].reverse
  if @regexp.match? follows.map{_1.to_s}.join("\n")
    set_statement(support(*follows))
  else
    set_statement
  end
end
postulate() click to toggle source
# File lib/korekto/statement.rb, line 196
def postulate
  expected_instantiations(n:0)
  set_statement
end
result() click to toggle source
# File lib/korekto/statement.rb, line 173
def result
  expected_instantiations(n:0)
  mapping,s1 = heap_search('M')
  set_statement(support(mapping,s1), mapping.title)
end
scan(regex, &blk) click to toggle source
# File lib/korekto/statement.rb, line 18
  def scan(regex, &blk) = @statement.scan(regex, &blk)
  def pattern?          = !@regexp.nil?
  def literal_regexp?   = @statement[0]=='/' && @statement[-1]=='/'

  private

  def syntax_check
    @context.syntax.each do |rule|
      raise Error, "syntax: #{rule}" unless @statement.instance_eval(rule)
    rescue # other than Korekto::Error < Exception
      raise Error, "#{$!.class}: #{rule}"
    end
  end

  def set_acceptance_code
    case @code[0] # type
    when 'P'
      postulate
    when 'D'
      definition
    when 'C'
      conclusion
    when 'X'
      instantiation
    when 'R'
      result
    when 'S'
      set
    when 'T'
      tautology
    when 'A', 'L'
      # Axiom=>Tautoloty, Let=>Set,
      pattern_type(0)
    when 'M', 'E'
      # Map=>Result, Existential=>Instantiation(X)
      pattern_type(1)
    when 'I'
      # Inference=>Conclusion
      pattern_type(2)
    when 'W'
      ['T','S','R','X','C'].any? do |code|
        begin
          @code[0]=code
          set_acceptance_code
          true
        rescue Error
          false
        end
      end or raise Error, 'did not match any statement pattern'
    else
      raise Error, "statement type #{@code[0]} not implemented"
    end
  end

  # Common helper

  def set_statement(support=nil, title=nil)
    @code = "#{@code[0]}#{@statement_number}"
    @code += '.' + @section unless @section=='-'
    @code += "/#{support}" if support
    @title = title if (title=title&.split(':',2)&.first) and not title.empty?
  end

  def support(*s)
    support = []
    s.each do |s|
      c = s.code.split('/',2)[0]
      support.push(c)
    end
    return support.join(',')
  end

  # Pattern helpers

  def newlines_count(n)
    raise Error, "expected #{n} newlines" unless n==@regexp.inspect.gsub('\\\\','').scan('\\n').length
  end

  def set_regexp
    @regexp = @context.symbols.s2r(@statement)
  end

  # Searches

  def detect_statement(type)
    statement = @context.type(type).detect do |statement|
      statement.match? @statement
    end
    raise Error, "does not match any '#{type}' statement" unless statement
    return statement
  end

  def heap_combos_search(type)
    @context.heap.combos do |s1, s2|
      compound = [s1,s2,@statement].join("\n")
      @context.type(type).each do |inference|
        return inference,s1,s2 if inference.match?(compound)
      end
    end
    raise Error, "does not match any '#{type}' statement"
  end

  def heap_search(type)
    @context.heap.each do |s1|
      compound = [s1,@statement].join("\n")
      @context.type(type).each do |s0|
        return s0,s1 if s0.match?(compound)
      end
    end
    raise Error, "does not match any '#{type}' statement"
  end

  # Defined/Undefined

  def expected_instantiations(title=nil, n:nil)
    undefined = @context.symbols.undefined(self)
    if n ||= title&.match(/[1-9]\d*/)&.to_s&.to_i
      raise Error, "expected #{n} undefined: #{undefined.join(' ')}" unless n==undefined.length
    else
      raise Error, 'nothing was undefined' if undefined.empty?
    end
  end

  def undefined_in_pattern
    @title = @title.split(':',2).first if @title
    undefined = @context.symbols.undefined(self)
    @title = "#{@title}: #{undefined.join(' ')}" unless undefined.empty?
  end

  # Statement type processing

  def pattern_type(nl)
    set_regexp
    newlines_count(nl)
    undefined_in_pattern
    follows = @context.heap.to_a[0..nl].reverse
    if @regexp.match? follows.map{_1.to_s}.join("\n")
      set_statement(support(*follows))
    else
      set_statement
    end
  end

  def tautology
    expected_instantiations(n:0)
    axiom = detect_statement('A')
    set_statement(support(axiom), axiom.title)
  end

  def set
    let = detect_statement('L')
    expected_instantiations(let.title)
    set_statement(support(let), let.title)
  end

  def result
    expected_instantiations(n:0)
    mapping,s1 = heap_search('M')
    set_statement(support(mapping,s1), mapping.title)
  end

  def instantiation
    existential,s1 = heap_search('E')
    expected_instantiations(existential.title)
    set_statement(support(existential,s1), existential.title)
  end

  def conclusion
    expected_instantiations(n:0)
    inference,s1,s2 = heap_combos_search('I')
    set_statement(support(inference,s1,s2), inference.title)
  end

  def definition
    expected_instantiations(@title)
    set_statement
  end

  def postulate
    expected_instantiations(n:0)
    set_statement
  end
end
set() click to toggle source
# File lib/korekto/statement.rb, line 167
def set
  let = detect_statement('L')
  expected_instantiations(let.title)
  set_statement(support(let), let.title)
end
set_acceptance_code() click to toggle source
# File lib/korekto/statement.rb, line 32
def set_acceptance_code
  case @code[0] # type
  when 'P'
    postulate
  when 'D'
    definition
  when 'C'
    conclusion
  when 'X'
    instantiation
  when 'R'
    result
  when 'S'
    set
  when 'T'
    tautology
  when 'A', 'L'
    # Axiom=>Tautoloty, Let=>Set,
    pattern_type(0)
  when 'M', 'E'
    # Map=>Result, Existential=>Instantiation(X)
    pattern_type(1)
  when 'I'
    # Inference=>Conclusion
    pattern_type(2)
  when 'W'
    ['T','S','R','X','C'].any? do |code|
      begin
        @code[0]=code
        set_acceptance_code
        true
      rescue Error
        false
      end
    end or raise Error, 'did not match any statement pattern'
  else
    raise Error, "statement type #{@code[0]} not implemented"
  end
end
set_regexp() click to toggle source
# File lib/korekto/statement.rb, line 96
def set_regexp
  @regexp = @context.symbols.s2r(@statement)
end
set_statement(support=nil, title=nil) click to toggle source

Common helper

# File lib/korekto/statement.rb, line 74
def set_statement(support=nil, title=nil)
  @code = "#{@code[0]}#{@statement_number}"
  @code += '.' + @section unless @section=='-'
  @code += "/#{support}" if support
  @title = title if (title=title&.split(':',2)&.first) and not title.empty?
end
support(*s) click to toggle source
# File lib/korekto/statement.rb, line 81
def support(*s)
  support = []
  s.each do |s|
    c = s.code.split('/',2)[0]
    support.push(c)
  end
  return support.join(',')
end
syntax_check() click to toggle source
# File lib/korekto/statement.rb, line 24
def syntax_check
  @context.syntax.each do |rule|
    raise Error, "syntax: #{rule}" unless @statement.instance_eval(rule)
  rescue # other than Korekto::Error < Exception
    raise Error, "#{$!.class}: #{rule}"
  end
end
tautology() click to toggle source
# File lib/korekto/statement.rb, line 161
def tautology
  expected_instantiations(n:0)
  axiom = detect_statement('A')
  set_statement(support(axiom), axiom.title)
end
to_s(= @statement) click to toggle source
# File lib/korekto/statement.rb, line 15
def to_s              = @statement
def to_str            = @statement
def match?(statement) = @regexp.match?(statement)
def scan(regex, &blk) = @statement.scan(regex, &blk)
def pattern?          = !@regexp.nil?
def literal_regexp?   = @statement[0]=='/' && @statement[-1]=='/'

private

def syntax_check
  @context.syntax.each do |rule|
    raise Error, "syntax: #{rule}" unless @statement.instance_eval(rule)
  rescue # other than Korekto::Error < Exception
    raise Error, "#{$!.class}: #{rule}"
  end
end

def set_acceptance_code
  case @code[0] # type
  when 'P'
    postulate
  when 'D'
    definition
  when 'C'
    conclusion
  when 'X'
    instantiation
  when 'R'
    result
  when 'S'
    set
  when 'T'
    tautology
  when 'A', 'L'
    # Axiom=>Tautoloty, Let=>Set,
    pattern_type(0)
  when 'M', 'E'
    # Map=>Result, Existential=>Instantiation(X)
    pattern_type(1)
  when 'I'
    # Inference=>Conclusion
    pattern_type(2)
  when 'W'
    ['T','S','R','X','C'].any? do |code|
      begin
        @code[0]=code
        set_acceptance_code
        true
      rescue Error
        false
      end
    end or raise Error, 'did not match any statement pattern'
  else
    raise Error, "statement type #{@code[0]} not implemented"
  end
end

# Common helper

def set_statement(support=nil, title=nil)
  @code = "#{@code[0]}#{@statement_number}"
  @code += '.' + @section unless @section=='-'
  @code += "/#{support}" if support
  @title = title if (title=title&.split(':',2)&.first) and not title.empty?
end

def support(*s)
  support = []
  s.each do |s|
    c = s.code.split('/',2)[0]
    support.push(c)
  end
  return support.join(',')
end

# Pattern helpers

def newlines_count(n)
  raise Error, "expected #{n} newlines" unless n==@regexp.inspect.gsub('\\\\','').scan('\\n').length
end

def set_regexp
  @regexp = @context.symbols.s2r(@statement)
end

# Searches

def detect_statement(type)
  statement = @context.type(type).detect do |statement|
    statement.match? @statement
  end
  raise Error, "does not match any '#{type}' statement" unless statement
  return statement
end

def heap_combos_search(type)
  @context.heap.combos do |s1, s2|
    compound = [s1,s2,@statement].join("\n")
    @context.type(type).each do |inference|
      return inference,s1,s2 if inference.match?(compound)
    end
  end
  raise Error, "does not match any '#{type}' statement"
end

def heap_search(type)
  @context.heap.each do |s1|
    compound = [s1,@statement].join("\n")
    @context.type(type).each do |s0|
      return s0,s1 if s0.match?(compound)
    end
  end
  raise Error, "does not match any '#{type}' statement"
end

# Defined/Undefined

def expected_instantiations(title=nil, n:nil)
  undefined = @context.symbols.undefined(self)
  if n ||= title&.match(/[1-9]\d*/)&.to_s&.to_i
    raise Error, "expected #{n} undefined: #{undefined.join(' ')}" unless n==undefined.length
  else
    raise Error, 'nothing was undefined' if undefined.empty?
  end
end

def undefined_in_pattern
  @title = @title.split(':',2).first if @title
  undefined = @context.symbols.undefined(self)
  @title = "#{@title}: #{undefined.join(' ')}" unless undefined.empty?
end

# Statement type processing

def pattern_type(nl)
  set_regexp
  newlines_count(nl)
  undefined_in_pattern
  follows = @context.heap.to_a[0..nl].reverse
  if @regexp.match? follows.map{_1.to_s}.join("\n")
    set_statement(support(*follows))
  else
    set_statement
  end
end

def tautology
  expected_instantiations(n:0)
  axiom = detect_statement('A')
  set_statement(support(axiom), axiom.title)
end

def set
  let = detect_statement('L')
  expected_instantiations(let.title)
  set_statement(support(let), let.title)
end

def result
  expected_instantiations(n:0)
  mapping,s1 = heap_search('M')
  set_statement(support(mapping,s1), mapping.title)
end

def instantiation
  existential,s1 = heap_search('E')
  expected_instantiations(existential.title)
  set_statement(support(existential,s1), existential.title)
end

def conclusion
  expected_instantiations(n:0)
  inference,s1,s2 = heap_combos_search('I')
  set_statement(support(inference,s1,s2), inference.title)
end

def definition
  expected_instantiations(@title)
  set_statement
end

def postulate
  expected_instantiations(n:0)
  
to_str(= @statement) click to toggle source
# File lib/korekto/statement.rb, line 16
def to_str            = @statement
def match?(statement) = @regexp.match?(statement)
def scan(regex, &blk) = @statement.scan(regex, &blk)
def pattern?          = !@regexp.nil?
def literal_regexp?   = @statement[0]=='/' && @statement[-1]=='/'

private

def syntax_check
  @context.syntax.each do |rule|
    raise Error, "syntax: #{rule}" unless @statement.instance_eval(rule)
  rescue # other than Korekto::Error < Exception
    raise Error, "#{$!.class}: #{rule}"
  end
end

def set_acceptance_code
  case @code[0] # type
  when 'P'
    postulate
  when 'D'
    definition
  when 'C'
    conclusion
  when 'X'
    instantiation
  when 'R'
    result
  when 'S'
    set
  when 'T'
    tautology
  when 'A', 'L'
    # Axiom=>Tautoloty, Let=>Set,
    pattern_type(0)
  when 'M', 'E'
    # Map=>Result, Existential=>Instantiation(X)
    pattern_type(1)
  when 'I'
    # Inference=>Conclusion
    pattern_type(2)
  when 'W'
    ['T','S','R','X','C'].any? do |code|
      begin
        @code[0]=code
        set_acceptance_code
        true
      rescue Error
        false
      end
    end or raise Error, 'did not match any statement pattern'
  else
    raise Error, "statement type #{@code[0]} not implemented"
  end
end

# Common helper

def set_statement(support=nil, title=nil)
  @code = "#{@code[0]}#{@statement_number}"
  @code += '.' + @section unless @section=='-'
  @code += "/#{support}" if support
  @title = title if (title=title&.split(':',2)&.first) and not title.empty?
end

def support(*s)
  support = []
  s.each do |s|
    c = s.code.split('/',2)[0]
    support.push(c)
  end
  return support.join(',')
end

# Pattern helpers

def newlines_count(n)
  raise Error, "expected #{n} newlines" unless n==@regexp.inspect.gsub('\\\\','').scan('\\n').length
end

def set_regexp
  @regexp = @context.symbols.s2r(@statement)
end

# Searches

def detect_statement(type)
  statement = @context.type(type).detect do |statement|
    statement.match? @statement
  end
  raise Error, "does not match any '#{type}' statement" unless statement
  return statement
end

def heap_combos_search(type)
  @context.heap.combos do |s1, s2|
    compound = [s1,s2,@statement].join("\n")
    @context.type(type).each do |inference|
      return inference,s1,s2 if inference.match?(compound)
    end
  end
  raise Error, "does not match any '#{type}' statement"
end

def heap_search(type)
  @context.heap.each do |s1|
    compound = [s1,@statement].join("\n")
    @context.type(type).each do |s0|
      return s0,s1 if s0.match?(compound)
    end
  end
  raise Error, "does not match any '#{type}' statement"
end

# Defined/Undefined

def expected_instantiations(title=nil, n:nil)
  undefined = @context.symbols.undefined(self)
  if n ||= title&.match(/[1-9]\d*/)&.to_s&.to_i
    raise Error, "expected #{n} undefined: #{undefined.join(' ')}" unless n==undefined.length
  else
    raise Error, 'nothing was undefined' if undefined.empty?
  end
end

def undefined_in_pattern
  @title = @title.split(':',2).first if @title
  undefined = @context.symbols.undefined(self)
  @title = "#{@title}: #{undefined.join(' ')}" unless undefined.empty?
end

# Statement type processing

def pattern_type(nl)
  set_regexp
  newlines_count(nl)
  undefined_in_pattern
  follows = @context.heap.to_a[0..nl].reverse
  if @regexp.match? follows.map{_1.to_s}.join("\n")
    set_statement(support(*follows))
  else
    set_statement
  end
end

def tautology
  expected_instantiations(n:0)
  axiom = detect_statement('A')
  set_statement(support(axiom), axiom.title)
end

def set
  let = detect_statement('L')
  expected_instantiations(let.title)
  set_statement(support(let), let.title)
end

def result
  expected_instantiations(n:0)
  mapping,s1 = heap_search('M')
  set_statement(support(mapping,s1), mapping.title)
end

def instantiation
  existential,s1 = heap_search('E')
  expected_instantiations(existential.title)
  set_statement(support(existential,s1), existential.title)
end

def conclusion
  expected_instantiations(n:0)
  inference,s1,s2 = heap_combos_search('I')
  set_statement(support(inference,s1,s2), inference.title)
end

def definition
  expected_instantiations(@title)
  set_statement
end

def postulate
  expected_instantiations(n:0)
  set_statement
type(= @code[0]) click to toggle source
# File lib/korekto/statement.rb, line 14
def type              = @code[0]
def to_s              = @statement
def to_str            = @statement
def match?(statement) = @regexp.match?(statement)
def scan(regex, &blk) = @statement.scan(regex, &blk)
def pattern?          = !@regexp.nil?
def literal_regexp?   = @statement[0]=='/' && @statement[-1]=='/'

private

def syntax_check
  @context.syntax.each do |rule|
    raise Error, "syntax: #{rule}" unless @statement.instance_eval(rule)
  rescue # other than Korekto::Error < Exception
    raise Error, "#{$!.class}: #{rule}"
  end
end

def set_acceptance_code
  case @code[0] # type
  when 'P'
    postulate
  when 'D'
    definition
  when 'C'
    conclusion
  when 'X'
    instantiation
  when 'R'
    result
  when 'S'
    set
  when 'T'
    tautology
  when 'A', 'L'
    # Axiom=>Tautoloty, Let=>Set,
    pattern_type(0)
  when 'M', 'E'
    # Map=>Result, Existential=>Instantiation(X)
    pattern_type(1)
  when 'I'
    # Inference=>Conclusion
    pattern_type(2)
  when 'W'
    ['T','S','R','X','C'].any? do |code|
      begin
        @code[0]=code
        set_acceptance_code
        true
      rescue Error
        false
      end
    end or raise Error, 'did not match any statement pattern'
  else
    raise Error, "statement type #{@code[0]} not implemented"
  end
end

# Common helper

def set_statement(support=nil, title=nil)
  @code = "#{@code[0]}#{@statement_number}"
  @code += '.' + @section unless @section=='-'
  @code += "/#{support}" if support
  @title = title if (title=title&.split(':',2)&.first) and not title.empty?
end

def support(*s)
  support = []
  s.each do |s|
    c = s.code.split('/',2)[0]
    support.push(c)
  end
  return support.join(',')
end

# Pattern helpers

def newlines_count(n)
  raise Error, "expected #{n} newlines" unless n==@regexp.inspect.gsub('\\\\','').scan('\\n').length
end

def set_regexp
  @regexp = @context.symbols.s2r(@statement)
end

# Searches

def detect_statement(type)
  statement = @context.type(type).detect do |statement|
    statement.match? @statement
  end
  raise Error, "does not match any '#{type}' statement" unless statement
  return statement
end

def heap_combos_search(type)
  @context.heap.combos do |s1, s2|
    compound = [s1,s2,@statement].join("\n")
    @context.type(type).each do |inference|
      return inference,s1,s2 if inference.match?(compound)
    end
  end
  raise Error, "does not match any '#{type}' statement"
end

def heap_search(type)
  @context.heap.each do |s1|
    compound = [s1,@statement].join("\n")
    @context.type(type).each do |s0|
      return s0,s1 if s0.match?(compound)
    end
  end
  raise Error, "does not match any '#{type}' statement"
end

# Defined/Undefined

def expected_instantiations(title=nil, n:nil)
  undefined = @context.symbols.undefined(self)
  if n ||= title&.match(/[1-9]\d*/)&.to_s&.to_i
    raise Error, "expected #{n} undefined: #{undefined.join(' ')}" unless n==undefined.length
  else
    raise Error, 'nothing was undefined' if undefined.empty?
  end
end

def undefined_in_pattern
  @title = @title.split(':',2).first if @title
  undefined = @context.symbols.undefined(self)
  @title = "#{@title}: #{undefined.join(' ')}" unless undefined.empty?
end

# Statement type processing

def pattern_type(nl)
  set_regexp
  newlines_count(nl)
  undefined_in_pattern
  follows = @context.heap.to_a[0..nl].reverse
  if @regexp.match? follows.map{_1.to_s}.join("\n")
    set_statement(support(*follows))
  else
    set_statement
  end
end

def tautology
  expected_instantiations(n:0)
  axiom = detect_statement('A')
  set_statement(support(axiom), axiom.title)
end

def set
  let = detect_statement('L')
  expected_instantiations(let.title)
  set_statement(support(let), let.title)
end

def result
  expected_instantiations(n:0)
  mapping,s1 = heap_search('M')
  set_statement(support(mapping,s1), mapping.title)
end

def instantiation
  existential,s1 = heap_search('E')
  expected_instantiations(existential.title)
  set_statement(support(existential,s1), existential.title)
end

def conclusion
  expected_instantiations(n:0)
  inference,s1,s2 = heap_combos_search('I')
  set_statement(support(inference,s1,s2), inference.title)
end

def definition
  expected_instantiations(@title)
  set_statement
end

def postulate
  expected_instantiations(n:0)
undefined_in_pattern() click to toggle source
# File lib/korekto/statement.rb, line 141
def undefined_in_pattern
  @title = @title.split(':',2).first if @title
  undefined = @context.symbols.undefined(self)
  @title = "#{@title}: #{undefined.join(' ')}" unless undefined.empty?
end