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/ltyextern.sml
ViewVC logotype

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

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

revision 52, Mon Mar 23 03:59:51 1998 UTC revision 53, Mon Mar 23 04:02:58 1998 UTC
# Line 52  Line 52 
52  val lt_inst_st = (map lt_norm) o lt_inst   (* strict instantiation *)  val lt_inst_st = (map lt_norm) o lt_inst   (* strict instantiation *)
53  val lt_pinst_st = lt_norm o lt_pinst   (* strict instantiation *)  val lt_pinst_st = lt_norm o lt_pinst   (* strict instantiation *)
54    
55    (********************************************************************
56     *                      KIND-CHECKING ROUTINES                      *
57     ********************************************************************)
58  exception TkTycChk  exception TkTycChk
59  exception LtyAppChk  exception LtyAppChk
60    
61    (* tkSubkind returns true if k1 is a subkind of k2, or if they are
62     * equivalent kinds.  it is NOT commutative.  tksSubkind is the same
63     * thing, component-wise on lists of kinds.
64     *)
65    fun tksSubkind (ks1, ks2) =
66        ListPair.all tkSubkind (ks1, ks2)   (* component-wise *)
67    and tkSubkind (k1, k2) =
68        tk_eqv (k1, k2) orelse              (* reflexive *)
69        case (tk_out k1, tk_out k2) of
70            (LK.TK_BOX, LK.TK_MONO) => true (* ground kinds (base case) *)
71          (* this next case is WRONG, but necessary until the
72           * infrastructure is there to give proper boxed kinds to
73           * certain tycons (e.g., ref : Omega -> Omega_b)
74           *)
75          | (LK.TK_MONO, LK.TK_BOX) => true
76          | (LK.TK_SEQ ks1, LK.TK_SEQ ks2) =>
77              tksSubkind (ks1, ks2)
78          | (LK.TK_FUN (ks1, k1'), LK.TK_FUN (ks2, k2')) =>
79              tksSubkind (ks1, ks2) andalso (* contravariant *)
80              tkSubkind (k1', k2')
81          | _ => false
82    
83    (* is a kind monomorphic? *)
84    fun tkIsMono k = tkSubkind (k, tkc_mono)
85    
86    (* assert that k1 is a subkind of k2 *)
87    fun tkAssertSubkind (k1, k2) =
88        if tkSubkind (k1, k2) then ()
89        else raise TkTycChk
90    
91    (* assert that a kind is monomorphic *)
92    fun tkAssertIsMono k =
93        if tkIsMono k then ()
94        else raise TkTycChk
95    
96    (* select the ith element from a kind sequence *)
97  fun tkSel (tk, i) =  fun tkSel (tk, i) =
98    (case (tk_out tk)    (case (tk_out tk)
99      of (LK.TK_SEQ ks) => (List.nth(ks, i) handle _ => raise TkTycChk)      of (LK.TK_SEQ ks) => (List.nth(ks, i) handle _ => raise TkTycChk)
100       | _ => raise TkTycChk)       | _ => raise TkTycChk)
101    
102  fun tks_eqv (ks1, ks2) = tk_eqv(tkc_seq ks1, tkc_seq ks2)  (* check the application of tycs of kinds `tks' to a type function of
103     * kind `tk'.
104     *)
105  fun tkApp (tk, tks) =  fun tkApp (tk, tks) =
106    (case (tk_out tk)    (case (tk_out tk)
107      of LK.TK_FUN(a, b) => if tks_eqv(a, tks) then b else raise TkTycChk      of LK.TK_FUN(a, b) =>
108           if tksSubkind(tks, a) then b else raise TkTycChk
109       | _ => raise TkTycChk)       | _ => raise TkTycChk)
110    
111  (* Warning: the following tkTyc function has not considered the  (* Kind-checking naturally requires traversing type graphs.  to avoid
112   * occurence of .TK_BOX, in other words, if there is TK_BOX present,   * re-traversing bits of the dag, we use a dictionary to memoize the
113   * then the tk_tyc checker will produce wrong results. (ZHONG)   * kind of each tyc we process.
114   *)   *
115  fun tk_tyc (t, kenv) =   * The problem is that a tyc can have different kinds, depending on
116    let fun g x =   * the valuations of its free variables.  So this dictionary maps a
117          (case tc_out x   * tyc to an association list that maps the kinds of the free
118            of (LK.TC_VAR (i, j)) => tkLookup(kenv, i, j)   * variables in the tyc (represented as a TK_SEQ) to the tyc's kind.
119             | (LK.TC_NVAR _) => bug "TC_NVAR not supported yet in tk_tyc"   *)
120             | (LK.TC_PRIM pt) => tkc_int (PrimTyc.pt_arity pt)  structure Memo :> sig
121             | (LK.TC_FN(ks, tc)) =>      type dict
122                 tkc_fun(ks, tk_tyc(tc, tkInsert(kenv, ks)))      val newDict         : unit -> dict
123             | (LK.TC_APP (tc, tcs)) => tkApp(g tc, map g tcs)      val recallOrCompute : dict * tkindEnv * tyc * (unit -> tkind) -> tkind
124             | (LK.TC_SEQ tcs) => tkc_seq (map g tcs)  end =
125             | (LK.TC_PROJ(tc, i)) => tkSel(g tc, i)  struct
126             | (LK.TC_SUM tcs) =>      structure TcDict = BinaryDict
127                 let val _ = map (fn x => tk_eqv(g x, tkc_mono)) tcs                             (struct
128                  in tkc_mono                                 type ord_key = tyc
129                                   val cmpKey = LK.tc_cmp
130                               end)
131    
132        type dict = (tkind * tkind) list TcDict.dict ref
133        val newDict : unit -> dict = ref o TcDict.mkDict
134    
135        fun recallOrCompute (dict, kenv, tyc, doit) =
136            (* what are the free vars of this tyc? *)
137            (* (might not be available for some tycs) *)
138            case LK.tc_freevars tyc of
139                SOME fvs => let
140                    (* get valuations of tyc's free variables in kenv *)
141                    val ks_fvs = tkLookupFreeVars (kenv, fvs)
142                    (* encode those as a kind sequence *)
143                    val k_fvs = tkc_seq ks_fvs
144                    (* query the dictionary *)
145                    val kci = case TcDict.peek(!dict, tyc) of
146                        SOME kci => kci
147                      | NONE => []
148                    (* look for an equivalent environment *)
149                    fun sameEnv (k_fvs',_) = tk_eqv(k_fvs, k_fvs')
150                in
151                    case List.find sameEnv kci of
152                        SOME (_,k) => k     (* HIT! *)
153                      | NONE => let
154                            (* not in the list.  we will compute
155                             * the answer and cache it
156                             *)
157                            val k = doit()
158                            val kci' = (k_fvs, k) :: kci
159                        in
160                            dict := TcDict.insert(!dict, tyc, kci');
161                            k
162                 end                 end
163             | (LK.TC_FIX ((n, tc, ts), i)) =>              end
164              | NONE =>
165                (* freevars were not available.  we'll have to
166                 * recompute and cannot cache the result.
167                 *)
168                doit()
169    
170    end (* Memo *)
171    
172    (* return the kind of a given tyc in the given kind environment *)
173    fun tkTycGen() = let
174        val dict = Memo.newDict()
175    
176        fun tkTyc kenv t = let
177            (* default recursive invocation *)
178            val g = tkTyc kenv
179            (* how to compute the kind of a tyc *)
180            fun mk() =
181                case tc_out t of
182                    LK.TC_VAR (i, j) =>
183                    tkLookup (kenv, i, j)
184                  | LK.TC_NVAR _ =>
185                    bug "TC_NVAR not supported yet in tkTyc"
186                  | LK.TC_PRIM pt =>
187                    tkc_int (PrimTyc.pt_arity pt)
188                  | LK.TC_FN(ks, tc) =>
189                    tkc_fun(ks, tkTyc (tkInsert (kenv,ks)) tc)
190                  | LK.TC_APP (tc, tcs) =>
191                    tkApp (g tc, map g tcs)
192                  | LK.TC_SEQ tcs =>
193                    tkc_seq (map g tcs)
194                  | LK.TC_PROJ(tc, i) =>
195                    tkSel(g tc, i)
196                  | LK.TC_SUM tcs =>
197                    (List.app (tkAssertIsMono o g) tcs;
198                     tkc_mono)
199                  | LK.TC_FIX ((n, tc, ts), i) =>
200                 let val k = g tc                 let val k = g tc
201                     val nk = case ts of [] => k                      val nk =
202                            case ts of
203                                [] => k
204                                       | _ => tkApp(k, map g ts)                                       | _ => tkApp(k, map g ts)
205                  in (case (tk_out nk)                  in
206                       of LK.TK_FUN(a, b) =>                      case (tk_out nk) of
207                            let val arg = case a of [x] => x                          LK.TK_FUN(a, b) =>
208                            let val arg =
209                                    case a of
210                                        [x] => x
211                                                  | _ => tkc_seq a                                                  | _ => tkc_seq a
212                             in if tk_eqv(arg, b) then                          in
213                                if tkSubkind(arg, b) then (* order? *)
214                                  (if n = 1 then b else tkSel(arg, i))                                  (if n = 1 then b else tkSel(arg, i))
215                                else raise TkTycChk                                else raise TkTycChk
216                            end                            end
217                        | _ => raise TkTycChk)                        | _ => raise TkTycChk
218                 end                 end
219             | (LK.TC_ABS tc) => (tk_eqv(g tc, tkc_mono); tkc_mono)                | LK.TC_ABS tc =>
220             | (LK.TC_BOX tc) => (tk_eqv(g tc, tkc_mono); tkc_mono)                  (tkAssertIsMono (g tc);
221             | (LK.TC_TUPLE (_,tcs)) =>                   tkc_mono)
222                 let val _ = map (fn x => tk_eqv(g x, tkc_mono)) tcs                | LK.TC_BOX tc =>
223                  in tkc_mono                  (tkAssertIsMono (g tc);
224                 end                   tkc_mono)
225             | (LK.TC_ARROW (_, ts1, ts2)) =>                | LK.TC_TUPLE (_,tcs) =>
226                 let val _ = map (fn x => tk_eqv(g x, tkc_mono)) ts1                  (List.app (tkAssertIsMono o g) tcs;
227                     val _ = map (fn x => tk_eqv(g x, tkc_mono)) ts2                   tkc_mono)
228                  in tkc_mono                | LK.TC_ARROW (_, ts1, ts2) =>
229                 end                  (List.app (tkAssertIsMono o g) ts1;
230             | _ => bug "unexpected TC_ENV or TC_CONT in tk_tyc")                   List.app (tkAssertIsMono o g) ts2;
231     in g t                   tkc_mono)
232    end                | _ => bug "unexpected TC_ENV or TC_CONT in tkTyc"
233        in
234  and tk_chk kenv (k, tc) =          Memo.recallOrCompute (dict, kenv, t, mk)
235    if tk_eqv(k, tk_tyc(tc, kenv)) then () else raise TkTycChk      end
236    in
237        tkTyc
238    end
239    
240    (* assert that the kind of `tc' is a subkind of `k' in `kenv' *)
241    fun tkChkGen() = let
242        val tkTyc = tkTycGen()
243        fun tkChk kenv (k, tc) =
244            tkAssertSubkind (tkTyc kenv tc, k)
245    in
246        tkChk
247    end
248    
249    (* lty application with kind-checking (exported) *)
250    fun lt_inst_chk_gen() = let
251        val tkChk = tkChkGen()
252  fun lt_inst_chk (lt : lty, ts : tyc list, kenv : tkindEnv) =  fun lt_inst_chk (lt : lty, ts : tyc list, kenv : tkindEnv) =
253    let val nt = lt_whnm lt    let val nt = lt_whnm lt
254     in (case ((* lt_outX *) lt_out nt, ts)     in (case ((* lt_outX *) lt_out nt, ts)
255          of (LK.LT_POLY(ks, b), ts) =>          of (LK.LT_POLY(ks, b), ts) =>
256               let val _ = ListPair.app (tk_chk kenv) (ks, ts)                   let val _ = ListPair.app (tkChk kenv) (ks, ts)
257                   fun h x = ltc_env(x, 1, 0, tcInsert(initTycEnv, (SOME ts, 0)))                       fun h x = ltc_env(x, 1, 0,
258                                           tcInsert(initTycEnv, (SOME ts, 0)))
259                in map h b                in map h b
260               end               end
261           | (_, []) => [nt]    (* ? problematic *)           | (_, []) => [nt]    (* ? problematic *)
262           | _ => raise LtyAppChk)           | _ => raise LtyAppChk)
263    end    end
264    in
265        lt_inst_chk
266    end
267    
268  (** a special lty application --- used inside the translate/specialize.sml *)  (** a special lty application --- used inside the translate/specialize.sml *)
269  fun lt_sp_adj(ks, lt, ts, dist, bnl) =  fun lt_sp_adj(ks, lt, ts, dist, bnl) =

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

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