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/primop-branch-3/compiler/FLINT/kernel/ltybasic.sml
ViewVC logotype

Diff of /sml/branches/primop-branch-3/compiler/FLINT/kernel/ltybasic.sml

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

revision 24, Thu Mar 12 00:49:58 1998 UTC revision 45, Sun Mar 22 20:11:09 1998 UTC
# Line 23  Line 23 
23    
24        val tcc_env = LK.tcc_env        val tcc_env = LK.tcc_env
25        val ltc_env = LK.ltc_env        val ltc_env = LK.ltc_env
       val tc_whnm = LK.tc_whnm  
       val lt_whnm = LK.lt_whnm  
       val tc_norm = LK.tc_norm  
       val lt_norm = LK.lt_norm  
26    
27        val itos = Int.toString        val itos = Int.toString
28        fun plist(p, []) = ""        fun plist(p, []) = ""
29          | plist(p, x::xs) =          | plist(p, x::xs) =
30              (p x) ^ (String.concat (map (fn z => ("," ^ (p z))) xs))              (p x) ^ (String.concat (map (fn z => ("," ^ (p z))) xs))
31    
32        fun parw(p, (t1, t2)) = "<" ^ (p t1) ^ "> -> <" ^ (p t2) ^ ">"        fun pfflag (LK.FF_VAR b) =
33                let fun pff (true, true) = "rr"  | pff (true, false) = "rc"
34                      | pff (false, true) = "cr" | pff (false, false) = "cc"
35                 in pff b
36                end
37            | pfflag (LK.FF_FIXED) = "f"
38    
39          fun parw(p, (ff, t1, t2)) =
40                "<" ^ (p t1) ^ "> -" ^ pfflag ff ^ "-> <" ^ (p t2) ^ ">"
41  in  in
42    
43  open LtyDef  open LtyDef
# Line 47  Line 51 
51     in h(n, [])     in h(n, [])
52    end    end
53    
54  val tkc_fn1 = tkc_fun(tkc_seq(tkc_arg 1), tkc_mono)  val tkc_fn1 = tkc_fun(tkc_arg 1, tkc_mono)
55  val tkc_fn2 = tkc_fun(tkc_seq(tkc_arg 2), tkc_mono)  val tkc_fn2 = tkc_fun(tkc_arg 2, tkc_mono)
56  val tkc_fn3 = tkc_fun(tkc_seq(tkc_arg 3), tkc_mono)  val tkc_fn3 = tkc_fun(tkc_arg 3, tkc_mono)
57    
58  fun tkc_int 0 = tkc_mono  fun tkc_int 0 = tkc_mono
59    | tkc_int 1 = tkc_fn1    | tkc_int 1 = tkc_fn1
60    | tkc_int 2 = tkc_fn2    | tkc_int 2 = tkc_fn2
61    | tkc_int 3 = tkc_fn3    | tkc_int 3 = tkc_fn3
62    | tkc_int i = tkc_fun(tkc_seq(tkc_arg i), tkc_mono)    | tkc_int i = tkc_fun(tkc_arg i, tkc_mono)
63    
64    (** primitive fflags and rflags *)
65    val ffc_plambda = ffc_var (false, false)
66    val ffc_rrflint = ffc_var (true, true)
67    
68    fun ffc_fspec (x as LK.FF_FIXED, (true,true)) = x
69      | ffc_fspec (x as LK.FF_VAR _, nx) = ffc_var nx
70      | ffc_fspec _ = bug "unexpected case in ffc_fspec"
71    
72    fun ffd_fspec (LK.FF_FIXED) = (true,true)
73      | ffd_fspec (LK.FF_VAR x) = x
74    
75  (** utility functions for constructing tycs *)  (** utility functions for constructing tycs *)
76  val tcc_int    = tcc_prim PT.ptc_int31  val tcc_int    = tcc_prim PT.ptc_int31
# Line 111  Line 126 
126   *            UTILITY FUNCTIONS FOR TESTING EQUIVALENCE                    *   *            UTILITY FUNCTIONS FOR TESTING EQUIVALENCE                    *
127   ***************************************************************************)   ***************************************************************************)
128    
129  (** testing equivalence of tkinds, tycs, and ltys *)  (** testing equivalence of tkinds, tycs, ltys, fflags, and rflags *)
130  val tk_eqv    : tkind * tkind -> bool = LK.tk_eqv  val tk_eqv    : tkind * tkind -> bool = LK.tk_eqv
131  val tc_eqv    : tyc * tyc -> bool = LK.tc_eqv  val tc_eqv    : tyc * tyc -> bool = LK.tc_eqv
132  val lt_eqv    : lty * lty -> bool = LK.lt_eqv  val lt_eqv    : lty * lty -> bool = LK.lt_eqv
133    val ff_eqv    : fflag * fflag -> bool = LK.ff_eqv
134    val rf_eqv    : rflag * rflag -> bool = LK.rf_eqv
135    
136  (** testing the equivalence for tycs and ltys with relaxed constraints *)  (** testing the equivalence for tycs and ltys with relaxed constraints *)
137    val tc_eqv_x  : tyc * tyc -> bool = LK.tc_eqv_x
138    val lt_eqv_x  : lty * lty -> bool = LK.lt_eqv_x
139  val tc_eqv_bx : tyc * tyc -> bool = LK.tc_eqv_bx  val tc_eqv_bx : tyc * tyc -> bool = LK.tc_eqv_bx
140  val lt_eqv_bx : lty * lty -> bool = LK.lt_eqv_bx  val lt_eqv_bx : lty * lty -> bool = LK.lt_eqv_bx
141    
# Line 128  Line 147 
147  fun tk_print (x : tkind) =  fun tk_print (x : tkind) =
148    let fun g (LK.TK_MONO) = "K0"    let fun g (LK.TK_MONO) = "K0"
149          | g (LK.TK_BOX) = "KB0"          | g (LK.TK_BOX) = "KB0"
150          | g (LK.TK_FUN z) =  (parw(tk_print, z))          | g (LK.TK_FUN (ks, k)) =
151                   "<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"
152          | g (LK.TK_SEQ zs) = "KS(" ^ (plist(tk_print, zs)) ^ ")"          | g (LK.TK_SEQ zs) = "KS(" ^ (plist(tk_print, zs)) ^ ")"
153     in g (tk_out x)     in g (tk_out x)
154    end    end
# Line 138  Line 158 
158          | g (LK.TC_NVAR(v,d,i)) = "NTV(v" ^ (itos v) ^ "," ^ (itos d)          | g (LK.TC_NVAR(v,d,i)) = "NTV(v" ^ (itos v) ^ "," ^ (itos d)
159                                 ^ "," ^ (itos i) ^ ")"                                 ^ "," ^ (itos i) ^ ")"
160          | g (LK.TC_PRIM pt) = PT.pt_print pt          | g (LK.TC_PRIM pt) = PT.pt_print pt
         | g (LK.TC_FN([], t)) = "TF(0," ^ (tc_print t) ^ ")"  
