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 70, Fri Apr 3 00:06:55 1998 UTC revision 71, Fri Apr 3 01:57:57 1998 UTC
# Line 385  Line 385 
385  fun lt_vs (r as ref(_ : int, _ : ltyI, AX_NO)) = NONE  fun lt_vs (r as ref(_ : int, _ : ltyI, AX_NO)) = NONE
386    | lt_vs (r as ref(_ : int, _ : ltyI, AX_REG (_,x))) = SOME x    | lt_vs (r as ref(_ : int, _ : ltyI, AX_REG (_,x))) = SOME x
387    
388    
389  (** converting from the hash-consing reps to the standard reps *)  (** converting from the hash-consing reps to the standard reps *)
390  fun tk_outX (r as ref(_ : int, t : tkindI, _ : aux_info)) = t  fun tk_outX (r as ref(_ : int, t : tkindI, _ : aux_info)) = t
391  fun tc_outX (r as ref(_ : int, t : tycI, _ : aux_info)) = t  fun tc_outX (r as ref(_ : int, t : tycI, _ : aux_info)) = t
# Line 396  Line 397 
397  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)
398  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)
399    
400    
401  (** key-comparison on tkind, tyc, lty *)  (** key-comparison on tkind, tyc, lty *)
402  fun tk_cmp (k1, k2) = cmp(tk_table, k1, k2)  fun tk_cmp (k1, k2) = cmp(tk_table, k1, k2)
403  fun tc_cmp (t1, t2) = cmp(tc_table, t1, t2)  fun tc_cmp (t1, t2) = cmp(tc_table, t1, t2)
# Line 408  Line 410 
410  (***************************************************************************  (***************************************************************************
411   *            UTILITY FUNCTIONS ON TKIND ENVIRONMENT                       *   *            UTILITY FUNCTIONS ON TKIND ENVIRONMENT                       *
412   ***************************************************************************)   ***************************************************************************)
   
