(* check-il-fn.sml
 *
 * COPYRIGHT (c) 2010 The Diderot Project (http://diderot.cs.uchicago.edu)
 * All rights reserved.
 *
 * Correctness checker for SSA-based ILs.
 *)

signature OPERATOR_TY =
  sig
    type rator
    type ty

    val sigOf : rator -> ty * ty list

  end

functor CheckILFn (

    structure IL : SSA
    structure OpTy : OPERATOR_TY
	where type rator = IL.Op.rator
	where type ty = IL.Ty.ty

  ) : sig

  end = struct

    structure IL = IL
    structure Ty = IL.Ty
    structure V = IL.Var
    structure VSet = V.Set

    fun checkVar bvs x = if VSet.member(x, bvs)
	  then ()
	  else (* error *)

    fun chkAssign (bvs, y, rhs) = (
	  (* check that y is not bound twice *)
	    if VSet.member(y, bvs)
	      then (* error *)
	      else ();
	    case rhs
	     of IL.VAR x => (
		  checkVar bvs x;
		  if Ty.same(V.ty y, V.ty x)
		    then ()
		    else (* error *))
	      | IL.LIT lit => let
		  val ty = (case lit
			 of IL.Int _ => Ty.IntTy
			  | IL.Float _ => Ty.realTy
			  | IL.String _ => Ty.StringTy
			  | IL.Bool _ => Ty.BoolTy
			(* end case *))
		  in
		    if Ty.same(V.ty y, ty)
		      then ()
		      else (* error *)
		  end
	      | IL.OP(rator, xs) => let
		  val (resTy, argTys) = OpTy.sigOf rator
		  in
		    List.app (checkVar bvs) xs;
		    if Ty.same(V.ty y, resTy)
		      then ()
		      else (* error *);
		    if ListPair.allEq (fn (x, ty) => Ty.same(V.ty x, ty)) (xs, argsTys)
		      then ()
		      else (* error *)
		  end
	      | IL.CONS xs => (
		  List.app (checkVar bvs) xs;
(* FIXME: check type of y *)())
	    (* end case *);
	    VSet.add(bvs, y))

    fun checkPhi (bvs, y, xs) = let
	  val ty = V.ty y
	  in
	  (* check that y is not bound twice *)
	    if VSet.member(y, bvs)
	      then (* error *)
	      else ();
	  (* check that rhs vars have the correct type *)
	    if List.all (fn x => Ty.same(V.ty x, ty)) xs
	      then ()
	      else (* error *)
	  end

  end