(** Bombs-Must-Detonate: BMDLang Type Checker
    @author Brian Go *)

type bmdtype = 
    TyInt
  | TyFloat
  | TyString
  | TyBool
  | TyVoid
  | TyList of bmdtype
  | TyEnumType of string
  | TyEnum of string
  | TyStruct of string
  | TyArray of bmdtype
  | TyArrow of bmdtype list * bmdtype
  | TyRef of bmdtype
  | TyTemplate of string

(** Used to keep track of the typing environment during typechecking *)
type typeenvdef =
    TyEnumDef of string * string list
  | TyStructDef of string * (string * bmdtype) list * Ast.data_type list
  | TyFunDef of string * bmdtype
  | TyVarDef of string * bmdtype
  | TyTemplateDef of string list
  | TyIncludeDef of string

exception Type_error of string

(** Eliminates duplicate entries in a list *)
let rec elim_repeats lst = match lst with
    cur::rest when List.mem cur rest -> elim_repeats rest
  | cur::rest -> cur::(elim_repeats rest)
  | [] -> []


(** Linker header information buffer *)
let link_buffer = ref []

(** Clears the linker header information buffer *)
let reset_link_buffer () = link_buffer := []

(** Gets the contents of the linker header infromation *)
let get_link_buffer () = String.concat "" ((elim_repeats !link_buffer)@["END_HEADER\n"])

(** Appends a string to the linker buffer *)
let append_link_buffer str = 
  link_buffer := str::!link_buffer

(** Raises a type error from the concatenated string list *)
let raise_type_error s_list =
  let str = String.concat "" s_list in
    raise (Type_error str)

(** Renaming of String.concat "" *)
let concat s = String.concat "" s

(** Concatenates a list with commas.  No comma after the final element. *)
let rec concat_commas slist = 
  match slist with 
      x::[] -> x
    | x::rest -> concat [x;", ";concat_commas rest]
    | [] -> ""

(** Replaces an association list by a list of keys *)
let get_first lst = 
  let helper (x,y) = x in
    List.map helper lst

(** Replaces an association list by a list of values *)
let get_second lst = 
  let helper (x,y) = y in
    List.map helper lst

(** Checks if the given struct name is defined in the environment *)
let rec isdef_struct name env = 
  match env with
      (TyStructDef (s,_,_))::rest -> ((s = name) || isdef_struct name rest)
    | _::rest -> isdef_struct name rest
    | [] -> false

(** Checks if the given enum is defined in the environment *)
let rec isdef_enum name env = 
  match env with
      (TyEnumDef (s,_))::rest -> ((s = name) || isdef_enum name rest)
    | _::rest -> isdef_enum name rest
    | [] -> false

(** Checks if the given variable is defined in the environment *)
let rec isdef_var name env =
  match env with
      (TyVarDef (s,_))::rest -> ((s = name) || isdef_var name rest)
    | _::rest -> isdef_var name rest
    | [] -> false

(** Checks if the given function is defined in the environment *)
let rec isdef_fun name env = 
  match env with
      (TyFunDef (s,_))::rest -> ((s = name) || isdef_fun name rest)
    | _::rest -> isdef_fun name rest
    | [] -> false

(** Checks if the given template definition is defined in the environment *)
let rec isdef_templated name env = 
  match env with
      (TyTemplateDef slist)::rest -> List.mem name slist
    | _::rest -> isdef_templated name rest
    | [] -> false

(** Removes the most recent template definition from the environment *)
let rec remove_template_def env = 
  match env with
      (TyTemplateDef _) :: rest -> rest
    | cur :: rest -> cur :: (remove_template_def rest)
    | [] -> []

(** Checks if the given identifier is defined as a struct, enum, variable, or function in the environment *)
let rec isdef_ident name env = 
  isdef_struct name env
  || isdef_enum name env
  || isdef_var name env
  || isdef_fun name env


(** Gets the type of the given variable from the environment.  Raises Not_found if not defined.*)
let rec gettype_var name env = 
  match env with
      (TyVarDef (s,t))::rest when (s = name) -> t
    | _::rest -> gettype_var name rest
    | [] -> raise Not_found

(** Gets the type of the given function from the environment. Raises Not_found if not defined. *)
let rec gettype_fun name env = 
  match env with
      (TyFunDef (s,t))::rest when (s = name) -> t
    | _::rest -> gettype_fun name rest
    | [] -> raise Not_found

(** Checks if s2 is an enum value of enum type s1.  Raises Not_found if s1 is not an enum type. *)
let rec is_enum_value s1 s2 env =
  match env with 
      (TyEnumDef (s,lst))::rest when (s = s1) -> List.mem s2 lst
    | _::rest -> is_enum_value s1 s2 rest
    | [] -> raise Not_found

(** Checks if file "name" has been included in the given environment *)
let rec isdef_include name env = 
  match env with
      (TyIncludeDef s)::rest when (s = name) -> true
    | _::rest -> isdef_include name rest
    | [] -> false

(** Finds the index of a value in a list.  Raises Not_found if it is not in the list *)
let rec indexof str lst index =
  match lst with
      cur::rest when cur = str -> index
    | _::rest -> indexof str rest (index+1)
    | [] -> raise Not_found

(** Casts enum value s1.s2 to an integer.  Raises Not_found if s1.s2 is not defined *)
let rec get_enum_value s1 s2 env = 
  match env with 
      (TyEnumDef (s,lst))::rest when (s = s1) -> indexof s2 lst 0
    | _::rest -> get_enum_value s1 s2 rest
    | [] -> raise Not_found

