SCM Repository

[smlnj] Diff of /sml/branches/primop-branch-3/compiler/Elaborator/types/unify.sml

[smlnj] / sml / branches / primop-branch-3 / compiler / Elaborator / types / unify.sml

Diff of /sml/branches/primop-branch-3/compiler/Elaborator/types/unify.sml

-revision 2528, Wed May  9 20:36:39 2007 UTC
+revision 2529, Wed May  9 23:22:59 2007 UTC
 Line 184
                 * against which we are unifying/instantiating
                 * Because we may be instantiating to nonstrict
                 * univariables, it is safer to do an occurrence
-                * check on all the arguments.
+                * check on all the arguments. (typing/tests/20.sml)
                 * [GK 4/28/07] *)
            | iter eq (CONty(tycon,args)) =
                (case tyconEqprop tycon
 Line 231
          val type2 = TU.prune type2
          val _ = debugPPType(">>unifyTy: type1: ",type1)
          val _ = debugPPType(">>unifyTy: type2: ",type2)
-         fun unifyRaw(type1, type2) = (* unify without reducing CONty(DEFtycs) *)
+         fun unifyRaw(type1, type2) =
              case (type1, type2)
            of (VARty var1,VARty var2) =>
                 unifyTyvars(var1,var2)  (* used to take type1 and type2 as args *)
-            | (VARty var1,etype2) => (* etype2 may be WILDCARDty *)
+            | (VARty var1, _) => (* type2 may be WILDCARDty *)
-                instTyvar(var1,type2,etype2)
+                instTyvar(var1,type2)
-            | (etype1,VARty var2) => (* etype1 may be WILDCARDty *)
+            | (_, VARty var2) => (* type1 may be WILDCARDty *)
-                instTyvar(var2,type1,etype1)
+                instTyvar(var2,type1)
             | (CONty(tycon1,args1),CONty(tycon2,args2)) =>
                 if TU.eqTycon(tycon1,tycon2) then
                     (* Because tycons are equal, they must have the
 Line 269
             | (WILDCARDty,_) => ()
             | (_,WILDCARDty) => ()
             | tys => raise Unify (TYP tys)
-     in unifyRaw(type1, type2)
+     in (* first try unifying without reducing CONty(DEFtycs) *)
-        handle Unify _ => (* try reducing CONty(DEFtyc, _) to make types equal *)
+        unifyRaw(type1, type2)
+        handle Unify _ =>
+          (* try head reducing type1 *)
                let val type1' = TU.headReduceType type1
                in unifyRaw(type1', type2)
-                  handle Unify _ => (* try reducing type2 *)
+             handle Unify _ => (* try head reducing type2 *)
                          unifyRaw(type1', TU.headReduceType type2)
                          (* if unification still fails, then type1 and type2
                             really cannot be made to be equal *)
-Line 356
+Line 358
          else unify(sortVars(var1,var2))
      end
- and instTyvar (var as ref(OPEN{kind=META,depth,eq}),ty,ety) =
+ (* instTyvar: tyvar * ty -> unit
-       (case ety
+  * instTyvar(tv,ty) -- instantiate tyvar tv to type ty.
+  * ty is not necessarily head normal form.
+  * ASSERT: ty is not a VARty (otherwise unifyTyvars would have been
+  * used instead. *)
+ and instTyvar (var as ref(OPEN{kind=META,depth,eq}),ty) =
+       (case ty
           of WILDCARDty => ()
-           | _ => adjustType(var,depth,eq,ety);
+           | _ => adjustType(var,depth,eq,ty);
         debugPPType("instTyvar ", VARty var);
         debugPPType("instTyvar to ", ty);
         (* Also need to check for circularity with ty here *)
         var := INSTANTIATED ty)
-   | instTyvar (var as ref(OPEN{kind=FLEX fields,depth,eq}),ty,ety) =
+   | instTyvar (var as ref(OPEN{kind=FLEX fields,depth,eq}),ty) =
-       (case ety
+       let val ty' = readReduceType ty (* try to reduce to a record type *)
+        in case ty'
           of CONty(RECORDtyc field_names, field_types) =>
                let val record_fields = ListPair.zip (field_names,field_types)
                 in app (fn t => adjustType(var,depth,eq,t)) field_types;
-Line 375
+Line 383
                end
            | WILDCARDty => (* propagate WILDCARDty to the fields *)
                (app (fn (lab,ty) => unifyTy(WILDCARDty,ty)) fields)
-           | _ => raise Unify (TYP(VARty(var), ety)))
+             | _ => raise Unify (TYP(VARty(var), ty))
+       end
-   | instTyvar (var as ref(i as SCHEME eq),ty,ety) =
+   | instTyvar (var as ref(i as SCHEME eq),ty) =
-       (adjustType(var,infinity,eq,ety);
+       let val ty' = readReduceType ty
-        var := INSTANTIATED ty)
+        in case ty'
+             of VARty var1 => unifyTyvars(var, var1)
+              | _ => adjustType(var,infinity,eq,ty');
+           var := INSTANTIATED ty'
+       end
-   | instTyvar (var as ref(i as LITERAL{kind,...}),ty,ety) =
+   | instTyvar (var as ref(i as LITERAL{kind,...}),ty) =
-       (case ety
+       (case headReduceType ty
           of WILDCARDty => ()
-           | _ =>
+           | ty' =>
-              if OLL.isLiteralTy(kind,ety)
+              if OLL.isLiteralTy(kind,ty')
               then var := INSTANTIATED ty
               else raise Unify (LIT i))   (* could return the ty for error msg*)
-   | instTyvar (ref(i as UBOUND _),_,ety) =
+   | instTyvar (ref(i as UBOUND _),ty) =
-       (case ety
+       (case ty
           of WILDCARDty => ()
            | _ =>  raise Unify (UBV i))   (* could return the ty for error msg*)

 Legend:



Removed from v.2528
 


changed lines


 
Added in v.2529
 Legend:



Removed from v.2528
 


changed lines


 
Added in v.2529
-Removed from v.2528
+Added in v.2529

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