(**********************************************************************)
(* (c) Greg Morrisett, Neal Glew, Chris Hawblitzel, Frederick Smith   *)
(*     June 1998, all rights reserved.                                *)
(**********************************************************************)

(* Breaking news:
   We now support prefix but open is broken.

   Prefixes:  All prefixes in declarations are eliminated by a pre-pass.
   The use of prefixes is eliminated by the parser for types, and by the
   type-checker for expressions.

   Current support for open:
      The name in P.NamedType is now a ref so that we can update types with
      their complete names.
   (After type-checking only complete names should remain.  The code generator does not and should not know about open.)
      Name lookups all check in the local environment, and the unprefixed global environment.  If that fails we successively try the open prefixes in LIFO order.

   The problem with open is the following:
   The current type-checker works as follows:
   1. Put all top-level declarations into the global_env
   2. Check that each top-level decl is well-formed/typed.

   In the presence of open (1) fails, because we insert types with
   incomplete names into the environment.  For example,
       prefix List {
        open List;
        struct <'a>t { 'a hd; <'a>t tl; }
        int length<'a>(<'a>t);
      }
   length gets inserted with type
             <'a>.<'a>t -> int NOT <'a>.<'a>List::t->int
   during (1), and type checking fails later when List has been closed and
   we cannot find t.  Worse, the struct t (correctly) has name List::t but
   the field tl gets inserted with type t NOT List::t.

The unfortunate solution to all these problems is to add an additional step.
   1. Record all type names in scope at the top level.
   2. Build the top-level environment adjusting all types based on the names in
   scope and open-prefixes.
   3. Type check the top-decls, keeping track of open_prefixes.
*)
(* Latest news:  I've changed things radically to support polymorphism,
 * exceptions, and a bit of type-inference.  In particular, we use
 * a simple form of local type inference (involving unification) to
 * type-check.  I commented out Cyclone-specific code and outright
 * removed the Cyclone-environment stuff to simplify things for now.
 *
 * Still need to verify that values do not have types that are not
 * exported (i.e., types that are not static.)
 *)

open Numtypes
open Popsyntax

exception Unimplemented
exception UnboundVar of (var*location)

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

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

let set_inloop fenv  = { fenv with f_inloop = true };;
let add_var x t fenv = { fenv with f_locals = (x,t)::fenv.f_locals };;

exception Unbound

(* Takes a name and a function defined : var -> bool.  Tests all open_prefixes
   looking for a defined instance and returns the completed name.
   e.g. complete_name global_env (is this a struct?) "x"
   where "foo" and "bar" are open prefixes will test successively
   x, foo.x, and then foo.bar, raising unbound if none of these is "defined"
*)
let complete_name global_env defined n =
  if defined n then n else
  let rec aux prefixes =
    match prefixes with
      hd::tl ->
	let n' = add_prefix hd n in
	if defined n' then n' else aux tl
    | [] -> raise Unbound
  in
  aux global_env.open_prefixes

let inloop f_env  = f_env.f_inloop;;
let retType f_env = f_env.f_ret_type;;
let terr loc s =
    let e = Poperr.Etypecheck (Poperr.TypeError s) in
    let e = Gcdfec.mk_err_elab loc (Poperr.error_message e) in
    Gcdfec.post_error e
let tyvars fenv = fenv.f_tyvars
let mk_env fenv = fenv
let lookup fenv id = List.assoc id fenv.f_locals

(* Cyclone *)

