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-2/src/compiler/FLINT/kernel/ltybasic.sml
ViewVC logotype

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

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

revision 2013, Fri Aug 11 04:09:23 2006 UTC revision 2014, Fri Aug 11 20:42:24 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 32  Line 33 
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) ^ ">"
# Line 47  Line 48 
48  open LtyDef  open 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 69  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 145  Line 146 
146   *            UTILITY FUNCTIONS FOR PRETTY PRINTING                        *   *            UTILITY FUNCTIONS FOR PRETTY PRINTING                        *
147   ***************************************************************************)   ***************************************************************************)
148    
149  (** pretty printing of tkinds, tycs, and ltys *)  (** (pretty?) printing of tkinds, tycs, and ltys -- see pplty.sml for real
150     ** pretty printing **)
151  fun tk_print (x : tkind) =  fun tk_print (x : tkind) =
152    let fun g (LK.TK_MONO) = "K0"    (case tk_out x
153          | g (LK.TK_BOX) = "KB0"      of LT.TK_MONO => "K0"
154          | g (LK.TK_FUN (ks, k)) =       | LT.TK_BOX => "KB0"
155         | LT.TK_FUN(ks, k) =>
156                 "<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"                 "<" ^ (plist(tk_print, ks)) ^ "->" ^ (tk_print k) ^ ">"
157          | 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  
158    
159  fun tc_print (x : tyc) =  fun tc_print (x : tyc) =
160    let fun g (LK.TC_VAR(i,j)) = "TV(" ^ (DI.di_print i) ^ "," ^ (itos j) ^ ")"    (case (tc_out x)
161          | g (LK.TC_NVAR v) = "NTV(v" ^ (itos v) ^ ")"      of LT.TC_VAR(i,j) => "TV(" ^ (DI.di_print i) ^ "," ^ (itos j) ^ ")"
162          | g (LK.TC_PRIM pt) = PT.pt_print pt       | LT.TC_NVAR v => "NTV(v" ^ (itos v) ^ ")"
163          | g (LK.TC_FN(ks, t)) =       | LT.TC_PRIM pt => PT.pt_print pt
164         | LT.TC_FN(ks, t) =>
165                "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"                "(\\[" ^ plist(tk_print, ks) ^ "]." ^ (tc_print t) ^ ")"
166          | g (LK.TC_APP(t, [])) = tc_print t ^ "[]"       | LT.TC_APP(t, []) => tc_print t ^ "[]"
167          | g (LK.TC_APP(t, zs)) =       | LT.TC_APP(t, zs) =>
168                (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"                (tc_print t) ^ "[" ^ (plist(tc_print, zs)) ^ "]"
169          | g (LK.TC_SEQ zs) = "TS(" ^ (plist(tc_print,zs)) ^ ")"       | LT.TC_SEQ zs => "TS(" ^ (plist(tc_print,zs)) ^ ")"
170          | g (LK.TC_PROJ (t, i)) =       | LT.TC_PROJ (t, i) =>
171                "TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"                "TP(" ^ (tc_print t) ^ "," ^ (itos i) ^ ")"
172          | g (LK.TC_SUM tcs) =       | LT.TC_SUM tcs =>
173                "TSUM(" ^ (plist(tc_print, tcs)) ^ ")"                "TSUM(" ^ (plist(tc_print, tcs)) ^ ")"
174          | g (LK.TC_FIX ((_, tc, ts), i)) =       | LT.TC_FIX ((_, tc, ts), i) =>
175                if tc_eqv(x,tcc_bool) then "B"                if tc_eqv(x,tcc_bool) then "B"
176                else if tc_eqv(x,tcc_list) then "LST"                else if tc_eqv(x,tcc_list) then "LST"
177                     else (let (* val ntc = case ts of [] => tc                     else (let (* val ntc = case ts of [] => tc
# Line 179  Line 181 
181                                      ^ "] &&" ^ (plist(tc_print, ts))                                      ^ "] &&" ^ (plist(tc_print, ts))
182                                            ^ "&&" ^*)  "===" ^ (itos i) ^ "}")                                            ^ "&&" ^*)  "===" ^ (itos i) ^ "}")
183                           end)                           end)
184          | g (LK.TC_ABS t) = "Ax(" ^ (tc_print t) ^ ")"       | LT.TC_ABS t => "Ax(" ^ (tc_print t) ^ ")"
185          | g (LK.TC_BOX t) = "Bx(" ^ (tc_print t) ^ ")"       | LT.TC_BOX t => "Bx(" ^ (tc_print t) ^ ")"
186          | g (LK.TC_TUPLE(_,zs)) = "TT<" ^ (plist(tc_print, zs)) ^ ">"       | LT.TC_TUPLE(_,zs) => "TT<" ^ (plist(tc_print, zs)) ^ ">"
187          | g (LK.TC_ARROW (ff,z1,z2)) =       | LT.TC_ARROW (ff,z1,z2) =>
188                 parw(fn u => plist(tc_print,u),(ff,z1,z2))                 parw(fn u => plist(tc_print,u),(ff,z1,z2))
189          | g (LK.TC_PARROW _) = bug "unexpected TC_PARROW in tc_print"       | LT.TC_PARROW _ => bug "unexpected TC_PARROW in tc_print"
190          | g (LK.TC_TOKEN (k, t)) =       | LT.TC_TOKEN (k, t) =>
191                if LK.token_isvalid k then           if LT.token_isvalid k then
192                   (LK.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"               (LT.token_abbrev k) ^ "(" ^ (tc_print t) ^ ")"
193                else bug "unexpected TC_TOKEN tyc in tc_print"                else bug "unexpected TC_TOKEN tyc in tc_print"
194          | g (LK.TC_CONT ts) = "Cnt(" ^ (plist(tc_print,ts)) ^ ")"       | LT.TC_CONT ts => "Cnt(" ^ (plist(tc_print,ts)) ^ ")"
195          | g (LK.TC_IND _) = bug "unexpected TC_IND in tc_print"       | LT.TC_IND _ => bug "unexpected TC_IND in tc_print"
196          | 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 *)  
197    
198  fun lt_print (x : lty) =  fun lt_print (x : lty) =
199    let fun h (i, t) = "(" ^ (itos i) ^ "," ^ (lt_print t) ^ ")"    (case lt_out x
200        of LT.LT_TYC t => tc_print t
201        fun g (LK.LT_TYC t) = tc_print t       | LT.LT_STR zs => "S{" ^ (plist(lt_print, zs)) ^ "}"
202          | g (LK.LT_STR zs) = "S{" ^ (plist(lt_print, zs)) ^ "}"       | LT.LT_FCT (ts1,ts2) =>
         | g (LK.LT_FCT (ts1,ts2)) =  
203               "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("               "(" ^ (plist(lt_print, ts1)) ^ ") ==> ("
204                   ^ (plist(lt_print, ts2)) ^ ")"                   ^ (plist(lt_print, ts2)) ^ ")"
205          | g (LK.LT_POLY(ks, ts)) =       | LT.LT_POLY(ks, ts) =>
206               "(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"               "(Q[" ^ plist(tk_print, ks) ^ "]." ^ (plist(lt_print,ts)) ^ ")"
207          | g (LK.LT_CONT ts) = "CNT(" ^ (plist(lt_print, ts)) ^ ")"       | LT.LT_CONT ts => "CNT(" ^ (plist(lt_print, ts)) ^ ")"
208          | g (LK.LT_IND _) = bug "unexpected LT_IND in lt_print"       | LT.LT_IND _ => bug "unexpected LT_IND in lt_print"
209          | g (LK.LT_ENV _) = bug "unexpected LT_ENV in lt_print"       | LT.LT_ENV _ => bug "unexpected LT_ENV in lt_print")
   
    in g (lt_out x)  
   end (* function lt_print *)  
210    
211  (** finding out the depth for a tyc's innermost-bound free variables *)  (** finding out the depth for a tyc's innermost-bound free variables *)
212  val tc_depth : tyc * depth -> depth = LK.tc_depth  val tc_depth : tyc * depth -> depth = LK.tc_depth
# Line 219  Line 215 
215  (** adjusting an lty or tyc from one depth to another *)  (** adjusting an lty or tyc from one depth to another *)
216  fun lt_adj (lt, d, nd) =  fun lt_adj (lt, d, nd) =
217    if d = nd then lt    if d = nd then lt
218    else ltc_env(lt, 0, nd - d, LK.initTycEnv)    else ltc_env(lt, 0, nd - d, LT.initTycEnv)
219    
220  fun tc_adj (tc, d, nd) =  fun tc_adj (tc, d, nd) =
221    if d = nd then tc    if d = nd then tc
222    else tcc_env(tc, 0, nd - d, LK.initTycEnv)    else tcc_env(tc, 0, nd - d, LT.initTycEnv)
223    
224  (** the following functions does the smiliar thing as lt_adj and  (** The following functions are similiar to lt_adj and tc_adj;
225      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,
226      assuming the last k levels are type abstractions. So lt_adj      assuming the last k levels are type abstractions. So lt_adj
227      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
228      called inside the lcontract.sml only. *)      called only in lcontract.sml. *)
229  local  local
230  fun mkTycEnv (i, k, dd, e) =  fun mkTycEnv (i, k, dd, e) =
231    if i >= k then e else mkTycEnv(i+1, k, dd, LK.tcInsert(e,(NONE, dd+i)))    if i >= k then e else mkTycEnv(i+1, k, dd, LT.tcInsert(e,(NONE, dd+i)))
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.initTycEnv))
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.initTycEnv))
241    
242  end (* lt_adj_k and tc_adj_k *)  end (* lt_adj_k and tc_adj_k *)
243    
# Line 255  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  exception tcUnbound = LT.tcUnbound
265  type tycEnv = LK.tycEnv  type tycEnv = LT.tycEnv
266  val initTycEnv = LK.initTycEnv  val initTycEnv = LT.initTycEnv
267  val tcInsert = LK.tcInsert  val tcInsert = LT.tcInsert
268    
269  (***************************************************************************  (***************************************************************************
270   *            UTILITY FUNCTIONS ON LTY ENVIRONMENT                         *   *            UTILITY FUNCTIONS ON LTY ENVIRONMENT                         *
# Line 289  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.initTycEnv)
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.2013  
changed lines
  Added in v.2014

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