namespace FicroKanSharp.Test

open FicroKanSharp
open Xunit
open FsUnitTyped

module TestThing =

    [<Fact>]
    let ``Example from the docs`` () : unit =
        let aAndB =
            Goal.conj
                (Goal.callFresh (fun x -> Goal.equiv (Term.Variable x) (Term.Literal 7)))
                (Goal.callFresh (fun x -> Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 5)) (Goal.equiv (Term.Variable x) (Term.Literal 6))))

        let u = Goal.evaluate aAndB State.empty
        match u |> Stream.peel with
        | None -> failwith "oh no"
        | Some (s, rest) ->

        s
        |> Map.toList
        |> shouldEqual
            [
                Variable.VariableCount 0, Term.Literal 7
                Variable.VariableCount 1, Term.Literal 5
            ]

        match rest |> Stream.peel with
        | None -> failwith "oh no"
        | Some (s, rest) ->

        s
        |> Map.toList
        |> shouldEqual
            [
                Variable.VariableCount 0, Term.Literal 7
                Variable.VariableCount 1, Term.Literal 6
            ]

        match rest |> Stream.peel with
        | None -> ()
        | Some s -> failwith $"{s}"

    [<Fact>]
    let ``Another example`` () =
        let aAndB =
            (Goal.callFresh (fun x -> Goal.equiv (Term.Variable x) (Term.Literal 5)))

        let u = Goal.evaluate aAndB State.empty
        match u |> Stream.peel with
        | None -> failwith "oh no"
        | Some (s, rest) ->

        s
        |> Map.toList
        |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]

        match Stream.peel rest with
        | None -> ()
        | Some s -> failwithf $"{s}"

    [<Fact>]
    let ``Recursive example`` () =
        let rec fives (x : Variable) =
            (Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 5)) (Goal.delay (fun () -> fives x)))

        let u = Goal.evaluate (Goal.callFresh fives) State.empty
        match u |> Stream.peel with
        | None -> failwith "oh no"
        | Some (s, rest) ->

        s
        |> Map.toList
        |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]

        match Stream.peel rest with
        | None -> failwith "oh no"
        | Some (s, rest) ->

        s
        |> Map.toList
        |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]

        match Stream.peel rest with
        | None -> failwith "oh no"
        | Some (s, _rest) ->

        s
        |> Map.toList
        |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]

    [<Fact>]
    let ``Another recursive example`` () =
        let rec fives (x : Variable) =
            (Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 5)) (Goal.delay (fun () -> fives x)))
        let rec sixes (x : Variable) =
            (Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 6)) (Goal.delay (fun () -> sixes x)))
        let fivesAndSixes =
            Goal.callFresh (fun x -> Goal.disj (fives x) (sixes x))

        let u = Goal.evaluate fivesAndSixes State.empty
        match u |> Stream.peel with
        | None -> failwith "oh no"
        | Some (s, rest) ->

        s
        |> Map.toList
        |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]

        match Stream.peel rest with
        | None -> failwith "oh no"
        | Some (s, rest) ->

        s
        |> Map.toList
        |> shouldEqual [Variable.VariableCount 0, Term.Literal 6]

        match Stream.peel rest with
        | None -> failwith "oh no"
        | Some (s, rest) ->

        s
        |> Map.toList
        |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]

        match Stream.peel rest with
        | None -> failwith "oh no"
        | Some (s, _rest) ->

        s
        |> Map.toList
        |> shouldEqual [Variable.VariableCount 0, Term.Literal 6]