(* util.sml
 *
 * COPYRIGHT (c) 2010 The Diderot Project (http://diderot.cs.uchicago.edu)
 * All rights reserved.
 *
 * Utilities for typechecking
 *)

structure Util =
  struct

    structure Ty = Types

  (* prune out instantiated meta variables from a type *)
    fun prune ty = let
	  fun pruneDiff (Ty.DiffVar(Dfv{bind=ref(SOME diff), ...}, i)) = (
		case pruneDiff diff
		 of Ty.DiffVar(dv, i') => Ty.DiffVar(dv, i+i')
		  | Ty.DiffConst i' => Ty.DiffConst(i+i')
		(* end case *))
	    | prunDiff diff = diff
	  fun pruneDim dim = (case dim
		 of Ty.DimVar(Ty.DV{bind=ref(SOME dim), ...}) => pruneDim dim
		  | dim => dim
		(* end case *))
	  fun pruneShape shape = (case shape
		 of ShapeVar(Ty.SV{bind=ref(SOME shape), ...}) => pruneShape shape
		  | ShapeExt(shape, dim) => ShapeExt(pruneShape shape, pruneDim dim)
		  | _ => shape
		(* end case *))
	  fun prune' (ty as Ty.T_Var(Ty.TV{bind, ...})) = (case !bind
		 of NONE => ty
		  | SOME ty => prune' ty
		(* end case *))
	    | prune' (Ty.T_Kernel diff) = Ty.T_Kernel(pruneDiff diff)
	    | prune' (Ty.T_Tensor shape) = Ty.T_Tensor(pruneShape shape)
	    | prune' (Ty.T_Image{dim, shape}) = Ty.T_Image{
		  dim = pruneDim dim,
		  shape = pruneShape shape
		}
	    | prune' (Ty.T_Field{diff, dim, shape}) = Ty.T_Field{
		  diff = pruneDiff diff,
		  dim = pruneDim dim,
		  shape = pruneShape shape
		}
	    | prune' (Ty.T_Fun(tys1, tys2)) = Ty.T_Fun(List.map prune' tys1, List.map prune' tys2)
	    | prune' ty = ty
	  in
	    prune' ty
	  end

    fun matchTypes (ty1, ty2) = let
	  fun match (Ty.T_Var tv1, Ty.T_Var tv2) =
	    | match (Ty.T_Var tv1, ty2) =
	    | match (ty1, Ty.T_Var tv2) =
	    | match (Ty.T_Bool, Ty.T_Bool) = true
	    | match (Ty.T_Int, Ty.T_Int) = true
	    | match (Ty.T_String, Ty.T_String) = true
	    | match (Ty.T_Kernel d1, Ty.T_Kernel d2) =
	    | match (Ty.T_Tensor s1, Ty.T_Tensor s2) =
	    | match (Ty.T_Image{dim=d1, shape=s1}, Ty.T_Image{dim=d2, shape=s2}) =
	    | match (Ty.T_Field{diff=k1, dim=d1, shape=s1}, Ty.T_Field{diff=k2, dim=d2, shape=s2}) =
	    | match (Ty.T_Fun(tys11, tys22), Ty.T_Fun(tys21, tys22)) =
	    | match _ = false
	  in
	    match (prune ty1, prune ty2)
	  end

  end