(****************************************************************)
(* We define Cyclone environments, and redefine functions that  *)
(* depend on the representation of environments.                *)
(*                                                              *)
(* A version of poptype without Cyclone support can be          *)
(* recovered simply by commenting out this code, and subsequent *)
(* code marked CYCLONE.                                         *)
(*                                                              *)
(* VARIABLE CONVENTIONS: fenv is used to name f_env's, cenv is  *)
(* used to name c_env's, and env is used where it could be      *)
(* either (depending on whether the Cyclone code is commented   *)
(* out).  Global environments are always named by global_env.   *)
(****************************************************************)
type c_env =
    Outermost of f_env
  | Frame of f_env * c_env
  | Hidden of f_env * c_env

let rec fenv_of_cenv cenv =
  match cenv with
    Outermost fenv -> fenv
  | Frame(fenv,_) -> fenv
  | Hidden(_,cenv) -> fenv_of_cenv cenv

let rec put_fenv cenv fenv =
  match cenv with
    Outermost _ -> Outermost fenv
  | Frame(_,cenv) -> Frame(fenv,cenv)
  | Hidden(fenv',cenv) -> Hidden(fenv',put_fenv cenv fenv)

let set_inloop cenv =
  put_fenv cenv (set_inloop(fenv_of_cenv cenv))

let add_var x t cenv =
  put_fenv cenv (add_var x t (fenv_of_cenv cenv))

let lookup cenv id =
  (********************************************************************)
  (* Special case for Cyclone: if we are looking up a function, we    *)
  (* need to look in the frame.  All Popcorn functions are outermost, *)
  (* and their types are given in the global environment as well as   *)
  (* the frame.  In Cyclone, an inner function won't be in the        *)
  (* global environment.                                              *)
  (********************************************************************)
  let fenv = fenv_of_cenv cenv in
  if fenv.f_name = id then
    FnType(fenv.f_tyvars,fenv.f_ret_type,List.map snd fenv.f_args)
  else lookup fenv id

let inloop cenv = inloop (fenv_of_cenv cenv)

let tyvars cenv = tyvars (fenv_of_cenv cenv)

let retType cenv = retType (fenv_of_cenv cenv)

let mk_env fenv = Outermost fenv

let set_outloop fenv =
  { f_name = fenv.f_name;
    f_tyvars = fenv.f_tyvars;
    f_args = fenv.f_args;
    f_ret_type = fenv.f_ret_type;
    f_locals = fenv.f_locals;
    f_inloop = false;
  }

let set_outloop cenv =
  put_fenv cenv (set_outloop(fenv_of_cenv cenv))

(* End Cyclone *)



(* returns true if the type constructor n can is a ? type *)
let possibly_null global_env n =
  (try (Dict.lookup global_env.structs n).st_possibly_null with
    Dict.Absent ->
      (try snd (Dict.lookup global_env.abstracts n) with
	Dict.Absent -> false))

(* returns the default initialization expression for a type t (if any) *)
let default_initializer global_env t loc =
  begin
    let err() = terr loc ("declaration of type "^(typ2string t)
			  ^" requires initializer") in
    let raise_err () = err (); raise Gcdfec.Exit in
    let make_exp re = { exp_typ = None; raw_exp = re; exp_loc = loc } in
    match t with
      IntType -> make_exp(Const(Int i32_0))
    | BooleanType -> make_exp(Const(Bool false))
    | StringType -> make_exp(Const(String ""))
    | NamedType (n,_) ->
	let n = !n in
	if not (possibly_null global_env n) then err ();
	make_exp(Const(Null))
    | _ -> raise_err ()
  end

(* checks that t is a valid type in the current global environment.
 * The set of VarType's must be drawn from tyvars.
 *)
let rec check_valid_type loc global_env (tyvars:var list) t =
  let err s = terr loc s in
  let raise_err s = err s; raise Gcdfec.Exit in
  match t with
    ArrayType t -> check_valid_type loc global_env tyvars t
  | FnType(vs,t,ts) -> check_valid_types loc global_env (vs@tyvars) (t::ts)
  | NamedType(n,ts) ->
      check_valid_types loc global_env tyvars ts;
      let defined name =
	(Dict.member global_env.structs name ||
	 Dict.member global_env.unions name ||
	 Dict.member global_env.abstracts name)
      in
      n :=
	 begin try
	   complete_name global_env defined !n
	 with Unbound -> raise_err ("bad type "^ !n)
	 end;
      let vs =
      	(try (Dict.lookup global_env.structs !n).st_tyvars with
	  Dict.Absent ->
	    (try (Dict.lookup global_env.unions !n).un_tyvars with
	      Dict.Absent ->
		(try fst (Dict.lookup global_env.abstracts !n) with
		  Dict.Absent -> raise_err ("bad type "^ !n))))
      in if (List.length vs) = (List.length ts) then ()
      else raise_err ("wrong # of type arguments for "^ !n)
  (* Evar and OptionEvar should only occur as pointers to other actual
   * types -- in fact, they shouldn't occur at all but what the hell.
   *)
  | Evar r ->
      (match !r with
	Some t -> check_valid_type loc global_env tyvars t
      |	_ -> raise_err "free existentially-bound variable!")
  | OptionEvar r ->
      (match !r with
	Some t -> check_valid_type loc global_env tyvars t
      |	_ -> raise_err "free existentially-bound ? variable!")
  | VarType v ->
      if List.mem v tyvars then () else
      raise_err ("free type variable #"^v)
  | _ -> ()
and check_valid_types loc global_env (tyvars:var list) ts =
  List.iter (check_valid_type loc global_env tyvars) 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           *)
(*   codegen(int f()                                                     *)
(*           { cut return(5); });          false           yes           *)
(*                                                                       *)
(*************************************************************************)
let rec doesRet (s,_) =
  match s with
    Skip -> false
  | Exp e ->
      begin match e.raw_exp with
	Raise _ -> true
      |	_ -> false
      end
  | 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 -> true (* FMS : Changed to true. *)
  | 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
  | Do(s,e) -> doesRet s
  | Try(s1,_,s2) -> doesRet s1 & doesRet s2
(* Cyclone *)
  | Cut s -> doesSpliceRet s
  | Splice s -> false (* this will be a type error *)
(**********************************************************************)
(* Check a statement to be sure that it does a splice followed by a   *)
(* return.  This is needed for the codegen, cut, splice, and fill     *)
(* special forms.  Like doesRet, this is a conservative analysis.     *)
(**********************************************************************)
and doesSpliceRet (s,_) =
  match s with
    Skip -> false
  | Exp _ -> false
  | Seq(s1,s2) -> doesSpliceRet s1 or doesSpliceRet s2
  | Return _ -> false (* return in the wrong context *)
  | IfThenElse(_,s1,s2) -> doesSpliceRet s1 & doesSpliceRet 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) -> doesSpliceRet s) ss) & (doesSpliceRet s)
  | CharSwitch(_,ss,s) ->
      (List.for_all (fun (_,s) -> doesSpliceRet s) ss) & (doesSpliceRet s)
  | UnionSwitch(_,ss,sopt) ->
      (List.for_all (fun (_,_,s) -> doesSpliceRet s) ss) &
      (match sopt with None -> true | Some s -> doesSpliceRet s)
  | Decl(_,_,_,s) -> doesSpliceRet s
  | Cut s -> false (* this will be a type error *)
  | Splice s -> doesRet s
  | Do(s,e) -> doesSpliceRet s
  | Try(s1,_,s2) -> doesSpliceRet s1 & doesSpliceRet s2
