--
-- This file has been auto-generated by egison-translator.
--

def term {a, b} : Matcher (Term a) :=
  matcher
    | var $ as integer with
      | Var i -> [i]
      | _ -> []
    | compound $ $ as (string, list term) with
      | Compound s l -> [(s, l)]
      | _ -> []
    | unify #$t $ as something with
      | s ->
        match unify t s as maybe something with
          | just $σ -> [σ]
          | nothing -> []
    | subterm $ $ as (term, something) with
      | s -> subterm s
    | $ as something with
      | tgt -> [tgt]

def var {a} (n: Integer) : Term a := Var n

def app {a} : [a] -> Term a :=
  cambda xs ->
    match xs as list something with
      | $x :: $xs -> Compound x xs

def occur := \v => var ~v | compound _ (_ ++ occur ~v :: _)

def fv :=
  \matchAll as (term) with
    | occur $v -> v

def tsubst :=
  \match as (something, term) with
    | ($σ, var $n) ->
      match σ as multiset (integer, term) with
        | cons (#n, $t) _ -> t
        | _ -> Var n
    | ($σ, compound $f $xs) -> Compound f (map 1#(tsubst σ $1) xs)

def unify :=
  \match as unorderedPair term with
    | (var $x, var #x) -> Just []
    | ( var $x
      , AndPat (PatVar "t") (NotPat (PApplyPat (VarExpr "occur") [ValuePat (VarExpr "x")])) ) ->
      Just [(x, t)]
    | (compound $f $xs, compound #f $ys) -> unifyList xs ys
    | _ -> Nothing

def unifyList :=
  \match as (list term, list term) with
    | ([], []) -> Just []
    | (cons $x $xs, cons $y $ys) ->
      match unify x y as maybe something with
        | nothing -> Nothing
        | just $σ1 ->
          match unifyList (map 1#(tsubst σ1 $1) xs) (map 1#(tsubst σ1 $1) ys) as
            maybe something with
            | nothing -> Nothing
            | just $σ2 -> Just JoinExpr (VarExpr "\963\&1") (VarExpr "\963\&2")
    | _ -> Nothing

def x := var 0

def y := var 1

def z := var 2

def w := var 3

def a := app "a"

def b := app "b"

def c := app "c"

def d := app "d"

def f := "f"

def g := "g"

def h := "h"

def showΣ $σ := S.concat ["{", showΣ' σ, "}"]

def showΣ' :=
  \match as list (something, something) with
    | [] -> ""
    | cons ($v, $t) [] -> S.concat ["[", showVar v, ", ", showTerm t, "]"]
    | cons ($v, $t) $σ ->
      S.concat ["[", showVar v, ", ", showTerm t, "], ", showΣ' σ]

def showVar :=
  \match as integer with
    | #0 -> "x"
    | #1 -> "y"
    | #2 -> "z"
    | #3 -> "w"

def showTerm :=
  \match as term with
    | var #0 -> "x"
    | var #1 -> "y"
    | var #2 -> "z"
    | var #3 -> "w"
    | var $x -> S.concat ["x", show x]
    | compound $f #[] -> f
    | compound #"+" ((compound #"+" _ & $x) :: $y :: []) ->
      S.concat ["(", showTerm x, ") + ", showTerm y]
    | compound #"+" ($x :: $y :: []) ->
      S.concat [showTerm x, " + ", showTerm y]
    | compound #"*" ((compound #"*" _ & $x) :: $y :: []) ->
      S.concat ["(", showTerm x, ") * ", showTerm y]
    | compound #"*" ($x :: $y :: []) ->
      S.concat [showTerm x, " * ", showTerm y]
    | compound $f $xs ->
      S.concat [f, "(", S.intercalate ", " (map showTerm xs), ")"]

-- Test: showΣ (head (unify (app "+" a b) x)) should be "{[x, a + b]}"
-- Test: showΣ (head (unify x (app "+" y z))) should be "{[x, y + z]}"
-- Test: showΣ (head (unify (app f x (app g y z) (app h x)) (app f a w y))) should be "{[x, a], [w, g(y, z)], [y, h(a)]}"

showΣ (head (unify (app "+" a b) x))

showΣ (head (unify x (app "+" y z)))

showΣ (head (unify (app f x (app g y z) (app h x)) (app f a w y)))