Meeting1.fsx

type Var = string
  
type Term = 
  | Number of int
  | Pair of (Term * Term) 
  | Variable of Var 

type Subs = (Var * Term ) list
let emptySubs : Subs = [] 

let eXtsub (x: Var)(y: Term) (s: Subs) : Subs =
 (x, y)::s

let rec walk t s : Term =
  let rec walk t s oldS =
    match t with
    | Variable(x) -> 
        match s with
        | []  -> t
        | (y, v)::s-> if x = y then 
                        walk v oldS oldS 
                      else 
                        walk t s oldS        
    | _ -> t
  walk t s s


let rec unify (u: Term) (v: Term) (s: Subs) : Subs option =  
  let u = walk u s
  let v = walk v s
  match (u, v) with
  | (Variable(x), Variable(y))  when x = y -> Some(s) 
  | (Variable(x), t ) -> Some(eXtsub x t s)
  | (t , Variable(y)) -> Some(eXtsub y t s)
  | (Pair(x1, y1), Pair(x2, y2)) -> 
          match unify x1 x2 s with
          | Some(newS) -> unify y1 y2 newS
          | None -> None
  | (w, r) when w = r -> Some(s)
  | _ -> None


let xx : Var = "X" 
let yy : Var = "Y"
let zz : Var = "Z" 

let sub1 : Subs = [(xx, Number(6)); (yy, Number(4))]
let var1 = Variable(xx)
let var2 = Variable(yy)
let var3 = Variable(zz)

unify var1 var3 sub1

let pair = (Pair(Number(3), Number(4)))
unify pair pair sub1

let sub2 :Subs= [(xx,Pair(Number(3),Number(4)))]
unify var1 (Pair(Number(3), var2)) sub2