(** Gets the total number of values of enum type ename.  Raises Not_found if ename is not an enum type *)
let rec get_nvalues_enum ename env = 
  match env with
      (TyEnumDef (s,lst))::rest when (s = ename) -> List.length lst
    | _::rest -> get_nvalues_enum ename rest
    | [] -> raise Not_found

(** Checks if s2 is a field of struct s1 from the environment.  Raises Not_found if s1 is not a struct *)
let rec is_struct_value s1 s2 env = 
  match env with 
      (TyStructDef (s,lst,_))::rest when (s = s1) -> List.mem s2 (get_first lst)
    | _::rest -> is_struct_value s1 s2 rest
    | [] -> raise Not_found

(** Gets the data type of field s2 of struct s1 from the environment.  Raises Not_found if s1 is not a struct *)
let rec gettype_struct s1 s2 env = 
  match env with
      (TyStructDef (s,lst,_))::rest when (s = s1) -> List.assoc s2 lst
    | _::rest -> gettype_struct s1 s2 rest
    | [] -> raise Not_found

(** Returns the integer index of field s2 in struct s1 as determined by environment env *)
let rec getfield_struct s1 s2 env = 
  let t_field = gettype_struct s1 s2 env in
  match env with
      (TyStructDef (s,lst,_))::rest when (s = s1) -> indexof (s2,t_field) lst 0
    | _::rest -> getfield_struct s1 s2 rest
    | [] -> raise Not_found

(** Returns the (string * bmdtype) list of struct fields of struct s1.  Raises Not_found if s1 is not defined. *)
let rec getfields_struct s1 env =
  match env with
      (TyStructDef (s,lst,_))::rest when (s = s1) -> lst
    | _::rest -> getfields_struct s1 rest
    | [] -> raise Not_found

(** Gets the number of fields of struct sname from the environment.  Raises Not_found if sname is not defined. *)
let rec nfields_struct sname env =
  match env with
      (TyStructDef (s,lst,_))::rest when (s = sname) -> List.length lst
    | _::rest -> nfields_struct sname rest
    | [] -> raise Not_found

(** Gets the AST data types of the struct fields *) 
let rec get_struct_data_type_list sname env =
  match env with 
      (TyStructDef (s,_,dtlist))::rest when (s = sname) -> dtlist
    | _::rest -> get_struct_data_type_list sname rest
    | [] -> raise Not_found


(** Annotates the data type AST element with information that will be needed by the IR *)
let annotate_data_type dt env = match dt with
    Ast.SynEnumOrStructType (s,tlist) ->
      if isdef_struct s env then 
	tlist := get_struct_data_type_list s env
      else if isdef_enum s env then
	tlist := [] 
      else 
	raise_type_error [s;" is not an enum or struct type but was used in a struct declaration."]
  | x -> ()
      
(** Creates a list of AST data type elements correlated with the struct fields *)
let rec make_struct_type_list varlist env = match varlist with
    (Ast.SynVarDeclareNoInit (dt,_))::rest ->
      let _ = annotate_data_type dt env in 
	dt::(make_struct_type_list rest env)
  | _::rest -> raise_type_error ["Struct declaration cannot contain a field initialization."]
  | [] -> []

(** Gives a string representation of the given type *)
let rec string_of_type ty = match ty with
    TyInt -> "int"
  | TyFloat -> "float"
  | TyString -> "string"
  | TyBool -> "bool"
  | TyVoid -> "void"
  | TyList t_list -> String.concat "" ["list(";string_of_type t_list;")"]
  | TyEnumType s -> String.concat "" ["enumType(";s;")"]
  | TyEnum s -> String.concat "" ["enum(";s;")"]
  | TyStruct s -> String.concat "" ["struct(";s;")"]
  | TyArray (t_arr) -> String.concat "" ["array(";string_of_type t_arr;")"]
  | TyArrow (t_args,t_ret) -> 
      let arg_string = List.map string_of_type t_args in
      let arg_string = if arg_string = []  then ["void"] else arg_string in
      String.concat " "
	(["function("]@arg_string@["->";string_of_type t_ret;")"])
  | TyRef t_ref -> String.concat "" ["ref(";string_of_type t_ref;")"]
  | TyTemplate s -> if s = "_unknown" then "_" else String.concat "" ["templated(";s;")"]

(** Gives an expanded string representation of the given enum type detailing its total number of values *)
let rec expanded_string_of_enum ename env =
  let nfields = get_nvalues_enum ename env in
    concat [ename;" : ";string_of_int nfields]

(** Gives an expanded string representation of the given struct type which includes the expanded representation
    of each of its fields *)
and expanded_string_of_struct sname env = 
  let struct_dts = get_second (getfields_struct sname env) in
  let helper x = x env in
  let string_list = List.map helper (List.map expanded_string_of_type struct_dts) in
    concat [sname;" : ";concat_commas string_list]
    
(** Gives a string representation of the given type with expanded represnetations of structs and enums *)
and expanded_string_of_type ty env = match ty with
    TyInt -> "int"
  | TyFloat -> "float"
  | TyString -> "string"
  | TyBool -> "bool"
  | TyVoid -> "void"
  | TyList t_list -> concat ["list(";expanded_string_of_type t_list env;")"]
  | TyEnumType s -> concat ["enumType(";expanded_string_of_enum s env;")"]
  | TyEnum s -> concat ["enum(";expanded_string_of_enum s env;")"]
  | TyStruct s -> concat ["struct(";expanded_string_of_struct s env;")"]
  | TyArray (t_arr) -> concat["array(";expanded_string_of_type t_arr env;")"]
  | TyArrow (t_args,t_ret) -> 
      let helper x = x env in
      let arg_string = List.map helper (List.map expanded_string_of_type t_args) in
      let arg_string = if arg_string = []  then ["void"] else arg_string in
      String.concat " "
	(["function("]@arg_string@["->";expanded_string_of_type t_ret env;")"])
  | TyRef t_ref -> concat ["ref(";expanded_string_of_type t_ref env;")"]
  | TyTemplate s -> if s = "_unknown" then "_" else concat ["templated(";s;")"]

