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."]