Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Diff of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml
ViewVC logotype

Diff of /sml/trunk/src/compiler/FLINT/kernel/ltykernel.sml

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

revision 53, Mon Mar 23 04:02:58 1998 UTC revision 60, Mon Mar 30 19:25:56 1998 UTC
# Line 399  Line 399 
399  fun tc_injX t = look(tc_table, wtoi(tc_hash t), t, tcI_eq, tc_mk)  fun tc_injX t = look(tc_table, wtoi(tc_hash t), t, tcI_eq, tc_mk)
400  fun lt_injX t = look(lt_table, wtoi(lt_hash t), t, ltI_eq, lt_mk)  fun lt_injX t = look(lt_table, wtoi(lt_hash t), t, ltI_eq, lt_mk)
401    
   
402  (** key-comparison on tkind, tyc, lty *)  (** key-comparison on tkind, tyc, lty *)
403  fun tk_cmp (k1, k2) = cmp(tk_table, k1, k2)  fun tk_cmp (k1, k2) = cmp(tk_table, k1, k2)
404  fun tc_cmp (t1, t2) = cmp(tc_table, t1, t2)  fun tc_cmp (t1, t2) = cmp(tc_table, t1, t2)
# Line 945  Line 944 
944   ***************************************************************************)   ***************************************************************************)
945    
946  (** testing the equality of values of tkind, tyc, lty *)  (** testing the equality of values of tkind, tyc, lty *)
947  fun eqlist (p, x::xs, y::ys) = (p(x,y)) andalso (eqlist(p, xs, ys))  fun eqlist p (x::xs, y::ys) = (p(x,y)) andalso (eqlist p (xs, ys))
948    | eqlist (p, [], []) = true    | eqlist p ([], []) = true
949    | eqlist _ = false    | eqlist _ _ = false
950    
951  (** testing the "pointer" equality on normalized tkind, tyc, and lty *)  (** testing the "pointer" equality on normalized tkind, tyc, and lty *)
952  fun tk_eq (x: tkind, y) = (x = y)  fun tk_eq (x: tkind, y) = (x = y)
# Line 957  Line 956 
956  (** testing the equivalence for arbitrary tkinds, tycs and ltys *)  (** testing the equivalence for arbitrary tkinds, tycs and ltys *)
957  val tk_eqv = tk_eq       (* all tkinds are normalized *)  val tk_eqv = tk_eq       (* all tkinds are normalized *)
958    
959  (** tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form *)  local (* tyc equivalence utilities *)
960  fun tc_eqv_gen (eqop1, eqop2, eqop3, eqop4) (t1, t2) =  (* The efficiency of checking FIX equivalence could probably be
961    (case (tc_outX t1, tc_outX t2)   * improved somewhat, but it doesn't seem so bad for my purposes right
962      of (TC_FN(ks1, b1), TC_FN(ks2, b2)) =>   * now.  Anyway, somebody might eventually want to do some profiling
963           (eqlist(tk_eqv, ks1, ks2)) andalso (eqop2(b1, b2))   * and improve this.  --league, 24 March 1998
964     *)
965    
966    (* Profiling code, temporary?? *)
967    structure Click =
968    struct
969        local
970            val s_unroll = Stats.makeStat "FIX unrolls"
971        in
972            fun unroll() = Stats.addStat s_unroll 1
973        end
974    end (* Click *)
975    
976    (** unrolling a fix, tyc -> tyc *)
977    fun tc_unroll_fix tyc =
978        case tc_outX tyc of
979            (TC_FIX((n,tc,ts),i)) => let
980                fun genfix i = tcc_fix ((n,tc,ts),i)
981                val fixes = List.tabulate(n, genfix)
982                val mu = tc
983                val mu = if null ts then mu
984                         else tcc_app (mu,ts)
985                val mu = tcc_app (mu, fixes)
986                val mu = if n=1 then mu
987                         else tcc_proj (mu, i)
988            in
989                Click.unroll();
990                mu
991            end
992          | _ => bug "unexpected non-FIX in tc_unroll_fix"
993    
994    (* In order to check equality of two FIXes, we need to be able to
995     * unroll them once, and check equality on the unrolled version, with
996     * an inductive assumption that they ARE equal.  The following code
997     * supports making and checking these inductive assumptions.
998     * Furthermore, we need to avoid unrolling any FIX more than once.
999     *)
1000    structure TcDict = BinaryDict
1001                           (struct
1002                               type ord_key = tyc
1003                               val cmpKey = tc_cmp
1004                           end)
1005    (* for each tyc in this dictionary, we store a dictionary containing
1006     * tycs that are assumed equivalent to it.
1007     *)
1008    type eqclass = unit TcDict.dict
1009    type hyp = eqclass TcDict.dict
1010    
1011    (* the null hypothesis, no assumptions about equality *)
1012    val empty_eqclass : eqclass = TcDict.mkDict()
1013    val null_hyp : hyp = TcDict.mkDict()
1014    
1015    (* add assumption t1=t2 to current hypothesis.  returns composite
1016     * hypothesis.
1017     *)
1018    fun assume_eq' (hyp, t1, t1eqOpt, t2) = let
1019        val t1eq  = case t1eqOpt of SOME e => e | NONE => empty_eqclass
1020        val t1eq' = TcDict.insert (t1eq, t2, ())
1021        val hyp'  = TcDict.insert (hyp, t1, t1eq')
1022    in
1023        hyp'
1024    end
1025    
1026    fun assume_eq (hyp, t1, t1eqOpt, t2, t2eqOpt) =
1027        assume_eq' (assume_eq' (hyp, t1, t1eqOpt, t2),
1028                    t2, t2eqOpt, t1)
1029    
1030    (* check whether t1=t2 according to the hypothesis *)
1031    val eq_by_hyp : eqclass option * tyc -> bool
1032        = fn (NONE, t2) => false
1033           | (SOME eqclass, t2) =>
1034             isSome (TcDict.peek (eqclass, t2))
1035    
1036    (* have we made any assumptions about `t' already? *)
1037    val visited : eqclass option -> bool
1038      = isSome
1039    
1040    (* tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form
1041     *     eqop1 is the default equality to be used for tycs
1042     *     eqop2 is used for body of FN, arguments in APP,
1043     *     eqop3 is used for ABS and BOX.
1044     *     eqop4 is used for arrow arguments and results
1045     * Each of these first takes the set of hypotheses.
1046     *)
1047    fun tc_eqv_gen (eqop1, eqop2, eqop3, eqop4) hyp (t1, t2) =
1048        case (tc_outX t1, tc_outX t2) of
1049            (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) =>
1050            if not (!Control.CG.checkDatatypes) then true
1051            else let
1052                val t1eqOpt = TcDict.peek (hyp, t1)
1053            in
1054                (* first check the induction hypothesis.  we only ever
1055                 * make hypotheses about FIX nodes, so this test is okay
1056                 * here.  if assume_eq appears in other cases, this
1057                 * test should be lifted outside the switch.
1058                 *)
1059                if eq_by_hyp (t1eqOpt, t2) then true
1060                (* next try structural eq on the components.  i'm not sure why
1061                 * this part is necessary, but it does seem to be... --league,
1062                 * 23 March 1998
1063                 *)
1064                else
1065                    (n1 = n2 andalso i1 = i2 andalso
1066                     eqop1 hyp (tc1, tc2) andalso
1067                     eqlist (eqop2 hyp) (ts1, ts2)) orelse
1068                    (* not equal by inspection; we have to unroll it.
1069                     * we prevent unrolling the same FIX twice by asking
1070                     * the `visited' function.
1071                     *)
1072                    if visited t1eqOpt then false
1073                    else let
1074                        val t2eqOpt = TcDict.peek (hyp, t2)
1075                    in
1076                        if visited t2eqOpt then false
1077                        else eqop1 (assume_eq (hyp, t1, t1eqOpt,
1078                                               t2, t2eqOpt))
1079                                   (tc_unroll_fix t1, tc_unroll_fix t2)
1080                    end
1081            end
1082          | (TC_FN(ks1, b1), TC_FN(ks2, b2)) =>
1083            eqlist tk_eqv (ks1, ks2) andalso eqop2 hyp (b1, b2)
1084       | (TC_APP(a1, b1), TC_APP(a2, b2)) =>       | (TC_APP(a1, b1), TC_APP(a2, b2)) =>
1085           (eqop1(a1, a2)) andalso (eqlist(eqop2, b1, b2))          eqop1 hyp (a1, a2) andalso eqlist (eqop2 hyp) (b1, b2)
1086       | (TC_SEQ ts1, TC_SEQ ts2) => eqlist(eqop1, ts1, ts2)        | (TC_SEQ ts1, TC_SEQ ts2) =>
1087       | (TC_SUM ts1, TC_SUM ts2) => eqlist(eqop1, ts1, ts2)          eqlist (eqop1 hyp) (ts1, ts2)
1088       | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) => eqlist(eqop1, ts1, ts2)        | (TC_SUM ts1, TC_SUM ts2) =>
1089       | (TC_ABS a, TC_ABS b) => eqop1(a, b)          eqlist (eqop1 hyp) (ts1, ts2)
1090       | (TC_ABS a, _) => eqop3(a, t2)        | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) =>
1091       | (_, TC_ABS b) => eqop3(t1, b)          eqlist (eqop1 hyp) (ts1, ts2)
1092       | (TC_BOX a, TC_BOX b) => eqop1(a, b)        | (TC_ABS a, TC_ABS b) =>
1093       | (TC_BOX a, _) => eqop3(a, t2)          eqop1 hyp (a, b)
1094       | (_, TC_BOX b) => eqop3(t1, b)        | (TC_ABS a, _) =>
1095            eqop3 hyp (a, t2)
1096          | (_, TC_ABS b) =>
1097            eqop3 hyp (t1, b)
1098          | (TC_BOX a, TC_BOX b) =>
1099            eqop1 hyp (a, b)
1100          | (TC_BOX a, _) =>
1101            eqop3 hyp (a, t2)
1102          | (_, TC_BOX b) =>
1103            eqop3 hyp (t1, b)
1104       | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) =>       | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) =>
1105           (token_eq(k1,k2)) andalso (eqop1(t1,t2))          token_eq(k1,k2) andalso eqop1 hyp (t1,t2)
1106       | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>       | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>
1107           (i1 = i2) andalso (eqop1(a1, a2))          i1 = i2 andalso eqop1 hyp (a1, a2)
1108       | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>       | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>
1109           (r1 = r2) andalso (eqop4(a1, a2)) andalso (eqop4(b1, b2))          r1 = r2 andalso eqop4 hyp (a1, a2) andalso eqop4 hyp (b1, b2)
1110       | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) =>       | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) =>
1111           (eqop1(a1, a2)) andalso (eqop1(b1, b2))          eqop1 hyp (a1, a2) andalso eqop1 hyp (b1, b2)
1112       | (TC_FIX((n1,tc1,ts1), i1), TC_FIX((n2,tc2,ts2), i2)) =>        | (TC_CONT ts1, TC_CONT ts2) =>
1113           true  (* INCORRECT: this is temporary (ZHONG) *)          eqlist (eqop1 hyp) (ts1, ts2)
1114       | (TC_CONT ts1, TC_CONT ts2) => eqlist(eqop1, ts1, ts2)        | _ => false
1115       | _ => false)  
1116    fun never h (t1,t2) = false
1117    
1118  fun tc_eqv (x as ref (_, _, AX_REG(true, _)),  (** general equality for tycs *)
1119    fun tc_eqv' hyp (x as ref (_, _, AX_REG(true, _)),
1120              y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y)              y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y)
1121    | tc_eqv (x, y) =    | tc_eqv' hyp (x, y) = let
1122        let val t1 = tc_whnm x          val t1 = tc_whnm x
1123            val t2 = tc_whnm y            val t2 = tc_whnm y
1124         in if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)      in
1125            else tc_eqv_gen (tc_eqv, tc_eqv, fn _ => false,          if tcp_norm t1 andalso tcp_norm t2 then tc_eq (t1, t2)
1126                             fn (ts1, ts2) => eqlist(tc_eqv, ts1, ts2)) (t1, t2)          else
1127        end (* function tc_eqv *)              tc_eqv_gen (tc_eqv', tc_eqv', never, eqlist o tc_eqv')
1128                           hyp (t1, t2)
1129        end (* tc_eqv' *)
1130    
1131  fun tc_eqv_x (x, y) =  (* slightly relaxed constraints (???) *)
1132    fun tc_eqv_x' hyp (x, y) =
1133    let val t1 = tc_whnm x    let val t1 = tc_whnm x
1134        val t2 = tc_whnm y        val t2 = tc_whnm y
1135     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
1136         else false) orelse         else false) orelse
1137         (tc_eqv_gen (tc_eqv_x, tc_eqv_x, fn _ => false,         (tc_eqv_gen (tc_eqv_x', tc_eqv_x', never, eqlist o tc_eqv_x')
1138                      fn (ts1, ts2) => eqlist(tc_eqv_x, ts1, ts2)) (t1, t2))                     hyp (t1, t2))
1139    end (* function tc_eqv_x *)    end (* function tc_eqv_x *)
1140    
1141  (** testing the equivalence of two tycs with relaxed constraints *)  (** testing the equivalence of two tycs with relaxed constraints *)
1142  fun tc_eqv_bx (x : tyc, y) =  fun mkeqop4 eqop1 hyp (ts1, ts2) =
1143        eqop1 hyp (tc_autotuple ts1, tc_autotuple ts2)
1144    
1145    fun tc_eqv_bx' hyp (x : tyc, y) =
1146    let val t1 = tc_whnm x    let val t1 = tc_whnm x
1147        val t2 = tc_whnm y        val t2 = tc_whnm y
1148     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
1149        else false) orelse        else false) orelse
1150        (tc_eqv_gen (tc_eqv_bx, tc_eqv_sp, fn _ => false,        (tc_eqv_gen (tc_eqv_bx', tc_eqv_sp', never,
1151                     fn (ts1, ts2) => tc_eqv_bx(tc_autotuple ts1,                     mkeqop4 tc_eqv_bx')
1152                                                tc_autotuple ts2)) (t1, t2))                    hyp (t1, t2))
1153    end (* function tc_eqv_bx *)    end (* function tc_eqv_bx *)
1154    
1155  and tc_eqv_sp (x : tyc, y) =  and tc_eqv_sp' hyp (x : tyc, y) =
1156    let val t1 = tc_whnm x    let val t1 = tc_whnm x
1157        val t2 = tc_whnm y        val t2 = tc_whnm y
1158     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
1159        else false) orelse        else false) orelse
1160        (tc_eqv_gen (tc_eqv_sp, tc_eqv_sp, tc_eqv_sp,        (tc_eqv_gen (tc_eqv_sp', tc_eqv_sp', tc_eqv_sp',
1161                     fn (ts1, ts2) => tc_eqv_sp(tc_autotuple ts1,                     mkeqop4 tc_eqv_sp')
1162                                                tc_autotuple ts2)) (t1, t2))                    hyp (t1, t2))
1163    end (* function tc_eqv_sp *)    end (* function tc_eqv_sp *)
1164    
1165  (*  in (* tyc equivalence utilities *)
1166   * all the complexity of lt_eqv comes from the partial-structure (or  
1167   * partial record) type (the LT_PST type). If we can remove LT_PST  (* TODO: explain the precise difference between these three notions of
1168   * type, then the following can be considerabily simplified. (ZHONG)   * equality!  --league
1169   *)   *)
1170    val tc_eqv = tc_eqv' null_hyp
1171    val tc_eqv_x = tc_eqv_x' null_hyp
1172    val tc_eqv_bx = tc_eqv_bx' null_hyp
1173    
1174    end (* tyc equivalence utilities *)
1175    
1176  (** lt_eqv_generator, invariant: x and y are in the wh-normal form *)  (** lt_eqv_generator, invariant: x and y are in the wh-normal form *)
1177  fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) =  fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) =
# Line 1050  Line 1191 
1191        fun seq (t1, t2) =        fun seq (t1, t2) =
1192          (case (lt_outX t1, lt_outX t2)          (case (lt_outX t1, lt_outX t2)
1193            of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) =>            of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) =>
1194                 (eqlist(tk_eqv, ks1, ks2)) andalso (eqlist(eqop1, b1, b2))                 (eqlist tk_eqv (ks1, ks2)) andalso (eqlist eqop1 (b1, b2))
1195             | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) =>             | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) =>
1196                 (eqlist(eqop1, as1, as2)) andalso (eqlist(eqop1, bs1, bs2))                 (eqlist eqop1 (as1, as2)) andalso (eqlist eqop1 (bs1, bs2))
1197             | (LT_TYC a, LT_TYC b) => eqop2(a, b)             | (LT_TYC a, LT_TYC b) => eqop2(a, b)
1198             | (LT_STR s1, LT_STR s2) => eqlist(eqop1, s1, s2)             | (LT_STR s1, LT_STR s2) => eqlist eqop1 (s1, s2)
1199             | (LT_PST s1, LT_PST s2) => pp(s1, s2)             | (LT_PST s1, LT_PST s2) => pp(s1, s2)
1200             | (LT_PST s1, LT_STR s2) => sp(s2, s1)             | (LT_PST s1, LT_STR s2) => sp(s2, s1)
1201             | (LT_STR s1, LT_PST s2) => sp(s1, s2)             | (LT_STR s1, LT_PST s2) => sp(s1, s2)
1202             | (LT_CONT s1, LT_CONT s2) => eqlist(eqop1, s1, s2)             | (LT_CONT s1, LT_CONT s2) => eqlist eqop1 (s1, s2)
1203             | _ => false)             | _ => false)
1204     in seq(x, y)     in seq(x, y)
1205    end (* function lt_eqv_gen *)    end (* function lt_eqv_gen *)

Legend:
Removed from v.53  
changed lines
  Added in v.60

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