(** Checks if op is a valid operator on values of type t1 and t2 *)
let rec isallowed_binop op t1 t2 = match (op,t1,t2) with
    (Ast.SynBinopAnd, TyBool, TyBool) -> true
  | (Ast.SynBinopOr, TyBool, TyBool) -> true
  | (Ast.SynBinopAdd, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynBinopSub, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynBinopMul, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynBinopDiv, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynBinopIDiv, TyInt, TyInt) -> true
  | (Ast.SynBinopMod, TyInt, TyInt) -> true
  | (Ast.SynBinopConcat, TyString, TyString) -> true
  | (Ast.SynBinopConcat, TyList t_list1, TyList t_list2) -> (t_list1 = t_list2)
  | (Ast.SynBinopCons, t_item, TyList t_list) -> (t_item = t_list)
  | (Ast.SynCompLt, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynCompGt, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynCompLte, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynCompGte, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynCompEq, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynCompNeq, (TyInt | TyFloat), (TyInt | TyFloat)) -> true
  | (Ast.SynCompEq, x, y) when (x = y) -> true
  | (Ast.SynCompNeq, x, y) when (x = y) -> true
  | _ -> false

(** Gets the type of the result of operator op on values of type t1 and t2.  Type error if invalid operator. *)
let rec gettype_binop op t1 t2 = match (op,t1,t2) with
    (Ast.SynBinopAnd, TyBool, TyBool) -> TyBool
  | (Ast.SynBinopOr, TyBool, TyBool) -> TyBool
  | (Ast.SynBinopAdd, TyInt, TyInt) -> TyInt
  | (Ast.SynBinopSub, TyInt, TyInt) -> TyInt
  | (Ast.SynBinopMul, TyInt, TyInt) -> TyInt
  | (Ast.SynBinopDiv, TyInt, TyInt) -> TyFloat
  | (Ast.SynBinopIDiv, TyInt, TyInt) -> TyInt
  | (Ast.SynBinopMod, TyInt, TyInt) -> TyInt
  | (Ast.SynBinopAdd, (TyInt | TyFloat), TyFloat) -> TyFloat
  | (Ast.SynBinopAdd, TyFloat, TyInt) -> TyFloat
  | (Ast.SynBinopSub, (TyInt | TyFloat), TyFloat) -> TyFloat
  | (Ast.SynBinopSub, TyFloat, TyInt) -> TyFloat
  | (Ast.SynBinopMul, (TyInt | TyFloat), TyFloat) -> TyFloat
  | (Ast.SynBinopMul, TyFloat, TyInt) -> TyFloat
  | (Ast.SynBinopDiv, (TyInt | TyFloat), TyFloat) -> TyFloat
  | (Ast.SynBinopDiv, TyFloat, TyInt) -> TyFloat
  | (Ast.SynBinopConcat, TyString, TyString) -> TyString
  | (Ast.SynBinopConcat, TyList t_list1, TyList t_list2) when (t_list1 = t_list2) -> TyList t_list1
  | (Ast.SynBinopCons, t_item, TyList t_list) when (t_item = t_list) -> TyList t_list
  | (Ast.SynCompLt, (TyInt | TyFloat), (TyInt | TyFloat)) -> TyBool
  | (Ast.SynCompGt, (TyInt | TyFloat), (TyInt | TyFloat)) -> TyBool
  | (Ast.SynCompLte, (TyInt | TyFloat), (TyInt | TyFloat)) -> TyBool
  | (Ast.SynCompGte, (TyInt | TyFloat), (TyInt | TyFloat)) -> TyBool
  | (Ast.SynCompEq, (TyInt | TyFloat), (TyInt | TyFloat)) -> TyBool
  | (Ast.SynCompNeq, (TyInt | TyFloat), (TyInt | TyFloat)) -> TyBool
  | (Ast.SynCompEq, x, y) when (x = y) -> TyBool
  | (Ast.SynCompNeq, x, y) when (x = y) -> TyBool
  | _ -> raise_type_error ["Attempted to perform an invalid binary operation ";Ast.string_of_binop op;" on values of type ";string_of_type t1;" and ";string_of_type t2]

(** Types a list of AST data type element *)
let rec type_data_types dt_lst env =
  match dt_lst with
      Ast.SynIntType::rest -> TyInt::(type_data_types rest env)
    | Ast.SynFloatType::rest -> TyFloat::(type_data_types rest env)
    | Ast.SynStringType::rest -> TyString::(type_data_types rest env)
    | Ast.SynBoolType::rest -> TyBool::(type_data_types rest env)
    | Ast.SynVoidType::rest -> TyVoid::(type_data_types rest env)
    | (Ast.SynEnumOrStructType (s,field_types))::rest ->
	if isdef_struct s env then 
	  let _ = field_types  := get_struct_data_type_list s env in
	    (TyStruct s)::(type_data_types rest env)
	else if isdef_enum s env then 
	  (TyEnum s)::(type_data_types rest env)
	else if isdef_templated s env then
	  (TyTemplate s)::(type_data_types rest env)
	else raise_type_error ["Invalid data type: ";s;" expected enum, struct, or templated type."]
    | (Ast.SynArrayType (dt,n))::rest ->
	let t_n,_ = type_value_producer n env in
	  if t_n = TyInt then 
	    (TyArray (type_data_type dt env))::(type_data_types rest env)
	  else
	    raise_type_error ["Invalid array index type ";string_of_type t_n;" expected an integer value."]
    | (Ast.SynListType dt)::rest ->
	(TyList (type_data_type dt env))::(type_data_types rest env)
    | (Ast.SynRefType dt)::rest ->
	(TyRef (type_data_type dt env))::(type_data_types rest env)
    | (Ast.SynArrowType (arglist_types,ret_type))::rest ->
	let arglist_types = type_data_types arglist_types env in
	  (TyArrow ((if arglist_types = [] then [TyVoid] else arglist_types), 
		    type_data_type ret_type env))::(type_data_types rest env)
    | [] -> []

