class Satre::TermParser
Public Class Methods
is_const_name(string)
click to toggle source
# File lib/satre/parser/term_parser.rb, line 40 def is_const_name(string) string.split('').all? { |c| Lexer.numeric?(c) } || string.nil? end
parse(inp)
click to toggle source
# File lib/satre/parser/term_parser.rb, line 74 def parse(inp) make_parser(method(:parse_term).curry.call([]), inp) end
parse_atom(vs, inp)
click to toggle source
# File lib/satre/parser/term_parser.rb, line 45 def parse_atom(vs, inp) FormulaParser.parse_infix_atom(vs, inp) rescue ParserError head = inp.first rest = inp[1..-1] if rest[0] == '(' rest = rest[1..-1] if rest[0] == ')' return Atom.new(Relation.new(head, [])), rest[1..-1] else ast, rest = parse_bracketed(parse_list(',').call(method(:parse_term).curry.call(vs)),')', rest) papply( ->(args) { Atom.new(Relation.new(head,args))}, ast, rest) end else return Atom.new(Relation.new(head, [])), rest if head != '(' fail(ParserError, 'Parse Atom') end end
parse_atomic_term(vs, inp)
click to toggle source
vs: set of bounds variables in the current scope inp: current input
# File lib/satre/parser/term_parser.rb, line 9 def parse_atomic_term(vs, inp) fail(ArgumentError, 'Term expected') if inp == [] head = inp.first rest = inp[1..-1] if head == '(' then parse_bracketed(method(:parse_term).curry.call(vs), ")", rest) elsif head == '-' then papply( ->(t) { Function.new("-", [t])}, method(:parse_atomic_term).curry.call(vs), rest ) elsif Lexer.alpanumeric?(head) && rest[0] == '(' if rest[1] == ')' papply( -> { Function.new(head, []) }, rest[2..-1]) else ast, rest = parse_bracketed(parse_list(',').call(method(:parse_term).curry.call(vs)) , ')', rest[1..-1]) papply(->(args) { Function.new(head, args) }, ast, rest) end else a = if is_const_name(head) && !vs.include?(head) then Function.new(head,[]) else Variable.new(head) end return a, rest end end
parse_formula(ifn, afn, vs, inp)
click to toggle source
# File lib/satre/parser/term_parser.rb, line 64 def parse_formula(ifn, afn, vs, inp) parse_Entails = parse_right_infix("|=", ->(p,q) { Entails.new(p,q)}) parse_Iff = parse_right_infix("<=>", ->(p,q) { Iff.new(p,q)}) parse_Imp = parse_right_infix("==>", ->(p,q) { Imp.new(p,q)}) parse_Or = parse_right_infix("\\/", ->(p,q) { Or.new(p,q)}) parse_And = parse_right_infix("/\\", ->(p,q) { And.new(p,q)}) parse_Atom = method(:parse_atomic_formula).curry.call(ifn, afn, vs) parse_Entails.call(parse_Imp.call(parse_Or.call(parse_And.call(parse_Iff.call(parse_Atom)))),inp) end
parse_term(vs, inp)
click to toggle source
build up parsing of general terms via parsing of the various infix operations
# File lib/satre/parser/term_parser.rb, line 29 def parse_term(vs, inp) colon = parse_right_infix("::", ->(e1,e2) { Function.new('::', [e1, e2]) }) plus = parse_right_infix("+", ->(e1,e2) { Function.new('+', [e1, e2]) }) minus = parse_left_infix("-", ->(e1,e2) { Function.new('-', [e1, e2]) }) mul = parse_right_infix("*", ->(e1,e2) { Function.new('*', [e1, e2]) }) div = parse_left_infix("/", ->(e1,e2) { Function.new('/', [e1, e2]) }) power = parse_left_infix("^", ->(e1,e2) { Function.new('^', [e1, e2]) }) atom = method(:parse_atomic_term).curry.call(vs) colon.call(plus.call(minus.call(mul.call(div.call(power.call(atom))))), inp) end