//Inspired on "How to specify it!" by John Hughes (& Java adaptation by Johannes Link)
//https://johanneslink.net/how-to-specify-it/

#r "nuget: fscheck"
open FsCheck

module BST =
    type BinarySearchTree<'v> =
        | Empty
        | Node of
            {| left: BinarySearchTree<'v>
               value: 'v
               right: BinarySearchTree<'v> |}

    let empty = Empty

    let rec add v t =
        match t with
        | Empty ->
            Node
                {| value = v
                   left = Empty
                   right = Empty |}
        | Node node when v <= node.value ->
            Node
                {| node with
                    left = node.left |> add v |}
        | Node node ->
            Node
                {| node with
                    right = node.right |> add v |}

    let rec toList t =
        match t with
        | Empty -> []
        | Node n ->
            List.concat [ n.left |> toList
                          [ n.value ]
                          n.right |> toList ]

    let rec ofList l =
        match l with
        | [] -> Empty
        | h :: t -> (ofList t) |> add h

    let rec contains v t =
        match t with
        | Empty -> false
        | Node n ->
            n.value = v
            || n.left |> contains v
            || n.right |> contains v

    let union t1 t2 =
        t1
        |> toList
        |> List.fold (fun s x -> s |> add x) t2

//Interesting part about BST: it's possible to represent illegal states
//as the sorted invariant is not encoded into its type
//That's why we need a custom arbitrary
type IntTree = BST.BinarySearchTree<int>
type EquivalentTrees = IntTree * IntTree

type Arbitraries =
    static member BST<'v when 'v: comparison>() =
        Arb.from<'v list>
        |> Arb.convert BST.ofList BST.toList

    static member EquivalentTrees() =
        Arb.from<int list>
        |> Arb.toGen
        |> Gen.map (fun xs -> BST.ofList xs, BST.ofList (List.sort xs))
        |> Arb.fromGen

Arb.register<Arbitraries> ()

let rec validTree (t: IntTree) =
    match t with
    | BST.BinarySearchTree.Empty -> true
    | BST.BinarySearchTree.Node n when n.left |> validTree && n.right |> validTree ->
        let ls = n.left |> BST.toList
        let rs = n.right |> BST.toList

        ls |> List.forall (fun l -> l <= n.value)
        && rs |> List.forall (fun r -> r > n.value)
    | _ -> false

let equivalent t1 t2 = t1 |> BST.toList = (t2 |> BST.toList)

//Invariant: any BST is sorted
Check.Quick("invariant. If I fail the arbitrary generates invalid trees!", (fun t -> t |> validTree))
//Checking arbitraries: EquivalentTrees are always equivalent
Check.Quick("verifying equivalence", (fun ((t1, t2): EquivalentTrees) -> equivalent t1 t2))

//Validity testing
Check.Quick("empty-valid", (fun () -> BST.BinarySearchTree.Empty |> validTree))
Check.Quick("add-valid", (fun (t: IntTree) x -> t |> BST.add x |> validTree))
Check.Quick("union-valid", (fun (t1: IntTree) (t2: IntTree) -> BST.union t1 t2 |> validTree))

//Postconditions for add
Check.Quick("add-always contains x", (fun (t: IntTree) x -> t |> BST.add x |> BST.contains x))

Check.Quick(
    "add-always grows tree by 1",
    (fun (t: IntTree) x ->
        let l = t |> BST.toList |> List.length
        let added = t |> BST.add x
        let al = added |> BST.toList |> List.length
        al = l + 1)
)

Check.Quick(
    "add-always contains original values",
    fun (t: IntTree) x ->
        let origs = t |> BST.toList
        let added = t |> BST.add x

        origs
        |> List.forall (fun o -> added |> BST.contains o)
)

//Metamorphic properties: related calls return related results
Check.Quick("add-add", (fun (t: IntTree) a b -> equivalent (BST.add a (BST.add b t)) (BST.add b (BST.add a t))))

Check.Quick(
    "add-union",
    (fun (t1: IntTree) (t2: IntTree) x -> equivalent (BST.add x (BST.union t1 t2)) (BST.union (BST.add x t1) t2))
)

Check.Quick("union-commutative", (fun (t1: IntTree) (t2: IntTree) -> equivalent (BST.union t1 t2) (BST.union t2 t1)))

//Equivalence
Check.Quick(
    "add-preserves equivalence",
    fun ((t1, t2): EquivalentTrees) x -> equivalent (BST.add x t1) (BST.add x t2)
)

Check.Quick(
    "union-preserves equivalence",
    fun (t: IntTree) ((t1, t2): EquivalentTrees) -> equivalent (BST.union t1 t) (BST.union t2 t)
)

//Induction
Check.Quick("union-zero", (fun (t1: IntTree) -> equivalent t1 (BST.union t1 BST.BinarySearchTree.Empty)))

Check.Quick(
    "any list can be created by its insertions",
    (fun (t: IntTree) -> equivalent t (t |> BST.toList |> BST.ofList))
)

//Model-based
Check.Quick(
    "add-model",
    (fun (t: IntTree) x ->
        let xs = t |> BST.toList
        let addedList = (x :: xs) |> List.sort
        let addedTree = t |> BST.add x
        (addedTree |> BST.toList) = addedList)
)

Check.Quick(
    "union-model",
    (fun (t1: IntTree) (t2: IntTree) ->
        let listUnion =
            (t1 |> BST.toList) @ (t2 |> BST.toList)
            |> List.sort

        let treeUnion = BST.union t1 t2
        (treeUnion |> BST.toList) = listUnion)
)