FOL parser

#I "packages/FParsec.1.0.1/lib/net40-client/"

#r "FParsecCS.dll"
#r "FParsec.dll"

open FParsec

let test p str =
    match run p str with
    | Success(result, _, _)   -> printfn "Success: %A" result
    | Failure(errorMsg, _, _) -> printfn "Failure: %s" errorMsg

//Types
type Term = | Function of string * Term list
            | Constant of string
            | Variable of string

type Predicate = | Predicate of string * Term list
                 | Equality of Term * Term

type Expr = | Atom of Predicate
            | Not of Expr
            | And of Expr * Expr
            | Or of Expr * Expr
            | Impl of Expr * Expr
            | Bicond of Expr * Expr
            | ForAll of string list * Expr
            | Exists of string list * Expr

//Parsing
let ws = spaces
let str_ws s = pstring s .>> ws

type IdentifierType = Var | NotVar

let identifier t =
    let fl, err = match t with
                  | Var -> isLower, "variable"
                  | NotVar -> isUpper, "non-variable identifier"
    let isChar c = isLetter c || isDigit c || c = '_'
    many1Satisfy2L fl isChar err .>> ws


let term, pRefTerm = createParserForwardedToRef()

let func =
    //NOTE: Second part fails immediately if there is no opening bracket,
    //so backtracking occurs
    identifier NotVar .>>.? (between (str_ws "(") (str_ws ")") (sepBy1 term (str_ws ",")))
        |>> Function

do pRefTerm := choice [
        func;
        identifier NotVar |>> Constant;
        identifier Var |>> Variable;
    ]

let termEquality =
    term .>>? str_ws "=" .>>. term |>> Equality

let predicate =
    choice [
        termEquality;
        identifier NotVar .>>.? (between (str_ws "(") (str_ws ")") (sepBy1 term (str_ws ","))) |>> Predicate
        identifier NotVar |>> (fun n -> Predicate (n,[]))
    ]

let opp = new OperatorPrecedenceParser<Expr,unit,unit>()
let expr = opp.ExpressionParser

let quantifiedExpr isForAll =
    let l,ctor = match isForAll with
                 | true -> "A", ForAll
                 | false -> "E", Exists
    str_ws ("[" + l + "]") >>. sepBy1 (identifier Var) (str_ws ",") .>>. expr |>> ctor

opp.TermParser <- choice [
    quantifiedExpr true
    quantifiedExpr false
    predicate |>> Atom
    between (str_ws "(") (str_ws ")") expr
]
opp.AddOperator(PrefixOperator("!", ws, 5, true, fun x -> Not x))
opp.AddOperator(InfixOperator("&", ws, 4, Associativity.Left, fun x y -> And (x,y)))
opp.AddOperator(InfixOperator("|", ws, 3, Associativity.Left, fun x y -> Or (x,y)))
opp.AddOperator(InfixOperator("=>", ws, 2, Associativity.Left, fun x y -> Impl (x,y)))
opp.AddOperator(InfixOperator("<=>", ws, 1, Associativity.Left, fun x y -> Bicond (x,y)))

test expr "[A] x !Pred1 & (([E] y Func1(x,y) = Func2(C1)) | Pred2)"