PEGJs Logic + Math parser

fol.pegjs

{
  function getTerms(t, ts) {
    if (t) {
      var arr = [];
      for (var i = 0; i < ts.length; ++i) {
        arr.push(ts[i][2]);
      }
      return [t].concat(arr);
    }
    return [];
  }
  function buildName(fst, rest) {
    return fst + rest.join("");
  }
  function getQual(q) {
    return q == "A." || q.toLowerCase() == "forall" || q == "∀"? "forall" : "exists";
  }
}

start = formula

// Patterns to match logic connectives
matchNeg  = "not"i / "!" / "~" / "¬"
matchQual = "A." / "forall"i / "∀" / "exists"i / "E." / "∃"
matchIff  = "iff"i / "<=>" / "⇔"
matchXor  = "xor"i / "⊕" / "⊻"
matchImp  = "implies"i / "=>" / "⇒"
matchOr   = "or"i / "v" / "∨"
matchAnd  = "and"i / "∧"

// Clause
//clause = head:pred ","

// Formula
formula = wformula / uformula

// Weighted formula
wformula =
  fm:negq _ ";" _ weight:[0-9.]+ {
    return { formula: fm, weight: Number(weight.join("")) };
  }

// Unweighted formula
uformula = fm:negq { return { formula: fm }; }

// Logical negation for qualifiers
negq  = matchNeg _ x:negq { return { not: x }; } / qual

// Universal & existential qualifications
qual = q:matchQual _ v:variable vs:("," _ variable)* _ ":"? _ fm:negq {
    return { qualifier: { kind: getQual(q), variables: getTerms(v, vs), formula: fm } };
  } / iff

// Material equivalence
iff  = x:xor _ matchIff _ y:iff { return { binop: { kind: "iff", left: x, right: y } }; } / xor

// Exclusive disjunction
xor = x:imp _ matchXor _ y:xor { return { binop: { kind: "xor", left: x, right: y } }; } / imp

// Logical implication
imp  = x:or _ matchImp _ y:imp { return { binop: { kind: "implies", left: x, right: y } }; } / or

// Disjunction
or = x:and _ matchOr _ y:or  { return { binop: { kind: "or", left: x, right: y } }; } / and

// Conjunction
and  = x:neg _ matchAnd _ y:and { return { binop: { kind: "and", left: x, right: y } }; } / neg

// Logical negation
neg  = matchNeg _ x:neg { return { not: x }; } / atomic

atomic
  = identity
  / pred
  / "⊤" { return { predicate: { name: "true" } }; }
  / "⊥" { return { predicate: { name: "false" } }; }
  / "(" _ expr:negq _ ")" { return expr; }
  / "[" _ expr:negq _ "]" { return expr; }

// Syntactic sugar for the identity predicates:
identity =
  t0:term _ s:("==" / "=" / "!=" / "/=" / "<=" / ">=" / "<" / ">") _ t1:term {
    var f = { predicate: { args: [t0, t1] } };
    switch (s) {
      case "<": f.predicate.name = "lt"; break;
      case "<=": f.predicate.name = "leq"; break;
      case ">": f.predicate.name = "gt"; break;
      case ">=": f.predicate.name = "geq"; break;
      default: f.predicate.name = "eq";
    }
    return s == "!=" || s == "/="? { not: f } : f;
  }

pred = fst:[a-zA-Z] txt:[a-zA-Z0-9]* ts:terms? {
    return { predicate: { name: (fst + txt.join("")), args: (ts? ts : undefined) } };
  }

terms = "(" _ t:term? ts:("," _ term)* _ ")" { return getTerms(t, ts); }

// Sugar for some basic functions:

term   = x:mulfun _ o:("+" / "-") _ y:term { return { kind: "function", name: (o=="+"?"add":"substact"), args: [x, y] }; } / mulfun

mulfun = x:expfun _ o:("*" / "/") _ y:mulfun { return { kind: "function", name: (o=="*"?"multiply":"divide"), args: [x, y] }; } / expfun

expfun = x:minfun _ "^" _ y:expfun { return { kind: "function", name: "power", args: [x, y] }; } / x:minfun

minfun = "-" x:minfun { return { negative: x}; } / tatomic

functerm = fst:[a-zA-Z] txt:[a-zA-Z0-9]* "(" _ t:term? ts:("," _ term)* _ ")" {
    return { kind: "function", name: buildName(fst, txt), args: getTerms(t, ts) };
  }
variable = fst:[a-z] txt:[a-zA-Z0-9]* { return { kind: "variable", name: buildName(fst, txt) }; }
constant = txt:[a-zA-Z0-9]+ { return { kind: "constant", name: txt.join("") }; }

tatomic
  = functerm
  / variable
  / constant // minus
  / "(" _ t:term _ ")" { return t; }
  / "[" _ t:term _ "]" { return t; }

_  = [ \t\r\n]* // optional whitespace

__ = [ \t\r\n]+ // mandatory whitespace