(** Types a single AST data type element *)
and type_data_type dt env = 
  let verified_type_lst = type_data_types [dt] env in
    match verified_type_lst with 
	x::rest -> x
      | [] -> raise_type_error ["Unexpected type error."]

(** Types the declaration of a list of struct fields.  Initial values not allowed, type error if they are. *)
and structdef_list lst env = match lst with
    (Ast.SynVarDeclareNoInit (dt,s))::[] -> [s,type_data_type dt env]
  | (Ast.SynVarDeclareNoInit (dt,s))::rest -> (s,type_data_type dt env)::(structdef_list rest env)
  | _ -> raise_type_error ["Expected uninitialized variable declaration in struct definition."] 

(** Types an argument list to a function, adding the arguments as variable declarations to the environment. *)
and vardef_arglist arglist env = 
  match arglist with 
      (dt,name)::rest -> vardef_arglist rest ((TyVarDef (name,type_data_type dt env))::env)
    | [] -> env

(** Types a value *)
and type_value v env = match v with
    Ast.SynIntValue _ -> TyInt, env
  | Ast.SynFloatValue _ -> TyFloat, env
  | Ast.SynBoolValue _ -> TyBool, env
  | Ast.SynStringValue _ -> TyString, env

(** Produces a comma-separated string representation of a list of types *)
and string_of_type_list lst = match lst with
    t::[] -> string_of_type t
  | t::rest -> String.concat "" [string_of_type t;", ";string_of_type_list rest]
  | [] -> ""

(** Checks if association list l1 has no conflicting key/value pairs with association list l2 *)
and are_assoclists_compatible l1 l2 = match l1 with
    (x,y)::rest -> 
      if List.mem_assoc x l2 
      then y = List.assoc x l2
      else are_assoclists_compatible rest l2
  | [] -> true

(** Returns an association list of template types to bmdtypes.  Type error if t2 cannot be unified to t1. *)
and unify_types t1 t2 = match t1,t2 with
    x,y when x = y -> []
  | TyList t_list1, TyList t_list2 -> unify_types t_list1 t_list2
  | TyArray t_arr1, TyArray t_arr2 -> unify_types t_arr1 t_arr2
  | TyArrow (args1,ret1), TyArrow (args2,ret2) -> 
      let assoc1 = unify_types ret1 ret2 in
      let assoc2 = List.flatten (List.map2 unify_types args1 args2) in
	if are_assoclists_compatible assoc1 assoc2 then
	  assoc1 @ assoc2
	else 
	  raise_type_error ["Could not unify templated arrow type ";
			    string_of_type t2;
			    " with ";
			    string_of_type t1]
  | TyRef t_ref1, TyRef t_ref2 -> unify_types t_ref1 t_ref2
  | TyTemplate s, t2 -> [(s,t2)]
  | _ -> raise_type_error ["Expected type ";
			   string_of_type t1;
			   " but got type ";
			   string_of_type t2]

(** Uses the association list (substitution list) template_map (key: template string, value: bmdtype)
    to type the given data type with those substitutions *)
and insert_template_types template_map env dt = 
  let insert_types = insert_template_types template_map env in
    match dt with
	TyList t -> TyList (insert_types t)
      | TyArray t -> TyArray (insert_types t)
      | TyArrow (args,ret) -> TyArrow (List.map insert_types args, insert_types ret)
      | TyRef t -> TyRef (insert_types t)
      | TyTemplate s -> 
	  if List.mem_assoc s template_map then
	    List.assoc s template_map
	  else if isdef_templated s env then
	    TyTemplate s
	  else 
	    raise_type_error ["Expression has free template type ";string_of_type dt;" in result."]
      | x -> x

(** Apply argtypes to the arrow type, making sure there are no 
   template inconsistencies, and get the return type *)
and apply_arrow_type arrowtype argtypes env = 
  let lhs_types, ret_type = match arrowtype with
      TyArrow (x,y) -> x,y
    | _ -> raise_type_error ["Attempted to apply arguments to something of non-arrow type ";string_of_type arrowtype;"."]
  in
  let isVoidArgs = lhs_types = [TyVoid] && (List.length argtypes = 0) in
  let _ = 
    if (not isVoidArgs) && ((List.length lhs_types) != (List.length argtypes))
    then raise_type_error ["Attempted to apply an incorrect number of arguments to arrow type ";string_of_type arrowtype;"."]
    else ()
  in
  let template_map = ref [] in
  let _ = 
    if isVoidArgs then () else
      for i = 0 to (List.length lhs_types)-1 do
	let cur_lhs, cur_arg = List.nth lhs_types i, List.nth argtypes i in
	let unify_result = unify_types cur_lhs cur_arg in
	  if are_assoclists_compatible unify_result !template_map then
	    template_map := unify_result @ !template_map
	  else
	    raise_type_error ["Could not apply argument types ";
			      string_of_type_list argtypes;
			      " to a function of type ";
			      string_of_type arrowtype]
      done
  in
    insert_template_types !template_map env ret_type
      
