(* Status;
   tc* take share a global_env which since I moved tcExp out of tcFunDecl
   is no longer in scope. This needs to be fixed.  The remaining typechecking
   code is in place. We probably need a single env containing this globalenv
   and whatever localenv. *)

open Popsyntax;;

module X = Poperr
module L = Poplocus

type global_env = { structs : (type_name,structdecl) Dict.dict;
		    unions  : (type_name,uniondecl)  Dict.dict;
		    abstracts : (type_name,bool) Dict.dict;
		    globals : (var,typ) Dict.dict
		  }

(* Environment of a function *)
type f_env =
    { f_name : var;
      f_args : (var * typ) list;
      f_ret_type : typ;
      f_locals : (var * typ) list;
      f_inloop : bool }

(* Nested environments needed for Cyclone type checking *)
type cyc_env =
    Outermost of f_env * (var,typ) Dict.dict
  | Frame of f_env * cyc_env
  | Hidden of f_env * cyc_env
  | NoFrame (* When we are not in a function. *)
;;

let rec set_inloop cenv =
  match cenv with
    Outermost(fenv,globals) ->
      Outermost({ f_name = fenv.f_name;
                  f_args = fenv.f_args;
                  f_ret_type = fenv.f_ret_type;
                  f_locals = fenv.f_locals;
                  f_inloop = true },
                globals)
  | Frame(fenv,cenv') ->
      Frame({ f_name = fenv.f_name;
              f_args = fenv.f_args;
              f_ret_type = fenv.f_ret_type;
              f_locals = fenv.f_locals;
              f_inloop = true },
            cenv')
  | Hidden(fenv,cenv') ->
      Hidden(fenv,set_inloop cenv')
  | NoFrame -> NoFrame

let rec add_var x t cenv =
  match cenv with
    Outermost(fenv,globals) ->
      Outermost({ f_name = fenv.f_name;
                  f_args = fenv.f_args;
                  f_ret_type = fenv.f_ret_type;
                  f_locals = (x,t)::fenv.f_locals;
                  f_inloop = fenv.f_inloop },
                globals)
  | Frame(fenv,cenv') ->
      Frame({ f_name = fenv.f_name;
              f_args = fenv.f_args;
              f_ret_type = fenv.f_ret_type;
              f_locals = (x,t)::fenv.f_locals;
              f_inloop = fenv.f_inloop },
            cenv')
  | Hidden(fenv,cenv') ->
      Hidden(fenv,add_var x t cenv')
  | NoFrame -> NoFrame

(****************************************************************)
(* Look up an identifier in an environment and return its type. *)
(* Raise Not_found if the identifier is not in the environment. *)
(****************************************************************)
let rec lookup0 cenv id =
  match cenv with
    Outermost(fenv,globals) ->
      (* IGNORE LOCALS AND ARGS!! *)
      if id=fenv.f_name
      then FnType(fenv.f_ret_type,List.map snd fenv.f_args)
      else (try
        Dict.lookup globals id
      with Dict.Absent -> raise Not_found)
  | Frame(fenv,cenv') ->
      (* IGNORE LOCALS AND ARGS!! *)
      if id=fenv.f_name
      then FnType(fenv.f_ret_type,List.map snd fenv.f_args)
      else lookup0 cenv' id
  | Hidden(_,cenv') -> lookup0 cenv' id
  | NoFrame -> raise Not_found

let rec lookup cenv id =
  match cenv with
    Outermost(fenv,globals) ->
      begin
        try List.assoc id fenv.f_locals
        with Not_found ->
          try
            List.assoc id fenv.f_args
          with Not_found ->
            if id=fenv.f_name
            then FnType(fenv.f_ret_type,List.map snd fenv.f_args)
            else (try
              Dict.lookup globals id
            with Dict.Absent -> raise Not_found)
      end
  | Frame(fenv,cenv') ->
      begin
        try List.assoc id fenv.f_locals
        with Not_found ->
          try
            List.assoc id fenv.f_args
          with Not_found ->
            if id=fenv.f_name
            then FnType(fenv.f_ret_type,List.map snd fenv.f_args)
            else lookup0 cenv' id
      end
  | Hidden(_,cenv') -> lookup cenv' id
  | NoFrame -> raise Not_found

let rec inloop cenv =
  match cenv with
    Outermost(fenv,globals) -> fenv.f_inloop
  | Frame(fenv,cenv') -> fenv.f_inloop
  | Hidden(_,cenv') -> inloop cenv'
  | NoFrame -> false

let rec retType cenv =
  match cenv with
    Outermost(fenv,globals) -> fenv.f_ret_type
  | Frame(fenv,cenv') -> fenv.f_ret_type
  | Hidden(fenv,cenv') -> retType cenv'
  | NoFrame -> VoidType

let terr loc s = raise (X.CompilerError (X.Etypecheck (X.TypeError s),loc));;

let make_exp re = {exp_typ = None; raw_exp = re; exp_loc = L.none}

let possibly_null global_env n =
  (try (Dict.lookup global_env.structs n).st_possibly_null with
    Dict.Absent ->
      (try (Dict.lookup global_env.unions n).un_possibly_null with
	Dict.Absent ->
	  (try (Dict.lookup global_env.abstracts n) with
	    Dict.Absent -> false)))

let default_initializer env t loc = 
  begin
    let err() = terr loc ("declaration of type "^(typ2string t)
			  ^" requires initializer") in
    match t with
      IntType -> make_exp(Const(Int 0))
    | BooleanType -> make_exp(Const(Bool false))
    | StringType -> make_exp(Const(String ""))
    | NamedType n ->
	if possibly_null env n then
	  make_exp(Const(Null n))
	else err()
    | _ -> err()
  end

let rec check_valid_type loc global_env t =
  match t with
    ArrayType t -> check_valid_type loc global_env t
  | FnType(t,ts) -> check_valid_types loc global_env (t::ts)
  | NamedType n ->
      (try (Dict.lookup global_env.structs n; ()) with
	  Dict.Absent ->
	    (try (Dict.lookup global_env.unions n; ()) with
	      Dict.Absent ->
		(try (Dict.lookup global_env.abstracts n; ()) with
		  Dict.Absent -> terr loc ("bad type "^n))))
  | _ -> ()
and check_valid_types loc global_env ts =
  List.iter (check_valid_type loc global_env) ts

(*************************************************************************)
(* Check a statement to make sure it does a return rather than fall off  *)
(* the end without doing a return. This is a conservative approximation: *)
(* doesRet returns false for some statements that always do a return.    *)
(*                                                                       *)
(*   EXAMPLE:                              WE RETURN:      CONSERVATIVE? *)
(*   { return(5); 0; }                     true            no            *)
(*   while (1==2) return(5);               false           no            *)
(*   while (1<2) return(5);                false           yes           *)
(*   compile(int f()                                                     *)
(*           { suspend return(5); });      false           yes           *)
(*                                                                       *)
(*************************************************************************)
let rec doesRet (s,_) =
  match s with
    Skip -> false
  | Exp _ -> false
  | Seq(s1,s2) -> doesRet s1 or doesRet s2
  | Return _ -> true
  | IfThenElse(_,s1,s2) -> doesRet s1 & doesRet s2
  | While(e,s) -> false (* s may never execute *)
  | Break -> false
  | Continue -> false
  | For(e1,e2,e3,s) -> false (* s may never execute *)
  | IntSwitch(_,ss,s) ->
      (List.for_all (fun (_,s) -> doesRet s) ss) & (doesRet s)
  | CharSwitch(_,ss,s) ->
      (List.for_all (fun (_,s) -> doesRet s) ss) & (doesRet s)
  | UnionSwitch(_,ss,sopt) ->
      (List.for_all (fun (_,_,s) -> doesRet s) ss) &
      (match sopt with None -> true | Some s -> doesRet s)
  | Decl(_,_,_,s) -> doesRet s
  | Suspend s -> doesResRet s
  | Resume s -> false (* this will be a type error *)
  | Do(s,e) -> doesRet s
(**********************************************************************)
(* Check a statement to be sure that it does a resume followed by a   *)
(* return.  This is needed for the compile, suspend, resume, and hole *)
(* special forms.  Like doesRet, this is a conservative analysis.     *)
(**********************************************************************)
and doesResRet (s,_) =
  match s with
    Skip -> false
  | Exp _ -> false
  | Seq(s1,s2) -> doesResRet s1 or doesResRet s2
  | Return _ -> false (* return in the wrong context *)
  | IfThenElse(_,s1,s2) -> doesResRet s1 & doesResRet s2
  | While(e,s) -> false (* s may never execute *)
  | Break -> false
  | Continue -> false
  | For(e1,e2,e3,s) -> false (* s may never execute *)
  | IntSwitch(_,ss,s) ->
      (List.for_all (fun (_,s) -> doesResRet s) ss) & (doesResRet s)
  | CharSwitch(_,ss,s) ->
      (List.for_all (fun (_,s) -> doesResRet s) ss) & (doesResRet s)
  | UnionSwitch(_,ss,sopt) ->
      (List.for_all (fun (_,_,s) -> doesResRet s) ss) &
      (match sopt with None -> true | Some s -> doesResRet s)
  | Decl(_,_,_,s) -> doesResRet s
  | Suspend s -> false (* this will be a type error *)
  | Resume s -> doesRet s
  | Do(s,e) -> doesResRet s

let rec check_constexp e =
  begin  
    let loc = e.exp_loc in
    match e.raw_exp with
      Const _ -> ()
    | ConstArray (el,t) -> List.iter check_constexp el
    | NewStruct (tn,el) -> List.iter check_constexp el
    | NewUnion (tn,f,eo) ->
	(match eo with
	  None -> ()
	| Some e -> check_constexp e)
    | NewTuple (el) -> List.iter check_constexp el;
    | _ -> terr loc 
	  "Global variable initializer must be a constant expression."
  end
(**********************************************************************)
(* The following recursive function typecheck Stmts, Expressions, ... *)
(* given an initial environment.                                      *)
(**********************************************************************)
let rec tcStmt global_env env (s,loc) =
  begin
    let tcExp' e = tcExp global_env env e in
    let tcStmt' s = tcStmt global_env env s in
    match s with
    Skip -> ()
  | Exp e -> (tcExp' e; ())
  | Seq(s1,s2) -> (tcStmt' s1; tcStmt' s2)
  | Return(eopt) ->
      (match eopt,(retType env) with
	None,VoidType -> ()
      | None,t -> terr loc ("must return a value of type "^(typ2string t))
      | Some e,t ->
	  let t' = tcExp' e in
	  if eqtype t t' then () else
	  terr loc ("returns value of type "^(typ2string t')^" but requires "
		    ^(typ2string t)))
  | IfThenElse(e,s1,s2) ->
      (match tcExp' e with
	BooleanType -> (tcStmt' s1; tcStmt' s2)
      | t -> terr e.exp_loc ("if argument has type "^(typ2string t)
			     ^" instead of bool"))
  | While(e,s) ->
      (match tcExp' e with
	BooleanType -> tcStmt global_env (set_inloop env) s
      | t -> terr e.exp_loc ("while argument has type "^(typ2string t)
			     ^" instead of bool"))
  | Break ->
      if inloop env then () else terr loc "break not inside loop"
  | Continue ->
      if inloop env then () else terr loc "continue not inside loop"
  | For(e1,e2,e3,s) ->
      begin
	tcExp' e1;
	tcExp' e3;
	match tcExp' e2 with
	  BooleanType -> tcStmt global_env (set_inloop env) s
	| t -> terr e2.exp_loc ("2nd for argument has type "^(typ2string t)
				^" instead of bool")
      end
  | IntSwitch(e,ss,s) ->
      begin
	match tcExp' e with
	  IntType ->
	    let rec check_unique ss =
	      match ss with
		[] -> ()
	      | [_] -> ()
	      | (i1,_)::(((i2,_)::_) as rest) ->
		  if i1 = i2 then
		    terr loc ("switch has two cases for "^(string_of_int i1))
		  else check_unique rest in
	    let ss = Sort.list (fun (i1,s1) (i2,s2) -> (i1 <= i2)) ss in
	    begin
	      check_unique ss;
	      List.iter (fun (_,s) -> tcStmt' s) ss;
	      tcStmt' s
	    end
	| t -> terr loc ("switch has argument type "^(typ2string t)
			 ^" but int cases")
      end
  | CharSwitch(e,ss,s) ->
      begin
	match tcExp' e with
	  CharType ->
	    let rec check_unique ss =
	      match ss with
		[] -> ()
	      | [_] -> ()
	      | (i1,_)::(((i2,_)::_) as rest) ->
		  if i1 = i2 then
		    terr loc ("switch has two cases for "^(Char.escaped i1))
		  else check_unique rest in
	    let ss = Sort.list (fun (i1,s1) (i2,s2) -> (i1 <= i2)) ss in
	      begin
		check_unique ss;
		List.iter (fun (_,s) -> tcStmt' s) ss;
		tcStmt' s
	      end
	| t -> terr loc ("switch has argument type "^(typ2string t)
			 ^" but char cases")
      end
  | UnionSwitch(e,ss,def) ->
      begin
	let err t = terr loc ("switch has argument type "^(typ2string t)
			      ^" but union cases") in
	match tcExp' e with
	  NamedType u ->
	    (try
	      (let ud = Dict.lookup global_env.unions u in
	      let ss =
		Sort.list (fun (f1,x1,s1) (f2,x2,s2) -> f1 <= f2) ss in
	      let rec check_unique ss =
		match ss with
		  [] -> ()
		| [_] -> ()
		| (f1,_,_)::(((f2,_,_)::_) as rest) ->
		    if f1 = f2 then
		      terr loc ("switch has two cases for field "^f1)
		    else check_unique rest in
	      let rec check_complete fields =
		match fields with
		  [] -> ()
		| (f,_)::rest ->
		    if List.exists (fun (f',_,_) -> f = f') ss then
		      check_complete rest
		    else
		      terr loc ("switch missing case for field "^f) in
	      let rec check_exhaustive fields =
		List.for_all (fun f->List.exists (fun (f',_,_)->(fst f)=f') ss)
		  fields
	      in
	      let tc_arm (f,x,((_,loc') as s)) =
		let t =
		  (try List.assoc f ud.un_fields with
		    Not_found -> terr loc' ("bad switch field "^f)) in
		let env =
		  (match x,t with
		    None,VoidType -> env
		  | Some _,VoidType ->
		      terr loc' ("field "^f^" has type void")
		  | None,_ ->
			terr loc' ("field "^f^" has non-void type -- an identifier is required")
		    | Some x,t -> add_var x t env)
		  in tcStmt global_env env s in
		begin
		  check_unique ss;
		  List.iter tc_arm ss;
		  let exhaustive = check_exhaustive ud.un_fields in
		  (match def with
		    None ->
		      begin
			(if ud.un_possibly_null then
			  terr loc ("switch on ? type "^u^" requires default")
			else ());
			(if not exhaustive then
			  terr loc ("non-exhaustive switch requires default"));
			check_complete ud.un_fields
		      end
		  | Some s ->
		      begin
			tcStmt global_env env s;
			if ud.un_possibly_null then ()
			else if exhaustive then
			  terr loc ("switch has redundant default")
			else ()
		      end)
		end) with Dict.Absent -> err (NamedType u))
	  | t -> err t
	end
    | Decl(x,t,eopt,s) ->
	begin
	  let e =
	    (match !eopt with
	      None -> default_initializer global_env t loc
	    | Some e -> e)
	  in eopt := (Some e);
	  let t' = tcExp' e in
	  if eqtype t t' then
	    tcStmt global_env (add_var x t env) s
	  else
	    terr loc (x^" declared with type "^(typ2string t)
		      ^" but initializer has type "^(typ2string t'))
	end
    | Suspend s ->
        begin
          match env with
            Frame(fenv,cenv) -> tcStmt global_env (Hidden(fenv,cenv)) s
          | Hidden _ -> terr loc "can't suspend while compile is suspended"
          | Outermost _ | NoFrame -> 
	      terr loc "suspend can only be used within compile"
        end
    | Resume s ->
        begin
          match env with
            Hidden(fenv,cenv) -> tcStmt global_env (Frame(fenv,cenv)) s
          | Frame _ -> terr loc "can't resume while already in compile"
          | Outermost _ | NoFrame -> 
	      terr loc "resume can only be used within suspend"
        end
    | Do(s,e) ->
	(match tcExp' e with
	  BooleanType -> tcStmt global_env (set_inloop env) s
	| t -> terr e.exp_loc ("do-while guard has type "^(typ2string t)
			       ^" instead of bool"))
  end(* end of tcStmt *)
and tcExp global_env env exp =
  begin
    let e = exp.raw_exp in
    let loc = exp.exp_loc in
    let tcExp' e = tcExp global_env env e in
    let t =
      begin
	match e with
	  Const(Int _) -> IntType
	| Const(Bool _) -> BooleanType
	| Const(String _) -> StringType
	| Const(Char _) -> CharType
	| Const(Null n) ->
	    if possibly_null global_env n then NamedType n
	    else terr loc ("null not valid for type "^n)
	| ConstArray([],Some t) ->
	    (check_valid_type loc global_env t; ArrayType t)
	| ConstArray([],None) ->
	    terr loc "empty array has no type"
	| ConstArray((e1::rest) as es,_) ->
	    begin
	      let t = tcExp' e1 in
	      let rec aux es =
		(match es with
		  [] -> ()
		| (e::rest) ->
		    if eqtype t (tcExp' e) then aux rest
		    else terr e.exp_loc "type mismatch in array constant")
	      in
	      aux rest;
	      ArrayType t
	    end
	| Var x ->
	    (try lookup env x with
	      Not_found -> terr loc ("unbound variable "^x))
	| Primop(p,[e1;e2]) ->
	    let t1 = tcExp' e1 in
	    let t2 = tcExp' e2 in
	    tcBinPrimop env loc p t1 t2
	| Primop(p,[e]) ->
	    let t1 = tcExp' e in
	    tcUnPrimop env loc p t1
	| Primop(_,_) -> terr loc "primop wrong # of args"
	| Conditional(e1,e2,e3) ->
	    (match tcExp' e1 with
	      BooleanType ->
		let t2 = tcExp' e2 in
		let t3 = tcExp' e3 in
		if eqtype t2 t3 then t2 else
		terr loc ("clauses of conditional do not match type: "
			  ^(typ2string t2)^" != "^(typ2string t3))
	    | t -> terr loc ("conditional argument has type "^(typ2string t)
			     ^"instead of bool"))
	| Assign(e1,e2) ->
	    let t1 = tcExp' e1 in
	    let t2 = tcExp' e2 in
	    (check_valid_lhs global_env e1;
	     if eqtype t1 t2 then t2 else
	     terr loc ("assignment type mismatch: "^(typ2string t1)^" != "
		       ^(typ2string t2)))
	| AssignOp(e1,p,e2) ->
	    let t1 = tcExp' e1 in
	    let t2 = tcExp' e2 in
	    (check_valid_lhs global_env e1;
	     let t_result = tcBinPrimop env loc p t1 t2 in
	     if eqtype t_result t1 then t_result
	     else terr loc "Cannot use this operator in front of an assignment.")
	| FunCall(e,es) ->
	    let t = tcExp' e in
	    (match t with
	      FnType(rt,argts) ->
		(try
		  (List.iter2
		     (fun e t ->
		       let t' = tcExp' e in
		       if eqtype t' t then () else
		       terr e.exp_loc ("argument type mismatch.  "^
				       "actual has type "
				       ^(typ2string t')^" but formal has type "
				       ^(typ2string t))) es argts); rt
		    with Invalid_argument _ ->
		      terr loc "argument number mismatch")
	    | t -> terr loc ("attempt to apply non function type "
			     ^(typ2string t)))
	| NewStruct(n,es) ->
	    (try
	      begin
	      	let sd = Dict.lookup global_env.structs n in
	      	let checkexp e (f,_,t) =
		  let t' = tcExp' e in
		  if eqtype t' t then () else
		  terr e.exp_loc
		    ("struct "^n^", field "^f^" has type "^(typ2string t)^
		     " but argument has type "^(typ2string t')) in
	      	List.iter2 checkexp es sd.st_fields; NamedType n
	      end
	    with
	      Dict.Absent -> terr loc (n^" not a struct")
	    | Invalid_argument _ ->
		terr loc ("struct "^n^" argument # mismatch"))
	| StructMember(e,f) ->
	    (match tcExp' e with
	      NamedType n ->
		(try
		  let rec aux fs =
		    match fs with
		      ((f',_,t)::rest) ->
		    	if f = f' then t else aux rest
		    | [] -> terr loc ("struct "^n^" has no "^f^" field")
		  in aux (Dict.lookup global_env.structs n).st_fields
		with
		  Dict.Absent -> terr loc (n^" not a struct"))
	    | t -> terr loc ((typ2string t)^" not a struct"))
	| NewUnion(n,f,eopt) ->
	    let rty = NamedType n in
	    (try
	      let ud = Dict.lookup global_env.unions n in
	      let t = List.assoc f ud.un_fields in
	      (match t,eopt with
		VoidType,None -> rty
	      |	_,None ->
		  terr loc ("union "^n^", field "^f^
			    " requires argument of type "^(typ2string t))
	      |	_,Some e ->
		  begin
		    let t' = tcExp' e in
		    if eqtype t' t then rty else
		    terr loc ("union "^n^", field "^f^
			      " requires argument of type "^(typ2string t)^
			      " not "^(typ2string t'))
		  end)
	    with
	      Dict.Absent -> terr loc (n^" not a union")
	    | Not_found ->
		terr loc ("union "^n^" has no "^f^" field"))
	| NewTuple(es) -> TupleType(List.map tcExp' es)
	| TupleMember(e,i) ->
	    (match tcExp' e with
	      TupleType ts ->
		(try List.nth ts (i - 1) with
		  Failure _ ->
		    terr loc ("tuple has "^(string_of_int (List.length ts))^
			      " fields"))
	    | t -> terr loc ("tuple projection applied to "^(typ2string t)^
			     " value"))
	| Subscript(e1,e2) ->
	    let t1 = tcExp' e1 in
	    let t2 = tcExp' e2 in
	    (match t1,t2 with
	      ArrayType t,IntType -> t
	    | StringType,IntType -> CharType
	    | _,IntType ->
		terr e1.exp_loc
		  ("subscript on non-array/string type "^(typ2string t1))
	    | _,_ ->
		terr e2.exp_loc
		  ("subscript type "^(typ2string t2)^" not an int"))
	| NewArray(e1,e2) ->
	    let t2 = tcExp' e2 in
	    (match tcExp' e1 with
	      IntType -> ArrayType t2
	    | t -> terr loc ((typ2string t)^" not an int"))
        | Compile fd ->
            let env' = Frame({ f_name = fd.fn_name;
                               f_args = fd.fn_args;
                               f_ret_type = fd.fn_ret_type;
                               f_locals = [];
                               f_inloop = false },
		             env) in
            tcFunDecl global_env env' loc fd;
            FnType(fd.fn_ret_type,List.map snd fd.fn_args)
        | Hole e ->
            begin
              match env with
                Frame(fenv,cenv) -> tcExp global_env (Hidden(fenv,cenv)) e
              | Hidden _ ->
                  terr loc "hole cannot be used while compile is suspended"
              | Outermost _ | NoFrame -> 
		  terr loc "hole can only be used within compile"
            end
      end
    in (exp.exp_typ <- Some t; t)
  end (* end of tcExp *)
and tcBinPrimop env loc p t1 t2 =
  begin
    match p with
      (Plus | Times | Minus | Div | Mod | Bitand | Bitor | Bitxor |
       Bitlshift | Bitlrshift | Bitarshift) ->
	(match t1,t2 with
	  IntType,IntType -> IntType
	| _ -> terr loc "primop arguments not ints")
    | (Gt | Lt | Gte | Lte) ->
	(match t1,t2 with
	  IntType,IntType -> BooleanType
	| _ -> terr loc "primop arguments not ints")
    | (Eq | Neq) ->
	if eqtype t1 t2 then BooleanType
	else terr loc ("comparison of two types: "^(typ2string t1)^" != "
		       ^(typ2string t2))
    | _ -> terr loc ("wrong # of args to primop")
  end
and tcUnPrimop env loc p t =
  begin
    match (p,t) with
      (Not,BooleanType) -> BooleanType
    | (Not,_) -> terr loc ("! requires bool")
    | (Bitnot,IntType) -> IntType
    | (Bitnot,_) -> terr loc ("bit negation requires int")
    | (Size,StringType) -> IntType
    | (Size,ArrayType _) -> IntType
    | (Size,_) -> terr loc ("size requires string or array")
    | (Ord,CharType) -> IntType
    | (Ord,_) -> terr loc ("ord requires a char")
    | (Chr,IntType) -> CharType
    | (Chr,_) -> terr loc ("chr require an int")
    | _ -> terr loc "wrong # of args for primop"
  end
and check_valid_lhs global_env e =
  begin
    match e.raw_exp with
      Var _ -> ()
    | StructMember(e1,f) ->
	(match e1.exp_typ with
	  Some(NamedType n) ->
	    let rec aux fs =
	      match fs with
		((f',rw,_)::rest) ->
		  if f = f' then
		    (match rw with
		      ReadWrite -> ()
		    | ReadOnly -> terr e.exp_loc ("field "^f^" is const"))
		  else aux rest
	      |	[] -> failwith "field lookup"
	    in aux (Dict.lookup global_env.structs n).st_fields
	| _ -> failwith "type lookup")
    | Subscript(e1,e2) ->
	(match e1.exp_typ with
	  Some(StringType) ->
	    terr e.exp_loc ("update not allowed on strings")
	| Some(ArrayType t) -> ()
	| _ -> failwith "type lookup2")
    | _ -> terr e.exp_loc "not a valid left-hand-side"
  end
and tcFunDecl global_env env loc fd =
  begin
    check_valid_type loc global_env fd.fn_ret_type;
    List.iter (fun (_,t) -> check_valid_type loc global_env t) fd.fn_args;
    
    if fd.fn_ret_type <> VoidType & not(doesRet fd.fn_body)
    then terr loc ("function body must return a value of type "^
		   (typ2string fd.fn_ret_type));
    tcStmt global_env env fd.fn_body
  end
(* end of tcFunDecl *)

let add_global_env ((structs, unions, abstracts, globals) as e) (d,loc) =
  let check_duplicate n =
    (if (Dict.member structs n) or (Dict.member unions n) or
      (Dict.member abstracts n) then
      terr loc ("duplicate type name "^n)
    else ()) in
  let check_duplicate_globals v =
    (if Dict.member globals v then
      terr loc ("duplicate global name "^v)
    else ()) in
  match d with
    StructDecl sd ->
      check_duplicate sd.st_name;
      (Dict.insert structs sd.st_name sd, unions, abstracts, globals)
  | UnionDecl ud ->
      check_duplicate ud.un_name;
      (structs, Dict.insert unions ud.un_name ud, abstracts, globals)
  | ExternType (n,b) ->
      check_duplicate n;
      (structs,unions,Dict.insert abstracts n b, globals)
  | ExternFun (t,v,ts) ->
      (structs,unions,abstracts,Dict.insert globals v (FnType(t,ts)))
  | FunDecl fd ->
      let v = fd.fn_name in
      let t = FnType(fd.fn_ret_type,List.map snd fd.fn_args) in
      (structs,unions,abstracts,Dict.insert globals v t)
  | ExternVal (v,t) -> (structs,unions,abstracts,Dict.insert globals v t)
  | GlobalDecl (s,v,t,eor) -> 
      (structs,unions,abstracts,Dict.insert globals v t)

let initial_global_env ds =
  let e_s = Dict.empty compare in
  let e_u = Dict.empty compare in
  let e_a = Dict.empty compare in
  let e_g = Dict.empty compare in
  let (s,u,a,g) = List.fold_left add_global_env (e_s,e_u,e_a,e_g) ds in
  { structs = s; unions = u; abstracts = a; globals = g }

let rec check_fundecl global_env loc fd =
  let env = Outermost({ f_name = fd.fn_name;
                        f_args = fd.fn_args;
                        f_ret_type = fd.fn_ret_type;
                        f_locals = [];
                        f_inloop = false },
		      global_env.globals) in
  tcFunDecl global_env env loc fd

let check_structdecl global_env loc sd =
  begin
    List.iter (fun (_,_,t) -> check_valid_type loc global_env t) sd.st_fields
  end

let check_uniondecl global_env loc ud =
  begin
    List.iter (fun (_,t) -> check_valid_type loc global_env t) ud.un_fields
  end

let check_globaldecl loc global_env (s,v,t,eor) =
  begin
    check_valid_type loc global_env t;
    let e = 
      match !eor with
	None -> default_initializer global_env t loc
      |	Some e ->
	  begin
	    let env = NoFrame in
	    check_constexp e;
	    let t' = tcExp global_env env e in
	    if eqtype t t' then e
	    else 
	      (terr loc 
		 ("The type of the initializer (" 
		  ^ (typ2string t')
		  ^ ") does not match the declared type (" 
		  ^ typ2string t ^")."))
	  end in
    eor := Some(e);    
  end
let check_decl global_env (d,loc) =
  match d with
    FunDecl fd -> check_fundecl global_env loc fd
  | StructDecl sd -> check_structdecl global_env loc sd
  | UnionDecl ud -> check_uniondecl global_env loc ud
  | ExternFun (t,_,ts) -> check_valid_types loc global_env (t::ts)
  | ExternType _ -> ()
  | ExternVal (v,t) -> check_valid_type loc global_env t
  | GlobalDecl d -> check_globaldecl loc global_env d

let check_decls ds =
  let global_env = initial_global_env ds in
  List.iter (check_decl global_env) ds;
  (ds,global_env)

let type_check ds = check_decls ds;;

