Unifikacja (informatyka) — część 2

type utree = Var of string | Const of string | Unary of string * utree | Binary of string * utree * utree

let rec find_var sv = function Var v -> if v = sv then true else false | Const c -> false | Unary (op,a) -> find_var sv a | Binary (op,a,b) -> (find_var sv a) or (find_var sv b)

exception NotUnificable

let ureplace sv rt t = let rec ureplace_aux = function Var v -> if sv = v then rt else Var v | Const c -> Const c | Unary (op,a) -> Unary (op,ureplace_aux a) | Binary (op,a,b) -> Binary (op,ureplace_aux a,ureplace_aux b) in List.map (function (a,b) -> ureplace_aux a, ureplace_aux b) t

let rec unify = function [] -> [] | (Var v, rt)::t -> (v,rt)::unify (ureplace v rt t) | (rt, Var v)::t -> (v,rt)::unify (ureplace v rt t) | (Unary (op1,a1),Unary (op2,a2))::t -> if op1 = op2 then unify ((a1,a2)::t) else raise NotUnificable | (Binary (op1,a1,b1), Binary (op2,a2,b2))::t -> if op1 = op2 then unify ((a1,a2)::(b1,b2)::t) else raise NotUnificable | _ -> raise NotUnificable

unify [Binary ("+", Var "x", Const "2"), Var "y"]

unify [(Binary ("+", Var "x", Const "2"), Binary ("+", Binary ("+", Var "z", Const "7"), Var "y"))]