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 2221, Tue Nov 28 21:56:55 2006 UTC revision 2222, Tue Nov 28 22:02:39 2006 UTC
# Line 6  Line 6 
6    
7  local structure PT = PrimTyc  local structure PT = PrimTyc
8        structure DI = DebIndex        structure DI = DebIndex
9          structure LT = Lty
10        structure LK = LtyKernel        structure LK = LtyKernel
11    
12        fun bug msg = ErrorMsg.impossible("LtyExtern: "^msg)        fun bug msg = ErrorMsg.impossible("LtyExtern: "^msg)
# Line 24  Line 25 
25        val tcc_env = LK.tcc_env        val tcc_env = LK.tcc_env
26        val ltc_env = LK.ltc_env        val ltc_env = LK.ltc_env
27    
28    (* duplicated in ltykernel.sml *)
29    
30        val itos = Int.toString        val itos = Int.toString
31    
32        fun plist(p, []) = ""        fun plist(p, []) = ""
33          | plist(p, x::xs) =          | plist(p, x::xs) =
34              (p x) ^ (String.concat (map (fn z => ("," ^ (p z))) xs))              (p x) ^ (String.concat (map (fn z => ("," ^ (p z))) xs))
35    
36        fun pfflag (LK.FF_VAR b) =        fun pfflag (LT.FF_VAR b) =
37              let fun pff (true, true) = "rr"  | pff (true, false) = "rc"              let fun pff (true, true) = "rr"  | pff (true, false) = "rc"
38                    | pff (false, true) = "cr" | pff (false, false) = "cc"                    | pff (false, true) = "cr" | pff (false, false) = "cc"
39               in pff b               in pff b
40              end              end
41          | pfflag (LK.FF_FIXED) = "f"          | pfflag (LT.FF_FIXED) = "f"
42    
43        fun parw(p, (ff, t1, t2)) =        fun parw(p, (ff, t1, t2)) =
44              "<" ^ (p t1) ^ "> -" ^ pfflag ff ^ "-> <" ^ (p t2) ^ ">"              "<" ^ (p t1) ^ "> -" ^ pfflag ff ^ "-> <" ^ (p t2) ^ ">"
45    
46  in  in
47    
48  open LtyDef  open Lty LtyDef
49    
50  (** new a type variable, currently not used *)  (** new a type variable, currently not used *)
51  val mkTvar : unit -> tvar = LK.mkTvar  val mkTvar : unit -> tvar = LT.mkTvar
52    
53  (** utility functions for constructing tkinds *)  (** utility functions for constructing tkinds *)
54  fun tkc_arg n =  fun tkc_arg n =
# Line 65  Line 70 
70  val ffc_plambda = ffc_var (false, false)  val ffc_plambda = ffc_var (false, false)
71  val ffc_rrflint = ffc_var (true, true)  val ffc_rrflint = ffc_var (true, true)
72    
73  fun ffc_fspec (x as LK.FF_FIXED, (true,true)) = x  fun ffc_fspec (x as LT.FF_FIXED, (true,true)) = x
74    | ffc_fspec (x as LK.FF_VAR _, nx) = ffc_var nx    | ffc_fspec (x as LT.FF_VAR _, nx) = ffc_var nx
75    | ffc_fspec _ = bug "unexpected case in ffc_fspec"    | ffc_fspec _ = bug "unexpected case in ffc_fspec"
76    
77  fun ffd_fspec (LK.FF_FIXED) = (true,true)  fun ffd_fspec (LT.FF_FIXED) = (true,true)
78    | ffd_fspec (LK.FF_VAR x) = x    | ffd_fspec (LT.FF_VAR x) = x
79    
80  (** utility functions for constructing tycs *)  (** utility functions for constructing tycs *)
81  val tcc_int    = tcc_prim PT.ptc_int31  val tcc_int    = tcc_prim PT.ptc_int31
# Line 83  Line 88 
88  val tcc_bool   =  val tcc_bool   =
89    let val tbool = tcc_sum [tcc_unit, tcc_unit]    let val tbool = tcc_sum [tcc_unit, tcc_unit]
90        val tsig_bool = tcc_fn ([tkc_mono], tbool)        val tsig_bool = tcc_fn ([tkc_mono], tbool)
91     in tcc_fix((1, tsig_bool, []), 0)     in tcc_fix((1, #["bool"], tsig_bool, []), 0)
92    end    end
93    
94  val tcc_list   =  (* not exported, used for the printing purpose *)  val tcc_list   =  (* not exported, used for the printing purpose *)
# Line 95  Line 100 
100                              (** the order here should be consistent with                              (** the order here should be consistent with
101                                  that in basics/basictypes.sml **)                                  that in basics/basictypes.sml **)
102        val tsig_list = tcc_fn([tkc_int 1], tlist)        val tsig_list = tcc_fn([tkc_int 1], tlist)
103     in tcc_fix((1, tsig_list, []), 0)     in tcc_fix((1, #["list"], tsig_list, []), 0)
104    end    end
105    
106  fun tcc_tv i     = tcc_var(DI.innermost, i)  fun tcc_tv i     = tcc_var(DI.innermost, i)
# Line 133  Line 138 
138  val ff_eqv    : fflag * fflag -> bool = LK.ff_eqv  val ff_eqv    : fflag * fflag -> bool = LK.ff_eqv
139  val rf_eqv    : rflag * rflag -> bool = LK.rf_eqv  val rf_eqv    : rflag * rflag -> bool = LK.rf_eqv
140    
 (** testing the equivalence for tycs and ltys with relaxed constraints *)  
 val tc_eqv_x  : tyc * tyc -> bool = LK.tc_eqv_x  
 val lt_eqv_x  : lty * lty -> bool = LK.lt_eqv_x  
141    
142  (***************************************************************************  (***************************************************************************
143   *            UTILITY FUNCTIONS FOR PRETTY PRINTING                        *   *            UTILITY FUNCTIONS FOR PRETTY PRINTING                        *
144   ***************************************************************************)   ***************************************************************************)
145    
146  (** pretty printing of tkinds, tycs, and ltys *)  (** (pretty?) printing of tkinds, tycs, and ltys -- see pplty.sml for real
147     ** pretty printing **)
148  fun tk_print (x : tkind) =  fun tk_print (x : tkind) =
149    let fun g (LK.TK_MONO) = "K0"    (case tk_out x
150          | g (LK.TK_BOX) = "KB0"      of LT.TK_MONO => "K0"
151          | g (LK.TK_FUN (ks, k)) =       | LT.TK_BOX => "KB0"
152         | LT.TK_FUN(ks, k) =>
153                 "<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"                 "<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"
154          | g (LK.TK_SEQ zs) = "KS(" ^ (plist(tk_print, zs)) ^ ")"       | LT.TK_SEQ zs => "KS(" ^ (plist(tk_print, zs)) ^ ")")
    in g (tk_out x)  
   end  
155    
156  fun tc_print (x : tyc) =  fun tc_print (x : tyc) =
157    let fun g (LK.TC_VAR(i,j)) = "TV(" ^ (DI.di_print i) ^ "," ^ (itos j) ^ ")"    (case (tc_out x)
158          | g (LK.TC_NVAR v) = "NTV(v" ^ (itos v) ^ ")"      of LT.TC_VAR(i,j) => "TV(" ^ (DI.di_print i) ^ "," ^ (itos j) ^ ")"
159          | g (LK.TC_PRIM pt) = PT.pt_print pt       | LT.TC_NVAR v => "NTV(v" ^ (itos v) ^ ")"
160          | g (LK.TC_FN(ks, t)) =       | LT.TC_PRIM pt => PT.pt_print pt
161         | LT.TC_FN(ks, t) =>
162                "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"                "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"
163          | g (LK.TC_APP(t, [])) = tc_print t ^ "[]"       | LT.TC_APP(t, []) => tc_print t ^ "[]"
164          | g (LK.TC_APP(t, zs)) =       | LT.TC_APP(t, zs) =>
165                (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"                (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"
166          | g (LK.TC_SEQ zs) = "TS(" ^ (plist(tc_print,zs)) ^ ")"       | LT.TC_SEQ zs => "TS(" ^ (plist(tc_print,zs)) ^ ")"
167          | g (LK.TC_PROJ (t, i)) =       | LT.TC_PROJ (t, i) =>
168                "TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"                "TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"
169          | g (LK.TC_SUM tcs) =       | LT.TC_SUM tcs =>
170                "TSUM(" ^ (plist(tc_print, tcs)) ^ ")"                "TSUM(" ^ (plist(tc_print, tcs)) ^ ")"
171          | g (LK.TC_FIX ((_, tc, ts), i)) =       | LT.TC_FIX {family={gen=tc,params=ts,...}, index=i} =>
172                if tc_eqv(x,tcc_bool) then "B"                if tc_eqv(x,tcc_bool) then "B"
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                               val _ = 1                               val _ = 1
177                            in ("DT{" ^ "DATA" (* ^ "[" ^ (tc_print tc)                 in ("DT{" ^ "DATA"  ^ (* "[" ^ (tc_print tc)
178                                      ^ "] &&" ^ (plist(tc_print, ts))                                      ^ "] &&" ^ (plist(tc_print, ts))
179                                            ^ "&&" *) ^ "===" ^ (itos i) ^ "}")                     ^ "&&" ^*)  "===" ^ (itos i) ^ "}")
180                           end)                           end)
181          | g (LK.TC_ABS t) = "Ax(" ^ (tc_print t) ^ ")"       | LT.TC_ABS t => "Ax(" ^ (tc_print t) ^ ")"
182          | g (LK.TC_BOX t) = "Bx(" ^ (tc_print t) ^ ")"       | LT.TC_BOX t => "Bx(" ^ (tc_print t) ^ ")"
183          | g (LK.TC_TUPLE(_,zs)) = "TT<" ^ (plist(tc_print, zs)) ^ ">"       | LT.TC_TUPLE(_,zs) => "TT<" ^ (plist(tc_print, zs)) ^ ">"
184          | g (LK.TC_ARROW (ff,z1,z2)) =       | LT.TC_ARROW (ff,z1,z2) =>
185                 parw(fn u => plist(tc_print,u),(ff,z1,z2))                 parw(fn u => plist(tc_print,u),(ff,z1,z2))
186          | g (LK.TC_PARROW _) = bug "unexpected TC_PARROW in tc_print"       | LT.TC_PARROW _ => bug "unexpected TC_PARROW in tc_print"
187          | g (LK.TC_TOKEN (k, t)) =       | LT.TC_TOKEN (k, t) =>
188                if LK.token_isvalid k then           if LT.token_isvalid k then
189                   (LK.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"               (LT.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"
190                else bug "unexpected TC_TOKEN tyc in tc_print"                else bug "unexpected TC_TOKEN tyc in tc_print"
191          | g (LK.TC_CONT ts) = "Cnt(" ^ (plist(tc_print,ts)) ^ ")"       | LT.TC_CONT ts => "Cnt(" ^ (plist(tc_print,ts)) ^ ")"
192          | g (LK.TC_IND _) = bug "unexpected TC_IND in tc_print"       | LT.TC_IND _ => bug "unexpected TC_IND in tc_print"
193          | g (LK.TC_ENV _) = bug "unexpected TC_ENV in tc_print"       | LT.TC_ENV _ => bug "unexpected TC_ENV in tc_print")
    in g (tc_out x)  
   end (* function tc_print *)  
194    
195  fun lt_print (x : lty) =  fun lt_print (x : lty) =
196    let fun h (i, t) = "(" ^ (itos i) ^ "," ^ (lt_print t) ^ ")"    (case lt_out x
197        of LT.LT_TYC t => tc_print t
198        fun g (LK.LT_TYC t) = tc_print t       | LT.LT_STR zs => "S{" ^ (plist(lt_print, zs)) ^ "}"
199          | g (LK.LT_STR zs) = "S{" ^ (plist(lt_print, zs)) ^ "}"       | LT.LT_FCT (ts1,ts2) =>
         | g (LK.LT_FCT (ts1,ts2)) =  
200               "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("               "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("
201                   ^ (plist(lt_print, ts2)) ^ ")"                   ^ (plist(lt_print, ts2)) ^ ")"
202          | g (LK.LT_POLY(ks, ts)) =       | LT.LT_POLY(ks, ts) =>
203               "(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"               "(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"
204          | g (LK.LT_CONT ts) = "CNT(" ^ (plist(lt_print, ts)) ^ ")"       | LT.LT_CONT ts => "CNT(" ^ (plist(lt_print, ts)) ^ ")"
205          | g (LK.LT_IND _) = bug "unexpected LT_IND in lt_print"       | LT.LT_IND _ => bug "unexpected LT_IND in lt_print"
206          | g (LK.LT_ENV _) = bug "unexpected LT_ENV in lt_print"       | LT.LT_ENV _ => bug "unexpected LT_ENV in lt_print")
207    
    in g (lt_out x)  
   end (* function lt_print *)  
208    
209  (** finding out the depth for a tyc's innermost-bound free variables *)  (** finding out the depth for a tyc's innermost-bound free variables *)
210  val tc_depth : tyc * depth -> depth = LK.tc_depth  val tc_depth : tyc * depth -> depth = LK.tc_depth
# Line 215  Line 213 
213  (** adjusting an lty or tyc from one depth to another *)  (** adjusting an lty or tyc from one depth to another *)
214  fun lt_adj (lt, d, nd) =  fun lt_adj (lt, d, nd) =
215    if d = nd then lt    if d = nd then lt
216    else ltc_env(lt, 0, nd - d, LK.initTycEnv)    else ltc_env(lt, 0, nd - d, LT.teEmpty)
217    
218  fun tc_adj (tc, d, nd) =  fun tc_adj (tc, d, nd) =
219    if d = nd then tc    if d = nd then tc
220    else tcc_env(tc, 0, nd - d, LK.initTycEnv)    else tcc_env(tc, 0, nd - d, LT.teEmpty)
221    
222  (** the following functions does the smiliar thing as lt_adj and  (** The following functions are similiar to lt_adj and tc_adj;
223      tc_adj; it adjusts an lty (or tyc) from depth d+k to depth nd+k,      they adjust an lty (or tyc) from depth d+k to depth nd+k,
224      assuming the last k levels are type abstractions. So lt_adj      assuming the last k levels are type abstractions. So lt_adj
225      is really lt_adj_k with k set to 0. Both functions are currently      is really lt_adj_k with k set to 0. Both functions are currently
226      called inside the lcontract.sml only. *)      called only in lcontract.sml. *)
227  local  local
228  fun mkTycEnv (i, k, dd, e) =  fun mkTycEnv (i, k, dd, te) =
229    if i >= k then e else mkTycEnv(i+1, k, dd, LK.tcInsert(e,(NONE, dd+i)))    if i >= k then te
230      else mkTycEnv(i+1, k, dd, LT.teCons(LT.Lamb(dd+i,[]),te))
231      (* dbm: no ks available *)
232    
233  in  in
234  fun lt_adj_k (lt, d, nd, k) =  fun lt_adj_k (lt, d, nd, k) =
235    if d = nd then lt    if d = nd then lt
236    else ltc_env(lt, k, nd-d+k, mkTycEnv(0, k, nd-d, LK.initTycEnv))    else ltc_env(lt, k, nd-d+k, mkTycEnv(0, k, nd-d, LT.teEmpty))
237    
238  fun tc_adj_k (tc, d, nd, k) =  fun tc_adj_k (tc, d, nd, k) =
239    if d = nd then tc    if d = nd then tc
240    else tcc_env(tc, k, nd-d+k, mkTycEnv(0, k, nd-d, LK.initTycEnv))    else tcc_env(tc, k, nd-d+k, mkTycEnv(0, k, nd-d, LT.teEmpty))
241    
242  end (* lt_adj_k and tc_adj_k *)  end (* lt_adj_k and tc_adj_k *)
243    
# Line 251  Line 251 
251   *            UTILITY FUNCTIONS ON TKIND ENVIRONMENT                       *   *            UTILITY FUNCTIONS ON TKIND ENVIRONMENT                       *
252   ***************************************************************************)   ***************************************************************************)
253    
254  type tkindEnv = LK.tkindEnv  type tkindEnv = LT.tkindEnv
255  exception tkUnbound = LK.tkUnbound  exception tkUnbound = LT.tkUnbound
256  val initTkEnv = LK.initTkEnv  val initTkEnv = LT.initTkEnv
257  val tkLookup = LK.tkLookup  val tkLookup = LT.tkLookup
258  val tkInsert = LK.tkInsert  val tkInsert = LT.tkInsert
259    
260  (***************************************************************************  (***************************************************************************
261   *            UTILITY FUNCTIONS ON TYC ENVIRONMENT                         *   *            UTILITY FUNCTIONS ON TYC ENVIRONMENT                         *
262   ***************************************************************************)   ***************************************************************************)
263    
264  exception tcUnbound = LK.tcUnbound  type tycEnv = LT.tycEnv
265  type tycEnv = LK.tycEnv  datatype teBinder = datatype LT.teBinder
266  val initTycEnv = LK.initTycEnv  val teEmpty = LT.teEmpty
267  val tcInsert = LK.tcInsert  val teCons = LT.teCons
268    
269  (***************************************************************************  (***************************************************************************
270   *            UTILITY FUNCTIONS ON LTY ENVIRONMENT                         *   *            UTILITY FUNCTIONS ON LTY ENVIRONMENT                         *
# Line 285  Line 285 
285        | SOME (lt, d) =>        | SOME (lt, d) =>
286            if d=nd then lt            if d=nd then lt
287            else if d > nd then bug "unexpected depth info in ltLookup"            else if d > nd then bug "unexpected depth info in ltLookup"
288                 else ltc_env(lt, 0, nd - d, LK.initTycEnv)                 else ltc_env(lt, 0, nd - d, LT.teEmpty)
289    (*easc*))    (*easc*))
290    
291  fun ltInsert (venv, lv, lt, d) = IntRedBlackMap.insert(venv, lv, (lt, d))  fun ltInsert (venv, lv, lt, d) = IntRedBlackMap.insert(venv, lv, (lt, d))

Legend:
Removed from v.2221  
changed lines
  Added in v.2222

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