(** 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 " 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. . 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