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

SCM Repository

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

Diff of /branches/charisee/src/compiler/typechecker/typechecker.sml

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

revision 2925, Tue Mar 3 22:00:11 2015 UTC revision 2926, Tue Mar 3 22:38:29 2015 UTC
# Line 288  Line 288 
288                       * system cannot express the constraint that the type is                       * system cannot express the constraint that the type is
289                       *     ALL[sigma1, d1, sigma2] . tensor[sigma1, d1] * tensor[d1, sigma2] -> tensor[sigma1, sigma2]                       *     ALL[sigma1, d1, sigma2] . tensor[sigma1, d1] * tensor[d1, sigma2] -> tensor[sigma1, sigma2]
290                       *)                       *)
291                      then (case (TU.prune ty1, TU.prune ty2)                      then let
                        of (Ty.T_Tensor(s1 as Ty.Shape(dd1 as _::_)), Ty.T_Tensor(s2 as Ty.Shape(d2::dd2))) => let  
                             val (dd1, d1) = let  
292                                    fun splitLast (prefix, [d]) = (List.rev prefix, d)                                    fun splitLast (prefix, [d]) = (List.rev prefix, d)
293                                      | splitLast (prefix, d::dd) = splitLast (d::prefix, dd)                                      | splitLast (prefix, d::dd) = splitLast (d::prefix, dd)
294                                      | splitLast (_, []) = raise Fail "impossible"                                      | splitLast (_, []) = raise Fail "impossible"
295                                    in                                    in
296                                      splitLast ([], dd1)                          case (TU.prune ty1, TU.prune ty2)
297                                    end                          (* tensor * tensor inner product *)
298                             of (Ty.T_Tensor(s1 as Ty.Shape(dd1 as _::_)), Ty.T_Tensor(s2 as Ty.Shape(d2::dd2))) => let
299                                  val (dd1, d1) = splitLast ([], dd1)
300                              val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner_tt)                              val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner_tt)
301                              val resTy = Ty.T_Tensor(Ty.Shape(dd1@dd2))                              val resTy = Ty.T_Tensor(Ty.Shape(dd1@dd2))
302                              in                              in
# Line 309  Line 309 
309                                      S "  found: ", TYS[ty1, ty2], S "\n"                                      S "  found: ", TYS[ty1, ty2], S "\n"
310                                    ])                                    ])
311                              end                              end
312                          (* made Field Check for Inner product*)                          (* tensor * field inner product *)
313                      |  (Ty.T_Field{diff=k1, dim=dim1, shape=s1 as Ty.Shape(dd1 as _::_)},                            | ( Ty.T_Tensor(s1 as Ty.Shape(dd1 as _::_)),
314                          Ty.T_Field{diff=k2, dim=dim2, shape=s2 as Ty.Shape(d2::dd2)} )=> let                                Ty.T_Field{diff, dim, shape=s2 as Ty.Shape(d2::dd2)}
315                                ) => let
316                          val (dd1, d1) = let                                val (dd1, d1) = splitLast ([], dd1)
317                              fun splitLast (prefix, [d]) = (List.rev prefix, d)                                val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner_tf)
318                              | splitLast (prefix, d::dd) = splitLast (d::prefix, dd)                                val resTy = Ty.T_Field{diff=diff, dim=dim, shape=Ty.Shape(dd1@dd2)}
                             | splitLast (_, []) = raise Fail "impossible"  
319                              in                              in
320                                  splitLast ([], dd1)                                  if U.equalDim(d1, d2)
                             end  
                         val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner_ff)  
                           (*val _=print(String.concat["\n F-dot-F\nrngTy",TypeUtil.toString rngTy])*)  
                         val resTy= Ty.T_Field{diff=k1, dim=dim1, shape=Ty.Shape(dd1@dd2)}  
                          (* val _=print(String.concat["\n rresTy",TypeUtil.toString resTy])*)  
   
                         in  
                             if U.equalDim(d1, d1)  
                               (*andalso U.matchDiff (k1, k2)*)  
                                 andalso U.equalDim(dim1, dim2)  
