[snipe.git] / type / typechecker.sml

(* L3 Compiler
 * TypeChecker
 * Author: Alex Vaynberg <alv@andrew.cmu.edu>
 * Modified: Frank Pfenning <fp@cs.cmu.edu>
 * Modified: Joshua Wise <jwise>
 * Modified: Chris Lu <czl>
 *) 

signature TYPE_CHECK =
sig
  (* prints error message and raises ErrorMsg.error if error found *)
  val typecheck : Ast.program -> Ast.program
  val typeof : Ast.program -> Type.vtype Symbol.table -> Mark.ext option -> Ast.exp -> Type.vtype
end;

structure TypeChecker :> TYPE_CHECK = 
struct
  structure A = Ast
  structure AU = AstUtils
  structure T = Type
  
  fun typeof (tds, funcs) vars mark e =
    ( case e
      of A.Var a => (case Symbol.look vars a
                     of NONE => (ErrorMsg.error mark ("variable `"^(Symbol.name a)^"' not declared here") ; raise ErrorMsg.Error)
                      | SOME t => t)
       | A.ConstExp _ => T.Int
       | A.OpExp (A.EQ, [a, b]) =>
           (case (typeof (tds, funcs) vars mark a, typeof (tds, funcs) vars mark b)
            of (T.Int, T.Int) => T.Int (* You shall pass! *)
             | (a', b') =>
                 if (T.typeeq (a', T.TNull) andalso T.castable (b', T.TNull)) orelse
                    (T.typeeq (b', T.TNull) andalso T.castable (a', T.TNull)) orelse
                    (T.typeeq (a', b'))
                 then T.Int
                 else (ErrorMsg.error mark ("incorrect types for equality opexp:" ^ T.Print.pp_type a' ^ ", " ^ T.Print.pp_type b') ; raise ErrorMsg.Error ))
       | A.OpExp (A.NEQ, el) => typeof (tds, funcs) vars mark (A.OpExp (A.EQ, el))
       | A.OpExp (_, el) => (List.app
                              (fn e =>
                                (case (typeof (tds, funcs) vars mark e)
                                 of T.Int => ()
                                  | _ => (ErrorMsg.error mark ("incorrect type for opexp; needed int") ; raise ErrorMsg.Error)))
                              el ; T.Int)
       | A.Marked e => typeof (tds, funcs) vars (Mark.ext e) (Mark.data e)
       | A.FuncCall (i, exps) =>
         let
           val func = (case Symbol.look funcs i
                       of NONE => (ErrorMsg.error mark ("function `"^(Symbol.name i)^"' not declared") ; raise ErrorMsg.Error)
                        | SOME f => f)
           val funcmark = AU.Function.mark func
           val (ftype, fparams) = (AU.Function.returntype func, AU.Function.params func)
           val exptypes = List.map (fn znt => typeof (tds, funcs) vars mark znt) exps
           val () = if (length exptypes = length fparams) then ()
                    else (ErrorMsg.error mark ("call to function `"^(Symbol.name i)^"' has incorrect parameter count [you must construct additional tycons]") ; raise ErrorMsg.Error)
           val () = List.app
                      (fn (t, (i, t')) =>
                        if not (T.castable (t', t))
                        then (ErrorMsg.error mark ("parameter `"^(Symbol.name i)^"' in function call has wrong type [you must construct additional tycons]") ; raise ErrorMsg.Error)
                        else ())
                      (ListPair.zip (exptypes, fparams))
         in
           ftype
         end
       | A.Member (e, i) =>
         let
           val t = typeof (tds, funcs) vars mark e
           val name = case t
                      of (T.Typedef i) => i
                       | _ => (ErrorMsg.error mark ("member operation only exists for struct types") ; raise ErrorMsg.Error)
           val s = case Symbol.look tds name
                   of SOME s => s
                    | NONE => (ErrorMsg.error mark ("undefined structure `"^(Symbol.name name)^"' in type") ; raise ErrorMsg.Error)
           val (s, smark) = (T.defdata s, T.defmark s)
           val vl = case s
                    of T.Struct vl => vl
                     | _ => raise ErrorMsg.InternalError "mark of marked typedef?"
           val t = case (List.find (fn (i', t) => (Symbol.name i = Symbol.name i')) vl)
                   of SOME (_, t) => t
                    | NONE => (ErrorMsg.error mark ("undefined member `"^(Symbol.name i)^"' in struct") ; ErrorMsg.error smark ("struct `"^(Symbol.name name)^"' defined here") ; raise ErrorMsg.Error)
         in
           t
         end
       | A.DerefMember (e, i) =>
         let
           val t = typeof (tds, funcs) vars mark e
           val name = case t
                      of (T.Pointer (T.Typedef i)) => i
                       | _ => (ErrorMsg.error mark ("dereference and member operation only exists for struct pointer types") ; raise ErrorMsg.Error)
           val s = case Symbol.look tds name
                   of SOME s => s
                    | NONE => (ErrorMsg.error mark ("undefined structure `"^(Symbol.name name)^"' in type") ; raise ErrorMsg.Error)
           val (s, smark) = case s
                            of T.Struct vl => (s, NONE)
                             | T.MarkedTypedef m => (Mark.data m, Mark.ext m)
           val vl = case s
                    of T.Struct vl => vl
                     | _ => raise ErrorMsg.InternalError "mark of marked typedef?"
           val t = case (List.find (fn (i', t) => (Symbol.name i = Symbol.name i')) vl)
                   of SOME (_, t) => t
                    | NONE => (ErrorMsg.error mark ("undefined member `"^(Symbol.name i)^"' in struct") ; ErrorMsg.error smark ("struct `"^(Symbol.name name)^"' defined here") ; raise ErrorMsg.Error)
         in
           t
         end
       | A.Dereference e =>
         (case typeof (tds, funcs) vars mark e
          of (T.Pointer e') => e'
           | _ => (ErrorMsg.error mark ("cannot deference non-pointer type") ; raise ErrorMsg.Error))
       | A.ArrIndex (e, i) =>
         (case (typeof (tds, funcs) vars mark e, typeof (tds, funcs) vars mark i)
          of (T.Array e', T.Int) => e'
           | (_, T.Int) => (ErrorMsg.error mark ("cannot index non-array type") ; raise ErrorMsg.Error)
           | _ => (ErrorMsg.error mark ("cannot index using non-int type") ; raise ErrorMsg.Error))
       | A.New (t) => T.Pointer t
       | A.NewArr (t, s) =>
         (case typeof (tds, funcs) vars mark s
          of T.Int => (T.Array t)
           | _ => (ErrorMsg.error mark ("cannot specify non-int array dimension") ; raise ErrorMsg.Error))
       | A.Null => T.TNull
       | A.Conditional (q, e1, e2) =>
         let
           val _ = case typeof (tds, funcs) vars mark q
                   of T.Int => ()
                    | _ => (ErrorMsg.error mark ("ternary condition not of Int type") ; raise ErrorMsg.Error)
           val t1 = typeof (tds, funcs) vars mark e1
           val t2 = typeof (tds, funcs) vars mark e2
         in
           if (T.typeeq (t1, t2) orelse T.castable (t1, t2))
           then t1
           else if (T.castable (t2, t1))
           then t2
           else (ErrorMsg.error mark ("ternary types do not agree [you must construct additional tycons]") ; raise ErrorMsg.Error)
         end
    )
  
  datatype asn = ASSIGNED | UNASSIGNED

  (* returncheck prog vars mark t l
   * Determines if the statement list 'l' is guaranteed to return vtype 't'.
   * If it ever does not return vtype 't', then raises an error.
   * true if vtype 't' is always returned, or false if there is a possibility that vtype 't' will not be returned.
   *)
  fun returncheck prog vars mark t l =
    let
      fun returns' nil = false
        | returns' (A.Assign _ :: stms) = returns' stms
        | returns' (A.AsnOp _ :: stms) = returns' stms
        | returns' (A.Effect _ :: stms) = returns' stms
        | returns' (A.Return e :: stms) =
            if (T.castable (t, typeof prog vars mark e))
            then true
            else (ErrorMsg.error mark ("return value of incorrect type for function") ; raise ErrorMsg.Error)
        | returns' (A.Nop :: stms) = returns' stms
        | returns' (A.Break :: stms) = true (* blah *)
        | returns' (A.Continue :: stms) = true (* blah *)
        | returns' (A.If (_, s1, NONE) :: stms) = returns' stms
        | returns' (A.If (_, s1, SOME s2) :: stms) = (returns' s1 andalso returns' s2) orelse returns' stms
        | returns' (A.For _ :: stms) = returns' stms
        | returns' (A.While _ :: stms) = returns' stms
        | returns' (A.MarkedStm m :: stms) = returncheck prog vars (Mark.ext m) t (Mark.kane m :: stms)
    in
      returns' l
    end
  
  (* returns l
   * true iff the statement list 'l' always returns.
   *)
  fun returns nil = false
    | returns (A.Assign _ :: stms) = returns stms
    | returns (A.AsnOp _ :: stms) = returns stms
    | returns (A.Effect _ :: stms) = returns stms
    | returns (A.Return e :: stms) = true
    | returns (A.Nop :: stms) = returns stms
    | returns (A.Break :: stms) = true (* blah *)
    | returns (A.Continue :: stms) = true (* blah *)
    | returns (A.If (_, s1, NONE) :: stms) = returns stms
    | returns (A.If (_, s1, SOME s2) :: stms) = (returns s1 andalso returns s2) orelse returns stms
    | returns (A.For _ :: stms) = returns stms
    | returns (A.While _ :: stms) = returns stms
    | returns (A.MarkedStm m :: stms) = returns (Mark.kane m :: stms)
  
  (* breakcheck l mark
   * Throws an error exception if a break or continue ever occurs in an illegal context.
   *)
  fun breakcheck nil mark = ()
    | breakcheck (A.Break :: stms) mark = ( ErrorMsg.error mark ("Illegal break outside loop") ;
                                             raise ErrorMsg.Error )
    | breakcheck (A.Continue :: stms) mark = ( ErrorMsg.error mark ("Illegal continue outside loop") ;
                                                raise ErrorMsg.Error )
    | breakcheck (A.If (_, s1, NONE) :: stms) mark =
        ( breakcheck s1 mark;
          breakcheck stms mark)
    | breakcheck (A.If (_, s1, SOME s2) :: stms) mark =
        ( breakcheck s1 mark;
          breakcheck s2 mark;
          breakcheck stms mark)
    | breakcheck (A.MarkedStm m :: stms) mark = (breakcheck [(Mark.kane m)] (Mark.ext m); breakcheck stms mark)
    | breakcheck (_ :: stms) mark = breakcheck stms mark
  
  (* varcheck_exp env exp mark
   * Throws an error exception if a variable used in this excpression was unassigned or undefined in this context.
   *)
  fun varcheck_exp env (A.Var v) mark =
        ( case Symbol.look env v
          of NONE => ( ErrorMsg.error mark ("undefined variable `" ^ Symbol.name v ^ "'") ;
                       raise ErrorMsg.Error )
           | SOME UNASSIGNED => ( ErrorMsg.error mark ("usage of unassigned variable `" ^ Symbol.name v ^ "'") ;
                                  raise ErrorMsg.Error )
           | SOME ASSIGNED => ())
    | varcheck_exp env (A.ConstExp _) mark = ()
    | varcheck_exp env (A.OpExp (_, l)) mark = List.app (fn znt => varcheck_exp env znt mark) l
    | varcheck_exp env (A.FuncCall (f, l)) mark = List.app (fn znt => varcheck_exp env znt mark) l
    | varcheck_exp env (A.Marked m) mark = varcheck_exp env (Mark.kane m) (Mark.ext m)
    | varcheck_exp env (A.Member (e, i)) mark = varcheck_exp env e mark
    | varcheck_exp env (A.DerefMember (e, i)) mark = varcheck_exp env e mark
    | varcheck_exp env (A.Dereference e) mark = varcheck_exp env e mark
    | varcheck_exp env (A.ArrIndex (e1, e2)) mark = (varcheck_exp env e1 mark ; varcheck_exp env e2 mark)
    | varcheck_exp env (A.New _) mark = ()
    | varcheck_exp env (A.NewArr (_, e)) mark = varcheck_exp env e mark
    | varcheck_exp env (A.Null) mark = ()
    | varcheck_exp env (A.Conditional (q, e1, e2)) mark = (varcheck_exp env q mark ; varcheck_exp env e1 mark ; varcheck_exp env e2 mark)
  
  (* computeassigns env exp
   * Computes the assigned variables after expression exp has been executed with a starting context of env.
   *)
  fun computeassigns env nil = env
    | computeassigns env (A.Assign (A.Var id,e) :: stms) =
        computeassigns (Symbol.bind env (id, ASSIGNED)) stms
    | computeassigns env (A.Assign (A.Marked a, e) :: stms) =
        computeassigns env (A.Assign (Mark.data a, e) :: stms)
    | computeassigns env (A.AsnOp (oper, a, e) :: stms) =
        computeassigns env (A.Assign (a, a) :: stms)
    | computeassigns env (A.Assign (_) :: stms) = computeassigns env stms
    | computeassigns env (A.Effect _ :: stms) = computeassigns env stms
    | computeassigns env (A.Return _ :: stms) = env
    | computeassigns env (A.Nop :: stms) = computeassigns env stms
    | computeassigns env (A.Break :: stms) = env
    | computeassigns env (A.Continue :: stms) = env
    | computeassigns env (A.If (e, s1, NONE) :: stms) = computeassigns env stms
    | computeassigns env (A.If (e, s1, SOME s2) :: stms) =
        let
          val env1 = computeassigns env s1
          val env2 = computeassigns env s2
          val env' =
            Symbol.intersect
              (fn (ASSIGNED, ASSIGNED) => ASSIGNED
                | _ => UNASSIGNED)
              (env1, env2)
          val env' =
            if (returns s1) then env2
            else if (returns s2) then env1
            else env'
        in
          computeassigns env' stms
        end
    | computeassigns env (A.While (e, s1) :: stms) = computeassigns env stms
    | computeassigns env (A.For (sbegin, e, sloop, inner) :: stms) =
       let
         val env' = case sbegin
                    of SOME(s) => computeassigns env [s]
                     | NONE => env
       in
         computeassigns env' stms
       end
    | computeassigns env (A.MarkedStm m :: stms) = computeassigns env ((Mark.kane m) :: stms)
  
  (* varcheck env l mark
   * Checks that all variables used in the statement list l have been defined before being used, and removes code that is unreachable according to simple return analysis.
   *)
  fun varcheck env nil mark = nil
    | varcheck env (A.Assign (A.Var id, e) :: stms) mark =
        let
          val sym = Symbol.look env id
          val _ = if not (isSome sym)
                  then (ErrorMsg.error mark ("assignment to undeclared variable " ^ (Symbol.name id)); raise ErrorMsg.Error)
                  else ()
          val t = valOf sym
          val _ = varcheck_exp env e mark
        in 
          A.Assign (A.Var id, e) :: (varcheck (Symbol.bind env (id, ASSIGNED)) stms mark)
        end
    | varcheck env (A.Assign (A.Marked a, e) :: stms) mark = varcheck env (A.Assign (Mark.data a, e) :: stms) mark
    | varcheck env ((a as A.Assign (A.Member (e', i), e)) :: stms) mark =
        (varcheck_exp env e' mark ;
         varcheck_exp env e mark ;
         a :: varcheck env stms mark)
    | varcheck env ((a as A.Assign (A.DerefMember (e', i), e)) :: stms) mark =
        (varcheck_exp env e' mark ;
         varcheck_exp env e mark ;
         a :: varcheck env stms mark)
    | varcheck env ((a as A.Assign (A.Dereference e', e)) :: stms) mark =
        (varcheck_exp env e' mark ;
         varcheck_exp env e mark ;
         a :: varcheck env stms mark)
    | varcheck env ((a as A.Assign (A.ArrIndex (e', e''), e)) :: stms) mark =
        (varcheck_exp env e' mark ;
         varcheck_exp env e'' mark ;
         varcheck_exp env e mark ;
         a :: varcheck env stms mark)
    | varcheck env ((a as A.Assign (A.NewArr (_, e'), e)) :: stms) mark =
        (varcheck_exp env e' mark ;
         varcheck_exp env e mark ;
         a :: varcheck env stms mark)
    | varcheck env ((A.Assign _) :: stms) mark = raise ErrorMsg.InternalError "assign to non lvalue"
    | varcheck env ((a as A.AsnOp (oper, e1, e2)) :: stms) mark = ( varcheck_exp env e1 mark ; varcheck_exp env e2 mark ; a :: varcheck env stms mark )
    | varcheck env ((a as A.Effect e) :: stms) mark = (varcheck_exp env e mark ; a :: varcheck env stms mark)
    | varcheck env (A.Return (e) :: stms) mark =
        ( varcheck_exp env e mark;
          A.Return (e) :: nil )
    | varcheck env (A.Nop :: stms) mark =
        ( A.Nop :: (varcheck env stms mark))
    | varcheck env (A.Break :: stms) mark =
        ( A.Break :: nil )
    | varcheck env (A.Continue :: stms) mark =
        ( A.Continue :: nil )
    | varcheck env (A.If (e, s1, NONE) :: stms) mark =
        ( varcheck_exp env e mark ;
          varcheck env s1 mark ;
          A.If (e, s1, NONE) :: (varcheck env stms mark) )
    | varcheck env ((i as A.If (e, s1, SOME s2)) :: stms) mark =
        ( varcheck_exp env e mark ;
          varcheck env s1 mark ; 
          varcheck env s2 mark ;
          A.If (e, s1, SOME s2) ::
            (if (returns [i])
             then nil
             else varcheck (computeassigns env [i]) stms mark)  )
    | varcheck env (A.While (e, s1) :: stms) mark =
        ( varcheck_exp env e mark ;
          varcheck env s1 mark ;
          A.While (e, s1) :: (varcheck env stms mark) )
    | varcheck env (A.For (sbegin, e, sloop, inner) :: stms) mark =
        let
          val sbegin = case sbegin
                       of SOME(s) => SOME (hd (varcheck env [s] mark))
                        | NONE => NONE
          val env' = case sbegin
                     of SOME(s) => computeassigns env [s]
                      | NONE => env
          val _ = varcheck_exp env' e mark
          val inner = varcheck env' inner mark
          val env'' = computeassigns env' inner
          val sloop = case sloop
                  of SOME(s) => SOME (hd (varcheck env'' [s] mark))
                   | NONE => NONE
        in
          A.For (sbegin, e, sloop, inner) :: (varcheck env' stms mark)
        end
    | varcheck env (A.MarkedStm m :: stms) mark = varcheck env ((Mark.kane m) :: stms) (Mark.ext m)

  fun bindvars sym stat l = foldr (fn ((i,t), s) => Symbol.bind s (i,stat)) sym l
  fun bindtypes sym l = foldr (fn ((i,t), s) => Symbol.bind s (i,t)) sym l

  fun dupchk mark l src =
        List.app
          (fn (n, _) =>
            let
              val name = Symbol.name n
              val all = List.filter (fn (n', _) => name = (Symbol.name n')) l
              val count = length all
            in
              if count = 1
              then ()
              else ( ErrorMsg.error mark ("multiple definition of variable " ^ (Symbol.name n) ^ " in " ^ src);
                     raise ErrorMsg.Error )
            end) l
  
  fun check_lvalue prog vars mark (A.Marked m) = check_lvalue prog vars (Mark.ext m) (Mark.data m)
    | check_lvalue prog vars mark (e as A.Var _) = typeof prog vars mark e
    | check_lvalue prog vars mark (e as A.Member _) = typeof prog vars mark e
    | check_lvalue prog vars mark (e as A.DerefMember _) = typeof prog vars mark e
    | check_lvalue prog vars mark (e as A.Dereference _) = typeof prog vars mark e
    | check_lvalue prog vars mark (e as A.ArrIndex _) = typeof prog vars mark e
    | check_lvalue prog vars mark _ = ( ErrorMsg.error mark ("invalid lvalue") ; raise ErrorMsg.Error )
  fun typecheck_stm prog vars mark stm =
    case stm
    of A.Assign (e1, e2) =>
         if not (T.castable (check_lvalue prog vars mark e1, typeof prog vars mark e2))
         then (ErrorMsg.error mark "incompatible types in assignment" ; raise ErrorMsg.Error )
         else if not (T.issmall (check_lvalue prog vars mark e1))
         then (ErrorMsg.error mark "lvalue is not small" ; raise ErrorMsg.Error)
         else ()
     | A.AsnOp (oper, e1, e2) => typecheck_stm prog vars mark (A.Assign (e1, A.OpExp (oper, [e1, e2])))
     | A.Effect e => 
         if not (T.issmall (typeof prog vars mark e))
         then (ErrorMsg.error mark "simple statement's value not small" ; raise ErrorMsg.Error )
         else ()
     | A.Return e => (typeof prog vars mark e ; ())
     | A.Nop => ()
     | A.Break => ()
     | A.Continue => ()
     | A.If (e, s, NONE) =>
         if T.castable (T.Int, typeof prog vars mark e)
         then (List.app (typecheck_stm prog vars mark) s)
         else (ErrorMsg.error mark "conditional in if statement is not of int type" ; raise ErrorMsg.Error )
     | A.If (e, s1, SOME s2) =>
         if T.castable (T.Int, typeof prog vars mark e)
         then (List.app (typecheck_stm prog vars mark) s1 ; List.app (typecheck_stm prog vars mark) s2)
         else (ErrorMsg.error mark "conditional in if statement is not of int type" ; raise ErrorMsg.Error )
     | A.For (sbegin, e, sloop, s) =>
         if T.castable (T.Int, typeof prog vars mark e)
         then (List.app (typecheck_stm prog vars mark) ((case sbegin of SOME l => [l] | NONE => nil) @ (case sloop of SOME l => [l] | NONE => nil) @ s))
         else (ErrorMsg.error mark "conditional in for statement is not of int type" ; raise ErrorMsg.Error )
     | A.While (e, s) =>
         if T.castable (T.Int, typeof prog vars mark e)
         then (List.app (typecheck_stm prog vars mark) s)
         else (ErrorMsg.error mark "conditional in while statement is not of int type" ; raise ErrorMsg.Error )
     | A.MarkedStm (m) => typecheck_stm prog vars (Mark.ext m) (Mark.data m)
        
  (* XXX does not check big vs. small types *)
  fun typecheck_type (tds, funcs) mark T.Int = ()
    | typecheck_type (tds, funcs) mark T.TNull = ()
    | typecheck_type (tds, funcs) mark (T.Pointer t) = typecheck_type (tds, funcs) mark t
    | typecheck_type (tds, funcs) mark (T.Array t) = typecheck_type (tds, funcs) mark t
    | typecheck_type (tds, funcs) mark (T.Typedef t) =
        case (Symbol.look tds t)
        of SOME _ => ()
         | NONE => (ErrorMsg.error mark ("typedef `"^(Symbol.name t)^"' does not exist") ; raise ErrorMsg.Error)

  fun typecheck_fn prog _ (id, A.MarkedFunction m) = typecheck_fn prog (Mark.ext m) (id, Mark.data m)
    | typecheck_fn (prog as (tds, funcs)) mark (id, A.Extern (t, al)) =
      (if (String.isPrefix "_l5_" (Symbol.name id))
       then
         let
           val n = String.extract (Symbol.name id, 4, NONE)
         in
           if List.exists (fn (id, f) => case (AU.Function.data f) of A.Function _ => (Symbol.name id = n) | _ => false) (Symbol.elemsi funcs)
           then (ErrorMsg.error mark ("you anus, extern " ^ Symbol.name id ^ " conflicts with local function"); raise ErrorMsg.Error)
           else ()
         end
       else () ;
       dupchk mark al ; 
       List.app (typecheck_type prog mark) (List.map (fn (_, t) => t) al) ;
       A.Extern (t, al))
    | typecheck_fn prog mark (id, A.Function (t, al, vl, sl)) =
      let
        val () = dupchk mark (al @ vl) ("function `"^Symbol.name id^"'")	(* Before we do any bindings, check for duplicate names. *)
        val () = List.app (typecheck_type prog mark) (List.map (fn (_, t) => t) (al @ vl))
        val env = Symbol.empty
        val env = bindvars env ASSIGNED al
        val env = bindvars env UNASSIGNED vl
        val vars = Symbol.empty
        val vars = bindtypes vars al
        val vars = bindtypes vars vl
        val () = breakcheck sl mark
        val () = if not (returncheck prog vars NONE t sl)
                 then ( ErrorMsg.error mark ("function `"^ Symbol.name id ^ "' does not return in all cases");
                        raise ErrorMsg.Error )
                 else ()
        val () = List.app (
                  fn (n, t) =>
                    if (T.issmall t)
                    then ()
                    else ( ErrorMsg.error mark ("variable `"^(Symbol.name n)^"' in function `"^(Symbol.name id)^"' not small") ; raise ErrorMsg.Error))
                 (al @ vl)
        val () = List.app (typecheck_stm prog vars mark) sl
      in
        A.Function (t, al, vl, varcheck env sl NONE)
      end

  structure SymbolSet = ListSetFn (
    struct
      type ord_key = Symbol.symbol
      val compare = Symbol.compare
    end
  )
  
  fun typecheck_structs (prog as (tds, funcs)) =
    let
      exception Yuq
      
      val all = SymbolSet.addList (SymbolSet.empty, Symbol.keys tds)
      fun lookup mark sym =
        let
          val s = case Symbol.look tds sym
                  of SOME a => a
                   | NONE => (ErrorMsg.error mark ("typedef `"^(Symbol.name sym)^"' does not exist") ; raise ErrorMsg.Error)
          val vl = case T.defdata s
                   of T.Struct vl => vl
                    | T.MarkedTypedef v => raise ErrorMsg.InternalError "data returned marked type"
        in
          (vl, T.defmark s)
        end
      fun checksym mark sym stack k remaining =
        if not (SymbolSet.member (remaining, sym))
        then k remaining
        else if (SymbolSet.member (stack, sym))
        then ( ErrorMsg.error mark ("structure `"^ (Symbol.name sym) ^"' is involved in a recursive mess") ; raise Yuq)
        else
          let
            val stack' = SymbolSet.add (stack, sym)
            val (vl, mark') = lookup mark sym
            val () = dupchk mark vl ("structure `"^(Symbol.name sym)^"'")
            fun remove k remaining' = k (SymbolSet.delete (remaining', sym))
            val newk = (* OH GOD D: *)
              foldr
                (fn ((_, T.Typedef s), k') => checksym mark' s stack' k'
                  | (_, k') => k')
                (remove k)
                vl
          in
            newk remaining handle Yuq => (ErrorMsg.error mark' ("from structure `"^(Symbol.name sym)^"'") ; raise Yuq)
          end
      fun chooseone k set =
        case (SymbolSet.listItems set)
        of nil => k set
         | (h::l) => checksym NONE h SymbolSet.empty (chooseone k) set
    in
      chooseone (fn _ => ()) all handle Yuq => raise ErrorMsg.Error
    end
  
  fun typecheck (tds, funcs) =
      let
        val main = case (Symbol.look funcs (Symbol.symbol "main"))
                   of NONE => ( ErrorMsg.error NONE ("no function named main");
                                raise ErrorMsg.Error )
                    | SOME m => m
        val (main, mainp) = (AU.Function.data main, AU.Function.mark main)
        val () = case main
                 of A.Extern _ => ( ErrorMsg.error mainp ("you anus, main can't be an extern");
                                    raise ErrorMsg.Error )
                  | A.Function (T.Int, nil, _, _) => ()
                  | A.Function (T.Int, _, _, _) => ( ErrorMsg.error mainp ("main should take no parameters");
                                                        raise ErrorMsg.Error )
                  | A.Function (_, _, _, _) => ( ErrorMsg.error mainp ("main has incorrect return type");
                                                 raise ErrorMsg.Error )
                  | _ => raise ErrorMsg.InternalError "marked of marked disallowed"
        val () = typecheck_structs (tds, funcs)
      in
        (tds, Symbol.mapi (typecheck_fn (tds, funcs) NONE) funcs)
      end
end