type Check a = Maybe a
type Type = String
type FSym = String
type FSymInfo = ([Type], Type)

-- note that variables are now polymorphic
data Term v = Var v | Fun FSym [Term v]
  deriving (Eq,Show)

assert :: Bool -> Check ()
assert True = return ()
assert False = Nothing

subst :: Eq v => v -> Term v -> v -> Term v
subst x t = (\ y -> if y == x then t else Var y)

varsTerm :: Term v -> [v]
varsTerm (Var x) = [x]
varsTerm (Fun f ts) = concatMap varsTerm ts

type TVar = (Int,Type) -- TVar represents typed variables, which are just numbers
type MatchProblem = [(Term TVar, Term String)] 
-- for t-terms variables are numbers with type annotation, 
-- for l-terms we use strings

type PatternProblem = [MatchProblem]

examplePatternProblem1 :: PatternProblem
examplePatternProblem1 = [
  [(Fun "conj" [Var (1,"Bool"), Var (2,"Bool")], Fun "conj" [Fun "True" [], Fun "True" []])],
  [(Fun "conj" [Var (1,"Bool"), Var (2,"Bool")], Fun "conj" [Fun "False" [], Var "y"])],
  [(Fun "conj" [Var (1,"Bool"), Var (2,"Bool")], Fun "conj" [Var "x", Fun "False" []])]
  ]

examplePatternProblem2 :: PatternProblem
examplePatternProblem2 = take 2 examplePatternProblem1

-- for each type we can look up the constructors
type TypeInfo = Type -> [(FSym,FSymInfo)]

exampleTypeInfo :: TypeInfo
exampleTypeInfo "Bool" = [("True",([],"Bool")), ("False",([],"Bool"))]
exampleTypeInfo "Nat" = [("Zero",([],"Nat")), ("Succ",(["Nat"],"Nat"))]

-- Exercise 2.2

patternCompleteness :: TypeInfo -> [PatternProblem] -> Bool
patternCompleteness ti bigP = undefined

test1 = patternCompleteness exampleTypeInfo [examplePatternProblem1]
test2 = patternCompleteness exampleTypeInfo [examplePatternProblem2]