413  (** tkind environment: maps each tyvar, i.e., its debindex, to its kind *)  (** tkind environment: maps each tyvar, i.e., its debindex, to its kind *)
414  type tkindEnv = tkind list list  type tkindEnv = tkind list list
415    
# Line 604  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 933  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 1078  Line 1081 
1081  val visited : eqclass option -> bool  val visited : eqclass option -> bool
1082    = isSome    = isSome
1083    
1084  (* tc_eqv_generator, invariant: t1 and t2 are in the wh-normal form  (* testing if two recursive datatypes are equivalent *)
1085   *     eqop1 is the default equality to be used for tycs  fun eq_fix (eqop1, hyp) (t1, t2) =
1086   *     eqop2 is used for body of FN, arguments in APP,    (case (tc_outX t1, tc_outX t2)
1087   *     eqop3 is used for ABS and BOX.      of (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) =>
  *     eqop4 is used for arrow arguments and results  
  * Each of these first takes the set of hypotheses.  
  *)  
 fun tc_eqv_gen (eqop1, eqop2, eqop3, eqop4) hyp (t1, t2) =  
     case (tc_outX t1, tc_outX t2) of  
         (TC_FIX((n1,tc1,ts1),i1), TC_FIX((n2,tc2,ts2),i2)) =>  
1088          if not (!Control.CG.checkDatatypes) then true          if not (!Control.CG.checkDatatypes) then true
1089          else let          else let
1090              val t1eqOpt = TcDict.peek (hyp, t1)              val t1eqOpt = TcDict.peek (hyp, t1)
# Line 1105  Line 1102 
1102              else              else
1103                  (n1 = n2 andalso i1 = i2 andalso                  (n1 = n2 andalso i1 = i2 andalso
1104                   eqop1 hyp (tc1, tc2) andalso                   eqop1 hyp (tc1, tc2) andalso
1105                   eqlist (eqop2 hyp) (ts1, ts2)) orelse                   eqlist (eqop1 hyp) (ts1, ts2)) orelse
1106                  (* not equal by inspection; we have to unroll it.                  (* not equal by inspection; we have to unroll it.
1107                   * we prevent unrolling the same FIX twice by asking                   * we prevent unrolling the same FIX twice by asking
1108                   * the `visited' function.                   * the `visited' function.
# Line 1120  Line 1117 
1117                                 (tc_unroll_fix t1, tc_unroll_fix t2)                                 (tc_unroll_fix t1, tc_unroll_fix t2)
1118                  end                  end
1119          end          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)) =>        | (TC_FN(ks1, b1), TC_FN(ks2, b2)) =>
1134          eqlist tk_eqv (ks1, ks2) andalso eqop2 hyp (b1, b2)          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 hyp (a1, a2) andalso eqlist (eqop2 hyp) (b1, b2)          eqop1 hyp (a1, a2) andalso eqlist (eqop1 hyp) (b1, b2)
1137        | (TC_SEQ ts1, TC_SEQ ts2) =>        | (TC_SEQ ts1, TC_SEQ ts2) =>
1138          eqlist (eqop1 hyp) (ts1, ts2)          eqlist (eqop1 hyp) (ts1, ts2)
1139        | (TC_SUM ts1, TC_SUM ts2) =>        | (TC_SUM ts1, TC_SUM ts2) =>
# Line 1132  Line 1142 
1142          eqlist (eqop1 hyp) (ts1, ts2)          eqlist (eqop1 hyp) (ts1, ts2)
1143        | (TC_ABS a, TC_ABS b) =>        | (TC_ABS a, TC_ABS b) =>
1144          eqop1 hyp (a, b)          eqop1 hyp (a, b)
       | (TC_ABS a, _) =>  
         eqop3 hyp (a, t2)  
       | (_, TC_ABS b) =>  
         eqop3 hyp (t1, b)  
1145        | (TC_BOX a, TC_BOX b) =>        | (TC_BOX a, TC_BOX b) =>
1146          eqop1 hyp (a, b)          eqop1 hyp (a, b)
       | (TC_BOX a, _) =>  
         eqop3 hyp (a, t2)  
       | (_, TC_BOX b) =>  
         eqop3 hyp (t1, 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 hyp (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 hyp (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 hyp (a1, a2) andalso eqop4 hyp (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 hyp (a1, a2) andalso eqop1 hyp (b1, b2)          eqop1 hyp (a1, a2) andalso eqop1 hyp (b1, b2)
1156        | (TC_CONT ts1, TC_CONT ts2) =>        | (TC_CONT ts1, TC_CONT ts2) =>
1157          eqlist (eqop1 hyp) (ts1, ts2)          eqlist (eqop1 hyp) (ts1, ts2)
1158        | _ => false        | _ => false
1159    
 fun never h (t1,t2) = false  
   
1160  (** general equality for tycs *)  (** general equality for tycs *)
1161  fun tc_eqv' hyp (x as ref (_, _, AX_REG(true, _)),  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)
# Line 1165  Line 1166 
1166      in      in
1167          if tcp_norm t1 andalso tcp_norm t2 then tc_eq (t1, t2)          if tcp_norm t1 andalso tcp_norm t2 then tc_eq (t1, t2)
1168          else          else
1169              tc_eqv_gen (tc_eqv', tc_eqv', never, eqlist o tc_eqv')              tc_eqv_gen (tc_eqv', fn _ => tc_eq, hyp) (t1, t2)
                        hyp (t1, t2)  
1170      end (* tc_eqv' *)      end (* tc_eqv' *)
1171    
1172  (* slightly relaxed constraints (???) *)  (* slightly relaxed constraints (???) *)
# Line 1175  Line 1175 
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', never, eqlist o tc_eqv_x')         (tc_eqv_gen (tc_eqv_x', eq_fix, hyp) (t1, t2))
                    hyp (t1, t2))  
1179    end (* function tc_eqv_x *)    end (* function tc_eqv_x *)
1180    
 (** testing the equivalence of two tycs with relaxed constraints *)  
 fun mkeqop4 eqop1 hyp (ts1, ts2) =  
     eqop1 hyp (tc_autotuple ts1, tc_autotuple ts2)  
   
 fun tc_eqv_bx' hyp (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', never,  
                    mkeqop4 tc_eqv_bx')  
                   hyp (t1, t2))  
   end (* function tc_eqv_bx *)  
   
 and tc_eqv_sp' hyp (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_sp', tc_eqv_sp', tc_eqv_sp',  
                    mkeqop4 tc_eqv_sp')  
                   hyp (t1, t2))  
   end (* function tc_eqv_sp *)  
   
1181  in (* tyc equivalence utilities *)  in (* tyc equivalence utilities *)
1182    
 (* TODO: explain the precise difference between these three notions of  
  * equality!  --league  
  *)  
1183  val tc_eqv = tc_eqv' null_hyp  val tc_eqv = tc_eqv' null_hyp
1184  val tc_eqv_x = tc_eqv_x' null_hyp  val tc_eqv_x = tc_eqv_x' null_hyp
 val tc_eqv_bx = tc_eqv_bx' null_hyp  
1185    
1186  end (* tyc equivalence utilities *)  end (* tyc equivalence utilities *)
1187    
1188    (*
1189     * all the complexity of lt_eqv comes from the partial-structure (or
1190     * partial record) type (the LT_PST type). If we can remove LT_PST
1191     * type, then the following can be considerabily simplified. (ZHONG)
1192     *)
1193    
1194  (** 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 *)
1195  fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) =  fun lt_eqv_gen (eqop1, eqop2) (x : lty, y) =
1196    let fun sp (r, []) = true    let fun sp (r, []) = true
# Line 1269  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 =)

Legend:
Removed from v.70  
changed lines
  Added in v.71

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