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/branches/SMLNJ/src/compiler/FLINT/kernel/ltykernel.sml
ViewVC logotype

Diff of /sml/branches/SMLNJ/src/compiler/FLINT/kernel/ltykernel.sml

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

revision 68, Fri Apr 3 00:06:42 1998 UTC revision 69, Fri Apr 3 00:06:55 1998 UTC
# Line 17  Line 17 
17  in  in
18    
19  type enc_tvar = int  type enc_tvar = int
20  fun tvToInt (d, i) = d * MVAL + i  fun tvEncode (d, i) = d * MVAL + i
21  fun tvFromInt x = ((x div MVAL), (x mod MVAL))  fun tvDecode x = ((x div MVAL), (x mod MVAL))
22    
23  fun exitLevel xs =  fun exitLevel xs =
24    let fun h ([], x) = rev x    let fun h ([], x) = rev x
# Line 326  Line 326 
326          | exitAux x = x          | exitAux x = x
327    
328        fun tc_aux tc =        fun tc_aux tc =
329          let fun g (TC_VAR(d, i)) = AX_REG(true, [tvToInt(d, i)])          let fun g (TC_VAR(d, i)) = AX_REG(true, [tvEncode(d, i)])
330                | g (TC_NVAR(v, d, i)) = baseAux (*** THIS IS WRONG ! ***)                | g (TC_NVAR(v, d, i)) = baseAux (*** THIS IS WRONG ! ***)
331                | g (TC_PRIM pt) = baseAux                | g (TC_PRIM pt) = baseAux
332                | g (TC_APP(ref(_, TC_FN _, AX_NO), _)) = AX_NO                | g (TC_APP(ref(_, TC_FN _, AX_NO), _)) = AX_NO
# Line 408  Line 408 
408  fun lt_key (ref (h : int, _ : ltyI, _ : aux_info)) = h  fun lt_key (ref (h : int, _ : ltyI, _ : aux_info)) = h
409    
410  (***************************************************************************  (***************************************************************************
411     *            UTILITY FUNCTIONS ON TKIND ENVIRONMENT                       *
412     ***************************************************************************)
413    (** tkind environment: maps each tyvar, i.e., its debindex, to its kind *)
414    type tkindEnv = tkind list list
415    
416    (** utility functions for manipulating the tkindEnv *)
417    exception tkUnbound
418    val initTkEnv : tkindEnv = []
419    
420    fun tkLookup (kenv, i, j) =
421      let val ks = List.nth(kenv, i-1) handle _ => raise tkUnbound
422       in List.nth(ks, j) handle _ => raise tkUnbound
423      end
424    
425    fun tkInsert (kenv, ks) = ks::kenv
426    
427    (* strip any unused type variables out of a kenv, given a list of
428     * [encoded] free type variables.  the result is a "parallel list" of
429     * the kinds of those free type variables in the environment.
430     * This is meant to use the same representation of a kind environment
431     * as in ltybasic.
432     * --CALeague
433     *)
434    fun tkLookupFreeVars (kenv, tyc) =
435        let
436            fun g (kenv, d, []) = []
437              | g (kenv, d, ftv::ftvs) =
438                let val (d', i') = tvDecode ftv
439                    val kenv' = List.drop (kenv, d'-d)
440                        handle _ => raise tkUnbound
441                    val k = List.nth (hd kenv', i')
442                        handle _ => raise tkUnbound
443                    val rest = g (kenv', d', ftvs)
444                in
445                    k :: rest
446                end
447    
448            fun h ftvs = g (kenv, 1, ftvs)
449        in
450            Option.map h (tc_vs tyc)
451        end
452    
453    (***************************************************************************
454   *            UTILITY FUNCTIONS ON TYC ENVIRONMENT                         *   *            UTILITY FUNCTIONS ON TYC ENVIRONMENT                         *
455   ***************************************************************************)   ***************************************************************************)
456    
# Line 467  Line 510 
510    
511        fun withEff ([], ol, nl, tenv) = false        fun withEff ([], ol, nl, tenv) = false
512          | withEff (a::r, ol, nl, tenv) =          | withEff (a::r, ol, nl, tenv) =
513              let val (i, j) = tvFromInt a              let val (i, j) = tvDecode a
514                  val neweff =                  val neweff =
515                    if i > ol then (ol <> nl)                    if i > ol then (ol <> nl)
516                    else (* case tcLookup(i, tenv)                    else (* case tcLookup(i, tenv)
# Line 562  Line 605 
605          of TC_TUPLE (_, [_]) => (* singleton record is not flattened to ensure          of TC_TUPLE (_, [_]) => (* singleton record is not flattened to ensure
606                                isomorphism btw plambdatype and flinttype *)                                isomorphism btw plambdatype and flinttype *)
607               (true, [ntc], false)               (true, [ntc], false)
608             | TC_TUPLE (_, []) =>  (* unit is not flattened to avoid coercions *)
609                 (true, [ntc], false)
610           | TC_TUPLE (_, ts) =>           | TC_TUPLE (_, ts) =>
611               if length ts < 10 then (true, ts, true)               if length ts < 10 then (true, ts, true)
612               else (true, [ntc], false)  (* ZHONG added the magic number 10 *)               else (true, [ntc], false)  (* ZHONG added the magic number 10 *)
# Line 891  Line 936 
936                                (case (tc_outX x)                                (case (tc_outX x)
937                                  of TC_TUPLE(_, [y, z]) =>                                  of TC_TUPLE(_, [y, z]) =>
938                                      (false, [ggg y, ggg z])                                      (false, [ggg y, ggg z])
939                                   | _ => (true, [nt1]))                                   | _ => (false, [nt1]))
940                              else (false, [nt1])                              else (false, [nt1])
941                          | _ => (unknown nt1, [nt1]))                          | _ => (unknown nt1, [nt1]))
942                     val nt = tcc_arw(FF_FIXED, nts1, ts2)                     val nt = tcc_arw(FF_FIXED, nts1, ts2)
# Line 943  Line 988 
988   ***************************************************************************)   ***************************************************************************)
989    
990  (** testing the equality of values of tkind, tyc, lty *)  (** testing the equality of values of tkind, tyc, lty *)
991  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))
992    | eqlist (p, [], []) = true    | eqlist p ([], []) = true
993    | eqlist _ = false    | eqlist _ _ = false
994    
995  (** testing the "pointer" equality on normalized tkind, tyc, and lty *)  (** testing the "pointer" equality on normalized tkind, tyc, and lty *)
996  fun tk_eq (x: tkind, y) = (x = y)  fun tk_eq (x: tkind, y) = (x = y)
# Line 955  Line 1000 
1000  (** testing the equivalence for arbitrary tkinds, tycs and ltys *)  (** testing the equivalence for arbitrary tkinds, tycs and ltys *)
1001  val tk_eqv = tk_eq       (* all tkinds are normalized *)  val tk_eqv = tk_eq       (* all tkinds are normalized *)
1002    
1003  (** tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form *)  local (* tyc equivalence utilities *)
1004  fun tc_eqv_gen (eqop1, eqop2, eqop3, eqop4) (t1, t2) =  (* The efficiency of checking FIX equivalence could probably be
1005     * improved somewhat, but it doesn't seem so bad for my purposes right
1006     * now.  Anyway, somebody might eventually want to do some profiling
1007     * and improve this.  --league, 24 March 1998
1008     *)
1009    
1010    (* Profiling code, temporary?? *)
1011    structure Click =
1012    struct
1013        local
1014            val s_unroll = Stats.makeStat "FIX unrolls"
1015        in
1016            fun unroll() = Stats.addStat s_unroll 1
1017        end
1018    end (* Click *)
1019    
1020    (** unrolling a fix, tyc -> tyc *)
1021    fun tc_unroll_fix tyc =
1022        case tc_outX tyc of
1023            (TC_FIX((n,tc,ts),i)) => let
1024                fun genfix i = tcc_fix ((n,tc,ts),i)
1025                val fixes = List.tabulate(n, genfix)
1026                val mu = tc
1027                val mu = if null ts then mu
1028                         else tcc_app (mu,ts)
1029                val mu = tcc_app (mu, fixes)
1030                val mu = if n=1 then mu
1031                         else tcc_proj (mu, i)
1032            in
1033                Click.unroll();
1034                mu
1035            end
1036          | _ => bug "unexpected non-FIX in tc_unroll_fix"
1037    
1038    (* In order to check equality of two FIXes, we need to be able to
1039     * unroll them once, and check equality on the unrolled version, with
1040     * an inductive assumption that they ARE equal.  The following code
1041     * supports making and checking these inductive assumptions.
1042     * Furthermore, we need to avoid unrolling any FIX more than once.
1043     *)
1044    structure TcDict = BinaryDict
1045                           (struct
1046                               type ord_key = tyc
1047                               val cmpKey = tc_cmp
1048                           end)
1049    (* for each tyc in this dictionary, we store a dictionary containing
1050     * tycs that are assumed equivalent to it.
1051     *)
1052    type eqclass = unit TcDict.dict
1053    type hyp = eqclass TcDict.dict
1054    
1055    (* the null hypothesis, no assumptions about equality *)
1056    val empty_eqclass : eqclass = TcDict.mkDict()
1057    val null_hyp : hyp = TcDict.mkDict()
1058    
1059    (* add assumption t1=t2 to current hypothesis.  returns composite
1060     * hypothesis.
1061     *)
1062    fun assume_eq' (hyp, t1, t1eqOpt, t2) = let
1063        val t1eq  = case t1eqOpt of SOME e => e | NONE => empty_eqclass
1064        val t1eq' = TcDict.insert (t1eq, t2, ())
1065        val hyp'  = TcDict.insert (hyp, t1, t1eq')
1066    in
1067        hyp'
1068    end
1069    
1070    fun assume_eq (hyp, t1, t1eqOpt, t2, t2eqOpt) =
1071        assume_eq' (assume_eq' (hyp, t1, t1eqOpt, t2),
1072                    t2, t2eqOpt, t1)
1073    
1074    (* check whether t1=t2 according to the hypothesis *)
1075    val eq_by_hyp : eqclass option * tyc -> bool
1076        = fn (NONE, t2) => false
1077           | (SOME eqclass, t2) =>
1078             isSome (TcDict.peek (eqclass, t2))
1079    
1080    (* have we made any assumptions about `t' already? *)
1081    val visited : eqclass option -> bool
1082      = isSome
1083    
1084    (* testing if two recursive datatypes are equivalent *)
1085    fun eq_fix (eqop1, hyp) (t1, t2) =
1086    (case (tc_outX t1, tc_outX t2)    (case (tc_outX t1, tc_outX t2)
1087      of (TC_FN(ks1, b1), TC_FN(ks2, b2)) =>      of (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) =>
1088           (eqlist(tk_eqv, ks1, ks2)) andalso (eqop2(b1, b2))          if not (!Control.CG.checkDatatypes) then true
1089            else let
1090                val t1eqOpt = TcDict.peek (hyp, t1)
1091            in
1092                (* first check the induction hypothesis.  we only ever
1093                 * make hypotheses about FIX nodes, so this test is okay
1094                 * here.  if assume_eq appears in other cases, this
1095                 * test should be lifted outside the switch.
1096                 *)
1097                if eq_by_hyp (t1eqOpt, t2) then true
1098                (* next try structural eq on the components.  i'm not sure why
1099                 * this part is necessary, but it does seem to be... --league,
1100                 * 23 March 1998
1101                 *)
1102                else
1103                    (n1 = n2 andalso i1 = i2 andalso
1104                     eqop1 hyp (tc1, tc2) andalso
1105                     eqlist (eqop1 hyp) (ts1, ts2)) orelse
1106                    (* not equal by inspection; we have to unroll it.
1107                     * we prevent unrolling the same FIX twice by asking
1108                     * the `visited' function.
1109                     *)
1110                    if visited t1eqOpt then false
1111                    else let
1112                        val t2eqOpt = TcDict.peek (hyp, t2)
1113                    in
1114                        if visited t2eqOpt then false
1115                        else eqop1 (assume_eq (hyp, t1, t1eqOpt,
1116                                               t2, t2eqOpt))
1117                                   (tc_unroll_fix t1, tc_unroll_fix t2)
1118                    end
1119            end
1120         | _ => bug "unexpected types in eq_fix")
1121    
1122    
1123    (* tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form
1124     *     eqop1 is the default equality to be used for tycs
1125     *     eqop2 is used for body of FN, arguments in APP,
1126     *     eqop3 is used for ABS and BOX.
1127     *     eqop4 is used for arrow arguments and results
1128     * Each of these first takes the set of hypotheses.
1129     *)
1130    fun tc_eqv_gen (eqop1, eqop2, hyp) (t1, t2) =
1131        case (tc_outX t1, tc_outX t2) of
1132            (TC_FIX _, TC_FIX _) => eqop2 (eqop1, hyp) (t1, t2)
1133          | (TC_FN(ks1, b1), TC_FN(ks2, b2)) =>
1134            eqlist tk_eqv (ks1, ks2) andalso eqop1 hyp (b1, b2)
1135       | (TC_APP(a1, b1), TC_APP(a2, b2)) =>       | (TC_APP(a1, b1), TC_APP(a2, b2)) =>
1136           (eqop1(a1, a2)) andalso (eqlist(eqop2, b1, b2))          eqop1 hyp (a1, a2) andalso eqlist (eqop1 hyp) (b1, b2)
1137       | (TC_SEQ ts1, TC_SEQ ts2) => eqlist(eqop1, ts1, ts2)        | (TC_SEQ ts1, TC_SEQ ts2) =>
1138       | (TC_SUM ts1, TC_SUM ts2) => eqlist(eqop1, ts1, ts2)          eqlist (eqop1 hyp) (ts1, ts2)
1139       | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) => eqlist(eqop1, ts1, ts2)        | (TC_SUM ts1, TC_SUM ts2) =>
1140       | (TC_ABS a, TC_ABS b) => eqop1(a, b)          eqlist (eqop1 hyp) (ts1, ts2)
1141       | (TC_ABS a, _) => eqop3(a, t2)        | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) =>
1142       | (_, TC_ABS b) => eqop3(t1, b)          eqlist (eqop1 hyp) (ts1, ts2)
1143       | (TC_BOX a, TC_BOX b) => eqop1(a, b)        | (TC_ABS a, TC_ABS b) =>
1144       | (TC_BOX a, _) => eqop3(a, t2)          eqop1 hyp (a, b)
1145       | (_, TC_BOX b) => eqop3(t1, b)        | (TC_BOX a, TC_BOX b) =>
1146            eqop1 hyp (a, b)
1147       | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) =>       | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) =>
1148           (token_eq(k1,k2)) andalso (eqop1(t1,t2))          token_eq(k1,k2) andalso eqop1 hyp (t1,t2)
1149       | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>       | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>
1150           (i1 = i2) andalso (eqop1(a1, a2))          i1 = i2 andalso eqop1 hyp (a1, a2)
1151       | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>       | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>
1152           (r1 = r2) andalso (eqop4(a1, a2)) andalso (eqop4(b1, b2))          r1 = r2 andalso eqlist (eqop1 hyp) (a1, a2)
1153                    andalso eqlist (eqop1 hyp) (b1, b2)
1154       | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) =>       | (TC_PARROW(a1, b1), TC_PARROW(a2, b2)) =>
1155           (eqop1(a1, a2)) andalso (eqop1(b1, b2))          eqop1 hyp (a1, a2) andalso eqop1 hyp (b1, b2)
1156       | (TC_FIX((n1,tc1,ts1), i1), TC_FIX((n2,tc2,ts2), i2)) =>        | (TC_CONT ts1, TC_CONT ts2) =>
1157           true  (* INCORRECT: this is temporary (ZHONG) *)          eqlist (eqop1 hyp) (ts1, ts2)
1158       | (TC_CONT ts1, TC_CONT ts2) => eqlist(eqop1, ts1, ts2)        | _ => false
      | _ => false)  