(* End Cyclone *)
let rec subst inst t =
  match t with
    VarType v ->
      (try List.assoc v inst with Not_found -> t)
  | ArrayType t -> ArrayType(subst inst t)
  | FnType(vs,t,ts) ->
      let inst = (List.map (fun v -> (v,VarType v)) vs) @ inst in
      FnType(vs,subst inst t,substs inst ts)
  | TupleType ts -> TupleType(substs inst ts)
  | NamedType(n,ts) -> NamedType(n,substs inst ts)
  | _ -> t
and substs inst ts = List.map (subst inst) ts

(* Do path compression on Evar's and OptionEvar's so that they point
 * directly to the defined type (if any).
 *)
let rec compress t =
  match t with
    Evar r ->
      (match !r with
	None -> t
      | Some t' ->
	  (compress t'; r := Some t'; t'))
  | OptionEvar r ->
      (match !r with
	None -> t
      | Some t' ->
	  (compress t'; r := Some t'; t'))
  | _ -> t

(* Returns true if t1 and t2 unify, false otherwise.  Is destructive so
 * not suitable for backtracking.
 *)
exception Unify
let unify global_env t1 t2 =
  (* check to see if an Evar or OptionEvar occurs in a type, raising
   * Unify if so. *)
  let rec occurs r t =
    match t with
      Evar r' -> if r = r' then raise Unify else ()
    | OptionEvar r' -> if r = r' then raise Unify else ()
    | ArrayType t -> occurs r t
    | FnType(_,t,ts) -> occurslist r (t::ts)
    | TupleType ts -> occurslist r ts
    | NamedType(_,ts) -> occurslist r ts
    | _ -> ()
  and occurslist r ts =
    match ts with
      [] -> ()
    | t::ts -> occurs r t; occurslist r ts in
  (* inner loop of unify -- raises Unify if the two types do not unify. *)
  let rec un t1 t2 =
    (* compress the types to get rid of any indirection *)
    let t1 = compress t1 in
    let t2 = compress t2 in
    (* check for structural/physical equality.  This is the common case and
     * in particular, succeeds when we have the same refs for Evars or
     * OptionEvars.
     *)
    if t1 = t2 then () else
    match t1,t2 with
      Evar r1,_ ->
	(match !r1 with
	  (* this case shouldn't really happen due to compression *)
	  Some t1' -> un t1' t2
	  (* as long as r1 doesn't occur in t2, set r1 to t2 *)
	| None -> occurs r1 t2; r1 := (Some t2))
    | _,Evar _ -> un t2 t1
    | OptionEvar r1,_ ->
	(* similar to Evar, but we can only unify r1 with other OptionEvar's
	 * or named types that are possibly null. *)
	(match !r1 with
	  Some t1' -> un t1' t2
	| None ->
	    (match t2 with
	      OptionEvar _ -> r1 := (Some t2)
	    | NamedType(tn,ts) ->
		let tn = !tn in
		if possibly_null global_env tn then r1 := (Some t2)
		else raise Unify
	    | _ -> raise Unify))
    | _,OptionEvar r2 -> un t2 t1
    | ArrayType t1,ArrayType t2 -> un t1 t2
    | FnType([],t1,ts1),FnType([],t2,ts2) -> uns (t1::ts1) (t2::ts2)
    | FnType(vs1,t1,ts1),FnType(vs2,t2,ts2) ->
	let inst = List.combine vs1 (List.map (fun v -> VarType v) vs2) in
	uns (t1::ts1) (substs inst (t2::ts2))
    | TupleType(ts1),TupleType(ts2) -> uns ts1 ts2
    | NamedType(tn1,ts1),NamedType(tn2,ts2) ->
	if !tn1 = !tn2 then uns ts1 ts2 else raise Unify
    | VarType(x),VarType(y) -> if x = y then () else raise Unify
    | _,_ -> raise Unify
  and uns ts1 ts2 =
    match ts1, ts2 with
      [],[] -> ()
    | t1::ts1,t2::ts2 -> un t1 t2; uns ts1 ts2
    | _,_ -> raise Unify
  in try un t1 t2; true with Unify -> false
;;

(* check that an expression, used for initialization of globals, is
 * "constant" (i.e., can be computed at compile time.)
 *)
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 a global environment and an initial function 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
    let unify = unify global_env 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 not (unify t t') then
	    terr loc ("returns value of type "^(typ2string t')^" but requires "
		      ^(typ2string t)))
  | IfThenElse(e,s1,s2) ->
      let t = tcExp' e in
      if not (unify BooleanType (tcExp' e))
      then terr e.exp_loc ("if argument has type "^(typ2string t)
			   ^" instead of bool");
      tcStmt' s1;
      tcStmt' s2
  | While(e,s) ->
      let t = tcExp' e in
      if not (unify BooleanType (tcExp' e))
      then terr e.exp_loc ("while argument has type "^(typ2string t)
			   ^" instead of bool");
      tcStmt global_env (set_inloop env) s
  | Break ->
      if not (inloop env) then terr loc "break not inside loop"
  | Continue ->
      if not (inloop env) then terr loc "continue not inside loop"
  | For(e1,e2,e3,s) ->
      begin
	tcExp' e1;
	tcExp' e3;
	let t = tcExp' e2 in
	if not (unify BooleanType t)
	then terr e2.exp_loc ("2nd for argument has type "^(typ2string t)
			      ^" instead of bool");
	tcStmt global_env (set_inloop env) s
      end
  | IntSwitch(e,ss,s) ->
      begin
	let t = tcExp' e in
	if not (unify IntType t)
	then terr loc ("switch has argument type "^(typ2string t)
		       ^" but int cases");
	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_int32 i1));
		 raise Gcdfec.Exit)
	      else check_unique rest in
	let ss = Sort.list (fun (i1,s1) (i2,s2) -> (i1 <=$ i2)) ss in
	check_unique ss;
	List.iter (fun (_,s) -> tcStmt' s) ss;
	tcStmt' s
      end
  | CharSwitch(e,ss,s) ->
      begin
	let t = tcExp' e in
	if not (unify CharType t)
	then terr loc ("switch has argument type "^(typ2string t)
		       ^" but char cases");
	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
      end
  | UnionSwitch(e,ss,def) ->
      (* UnionSwitch's can actually be one of two things:  a switch on a
       * union value or a switch on an exn value.  We can't tell
       *syntactically. *)
      begin
	let err t = terr loc ("switch has argument type "^(typ2string t)
			      ^" but union cases") in
	match compress (tcExp' e) with
	  NamedType(u,ts) ->
	    (try
	      let u = !u in
	      (let ud = Dict.lookup global_env.unions u in
	      (* compute instantiation for union type *)
	      let inst = List.combine ud.un_tyvars ts in
	      (* sort statements by data constructor name *)
	      let ss =
		Sort.list (fun (f1,x1,s1) (f2,x2,s2) -> f1 <= f2) ss in
	      (* check for duplicate cases -- assumes sorted cases *)
	      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
	      (* find missing field for error message *)
	      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
	      (* check that fields are complete -- assumes default is empty *)
	      let rec check_exhaustive fields =
		List.for_all (fun f->List.exists (fun (f',_,_)->(fst f)=f') ss)
		  fields
	      in
	      (* type-check a clause of the switch *)
	      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);
		      raise Gcdfec.Exit) in
		(* add x to the environment with the type asssociated with f.
		 * if f has VoidType then x shouldn't really be there. *)
		let env =
		  (match x,t with
		    None,VoidType -> env
		  | Some _,VoidType ->
		      terr loc' ("field "^f^" has type void");
		      raise Gcdfec.Exit
		  | None,_ ->
		      terr loc' ("field "^f^" has non-void type -- an identifier is required");
		      env
		    | Some x,t -> add_var x (subst inst 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");
			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 not ud.un_possibly_null & exhaustive then
			  terr loc ("switch has redundant default")
		      end)
		end) with Dict.Absent -> err (NamedType(u,[])))
	(* the switch is really an exception switch *)
	| ExnType ->
	    (* sort the cases by exn name *)
	    let ss = Sort.list (fun (f1,x1,s1) (f2,x2,s2) -> f1 <= f2) ss in
	    (* check that the cases are unique *)
	    let rec check_unique ss =
	      match ss with
		[] -> ()
	      |	[_] -> ()
	      |	(f1,_,_)::(((f2,_,_)::_) as rest) ->
		  if f1 = f2 then
		    (terr loc ("exn switch has two cases for exn "^f1);
		     raise Gcdfec.Exit)
		  else check_unique rest in
	    (* check a case, adding x to the environment with the appropriate
	     * type.  If the exception f carries void, then x shouldn't
	     * really be there. *)
	    let tc_arm (f,x,((_,loc') as s)) =
	      let t =
		(try Dict.lookup global_env.exceptions f with
		  Dict.Absent ->
		    terr loc' ("unknown exception "^f);
		    raise Gcdfec.Exit) in
	      let env =
		(match x,t with
		  None,VoidType -> env
		| Some _,VoidType ->
		    terr loc' ("exception "^f^" carries no type");
		    env
		| None,_ ->
		    terr loc' ("exception "^f^" has non-void type -- an identifier is required");
		    env
		| Some x,t -> add_var x t env)
	      in tcStmt global_env env s in
	    begin
	      check_unique ss;
	      List.iter tc_arm ss;
	      (match def with
		None ->
		  terr loc ("exception switch requires default");
		  raise Gcdfec.Exit
	      |	Some s -> tcStmt global_env env s)
	    end
	| 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
	  check_valid_type loc global_env (tyvars env) t;
(* We need to check that t is valid because this function will expand type names in t with the appropriate prefixes *)
	  if not (unify t t')
	  then terr loc (x^" declared with type "^(typ2string t)
			 ^" but initializer has type "^(typ2string t'));
	  tcStmt global_env (add_var x t env) s
	end
(* Cyclone *)
    | Cut s ->
        begin
          match env with
            Frame(fenv,cenv) ->
              (* set_outloop to prevent break/continue across cut *)
              tcStmt global_env (set_outloop(Hidden(fenv,cenv))) s
          | Hidden _ -> terr loc "can't cut while codegen is in cut"
          | Outermost _ ->
	      terr loc "cut can only be used within codegen"
        end
    | Splice s ->
        begin
          match env with
            Hidden(fenv,cenv) ->
              (* set_outloop to prevent break/continue across splice *)
              tcStmt global_env (set_outloop(Frame(fenv,cenv))) s
          | Frame _ -> terr loc "can't splice while already in codegen"
          | Outermost _ ->
	      terr loc "splice can only be used within cut"
        end
(* End Cyclone *)
    | Do(s,e) ->
	let t = tcExp' e in
	if not (unify BooleanType t)
	then terr e.exp_loc ("do-while guard has type "^(typ2string t)
			     ^" instead of bool");
	tcStmt global_env (set_inloop env) s
    | Try(s1,x,s2) ->
	begin
	  tcStmt' s1;
	  tcStmt global_env (add_var x ExnType env) s2
	end
  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 unify = unify global_env in
    let unify_un t1 t2 = (unify t1 t2; ()) in
    let t =
      begin
	match e with
	  Const(Int _) -> IntType
	| Const(Bool _) -> BooleanType
	| Const(String _) -> StringType
	| Const(Char _) -> CharType
	| Const(Null) -> OptionEvar(ref None)

	| ConstArray([],Some t) ->
	    (check_valid_type loc global_env (tyvars env) t; ArrayType t)
	| ConstArray([],None) ->
	    terr loc "empty array has no type"; raise Gcdfec.Exit
	| ConstArray((e1::rest) as es,_) ->
	    begin
	      let t = tcExp' e1 in
	      let rec aux es =
		(match es with
		  [] -> ()
		| (e::rest) ->
		    if unify t (tcExp' e) then aux rest
		    else (terr e.exp_loc "type mismatch in array constant";
			  raise Gcdfec.Exit))
	      in
	      aux rest;
	      ArrayType t
	    end
	| Var x ->
	    begin try lookup env x
	    with Not_found -> try (Dict.lookup global_env.globals x)
	    with Dict.Absent ->
	      begin
		let x' = try
		  complete_name global_env (Dict.member global_env.globals) x
		with Unbound -> raise (UnboundVar (x,loc))
		in
		exp.raw_exp <- Var x';
		Dict.lookup global_env.globals x'
	      end
	    end
	| Primop(p,[e1;e2]) ->
	    let t1 = tcExp' e1 in
	    let t2 = tcExp' e2 in
	    tcBinPrimop global_env env loc p t1 t2
	| Primop(p,[e]) ->
	    let t1 = tcExp' e in
	    tcUnPrimop global_env env loc p t1
	| Primop(_,_) -> terr loc "primop wrong # of args"; raise Gcdfec.Exit
	| Conditional(e1,e2,e3) ->
	    let t1 = tcExp' e1 in
	    if not (unify BooleanType t1)
	    then terr loc ("conditional argument has type "^(typ2string t1)
			   ^"instead of bool");
	    let t2 = tcExp' e2 in
	    let t3 = tcExp' e3 in
	    if unify t2 t3 then t2
	    else
	      (terr loc ("clauses of conditional do not match type: "
			 ^(typ2string t2)^" != "^(typ2string t3));
	       raise Gcdfec.Exit)
	| Assign(e1,e2) ->
	    let t1 = tcExp' e1 in
	    let t2 = tcExp' e2 in
	    check_valid_lhs global_env e1;
	    if not (unify t1 t2)
	    then terr loc ("assignment type mismatch: "^(typ2string t1)
			   ^" != " ^(typ2string t2));
	    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 global_env env loc p t1 t2 in
	    begin
	      if not (unify t_result t1)
	      then terr loc "Cannot use this operator in front of an assignment.";
	      t_result
	    end
	| FunCall(e,ts,es) ->
	    let t = tcExp' e in
	    (match t with
	      FnType(vs,rt,argts) ->
		(* inst is the instantiation of the bound type variables vs.
		 * we substitute Evar's for them to be unified.  *)
		let inst = List.map (fun v -> (v,Evar(ref None))) vs in
		let rt = (subst inst) rt in
		let argts = List.map (subst inst) argts in
		((try
		  (match !ts with
		    (* implicit instantiation *)
		    None -> ts := Some(List.map snd inst)
		    (* explicit instantiation *)
		  | Some ts -> List.iter2 unify_un ts (List.map snd inst));
		  (List.iter2
		     (fun e t ->
		       let t' = tcExp' e in
		       if not (unify t' t)
		       then 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"; raise Gcdfec.Exit))
	    | t -> terr loc ("attempt to apply non function type "
			     ^(typ2string t)); raise Gcdfec.Exit)
	| NewStruct(n,ts,es) ->
	    (* The parser does not distinguish NewExn from NewStruct so
	       we have to make this distinction here.  If a struct and an
	       exception have the same name we will consider that an error.
	     *)
	    begin let defined name =
	      Dict.member global_env.structs name ||
	      Dict.member global_env.exceptions name
	    in
	    let name =
	      try complete_name global_env defined n
	      with Unbound ->
		terr loc (n ^ " refers to neither a struct nor an exception.");
		raise Gcdfec.Exit
	    in
	    match (Dict.member global_env.structs name,
		   Dict.member global_env.exceptions name)
	    with
	      (true,true) ->
		terr loc ("Ambiguous new (struct? or exception?) " ^ n);
		raise Gcdfec.Exit
	    | (false,false) -> failwith "poptype.ml:NewStruct:Impossible."
	    | (false,true) ->
		(* It is a NewExn *)
		begin
		  let eopt =
		    match (!ts,es) with
		      (None,[])  -> None
		    | (None,[e]) -> (Some e)
		    | (Some _,_) ->
		    	terr loc (n^" is an exception. Type arguments are not allowed.");
		    	raise Gcdfec.Exit
		    | _ ->
		    	terr loc (n^" is an exception.  Too many arguments");
		    	raise Gcdfec.Exit
		  in
		  exp.raw_exp <- NewExn (name,eopt);
		  tcExp' exp
		end
	    | (true,false) ->
		(* It is a NewStruct. *)
	    	begin try
		  exp.raw_exp <- NewStruct (name,ts,es);
		  let sd = Dict.lookup global_env.structs name in
		  (* inst is the instantiat'n for the bound type variables with
		   * Evar's used for unification. *)
		  let inst = List.map (fun v->(v,Evar(ref None))) sd.st_tyvars
		  in
		  begin match !ts with
		    (* implicit instantiation *)
		    None -> ts := Some(List.map snd inst)
		    (* explicit instantiation *)
		  | Some ts -> List.iter2 unify_un ts (List.map snd inst)
		  end;
		  let checkexp e (f,_,t) =
		    let t = subst inst t in
		    let t' = tcExp' e in
		    if not (unify t' t)
		    then 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(ref n,List.map snd inst)
	    	with
		  Dict.Absent -> failwith "poptype.ml:NewStruct:Impossible."
	    	| Invalid_argument _ ->
		    terr loc ("struct "^n^" argument # mismatch");
		    raise Gcdfec.Exit
	    	end
	    end
	| StructMember(e,f) ->
	    begin try
	      match compress (tcExp' e) with
	      	NamedType(n,ts) ->
		  (try
		    let n = !n in
		    let sd = Dict.lookup global_env.structs n in
		    let rec aux fs =
		      match fs with
		      	((f',_,t)::rest) ->
		    	  if f = f' then
			    let inst = List.map2 (fun v t -> (v,t))
			  	sd.st_tyvars ts in
			    subst inst t
			  else aux rest
		      | [] ->
			  terr loc ("struct "^n^" has no "^f^" field");
			  raise Gcdfec.Exit
		    in aux sd.st_fields
		  with
		    Dict.Absent ->
		      terr loc (!n ^ " not a struct");
		      raise Gcdfec.Exit)
	      | t ->
		  terr loc ((typ2string t)^" not a struct");
		  raise Gcdfec.Exit
	    with UnboundVar (x,loc) ->
	      match e.raw_exp with
		Var y ->
		  begin
		    exp.raw_exp <- Var (add_prefix y f);
		    try tcExp' exp
		    with UnboundVar _ -> raise (UnboundVar (x,loc))
		  end
	      |	_ -> raise (UnboundVar(x,loc))
	    end
	| NewUnion(n,ts,f,eopt) ->
	    let name =
	      try complete_name global_env (Dict.member global_env.unions) n
	      with Unbound ->
		terr loc (n^" is not a union");
		raise Gcdfec.Exit
	    in
	    exp.raw_exp <- NewUnion (name,ts,f,eopt);
	    begin try
	      (* similar to NewStruct *)
	      let ud = Dict.lookup global_env.unions n in
	      let inst = List.map (fun v->(v,Evar(ref None))) ud.un_tyvars in
	      let evars = List.map snd inst in
	      let rty = NamedType(ref n,evars) in
	      (match !ts with
		None -> ts := Some(evars)
	      |	Some ts -> List.iter2 unify_un evars ts);
	      let t = subst inst (List.assoc f ud.un_fields) in
	      begin match t,eopt with
		VoidType,None -> ()
	      |	_,None ->
		  terr loc ("union "^n^", field "^f^
			    " requires argument of type "^(typ2string t));
		  raise Gcdfec.Exit
	      |	_,Some e ->
		  let t' = tcExp' e in
		  if unify t' t then ()
		  else terr loc ("union "^n^", field "^f^
				 " requires argument of type "
				 ^(typ2string t)^
				 " not "^(typ2string t'))
	      end;
	      rty
	    with
	      Dict.Absent -> failwith ("poptype.ml:NewUnion:Impossible.")
	    | Not_found ->
		terr loc ("union "^n^" has no "^f^" field");
		raise Gcdfec.Exit
	    end
	| NewTuple(es) -> TupleType(List.map tcExp' es)
	| TupleMember(e,i) ->
	    (match compress (tcExp' e) with
	      TupleType ts ->
		(try List.nth ts (i - 1) with
		  Failure _ ->
		    terr loc ("tuple has "^(string_of_int (List.length ts))^
			      " fields");
		    raise Gcdfec.Exit)
	    | Evar _ ->
		terr loc ("cannot determine # of fields in tuple type");
		raise Gcdfec.Exit
	    | t -> terr loc ("tuple projection applied to "^(typ2string t)^
			     " value");
		raise Gcdfec.Exit)
	| Subscript(e1,e2) ->
	    begin
	      let t1 = tcExp' e1 in
	      let t2 = tcExp' e2 in
	      if not (unify IntType t2)
	      then terr e2.exp_loc
		  ("subscript type "^(typ2string t2)^" not an int");
	      match compress t1 with
	      	StringType -> CharType
	      | _ ->
		  let t = Evar(ref None) in
		  if unify (ArrayType t) t1 then t
		  else  (terr e1.exp_loc
			   ("subscript on non-array/string type "
			    ^(typ2string t1));
			 raise Gcdfec.Exit)
	    end
	| NewArray(e1,e2) ->
	    let t2 = tcExp' e2 in
	    let t1 = tcExp' e1 in
	    if not (unify IntType t1)
	    then terr loc ((typ2string t1)^" not an int");
	    ArrayType t2
	| NewExn(id,eopt) ->
	    begin try
	      let t1 = Dict.lookup global_env.exceptions id in
	      begin match t1,eopt with
		VoidType,None -> ()
	      |	t,Some e ->
		  let t2 = tcExp' e in
		  if not (unify t t2)
		  then terr loc ("exception "^id^" requires "
				 ^(typ2string t)^"<>"^(typ2string t2));
		  ()
	      |	_,None -> terr loc ("exception "^id^" requires "^(typ2string t1)
				    ^" value")
	      end;
	      ExnType
	    with Dict.Absent ->
	      terr loc ("unknown exception or struct: "^id);
	      raise Gcdfec.Exit
	    end
	| Raise e ->
	    let t = tcExp' e in
	    if not (unify t ExnType)
	    then (terr loc ("expected type exn found type " ^ (typ2string t)));
	    Evar(ref None)
(* Cyclone *)
        | Codegen fd ->
            let env' = Frame({ f_name = fd.fn_name;
	                       f_tyvars = fd.fn_tyvars;
                               f_args = fd.fn_args;
                               f_ret_type = fd.fn_ret_type;
                               f_locals = fd.fn_args;
                               f_inloop = false },
		             env) in
            tcFunDecl global_env env' loc fd;
            FnType(fd.fn_tyvars,fd.fn_ret_type,List.map snd fd.fn_args)
        | Fill e ->
            begin
              match env with
                Frame(fenv,cenv) -> tcExp global_env (Hidden(fenv,cenv)) e
              | Hidden _ ->
                  terr loc "fill cannot be used while codegen is in cut";
		  raise Gcdfec.Exit
              | Outermost _ ->
		  terr loc "fill can only be used within codegen";
		  raise Gcdfec.Exit
            end
(* End Cyclone *)
      end
    in (exp.exp_typ <- Some t; t)
  end (* end of tcExp *)
and tcBinPrimop global_env env loc p t1 t2 =
  begin
    match p with
      (Plus | Times | Minus | Div | Mod | Bitand | Bitor | Bitxor |
       Bitlshift | Bitlrshift | Bitarshift) ->
	 if not (unify global_env IntType t1)
	 then terr loc "first argument to primitive not an int";
	 if not (unify global_env IntType t2)
	 then terr loc "second argument to primitive not an int";
	 IntType
    | (Gt | Lt | Gte | Lte) ->
	if not (unify global_env IntType t1)
	then terr loc "first argument to comparison not an int";
	if not (unify global_env IntType t2)
	then terr loc "second argument to comparison not an int";
	BooleanType
    | (Eq | Neq) ->
	if not (unify global_env t1 t2)
	then terr loc ("comparison of two types: "^(typ2string t1)^" != "
		       ^(typ2string t2));
	BooleanType
    | _ ->
	terr loc ("wrong # of args to primop");
	raise Gcdfec.Exit
  end
and tcUnPrimop global_env env loc p t =
  begin
    let unify_t = unify global_env t in
    match p with
      Not ->
	if not (unify_t BooleanType)
	then terr loc ("! requires bool <> "^(typ2string t));
	BooleanType
    | Bitnot ->
	if not (unify_t IntType)
	then terr loc ("bitwise negation requires int <> "^(typ2string t));
	IntType
    | Size ->
	begin match compress t with
	  StringType -> ()
	| ArrayType _ -> ()
	| _ -> terr loc ("size requires string/array <> "^(typ2string t))
	end;
	IntType
    | Ord ->
	if not (unify_t CharType)
	then terr loc ("ord requires char <> "^(typ2string t));
	IntType
    | Chr ->
	if not (unify_t IntType)
	then terr loc ("chr requires int <> "^(typ2string t));
	CharType
    | _ ->
	terr loc "wrong # of args for primop";
	raise Gcdfec.Exit
  end
and check_valid_lhs global_env e =
  begin
    match e.raw_exp with
      Var _ -> ()
    | StructMember(e1,f) ->
	(match e1.exp_typ with
	  Some t ->
	    (match compress t with
	      NamedType(n,_) ->
		let n = !n in
	    	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 0")
	| _ -> failwith "type lookup")
    | Subscript(e1,e2) ->
	(match e1.exp_typ with
	  Some t ->
	    (match compress t with
	      StringType ->
	    	terr e.exp_loc ("update not allowed on strings")
	    | ArrayType t -> ()
	    | _ -> terr e.exp_loc "not a valid left-hand-side")
	| None -> failwith "type lookup 1")
    | _ -> 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_tyvars fd.fn_ret_type;
    List.iter (fun (_,t) -> check_valid_type loc global_env fd.fn_tyvars 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));
    try
      tcStmt global_env env fd.fn_body
	with UnboundVar (x,loc) ->
	  (terr loc ("unbound variable "^x); raise Gcdfec.Exit)
  end
(* end of tcFunDecl *)

let rec add_global_env ((structs,unions,abstracts,globals,exns) 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
  begin match d with
    StructDecl sd ->
      check_duplicate sd.st_name;
      (Dict.insert structs sd.st_name sd, unions, abstracts, globals, exns)
  | UnionDecl ud ->
      check_duplicate ud.un_name;
      (structs, Dict.insert unions ud.un_name ud, abstracts, globals, exns)
  | ExceptionDecl(v,s,t) ->
      (structs, unions, abstracts, globals, Dict.insert exns v t)
  | ExternType (n,vs,b) ->
      check_duplicate n;
      (structs,unions,Dict.insert abstracts n (vs,b), globals, exns)
  | FunDecl fd ->
      let v = fd.fn_name in
      let t = FnType(fd.fn_tyvars,fd.fn_ret_type,List.map snd fd.fn_args) in
      (structs,unions,abstracts,Dict.insert globals v t,exns)
  | ExternVal (v,t) -> (structs,unions,abstracts,Dict.insert globals v t,exns)
  | GlobalDecl (s,v,t,eor) ->
      (structs,unions,abstracts,Dict.insert globals v t,exns)
  | PrefixDecl _ -> failwith "poptype.ml:add_global_env: prefixes should have been eliminated"
  | OpenDecl(prefix,ds') -> add_globals_env e ds'
  end
and add_globals_env e ds = List.fold_left add_global_env e ds

let initial_global_env ds =
  let empty_env =
    let d () = Dict.empty compare in
    (d(), d(), d(), d(), d())
  in
  let (s,u,a,g,e) = add_globals_env empty_env ds in
  { structs = s; unions = u; abstracts = a; globals = g; exceptions = e;
    open_prefixes = []
  }

let rec check_fundecl global_env loc fd =
  let env =
     mk_env { f_name = fd.fn_name;
	      f_tyvars = fd.fn_tyvars;
              f_args = fd.fn_args;
              f_ret_type = fd.fn_ret_type;
              f_locals = fd.fn_args;
              f_inloop = false
	    }
  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 sd.st_tyvars t)
      sd.st_fields
  end

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

let check_globaldecl loc global_env (s,v,t,eor) =
  begin
    check_valid_type loc global_env [] t;
    let env =
       mk_env { f_name = "*BOGUS*";
		f_tyvars = [];
		f_args = [];
		f_ret_type = VoidType;
		f_locals = [];
		f_inloop = false
	      }
    in
    let e =
      match !eor with
	None -> default_initializer global_env t loc
      |	Some e -> check_constexp e; e
    in
    let t' = tcExp global_env env e in
    (* FMS:
       We need to unify this so the uninstantiated type variable in
       t' gets instantiated for null.
       It is unfortunate but we must do this even when we create
       a default initializer.
       *)
    if not (unify global_env t t')
    then (terr loc ("The type of the initializer ("
		    ^ (typ2string t')
		    ^ ") does not match the declared type ("
		    ^ typ2string t ^").");
	  raise Gcdfec.Exit);
    eor := Some(e);
  end

let check_top_decls ds =
  let global_env = initial_global_env ds in
  let rec check_decls global_env ds =
    let check_decl (d,loc) =
      begin 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
      | ExceptionDecl(v,s,t) ->
	  begin
	    if s = Abstract
	    then terr loc "Exceptions cannot be delared abstract.";
	    check_valid_type loc global_env [] t
	  end
      | ExternType _ -> ()
      | ExternVal (v,t) -> check_valid_type loc global_env [] t
      | GlobalDecl d -> check_globaldecl loc global_env d
      | PrefixDecl _ -> failwith "poptype.ml:check_decl:prefixes should have been eliminated.\n"
      |	OpenDecl (prefix,ds) ->
	  check_decls
	    {global_env with open_prefixes = prefix::global_env.open_prefixes}
	    ds
      end in
    List.iter check_decl ds
  in
  check_decls global_env ds;
  (ds,global_env)

(* This approach has the drawback that error messages will show funny names
   but it is the easiest to implement and seems appropriate at this time. *)
let eliminate_prefixes ds =
  let rec aux current_prefix_opt ds =
    let aux' = aux current_prefix_opt in
    match (current_prefix_opt,ds) with
      (None,(PrefixDecl (prefix,ds'),loc) :: tl) ->
	(aux (Some prefix) ds') @ (aux' tl)
    | (None,(OpenDecl (prefix,ds'),loc) :: tl) ->
	(OpenDecl (prefix,aux' ds'),loc) :: (aux' tl)
    | (None,hd::tl) -> hd :: (aux' tl)
    | (Some p,(hd,loc)::tl) ->
	begin
	  let loop td = td :: (aux' tl) in
	  match hd with
	    FunDecl fd -> loop
	      	(FunDecl { fd with fn_name = add_prefix p fd.fn_name}, loc)
	  | StructDecl sd -> loop
		(StructDecl { sd with st_name = add_prefix p sd.st_name }, loc)
	  | UnionDecl ud -> loop
		(UnionDecl { ud with un_name = add_prefix p ud.un_name }, loc)
	  | ExceptionDecl(v,s,t) -> loop
	      	(ExceptionDecl(add_prefix p v, s,t), loc)
	  | ExternType (tn,vs,b) -> loop
	      	(ExternType (add_prefix p tn,vs,b), loc)
	  | ExternVal (v,t) -> loop
	      	(ExternVal (add_prefix p v,t), loc)
	  | GlobalDecl (sc,v,t,eor) -> loop
	      	(GlobalDecl (sc, add_prefix p v,t,eor),loc)
	  | PrefixDecl (p',ds') ->
	      (aux (Some (add_prefix p p')) ds') @ (aux' tl)
	  | OpenDecl (p',ds') -> loop
		(OpenDecl (p',aux' ds'),loc)
  	end
    | (_,[]) -> []
  in
  aux None ds

let type_check ds = check_top_decls (eliminate_prefixes ds);;

