(* -----------------------------------------------------------
    Here are some test programs for your type checker. Note that
    two of these programs are not type correct.
   -----------------------------------------------------------
 *)


val prog = letdef ([("id",lambda ("x", variable "x"))],
		   cond (application(variable "id", constant_bool true),
			 application(variable "id", constant_int 3),
                         constant_int 4))



val prog1 = lambda ("x", cond (application (variable "x", constant_bool true),
			       application(variable "x", constant_bool false),
			       constant_bool false))



val prog2 = 
    letdef ([("id",lambda ("y", variable "y")),
	     ("f", lambda ("x",lambda ("y", 
			cond 
			  (application (variable "x", constant_bool true),
			   application(variable "x", variable "y"),
			   constant_int 4))))],
             application (variable "f", variable "id"))


val prog3 = 
    letdef ([("id",lambda ("y", variable "y")),
	     ("f", lambda ("y", 
			cond 
			  (application (variable "id", constant_bool true),
			   application(variable "id", variable "y"),
			   constant_int 4)))],
            variable "f")

val prog4 = 
     letdef ([("nil", alist []), 
              ("a", application (application(variable "cons", constant_int 3),
				variable "nil"))],
             variable "a")

	       



val prog5 = 
     letdef ([("length", lambda("L", 
       cond(application(application(variable "=", variable "L"), alist []),
	    constant_int 0, 
	    application(application(variable "+",constant_int 1),
			application(variable "length",
				    application(variable "tl", variable "L"))))
       ))],
     application(application(variable "+", 
		      application(variable "length",
				  alist [constant_bool true])),
		 application(variable "length", alist [constant_int 1])))





val prog6 = 
     letdef ([("length", lambda("L", 
       cond(application(application(variable "=", variable "L"), alist []),
	    constant_int 0, 
	    application(application(variable "+",constant_int 1),
			application(variable "length",
				    application(variable "tl", variable "L"))))
       ))],
     variable "length")



val prog7 = 
  lambda ("x", letdef([("id", variable "x")], 
		      cond (application(variable "id", constant_bool true),
			    application(variable "id", constant_int 5),
			    application(variable "id", constant_int 7))))



val compose = 
    lambda("f", lambda("g", lambda("x",
       application(variable "f", application (variable "g", variable "x")))))



val prog8 = 
   letdef(
       [("length", 
         lambda("L", 
	   cond(application(application(variable "=", variable "L"), alist []),
		constant_int 0, 
		application(application(variable "+",constant_int 1),
			    application(variable "length",
				application(variable "tl", variable "L")))))
	   ),
       ("nil", alist[]),
       ("a", application(application(variable "cons", constant_int 1),
			 variable "nil")),
       ("b", application(application(variable "cons", constant_bool true),
			 variable "nil"))],
       application (application (variable "+", application (variable "length",
							 variable "a")),
		 application(variable "length", variable "b")))
		 




(* -------------------------------------------------------------------
   Here is an environment that gives the types of some of the predefined 
   operators.
   ------------------------------------------------------------------- *)

val init_env = [("+", integer-->integer-->integer),
		("=", typevar "T=" --> typevar "T=" --> boolean),
		("cons",  typevar "Tcons" --> 
			  listtype (typevar "Tcons") --> 
			  listtype (typevar "Tcons")),
		("hd", listtype (typevar "Thd") --> typevar "Thd"),
		("tl", listtype (typevar "Ttl") --> 
		                           listtype(typevar "Ttl"))]