321                                  andalso U.equalTypes(domTy, [ty1, ty2])                                  andalso U.equalTypes(domTy, [ty1, ty2])
322                                  andalso U.equalType(rngTy, resTy)                                  andalso U.equalType(rngTy, resTy)
323                                  then (AST.E_Apply(BV.op_inner_ff, tyArgs, [e1', e2'], rngTy), rngTy)                                    then (AST.E_Apply(BV.op_inner_tf, tyArgs, [e1', e2'], rngTy), rngTy)
324                              else err (cxt, [                              else err (cxt, [
325                                  S "type error for arguments of binary operator \"•\"\n",                                  S "type error for arguments of binary operator \"•\"\n",
326                                  S "  found: ", TYS[ty1, ty2], S "\n"])                                        S "  found: ", TYS[ty1, ty2], S "\n"
327                                        ])
328                              end                              end
329                            (* field * tensor inner product *)
330                  |   (Ty.T_Field{diff=k1, dim=dim1, shape=s1}, Ty.T_Tensor _ )=> let                            | ( Ty.T_Field{diff, dim, shape=s1 as Ty.Shape(dd1 as _::_)},
331                                  Ty.T_Tensor(s2 as Ty.Shape(d2::dd2))
332                                ) => let
333                                  val (dd1, d1) = splitLast ([], dd1)
334                          val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner_ft)                          val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner_ft)
335                                  val resTy = Ty.T_Field{diff=diff, dim=dim, shape=Ty.Shape(dd1@dd2)}
336                          in                          in
337                              (AST.E_Apply(BV.op_inner_ft, tyArgs, [e1', e2'], rngTy), rngTy)                                  if U.equalDim(d1, d2)
338                                    andalso U.equalTypes(domTy, [ty1, ty2])
339                                    andalso U.equalType(rngTy, resTy)
340                                      then (AST.E_Apply(BV.op_inner_ft, tyArgs, [e1', e2'], rngTy), rngTy)
341                                      else err (cxt, [
342                                          S "type error for arguments of binary operator \"•\"\n",
343                                          S "  found: ", TYS[ty1, ty2], S "\n"
344                                        ])
345                          end                          end
346                            (* field * field inner product *)
   
                 (*  
347                      |  (Ty.T_Field{diff=k1, dim=dim1, shape=s1 as Ty.Shape(dd1 as _::_)},                      |  (Ty.T_Field{diff=k1, dim=dim1, shape=s1 as Ty.Shape(dd1 as _::_)},
348                          Ty.T_Tensor(s2 as Ty.Shape(d2::dd2) ))=> let                                Ty.T_Field{diff=k2, dim=dim2, shape=s2 as Ty.Shape(d2::dd2)}
349                              val dd1=[3]                              ) => let
350                                  val (dd1, d1) = splitLast ([], dd1)
351                              val (dd1, d1) = let                                val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner_ff)
                                     fun splitLast (prefix, [d]) = (List.rev prefix, d)  
                                     | splitLast (prefix, d::dd) = splitLast (d::prefix, dd)  
                                     | splitLast (_, []) = raise Fail "impossible"  
                                 in  
                                     splitLast ([], dd1)  
                                 end  
   
                             val (tyArgs, Ty.T_Fun(domTy, rngTy)) = Util.instantiate(Var.typeOf BV.op_inner_ft)  
                             in  
                                 (AST.E_Apply(BV.op_inner_ft, tyArgs, [e1', e2'], rngTy), rngTy)  
                             end  
   
352                              val resTy= Ty.T_Field{diff=k1, dim=dim1, shape=Ty.Shape(dd1@dd2)}                              val resTy= Ty.T_Field{diff=k1, dim=dim1, shape=Ty.Shape(dd1@dd2)}
   
   
353                              in                              in
354                                  if U.equalDim(d1, d1)                                  if U.equalDim(d1, d1)
355                                    andalso U.equalDiff(k1, k2)
356                                    andalso U.equalDim(dim1, dim2)
357                                  andalso U.equalTypes(domTy, [ty1, ty2])                                  andalso U.equalTypes(domTy, [ty1, ty2])
358                                  andalso U.equalType(rngTy, resTy)                                  andalso U.equalType(rngTy, resTy)
359                                  then (AST.E_Apply(BV.op_inner_ft, tyArgs, [e1', e2'], rngTy), rngTy)                                    then (AST.E_Apply(BV.op_inner_ff, tyArgs, [e1', e2'], rngTy), rngTy)
360                          else err (cxt, [                          else err (cxt, [
361                                      S "type error for arguments of binary operator \"•\"\n",                                      S "type error for arguments of binary operator \"•\"\n",
362                                      S "  found: ", TYS[ty1, ty2], S "\n"])                                      S "  found: ", TYS[ty1, ty2], S "\n"])
363                                  end
                             end*)  
364                      | (ty1, ty2) => err (cxt, [                      | (ty1, ty2) => err (cxt, [
365                                S "type error for arguments of binary operator \"•\"\n",                                S "type error for arguments of binary operator \"•\"\n",
366                                S " found: ", TYS[ty1, ty2], S "\n"                                S " found: ", TYS[ty1, ty2], S "\n"
367                              ])                              ])
368                        (* end case *))                          (* end case *)
369                          end
370                    else if Atom.same(rator, BasisNames.op_colon)                    else if Atom.same(rator, BasisNames.op_colon)
371                      then (case (TU.prune ty1, TU.prune ty2)                      then (case (TU.prune ty1, TU.prune ty2)
372                         of (Ty.T_Tensor(s1 as Ty.Shape(dd1 as _::_::_)),                         of (Ty.T_Tensor(s1 as Ty.Shape(dd1 as _::_::_)),

Legend:
Removed from v.2925  
changed lines
  Added in v.2926

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