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

type_check :: Sig -> Vars -> Term -> Maybe Type
type_check sig vars (Var x) = vars x
type_check sig vars (Fun f ts) = do
  (tys_in,ty_out) <- sig f
  tys_ts <- mapM (type_check sig vars) ts
  if tys_ts == tys_in then Just ty_out else Nothing


-- exercise 3.1

sigma_example :: Sig
sigma_example f = undefined

-- exercise 3.2

vars_example :: Vars
vars_example = undefined 
  
  
-- exercise 3.3

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

test_terms = map (type_check sigma_example vars_example) [t_1, t_2, t_3]

-- exercise 3.4

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

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


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

-- exercise 3.5

phi_assoc :: Formula
phi_assoc = undefined 

test_formula :: Maybe ()  
test_formula = type_check_formula undefined undefined undefined undefined