type PrologTerm =
    | Atom of string
    | Variable of string
    | Structure of string*PrologTerm list

let a = Structure("pidory", [Atom("emil");
                                        Atom("jeka")])

let b = Structure("pidory", [Variable("E");
                                        Variable("J")])
let unify term1 term2 =
    let rec unify' term1 term2 state acc =
        match term1 with
        | _ when state = false -> (false, [])
        | Atom(x) -> match term2 with
                                    | Atom(y) -> (x=y, acc)
                                    | Variable(y) -> (true, [(y,x)]@acc)
                                    | _ -> (false, [])

        | Variable(x) -> match term2 with
                                    | Atom(y) -> (true, [(x,y)]@acc)
                                    | Variable(y) -> (true, [(x,y)]@acc)
                                    | Structure(n, l) -> (true, [(x,string(Structure(n, l)))]@acc)

        | Structure(nx, x) -> match term2 with
                                    | Variable(y) -> (true, [(y,string(Structure(nx, x)))]@acc)
                                    | Structure(ny, y) -> if x.Length <> y.Length then (false, []) else (Seq.zip x y)
                                                                                                                    |> Seq.map(fun s -> unify' (fst s) (snd s) state [])
                                                                                                                    |> Seq.reduce(fun (s1, s2) (acc1, acc2) -> (s1&&acc1, s2@acc2))
                                                                                                                    |> fun (s1, s2) -> (s1, s2@acc)
                                    | _ -> (false,[])
    let res = unify' term1 term2 true []
    if (fst res) = false then res
    else  res |> Seq.distinct |>


let rec filter (source : (string*string) list) acc =
    let pairs = source |> Seq.filter(fun (s1, s2) -> ['_']@['A'..'Z'] |> Seq.exists (fun x-> x=s2.[0]))
    if (pairs |> Seq.length) <=0
       then acc@source
    else
       let xpair = pairs |> Seq.head
       filter (source |> Seq.map (fun (s1, s2) -> if s2 = (snd xpair) then (s1, fst xpair) else if s1 = (snd xpair) then (fst xpair, s2) else (s1, s2)) |> Seq.distinct |> Seq.filter (fun (s1, s2) ->  ((s1 <> s2) || (s1 <> (fst xpair)))) |> Seq.toList) [xpair]@acc

let c = [("A","1");("B","a");("B","A");("C","A");("D","C");("E","a");("F","E");("F","1")]


filter c []

unify (Variable("X")) (Atom("x"))

unify a b

['_']@['A'..'Z'] |> List.exists (fun x-> x='1')