1159    
1160  fun tc_eqv (x as ref (_, _, AX_REG(true, _)),  (** general equality for tycs *)
1161    fun tc_eqv' hyp (x as ref (_, _, AX_REG(true, _)),
1162              y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y)              y as ref (_, _, AX_REG(true, _))) = tc_eq(x,y)
1163    | tc_eqv (x, y) =    | tc_eqv' hyp (x, y) = let
1164        let val t1 = tc_whnm x          val t1 = tc_whnm x
1165            val t2 = tc_whnm y            val t2 = tc_whnm y
1166         in if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)      in
1167            else tc_eqv_gen (tc_eqv, tc_eqv, fn _ => false,          if tcp_norm t1 andalso tcp_norm t2 then tc_eq (t1, t2)
1168                             fn (ts1, ts2) => eqlist(tc_eqv, ts1, ts2)) (t1, t2)          else
1169        end (* function tc_eqv *)              tc_eqv_gen (tc_eqv', fn _ => tc_eq, hyp) (t1, t2)
1170        end (* tc_eqv' *)
1171    
1172  fun tc_eqv_x (x, y) =  (* slightly relaxed constraints (???) *)
1173    fun tc_eqv_x' hyp (x, y) =
1174    let val t1 = tc_whnm x    let val t1 = tc_whnm x
1175        val t2 = tc_whnm y        val t2 = tc_whnm y
1176     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)
1177         else false) orelse         else false) orelse
1178         (tc_eqv_gen (tc_eqv_x, tc_eqv_x, fn _ => false,         (tc_eqv_gen (tc_eqv_x', eq_fix, hyp) (t1, t2))
                     fn (ts1, ts2) => eqlist(tc_eqv_x, ts1, ts2)) (t1, t2))  
1179    end (* function tc_eqv_x *)    end (* function tc_eqv_x *)
1180    
1181  (** testing the equivalence of two tycs with relaxed constraints *)  in (* tyc equivalence utilities *)
 fun tc_eqv_bx (x : tyc, y) =  
   let val t1 = tc_whnm x  
       val t2 = tc_whnm y  
    in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)  
       else false) orelse  
       (tc_eqv_gen (tc_eqv_bx, tc_eqv_sp, fn _ => false,  
                    fn (ts1, ts2) => tc_eqv_bx(tc_autotuple ts1,  
                                               tc_autotuple ts2)) (t1, t2))  
   end (* function tc_eqv_bx *)  
