type Type = String
type Var  = String
type FSym = String
type FSymInfo = ([Type], Type)
type Vars = Var -> Maybe Type
type Sig = FSym -> Maybe FSymInfo
data Term = 
  Var Var 
  | Fun FSym [Term]
  deriving (Eq, Show)

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

-- Exercise 3.1 - Matching Algorithm

match :: Term -> Term -> Maybe Subst
match l t = do 
  xtList <- matchList [(l,t)] -- call main algorithm
  return (\ x -> case lookup x xtList of  -- convert list to substitution
     Just s -> s
     Nothing -> Var x)
  
matchList :: [(Term,Term)] -> Maybe SubstList
matchList = error "TODO"
  

-- Exercise 3.2 - Evaluation

type Equations = [(Term,Term)]

  
exampleProg :: Equations
exampleProg = [
      (Fun "add" [Fun "Succ" [Var "x"], Var "y"], 
       Fun "Succ" [Fun "add" [Var "x", Var "y"]]),
      (Fun "add" [Fun "Zero" [], Var "y"], 
       Var "y"),
      (Fun "append" [Fun "Cons" [Var "x",Var "xs"], Var "ys"], 
       Fun "Cons" [Var "x", Fun "append" [Var "xs", Var "ys"]]),
      (Fun "append" [Fun "Nil" [], Var "ys"], 
       Var "ys")
      ]
  
one = Fun "Succ" [Fun "Zero" []]
exampleTerm :: Term
exampleTerm = Fun "append" [Fun "Cons" [Fun "add" [one, one], Fun "Nil" []], 
  Fun "Cons" [one, Fun "Nil" []]]
  
-- invoking oneStep on a normal form should deliver Nothing
-- you can choose the evaluation strategy in oneStep
oneStep :: Equations -> Term -> Maybe Term 
oneStep = undefined
        
-- many step evaluation    
evaluate :: Equations -> Term -> Term
evaluate pi t = case oneStep pi t of
  Just s -> evaluate pi s
  Nothing -> t

test = evaluate exampleProg exampleTerm