(** Types a function call as a value-producer (checks argument types, gives the return type).
    Updates the linker header with inferred remote call types. *)
and type_function_call_value funcall env = match funcall with
    Ast.SynLocalCall (s,vprod_list,isvar) -> 
      if isdef_fun s env || isdef_var s env then
	let fun_type = 
	  if isdef_fun s env then 
	    gettype_fun s env 
	  else 
	    let _ = isvar := true in
	      gettype_var s env 
	in
	let vplist_types,_ = type_value_producer_list_nonuniform vprod_list env in
	  try
	    apply_arrow_type fun_type vplist_types env, env
	  with
	      Type_error err_string ->
		raise_type_error ["Call to (local) function ";s;" was malformed. ";err_string]
      else 
	raise_type_error ["(Local) function call to undefined function ";s;"."]
  | Ast.SynRemoteCall (s,vprod_list, var_ident) -> (** the linker must do most of the work here **)
      let argtypes,_ = type_value_producer_list_nonuniform vprod_list env in
      let rettype,_ = type_variable_identifier var_ident env in
      let _ = append_link_buffer (concat ["require ";s;" = ";expanded_string_of_type (TyArrow (argtypes,rettype)) env;"\n";]) in
	TyBool, env (** the result is true or false depending on call success/failure **)
  | Ast.SynRemoteCallNoResult (s,vprod_list) -> (** again, the linker will do most of the work **)
      let argtypes,_ = type_value_producer_list_nonuniform vprod_list env in
      let rettype = TyTemplate ("_unknown") in
      let _ = append_link_buffer (concat ["require ";s;" = ";expanded_string_of_type (TyArrow (argtypes,rettype)) env;"\n";]) in
	TyBool, env
	
(** Types a binary operation vp1 op vp2.  Type error if not a valid operation *)
and type_binop vp1 op vp2 env =
  let t_vp1,_ = type_value_producer vp1 env in
  let t_vp2,_ = type_value_producer vp2 env in
    if isallowed_binop op t_vp1 t_vp2 then
      (gettype_binop op t_vp1 t_vp2), env
    else 
      raise_type_error ["Attempted to perform an invalid binary operation ";Ast.string_of_binop op;" on values of type ";string_of_type t_vp1;" and ";string_of_type t_vp2;"."]
    
(** Types a unary operation expression. Type error if not a valid operation. *)
and type_prefix_unop op vp env = 
  let t_vp,_ = type_value_producer vp env in
    match (op,t_vp) with 
	Ast.SynUnopNot, TyBool -> TyBool, env
      | Ast.SynUnopCar, TyList t_list -> t_list, env
      | Ast.SynUnopCdr, TyList t_list -> TyList t_list, env
      | Ast.SynUnopTrunc, (TyFloat | TyInt) -> TyInt, env
      | Ast.SynUnopDeref, TyRef t_ref -> t_ref, env
      | Ast.SynUnopNeg, TyInt -> TyInt, env
      | Ast.SynUnopNeg, TyFloat -> TyFloat, env
      | Ast.SynUnopNull, _ -> TyBool, env
      | _ -> raise_type_error ["Attempted to perform an invalid prefix unary operation on a value of type ";string_of_type t_vp;"."]

