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]

typeCheck :: Sig -> Vars -> Term -> Maybe Type
typeCheck sig vars (Var x) = vars x
typeCheck sig vars (Fun f ts) = do
  (tysIn,tyOut) <- sig f
  tysTs <- mapM (typeCheck sig vars) ts
  if tysTs == tysIn then return tyOut else Nothing


-- exercise 3.1

sigmaExample :: Sig
sigmaExample f = undefined

-- exercise 3.2

varsExample :: Vars
varsExample = undefined 
  
  
-- exercise 3.3

t_1, t_2, t_3 :: Term
t_1 = undefined
t_2 = undefined
t_3 = undefined

testTerms = map (typeCheck sigmaExample varsExample) [t_1, t_2, t_3]

-- exercise 3.4

type PSym = String
type PSymInfo = [Type]
type P = PSym -> Maybe PSymInfo

data Formula = 
  TrueF 
  | Negate Formula
  | Conj Formula Formula
  | Forall Var Formula
  | Predicate PSym [Term]


typeCheckFormula :: Sig -> Vars -> P -> Formula -> Maybe ()
typeCheckFormula sig vars p_set TrueF = return ()
typeCheckFormula sig vars p_set _ = undefined 


pExample :: P
pExample "=" = return ["List","List"]
pExample _ = Nothing

phiAssoc :: Formula
phiAssoc = Forall "xs" (Forall "ys" (Forall "zs" (
   Predicate "=" [
     Fun "app" [Var "xs", Fun "app" [Var "ys", Var "zs"]],
     Fun "app" [Fun "app" [Var "xs", Var "ys"], Var "zs"]
     ]
  )))

psiAssoc :: Formula
psiAssoc = Forall "x" (Forall "y" (Forall "z" (
   Predicate "=" [
     Fun "app" [Var "x", Fun "app" [Var "y", Var "z"]],
     Fun "app" [Fun "app" [Var "x", Var "y"], Var "z"]
     ]
  )))

testFormulaPhi = typeCheckFormula sigmaExample varsExample pExample phiAssoc
testFormulaPsi = typeCheckFormula sigmaExample varsExample pExample psiAssoc