161          | g (LK.TC_FN(ks, t)) =          | g (LK.TC_FN(ks, t)) =
162                "\\" ^ (itos (length ks)) ^ ".(" ^ (tc_print t) ^ ")"                "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"
163          | g (LK.TC_APP(t, [])) = tc_print t ^ "[]"          | g (LK.TC_APP(t, [])) = tc_print t ^ "[]"
164          | g (LK.TC_APP(t, zs)) =          | g (LK.TC_APP(t, zs)) =
165                (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"                (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"
# Line 154  Line 173 
173                else if tc_eqv(x,tcc_list) then "LST"                else if tc_eqv(x,tcc_list) then "LST"
174                     else (let val ntc = case ts of [] => tc                     else (let val ntc = case ts of [] => tc
175                                                  | _ => tcc_app(tc, ts)                                                  | _ => tcc_app(tc, ts)
176                            in ("DT{" ^ (tc_print ntc) ^ "===" ^ (itos i) ^ "}")                            in ("DT{" ^ "DATA" (* (tc_print ntc) *)
177                                        ^ "===" ^ (itos i) ^ "}")
178                           end)                           end)
179          | g (LK.TC_ABS t) = "Ax(" ^ (tc_print t) ^ ")"          | g (LK.TC_ABS t) = "Ax(" ^ (tc_print t) ^ ")"
180          | g (LK.TC_BOX t) = "Bx(" ^ (tc_print t) ^ ")"          | g (LK.TC_BOX t) = "Bx(" ^ (tc_print t) ^ ")"
181          | g (LK.TC_TUPLE zs) = "TT<" ^ (plist(tc_print, zs)) ^ ">"          | g (LK.TC_TUPLE(_,zs)) = "TT<" ^ (plist(tc_print, zs)) ^ ">"
182          | g (LK.TC_ARROW (_,z1,z2)) = parw(fn u => plist(tc_print,u), (z1,z2))          | g (LK.TC_ARROW (ff,z1,z2)) =
183                   parw(fn u => plist(tc_print,u),(ff,z1,z2))
184          | g (LK.TC_PARROW _) = bug "unexpected TC_PARROW in tc_print"          | g (LK.TC_PARROW _) = bug "unexpected TC_PARROW in tc_print"
185            | g (LK.TC_TOKEN (k, t)) =
186                  if LK.token_isvalid k then
187                     (LK.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"
188                  else bug "unexpected TC_TOKEN tyc in tc_print"
189          | g (LK.TC_CONT ts) = "Cnt(" ^ (plist(tc_print,ts)) ^ ")"          | g (LK.TC_CONT ts) = "Cnt(" ^ (plist(tc_print,ts)) ^ ")"
190          | g (LK.TC_IND _) = bug "unexpected TC_IND in tc_print"          | g (LK.TC_IND _) = bug "unexpected TC_IND in tc_print"
191          | g (LK.TC_ENV _) = bug "unexpected TC_ENV in tc_print"          | g (LK.TC_ENV _) = bug "unexpected TC_ENV in tc_print"
# Line 177  Line 202 
202               "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("               "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("
203                   ^ (plist(lt_print, ts2)) ^ ")"                   ^ (plist(lt_print, ts2)) ^ ")"
204          | g (LK.LT_POLY(ks, ts)) =          | g (LK.LT_POLY(ks, ts)) =
205               "Q" ^ (itos (length ks)) ^ ".(" ^ (plist(lt_print,ts)) ^ ")"               "(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"
206          | g (LK.LT_CONT ts) = "CNT(" ^ (plist(lt_print, ts)) ^ ")"          | g (LK.LT_CONT ts) = "CNT(" ^ (plist(lt_print, ts)) ^ ")"
207          | g (LK.LT_IND _) = bug "unexpected LT_IND in lt_print"          | g (LK.LT_IND _) = bug "unexpected LT_IND in lt_print"
208          | g (LK.LT_ENV _) = bug "unexpected LT_ENV in lt_print"          | g (LK.LT_ENV _) = bug "unexpected LT_ENV in lt_print"
# Line 191  Line 216 
216    
217  (** adjusting an lty or tyc from one depth to another *)  (** adjusting an lty or tyc from one depth to another *)
218  fun lt_adj (lt, d, nd) =  fun lt_adj (lt, d, nd) =
219    if d = nd then lt else lt_norm(ltc_env(lt, 0, nd - d, LK.initTycEnv))    if d = nd then lt
220      else ltc_env(lt, 0, nd - d, LK.initTycEnv)
221    
222  fun tc_adj (tc, d, nd) =  fun tc_adj (tc, d, nd) =
223    if d = nd then tc else tc_norm(tcc_env(tc, 0, nd - d, LK.initTycEnv))    if d = nd then tc
224      else tcc_env(tc, 0, nd - d, LK.initTycEnv)
225    
226    (** the following functions does the smiliar thing as lt_adj and
227        tc_adj; it adjusts an lty (or tyc) from depth d+k to depth nd+k,
228        assuming the last k levels are type abstractions. So lt_adj
229        is really lt_adj_k with k set to 0. Both functions are currently
230        called inside the lcontract.sml only. *)
231    local
232    fun mkTycEnv (i, k, dd, e) =
233      if i >= k then e else mkTycEnv(i+1, k, dd, LK.tcInsert(e,(NONE, dd+i)))
234    
235  (** the following function is called only inside transtype.sml *)  in
236  fun tc_adj_one (tc, d, nd) =  fun lt_adj_k (lt, d, nd, k) =
237      if d = nd then lt
238      else ltc_env(lt, k, nd-d+k, mkTycEnv(0, k, nd-d, LK.initTycEnv))
239    
240    fun tc_adj_k (tc, d, nd, k) =
241    if d = nd then tc    if d = nd then tc
242    else (let val dd = nd - d    else tcc_env(tc, k, nd-d+k, mkTycEnv(0, k, nd-d, LK.initTycEnv))
243           in tc_norm(tcc_env(tc, 1, dd + 1,  
244                              LK.tcInsert(LK.initTycEnv, (NONE, dd))))  end (* lt_adj_k and tc_adj_k *)
         end)  
245    
246  (** automatically flattening the argument or the result type *)  (** automatically flattening the argument or the result type *)
247  val lt_autoflat : lty -> bool * lty list * bool = LK.lt_autoflat  val lt_autoflat : lty -> bool * lty list * bool = LK.lt_autoflat
248    
249    (** testing if a tyc is a unknown constructor *)
250    val tc_unknown : tyc -> bool = LK.tc_unknown
251    
252  (***************************************************************************  (***************************************************************************
253   *            UTILITY FUNCTIONS ON TKIND ENVIRONMENT                       *   *            UTILITY FUNCTIONS ON TKIND ENVIRONMENT                       *
254   ***************************************************************************)   ***************************************************************************)

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

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