(** Types an array value producer (i.e. {elem1, elem2...}.  Error if empty (we need to infer the type),
    or if values of different types are used. *)
and type_array_value_producer vp_list env = match vp_list with
    vp::[] ->
      let vp_type,_ = type_value_producer vp env in
	TyArray vp_type, env
  | vp::rest ->
      let vp_type,_ = type_value_producer vp env in
      let rest_type,_ = type_array_value_producer rest env in
	(match rest_type with
	     TyArray rest_arr_type when rest_arr_type = vp_type ->
	       TyArray vp_type, env
	   | _ -> raise_type_error ["An element of type ";string_of_type vp_type;" is being used with an array of type ";string_of_type rest_type;"."])
  | [] -> raise_type_error ["Constant array values must be non-empty."]

(** Types a list of value producers (i.e. [elem1; elem2;...])  Error if empty or 
    if values of different types are used. *)
and type_value_producer_list vp_list env = match vp_list with
    vp::[] ->
      let vp_type,_ = type_value_producer vp env in
	TyList vp_type, env
  | vp::rest ->
      let vp_type,_ = type_value_producer vp env in
      let rest_type,_ = type_value_producer_list rest env in
	if TyList vp_type = rest_type then
	  TyList vp_type, env
	else 
	  raise_type_error ["An element of type ";string_of_type vp_type;" is being used with list of type ";string_of_type rest_type;"."]
  | [] -> raise_type_error ["Constant list values must be non-empty."]

(** Types a list value producer *)
and type_list_value_producer vp_list env = match vp_list with
    Ast.SynListNil dt -> 
      let t_dt = type_data_type dt env in
	TyList t_dt, env
  | Ast.SynListList vp_list ->
      type_value_producer_list vp_list env
  | Ast.SynListCons (vp1,vp2) ->
      let t_vp1,_ = type_value_producer vp1 env in
      let t_vp2,_ = type_value_producer vp2 env in
	(match t_vp2 with 
	    TyList t_list when t_list = t_vp1 -> t_vp2, env
	  | _ -> raise_type_error ["Cannot cons a value of type ";string_of_type t_vp1;" to a list of type ";string_of_type t_vp2;"."])

(** Types a value producer *)
and type_value_producer vp env = match vp with
    Ast.SynValue v -> type_value v env
  | Ast.SynFunctionCallValue funcall -> type_function_call_value funcall env
  | Ast.SynVarIdentifier vident -> type_variable_identifier vident env 
  | Ast.SynBinop (vp1,op,vp2) -> type_binop vp1 op vp2 env
  | Ast.SynPrefixUnop (op,vp) -> type_prefix_unop op vp env
  | Ast.SynParenthesized vp -> type_value_producer vp env
  | Ast.SynArrayValueProducer vp_list -> type_array_value_producer vp_list env
  | Ast.SynListValueProducer vp_list -> type_list_value_producer vp_list env

(** Returns a list of types, i.e. for parameters *)
and type_value_producer_list_nonuniform vp_list environment =  
  let helper vplist env = 
    match vplist with
	vp::rest -> 
	  let t_vp,_ = type_value_producer vp env in
	  let t_rest,_ = type_value_producer_list_nonuniform rest env in
	    t_vp::t_rest
      | [] -> []
  in
    helper vp_list environment, environment

(** Types a variable identifier *)
and type_variable_identifier v_ident env = match v_ident with
    Ast.SynVarName s -> 
      if isdef_var s env then
	gettype_var s env, env
      else if isdef_enum s env then
	TyEnumType s, env
      else if isdef_struct s env then
	TyStruct s, env
      else if isdef_fun s env then
	gettype_fun s env, env
      else
	raise_type_error ["Variable ";s;" was used but not defined."]
  | Ast.SynStructOrEnumValue (vid1,s2,field_info) ->
      let t_vid,_ = type_variable_identifier vid1 env in
	(match t_vid with
	     TyEnumType s1 -> 
	       if is_enum_value s1 s2 env then
		 let index = get_enum_value s1 s2 env in
		 let _ = field_info := (Ast.VIdEnumValue index) in
		   TyEnum s1, env
	       else 
		 raise_type_error [s1;".";s2;" is not an enum value of enum type ";s1;"."]
	   | TyStruct s1 ->
	       if isdef_struct s1 env then
		 if is_struct_value s1 s2 env then
		   let index = getfield_struct s1 s2 env in
		   let _ = field_info := (Ast.VIdStructField index) in
		   gettype_struct s1 s2 env, env
		 else
		   raise_type_error [s1;".";s2;" refers to a non-existent field of struct type ";string_of_type t_vid;"."]
	       else
		 raise_type_error [s1;" is used as a struct but is not a struct."]
	   | _ -> raise_type_error ["An identifier of type ";string_of_type t_vid;" is not a struct or enum type in this scope."])
  | Ast.SynArrayCell (vp,i) -> 
      let t,_ = type_variable_identifier vp env in
      let t_index,_ = type_value_producer i env in
	(match (t,t_index) with
	     TyArray t_arr, TyInt ->
	       t_arr, env
	   | _ -> raise_type_error ["A value of non-array-type ";string_of_type t;" is used as an array type."])	    

(** Types a variable assignment *)
let type_var_assign vasgn env = match vasgn with 
    Ast.SynVarAssignment (var,vprod) ->
      let var_type, temp_env = type_variable_identifier var env in
      let vp_type, new_env = type_value_producer vprod temp_env in
	if vp_type = var_type or TyRef vp_type = var_type then 
	  TyVoid, new_env
	else 
	  raise_type_error ["Cannot assign a value of type ";string_of_type vp_type;" to something of type ";string_of_type var_type;"."]
  | Ast.SynVarModify (vident, op, vprod) -> 
      let var_type, temp_env = type_variable_identifier vident env in
      let vp_type, new_env = type_value_producer vprod temp_env in
      let t1, t2 = 
	(match op with 
	     Ast.SynBinopCons -> vp_type, var_type
	   | _ -> var_type, vp_type) (** flip order for cons, the list is being mutated **)
      in
	if isallowed_binop op t1 t2 then
	  TyVoid, new_env
	else 
	  raise_type_error ["Cannot use operator ";Ast.string_of_binop op;" to mutate a value of type ";string_of_type var_type;" with an argument of type ";string_of_type vp_type;"."]

(** Types a variable declaration *)
let type_var_declaration vdecl env = match vdecl with
    Ast.SynVarDeclareNoInit (dt,s) ->
      if isdef_ident s env then 
	raise_type_error ["Cannot declare ";s;" as a variable; it has already been declared."]
      else
	let new_dt = type_data_type dt env in
	  (match new_dt with
	       TyTemplate s -> raise_type_error ["Cannot declare templated variable ";s;" without explicit initialization."]
	     | _ ->
		 let new_env = (TyVarDef (s,new_dt))::env in
		   TyVoid, new_env)
  | Ast.SynVarDeclareWithInit (dt,s,vp) ->
      if isdef_ident s env then
	raise_type_error ["Cannot declare ";s;" as a variable; it has already been declared."]
      else
	let new_dt = type_data_type dt env in
	let temp2_env = (TyVarDef (s,new_dt))::env in
	let vp_dt,new_env = type_value_producer vp temp2_env in
	  if vp_dt = new_dt then
	    TyVoid, new_env
	  else 
            raise_type_error ["Variable ";s;" has type ";string_of_type new_dt;" but is being initialized with a value of type ";string_of_type vp_dt;"."]

(** Types a conditional expression *)
let rec type_conditional cond env rettype = match cond with 
    Ast.SynIf (vprod,expr_list) ->
      let vp_type, new_env = type_value_producer vprod env in
	if vp_type = TyBool then
	  let body_type,_ = type_expression_list expr_list env rettype in
	    if body_type = TyVoid then
	      TyVoid, new_env
	    else 
	      raise_type_error ["Conditional body was not well-formed."]
	else
	  raise_type_error ["Conditional test expression must have a boolean type."]
  | Ast.SynIfCase (vprod,expr_list,continued_cond) ->
      let vp_type, new_env = type_value_producer vprod env in
	if vp_type = TyBool then
	  let body_type,_ = type_expression_list expr_list env rettype in
	    if body_type = TyVoid then
	      type_continued_conditional continued_cond new_env rettype
	    else 
	      raise_type_error ["Conditional case body was not well-formed."]
	else 
	  raise_type_error["Conditional case test expression must have a boolean type."]

(** Types an else case *)
and type_continued_conditional continued_cond env rettype = match continued_cond with
    Ast.SynFinalElse expr_list -> 
      let body_type,_ = type_expression_list expr_list env rettype in
	if body_type = TyVoid then
	  TyVoid, env
	else
	  raise_type_error ["Final else body was not well-formed."]
  | Ast.SynElse cond -> type_conditional cond env rettype

(** Types a loop *)
and type_loop loop env rettype = match loop with
    Ast.SynWhile (vprod, loop_expr_list) -> 
      let vp_type, new_env = type_value_producer vprod env in
	(match vp_type with
	     TyBool ->
	       let body_type,_ = type_expression_list loop_expr_list env rettype in
		 (match body_type with
		      TyVoid -> TyVoid, new_env
		    | _ -> raise_type_error ["While loop body was not well-formed."])
	   | _ -> raise_type_error ["While loop test expression must have a boolean type."])
  | Ast.SynDoWhile (loop_expr_list, vprod) -> 
      let vp_type, new_env = type_value_producer vprod env in
	(match vp_type with
	     TyBool ->
	       let body_type,_ = type_expression_list loop_expr_list env rettype in
		 (match body_type with
		      TyVoid -> TyVoid, new_env
		    | _ -> raise_type_error ["While loop body was not well-formed."])
	   | _ -> raise_type_error ["While loop test expression must have a boolean type."])
  | Ast.SynFor (init_expr, test_vprod, step_expr, loop_expr_list) ->
      let _, init_env = type_expression init_expr env rettype in
      let vp_type, _ = type_value_producer test_vprod init_env in
      let _ = type_expression step_expr init_env rettype in
	(match vp_type with
	     TyBool ->
	       let _ = type_expression step_expr in (** we dont care about the type as long as it has one **)
	       let body_type,_ = type_expression_list loop_expr_list init_env rettype in
		 (match body_type with
		      TyVoid -> TyVoid, env
		    | _ -> raise_type_error ["For loop body was not well-formed."])
	   | _ -> raise_type_error ["For loop test expression must have a boolean type."])

(** Types a function call expression.  This is not a value producer, so regardless of return type 
   the expression will have type void *)
and type_function_call funcall env rettype = match funcall with
    Ast.SynLocalCall (s,vprod_list,isvar) -> 
     if isdef_fun s env || isdef_var s env then
	let fun_type = 
	  if isdef_fun s env then 
	    gettype_fun s env 
	  else 
	    let _ = isvar := true in
	      gettype_var s env 
	in
	
	let vplist_types,_ = type_value_producer_list_nonuniform vprod_list env in
	  try
	    let _ = apply_arrow_type fun_type vplist_types env in
	      TyVoid, env
	  with
	      Type_error err_string ->
		raise_type_error ["Call to (local) function ";s;" was malformed. ";err_string]
     else 
	raise_type_error ["(Local) function call to undefined function ";s;"."]
  | Ast.SynRemoteCall (s,vprod_list, var_ident) -> (** the linker must do most of the work here **)
      let argtypes,_ = type_value_producer_list_nonuniform vprod_list env in
      let rettype,_ = type_variable_identifier var_ident env in
      let _ = append_link_buffer (concat ["require ";s;" = ";expanded_string_of_type (TyArrow (argtypes,rettype)) env;"\n"]) in
	TyVoid, env
  | Ast.SynRemoteCallNoResult (s,vprod_list) -> (** again, the linker will do most of the work **)
      let argtypes,_ = type_value_producer_list_nonuniform vprod_list env in
      let rettype = TyTemplate "_unknown" in
      let _ = append_link_buffer (concat ["require ";s;" = ";expanded_string_of_type (TyArrow (argtypes,rettype)) env;"\n"]) in
	TyVoid, env

(** Types an expression.  We use void to indicate a successful typing, since expressions have no 
    actual type. *)
and type_expression expr env rettype = match expr with
    Ast.SynVarDeclare vdecl -> type_var_declaration vdecl env
  | Ast.SynEnumDeclare (s, slist) ->
      if isdef_ident s env then
	raise_type_error ["Cannot declare ";s;" as a variable; it has already been declared."]
      else 
	TyVoid, (TyEnumDef (s,slist))::env
  | Ast.SynVarAssign vasgn -> type_var_assign vasgn env
  | Ast.SynCond cond -> type_conditional cond env rettype
  | Ast.SynLoop loop -> type_loop loop env rettype
  | Ast.SynFunctionCall funcall -> type_function_call funcall env rettype
  | Ast.SynReturnStatement ret -> 
      (match ret with
	   Ast.SynVoidReturn -> 
	     if rettype = TyVoid then
	       TyVoid, env
	     else 
	       raise_type_error ["Invalid return statement: expected a value of type void but received one of type ";string_of_type rettype;"."]
	 | Ast.SynValueReturn vprod ->
	     let vp_type, new_env = type_value_producer vprod env in
	       if vp_type = rettype then
		 TyVoid, new_env
	       else 
		 raise_type_error ["Invalid return statement: expected a value of type ";string_of_type rettype;" but received one of type ";string_of_type vp_type;"."])
  | Ast.SynBreak -> TyVoid, env
  | Ast.SynContinue -> TyVoid, env

(** Types an expression list.  Checks if all expressions are validly (void) typed, and then returns
    void type.  Otherwise raises type errors *)
and type_expression_list lst env rettype = match lst with
    expr::rest -> 
      let ty,new_env = type_expression expr env rettype in
	(match ty with
	     TyVoid -> type_expression_list rest new_env rettype
	   | _ -> raise_type_error ["Invalid expression encountered."])
  | [] -> TyVoid, env

(** Types a program (top-level expression list *)
and type_program p env = match p with
    expr::rest -> 
      let t,new_env = type_global_expression expr env in
	(match t with
	     TyVoid -> type_program rest new_env
	   | _ -> raise_type_error ["Global expression was not well formed (non-void type)."])
  | [] -> TyVoid, env

(** Types a top level expression *)
and type_global_expression ast env = 
  match ast with
      Ast.SynFunctionDeclare (dt,lbl,arg_list) ->
	if isdef_ident lbl env then
	  raise_type_error ["Function ";lbl;" is defined more than once."]
	else
	  let fun_type = 
	    let arglist_types = type_data_types (get_first arg_list) env in
	    TyArrow ((if arglist_types = [] then [TyVoid] else arglist_types), 
		     type_data_type dt env) in
	  let new_env = (TyFunDef (lbl,fun_type))::env in
	    TyVoid, new_env
    | Ast.SynRemotableFunctionDeclare (dt,lbl,arg_list) ->
	let fun_type = 
	  let arglist_types = type_data_types (get_first arg_list) env in
	    TyArrow ((if arglist_types = [] then [TyVoid] else arglist_types), 
		     type_data_type dt env) 
	in
	let _ = append_link_buffer (concat ["provide ";lbl;" = ";expanded_string_of_type fun_type env;"\n"]) in
	let new_env = (TyFunDef (lbl,fun_type))::env in
	  TyVoid, new_env
    | Ast.SynFunctionDefine ((dt,lbl,arg_list),expr_list) ->
	let ret_type = type_data_type dt env in
	let fun_type =
	  let arglist_types = type_data_types (get_first arg_list) env in
	    TyArrow ((if arglist_types = [] then [TyVoid] else arglist_types),
		     ret_type) in
	let new_env = (TyFunDef (lbl,fun_type))::env in
	let body_env = vardef_arglist arg_list new_env in
	let body_type,_ = type_expression_list expr_list body_env ret_type in
	  (match body_type with 
	      TyVoid -> TyVoid, new_env
	    | _ -> raise_type_error ["Function body had an invalid type."])
    | Ast.SynTemplatedDeclare (typelist, expr) ->
	let new_env = (TyTemplateDef typelist)::env in
	let result_type,result_env = type_global_expression expr new_env in
	  result_type, remove_template_def result_env
    | Ast.SynTemplatedDefine (typelist, expr) ->
	let new_env = (TyTemplateDef typelist)::env in
	let result_type,result_env = type_global_expression expr new_env in
	  result_type, remove_template_def result_env
    | Ast.SynStructDeclare (s,varlist) -> 
	let typed_varlist = structdef_list varlist env in
	let type_list = make_struct_type_list varlist env in
	let new_env = (TyStructDef (s, typed_varlist, type_list))::env in
	  TyVoid, new_env
    | Ast.SynGlobalEnumDeclare (s, lst) ->
	TyVoid, (TyEnumDef (s,lst))::env
    | Ast.SynGlobalVarDeclare vdecl -> 
	(match vdecl with
	     Ast.SynVarDeclareNoInit (dt, s) ->
	       let new_dt = type_data_type dt env in
	       let new_env = (TyVarDef (s,new_dt))::env in
		 TyVoid, new_env
	   | _ -> raise_type_error ["Global variable declarations cannot be initialized."])
    | Ast.SynInclude data ->
	(** If this is the first time processing this include, parses the include and inserts 
	    its AST after typechecking it.  If not, skips it. *)
	(match !data with
	     Ast.IncludeFileName s ->
	       if isdef_include s env then
		 let _ = begin
		   data := (Ast.IncludeAst []);
		   print_string "Skipping repeat include ";
		   print_string s;
		   print_string ".\n";
		   flush stdout;
		 end
		 in
		   TyVoid, env
	       else
		 (let ast = ref [] in
		    try
		      let inchan = open_in s in
		      let lexbuf = Lexing.from_channel inchan in
			begin
			  ast := Bmdparse.program Bmdlex.bmd_lang lexbuf;
			  print_string "Type checking include ";
			  print_string s;
			  print_string ".\n";
			  flush stdout;
			  let t,new_env = type_program !ast env in
			    (match t with 
				 TyVoid -> 
				   let _ = data := (Ast.IncludeAst !ast) in
				     TyVoid, (TyIncludeDef s)::new_env
			       | _ -> raise_type_error ["Typechecking of include file ";s;" failed.\n"])
			end
		    with 
			Parsing.Parse_error -> raise_type_error ["Syntax error in include file ";s;" line ";string_of_int !Bmdlex.line_count;".\n"])
	   | _ ->
	       raise_type_error ["Unexpected type error: include should be specified by file name, not as an ast."])
    | Ast.SynStateMachine _ ->
	(** State machine declarations should be eliminated from code during source-to-source compilation. *)
	raise_type_error ["Unexpected type error: source-to-source compilation of state machine failed."]

(** Determines whether an AST is validly typed.  Prints typing exceptions. *)
let is_typed p = 
  try
    let t,_ = type_program p [] in
      match t with
	  TyVoid -> true
	| _ -> false
  with Type_error s -> 
    let _ = output_string stderr s in
    let _ = output_string stderr "\n" in
    let _ = flush stderr in
      false