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 44, Sun Mar 22 20:10:57 1998 UTC revision 45, Sun Mar 22 20:11:09 1998 UTC
# Line 4  Line 4 
4  structure LtyKernel :> LTYKERNEL =  structure LtyKernel :> LTYKERNEL =
5  struct  struct
6    
7    fun bug s = ErrorMsg.impossible ("LtyKernel:" ^ s)
8    
9  (***************************************************************************  (***************************************************************************
10   *                UTILITY FUNCTIONS FOR HASHCONSING BASICS                 *   *                UTILITY FUNCTIONS FOR HASHCONSING BASICS                 *
11   ***************************************************************************)   ***************************************************************************)
# Line 34  Line 36 
36    
37  end (* local of hashconsing implementation basics *)  end (* local of hashconsing implementation basics *)
38    
   
39  (***************************************************************************  (***************************************************************************
40   *                 DATATYPE DEFINITIONS                                    *   *                 DATATYPE DEFINITIONS                                    *
41   ***************************************************************************)   ***************************************************************************)
# Line 44  Line 45 
45    = TK_MONO                                    (* ground mono tycon *)    = TK_MONO                                    (* ground mono tycon *)
46    | TK_BOX                                     (* boxed/tagged tycon *)    | TK_BOX                                     (* boxed/tagged tycon *)
47    | TK_SEQ of tkind list                       (* sequence of tycons *)    | TK_SEQ of tkind list                       (* sequence of tycons *)
48    | TK_FUN of tkind * tkind                    (* tycon function *)    | TK_FUN of tkind list * tkind               (* tycon function *)
49    
50  withtype tkind = tkindI hash_cell              (* hash-consing-impl of tkind *)  withtype tkind = tkindI hash_cell              (* hash-consing-impl of tkind *)
51    
# Line 52  Line 53 
53  type tvar = LambdaVar.lvar                     (* temporary definitions *)  type tvar = LambdaVar.lvar                     (* temporary definitions *)
54  val mkTvar = LambdaVar.mkLvar  val mkTvar = LambdaVar.mkLvar
55    
56  (** definitions of lambda tycons and lambda types *)  (* an special extensible token key *)
57    type token = int
58    
59    datatype fflag                                 (* calling conventions *)
60      = FF_VAR of bool * bool                      (* is it fixed ? *)
61      | FF_FIXED                                   (* used after rep. analysis *)
62    
63    datatype rflag = RF_TMP                        (* tuple kind: a template *)
64    
65    (** definitions of lambda type constructors *)
66  datatype tycI  datatype tycI
67    = TC_VAR of DebIndex.index * int             (* tyc variables *)    = TC_VAR of DebIndex.index * int             (* tyc variables *)
68    | TC_NVAR of tvar * DebIndex.depth * int     (* named tyc variables *)    | TC_NVAR of tvar * DebIndex.depth * int     (* named tyc variables *)
# Line 66  Line 76 
76    | TC_SUM of tyc list                         (* sum tyc *)    | TC_SUM of tyc list                         (* sum tyc *)
77    | TC_FIX of (int * tyc * tyc list) * int     (* recursive tyc *)    | TC_FIX of (int * tyc * tyc list) * int     (* recursive tyc *)
78    
79    | TC_TUPLE of tyc list                       (* std record tyc *)    | TC_TUPLE of rflag * tyc list               (* std record tyc *)
80    | TC_ARROW of rawflag * tyc list * tyc list  (* std function tyc *)    | TC_ARROW of fflag * tyc list * tyc list    (* std function tyc *)
81    | TC_PARROW of tyc * tyc                     (* special fun tyc, not used *)    | TC_PARROW of tyc * tyc                     (* special fun tyc, not used *)
82    
83    | TC_BOX of tyc                              (* boxed tyc *)    | TC_BOX of tyc                              (* boxed tyc *)
84    | TC_ABS of tyc                              (* abstract tyc, not used *)    | TC_ABS of tyc                              (* abstract tyc, not used *)
85      | TC_TOKEN of token * tyc                    (* extensible token tyc *)
86    | TC_CONT of tyc list                        (* intern continuation tycon *)    | TC_CONT of tyc list                        (* intern continuation tycon *)
87    | TC_IND of tyc * tycI                       (* indirect tyc thunk *)    | TC_IND of tyc * tycI                       (* indirect tyc thunk *)
88    | TC_ENV of tyc * int * int * tycEnv         (* tyc closure *)    | TC_ENV of tyc * int * int * tycEnv         (* tyc closure *)
89    
90  and ltyI  withtype tyc = tycI hash_cell                  (* hash-consed tyc cell *)
91         and tycEnv = tyc     (*
92                               * This really is (tyc list option * int) list,
93                               * it is encoded using SEQ[(PROJ(SEQ tcs),i)]
94                               * and SEQ[(PROJ(VOID, i))]. (ZHONG)
95                               *)
96    
97    (** definitions of lambda types *)
98    datatype ltyI
99    = LT_TYC of tyc                              (* monomorphic type *)    = LT_TYC of tyc                              (* monomorphic type *)
100    | LT_STR of lty list                         (* structure record type *)    | LT_STR of lty list                         (* structure record type *)
101    | LT_FCT of lty list * lty list              (* functor arrow type *)    | LT_FCT of lty list * lty list              (* functor arrow type *)
# Line 87  Line 106 
106    | LT_IND of lty * ltyI                       (* a lty thunk and its sig *)    | LT_IND of lty * ltyI                       (* a lty thunk and its sig *)
107    | LT_ENV of lty * int * int * tycEnv         (* lty closure *)    | LT_ENV of lty * int * int * tycEnv         (* lty closure *)
108    
109  withtype tyc = tycI hash_cell                  (* hash-consed tyc cell *)  withtype lty = ltyI hash_cell                  (* hash-consed lty cell *)
110    
111       and lty = ltyI hash_cell                  (* hash-consed lty cell *)  (***************************************************************************
112     *                   TOKEN TYC UTILITY FUNCTIONS                           *
113     ***************************************************************************)
114    
115       and tycEnv = tyc     (*  type token_info
116                             * This really is (tyc list option * int) list,    = {name      : string,
117                             * it is encoded using SEQ[(PROJ(SEQ tcs),i)]       abbrev    : string,
118                             * and SEQ[(PROJ(VOID, i))]. (ZHONG)       reduce_one: token * tyc -> tyc,
119                             *)       is_whnm   : tyc -> bool,
120         is_known  : token * tyc -> bool}
121    
122    local val token_key = ref 0
123          val token_table_size = 10
124          val default_token_info =
125            {name="TC_GARBAGE",
126             abbrev="GB",
127             reduce_one=(fn _ => bug "token not implemented"),
128             is_whnm=(fn _ => bug "token not implemented"),
129             is_known=(fn _ => bug "token not implemented")}
130          val token_array : token_info Array.array =
131                Array.array(token_table_size,default_token_info)
132          val token_validity_table = Array.array(token_table_size,false)
133          fun get_next_token () =
134            let val n = !token_key
135             in if n > token_table_size then bug "running out of tokens"
136                else (token_key := n+1; n)
137            end
138          fun store_token_info (x, k) = Array.update(token_array, k, x)
139          fun get_is_whnm k = #is_whnm (Array.sub(token_array, k))
140          fun get_reduce_one (z as (k, t)) =
141                (#reduce_one (Array.sub(token_array, k))) z
142          fun get_name k = #name (Array.sub(token_array, k))
143          fun get_abbrev k = #abbrev (Array.sub(token_array, k))
144          fun get_is_known (z as (k, t)) =
145                (#is_known (Array.sub(token_array, k))) z
146          fun is_valid k = Array.sub(token_validity_table, k)
147          fun set_valid k = Array.update(token_validity_table, k, true)
148    in
149    
150    val register_token: token_info -> token =
151      (fn x => let val k = get_next_token ()
152                in store_token_info(x, k); set_valid k; k
153               end)
154    
155       and rawflag = bool * bool (* are arguments/results raw or cooked ? *)  val token_name    : token -> string = get_name
156    val token_abbrev  : token -> string = get_abbrev
157    val token_whnm    : token -> tyc -> bool = get_is_whnm
158    val token_reduce  : token * tyc -> tyc = get_reduce_one
159    val token_isKnown : token * tyc -> bool = get_is_known
160    val token_isvalid : token -> bool = is_valid
161    val token_eq      : token * token -> bool = fn (x,y) => (x=y)
162    val token_int     : token -> int = fn x => x
163    val token_key     : int -> token = fn x => x
164    
165    end (* end of all token-related hacks *)
166    
167  (***************************************************************************  (***************************************************************************
168   *                   HASHCONSING IMPLEMENTATIONS                           *   *                   HASHCONSING IMPLEMENTATIONS                           *
# Line 182  Line 246 
246          let fun g (TK_MONO) = 0w1          let fun g (TK_MONO) = 0w1
247                | g (TK_BOX) = 0w2                | g (TK_BOX) = 0w2
248                | g (TK_SEQ ks) = combine (3::map getnum ks)                | g (TK_SEQ ks) = combine (3::map getnum ks)
249                | g (TK_FUN(k1, k2)) = combine [4, getnum k1, getnum k2]                | g (TK_FUN(ks, k)) = combine (4::getnum k::(map getnum ks))
250           in g tk           in g tk
251          end          end
252    
# Line 199  Line 263 
263                       combine (8::n::i::(getnum t)::(map getnum ts))                       combine (8::n::i::(getnum t)::(map getnum ts))
264                | g (TC_ABS t) = combine [9, getnum t]                | g (TC_ABS t) = combine [9, getnum t]
265                | g (TC_BOX t) = combine [10, getnum t]                | g (TC_BOX t) = combine [10, getnum t]
266                | g (TC_TUPLE ts) = combine (11::(map getnum ts))                | g (TC_TUPLE (_, ts)) = combine (11::(map getnum ts))
267                | g (TC_ARROW(rw, ts1, ts2)) =                | g (TC_ARROW(rw, ts1, ts2)) =
268                       let fun h(true, true) = 10                       let fun h (FF_FIXED) = 10
269                             | h(true, _) = 20                             | h (FF_VAR(true,b2)) = if b2 then 20 else 30
270                             | h(_, true) = 30                             | h (FF_VAR(false,b2)) = if b2 then 40 else 50
                            | h _ = 40  
271                        in combine (12::(h rw)::(map getnum (ts1@ts2)))                        in combine (12::(h rw)::(map getnum (ts1@ts2)))
272                       end                       end
273                | g (TC_PARROW (t1,t2)) = combine [13, getnum t1, getnum t2]                | g (TC_PARROW (t1,t2)) = combine [13, getnum t1, getnum t2]
274                | g (TC_CONT ts) = combine (14::(map getnum ts))                | g (TC_TOKEN (i, tc)) = combine [14, i, getnum tc]
275                  | g (TC_CONT ts) = combine (15::(map getnum ts))
276                | g (TC_ENV(t,i,j,env)) =                | g (TC_ENV(t,i,j,env)) =
277                       combine[15, getnum t, i, j, getnum env]                       combine[16, getnum t, i, j, getnum env]
278                | g (TC_IND _) = bug "unexpected TC_IND in tc_hash"                | g (TC_IND _) = bug "unexpected TC_IND in tc_hash"
279    
280           in g tc           in g tc
# Line 263  Line 327 
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, [tvToInt(d, i)])
330                | g (TC_NVAR(v, d, i)) = baseAux (*** incorrect ? ***)                | 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
333                | g (TC_PROJ(ref(_, TC_SEQ _, AX_NO), _)) = AX_NO                | g (TC_PROJ(ref(_, TC_SEQ _, AX_NO), _)) = AX_NO
# Line 284  Line 348 
348                       end                       end
349                | g (TC_ABS t) = getAux t                | g (TC_ABS t) = getAux t
350                | g (TC_BOX t) = getAux t                | g (TC_BOX t) = getAux t
351                | g (TC_TUPLE ts) = fsmerge ts                | g (TC_TUPLE (_, ts)) = fsmerge ts
352                | g (TC_ARROW(_, ts1, ts2)) = fsmerge (ts1@ts2)                | g (TC_ARROW(_, ts1, ts2)) = fsmerge (ts1@ts2)
353                | g (TC_PARROW(t1, t2)) = fsmerge [t1, t2]                | g (TC_PARROW(t1, t2)) = fsmerge [t1, t2]
354                  | g (TC_TOKEN (k, (ref(_, t, AX_NO)))) = AX_NO
355                  | g (TC_TOKEN (k, (x as ref(_, t, AX_REG(b,vs))))) =
356                         AX_REG((token_whnm k x) andalso b, vs)
357                | g (TC_CONT ts) = fsmerge ts                | g (TC_CONT ts) = fsmerge ts
358                | g (TC_IND _) = bug "unexpected TC_IND in tc_aux"                | g (TC_IND _) = bug "unexpected TC_IND in tc_aux"
359                | g (TC_ENV _) = AX_NO                | g (TC_ENV _) = AX_NO
# Line 346  Line 413 
413    
414  (** utility functions for manipulating the tycEnv *)  (** utility functions for manipulating the tycEnv *)
415  local val tc_void = tc_injX(TC_PRIM(PT.ptc_void))  local val tc_void = tc_injX(TC_PRIM(PT.ptc_void))
416        val rawtt = (true, true)        fun tc_cons (t, b) = tc_injX(TC_ARROW(FF_FIXED, [t],[b]))
       fun tc_cons (t, b) = tc_injX(TC_ARROW(rawtt, [t],[b]))  
417        fun tc_interp x =        fun tc_interp x =
418          (case tc_outX x          (case tc_outX x
419            of TC_PROJ(y, i) =>            of TC_PROJ(y, i) =>
# Line 392  Line 458 
458    | ltp_norm _ = false    | ltp_norm _ = false
459    
460    
 (** finding out the innermost binding depth for a tyc's free variables *)  
 fun tc_depth (x, d) =  
   let val tvs = tc_vs x  
    in case tvs  
        of NONE => bug "unexpected case in tc_depth"  
         | SOME [] => DI.top  
         | SOME (a::_) => d + 1 - (#1(tvFromInt a))  
   end  
   
 fun tcs_depth ([], d) = DI.top  
   | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d))  
   
461  (** utility functions for tc_env and lt_env *)  (** utility functions for tc_env and lt_env *)
462  local fun tcc_env_int(x, 0, 0, te) = x  local fun tcc_env_int(x, 0, 0, te) = x
463          | tcc_env_int(x, i, j, te) = tc_injX(TC_ENV(x, i, j, te))          | tcc_env_int(x, i, j, te) = tc_injX(TC_ENV(x, i, j, te))
# Line 476  Line 530 
530  val tcc_app = tc_injX o TC_APP  val tcc_app = tc_injX o TC_APP
531  val tcc_seq = tc_injX o TC_SEQ  val tcc_seq = tc_injX o TC_SEQ
532  val tcc_proj = tc_injX o TC_PROJ  val tcc_proj = tc_injX o TC_PROJ
 val tcc_sum = tc_injX o TC_SUM  
533  val tcc_fix = tc_injX o TC_FIX  val tcc_fix = tc_injX o TC_FIX
534  val tcc_abs = tc_injX o TC_ABS  val tcc_abs = tc_injX o TC_ABS
 val tcc_box = tc_injX o TC_BOX  
535  val tcc_tup = tc_injX o TC_TUPLE  val tcc_tup = tc_injX o TC_TUPLE
536  val tcc_parw = tc_injX o TC_PARROW  val tcc_parw = tc_injX o TC_PARROW
537    val tcc_box = tc_injX o TC_BOX
538    val tcc_real = tc_injX (TC_PRIM PT.ptc_real)
539  val ltc_tyc = lt_injX o LT_TYC  val ltc_tyc = lt_injX o LT_TYC
540  val ltc_str = lt_injX o LT_STR  val ltc_str = lt_injX o LT_STR
541  val ltc_pst = lt_injX o LT_PST  val ltc_pst = lt_injX o LT_PST
542  val ltc_fct = lt_injX o LT_FCT  val ltc_fct = lt_injX o LT_FCT
543  val ltc_poly = lt_injX o LT_POLY  val ltc_poly = lt_injX o LT_POLY
544    val tcc_sum = tc_injX o TC_SUM
545    val tcc_token = tc_injX o TC_TOKEN
546    
547  (** the following function contains the procedure on how to  (** the following function contains the procedure on how to
548      flatten the arguments and results of an arbitrary FLINT function   *  flatten the arguments and results of an arbitrary FLINT function
549   *)   *)
550  fun isKnown tc =  fun isKnown tc =
551    (case tc_outX(tc_whnm tc)    (case tc_outX(tc_whnm tc)
# Line 497  Line 553 
553       | (TC_CONT _ | TC_FIX _ | TC_SUM _ | TC_TUPLE _) => true       | (TC_CONT _ | TC_FIX _ | TC_SUM _ | TC_TUPLE _) => true
554       | TC_APP(tc, _) => isKnown tc       | TC_APP(tc, _) => isKnown tc
555       | TC_PROJ(tc, _) => isKnown tc       | TC_PROJ(tc, _) => isKnown tc
556         | TC_TOKEN(k, x) => token_isKnown(k, x)
557       | _ => false)       | _ => false)
558    
559  and tc_autoflat tc =  and tc_autoflat tc =
560    let val ntc = tc_whnm tc    let val ntc = tc_whnm tc
561     in (case tc_outX ntc     in (case tc_outX ntc
562          of TC_TUPLE [_] => (* singleton record is not flattened to ensure          of TC_TUPLE (_, [_]) => (* singleton record is not flattened to ensure
563                                isomorphism btw plambdatype and flinttype *)                                isomorphism btw plambdatype and flinttype *)
564               (true, [ntc], false)               (true, [ntc], false)
565           | TC_TUPLE ts => (true, ts, true)           | TC_TUPLE (_, ts) =>
566                 if length ts < 10 then (true, ts, true)
567                 else (true, [ntc], false)  (* ZHONG added the magic number 10 *)
568           | _ => if isKnown ntc then (true, [ntc], false)           | _ => if isKnown ntc then (true, [ntc], false)
569                  else (false, [ntc], false))                  else (false, [ntc], false))
570    end    end
571    
572  and tc_autotuple [x] = x  and tc_autotuple [x] = x
573    | tc_autotuple xs = tcc_tup xs    | tc_autotuple xs =
574           if length xs < 10 then tcc_tup (RF_TMP, xs)
575           else bug "fatal error with tc_autotuple"
576    
577  and tcs_autoflat (flag, ts) =  and tcs_autoflat (flag, ts) =
578    if flag then (flag, ts)    if flag then (flag, ts)
579    else (case ts    else (case ts
580           of [tc] => (let val (nraw, ntcs, _) = tc_autoflat tc           of [tc] => (let val ntc = tc_whnm tc
581                             val (nraw, ntcs, _) = tc_autoflat ntc
582                        in (nraw, ntcs)                        in (nraw, ntcs)
583                       end)                       end)
584            | _ => bug "unexpected cooked multiples in tcs_autoflat")            | _ => bug "unexpected cooked multiples in tcs_autoflat")
# Line 530  Line 592 
592       | _ => (true, [lt], false))       | _ => (true, [lt], false))
593    
594  (** a special version of tcc_arw that does automatic flattening *)  (** a special version of tcc_arw that does automatic flattening *)
595  and tcc_arw  (x as ((true, true), ts1, ts2)) = tc_injX (TC_ARROW x)  and tcc_arw (x as (FF_FIXED, _, _)) = tc_injX (TC_ARROW x)
596    | tcc_arw  (b as (b1, b2), ts1, ts2) =    | tcc_arw (x as (FF_VAR (true, true), _, _)) = tc_injX (TC_ARROW x)
597      | tcc_arw (b as (FF_VAR (b1, b2)), ts1, ts2) =
598        let val (nb1, nts1) = tcs_autoflat (b1, ts1)        let val (nb1, nts1) = tcs_autoflat (b1, ts1)
599            val (nb2, nts2) = tcs_autoflat (b2, ts2)            val (nb2, nts2) = tcs_autoflat (b2, ts2)
600         in tc_injX (TC_ARROW((nb1, nb2),  nts1, nts2))         in tc_injX (TC_ARROW(FF_VAR(nb1, nb2),  nts1, nts2))
601        end        end
602    
603  (** utility function to read the top-level of a tyc *)  (** utility function to read the top-level of a tyc *)
# Line 578  Line 641 
641                          tcc_fix((n, prop tc, map prop ts), i)                          tcc_fix((n, prop tc, map prop ts), i)
642                     | TC_ABS tc => tcc_abs (prop tc)                     | TC_ABS tc => tcc_abs (prop tc)
643                     | TC_BOX tc => tcc_box (prop tc)                     | TC_BOX tc => tcc_box (prop tc)
644                     | TC_TUPLE tcs => tcc_tup (map prop tcs)                     | TC_TUPLE (rk, tcs) => tcc_tup (rk, map prop tcs)
645                     | TC_ARROW (r, ts1, ts2) =>                     | TC_ARROW (r, ts1, ts2) =>
646                         tcc_arw (r, map prop ts1, map prop ts2)                         tcc_arw (r, map prop ts1, map prop ts2)
647                     | TC_PARROW (t1, t2) => tcc_parw (prop t1, prop t2)                     | TC_PARROW (t1, t2) => tcc_parw (prop t1, prop t2)
648                       | TC_TOKEN (k, t) => tcc_token(k, prop t)
649                     | TC_CONT _ => bug "unexpected TC_CONT in tc_lzrd"                     | TC_CONT _ => bug "unexpected TC_CONT in tc_lzrd"
650                     | TC_IND (tc, _) => h(tc, ol, nl, tenv)                     | TC_IND (tc, _) => h(tc, ol, nl, tenv)
651                     | TC_ENV(tc, ol', nl', tenv') =>                     | TC_ENV(tc, ol', nl', tenv') =>
# Line 656  Line 720 
720                     | _ => let val xx = tcc_app(tc', tcs)                     | _ => let val xx = tcc_app(tc', tcs)
721                             in stripInd xx                             in stripInd xx
722                            end                            end
 (*  
                        let fun h x =  
                              let val nx = tc_whnm x  
                               in (case tc_outX nx  
                                    of TC_BOX z => h z  
                                     | TC_ABS z => h z  
                                     | _ => nx)  
                              end  
                         in tcc_app(tc', map h tcs)  
                        end  
 *)  
723               end)               end)
724          | TC_PROJ(tc, i) =>          | TC_PROJ(tc, i) =>
725              (let val tc' = tc_whnm tc              (let val tc' = tc_whnm tc
# Line 685  Line 738 
738                              in stripInd xx                              in stripInd xx
739                             end)                             end)
740               end)               end)
741            | TC_TOKEN(k, tc)  =>
742                (let val tc' = tc_whnm tc
743                  in if token_whnm k tc'
744                     then let val xx = tcc_token(k, tc') in stripInd xx end
745                     else let val res = token_reduce(k, tc')
746                              val nres = tc_whnm res
747                           in tyc_upd(nt, nres); nres
748                          end
749                 end)
750          | TC_IND (tc, _) => tc_whnm tc          | TC_IND (tc, _) => tc_whnm tc
751          | TC_ENV _ => bug "unexpected TC_ENV in tc_whnm"          | TC_ENV _ => bug "unexpected TC_ENV in tc_whnm"
752          | _ => nt          | _ => nt
# Line 715  Line 777 
777                       tcc_fix((n, tc_norm tc, map tc_norm ts), i)                       tcc_fix((n, tc_norm tc, map tc_norm ts), i)
778                   | TC_ABS tc => tcc_abs(tc_norm tc)                   | TC_ABS tc => tcc_abs(tc_norm tc)
779                   | TC_BOX tc => tcc_box(tc_norm tc)                   | TC_BOX tc => tcc_box(tc_norm tc)
780                   | TC_TUPLE tcs => tcc_tup(map tc_norm tcs)                   | TC_TUPLE (rk, tcs) => tcc_tup(rk, map tc_norm tcs)
781                   | TC_ARROW (r, ts1, ts2) =>                   | TC_ARROW (r, ts1, ts2) =>
782                       tcc_arw(r, map tc_norm ts1, map tc_norm ts2)                       tcc_arw(r, map tc_norm ts1, map tc_norm ts2)
783                   | TC_PARROW (t1, t2) => tcc_parw(tc_norm t1, tc_norm t2)                   | TC_PARROW (t1, t2) => tcc_parw(tc_norm t1, tc_norm t2)
784                     | TC_TOKEN (k, t) => tcc_token(k, tc_norm t)
785                   | TC_IND (tc, _) => tc_norm tc                   | TC_IND (tc, _) => tc_norm tc
786                   | TC_ENV _ => bug "unexpected tycs in tc_norm"                   | TC_ENV _ => bug "unexpected tycs in tc_norm"
787                   | _ => nt)                   | _ => nt)
# Line 747  Line 810 
810    end (* function lt_norm *)    end (* function lt_norm *)
811    
812  (***************************************************************************  (***************************************************************************
813     *         REGISTER A NEW TOKEN TYC --- TC_WRAP                            *
814     ***************************************************************************)
815    
816    (** we add a new constructor named TC_RBOX through the token facility *)
817    local val name = "TC_WRAP"
818          val abbrev = "WR"
819          val is_known = fn _ => true      (* why is this ? *)
820          fun tcc_tok k t = tcc_token(k, t)
821    
822          fun unknown tc =
823            (case tc_outX tc
824              of (TC_VAR _ | TC_NVAR _) => true
825               | (TC_APP(tc, _)) => unknown tc
826               | (TC_PROJ(tc, _)) => unknown tc
827               | _ => false)
828    
829          fun flex_tuple ts =
830            let fun hhh(x::r, ukn, wfree) =
831                     let fun iswp tc =
832                           (case tc_outX tc
833                             of TC_TOKEN(k', t) => (* WARNING: need check k' *)
834                                  (case tc_outX t
835                                    of TC_PRIM pt => false
836                                     | _ => true)
837                              | _ => true)
838                      in hhh(r, (unknown x) orelse ukn, (iswp x) andalso wfree)
839                     end
840                  | hhh([], ukn, wfree) = ukn andalso wfree
841             in hhh(ts, false, true)
842            end
843    
844          fun is_whnm tc =
845            (case tc_outX tc
846              of (TC_ARROW(FF_FIXED, [t], _)) => (unknown t)
847               | (TC_TUPLE(rf, ts)) => flex_tuple ts
848               | (TC_PRIM pt) => PT.unboxed pt
849               | _ => false)
850    
851          (* invariants: tc itself is in whnm but is_whnm tc = false *)
852          fun reduce_one (k, tc) =
853            (case tc_outX tc
854              of TC_TUPLE (rk, ts) =>
855                   let fun hhh (x::r, nts, ukn) =
856                             let val nx = tc_whnm x
857                                 val b1 = unknown nx
858                                 val nnx =
859                                   (case tc_outX nx
860                                     of TC_TOKEN(k', t) =>
861                                          if token_eq(k, k') then
862                                            (case tc_outX t
863                                              of TC_PRIM _ => t
864                                               | _ => nx)
865                                          else nx
866                                      | _ => nx)
867                              in hhh(r, nnx::nts, b1 orelse ukn)
868                             end
869                         | hhh ([], nts, ukn) =
870                             let val nt = tcc_tup(rk, rev nts)
871                              in if ukn then tcc_token(k, nt) else nt
872                             end
873                    in hhh(ts, [], false)
874                   end
875               | TC_ARROW (FF_FIXED, [_,_], [_]) => tc
876               | TC_ARROW (FF_FIXED, [t1], ts2 as [_]) =>
877                   let val nt1 = tc_whnm t1
878                       fun ggg z =
879                         let val nz = tc_whnm z
880                          in (case tc_outX nz
881                               of TC_PRIM pt =>
882                                    if PT.unboxed pt then tcc_token(k, nz)
883                                    else nz
884                                | _ => nz)
885                         end
886                       val (wp, nts1) =
887                         (case tc_outX nt1
888                           of TC_TUPLE(_, [x,y]) => (false, [ggg x, ggg y])
889                            | TC_TOKEN(k', x) =>
890                                if token_eq(k, k') then
891                                  (case (tc_outX x)
892                                    of TC_TUPLE(_, [y, z]) =>
893                                        (false, [ggg y, ggg z])
894                                     | _ => (true, [nt1]))
895                                else (false, [nt1])
896                            | _ => (unknown nt1, [nt1]))
897                       val nt = tcc_arw(FF_FIXED, nts1, ts2)
898                    in if wp then tcc_token(k, nt) else nt
899                   end
900               | TC_ARROW (FF_FIXED, _, _) =>
901                   bug "unexpected reduce_one on ill-formed FF_FIX arrow types"
902               | TC_ARROW (FF_VAR(b1,b2), ts1, ts2) =>
903                   bug "calling reduce_one on FF_VAR arrow types"
904               | TC_PRIM pt =>
905                   if PT.unboxed pt then
906                     bug "calling reduce_one on an already-reduced whnm"
907                   else tc
908               | TC_TOKEN(k', t) =>
909                   if token_eq(k, k') then tc
910                   else bug "unexpected token in reduce_one"
911               | (TC_BOX _ | TC_ABS _ | TC_PARROW _) =>
912                   bug "unexpected tc_box/abs/parrow in reduce_one"
913               | TC_ENV _ => bug "unexpected TC_ENV in reduce_one"
914               | TC_IND _ => bug "unexpected TC_IND in reduce_one"
915               | _ => tc)
916    
917    in
918    
919    val wrap_token =
920      register_token {name=name, abbrev=abbrev, reduce_one=reduce_one,
921                      is_whnm=is_whnm, is_known=is_known}
922    
923    end (* end of creating the box token for "tcc_rbox" *)
924    
925    (** testing if a tyc is a unknown constructor *)
926    fun tc_unknown tc = not (isKnown tc)
927    
928    (***************************************************************************
929   *         REBINDING THE INJECTION AND PROJECTION FUNCTIONS                *   *         REBINDING THE INJECTION AND PROJECTION FUNCTIONS                *
930   ***************************************************************************)   ***************************************************************************)
931  (** converting from the standard reps to the hash-consing reps *)  (** converting from the standard reps to the hash-consing reps *)
# Line 785  Line 964 
964           (eqop1(a1, a2)) andalso (eqlist(eqop2, b1, b2))           (eqop1(a1, a2)) andalso (eqlist(eqop2, b1, b2))
965       | (TC_SEQ ts1, TC_SEQ ts2) => eqlist(eqop1, ts1, ts2)       | (TC_SEQ ts1, TC_SEQ ts2) => eqlist(eqop1, ts1, ts2)
966       | (TC_SUM ts1, TC_SUM ts2) => eqlist(eqop1, ts1, ts2)       | (TC_SUM ts1, TC_SUM ts2) => eqlist(eqop1, ts1, ts2)
967       | (TC_TUPLE ts1, TC_TUPLE ts2) => eqlist(eqop1, ts1, ts2)       | (TC_TUPLE (_, ts1), TC_TUPLE (_, ts2)) => eqlist(eqop1, ts1, ts2)
968       | (TC_ABS a, TC_ABS b) => eqop1(a, b)       | (TC_ABS a, TC_ABS b) => eqop1(a, b)
969       | (TC_ABS a, _) => eqop3(a, t2)       | (TC_ABS a, _) => eqop3(a, t2)
970       | (_, TC_ABS b) => eqop3(t1, b)       | (_, TC_ABS b) => eqop3(t1, b)
971       | (TC_BOX a, TC_BOX b) => eqop1(a, b)       | (TC_BOX a, TC_BOX b) => eqop1(a, b)
972       | (TC_BOX a, _) => eqop3(a, t2)       | (TC_BOX a, _) => eqop3(a, t2)
973       | (_, TC_BOX b) => eqop3(t1, b)       | (_, TC_BOX b) => eqop3(t1, b)
974         | (TC_TOKEN(k1,t1), TC_TOKEN(k2,t2)) =>
975             (token_eq(k1,k2)) andalso (eqop1(t1,t2))
976       | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>       | (TC_PROJ(a1, i1), TC_PROJ(a2, i2)) =>
977           (i1 = i2) andalso (eqop1(a1, a2))           (i1 = i2) andalso (eqop1(a1, a2))
978       | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>       | (TC_ARROW(r1, a1, b1), TC_ARROW(r2, a2, b2)) =>
# Line 813  Line 994 
994                             fn (ts1, ts2) => eqlist(tc_eqv, ts1, ts2)) (t1, t2)                             fn (ts1, ts2) => eqlist(tc_eqv, ts1, ts2)) (t1, t2)
995        end (* function tc_eqv *)        end (* function tc_eqv *)
996    
997    fun tc_eqv_x (x, y) =
998      let val t1 = tc_whnm x
999          val t2 = tc_whnm y
1000       in (if (tcp_norm t1) andalso (tcp_norm t2) then tc_eq(t1, t2)
1001           else false) orelse
1002           (tc_eqv_gen (tc_eqv_x, tc_eqv_x, fn _ => false,
1003                        fn (ts1, ts2) => eqlist(tc_eqv_x, ts1, ts2)) (t1, t2))
1004      end (* function tc_eqv_x *)
1005    
1006  (** testing the equivalence of two tycs with relaxed constraints *)  (** testing the equivalence of two tycs with relaxed constraints *)
1007  fun tc_eqv_bx (x : tyc, y) =  fun tc_eqv_bx (x : tyc, y) =
1008    let val t1 = tc_whnm x    let val t1 = tc_whnm x
# Line 873  Line 1063 
1063    
1064  fun lt_eqv(x : lty, y) =  fun lt_eqv(x : lty, y) =
1065    let val seq = lt_eqv_gen (lt_eqv, tc_eqv)    let val seq = lt_eqv_gen (lt_eqv, tc_eqv)
1066     in if (ltp_norm x) andalso (ltp_norm y) then     in if ((ltp_norm x) andalso (ltp_norm y)) then
1067               (lt_eq(x, y)) orelse (seq(x, y))
1068          else (let val t1 = lt_whnm x
1069                    val t2 = lt_whnm y
1070                 in if (ltp_norm t1) andalso (ltp_norm t2) then
1071                      (lt_eq(t1, t2)) orelse (seq(t1, t2))
1072                    else seq(t1, t2)
1073                end)
1074      end (* function lt_eqv *)
1075    
1076    fun lt_eqv_x(x : lty, y) =
1077      let val seq = lt_eqv_gen (lt_eqv_x, tc_eqv_x)
1078       in if ((ltp_norm x) andalso (ltp_norm y)) then
1079          (lt_eq(x, y)) orelse (seq(x, y))          (lt_eq(x, y)) orelse (seq(x, y))
1080        else (let val t1 = lt_whnm x        else (let val t1 = lt_whnm x
1081                  val t2 = lt_whnm y                  val t2 = lt_whnm y
# Line 895  Line 1097 
1097              end)              end)
1098    end (* function lt_eqv_bx *)    end (* function lt_eqv_bx *)
1099    
1100    (** testing equivalence of fflags and rflags *)
1101    val ff_eqv   : fflag * fflag -> bool = (op =)
1102    val rf_eqv   : rflag * rflag -> bool = (op =)
1103    
1104    (***************************************************************************
1105     *  UTILITY FUNCTIONS ON FINDING OUT THE DEPTH OF THE FREE TYC VARIABLES   *
1106     ***************************************************************************)
1107    (** finding out the innermost binding depth for a tyc's free variables *)
1108    fun tc_depth (x, d) =
1109      let val tvs = tc_vs (tc_norm x)
1110          (* unfortunately we have to reduce everything to the normal form
1111             before we can talk about its list of free type variables.
1112           *)
1113       in case tvs
1114           of NONE => bug "unexpected case in tc_depth"
1115            | SOME [] => DI.top
1116            | SOME (a::_) => d + 1 - (#1(tvFromInt a))
1117      end
1118    
1119    fun tcs_depth ([], d) = DI.top
1120      | tcs_depth (x::r, d) = Int.max(tc_depth(x, d), tcs_depth(r, d))
1121    
1122  end (* toplevel local *)  end (* toplevel local *)
1123  end (* abstraction LtyKernel *)  end (* abstraction LtyKernel *)
1124    

Legend:
Removed from v.44  
changed lines
  Added in v.45

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