simple implementation of prolog in f#

prolog.fs

let rec findSentence (matcher:'e->'a-> 'a-> bool * 'e) (matcherEnv:'e) (sentences:'a list list) (target:'a) =
    printfn "searching target %A in %A" target sentences
    match sentences with
        | [] -> None
        | (name::subTargets)::sentences -> 
            let matched, resMatcherEnv = matcher matcherEnv name target
            if matched then Some(subTargets,sentences, resMatcherEnv)
            else findSentence matcher matcherEnv sentences target
        | _::t -> findSentence matcher matcherEnv t target



let rec search matcher (matcherEnv:'e) (targets: 'a list) (sentences:'a list list) (solutions: ('a * 'a list list * 'e ) list) =
    let currentSolution = (solutions |>List.map (fun (x,_,_)->x), matcherEnv)
    currentSolution |> printfn "search targets %A solutions %A" targets
    match targets with
    | [] -> true,currentSolution //all targets resolve success
    | target::targets -> //resolving next target
        
        let solution = findSentence matcher matcherEnv sentences target
        match solution with
        | Some(newTargets,solSentences, solMatcherEnv) -> //found solution for target
            printfn "found solution for target %A" target
            let targets = newTargets @ targets // adding new targets from new solution
            let solutions = (target,solSentences, matcherEnv)::solutions // storing target as solved and not checked sentences for this target
            search matcher solMatcherEnv targets sentences solutions // continue search
        | None -> // not found solution for target
            printfn "not found solution for target %A" target
            match solutions with 
                | [] -> false,currentSolution // no previously resolved solutions, fail
                | ((target,rollbackSentences, rollbackMatcherEnv) :: solutions) -> 
                    let solution = findSentence matcher rollbackMatcherEnv rollbackSentences target//continue search for target in not checked sentences
                    match solution with
                    | Some(newTargets,solSentences, solMatcherEnv) -> 
                        let targets = newTargets @ targets // adding new targets from new solution
                        let solutions = (target,solSentences, rollbackMatcherEnv)::solutions // storing target as solved and not checked sentences for this target
                        search matcher solMatcherEnv targets sentences solutions// continue search
                    | None -> false,currentSolution//no solution fail



let solve matcher matcherEnv sentences target = search matcher matcherEnv [target] sentences []
let sentences = [
    ["дает молоко"];
    ["имеет волосяной покров"];
    ["имеет рога"];
    ["млекопитающее";"дает молоко";"имеет волосяной покров"];
    ["козел";"борька"];
    ["козел";"млекопитающее";"имеет рога"];
]
let stringMatcher _ a b = (a = b, ())
findSentence stringMatcher () sentences "млекопитающее"
solve stringMatcher () sentences "козел"

//[<StructuredFormatDisplay("{AsString}")>]
type Term = | Var of string 
            | Atom of string 
            | Struct of Term list 
            //member m.AsString = 
            //    match m with    
            //    | Var(s) -> s
            //    | Atom(s) -> s
            //    | Struct(terms) -> List.map (sprintf "%A") terms |> Seq.ofList |> String.concat "," |> sprintf "(%s)"

let rec toString t = 
    match t with    
    | Var(s) -> s
    | Atom(s) -> s
    | Struct(terms) -> List.map toString terms |> Seq.ofList |> String.concat "," |> sprintf "(%s)"

let lookup k = List.tryFind (List.head >> ((=) k))

let rec value x env =
    match x with 
    | Var(_) -> let kv = lookup x env
                match kv with
                | Some([_;v]) when x <> v -> value v env
                | _ -> x
    | _ -> x


let test = value (Var("X")) [[Var("X");Var("W")];[Var("W");Var("U")];[Var("U");Var("V")];[Var("V");Var("Y")]] = Var("Y")
let test2 = value (Var("X")) [[Var("X");Var("Y")];[Var("Z");Atom("a")];[Var("Y");Var("Z")]] = Atom("a")

let rec unify env x y  =
    
    let x = value x env
    let y = value y env
    match x,y with
    | _, _ when x = y -> true, env
    | Var(_), Struct(l) when List.contains x l-> sprintf "cyclic defenition %A = %A" x l |> failwith
    | Struct(l) , Var(_) when List.contains y l-> sprintf "cyclic defenition %A = %A" y l |> failwith
    | Var(_), _ -> true, [x;y]::env
    | _ , Var(_) -> true, [y;x]::env
    | Struct(x::xs),Struct(y::ys) -> 
        let f1, env = unify env x y 
        if f1 
        then let f2, env = unify env (Struct(xs)) (Struct(ys)) 
             f2, env
        else false, env
    | _,_ -> false, env

let test3 = unify [] (Struct([Atom("a");Var("X");Var("X")])) (Struct([Atom("a");Var("Y");Atom("b")])) = (true, [[Var "Y"; Atom "b"]; [Var "X"; Var "Y"]])
let test4 = unify [] (Struct([Atom("a");Var("X");Atom("b")])) (Struct([Atom("a");Struct([Atom("c");Var("Y")]);Var("Y")])) = (true, [[Var "Y"; Atom "b"]; [Var "X"; Struct [Atom "c"; Var "Y"]]]) 
let test5 = unify [] (Struct([Atom("a");Var("X");Var("X");Var("X")])) (Struct([Atom("a");Var("Y");Var("Y");Var("Y")])) = (true, [[Var "X"; Var "Y"]])
//let test6 = unify [] (Struct([Var("X")])) (Struct([Struct([Atom("a");Var("X")])]))= (true, [[Var "X"; Struct [Atom "a"; Var "X"]]]) // fail: cyclic defenition Var "X" = [Atom "a"; Var "X"]

let unifyMatcher env x y = 
    let res, renv = unify env x y
    printfn "unify %A -> %A" (env,x,y) (res,renv)
    res,renv

let sentences2 = [
   [Struct([Atom("grandfather");Var("X"); Var("Z")]);
        Struct([Atom("father");Var("X");Var("Y")]);
        Struct([Atom("father");Var("Y");Var("Z")])
   ]
   [Struct([Atom("father");Var("carl");Atom("sam")])]
   [Struct([Atom("father");Var("sam");Atom("luis")])]
]

solve unifyMatcher [] sentences2 (Struct([Atom("grandfather");Var("X");Atom("luis")]))