type Type = String
type Var  = String
type FSym = String
data Term = 
  Var Var 
  | Fun FSym [Term]
  deriving (Eq, Show)

type Subst = Var -> Term
type Subst_List = [(Var,Term)]

-- Exercise 1.1 - Matching Algorithm

match :: Term -> Term -> Maybe Subst
match l t = do 
  var_term_list <- match_list [(l,t)]
  undefined
  
-- you are also allowed to modify the existing implementation
-- if you're not happy with the proposed structure
match_list :: [(Term,Term)] -> Maybe Subst_List
match_list [] = return []
match_list ((Fun _ _, Var _) : _) = Nothing      -- fun-var
match_list _ = undefined
  

-- Exercise 1.2 - evaluate one-step, if possible

-- equations are represented as list of pairs (lhs, rhs)
type Equations = [(Term,Term)]
  
-- performing one step
one_step :: Equations -> Term -> Maybe Term
one_step eqs (Var x) = Nothing
one_step eqs t@(Fun f ts) = let arg_steps = map (one_step eqs) ts in
  undefined 
        
-- evaluate as long as possible
evaluate :: Equations -> Term -> Term
evaluate eqs t = case one_step eqs t of
  Just s -> evaluate eqs s
  Nothing -> t



-- Tests

lhs1, lhs2 :: Term
lhs1 = Fun "append" [Fun "Cons" [Var "x",Var "xs"], Var "ys"]
lhs2 = Fun "append" [Fun "Nil" [], Var "ys"]

example_eqs :: Equations
example_eqs = 
  [(Fun "add" [Fun "Succ" [Var "x"], Var "y"], Fun "Succ" [Fun "add" [Var "x", Var "y"]]),
   (Fun "add" [Fun "Zero" [], Var "y"], Var "y"),
   (lhs1, Fun "Cons" [Var "x", Fun "append" [Var "xs", Var "ys"]]),
   (lhs2, Var "ys")]
  
example_term :: Term
example_term = Fun "append" [Fun "Cons" [Fun "add" [one, one], Fun "Nil" []], 
  Fun "Cons" [one, Fun "Nil" []]]
  where one = Fun "Succ" [Fun "Zero" []]


is_Just (Just _) = True
is_Just _ = False

test_matching = let t = example_term
  in ("t: ", t, 
      "lhs1: ", lhs1,
      "lhs1 matches t: ", is_Just $ match lhs1 t, 
      "lhs2: ", lhs2,
      "lhs2 matches t: ", is_Just $ match lhs2 t)  

test_evaluation = let 
  t = example_term 
  eqs = example_eqs
  in ("t: ", t, "after one step: ", one_step eqs t, "fully evaluated: ", evaluate eqs t)