module Term

type Term =
// Constants
| False
| True

// Variables
| Var of int

// Quantifiers
| All of Term * Term

// Predicates
| Eqv of Term * Term
| Not of Term
| Or of Term list

// Comparison
| Equal of Term * Term

type ShapeInfo = Shape of Term

let (|Leaf|Node|) a =
    match a with
    | False
    | True ->
        Leaf(Shape a)
    | Var n ->
        Leaf(Shape a)
    | Not x ->
        Node(Shape a, [x])
    | All(x, y)
    | Equal(x, y)
    | Eqv(x, y) ->
        Node(Shape a, [x; y])
    | Or xs ->
        Node(Shape a, xs)

let FromLeaf(Shape a) =
    a

let FromNode(Shape a, xs) =
    match a, xs with
    | All(_, _), [x; y] ->
        All(x, y)

    | Eqv(_, _), [x; y] ->
        Eqv(x, y)
    | Not _, [x] ->
        Not x
    | Or _, xs ->
        Or xs

    | Equal(_, _), [x; y] ->
        Equal(x, y)

    | _ ->
        failwith "Internal error"

let rec eval model a =
    match a with
    | Equal(x, y) when x = y ->
        True
    | Not False ->
        True
    | Not True ->
        False
    | Or xs ->
        let xs' = List.map(eval model) xs
            |> List.filter(fun x -> x <> False)
        if List.exists(fun x -> x = True) xs' then
            True
        else
            match xs' with
            | [] ->
                False
            | [x] ->
                x
            | _ ->
                Or xs'

    | Node(s, xs) ->
        FromNode(s, List.map(eval model) xs)
    | Leaf _ ->
        a