class Satre::FormulaParser
Public Class Methods
parse(inp)
click to toggle source
# File lib/satre/parser/formula_parser.rb, line 61 def parse(inp) make_parser(method(:parse_formula).curry.call(method(:parse_infix_atom), TermParser.method(:parse_atom), []), inp) end
parse_atomic_formula(ifn, afn, vs, inp)
click to toggle source
ifn: restricted parser for infix atoms afn: more general parser for arbitary atoms
# File lib/satre/parser/formula_parser.rb, line 29 def parse_atomic_formula(ifn, afn, vs, inp) fail(ArgumentError, 'Expected an formula at end of input') if inp == [] head = inp.first rest = inp[1..-1] case head when "false" then return False.new, rest when "true" then return True.new, rest when "(" begin ifn.call(vs, inp) rescue parse_bracketed(method(:parse_formula).curry.call(ifn, afn, vs), ")", rest) end when "~" ast, rest = parse_atomic_formula(ifn, afn, vs, rest) papply(->(p) { Not.new(p) }, ast, rest) when "forall" then parse_quant(ifn, afn, vs.push(rest[0]), ->(x,p) { Forall.new(x,p) }, rest[0], rest[1..-1]) when "exists" then parse_quant(ifn, afn, vs.push(rest[0]), ->(x,p) { Exists.new(x,p) }, rest[0], rest[1..-1]) else afn.call(vs, inp) end end
parse_formula(ifn, afn, vs, inp)
click to toggle source
# File lib/satre/parser/formula_parser.rb, line 7 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_infix_atom(vs, inp)
click to toggle source
# File lib/satre/parser/formula_parser.rb, line 52 def parse_infix_atom(vs, inp) tm, rest = TermParser.parse_term(vs, inp) if rest != [] && ["=", '<', '<=', '>', ">="].include?(rest.first) ast, ost = TermParser.parse_term(vs, rest[1..-1]) papply( ->(tm_) {Atom.new(Relation.new(rest[0], [tm, tm_])) }, ast, ost ) else fail ParserError, 'calculated' # Excepion erfinden end end
parse_quant(ifn, afn, vs, qcon, x, inp)
click to toggle source
absorbs the list of variables allowing the convention of repeated quantifiers
# File lib/satre/parser/formula_parser.rb, line 19 def parse_quant(ifn, afn, vs, qcon, x, inp) fail(ArgumentError, 'Body of quantified term expected') if inp == [] head = inp.first rest = inp[1..-1] ast, rest = if head == '.' then parse_formula(ifn, afn, vs, rest) else parse_quant(ifn, afn, vs.push(head), qcon, head, rest) end papply( ->(fm) { qcon.call(x,fm) }, ast, rest ) end