1182    
1183  and tc_eqv_sp (x : tyc, y) =  val tc_eqv = tc_eqv' null_hyp
1184    let val t1 = tc_whnm x  val tc_eqv_x = tc_eqv_x' null_hyp
1185        val t2 = tc_whnm y  
1186     in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)  end (* tyc equivalence utilities *)
       else false) orelse  
       (tc_eqv_gen (tc_eqv_sp, tc_eqv_sp, tc_eqv_sp,  
                    fn (ts1, ts2) => tc_eqv_sp(tc_autotuple ts1,  
                                               tc_autotuple ts2)) (t1, t2))  
   end (* function tc_eqv_sp *)  
1187    
1188  (*  (*
1189   * all the complexity of lt_eqv comes from the partial-structure (or   * all the complexity of lt_eqv comes from the partial-structure (or
# Line 1048  Line 1209 
1209        fun seq (t1, t2) =        fun seq (t1, t2) =
1210          (case (lt_outX t1, lt_outX t2)          (case (lt_outX t1, lt_outX t2)
1211            of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) =>            of (LT_POLY(ks1, b1), LT_POLY(ks2, b2)) =>
1212                 (eqlist(tk_eqv, ks1, ks2)) andalso (eqlist(eqop1, b1, b2))                 (eqlist tk_eqv (ks1, ks2)) andalso (eqlist eqop1 (b1, b2))
1213             | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) =>             | (LT_FCT(as1, bs1), LT_FCT(as2, bs2)) =>
1214                 (eqlist(eqop1, as1, as2)) andalso (eqlist(eqop1, bs1, bs2))                 (eqlist eqop1 (as1, as2)) andalso (eqlist eqop1 (bs1, bs2))
1215             | (LT_TYC a, LT_TYC b) => eqop2(a, b)             | (LT_TYC a, LT_TYC b) => eqop2(a, b)
1216             | (LT_STR s1, LT_STR s2) => eqlist(eqop1, s1, s2)             | (LT_STR s1, LT_STR s2) => eqlist eqop1 (s1, s2)
1217             | (LT_PST s1, LT_PST s2) => pp(s1, s2)             | (LT_PST s1, LT_PST s2) => pp(s1, s2)
1218             | (LT_PST s1, LT_STR s2) => sp(s2, s1)             | (LT_PST s1, LT_STR s2) => sp(s2, s1)
1219             | (LT_STR s1, LT_PST s2) => sp(s1, s2)             | (LT_STR s1, LT_PST s2) => sp(s1, s2)
1220             | (LT_CONT s1, LT_CONT s2) => eqlist(eqop1, s1, s2)             | (LT_CONT s1, LT_CONT s2) => eqlist eqop1 (s1, s2)
1221             | _ => false)             | _ => false)
1222     in seq(x, y)     in seq(x, y)
1223    end (* function lt_eqv_gen *)    end (* function lt_eqv_gen *)
# Line 1085  Line 1246 
1246              end)              end)
1247    end (* function lt_eqv *)    end (* function lt_eqv *)
1248    
 fun lt_eqv_bx (x : lty, y) =  
   let val seq = lt_eqv_gen (lt_eqv_bx, tc_eqv_bx)  
    in if (ltp_norm x) andalso (ltp_norm y) then  
         (lt_eq(x, y)) orelse (seq(x, y))  
       else (let val t1 = lt_whnm x  
                 val t2 = lt_whnm y  
              in if (ltp_norm t1) andalso (ltp_norm t2) then  
                  (lt_eq(t1, t2)) orelse (seq(t1, t2))  
                 else seq(t1, t2)  
             end)  
   end (* function lt_eqv_bx *)  
   
1249  (** testing equivalence of fflags and rflags *)  (** testing equivalence of fflags and rflags *)
1250  val ff_eqv   : fflag * fflag -> bool = (op =)  val ff_eqv   : fflag * fflag -> bool = (op =)
1251  val rf_eqv   : rflag * rflag -> bool = (op =)  val rf_eqv   : rflag * rflag -> bool = (op =)
# Line 1113  Line 1262 
1262     in case tvs     in case tvs
1263         of NONE => bug "unexpected case in tc_depth"         of NONE => bug "unexpected case in tc_depth"
1264          | SOME [] => DI.top          | SOME [] => DI.top
1265          | SOME (a::_) => d + 1 - (#1(tvFromInt a))          | SOME (a::_) => d + 1 - (#1(tvDecode a))
1266    end    end
1267    
1268  fun tcs_depth ([], d) = DI.top  fun tcs_depth ([], d) = DI.top

Legend:
Removed from v.68  
changed lines
  Added in v.69

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