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
heap_combos_search(type)
click to toggle source
# File lib/korekto/statement.rb, line 110 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
heap_search(type)
click to toggle source
# File lib/korekto/statement.rb, line 120 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
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