import Data.List
import Control.Monad


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

failure :: Check a
failure = Nothing

is_result :: Check a -> Bool
is_result Nothing = False
is_result _ = True

assert :: Bool -> Check ()
assert p = if p then return () else failure

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

-- Exercise 1.1 - Matching Algorithm

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

-- Exercise 1.2

type Equations = [(Term,Term)]

  
example_prog :: Equations
example_prog = [
      (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" []]
example_term :: Term
example_term = Fun "append" [Fun "Cons" [Fun "add" [one, one], Fun "Nil" []], 
  Fun "Cons" [one, Fun "Nil" []]]
  
-- invoking one_step on a normal form should deliver Nothing
-- you can choose the evaluation strategy in one_step
one_step :: Equations -> Term -> Check Term 
one_step = undefined
        
-- many step evaluation    
evaluate :: Equations -> Term -> Term
evaluate pi t = case one_step pi t of
  Just s -> evaluate pi s
  Nothing -> t

test = evaluate example_prog example_term