Home My Page Projects Code Snippets Project Openings diderot
Summary Activity Tracker Tasks SCM

SCM Repository

[diderot] Diff of /branches/vis12/src/compiler/typechecker/util.sml
ViewVC logotype

Diff of /branches/vis12/src/compiler/typechecker/util.sml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 1685, Sun Jan 22 15:23:36 2012 UTC revision 1687, Wed Jan 25 13:02:32 2012 UTC
# Line 4  Line 4 
4   * All rights reserved.   * All rights reserved.
5   *   *
6   * Utilities for typechecking   * Utilities for typechecking
7     *
8     * TODO:
9     *      coercions to lift integers to reals
10     *      coercions to lift fixed-sized sequences to dynamic-sized sequences
11   *)   *)
12    
13  structure Util : sig  structure Util : sig
14    
15      val matchType : Types.ty * Types.ty -> bool    (* when matching two types (ty1 and ty2), there are three possible outcomes:
16      val matchTypes : Types.ty list * Types.ty list -> bool     *   EQ       -- types are equal
17       *   COERCE   -- ty2 can be coerced to match ty1 (e.g., int -> float, fixed seq -> dynamic seq)
18       *   FAIL     -- types do not match
19       *)
20        datatype match = EQ | COERCE | FAIL
21    
22        val matchType : Types.ty * Types.ty -> match
23    
24        val equalType : Types.ty * Types.ty -> bool
25        val equalTypes : Types.ty list * Types.ty list -> bool
26    
27      val tryMatchType : Types.ty * Types.ty -> bool      val tryMatchType : Types.ty * Types.ty -> bool
28      val tryMatchTypes : Types.ty list * Types.ty list -> bool      val tryMatchTypes : Types.ty list * Types.ty list -> bool
29    
30      val instantiate : Types.scheme -> (Types.meta_var list * Types.ty)      val instantiate : Types.scheme -> (Types.meta_var list * Types.ty)
31    
32      val matchDim : Types.dim * Types.dim -> bool      val equalDim : Types.dim * Types.dim -> bool
33    
34    end = struct    end = struct
35    
# Line 24  Line 37 
37      structure MV = MetaVar      structure MV = MetaVar
38      structure TU = TypeUtil      structure TU = TypeUtil
39    
40        datatype match = EQ | COERCE | FAIL
41    
42    (* a patch list tracks the meta variables that have been updated so that we can undo    (* a patch list tracks the meta variables that have been updated so that we can undo
43     * the effects of unification when just testing for a possible type match.     * the effects of unification when just testing for a possible type match.
44     *)     *)
# Line 58  Line 73 
73            end            end
74    
75  (* FIXME: what about the bounds? *)  (* FIXME: what about the bounds? *)
76      fun matchDiff (pl, diff1, diff2) = (case (TU.pruneDiff diff1, TU.pruneDiff diff2)      fun equalDiff (pl, diff1, diff2) = (case (TU.pruneDiff diff1, TU.pruneDiff diff2)
77             of (Ty.DiffConst k1, Ty.DiffConst k2) => (k1 = k2)             of (Ty.DiffConst k1, Ty.DiffConst k2) => (k1 = k2)
78              | (Ty.DiffConst k, Ty.DiffVar(dv, i)) => let              | (Ty.DiffConst k, Ty.DiffVar(dv, i)) => let
79                  val k' = k+i                  val k' = k+i
# Line 75  Line 90 
90              | (Ty.DiffVar(dv1, i1), Ty.DiffVar(dv2, i2)) => raise Fail "unimplemented" (* FIXME *)              | (Ty.DiffVar(dv1, i1), Ty.DiffVar(dv2, i2)) => raise Fail "unimplemented" (* FIXME *)
91            (* end case *))            (* end case *))
92    
93      fun matchDim (pl, dim1, dim2) = (case (TU.pruneDim dim1, TU.pruneDim dim2)    (* match two differentiation constants where the first is allowed to be less than the second *)
94        fun matchDiff (diff1, diff2) = (case (TU.pruneDiff diff1, TU.pruneDiff diff2)
95               of (Ty.DiffConst k1, Ty.DiffConst k2) => (k1 <= k2)
96                | _ => raise Fail "unimplemented" (* FIXME *)
97              (* end case *))
98    
99        fun equalDim (pl, dim1, dim2) = (case (TU.pruneDim dim1, TU.pruneDim dim2)
100             of (Ty.DimConst d1, Ty.DimConst d2) => (d1 = d2)             of (Ty.DimConst d1, Ty.DimConst d2) => (d1 = d2)
101              | (Ty.DimVar dv, dim2) => (bindDimVar(pl, dv, dim2); true)              | (Ty.DimVar dv, dim2) => (bindDimVar(pl, dv, dim2); true)
102              | (dim1, Ty.DimVar dv) => (bindDimVar(pl, dv, dim1); true)              | (dim1, Ty.DimVar dv) => (bindDimVar(pl, dv, dim1); true)
103            (* end case *))            (* end case *))
104    
105      fun matchShape (pl, shape1, shape2) = (case (TU.pruneShape shape1, TU.pruneShape shape2)      fun equalShape (pl, shape1, shape2) = (case (TU.pruneShape shape1, TU.pruneShape shape2)
106             of (Ty.Shape dd1, Ty.Shape dd2) => let             of (Ty.Shape dd1, Ty.Shape dd2) => let
107                  fun chk ([], []) = true                  fun chk ([], []) = true
108                    | chk (d1::dd1, d2::dd2) = matchDim(pl, d1, d2) andalso chk (dd1, dd2)                    | chk (d1::dd1, d2::dd2) = equalDim(pl, d1, d2) andalso chk (dd1, dd2)
109                    | chk _ = false                    | chk _ = false
110                  in                  in
111                    chk (dd1, dd2)                    chk (dd1, dd2)
# Line 92  Line 113 
113              | (Ty.Shape dd, Ty.ShapeExt(shape, d2)) => let              | (Ty.Shape dd, Ty.ShapeExt(shape, d2)) => let
114                  fun chk ([], _) = false                  fun chk ([], _) = false
115                    | chk ([d], revDD) =                    | chk ([d], revDD) =
116                        matchDim(pl, d, d2) andalso matchShape(pl, Ty.Shape(List.rev revDD), shape)                        equalDim(pl, d, d2) andalso equalShape(pl, Ty.Shape(List.rev revDD), shape)
117                    | chk (d::dd, revDD) = chk(dd, d::revDD)                    | chk (d::dd, revDD) = chk(dd, d::revDD)
118                  in                  in
119                    chk (dd, [])                    chk (dd, [])
120                  end                  end
121              | (Ty.ShapeVar sv, shape) => (bindShapeVar (pl, sv, shape); true)              | (Ty.ShapeVar sv, shape) => (bindShapeVar (pl, sv, shape); true)
122              | (Ty.ShapeExt(shape1, d1), Ty.ShapeExt(shape2, d2)) =>              | (Ty.ShapeExt(shape1, d1), Ty.ShapeExt(shape2, d2)) =>
123                  matchDim(pl, d1, d2) andalso matchShape(pl, shape1, shape2)                  equalDim(pl, d1, d2) andalso equalShape(pl, shape1, shape2)
124              | (shape1, shape2) => matchShape(pl, shape2, shape1)              | (shape1, shape2) => equalShape(pl, shape2, shape1)
125          (* end case *))          (* end case *))
126    
127  (* QUESTION: do we need an occurs check? *)  (* QUESTION: do we need an occurs check? *)
# Line 125  Line 146 
146              | match (Ty.T_Int, Ty.T_Int) = true              | match (Ty.T_Int, Ty.T_Int) = true
147              | match (Ty.T_String, Ty.T_String) = true              | match (Ty.T_String, Ty.T_String) = true
148              | match (Ty.T_Sequence(ty1, d1), Ty.T_Sequence(ty2, d2)) =              | match (Ty.T_Sequence(ty1, d1), Ty.T_Sequence(ty2, d2)) =
149                  matchDim(pl, d1, d2) andalso match(ty1, ty2)                  equalDim(pl, d1, d2) andalso match(ty1, ty2)
150              | match (Ty.T_Kernel k1, Ty.T_Kernel k2) = matchDiff (pl, k1, k2)              | match (Ty.T_DynSequence ty1, Ty.T_DynSequence ty2) = match(ty1, ty2)
151              | match (Ty.T_Tensor s1, Ty.T_Tensor s2) = matchShape (pl, s1, s2)              | match (Ty.T_Kernel k1, Ty.T_Kernel k2) = equalDiff (pl, k1, k2)
152                | match (Ty.T_Tensor s1, Ty.T_Tensor s2) = equalShape (pl, s1, s2)
153              | match (Ty.T_Image{dim=d1, shape=s1}, Ty.T_Image{dim=d2, shape=s2}) =              | match (Ty.T_Image{dim=d1, shape=s1}, Ty.T_Image{dim=d2, shape=s2}) =
154                  matchDim (pl, d1, d2) andalso matchShape(pl, s1, s2)                  equalDim (pl, d1, d2) andalso equalShape(pl, s1, s2)
155              | match (Ty.T_Field{diff=k1, dim=d1, shape=s1}, Ty.T_Field{diff=k2, dim=d2, shape=s2}) =              | match (Ty.T_Field{diff=k1, dim=d1, shape=s1}, Ty.T_Field{diff=k2, dim=d2, shape=s2}) =
156                  matchDiff (pl, k1, k2) andalso matchDim (pl, d1, d2) andalso matchShape(pl, s1, s2)                  equalDiff (pl, k1, k2) andalso equalDim (pl, d1, d2) andalso equalShape(pl, s1, s2)
157              | match (Ty.T_Fun(tys11, ty12), Ty.T_Fun(tys21, ty22)) =              | match (Ty.T_Fun(tys11, ty12), Ty.T_Fun(tys21, ty22)) =
158                  ListPair.allEq match (tys11, tys21) andalso match (ty12, ty22)                  ListPair.allEq match (tys11, tys21) andalso match (ty12, ty22)
159              | match _ = false              | match _ = false
# Line 139  Line 161 
161              match (TU.pruneHead ty1, TU.pruneHead ty2)              match (TU.pruneHead ty1, TU.pruneHead ty2)
162            end            end
163    
164      fun matchTypes (tys1, tys2) = let      fun equalTypes (tys1, tys2) = let
165            val pl = ref[]            val pl = ref[]
166            in            in
167              ListPair.allEq (fn (ty1, ty2) => unifyType(pl, ty1, ty2)) (tys1, tys2)              ListPair.allEq (fn (ty1, ty2) => unifyType(pl, ty1, ty2)) (tys1, tys2)
168            end            end
169    
170      fun matchType (ty1, ty2) = unifyType (ref[], ty1, ty2)      fun equalType (ty1, ty2) = unifyType (ref[], ty1, ty2)
171    
172    (* TODO: add removal of differentiation *)
173        fun matchType (ty1, ty2) = (case (TU.pruneHead ty1, TU.pruneHead ty2)
174               of (Ty.T_Tensor(Ty.Shape[]), Ty.T_Int) => COERCE
175                | (Ty.T_DynSequence ty1, Ty.T_Sequence(ty2, _)) =>
176                    if equalType(ty1, ty2) then COERCE else FAIL
177                | (Ty.T_Field{diff=k1, dim=d1, shape=s1}, Ty.T_Field{diff=k2, dim=d2, shape=s2}) =>
178                    if equalType (ty1, ty2)
179                      then EQ
180                    else if matchDiff (k1, k2) andalso equalDim(ref[], d1, d2)
181                    andalso equalShape(ref[], s1, s2)
182                      then COERCE
183                      else FAIL
184                | (ty1, ty2) => if equalType(ty1, ty2) then EQ else FAIL
185              (* end case *))
186    
187    (* try to match types; if we fail, all meta-variable bindings are undone *)    (* try to match types; if we fail, all meta-variable bindings are undone *)
188      fun tryMatchType (ty1, ty2) = let      fun tryMatchType (ty1, ty2) = let
# Line 162  Line 199 
199              orelse (undo pl; false)              orelse (undo pl; false)
200            end            end
201    
202    (* rebind matchDim without patch-list argument *)    (* rebind equalDim without patch-list argument *)
203      val matchDim = fn (d1, d2) => matchDim(ref [], d1, d2)      val equalDim = fn (d1, d2) => equalDim(ref [], d1, d2)
204    
205  (* QUESTION: perhaps this function belongs in the TypeUtil module? *)  (* QUESTION: perhaps this function belongs in the TypeUtil module? *)
206    (* instantiate a type scheme, returning the argument meta variables and the resulting type.    (* instantiate a type scheme, returning the argument meta variables and the resulting type.

Legend:
Removed from v.1685  
changed lines
  Added in v.1687

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0