(* Types for our language *)
(*
  Functions: a -> b
  Booleans: bool
  Integers: int
  Floating-point numbers: float
  Pairs: a * b
  Lists: [a]
  Unit: unit

  type tyvar = TV of int
  type ty = TyVar of tyvar 
            |  Unit | Bool | Int | Float
                    | Pair of ty * ty
                    | List of ty
                    | Fun of ty * ty
*)



(*
  Unification Algorithm

  A substitution is an assignment of expressions to variables, a function
  from variables -> expressions.
  A unifier is a substitution that, when applied to all of the equations,
  makes them all true.

  A most general unifier X is a unifier for which,
  for any other unifier Y, Y = Z(X) for some substitution Z.
  

  Input  - list of pairs, each pair interpreted as an equation
  Output - None (on failure), or Some substitution function from vars
           to their associated values (or TyVar n for n if n is not
           mapped to anything).
*)

open Mp3common

(*
  Problem 1
*)
let rec has_var t x = failwith "not implemented"
     
(*
  Problem 2
*)
let rec substitute t x t' = failwith "not implemented"

(*
  Problem 3
*)
let rec subst_lst lst x t' = failwith "not implemented"

(*
  Problem 4
*)
let rec subst_sol_lst lst x t' = failwith "not implemented"

(*
  Problem 4
*)
let rec subst_sol_ls lst x t' = failwith "not implemented"

(*
  Problem 5
*)
let rec getval lst x = failwith "not implemented"

(*
  Problem 6
*)
let rec unify_aux sol lst = failwith "not implemented"

(*
  Problem 7
*)
let unify lst = failwith "not implemented"

(*
  Problem 8 -- enter your solution inside this comment.

*)

(*
  Problem 9 -- enter your solution inside this comment.

*)